typechecker: add workaround for fallout from #2162.

Statements of the forms

   x <- e;
   x <- s;
   s;

where e is a non-monadic term and s is a monadic term in the wrong
monad are now accepted with a warning instead of causing a fatal
type error.

Note that statements of the form

   e;

which also used to be accepted will now fail. The chance of this
appearing in the wild is low.

While I've fixed all the fallout in the saw tree, the amount (and
nature) suggests that downstream users will also have cases to fix and
we should allow time for this before making it a hard fail.

Add tests for all these forms.

CHANGES.md

@@ -16,18 +16,30 @@ 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.)
-There are two primary visible consequences.
+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 top-level statements of the form ```x <- e;```
-where ```e``` is a pure (non-monadic) term used to be (improperly)
-accepted.
-These are now rejected and need to be changed to ```let x = e;```.
-See issue #2162.
+
+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;```.
+
+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.
 
 * A number of SAWScript type checking problems have been fixed,
 including issue #2077.

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

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];

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

intTests/test_type_errors/err007.saw

@@ -0,0 +1,2 @@
+// This was allowed prior to Dec 2024 and now fails.
+[0];

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 was historically ignored and will have no effect; if you really want to do this, prefix the expression with return
+ err008.saw:3:1-3:19: Warning: This will become an error in a future release of SAW

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 }};

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 was historically ignored and will have no effect; if you really want to do this, prefix the expression with return
+ err009.saw:4:1-4:40: Warning: This will become an error in a future release of SAW

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] |};

src/SAWScript/MGU.hs

@@ -418,9 +418,9 @@ recordError :: Pos -> String -> TI ()
 recordError pos err = do
   TI $ modify $ \rw -> rw { errors = (pos, err) : errors rw }
 
--- Add a warning message. (not yet used)
-_recordWarning :: Pos -> String -> TI ()
-_recordWarning pos msg = do
+-- 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.
@@ -769,6 +769,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
+
 -- }}}
 
 
@@ -1049,23 +1065,132 @@ 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  :: 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.
+            --
+            -- 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 was historically ignored and " ++
+                                       "will have no effect; if you really " ++
+                                       "want to do this, prefix the " ++
+                                       "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.
+                  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') -> 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
@@ -1094,7 +1219,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
@@ -1130,7 +1256,10 @@ inferStmts ln blockpos ctx stmts = case stmts of
 -- subsequent statements in a block are nested inside prior ones.)
 inferSingleStmt :: LName -> Pos -> Type -> Stmt -> TI Stmt
 inferSingleStmt ln pos ctx s = do
-  (_wrapper, s', _ty') <- inferStmt ln pos ctx s
+  -- 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''