WIP: try fixing issue with monadic binders escaping their scope

i.e. #681.  Doesn't work yet; fixes one test case but still fails
others, and strangely seems to cause an unrelated test case to fail...

src/Swarm/Game/CESK.hs

@@ -159,6 +159,8 @@ data Frame
     --   in the given environment (extended by binding the variable,
     --   if there is one, to the output of the first command).
     FBind (Maybe Var) Term Env
+  | -- | We are evaluating a term which was wrapped in @TLocal@.
+    FLocal
   | -- | Discard any environment generated as the result of executing
     --   a command.
     FDiscardEnv
@@ -368,6 +370,7 @@ prettyFrame (FDef x) (_, inner) = (11, "def" <+> pretty x <+> "=" <+> inner <+>
 prettyFrame FExec inner = prettyPrefix "E·" inner
 prettyFrame (FBind Nothing t _) (p, inner) = (0, pparens (p < 1) inner <+> ";" <+> ppr t)
 prettyFrame (FBind (Just x) t _) (p, inner) = (0, hsep [pretty x, "<-", pparens (p < 1) inner, ";", ppr t])
+prettyFrame FLocal (p, inner) = (10, "inner" <+> pparens (p < 11) inner)
 prettyFrame FDiscardEnv inner = prettyPrefix "D·" inner
 prettyFrame (FImmediate c _worldUpds _robotUpds) inner = prettyPrefix ("I[" <> ppr c <> "]·") inner
 prettyFrame (FUpdate addr) inner = prettyPrefix ("S@" <> pretty addr) inner

src/Swarm/Game/Step.hs

@@ -531,6 +531,9 @@ stepCESK cesk = case cesk of
   -- If we see an update frame, it means we're supposed to set the value
   -- of a particular cell to the value we just finished computing.
   Out v s (FUpdate loc : k) -> return $ Out v (setCell loc (V v) s) k
+  -- XXX local
+  In (TLocal t) e s k -> return $ In t e s (FLocal : k)
+  Out v s (FLocal : k) -> return $ Out (VLocal v) s k
   ------------------------------------------------------------
   -- Execution
 
@@ -594,7 +597,6 @@ stepCESK cesk = case cesk of
   -- and the next continuation frame contains a previous environment
   -- to union with, then pass the unioned environments along in
   -- another VResult.
-
   Out (VResult v e2) s (FUnionEnv e1 : k) -> return $ Out (VResult v (e1 `union` e2)) s k
   -- Or, if a command completes with no environment, but there is a
   -- previous environment to union with, just use that environment.
@@ -613,6 +615,11 @@ stepCESK cesk = case cesk of
     robotContext . defReqs %= (`union` rctx)
     return $ Out v s k
   Out v s (FLoadEnv {} : k) -> return $ Out v s k
+
+  -- To execute a value wrapped in VLocal, we push a FDiscardEnv frame
+  -- on the stack and continue.
+  Out (VLocal v) s (FExec : k) -> return $ Out v s (FExec : FDiscardEnv : k)
+
   -- Any other type of value wiwth an FExec frame is an error (should
   -- never happen).
   Out _ s (FExec : _) -> badMachineState s "FExec frame with non-executable value"
@@ -2066,6 +2073,7 @@ compareValues v1 = case v1 of
   VBind {} -> incomparable v1
   VDelay {} -> incomparable v1
   VRef {} -> incomparable v1
+  VLocal {} -> incomparable v1
 
 -- | Values with different types were compared; this should not be
 --   possible since the type system should catch it.

src/Swarm/Language/Elaborate.hs

@@ -31,6 +31,10 @@ elaborate =
     . transform rewrite
  where
   rewrite :: Syntax' Polytype -> Syntax' Polytype
+  -- Any variables with a command type should be wrapped in TLocal,
+  -- to ensure any names bound by the commands they represent do not
+  -- escape into the context in which the variable is used.
+  rewrite s@(Syntax' l (TVar _) ty@(Forall _ (TyCmd _))) = Syntax' l (SLocal s) ty
   rewrite (Syntax' l t ty) = Syntax' l (rewriteTerm t) ty
 
   rewriteTerm :: Term' Polytype -> Term' Polytype

src/Swarm/Language/LSP/Hover.hs

@@ -152,3 +152,4 @@ explain = \case
   SDef {} -> pure $ pureDoc "A (recursive) definition command, which binds a variable to a value in subsequent commands."
   SBind {} -> pure $ pureDoc "A monadic bind for commands, of the form `c1 ; c2` or `x <- c1; c2`."
   SDelay {} -> pure $ pureDoc "Delay evaluation of a term, written `{...}`.  Swarm is an eager language, but in some cases (e.g. for `if` statements and recursive bindings) we need to delay evaluation.  The counterpart to `{...}` is `force`, where `force {t} = t`. Note that 'Force' is just a constant, whereas 'SDelay' has to be a special syntactic form so its argument can get special treatment during evaluation."
+  SLocal {} -> pure $ pureDoc "A wrapper for commands whose environment should not leak.  This never shows up in surface syntax."

src/Swarm/Language/Pretty.hs

@@ -129,6 +129,7 @@ instance PrettyPrec Term where
   prettyPrec p (TRequire n e) = pparens (p > 10) $ "require" <+> pretty n <+> ppr @Term (TText e)
   prettyPrec _ (TVar s) = pretty s
   prettyPrec _ (TDelay _ t) = braces $ ppr t
+  prettyPrec p (TLocal t) = pparens (p > 10) $ "local" <+> prettyPrec 11 t
   prettyPrec _ t@TPair {} = prettyTuple t
   prettyPrec _ (TLam x mty body) =
     "\\" <> pretty x <> maybe "" ((":" <>) . ppr) mty <> "." <+> ppr body

src/Swarm/Language/Requirement.hs

@@ -242,3 +242,4 @@ requirements' = go
     -- typechecked; Def commands are only allowed at the top level,
     -- so simply returning mempty is safe.
     TDef {} -> mempty
+    TLocal t -> go ctx t

src/Swarm/Language/Syntax.hs

@@ -68,6 +68,7 @@ module Swarm.Language.Syntax (
   pattern TDef,
   pattern TBind,
   pattern TDelay,
+  pattern TLocal,
 
   -- * Terms
   Var,
@@ -869,6 +870,8 @@ data Term' ty
     --   be a special syntactic form so its argument can get special
     --   treatment during evaluation.
     SDelay DelayType (Syntax' ty)
+  | -- | XXX
+    SLocal (Syntax' ty)
   deriving (Eq, Show, Functor, Foldable, Traversable, Data, Generic, FromJSON, ToJSON)
 
 -- The Traversable instance for Term (and for Syntax') is used during
@@ -979,8 +982,12 @@ pattern TBind mv t1 t2 <- SBind (fmap lvVar -> mv) (STerm t1) (STerm t2)
 pattern TDelay :: DelayType -> Term -> Term
 pattern TDelay m t = SDelay m (STerm t)
 
+-- | Match a TLocal without syntax
+pattern TLocal :: Term -> Term
+pattern TLocal t = SLocal (STerm t)
+
 -- | COMPLETE pragma tells GHC using this set of pattern is complete for Term
-{-# COMPLETE TUnit, TConst, TDir, TInt, TAntiInt, TText, TAntiText, TBool, TRequireDevice, TRequire, TVar, TPair, TLam, TApp, TLet, TDef, TBind, TDelay #-}
+{-# COMPLETE TUnit, TConst, TDir, TInt, TAntiInt, TText, TAntiText, TBool, TRequireDevice, TRequire, TVar, TPair, TLam, TApp, TLet, TDef, TBind, TDelay, TLocal #-}
 
 -- | Make infix operation (e.g. @2 + 3@) a curried function
 --   application (@((+) 2) 3@).
@@ -1028,6 +1035,7 @@ erase (SApp s1 s2) = TApp (eraseS s1) (eraseS s2)
 erase (SLet r x mty s1 s2) = TLet r (lvVar x) mty (eraseS s1) (eraseS s2)
 erase (SDef r x mty s) = TDef r (lvVar x) mty (eraseS s)
 erase (SBind mx s1 s2) = TBind (lvVar <$> mx) (eraseS s1) (eraseS s2)
+erase (SLocal s) = TLocal (eraseS s)
 
 ------------------------------------------------------------
 -- Free variable traversals
@@ -1069,6 +1077,7 @@ freeVarsS f = go S.empty
     SDef r x xty s1 -> rewrap $ SDef r x xty <$> go (S.insert (lvVar x) bound) s1
     SBind mx s1 s2 -> rewrap $ SBind mx <$> go bound s1 <*> go (maybe id (S.insert . lvVar) mx bound) s2
     SDelay m s1 -> rewrap $ SDelay m <$> go bound s1
+    SLocal s1 -> rewrap $ SLocal <$> go bound s1
    where
     rewrap s' = Syntax' l <$> s' <*> pure ty
 

src/Swarm/Language/Typecheck.hs

@@ -456,6 +456,9 @@ infer s@(Syntax l t) = (`catchError` addLocToTypeErr s) $ case t of
     c2' <- maybe id ((`withBinding` Forall [] a) . lvVar) mx $ infer c2
     _ <- decomposeCmdTy (c2' ^. sType)
     return $ Syntax' l (SBind mx c1' c2') (c2' ^. sType)
+  SLocal s1 -> do
+    s1' <- infer s1
+    return $ Syntax' l (SLocal s1') (s1' ^. sType)
  where
   noSkolems :: UPolytype -> Infer ()
   noSkolems (Forall xs upty) = do
@@ -655,6 +658,7 @@ analyzeAtomic locals (Syntax l t) = case t of
   SPair s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic locals s2
   SApp s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic locals s2
   SDelay _ s1 -> analyzeAtomic locals s1
+  SLocal s1 -> analyzeAtomic locals s1
   -- Bind is similarly simple except that we have to keep track of a local variable
   -- bound in the RHS.
   SBind mx s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic (maybe id (S.insert . lvVar) mx locals) s2

src/Swarm/Language/Value.hs

@@ -86,6 +86,8 @@ data Value where
   VDelay :: Term -> Env -> Value
   -- | A reference to a memory cell in the store.
   VRef :: Int -> Value
+  -- | XXX
+  VLocal :: Value -> Value
   deriving (Eq, Show, Generic, FromJSON, ToJSON)
 
 -- | Ensure that a value is not wrapped in 'VResult'.
@@ -118,6 +120,7 @@ valueToTerm (VResult v _) = valueToTerm v
 valueToTerm (VBind mx c1 c2 _) = TBind mx c1 c2
 valueToTerm (VDelay t _) = TDelay SimpleDelay t
 valueToTerm (VRef n) = TRef n
+valueToTerm (VLocal v) = TLocal (valueToTerm v)
 
 -- | An environment is a mapping from variable names to values.
 type Env = Ctx Value

test/unit/TestEval.hs

@@ -261,6 +261,12 @@ testEval g =
                   `evaluatesToP` VInt i
             )
         ]
+    , testGroup
+        "binders"
+        [ testCase
+            "binder in local scope #681"
+            ("def f = a <- return 1 end; let a = 2 in f; return a" `evaluatesTo` VInt 2)
+        ]
     ]
  where
   tquote :: String -> Text