Two tweaks to previous change.

1. Don't allow the wrong monad in a bind whose pattern is a tuple
pattern. The old saw produces a type error for that so we don't have
to allow it now.

2. For binds in the wrong monad, unify the pattern type with the full
wrong monadic type of the expression, not just the associated value
type. This assigns the variables in the pattern types in the wrong
monad, which matches both the historical behavior and also what
happens inside the interpreter during execution.

It also turns out that binds in the wrong monad with an explicit type
signature expecting the bind to work didn't typecheck in the old saw.
So we don't need to make that work as part of the workarounds either.

Add three more test cases...

intTests/test_type_errors/err010.log.good

@@ -0,0 +1,4 @@
+ Loading file "err010.saw"
+ err010.saw:12:1-12:9: Warning: Monadic bind with the wrong monad; found LLVMSetup but expected TopLevel
+ err010.saw:12:1-12:9: Warning: This was historically ignored and will have no effect; if you really want to do this, prefix the expression with return
+ err010.saw:12:1-12:9: Warning: This will become an error in a future release of SAW

intTests/test_type_errors/err010.saw

@@ -0,0 +1,12 @@
+// This was allowed prior to Dec 2024 and is currently a warning;
+// should eventually become an error.
+//
+// This case checks what happens if you take a tuple in the wrong
+// monad and bind it to a single value.
+
+let f x = do {
+   llvm_assert {{ True }};
+   return (x, x);
+};
+
+a <- f 0;

intTests/test_type_errors/err011.log.good

@@ -0,0 +1,15 @@
+ Loading file "err011.saw"
+ err011.saw:11:11-11:14: Type mismatch.
+    Mismatch of type constructors. Expected: TopLevel but got LLVMSetup
+    err011.saw:11:1-11:14: The type TopLevel arises from this type annotation
+    internal:1:9-1:18: The type LLVMSetup arises from this type annotation
+
+    Expected: TopLevel
+    Found:    LLVMSetup
+
+    Expected: TopLevel (t.0, t.1)
+    Found:    LLVMSetup (Int, Int)
+
+    within "<toplevel>" (err011.saw:11:1-11:14)
+
+FAILED

intTests/test_type_errors/err011.saw

@@ -0,0 +1,11 @@
+// This was not allowed even prior to Dec 2024.
+//
+// This case checks what happens if you take a tuple in the wrong
+// monad and bind it to a tuple pattern.
+
+let f x = do {
+   llvm_assert {{ True }};
+   return (x, x);
+};
+
+(a, b) <- f 0;

intTests/test_type_errors/err012.log.good

@@ -0,0 +1,15 @@
+ Loading file "err012.saw"
+ err012.saw:12:2-12:17: Warning: Monadic bind with the wrong monad; found LLVMSetup but expected TopLevel
+ err012.saw:12:2-12:17: Warning: This was historically ignored and will have no effect; if you really want to do this, prefix the expression with return
+ err012.saw:12:2-12:17: Warning: This will become an error in a future release of SAW
+ err012.saw:12:14-12:17: Type mismatch.
+    Mismatch of type constructors. Expected: Int but got <Block>
+    err012.saw:12:6-12:9: The type Int arises from this type annotation
+    err012.saw:12:2-12:17: The type LLVMSetup Int arises from this type annotation
+
+    Expected: Int
+    Found:    LLVMSetup Int
+
+    within "<toplevel>" (err012.saw:12:2-12:17)
+
+FAILED

intTests/test_type_errors/err012.saw

@@ -0,0 +1,12 @@
+// This was not allowed even prior to Dec 2024.
+//
+// This case checks what happens if you take a value in the wrong
+// monad and bind it to a pattern that includes a type signature.
+
+let f x = do {
+   llvm_assert {{ True }};
+   return x;
+};
+
+// note that you need the parens because of a possibly silly parser issue
+(a : Int) <- f 3;

src/SAWScript/MGU.hs

@@ -1165,10 +1165,25 @@ inferStmt ln atSyntacticTopLevel blockpos ctx s =
                                        "expression with return"
                   recordWarning spos $ "This will become an error in a " ++
                                        "future release of SAW"
-                  unify ln pty (getPos e') valty'
-                  -- Wrap the expression in "return" so the variable, if any,
-                  -- gets bound to a value of type m t instead of type t, which
-                  -- is the historic behavior.
+
+                  -- The historic behavior is that the pattern gets bound
+                  -- to a value of type m t instead of type t. This means:
+                  --    - we should unify pty, which is the type of the
+                  --      pattern, with m t, which is tBlock ctx' valty'
+                  --      (rather than tBlock ctx valty', which is the
+                  --      type we should be getting)
+                  --    - this will fail if the pattern includes a type
+                  --      signature with a non-monad type, but that's ok
+                  --      because that case also fails in old SAW
+                  --    - we do _not_ need to update pty before returning
+                  --      it out of inferStmt
+                  --    - we _do_ need to wrap the expression in "return"
+                  --      so that the ultimate results are well-typed and
+                  --      happen in the TopLevel monad
+                  unify ln pty (getPos e') (tBlock spos ctx' valty')
+
+                  -- Wrap the expression in "return" to produce an
+                  -- expression of type TopLevel (m t).
                   return $ wrapReturn e'
 
             -- Figure out which case applies.
@@ -1181,7 +1196,14 @@ inferStmt ln atSyntacticTopLevel blockpos ctx s =
                         restrictToCorrect
                     else
                         case monadType ty' of
-                            Just (ctx', valty') -> allowWrongMonad ctx' valty'
+                            Just (ctx', valty') ->
+                               -- Allow it only for _ and a single var.
+                               -- Binding elements of a tuple this way
+                               -- failed typecheck in the old saw and
+                               -- doesn't need to be allowed now.
+                               case pat of
+                                   PTuple _ _ -> restrictToCorrect
+                                   _ -> allowWrongMonad ctx' valty'
                             Nothing ->
                                -- allow it only if actually binding something
                                -- (just proclaiming a value by itself is not a