Lower the boom on the mess in the saw-script typechecker

intTests/test_type_errors/err003.log.good

@@ -0,0 +1,3 @@
+ Loading file "err003.saw"
+ err003.saw:3:16-3:27: Unbound type variable Nonexistent
+FAILED

intTests/test_type_errors/err003.saw

@@ -0,0 +1,8 @@
+
+let bar = do {
+   typedef t = Nonexistent;
+
+   let foo (a: t) = a;
+
+   return 0;
+};

intTests/test_type_errors/err004.log.good

@@ -0,0 +1,3 @@
+ Loading file "err004.saw"
+ err004.saw:2:13-2:24: Unbound type variable Nonexistent
+FAILED

intTests/test_type_errors/err004.saw

@@ -0,0 +1,4 @@
+
+typedef t = Nonexistent;
+
+let foo (a: t) = a;

intTests/test_type_errors/err005.log.good

@@ -0,0 +1,3 @@
+ Loading file "err005.saw"
+ err005.saw:1:30-1:31: Unbound type variable x
+FAILED

intTests/test_type_errors/err005.saw

@@ -0,0 +1 @@
+typedef x = { foo: Int, bar: x };

src/SAWScript/Interpreter.hs

@@ -65,7 +65,7 @@ import SAWScript.JavaExpr
 import SAWScript.LLVMBuiltins
 import SAWScript.Options
 import SAWScript.Lexer (lexSAW)
-import SAWScript.MGU (checkDecl, checkDeclGroup)
+import SAWScript.MGU (checkDecl, checkDeclGroup, checkStmt)
 import SAWScript.Parser (parseSchema)
 import SAWScript.TopLevel
 import SAWScript.Utils
@@ -294,6 +294,8 @@ processStmtBind printBinds pat expr = do -- mx mt
   -- 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
@@ -377,6 +379,18 @@ interpretStmt :: InteractiveMonad m =>
   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 (rwTypes rw) (rwTypedef rw) stmt
+-}
+
   case stmt of
 
     SS.StmtBind pos pat expr ->
@@ -412,9 +426,15 @@ interpretStmt printBinds stmt =
          putTopLevelRW $ rw { rwCryptol = cenv' }
          --showCryptolEnv
 
-    SS.StmtTypedef _ name ty ->
+    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 (rwTypes rw) (rwTypedef rw) pos ctx stmt
+         let (SS.StmtTypedef _ name ty) = stmt'
          putTopLevelRW $ addTypedef (getVal name) ty rw
 
 interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel ()

src/SAWScript/MGU.hs

@@ -18,6 +18,7 @@
 module SAWScript.MGU
        ( checkDecl
        , checkDeclGroup
+       , checkStmt
        , instantiate
        ) where
 
@@ -1186,7 +1187,7 @@
           getErrorTyVar pos
       else do
           -- note that this will ignore the extra params
           args' <- zipWithM checkType params args
           return $ TyCon pos tycon args'
 
   TyRecord pos fields -> do
@@ -1256,6 +1257,26 @@
     (res, _, []) -> Right res
     (_, _, errs) -> Left errs
 
+-- Check a single statement. (This is an external interface.)
+--
+-- The first two arguments are the starting variable and typedef
+-- environments to use.
+--
+-- The third is a current position, and the fourth is the
+-- context/monad type associated with the execution.
+checkStmt :: Map LName Schema -> Map Name Type -> Pos -> Context -> Stmt -> Either [(Pos, String)] Stmt
+checkStmt env tenv pos ctx stmt = do
+  -- Ugh. This should all be cleaned out further. XXX
+  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'
+
+
 -- Check a single declaration. (This is an external interface.)
 --
 -- The first two arguments are the starting variable and typedef