diff --git a/CHANGES.md b/CHANGES.md
index 59de003989..de710bf21b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -11,13 +11,53 @@
 
 ## Bug fixes
 
+* Unexpected special-case type behavior of monad binds in the
+  syntactic top level has been removed.
+  (This was _not_ specifically associated with the TopLevel monad, so
+  top-level binds and binds in functions in TopLevel, or in nested
+  do-blocks, would behave differently.)
+  See issue #2162.
+
+  There are three primary visible consequences.
+  The first is that the REPL no longer accepts
+  non-monadic expressions.
+  These can still be evaluated and printed; just prefix them with
+  ```return```.
+  (Affordances specifically for the REPL so this is not required there
+  may be restored in the future.)
+
+  The second is that statements of the form ```x <- e;``` where ```e```
+  is a pure (non-monadic) term used to be (improperly) accepted at the
+  top level of scripts.
+  These statements now generate a warning.
+  This will become an error in a future release and such statements
+  should be rewritten as ```let x = e;```.
+  For example, ```t <- unfold_term ["reverse"] {{ reverse 0b01 }};```
+  should be changed to ```let t = unfold_term ["reverse"] {{ reverse 0b01 }};```.
+
+  The third is that statements of the form ```x <- s;``` or just ```s;```
+  where ```s``` is a term in the _wrong_ monad also used to be
+  improperly accepted at the top level of scripts.
+  These statements silently did nothing.
+  They will now generate a warning.
+  This will become an error in a future release.
+  Such statements should be removed or rewritten.
+  For example, it used to be possible to write ```llvm_assert {{ False }};```
+  at the top level (outside any specification) and it would be ignored.
+  ```llvm_assert``` is only meaningful within an LLVM specification.
+
 * A number of SAWScript type checking problems have been fixed,
-including issue #2077.
-Some of these problems were partially mutually compensating; for
-example, in some cases nonexistent typedefs had been mishandled in
-ways that made them mostly work.
-Some previously accepted scripts and specs may be rejected and need
-(generally minor) adjustment.
+  including issue #2077.
+  Some previously accepted scripts and specs may be rejected and need
+  (generally minor) adjustment.
+  Prior to these changes the typechecker allowed unbound type variables
+  in a number of places (such as on the right-hand side of typedefs, and
+  in function signatures), so for example type names contaning typos
+  would not necessarily have been caught and will now fail.
+  ```typedef t = nonexistent``` was previously accepted and now is not.
+  These problems could trigger panics, but there does not appear to have
+  been any way to produce unsoundness in the sense of false
+  verifications.
 
 * Counterexamples including SMT arrays are now printed with the array
   contents instead of placeholder text.
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index 3cdcf54888..2ee1e23fbc 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -3353,8 +3353,8 @@ look up `S<u8, u16>` and `S<u32, u64>` from the example above as `MIRAdt`s:
 ~~~~
 m <- mir_load_module "example.linked-mir.json";
 
-s_8_16  <- mir_find_adt m "example::S" [mir_u8,  mir_u16];
-s_32_64 <- mir_find_adt m "example::S" [mir_u32, mir_u64];
+let s_8_16  = mir_find_adt m "example::S" [mir_u8,  mir_u16];
+let s_32_64 = mir_find_adt m "example::S" [mir_u32, mir_u64];
 ~~~~
 
 The `mir_adt` command (for constructing a struct type), `mir_struct_value` (for
@@ -3384,7 +3384,7 @@ pub fn s(x: u32) -> Option<u32> {
 ~~~~
 m <- mir_load_module "example.linked-mir.json";
 
-option_u32 <- mir_find_adt m "core::option::Option" [mir_u32];
+let option_u32 = mir_find_adt m "core::option::Option" [mir_u32];
 
 let n_spec = do {
   mir_execute_func [];
diff --git a/doc/rust-tutorial/code/enums.saw b/doc/rust-tutorial/code/enums.saw
index c45c4b67f5..05c337a6ce 100644
--- a/doc/rust-tutorial/code/enums.saw
+++ b/doc/rust-tutorial/code/enums.saw
@@ -2,7 +2,7 @@ enable_experimental;
 
 m <- mir_load_module "enums.linked-mir.json";
 
-option_u32 <- mir_find_adt m "core::option::Option" [mir_u32];
+let option_u32 = mir_find_adt m "core::option::Option" [mir_u32];
 
 let i_found_something_spec = do {
   x <- mir_fresh_var "x" mir_u32;
diff --git a/doc/rust-tutorial/code/structs.saw b/doc/rust-tutorial/code/structs.saw
index be8d957c92..e08eca0212 100644
--- a/doc/rust-tutorial/code/structs.saw
+++ b/doc/rust-tutorial/code/structs.saw
@@ -2,9 +2,9 @@ enable_experimental;
 
 m <- mir_load_module "structs.linked-mir.json";
 
-s_adt <- mir_find_adt m "structs::S" [];
-t_adt <- mir_find_adt m "structs::T" [];
-foo_adt <- mir_find_adt m "structs::Foo" [mir_u32, mir_u64];
+let s_adt = mir_find_adt m "structs::S" [];
+let t_adt = mir_find_adt m "structs::T" [];
+let foo_adt = mir_find_adt m "structs::Foo" [mir_u32, mir_u64];
 
 let make_foo_spec = do {
   mir_execute_func [];
@@ -17,7 +17,7 @@ let make_foo_spec = do {
 
 mir_verify m "structs::make_foo" [] false make_foo_spec z3;
 
-bar_adt <- mir_find_adt m "structs::Bar" [];
+let bar_adt = mir_find_adt m "structs::Bar" [];
 
 let do_stuff_with_bar_spec1 = do {
   z1 <- mir_fresh_var "z1" mir_u32;
diff --git a/examples/misc/rewrite.saw b/examples/misc/rewrite.saw
index 0a5debedcf..3e8559c162 100644
--- a/examples/misc/rewrite.saw
+++ b/examples/misc/rewrite.saw
@@ -7,7 +7,7 @@ rule_thm <- prove_print (admit "assume rule") rule;
 print "== Original version of rule:";
 print_term rule;
 let rule_ss = addsimps [rule_thm] empty_ss;
-t <- rewrite rule_ss rule;
+let t = rewrite rule_ss rule;
 print "== Rule rewritten with itself:";
 print_term t;
 print "== Proof result:";
diff --git a/examples/mr_solver/monadify.saw b/examples/mr_solver/monadify.saw
index 20a382d7d1..e174a18c45 100644
--- a/examples/mr_solver/monadify.saw
+++ b/examples/mr_solver/monadify.saw
@@ -21,8 +21,8 @@ let run_test name cry_term mon_term_expected =
               print_term mon_term_expected;
               exit 1; }; };
 
-my_abs <- unfold_term ["my_abs"] {{ my_abs }};
-my_abs_M <- parse_core_mod "CryptolM" "\
+let my_abs = unfold_term ["my_abs"] {{ my_abs }};
+let my_abs_M = parse_core_mod "CryptolM" "\
 \ \\(x : (mseq VoidEv (TCNum 64) Bool)) -> \
 \   bindS VoidEv (isFinite (TCNum 64)) \
 \         (mseq VoidEv (TCNum 64) Bool) \
@@ -45,8 +45,8 @@ my_abs_M <- parse_core_mod "CryptolM" "\
 \               (retS VoidEv (mseq VoidEv (TCNum 64) Bool) x)))";
 run_test "my_abs" my_abs my_abs_M;
 
-err_if_lt0 <- unfold_term ["err_if_lt0"] {{ err_if_lt0 }};
-err_if_lt0_M <- parse_core_mod "CryptolM" "\
+let err_if_lt0 = unfold_term ["err_if_lt0"] {{ err_if_lt0 }};
+let err_if_lt0_M = parse_core_mod "CryptolM" "\
 \ \\(x : (mseq VoidEv (TCNum 64) Bool)) -> \
 \   bindS VoidEv (isFinite (TCNum 64)) (mseq VoidEv (TCNum 64) Bool) (assertFiniteS VoidEv (TCNum 64)) \
 \     (\\(x' : (isFinite (TCNum 64))) -> \
@@ -77,8 +77,8 @@ print "Monadified term:";
 print_term sha1M;
 */
 
-fib <- unfold_term ["fib"] {{ fib }};
-fibM <- parse_core_mod "CryptolM" "\
+let fib = unfold_term ["fib"] {{ fib }};
+let fibM = parse_core_mod "CryptolM" "\
 \ \\(_x : Vec 64 Bool) -> \
 \    FixS VoidEv (Tp_Arr (Tp_bitvector 64) (Tp_M (Tp_bitvector 64))) \
 \      (\\(fib : (Vec 64 Bool -> SpecM VoidEv (Vec 64 Bool))) -> \
@@ -115,12 +115,12 @@ fibM <- parse_core_mod "CryptolM" "\
 \      _x";
 run_test "fib" fib fibM;
 
-noErrors <- unfold_term ["noErrors"] {{ SpecPrims::noErrors }};
-noErrorsM <- parse_core_mod "CryptolM" "\\(a : sort 0) -> existsS VoidEv a";
+let noErrors = unfold_term ["noErrors"] {{ SpecPrims::noErrors }};
+let noErrorsM = parse_core_mod "CryptolM" "\\(a : sort 0) -> existsS VoidEv a";
 run_test "noErrors" noErrors noErrorsM;
 
-fibSpecNoErrors <- unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }};
-fibSpecNoErrorsM <- parse_core_mod "CryptolM" "\
+let fibSpecNoErrors = unfold_term ["fibSpecNoErrors"] {{ fibSpecNoErrors }};
+let fibSpecNoErrorsM = parse_core_mod "CryptolM" "\
 \ \\(__p1 : (mseq VoidEv (TCNum 64) Bool)) -> \
 \   existsS VoidEv (mseq VoidEv (TCNum 64) Bool)";
 run_test "fibSpecNoErrors" fibSpecNoErrors fibSpecNoErrorsM;
diff --git a/examples/mr_solver/mr_solver_unit_tests.saw b/examples/mr_solver/mr_solver_unit_tests.saw
index ac0f9482d4..870f50521b 100644
--- a/examples/mr_solver/mr_solver_unit_tests.saw
+++ b/examples/mr_solver/mr_solver_unit_tests.saw
@@ -19,11 +19,11 @@ let run_test name test expected =
 // The constant 0 function const0 x = 0
 let ret0_core = "retS VoidEv (Vec 64 Bool) (bvNat 64 0)";
 let const0_core = str_concat "\\ (_:Vec 64 Bool) -> " ret0_core;
-const0 <- parse_core_mod "SpecM" const0_core;
+let const0 = parse_core_mod "SpecM" const0_core;
 
 // The constant 1 function const1 x = 1
 let const1_core = "\\ (_:Vec 64 Bool) -> retS VoidEv (Vec 64 Bool) (bvNat 64 1)";
-const1 <- parse_core_mod "SpecM" const1_core;
+let const1 = parse_core_mod "SpecM" const1_core;
 
 // const0 <= const0
 prove_extcore mrsolver (refines [] const0 const0);
@@ -41,7 +41,7 @@ run_test "refines [x] (const0 x) (const0 x)"
                                       (term_apply const0 [x]))) true;
 
 // The function test_fun0 <= const0
-test_fun0 <- parse_core_mod "test_funs" "test_fun0";
+let test_fun0 = parse_core_mod "test_funs" "test_fun0";
 prove_extcore mrsolver (refines [] const0 test_fun0);
 // (testing that "refines [] const0 test_fun0" is actually "const0 <= test_fun0")
 let const0_test_fun0_refines =
@@ -60,7 +60,7 @@ run_test "refines [] const0 const1" (is_convertible (parse_core_mod "SpecM" cons
                                                     (refines [] const0 const1)) true;
 
 // The function test_fun1 = const1
-test_fun1 <- parse_core_mod "test_funs" "test_fun1";
+let test_fun1 = parse_core_mod "test_funs" "test_fun1";
 prove_extcore mrsolver (refines [] const1 test_fun1);
 fails (prove_extcore mrsolver (refines [] const0 test_fun1));
 // (testing that "refines [] const1 test_fun1" is actually "const1 <= test_fun1")
@@ -82,7 +82,7 @@ let ifxEq0_core = "\\ (x:Vec 64 Bool) -> \
                        \     (bvEq 64 x (bvNat 64 0)) \
                        \     (retS VoidEv (Vec 64 Bool) x) \
                        \     (retS VoidEv (Vec 64 Bool) (bvNat 64 0))";
-ifxEq0 <- parse_core_mod "SpecM" ifxEq0_core;
+let ifxEq0 = parse_core_mod "SpecM" ifxEq0_core;
 
 // ifxEq0 <= const0
 prove_extcore mrsolver (refines [] ifxEq0 const0);
@@ -106,7 +106,7 @@ run_test "refines [] ifxEq0 const1" (is_convertible (parse_core_mod "SpecM" ifxE
 // noErrors1 x = existsS x. retS x
 let noErrors1_core =
   "\\ (_:Vec 64 Bool) -> existsS VoidEv (Vec 64 Bool)";
-noErrors1 <- parse_core_mod "SpecM" noErrors1_core;
+let noErrors1 = parse_core_mod "SpecM" noErrors1_core;
 
 // const0 <= noErrors
 prove_extcore mrsolver (refines [] noErrors1 noErrors1);
@@ -136,14 +136,14 @@ let noErrorsRec1_core =
               \ (Vec 64 Bool) \
               \ (existsS VoidEv (Vec 64 Bool)) \
               \ (f x))";
-noErrorsRec1 <- parse_core_mod "SpecM" noErrorsRec1_core;
+let noErrorsRec1 = parse_core_mod "SpecM" noErrorsRec1_core;
 
 // loop x = loop x
 let loop1_core =
   "FixS VoidEv (Tp_Arr (Tp_bitvector 64) (Tp_M (Tp_bitvector 64))) \
       \ (\\ (f: Vec 64 Bool -> SpecM VoidEv (Vec 64 Bool)) \
           \ (x:Vec 64 Bool) -> f x)";
-loop1 <- parse_core_mod "SpecM" loop1_core;
+let loop1 = parse_core_mod "SpecM" loop1_core;
 
 // loop1 <= noErrorsRec1
 prove_extcore mrsolver (refines [] loop1 noErrorsRec1);
diff --git a/heapster-saw/examples/Dilithium2.saw b/heapster-saw/examples/Dilithium2.saw
index 89a45c9d20..a62f408887 100644
--- a/heapster-saw/examples/Dilithium2.saw
+++ b/heapster-saw/examples/Dilithium2.saw
@@ -301,49 +301,49 @@ heapster_typecheck_fun_rename env "pqcrystals_dilithium2_ref_verify" "crypto_sig
 // The saw-core terms generated by Heapster //
 //////////////////////////////////////////////
 
-randombytes <- parse_core_mod "Dilithium2" "randombytes";
-shake256_init <- parse_core_mod "Dilithium2" "shake256_init";
-shake256_absorb <- parse_core_mod "Dilithium2" "shake256_absorb";
-shake256_finalize <- parse_core_mod "Dilithium2" "shake256_finalize";
-shake256_squeeze <- parse_core_mod "Dilithium2" "shake256_squeeze";
-shake256 <- parse_core_mod "Dilithium2" "shake256";
-poly_challenge <- parse_core_mod "Dilithium2" "poly_challenge";
-poly_ntt <- parse_core_mod "Dilithium2" "poly_ntt";
-polyvec_matrix_expand <- parse_core_mod "Dilithium2" "polyvec_matrix_expand";
-polyvec_matrix_pointwise_montgomery <- parse_core_mod "Dilithium2" "polyvec_matrix_pointwise_montgomery";
-polyvecl_uniform_eta <- parse_core_mod "Dilithium2" "polyvecl_uniform_eta";
-polyvecl_uniform_gamma1 <- parse_core_mod "Dilithium2" "polyvecl_uniform_gamma1";
-polyvecl_reduce <- parse_core_mod "Dilithium2" "polyvecl_reduce";
-polyvecl_add <- parse_core_mod "Dilithium2" "polyvecl_add";
-polyvecl_ntt <- parse_core_mod "Dilithium2" "polyvecl_ntt";
-polyvecl_invntt_tomont <- parse_core_mod "Dilithium2" "polyvecl_invntt_tomont";
-polyvecl_pointwise_poly_montgomery <- parse_core_mod "Dilithium2" "polyvecl_pointwise_poly_montgomery";
-polyvecl_chknorm <- parse_core_mod "Dilithium2" "polyvecl_chknorm";
-polyveck_uniform_eta <- parse_core_mod "Dilithium2" "polyveck_uniform_eta";
-polyveck_reduce <- parse_core_mod "Dilithium2" "polyveck_reduce";
-polyveck_caddq <- parse_core_mod "Dilithium2" "polyveck_caddq";
-polyveck_add <- parse_core_mod "Dilithium2" "polyveck_add";
-polyveck_sub <- parse_core_mod "Dilithium2" "polyveck_sub";
-polyveck_shiftl <- parse_core_mod "Dilithium2" "polyveck_shiftl";
-polyveck_ntt <- parse_core_mod "Dilithium2" "polyveck_ntt";
-polyveck_invntt_tomont <- parse_core_mod "Dilithium2" "polyveck_invntt_tomont";
-polyveck_pointwise_poly_montgomery <- parse_core_mod "Dilithium2" "polyveck_pointwise_poly_montgomery";
-polyveck_chknorm <- parse_core_mod "Dilithium2" "polyveck_chknorm";
-polyveck_power2round <- parse_core_mod "Dilithium2" "polyveck_power2round";
-polyveck_decompose <- parse_core_mod "Dilithium2" "polyveck_decompose";
-polyveck_make_hint <- parse_core_mod "Dilithium2" "polyveck_make_hint";
-polyveck_use_hint <- parse_core_mod "Dilithium2" "polyveck_use_hint";
-polyveck_pack_w1 <- parse_core_mod "Dilithium2" "polyveck_pack_w1";
-pack_pk <- parse_core_mod "Dilithium2" "pack_pk";
-unpack_pk <- parse_core_mod "Dilithium2" "unpack_pk";
-pack_sk <- parse_core_mod "Dilithium2" "pack_sk";
-unpack_sk <- parse_core_mod "Dilithium2" "unpack_sk";
-pack_sig <- parse_core_mod "Dilithium2" "pack_sig";
-unpack_sig <- parse_core_mod "Dilithium2" "unpack_sig";
-crypto_sign_keypair <- parse_core_mod "Dilithium2" "crypto_sign_keypair";
-crypto_sign_signature <- parse_core_mod "Dilithium2" "crypto_sign_signature";
-crypto_sign <- parse_core_mod "Dilithium2" "crypto_sign";
-crypto_sign_verify <- parse_core_mod "Dilithium2" "crypto_sign_verify";
+let randombytes = parse_core_mod "Dilithium2" "randombytes";
+let shake256_init = parse_core_mod "Dilithium2" "shake256_init";
+let shake256_absorb = parse_core_mod "Dilithium2" "shake256_absorb";
+let shake256_finalize = parse_core_mod "Dilithium2" "shake256_finalize";
+let shake256_squeeze = parse_core_mod "Dilithium2" "shake256_squeeze";
+let shake256 = parse_core_mod "Dilithium2" "shake256";
+let poly_challenge = parse_core_mod "Dilithium2" "poly_challenge";
+let poly_ntt = parse_core_mod "Dilithium2" "poly_ntt";
+let polyvec_matrix_expand = parse_core_mod "Dilithium2" "polyvec_matrix_expand";
+let polyvec_matrix_pointwise_montgomery = parse_core_mod "Dilithium2" "polyvec_matrix_pointwise_montgomery";
+let polyvecl_uniform_eta = parse_core_mod "Dilithium2" "polyvecl_uniform_eta";
+let polyvecl_uniform_gamma1 = parse_core_mod "Dilithium2" "polyvecl_uniform_gamma1";
+let polyvecl_reduce = parse_core_mod "Dilithium2" "polyvecl_reduce";
+let polyvecl_add = parse_core_mod "Dilithium2" "polyvecl_add";
+let polyvecl_ntt = parse_core_mod "Dilithium2" "polyvecl_ntt";
+let polyvecl_invntt_tomont = parse_core_mod "Dilithium2" "polyvecl_invntt_tomont";
+let polyvecl_pointwise_poly_montgomery = parse_core_mod "Dilithium2" "polyvecl_pointwise_poly_montgomery";
+let polyvecl_chknorm = parse_core_mod "Dilithium2" "polyvecl_chknorm";
+let polyveck_uniform_eta = parse_core_mod "Dilithium2" "polyveck_uniform_eta";
+let polyveck_reduce = parse_core_mod "Dilithium2" "polyveck_reduce";
+let polyveck_caddq = parse_core_mod "Dilithium2" "polyveck_caddq";
+let polyveck_add = parse_core_mod "Dilithium2" "polyveck_add";
+let polyveck_sub = parse_core_mod "Dilithium2" "polyveck_sub";
+let polyveck_shiftl = parse_core_mod "Dilithium2" "polyveck_shiftl";
+let polyveck_ntt = parse_core_mod "Dilithium2" "polyveck_ntt";
+let polyveck_invntt_tomont = parse_core_mod "Dilithium2" "polyveck_invntt_tomont";
+let polyveck_pointwise_poly_montgomery = parse_core_mod "Dilithium2" "polyveck_pointwise_poly_montgomery";
+let polyveck_chknorm = parse_core_mod "Dilithium2" "polyveck_chknorm";
+let polyveck_power2round = parse_core_mod "Dilithium2" "polyveck_power2round";
+let polyveck_decompose = parse_core_mod "Dilithium2" "polyveck_decompose";
+let polyveck_make_hint = parse_core_mod "Dilithium2" "polyveck_make_hint";
+let polyveck_use_hint = parse_core_mod "Dilithium2" "polyveck_use_hint";
+let polyveck_pack_w1 = parse_core_mod "Dilithium2" "polyveck_pack_w1";
+let pack_pk = parse_core_mod "Dilithium2" "pack_pk";
+let unpack_pk = parse_core_mod "Dilithium2" "unpack_pk";
+let pack_sk = parse_core_mod "Dilithium2" "pack_sk";
+let unpack_sk = parse_core_mod "Dilithium2" "unpack_sk";
+let pack_sig = parse_core_mod "Dilithium2" "pack_sig";
+let unpack_sig = parse_core_mod "Dilithium2" "unpack_sig";
+let crypto_sign_keypair = parse_core_mod "Dilithium2" "crypto_sign_keypair";
+let crypto_sign_signature = parse_core_mod "Dilithium2" "crypto_sign_signature";
+let crypto_sign = parse_core_mod "Dilithium2" "crypto_sign";
+let crypto_sign_verify = parse_core_mod "Dilithium2" "crypto_sign_verify";
 
 
 ////////////////////////////////////////////////////
diff --git a/heapster-saw/examples/arrays_mr_solver.saw b/heapster-saw/examples/arrays_mr_solver.saw
index a67d31ec6a..21c9f2f453 100644
--- a/heapster-saw/examples/arrays_mr_solver.saw
+++ b/heapster-saw/examples/arrays_mr_solver.saw
@@ -1,10 +1,10 @@
 include "arrays.saw";
 
 // Test that contains0 |= contains0
-contains0 <- parse_core_mod "arrays" "contains0";
+let contains0 = parse_core_mod "arrays" "contains0";
 prove_extcore mrsolver (refines [] contains0 contains0);
 
-noErrorsContains0 <- parse_core_mod "arrays" "noErrorsContains0";
+let noErrorsContains0 = parse_core_mod "arrays" "noErrorsContains0";
 prove_extcore mrsolver (refines [] contains0 noErrorsContains0);
 
 include "specPrims.saw";
@@ -13,6 +13,6 @@ import "arrays.cry";
 monadify_term {{ zero_array_spec }};
 
 // FIXME: Uncomment once FunStacks are removed
-zero_array <- parse_core_mod "arrays" "zero_array";
+let zero_array = parse_core_mod "arrays" "zero_array";
 prove_extcore mrsolver (refines [] zero_array {{ zero_array_loop_spec }});
 prove_extcore mrsolver (refines [] zero_array {{ zero_array_spec }});
diff --git a/heapster-saw/examples/exp_explosion_mr_solver.saw b/heapster-saw/examples/exp_explosion_mr_solver.saw
index 0cf92af63e..f4833cd98f 100644
--- a/heapster-saw/examples/exp_explosion_mr_solver.saw
+++ b/heapster-saw/examples/exp_explosion_mr_solver.saw
@@ -2,5 +2,5 @@ include "exp_explosion.saw";
 
 import "exp_explosion.cry";
 
-exp_explosion <- parse_core_mod "exp_explosion" "exp_explosion";
+let exp_explosion = parse_core_mod "exp_explosion" "exp_explosion";
 prove_extcore mrsolver (refines [] exp_explosion {{ exp_explosion_spec }});
diff --git a/heapster-saw/examples/linked_list_mr_solver.saw b/heapster-saw/examples/linked_list_mr_solver.saw
index a64acdef73..9eec7bf536 100644
--- a/heapster-saw/examples/linked_list_mr_solver.saw
+++ b/heapster-saw/examples/linked_list_mr_solver.saw
@@ -26,10 +26,10 @@ heapster_typecheck_fun env "is_head"
   "(). arg0:int64<>, arg1:List<int64<>,always,R> -o \
      \ arg0:true, arg1:true, ret:int64<>";
 
-is_head <- parse_core_mod "linked_list" "is_head";
+let is_head = parse_core_mod "linked_list" "is_head";
 prove_extcore mrsolver (refines [] is_head is_head);
 
-is_elem <- parse_core_mod "linked_list" "is_elem";
+let is_elem = parse_core_mod "linked_list" "is_elem";
 prove_extcore mrsolver (refines [] is_elem is_elem);
 
 is_elem_noErrorsSpec <- parse_core
@@ -61,5 +61,5 @@ monadify_term {{ Left }};
 monadify_term {{ nil }};
 monadify_term {{ cons }};
 
-sorted_insert_no_malloc <- parse_core_mod "linked_list" "sorted_insert_no_malloc";
+let sorted_insert_no_malloc = parse_core_mod "linked_list" "sorted_insert_no_malloc";
 prove_extcore mrsolver (refines [] sorted_insert_no_malloc {{ sorted_insert_spec }});
diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw
index 27d38a002d..5a41fd28a8 100644
--- a/heapster-saw/examples/sha512_mr_solver.saw
+++ b/heapster-saw/examples/sha512_mr_solver.saw
@@ -1,9 +1,9 @@
 include "sha512.saw";
 
-round_00_15 <- parse_core_mod "SHA512" "round_00_15";
-round_16_80 <- parse_core_mod "SHA512" "round_16_80";
-processBlock <- parse_core_mod "SHA512" "processBlock";
-processBlocks <- parse_core_mod "SHA512" "processBlocks";
+let round_00_15= parse_core_mod "SHA512" "round_00_15";
+let round_16_80 = parse_core_mod "SHA512" "round_16_80";
+let processBlock = parse_core_mod "SHA512" "processBlock";
+let processBlocks = parse_core_mod "SHA512" "processBlocks";
 
 // Test that every function refines itself
 // prove_extcore mrsolver (refines [] processBlocks processBlocks);
diff --git a/intTests/test1894/test.saw b/intTests/test1894/test.saw
index 7e22ea36a3..900a38462d 100644
--- a/intTests/test1894/test.saw
+++ b/intTests/test1894/test.saw
@@ -1 +1 @@
-(\n -> n) 1;
+return ((\n -> n) 1);
diff --git a/intTests/test1973/test.saw b/intTests/test1973/test.saw
index 173e71ba4e..ed2a7fc2cd 100644
--- a/intTests/test1973/test.saw
+++ b/intTests/test1973/test.saw
@@ -2,7 +2,7 @@ enable_experimental;
 
 m <- mir_load_module "test.linked-mir.json";
 
-s_adt <- mir_find_adt m "test::S" [];
+let s_adt = mir_find_adt m "test::S" [];
 
 let f_spec = do {
   s_ref <- mir_alloc (mir_adt s_adt);
diff --git a/intTests/test2162/test.sh b/intTests/test2162/test.sh
new file mode 100644
index 0000000000..8ab3833632
--- /dev/null
+++ b/intTests/test2162/test.sh
@@ -0,0 +1,39 @@
+# Don't exit unexpectedly.
+set +e
+
+# Run all three tests so if something goes wrong we can see all the
+# output.
+echo "*** test1.saw ***"
+$SAW test1.saw
+R1=$?
+
+echo "*** test2.saw ***"
+$SAW test2.saw
+R2=$?
+
+echo "*** test3.saw ***"
+$SAW test3.saw
+R3=$?
+
+EX=0
+
+# t1 should succeed; t2 and t3 should fail
+# (until #2167 gets done; until then t2 succeeds with a warning)
+if [ $R1 != 0 ]; then
+    echo "*** test1.saw failed (exit $R1) ***"
+    EX=1
+fi
+#if [ $R2 == 0 ]; then
+#    echo "*** test2.saw did not fail (exit $R2) ***"
+#    EX=1
+#fi
+if [ $R2 != 0 ]; then
+    echo "*** test2.saw failed (exit $R2) ***"
+    EX=1
+fi
+if [ $R3 == 0 ]; then
+    echo "*** test3.saw did not fail (exit $R3) ***"
+    EX=1
+fi
+
+exit $EX
diff --git a/intTests/test2162/test1.saw b/intTests/test2162/test1.saw
new file mode 100644
index 0000000000..513a7b43f9
--- /dev/null
+++ b/intTests/test2162/test1.saw
@@ -0,0 +1,25 @@
+// Create three monadic functions, one polymorphic in its monad and
+// the other two bound to TopLevel and LLVMSetup respectively.
+let f x = return x;
+let g x = do { disable_crucible_profiling; return x; };
+let h x = do { llvm_assert {{ True }}; return x; };
+
+// We should be able to run f and g at the top level, but not h.
+a0 <- f 3;
+a1 <- g 3;
+//a2 <- h 3;
+
+// We should be able to use b0 and b1 together in the same function.
+let foo () = do {
+   b0 <- f 3;
+   b1 <- g 3;
+   return 0;
+};
+
+// We should also be able to use b0 and b2 together in the same function.
+let bar () = do {
+   b0 <- f 3;
+   b2 <- h 3;
+   return 0;
+};
+
diff --git a/intTests/test2162/test2.saw b/intTests/test2162/test2.saw
new file mode 100644
index 0000000000..ac8e5ddad1
--- /dev/null
+++ b/intTests/test2162/test2.saw
@@ -0,0 +1,3 @@
+// Running this at the top level should produce a type error.
+let h x = do { llvm_assert {{ True }}; return x; };
+a <- h 3;
diff --git a/intTests/test2162/test3.saw b/intTests/test2162/test3.saw
new file mode 100644
index 0000000000..abf19e1cce
--- /dev/null
+++ b/intTests/test2162/test3.saw
@@ -0,0 +1,14 @@
+// Create three monadic functions, one polymorphic in its monad and
+// the other two bound to TopLevel and LLVMSetup respectively.
+let f x = return x;
+let g x = do { disable_crucible_profiling; return x; };
+let h x = do { llvm_assert {{ True }}; return x; };
+
+// Using all three together in the same function should produce a type
+// error.
+let foo () = do {
+   b0 <- f 3;
+   b1 <- g 3;
+   b2 <- h 3;
+   return 0;
+};
diff --git a/intTests/test_intro_examples/rewrite.saw b/intTests/test_intro_examples/rewrite.saw
index d5a7e693e8..9fecaf1d19 100644
--- a/intTests/test_intro_examples/rewrite.saw
+++ b/intTests/test_intro_examples/rewrite.saw
@@ -5,8 +5,8 @@ let {{
 }};
 f_eq_g <- prove_print abc {{ \x y -> f x y == g x y }};
 print f_eq_g;
-t1 <- unfold_term ["h"] {{ \x y -> h x y == 2*(f x y) }};
+let t1 = unfold_term ["h"] {{ \x y -> h x y == 2*(f x y) }};
 print_term t1;
-t2 <- rewrite (addsimp f_eq_g empty_ss) t1;
+let t2 = rewrite (addsimp f_eq_g empty_ss) t1;
 print_term t2;
 prove_print (unint_yices ["g"]) t2;
diff --git a/intTests/test_type_errors/err006.log.good b/intTests/test_type_errors/err006.log.good
new file mode 100644
index 0000000000..af832f4b40
--- /dev/null
+++ b/intTests/test_type_errors/err006.log.good
@@ -0,0 +1,3 @@
+ Loading file "err006.saw"
+ err006.saw:3:1-3:20: Warning: Monadic bind of non-monadic value; rewrite as let-binding or use return
+ err006.saw:3:1-3:20: Warning: This will become an error in a future release of SAW
diff --git a/intTests/test_type_errors/err006.saw b/intTests/test_type_errors/err006.saw
new file mode 100644
index 0000000000..b8fad199d0
--- /dev/null
+++ b/intTests/test_type_errors/err006.saw
@@ -0,0 +1,3 @@
+// This was allowed prior to Dec 2024 and is currently a warning;
+// should eventually become an error.
+x <- concat [0] [1];
diff --git a/intTests/test_type_errors/err007.log.good b/intTests/test_type_errors/err007.log.good
new file mode 100644
index 0000000000..666765014e
--- /dev/null
+++ b/intTests/test_type_errors/err007.log.good
@@ -0,0 +1,12 @@
+ Loading file "err007.saw"
+ err007.saw:2:1-2:4: Type mismatch.
+    Mismatch of type constructors. Expected: <Block> but got ([])
+    err007.saw:2:1-2:4: The type TopLevel t.0 arises from this type annotation
+    err007.saw:2:1-2:4: The type [Int] arises from the type of this term
+    
+    Expected: TopLevel t.0
+    Found:    [Int]
+    
+    within "<toplevel>" (err007.saw:2:1-2:4)
+
+FAILED
diff --git a/intTests/test_type_errors/err007.saw b/intTests/test_type_errors/err007.saw
new file mode 100644
index 0000000000..2abf69b6ec
--- /dev/null
+++ b/intTests/test_type_errors/err007.saw
@@ -0,0 +1,2 @@
+// This was allowed prior to Dec 2024 and now fails.
+[0];
diff --git a/intTests/test_type_errors/err008.log.good b/intTests/test_type_errors/err008.log.good
new file mode 100644
index 0000000000..a1fe6aa46d
--- /dev/null
+++ b/intTests/test_type_errors/err008.log.good
@@ -0,0 +1,4 @@
+ Loading file "err008.saw"
+ err008.saw:3:1-3:19: Warning: Monadic bind with the wrong monad; found LLVMSetup but expected TopLevel
+ err008.saw:3:1-3:19: Warning: This creates the action but does not execute it; if you meant to do that, prefix the expression with return
+ err008.saw:3:1-3:19: Warning: This will become an error in a future release of SAW
diff --git a/intTests/test_type_errors/err008.saw b/intTests/test_type_errors/err008.saw
new file mode 100644
index 0000000000..2e472a69e5
--- /dev/null
+++ b/intTests/test_type_errors/err008.saw
@@ -0,0 +1,3 @@
+// This was allowed prior to Dec 2024 and is currently a warning;
+// should eventually become an error.
+llvm_assert {{ True }};
diff --git a/intTests/test_type_errors/err009.log.good b/intTests/test_type_errors/err009.log.good
new file mode 100644
index 0000000000..bd853356d3
--- /dev/null
+++ b/intTests/test_type_errors/err009.log.good
@@ -0,0 +1,4 @@
+ Loading file "err009.saw"
+ err009.saw:4:1-4:40: Warning: Monadic bind with the wrong monad; found LLVMSetup but expected TopLevel
+ err009.saw:4:1-4:40: Warning: This creates the action but does not execute it; if you meant to do that, prefix the expression with return
+ err009.saw:4:1-4:40: Warning: This will become an error in a future release of SAW
diff --git a/intTests/test_type_errors/err009.saw b/intTests/test_type_errors/err009.saw
new file mode 100644
index 0000000000..443e04680d
--- /dev/null
+++ b/intTests/test_type_errors/err009.saw
@@ -0,0 +1,4 @@
+// This was allowed prior to Dec 2024 and is currently a warning;
+// should eventually become an error.
+enable_experimental;
+x <- llvm_fresh_cryptol_var "foo" {| [8] |};
diff --git a/intTests/test_type_errors/err010.log.good b/intTests/test_type_errors/err010.log.good
new file mode 100644
index 0000000000..0230ce802c
--- /dev/null
+++ b/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 creates the action but does not execute it; if you meant to do that, prefix the expression with return
+ err010.saw:12:1-12:9: Warning: This will become an error in a future release of SAW
diff --git a/intTests/test_type_errors/err010.saw b/intTests/test_type_errors/err010.saw
new file mode 100644
index 0000000000..fd416627ab
--- /dev/null
+++ b/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;
diff --git a/intTests/test_type_errors/err011.log.good b/intTests/test_type_errors/err011.log.good
new file mode 100644
index 0000000000..6d925c3806
--- /dev/null
+++ b/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
diff --git a/intTests/test_type_errors/err011.saw b/intTests/test_type_errors/err011.saw
new file mode 100644
index 0000000000..55827c6556
--- /dev/null
+++ b/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;
diff --git a/intTests/test_type_errors/err012.log.good b/intTests/test_type_errors/err012.log.good
new file mode 100644
index 0000000000..34a7bf4700
--- /dev/null
+++ b/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 creates the action but does not execute it; if you meant to do that, 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
diff --git a/intTests/test_type_errors/err012.saw b/intTests/test_type_errors/err012.saw
new file mode 100644
index 0000000000..63f375858b
--- /dev/null
+++ b/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;
diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs
index 8d496af8b4..a689a4339f 100644
--- a/saw/SAWScript/REPL/Command.hs
+++ b/saw/SAWScript/REPL/Command.hs
@@ -171,8 +171,14 @@ typeOfCmd str
      let pos = getPos expr
          decl = SS.Decl pos (SS.PWild pos Nothing) Nothing expr
      rw <- getValueEnvironment
-     ~(SS.Decl _pos _ (Just schema) _expr') <-
-       either failTypecheck return $ checkDecl (rwValueTypes rw) (rwNamedTypes rw) decl
+     decl' <- do
+       let (errs_or_results, warns) = checkDecl (rwValueTypes rw) (rwNamedTypes rw) decl
+       let issueWarning (msgpos, msg) =
+             -- XXX the print functions should be what knows how to show positions...
+             putStrLn (show msgpos ++ ": Warning: " ++ msg)
+       io $ mapM_ issueWarning warns
+       either failTypecheck return $ errs_or_results
+     let ~(SS.Decl _pos _ (Just schema) _expr') = decl'
      io $ putStrLn $ SS.pShow schema
 
 quitCmd :: REPL ()
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 71669da99c..be9da6fe51 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -43,6 +43,7 @@ import qualified Control.Exception as X
 import Control.Monad (unless, (>=>), when)
 import Control.Monad.IO.Class (liftIO)
 import qualified Data.ByteString as BS
+import Data.List (genericLength)
 import qualified Data.Map as Map
 import Data.Map ( Map )
 import qualified Data.Set as Set
@@ -65,7 +66,7 @@ import SAWScript.JavaExpr
 import SAWScript.LLVMBuiltins
 import SAWScript.Options
 import SAWScript.Lexer (lexSAW)
-import SAWScript.MGU (checkDecl, checkDeclGroup, checkStmt)
+import SAWScript.MGU (checkStmt)
 import SAWScript.Parser (parseSchema)
 import SAWScript.Panic (panic)
 import SAWScript.TopLevel
@@ -120,6 +121,41 @@ import SAWScript.AutoMatch
 
 import qualified Lang.Crucible.FunctionHandle as Crucible
 
+
+-- Support ---------------------------------------------------------------------
+
+-- This is used to reject top-level execution of polymorphic
+-- expressions. Assumes we aren't inside an uninstantiated forall
+-- quantifier. Also assumes the typechecker has already approved the
+-- type. This means we know it doesn't contain unbound named type
+-- variables. Fail if we encounter a unification var.
+--
+-- XXX: this serves little purpose. A polymorphic expression must
+-- either be a partially applied (or unapplied) polymorphic function,
+-- in which case we aren't going to actually execute anything anyway,
+-- or be fully applied but have a polymorphic return type, and the
+-- only such functions we can have are those that don't return (like
+-- "fail") so we don't actually care what they produce. So this code
+-- and the check that calls it should probably be removed.
+--
+-- XXX: also, this is here transiently so that the rejection continues
+-- to work while the interaction between the interpreter and the
+-- typechecker is rationalized. In the long run, the rejection should
+-- really belong only to the repl for repl purposes and the
+-- polymorphism check should be part of the currently nonexistent
+-- incremental interface to the typechecker. Alternatively, if there
+-- are cases that really require rejection of polymorphic expressions
+-- at the top level, they also require rejection of polymorphic
+-- expressions in nested do-blocks that aren't inside functions, and
+-- it can and should all happen inside the typechecker.
+isPolymorphic :: SS.Type -> Bool
+isPolymorphic ty0 = case ty0 of
+    SS.TyCon _pos _tycon args -> any isPolymorphic args
+    SS.TyRecord _pos fields -> any isPolymorphic fields
+    SS.TyVar _pos _a -> False
+    SS.TyUnifyVar _pos _ix -> True
+
+
 -- Environment -----------------------------------------------------------------
 
 bindPatternLocal :: SS.Pattern -> Maybe SS.Schema -> Value -> LocalEnv -> LocalEnv
@@ -154,6 +190,24 @@ bindPatternEnv pat ms v env =
                   Just t -> error ("bindPatternEnv: expected tuple type " ++ show t)
         _ -> error "bindPatternEnv: expected tuple value"
 
+-- Typechecker ----------------------------------------------------------------
+
+-- Process a typechecker result.
+-- Wraps the typechecker in the stuff needed to print its warnings and errors.
+--
+-- XXX: this code should probably live inside the typechecker.
+--
+-- Usage is processTypeCheck $ checkStmt ...
+type MsgList = [(SS.Pos, String)]
+processTypeCheck :: InteractiveMonad m => (Either MsgList a, MsgList) -> m a
+processTypeCheck (errs_or_output, warns) =
+  liftTopLevel $ do
+    let issueWarning (pos, msg) =
+          -- XXX the print functions should be what knows how to show positions...
+          printOutLnTop Warn (show pos ++ ": Warning: " ++ msg)
+    mapM_ issueWarning warns
+    either failTypecheck return errs_or_output
+
 -- Interpretation of SAWScript -------------------------------------------------
 
 interpret :: SS.Expr -> TopLevel Value
@@ -284,6 +338,22 @@ stmtInterpreter :: StmtInterpreter
 stmtInterpreter ro rw stmts =
   fst <$> runTopLevel (withLocalEnv emptyLocal (interpretStmts stmts)) ro rw
 
+-- Get the type of an AST element. For now, only patterns because that's
+-- what we're using.
+--
+-- Assumes we have been through the typechecker and the types are filled in.
+--
+-- XXX: this should be a typeclass function with instances for all the AST
+-- types.
+---
+-- XXX: also it should be moved to ASTUtil once we have such a place.
+getType :: SS.Pattern -> SS.Type
+getType pat = case pat of
+    SS.PWild _pos ~(Just t) -> t
+    SS.PVar _pos _x ~(Just t) -> t
+    SS.PTuple tuplepos pats ->
+        SS.TyCon tuplepos (SS.TupleCon (genericLength pats)) (map getType pats)
+
 processStmtBind ::
   InteractiveMonad m =>
   Bool ->
@@ -291,64 +361,52 @@ processStmtBind ::
   SS.Expr ->
   m ()
 processStmtBind printBinds pat expr = do -- mx mt
-  -- Extract the variable and type from the pattern, if any. If there
-  -- isn't any single variable use "it". We seem to get here only for
-  -- statements typed at the repl, so it apparently isn't wrong to use
-  -- "it".
-  -- XXX: that's not actually true, file loads come here via
-  -- interpretStmt and interpretFile.
-  -- XXX: it seems problematic to discard the type for a tuple binding...
-  let it pos = SS.Located "it" "it" pos
-  let (lname, mt) = case pat of
-        SS.PWild pos t -> (it pos, t)
-        SS.PVar _pos x t -> (x, t)
-        SS.PTuple pos _pats -> (it pos, Nothing)
-  ctx <- getMonadContext
-  -- XXX SS.PosREPL probably is not what we want
-  -- but the position we want for the block type isn't the position of
-  -- the pattern (perhaps we want the position of the "do" that makes
-  -- this a block context? but there isn't necessarily one in the
-  -- repl)
-  let pos = SS.PosREPL
-  let tyctx = SS.tContext pos ctx
-  let expr' = case mt of
-                Nothing -> expr
-                Just t -> SS.TSig (SS.maxSpan' expr t) expr (SS.tBlock pos tyctx t)
-  let decl = SS.Decl (SS.maxSpan' pat expr') pat Nothing expr'
   rw <- liftTopLevel getMergedEnv
-  let opts = rwPPOpts rw
-
-  ~(SS.Decl _ _ (Just schema) expr'') <- liftTopLevel $
-    either failTypecheck return $ checkDecl (rwValueTypes rw) (rwNamedTypes rw) decl
-
-  val <- liftTopLevel $ interpret expr''
-
-  -- Run the resulting TopLevel action.
-  (result, ty) <-
-    case schema of
-      SS.Forall [] t ->
-        case t of
-          SS.TyCon _ SS.BlockCon [c, t'] | SS.isContext ctx c -> do
-            result <- actionFromValue val
-            return (result, t')
-          _ -> return (val, t)
-      _ -> fail $ "Not a monomorphic type: " ++ SS.pShow schema
+
+  val <- liftTopLevel $ interpret expr
+
+  -- Fetch the type from updated pattern, since the typechecker will
+  -- have filled it in there.
+  --
+  -- Note that this type won't include the current monad type, because
+  -- it's the type of the value that the pattern on the left of <- is
+  -- trying to bind.
+  let ty = getType pat
+
+  -- Reject polymorphic values. XXX: as noted above this should either
+  -- be inside the typechecker or restricted to the repl.
+  when (isPolymorphic ty) $ fail $ "Not a monomorphic type: " ++ SS.pShow ty
+
+  -- Run the resulting TopLevel (or ProofScript) action.
+  result <- actionFromValue val
+
   --io $ putStrLn $ "Top-level bind: " ++ show mx
   --showCryptolEnv
 
-  -- Print non-unit result if it was not bound to a variable
-  case pat of
-    SS.PWild _ _ | printBinds && not (isVUnit result) ->
-      liftTopLevel $
-      do nenv <- io . scGetNamingEnv =<< getSharedContext
-         printOutLnTop Info (showsPrecValue opts nenv 0 result "")
-    _ -> return ()
-
-  -- Print function type if result was a function
-  case ty of
-    SS.TyCon _ SS.FunCon _ ->
-      liftTopLevel $ printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty
-    _ -> return ()
+  -- When in the repl, print the result.
+  when printBinds $ do
+    let opts = rwPPOpts rw
+
+    -- Extract the variable, if any, from the pattern. If there isn't
+    -- any single variable use "it".
+    let name = case pat of
+          SS.PWild _patpos _t -> "it"
+          SS.PVar _patpos x _t -> getVal x
+          SS.PTuple _patpos _pats -> "it"
+
+    -- Print non-unit result if it was not bound to a variable
+    case pat of
+      SS.PWild _ _ | not (isVUnit result) ->
+        liftTopLevel $
+        do nenv <- io . scGetNamingEnv =<< getSharedContext
+           printOutLnTop Info (showsPrecValue opts nenv 0 result "")
+      _ -> return ()
+
+    -- Print function type if result was a function
+    case ty of
+      SS.TyCon _ SS.FunCon _ ->
+        liftTopLevel $ printOutLnTop Info $ name ++ " : " ++ SS.pShow ty
+      _ -> return ()
 
   liftTopLevel $
    do rw' <- getTopLevelRW
@@ -373,41 +431,30 @@ instance InteractiveMonad ProofScript where
   actionFromValue = fromValue
   getMonadContext = return SS.ProofScript
 
--- | Interpret a block-level statement in the TopLevel monad.
+-- | Interpret a block-level statement in an interactive monad (TopLevel or ProofScript)
 interpretStmt :: InteractiveMonad m =>
   Bool {-^ whether to print non-unit result values -} ->
   SS.Stmt ->
   m ()
-interpretStmt printBinds stmt =
-  let ?fileReader = BS.readFile in
-
--- XXX: not yet. The code in processStmtBind that typechecks the
--- statement incrementally does extra things behind the typechecker's
--- back (it wraps each bind in a Decl so it passes through generalize)
--- and we need to figure out the correct way to make that happen
--- before typechecking up front.
-{-
-  rw <- getTopLevelRW
-  stmt' <- either failTypecheck return $
-           checkStmt (rwValueTypes rw) (rwNamedTypes rw) stmt
--}
+interpretStmt printBinds stmt = do
+  let ?fileReader = BS.readFile
+
+  ctx <- getMonadContext
+  rw <- liftTopLevel $ getTopLevelRW
+  stmt' <- processTypeCheck $ checkStmt (rwValueTypes rw) (rwNamedTypes rw) ctx stmt
 
-  case stmt of
+  case stmt' of
 
     SS.StmtBind pos pat expr ->
       withTopLevel (withPosition pos) (processStmtBind printBinds pat expr)
 
-    SS.StmtLet _ dg           ->
-      liftTopLevel $
-      do rw <- getTopLevelRW
-         dg' <- either failTypecheck return $
-                checkDeclGroup (rwValueTypes rw) (rwNamedTypes rw) dg
-         env <- interpretDeclGroup dg'
+    SS.StmtLet _pos dg ->
+      liftTopLevel $ do
+         env <- interpretDeclGroup dg
          withLocalEnv env getMergedEnv >>= putTopLevelRW
 
     SS.StmtCode _ lstr ->
-      liftTopLevel $
-      do rw <- getTopLevelRW
+      liftTopLevel $ do
          sc <- getSharedContext
          --io $ putStrLn $ "Processing toplevel code: " ++ show lstr
          --showCryptolEnv
@@ -416,8 +463,7 @@ interpretStmt printBinds stmt =
          --showCryptolEnv
 
     SS.StmtImport _ imp ->
-      liftTopLevel $
-      do rw <- getTopLevelRW
+      liftTopLevel $ do
          sc <- getSharedContext
          --showCryptolEnv
          let mLoc = iModule imp
@@ -427,15 +473,8 @@ interpretStmt printBinds stmt =
          putTopLevelRW $ rw { rwCryptol = cenv' }
          --showCryptolEnv
 
-    SS.StmtTypedef _ _ _ ->
-      liftTopLevel $
-      do rw <- getTopLevelRW
-         ctx <- getMonadContext
-         pos <- getPosition
-         -- XXX: hack this until such time as we can get it to work up front
-         stmt' <- either failTypecheck return $
-                  checkStmt (rwValueTypes rw) (rwNamedTypes rw) pos ctx stmt
-         let (SS.StmtTypedef _ name ty) = stmt'
+    SS.StmtTypedef _ name ty ->
+      liftTopLevel $ do
          putTopLevelRW $ addTypedef (getVal name) ty rw
 
 interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel ()
diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs
index 465fa0ba74..9ab98e3b63 100644
--- a/src/SAWScript/MGU.hs
+++ b/src/SAWScript/MGU.hs
@@ -17,7 +17,6 @@ Stability   : provisional
 
 module SAWScript.MGU
        ( checkDecl
-       , checkDeclGroup
        , checkStmt
        , instantiate
        ) where
@@ -380,12 +379,18 @@ data RW = RW
     -- | The unification var substitution we're accumulating
     subst :: Subst,
 
-    -- | Any type errors we've generated so far
-    errors :: [(Pos, String)]
+    -- | Any type errors and warnings we've generated so far
+    errors :: [(Pos, String)],
+    warnings :: [(Pos, String)]
   }
 
 emptyRW :: RW
-emptyRW = RW 0 emptySubst []
+emptyRW = RW
+  { nextTypeIndex = 0
+  , subst = emptySubst
+  , errors = []
+  , warnings = []
+  }
 
 -- Get a fresh unification var number.
 getFreshTypeIndex :: TI TypeIndex
@@ -418,6 +423,11 @@ recordError :: Pos -> String -> TI ()
 recordError pos err = do
   TI $ modify $ \rw -> rw { errors = (pos, err) : errors rw }
 
+-- Add a warning message.
+recordWarning :: Pos -> String -> TI ()
+recordWarning pos msg = do
+  TI $ modify $ \rw -> rw { warnings = (pos, msg) : warnings rw }
+
 -- Apply the current substitution with appSubst.
 applyCurrentSubst :: AppSubst t => t -> TI t
 applyCurrentSubst t = do
@@ -764,6 +774,22 @@ unify m t1 pos t2 = do
          -- Indent all but the first line by four spaces.
          morelines' = map (\msg -> "    " ++ msg) morelines
 
+-- Check if two types match but don't actually unify them
+-- (that is, on success throw away the substitution and on error
+-- throw away the complaints)
+--
+-- This is inelegant, and used for some workaround logic to decide
+-- which unifications to attempt to avoid failures on things we don't
+-- want to make fatal just yet. It should be removed when no longer
+-- needed.
+matches :: Type -> Type -> TI Bool
+matches t1 t2 = do
+  t1' <- applyCurrentSubst =<< resolveCurrentTypedefs t1
+  t2' <- applyCurrentSubst =<< resolveCurrentTypedefs t2
+  case mgu t1' t2' of
+    Right _ -> return True
+    Left _ -> return False
+
 -- }}}
 
 
@@ -1044,23 +1070,158 @@ legalEndOfBlock s = case s of
     StmtBind _spos (PWild _patpos _mt) _e -> True
     _ -> False
 
+-- break a monadic type down into its monad and value types, if it is one
+--
+--    monadType (TopLevel Int) gives Just (TopLevel, Int)
+--    monadType Int gives Nothing
+--
+monadType  :: Type -> Maybe (Type, Type)
+monadType ty = case ty of
+  TyCon _ BlockCon [ctx@(TyCon _ (ContextCon _) []), valty] ->
+      Just (ctx, valty)
+  -- We don't currently ever generate this type, but be future-proof
+  TyCon pos (ContextCon ctx) [valty] ->
+      Just (TyCon pos (ContextCon ctx) [], valty)
+  _ ->
+      Nothing
+
+-- wrap an expression in "return"
+wrapReturn :: Expr -> Expr
+wrapReturn e =
+   let ePos = getPos e
+       retPos = PosInternal "<implicitly inserted return>"
+       ret = Var $ Located "return" "return" retPos 
+   in
+   Application ePos ret e
+
 -- type inference for a single statement
 --
+-- the boolean is whether we're at the syntactic top level, which is used
+-- for workaround logic for issue #2162
+--
 -- the passed-in position should be the position associated with the monad type
 -- the first type argument (ctx) is the monad type for any binds that occur
 --
 -- returns a wrapper for checking subsequent statements as well as
 -- an updated statement and a type.
-inferStmt :: LName -> Pos -> Type -> Stmt -> TI (TI a -> TI a, Stmt, Type)
-inferStmt ln blockpos ctx s =
+inferStmt :: LName -> Bool -> Pos -> Type -> Stmt -> TI (TI a -> TI a, Stmt, Type)
+inferStmt ln atSyntacticTopLevel blockpos ctx s =
     case s of
         StmtBind spos pat e -> do
             (pty, pat') <- inferPattern pat
-            -- The expression should be of monad type; unify both
-            -- the monad type (ctx) and the result type expected
-            -- by the pattern (pty).
-            e' <- checkExpr ln e (tBlock blockpos ctx pty)
-            let s' = StmtBind spos pat' e'
+            -- The expression should be of monad type. The
+            -- straightforward way to proceed here is to unify both
+            -- the monad type (ctx) and the result type expected by
+            -- the pattern (pty), like this:
+            --    e' <- checkExpr ln e (tBlock blockpos ctx pty)
+            --
+            -- However, historically when at the syntactic top level
+            -- (only), the monad type was left off, meaning that
+            -- various incorrect forms were silently accepted. Fixing
+            -- this in Dec 2024 triggered a lot of fallout, so for the
+            -- time being we want to check for, warn about, and allow
+            -- the following cases. (Again, only when at the syntactic
+            -- top level. Which is not when in the TopLevel monad.)
+            --    x <- e for non-monadic e
+            --    x <- e for e in the wrong monad
+            --
+            -- These should be made errors again at some point, but
+            -- definitely no earlier than the _second_ release after
+            -- December 2024, as the first such release should include
+            -- the warning behavior. Probably the explicit messages
+            -- should then in turn not be removed for at least one
+            -- further release. See #2167 and #2162.
+            --
+            -- To accomplish this, call inferExpr to get a type for
+            -- the expression, and examine it. If the special cases
+            -- apply, issue special-case warnings with explanations,
+            -- unify the type with only the pattern type, and patch up
+            -- the expression by wrapping it in "return".  (The latter
+            -- will restore the old behavior for both cases, so we
+            -- don't need to also gunk up the interpreter to handle
+            -- this problem.)
+            --
+            -- If the special cases don't apply, unify the result type
+            -- with the complete type.
+            (e', ty) <- inferExpr (ln, e)
+            ty' <- applyCurrentSubst =<< resolveCurrentTypedefs ty
+
+            -- The correct, restricted case
+            let restrictToCorrect = do
+                  -- unify the type of e with the expected monad and
+                  -- pattern types
+                  unify ln (tBlock blockpos ctx pty) (getPos e') ty
+                  return e'
+
+            -- The special case for non-monadic values
+            let allowNonMonadic = do
+                  recordWarning spos $ "Monadic bind of non-monadic value; " ++
+                                       "rewrite as let-binding or use return"
+                  recordWarning spos $ "This will become an error in a " ++
+                                       "future release of SAW"
+                  unify ln pty (getPos e') ty
+                  -- Wrap the expression in "return" to correct the type
+                  return $ wrapReturn e'
+
+            -- The special case for the wrong monad
+            let allowWrongMonad ctx' valty' = do
+                  recordWarning spos $ "Monadic bind with the wrong monad; " ++
+                                       "found " ++ pShow ctx' ++
+                                       " but expected " ++ pShow ctx
+                  recordWarning spos $ "This creates the action but does " ++
+                                       "not execute it; if you meant to do " ++
+                                       "that, prefix the " ++
+                                       "expression with return"
+                  recordWarning spos $ "This will become an error in a " ++
+                                       "future release of SAW"
+
+                  -- 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.
+            e'' <-
+                if not atSyntacticTopLevel then
+                    restrictToCorrect
+                else do
+                    ok <- matches (tBlock blockpos ctx pty) ty
+                    if ok then
+                        restrictToCorrect
+                    else
+                        case monadType ty' of
+                            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
+                               -- case we need to worry about)
+                               case pat of
+                                   PWild _ _ -> restrictToCorrect
+                                   _ -> allowNonMonadic
+
+            let s' = StmtBind spos pat' e''
             let wrapper = withPattern pat'
             return (wrapper, s', pty)
         StmtLet spos dg -> do
@@ -1089,7 +1250,8 @@ inferStmts ln blockpos ctx stmts = case stmts of
         return ([], t)
 
     s : more -> do
-        (wrapper, s', t) <- inferStmt ln blockpos ctx s
+        let atSyntacticTopLevel = False
+        (wrapper, s', t) <- inferStmt ln atSyntacticTopLevel blockpos ctx s
         case more of
             [] ->
                 if legalEndOfBlock s then
@@ -1104,6 +1266,34 @@ inferStmts ln blockpos ctx stmts = case stmts of
                (more', t') <- wrapper $ inferStmts ln blockpos ctx more
                return (s' : more', t')
 
+-- Wrapper around inferStmt suitable for checking one statement at a
+-- time. This is temporary scaffolding for the interpreter while
+-- fixing it. (Currently the interpreter typechecks one statement at a
+-- time when executing, even when not at the repl, and this involves
+-- assorted messiness and technical debt. Eventually we'll get it into
+-- a state where we can always just typecheck immediately after
+-- parsing (including incrementally from the repl) but we're some
+-- distance from that. In the meantime the first step is to get it to
+-- typecheck one statement at a time without special-casing any of
+-- them, and this is how it does that.
+--
+-- Run inferStmt and then apply the current substitution before
+-- returning the updated statement. Ignore the wrapper returned for
+-- typechecking subsequent statements; the interpreter has its own
+-- (misbegotten) logic for handling that in its own way. (Which should
+-- be removed, but we need to get rid of these wrappers here first;
+-- any sane incremental typechecking interface requires updating the
+-- environment for sequential declarations, not pretending that
+-- subsequent statements in a block are nested inside prior ones.)
+inferSingleStmt :: LName -> Pos -> Type -> Stmt -> TI Stmt
+inferSingleStmt ln pos ctx s = do
+  -- currently we are always at the syntactic top level here because
+  -- that's how the interpreter works
+  let atSyntacticTopLevel = True
+  (_wrapper, s', _ty') <- inferStmt ln atSyntacticTopLevel pos ctx s
+  s'' <- applyCurrentSubst s'
+  return s''
+
 --
 -- decls
 --
@@ -1309,20 +1499,28 @@ checkType kind ty = case ty of
 ------------------------------------------------------------
 -- External interface {{{
 
+-- Some short names for use in the signatures below
+type MsgList = [(Pos, String)]
+type Result a = (Either MsgList a, MsgList)
+
 -- Run the TI monad.
-runTIWithEnv :: VarEnv -> TyEnv -> TI a -> (a, Subst, [(Pos, String)])
-runTIWithEnv env tenv m = (a, subst rw, errors rw)
+--
+-- Note that the error and warning lists accumulate in reverse order
+-- (later messages are consed onto the head of the list) so we
+-- reverse on the way out.
+runTIWithEnv :: VarEnv -> TyEnv -> TI a -> (a, Subst, MsgList, MsgList)
+runTIWithEnv env tenv m = (a, subst rw, reverse $ errors rw, reverse $ warnings rw)
   where
   m' = runReaderT (unTI m) (RO env tenv)
   (a,rw) = runState m' emptyRW
 
 -- Run the TI monad and interpret/collect the results
 -- (failure if any errors were produced)
-evalTIWithEnv :: VarEnv -> TyEnv -> TI a -> Either [(Pos, String)] a
+evalTIWithEnv :: VarEnv -> TyEnv -> TI a -> Result a
 evalTIWithEnv env tenv m =
   case runTIWithEnv env tenv m of
-    (res, _, []) -> Right res
-    (_, _, errs) -> Left errs
+    (res, _, [], warns) -> (Right res, warns)
+    (_, _, errs, warns) -> (Left errs, warns)
 
 -- | Check a single statement. (This is an external interface.)
 --
@@ -1331,59 +1529,55 @@ evalTIWithEnv env tenv m =
 --
 -- The third is a current position, and the fourth is the
 -- context/monad type associated with the execution.
-
--- (separate comment so this part doesn't appear in the Haddocks)
--- XXX: we shouldn't need a position here.
--- The position is used for the following things:
---
---    - to create ln, which is used as part of the error printing
---      scheme, but is no longer particularly useful after recent
---      improvements (especially here where it contains no real
---      information) and should be removed;
---
---    - to be the position associated with the monad context, which
---      in a tidy world should just be PosRepl (as in, the only
---      time we should be typechecking a single statement is when
---      it was just typed interactively, and which monad we're in
---      is a direct property of that context) but this is not
---      currently true and will require a good bit of interpreter
---      cleanup to make it true;
---
---    - to pass to inferStmt, which also uses it as part of the
---      position associated with the monad context. (This part is a
---      result of BlockCon existing and can go away when BlockCon is
---      removed.)
---
-checkStmt :: VarEnv -> TyEnv -> Pos -> Context -> Stmt -> Either [(Pos, String)] Stmt
-checkStmt env tenv pos ctx stmt = do
-  ln <- case ctx of
-       TopLevel -> return $ Located "<toplevel>" "<toplevel>" pos
-       ProofScript -> return $ Located "<proofscript>" "<proofscript>" pos
-       _ -> panic "checkStmt" ["Invalid monad context " ++ pShow ctx]
-  let ctxtype = TyCon pos (ContextCon ctx) []
-  case evalTIWithEnv env tenv (inferStmt ln pos ctxtype stmt) of
-    Left errs -> Left errs
-    Right (_wrapper, stmt', _type) -> Right stmt'
+checkStmt :: VarEnv -> TyEnv -> Context -> Stmt -> Result Stmt
+checkStmt env tenv ctx stmt =
+  -- XXX: we shouldn't need this position here.
+  -- The position is used for the following things:
+  --
+  --    - to create ln, which is used as part of the error printing
+  --      scheme, but is no longer particularly useful after recent
+  --      improvements (especially here where it contains no real
+  --      information) and should be removed;
+  --
+  --    - to be the position associated with the monad context, which
+  --      in a tidy world should just be PosRepl (as in, the only
+  --      time we should be typechecking a single statement is when
+  --      it was just typed interactively, and which monad we're in
+  --      is a direct property of that context) but this is not
+  --      currently true and will require a good bit of interpreter
+  --      cleanup to make it true;
+  --
+  --    - to pass to inferStmt, which also uses it as part of the
+  --      position associated with the monad context. (This part is a
+  --      result of BlockCon existing and can go away when BlockCon is
+  --      removed.)
+  --
+  -- XXX: using the position of the statement as the position
+  -- associated with the monad context is not correct (or at least,
+  -- will be confusing) and we should figure something else out if the
+  -- interpreter cleanup doesn't come through soon. Note that
+  -- currently we come through here only for syntactically top-level
+  -- statements in the interpreter; these are TopLevel except when in
+  -- the ProofScript repl. So perhaps we should use PosRepl when in
+  -- ProofScript, and then either PosRepl or PosBuiltin for TopLevel?
+  -- But we don't have a good way of knowing here whether we're
+  -- actually in the repl.
+  let pos = getPos stmt
+      ln = case ctx of
+          TopLevel -> Located "<toplevel>" "<toplevel>" pos
+          ProofScript -> Located "<proofscript>" "<proofscript>" pos
+          _ -> panic "checkStmt" ["Invalid monad context " ++ pShow ctx]
+      ctxtype = TyCon pos (ContextCon ctx) []
+  in
+  evalTIWithEnv env tenv (inferSingleStmt ln pos ctxtype stmt)
 
 -- | Check a single declaration. (This is an external interface.)
 --
 -- The first two arguments are the starting variable and typedef
 -- environments to use.
-checkDecl :: VarEnv -> TyEnv -> Decl -> Either [(Pos, String)] Decl
+checkDecl :: VarEnv -> TyEnv -> Decl -> Result Decl
 checkDecl env tenv decl =
-  case evalTIWithEnv env tenv (inferDecl decl) of
-    Left errs -> Left errs
-    Right decl' -> Right decl'
-
--- | Check a declgroup. (This is an external interface.)
---
--- The first two arguments are the starting variable and typedef
--- environments to use.
-checkDeclGroup :: VarEnv -> TyEnv -> DeclGroup -> Either [(Pos, String)] DeclGroup
-checkDeclGroup env tenv dg =
-  case evalTIWithEnv env tenv (inferDeclGroup dg) of
-    Left errs -> Left errs
-    Right dg' -> Right dg'
+  evalTIWithEnv env tenv (inferDecl decl)
 
 -- }}}