more comments, ensure def has command type, and properly make let loc…

…al vs def global

src/swarm-lang/Swarm/Language/Elaborate.hs

@@ -40,12 +40,15 @@ elaborate =
     -- (force x).  When interpreting t1, we will put a binding (x |->
     -- delay t1) in the context.
     --
-    -- Here we also take inferred types for variables bound by let or
-    -- bind and stuff them into the term itself, so that we will still
-    -- have access to them at runtime, after type annotations on the
-    -- AST are erased.  We need them at runtime so we can keep track
-    -- of the types of variables in scope, for use in typechecking
-    -- additional terms entered at the REPL.
+    -- Here we also take inferred types for variables bound by def or
+    -- bind (but NOT let) and stuff them into the term itself, so that
+    -- we will still have access to them at runtime, after type
+    -- annotations on the AST are erased.  We need them at runtime so
+    -- we can keep track of the types of variables in scope, for use
+    -- in typechecking additional terms entered at the REPL.  The
+    -- reason we do not do this for 'let' is so that 'let' introduces
+    -- truly local bindings which will not be available for use in
+    -- later REPL terms.
     --
     -- We assume requirements for these variables have already been
     -- filled in during typechecking.  The reason we need to wait
@@ -59,7 +62,10 @@ elaborate =
       let wrap
             | r = wrapForce (lvVar x) -- wrap in 'force' if recursive
             | otherwise = id
-       in SLet ls r x (mty <|> Just (t1 ^. sType)) mreq (wrap t1) (wrap t2)
+          mty' = case ls of
+            LSDef -> mty <|> Just (t1 ^. sType)
+            LSLet -> Nothing
+       in SLet ls r x mty' mreq (wrap t1) (wrap t2)
     SBind x (Just ty) _ mreq c1 c2 -> SBind x Nothing (Just ty) mreq c1 c2
     -- Rewrite @f $ x@ to @f x@.
     SApp (Syntax' _ (SApp (Syntax' _ (TConst AppF) _ _) l) _ _) r -> SApp l r
@@ -82,9 +88,8 @@ insertSuspend t = case t of
   TRequireDevice {} -> thenSuspend
   TRequire {} -> thenSuspend
   TRequirements {} -> thenSuspend
-  -- Recurse through let, tydef, bind, and annotate (but NOT through
-  -- let).
-  TLet LSDef r x mty mreq t1 t2 -> TLet LSDef r x mty mreq t1 (insertSuspend t2)
+  -- Recurse through def, tydef, bind, and annotate.
+  TLet ls r x mty mreq t1 t2 -> TLet ls r x mty mreq t1 (insertSuspend t2)
   TTydef x pty mtd t1 -> TTydef x pty mtd (insertSuspend t1)
   TBind mx mty mreq c1 c2 -> TBind mx mty mreq c1 (insertSuspend c2)
   TAnnotate t1 ty -> TAnnotate (insertSuspend t1) ty

src/swarm-lang/Swarm/Language/Typecheck.hs

@@ -54,7 +54,7 @@ import Control.Effect.Reader
 import Control.Effect.Throw
 import Control.Lens ((^.))
 import Control.Lens.Indexed (itraverse)
-import Control.Monad (forM_, when, (<=<), (>=>))
+import Control.Monad (forM_, void, when, (<=<), (>=>))
 import Control.Monad.Free (Free (..))
 import Data.Data (Data, gmapM)
 import Data.Foldable (fold, traverse_)
@@ -975,6 +975,15 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
     let Syntax' _ tt1 _ _ = t1
         reqs = requirements tdCtx reqCtx tt1
 
+    -- If we are checking a 'def', ensure t2 has a command type.  This ensures that
+    -- something like 'def ... end; x + 3' is not allowed, since this
+    -- would result in the whole thing being wrapped in return, like
+    -- 'return (def ... end; x + 3)', which means the def would be local and
+    -- not persist to the next REPL input, which could be surprising.
+    --
+    -- On the other hand, 'let x = y in x + 3' is perfectly fine.
+    when (ls == LSDef) $ void $ decomposeCmdTy t2 (Expected, expected)
+
     -- Now check the type of the body, under a context extended with
     -- the type and requirements of the bound variable.
     t2' <-
@@ -985,8 +994,33 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
     -- Make sure no skolem variables have escaped.
     ask @UCtx >>= mapM_ (noSkolems l)
 
+    -- Annotate a 'def' with requirements, but not 'let'.  The reason
+    -- is so that let introduces truly "local" bindings which never
+    -- persist, but def introduces "global" bindings.  Variables bound
+    -- in the environment can only be used to typecheck future REPL
+    -- terms if the environment holds not only a value but also a type
+    -- + requirements for them.  For example:
+    --
+    -- > def x : Int = 3 end; return (x + 2)
+    -- 5
+    -- > x
+    -- 3
+    -- > let y : Int = 3 in y + 2
+    -- 5
+    -- > y
+    -- 1:1: Unbound variable y
+    -- > let y = 3 in def x = 5 end; return (x + y)
+    -- 8
+    -- > y
+    -- 1:1: Unbound variable y
+    -- > x
+    -- 5
+    let mreqs = case ls of
+          LSDef -> Just reqs
+          LSLet -> Nothing
+
     -- Return the annotated let.
-    return $ Syntax' l (SLet ls r x mxTy (Just reqs) t1' t2') cs expected
+    return $ Syntax' l (SLet ls r x mxTy mreqs t1' t2') cs expected
 
   -- Kind-check a type definition and then check the body under an
   -- extended context.

test/unit/TestEval.hs

@@ -327,15 +327,15 @@ testEval g =
         "nesting"
         [ testCase
             "def nested in def"
-            ("def x : Int = def y : Int = 3 end; y + 2 end; x" `evaluatesTo` VInt 5)
+            ("def x : Cmd Int = def y : Int = 3 end; return (y + 2) end; x" `evaluatesTo` VInt 5)
         , testCase
             "nested def does not escape"
-            ( "def z = 1 end; def x = def z = 3 end; z + 2 end; x + z"
+            ( "def z = 1 end; def x = def z = 3 end; return (z + 2) end; n <- x; return (n + z)"
                 `evaluatesTo` VInt 6
             )
         , testCase
             "nested tydef"
-            ( "def x = (tydef X = Int end; def z : X = 3 end; z + 2) end; x"
+            ( "def x = (tydef X = Int end; def z : X = 3 end; return (z + 2)) end; x"
                 `evaluatesTo` VInt 5
             )
         ]

test/unit/TestLanguagePipeline.hs

@@ -625,6 +625,24 @@ testLanguagePipeline =
                 "1:1: Undefined type U"
             )
         ]
+    , testGroup
+        "let and def types"
+        [ testCase
+            "let at non-cmd type"
+            (valid "let x = 3 in x + 2")
+        , testCase
+            "let at cmd type"
+            (valid "let x = 3 in move; return (x+2)")
+        , testCase
+            "def at non-cmd type"
+            ( process
+                "def x = 3 end; x + 2"
+                "1:16: Type mismatch:\n  From context, expected `x + 2` to have a type like"
+            )
+        , testCase
+            "def at cmd type"
+            (valid "def x = 3 end; move; return (x+2)")
+        ]
     ]
  where
   valid = flip process ""