Scoped type variables (#2178)

Type variables in polymorphic types now scope over any nested local type signatures by default. Closes #2168.

- Any polymorphic type, whether written with an explicit `forall` or not, brings all its variables into scope in the body of its definition.
- Any type variables declared with an explicit `forall` are introduced as new variables, and in particular they will shadow any type variables already in scope with the same names.
- Any type variables not bound by an explicit `forall` *which are not already in scope* will be implicitly quantified.  Any such type variable names which are in scope will simply refer to the name in the enclosing scope.

So, for example, this will work:
```
def balance : RBNode k v -> RBTree k v = \t.
  let baseCase : RBTree k v = inr t in
  let balanceRR : RBNode k v -> RBTree k v = ...
  in undefined
end
```
The type signature on `balance` will bring `k` and `v` into scope in its body (even though there is not an explicit `forall` written); then the `k` and `v` in the type signatures on `baseCase` and `balanceRR` will both refer to the `k` and `v` bound in the type of `balance`.  In particular, this means that `inr t` is a valid definition for `baseCase` since their types match.  On the other hand, if one were to write
```
def balance : RBNode k v -> RBTree k v = \t.
  let baseCase : forall k v. RBTree k v = inr t in
  undefined
end
```
then the `k` and `v` in the type of `baseCase` would be *new* type variables which are different than the `k` and `v` in the type of `balance` (which would now be shadowed within the definition of `baseCase`).  This would now be a type error (which is what happens currently), since `baseCase` is required to be an `RBTree k v` for *any* types `k` and `v`, but `inr t` only has the specific type that was given as an input to `balance`.

Finally, if one wrote 
```
def balance : RBNode k v -> RBTree k v = \t.
  let baseCase : forall k. RBTree k v = inr t in
  undefined
end
```
then only `k` would be a new type variable, whereas `v` would refer to the `v` from the type of `balance`. (This would still be a type error, of course.)

In addition, what used to be `Polytype` is now two separate types: `RawPolytype` is what we get out of the parser, before implicit quantification has been carried out.  A `Polytype` is guaranteed to be properly quantified, i.e. variables bound by the forall are explicitly listed.  We carefully do not export the constructor so we can be sure that the typechecker is making sure that we never accidentally use a `RawPolytype` before we implicitly quantify over it.

src/swarm-doc/Swarm/Doc/Command.hs

@@ -62,7 +62,7 @@ mkEntry c =
   cmdInfo = constInfo c
   cmdEffects = effectInfo $ constDoc cmdInfo
 
-  getArgs ((Forall _ t)) = unchainFun t
+  getArgs = unchainFun . ptBody
 
   rawArgs = getArgs $ inferConst c
 

src/swarm-engine/Swarm/Game/Step.hs

@@ -640,10 +640,10 @@ stepCESK cesk = case cesk of
     _ -> badMachineState s "FProj frame with non-record value"
   -- To evaluate non-recursive let expressions, we start by focusing on the
   -- let-bound expression.
-  In (TLet _ False x mty mreq t1 t2) e s k ->
+  In (TLet _ False x _ mty mreq t1 t2) e s k ->
     return $ In t1 e s (FLet x ((,) <$> mty <*> mreq) t2 e : k)
   -- To evaluate a recursive let binding:
-  In (TLet _ True x mty mreq t1 t2) e s k -> do
+  In (TLet _ True x _ mty mreq t1 t2) e s k -> do
     -- First, allocate a cell for it in the store with the initial
     -- value of Blackhole.
     let (loc, s') = allocate VBlackhole s

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

@@ -81,6 +81,10 @@ delete x (Ctx c) = Ctx (M.delete x c)
 assocs :: Ctx t -> [(Var, t)]
 assocs = M.assocs . unCtx
 
+-- | Get the list of bound variables from a context.
+vars :: Ctx t -> [Var]
+vars = M.keys . unCtx
+
 -- | Add a key-value binding to a context (overwriting the old one if
 --   the key is already present).
 addBinding :: Var -> t -> Ctx t -> Ctx t

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

@@ -6,7 +6,6 @@
 -- Term elaboration which happens after type checking.
 module Swarm.Language.Elaborate where
 
-import Control.Applicative ((<|>))
 import Control.Lens (transform, (^.))
 import Swarm.Language.Syntax
 
@@ -46,11 +45,11 @@ elaborate = transform rewrite
     -- Eventually, once requirements analysis is part of typechecking,
     -- we'll infer them both at typechecking time then fill them in
     -- during elaboration here.
-    SLet ls r x mty mreq t1 t2 ->
-      let mty' = case ls of
-            LSDef -> mty <|> Just (t1 ^. sType)
+    SLet ls r x mty _ mreq t1 t2 ->
+      let mpty = case ls of
+            LSDef -> Just (t1 ^. sType)
             LSLet -> Nothing
-       in SLet ls r x mty' mreq t1 t2
+       in SLet ls r x mty mpty mreq t1 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
@@ -66,7 +65,7 @@ insertSuspend t = case t of
   TRequire {} -> thenSuspend
   TRequirements {} -> thenSuspend
   -- Recurse through def, tydef, bind, and annotate.
-  TLet ls r x mty mreq t1 t2 -> TLet ls r x mty mreq t1 (insertSuspend t2)
+  TLet ls r x mty mpty mreq t1 t2 -> TLet ls r x mty mpty 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/Kindcheck.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- |
 -- SPDX-License-Identifier: BSD-3-Clause
@@ -65,7 +66,7 @@ instance PrettyPrec KindError where
 
 -- | Check that a polytype is well-kinded.
 checkPolytypeKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Polytype -> m TydefInfo
-checkPolytypeKind pty@(Forall xs t) = TydefInfo pty (Arity $ length xs) <$ checkKind t
+checkPolytypeKind pty@(unPoly -> (xs, t)) = TydefInfo pty (Arity $ length xs) <$ checkKind t
 
 -- | Check that a type is well-kinded. For now, we don't allow
 --   higher-kinded types, *i.e.* all kinds will be of the form @Type

src/swarm-lang/Swarm/Language/LSP/Hover.hs

@@ -23,7 +23,7 @@ import Data.Foldable (asum)
 import Data.Graph
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Map qualified as M
-import Data.Maybe (catMaybes, fromMaybe)
+import Data.Maybe (catMaybes, fromMaybe, isNothing)
 import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.Lines qualified as R
@@ -111,7 +111,7 @@ narrowToPosition ::
 narrowToPosition s0@(Syntax' _ t _ ty) pos = fromMaybe s0 $ case t of
   SLam lv _ s -> d (locVarToSyntax' lv $ getInnerType ty) <|> d s
   SApp s1 s2 -> d s1 <|> d s2
-  SLet _ _ lv _ _ s1@(Syntax' _ _ _ lty) s2 -> d (locVarToSyntax' lv lty) <|> d s1 <|> d s2
+  SLet _ _ lv _ _ _ s1@(Syntax' _ _ _ lty) s2 -> d (locVarToSyntax' lv lty) <|> d s1 <|> d s2
   SBind mlv _ _ _ s1@(Syntax' _ _ _ lty) s2 -> (mlv >>= d . flip locVarToSyntax' (getInnerType lty)) <|> d s1 <|> d s2
   STydef typ typBody _ti s1 -> d s1 <|> Just (locVarToSyntax' typ $ fromPoly typBody)
   SPair s1 s2 -> d s1 <|> d s2
@@ -182,6 +182,15 @@ instance ExplainableType Polytype where
     t -> t
   eq = (==)
 
+instance ExplainableType RawPolytype where
+  fromPoly = forgetQ
+  prettyType = prettyTextLine
+  getInnerType = fmap $ \case
+    (l :->: _r) -> l
+    (TyCmd t) -> t
+    t -> t
+  eq r t = r == forgetQ t
+
 explain :: ExplainableType ty => Syntax' ty -> Tree Text
 explain trm = case trm ^. sTerm of
   TUnit -> literal "The unit value."
@@ -205,7 +214,7 @@ explain trm = case trm ^. sTerm of
   TRequire {} -> pure "Require a certain number of an entity."
   SRequirements {} -> pure "Query the requirements of a term."
   -- definition or bindings
-  SLet ls isRecursive var mTypeAnn _ rhs _b -> pure $ explainDefinition ls isRecursive var (rhs ^. sType) mTypeAnn
+  SLet ls isRecursive var mTypeAnn _ _ rhs _b -> pure $ explainDefinition ls isRecursive var (rhs ^. sType) mTypeAnn
   SLam (LV _s v) _mType _syn ->
     pure $
       typeSignature v ty $
@@ -264,15 +273,15 @@ explainFunction s =
           (map explain params)
       ]
 
-explainDefinition :: ExplainableType ty => LetSyntax -> Bool -> LocVar -> ty -> Maybe Polytype -> Text
+explainDefinition :: ExplainableType ty => LetSyntax -> Bool -> LocVar -> ty -> Maybe RawPolytype -> Text
 explainDefinition ls isRecursive (LV _s var) ty maybeTypeAnnotation =
   typeSignature var ty $
     T.unwords
       [ "A"
       , (if isRecursive then "" else "non-") <> "recursive"
       , if ls == LSDef then "definition" else "let"
       , "expression"
-      , if null maybeTypeAnnotation then "without" else "with"
+      , if isNothing maybeTypeAnnotation then "without" else "with"
       , "a type annotation on the variable."
       ]
 

src/swarm-lang/Swarm/Language/LSP/VarUsage.hs

@@ -101,10 +101,10 @@ getUsage bindings (CSyntax _pos t _comments) = case t of
   SLam v _ s -> checkOccurrences bindings v Lambda [s]
   SApp s1 s2 -> getUsage bindings s1 <> getUsage bindings s2
   -- Warn on unused 'let' bindings...
-  SLet LSLet _ v _ _ s1 s2 -> getUsage bindings s1 <> checkOccurrences bindings v Let [s2]
+  SLet LSLet _ v _ _ _ s1 s2 -> getUsage bindings s1 <> checkOccurrences bindings v Let [s2]
   -- But don't warn on unused 'def' bindings, because they may be
   -- intended to be used at a later REPL input.
-  SLet LSDef _ _ _ _ s1 s2 -> getUsage bindings s1 <> getUsage bindings s2
+  SLet LSDef _ _ _ _ _ s1 s2 -> getUsage bindings s1 <> getUsage bindings s2
   SPair s1 s2 -> getUsage bindings s1 <> getUsage bindings s2
   SBind maybeVar _ _ _ s1 s2 -> case maybeVar of
     Just v -> checkOccurrences bindings v Bind [s1, s2]

src/swarm-lang/Swarm/Language/Parser/Term.hs

@@ -104,8 +104,8 @@ parseTermAtom2 =
 
 -- | Construct an 'SLet', automatically filling in the Boolean field
 --   indicating whether it is recursive.
-sLet :: LetSyntax -> LocVar -> Maybe Polytype -> Syntax -> Syntax -> Term
-sLet ls x ty t1 = SLet ls (lvVar x `S.member` setOf freeVarsV t1) x ty mempty t1
+sLet :: LetSyntax -> LocVar -> Maybe RawPolytype -> Syntax -> Syntax -> Term
+sLet ls x ty t1 = SLet ls (lvVar x `S.member` setOf freeVarsV t1) x ty Nothing mempty t1
 
 sNoop :: Syntax
 sNoop = STerm (TConst Noop)
@@ -121,7 +121,7 @@ bindTydef xs ty
   | not (S.null free) =
       failT $
         "Undefined type variable(s) on right-hand side of tydef:" : S.toList free
-  | otherwise = return $ Forall xs ty
+  | otherwise = return . absQuantify $ mkPoly xs ty
  where
   free = tyVars ty `S.difference` S.fromList xs
 
@@ -160,7 +160,7 @@ parseExpr :: Parser Syntax
 parseExpr =
   parseLoc $ ascribe <$> parseExpr' <*> optional (symbol ":" *> parsePolytype)
  where
-  ascribe :: Syntax -> Maybe Polytype -> Term
+  ascribe :: Syntax -> Maybe RawPolytype -> Term
   ascribe s Nothing = s ^. sTerm
   ascribe s (Just ty) = SAnnotate s ty
 

src/swarm-lang/Swarm/Language/Parser/Type.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 -- |
@@ -13,13 +14,11 @@ module Swarm.Language.Parser.Type (
 ) where
 
 import Control.Lens (view)
-import Control.Monad (join)
 import Control.Monad.Combinators (many)
 import Control.Monad.Combinators.Expr (Operator (..), makeExprParser)
 import Data.Fix (Fix (..), foldFix)
 import Data.List.Extra (enumerate)
 import Data.Maybe (fromMaybe)
-import Data.Set qualified as S
 import Swarm.Language.Parser.Core (LanguageVersion (..), Parser, languageVersion)
 import Swarm.Language.Parser.Lex (
   braces,
@@ -34,34 +33,16 @@ import Swarm.Language.Parser.Lex (
 import Swarm.Language.Parser.Record (parseRecord)
 import Swarm.Language.Types
 import Text.Megaparsec (choice, optional, some, (<|>))
-import Witch (from)
 
 -- | Parse a Swarm language polytype, which starts with an optional
 --   quanitifation (@forall@ followed by one or more variables and a
 --   period) followed by a type.  Note that anything accepted by
 --   'parseType' is also accepted by 'parsePolytype'.
-parsePolytype :: Parser Polytype
+parsePolytype :: Parser RawPolytype
 parsePolytype =
-  join $
-    ( quantify . fromMaybe []
-        <$> optional ((reserved "forall" <|> reserved "∀") *> some tyVar <* symbol ".")
-    )
-      <*> parseType
- where
-  quantify :: [Var] -> Type -> Parser Polytype
-  quantify xs ty
-    -- Iplicitly quantify over free type variables if the user didn't write a forall
-    | null xs = return $ Forall (S.toList free) ty
-    -- Otherwise, require all variables to be explicitly quantified
-    | S.null free = return $ Forall xs ty
-    | otherwise =
-        fail $
-          unlines
-            [ "  Type contains free variable(s): " ++ unwords (map from (S.toList free))
-            , "  Try adding them to the 'forall'."
-            ]
-   where
-    free = tyVars ty `S.difference` S.fromList xs
+  mkPoly . fromMaybe []
+    <$> optional ((reserved "forall" <|> reserved "∀") *> some tyVar <* symbol ".")
+    <*> parseType
 
 -- | Parse a Swarm language (mono)type.
 parseType :: Parser Type

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

@@ -77,7 +77,7 @@ extractTCtx :: Syntax' ty -> TCtx
 extractTCtx (Syntax' _ t _ _) = extractTCtxTerm t
  where
   extractTCtxTerm = \case
-    SLet _ _ (LV _ x) mty _ _ t2 -> maybe id (Ctx.addBinding x) mty (extractTCtx t2)
+    SLet _ _ (LV _ x) _ mty _ _ t2 -> maybe id (Ctx.addBinding x) mty (extractTCtx t2)
     SBind mx _ mty _ c1 c2 ->
       maybe
         id
@@ -94,7 +94,7 @@ extractReqCtx :: Syntax' ty -> ReqCtx
 extractReqCtx (Syntax' _ t _ _) = extractReqCtxTerm t
  where
   extractReqCtxTerm = \case
-    SLet _ _ (LV _ x) _ mreq _ t2 -> maybe id (Ctx.addBinding x) mreq (extractReqCtx t2)
+    SLet _ _ (LV _ x) _ _ mreq _ t2 -> maybe id (Ctx.addBinding x) mreq (extractReqCtx t2)
     SBind mx _ _ mreq c1 c2 ->
       maybe
         id

src/swarm-lang/Swarm/Language/Requirements/Analysis.hs

@@ -109,15 +109,15 @@ requirements tdCtx ctx =
     -- will be used at least once in the body. We delete the let-bound
     -- name from the context when recursing for the same reason as
     -- lambda.
-    TLet LSLet r x mty _ t1 t2 -> do
+    TLet LSLet r x mty _ _ t1 t2 -> do
       when r $ add (singletonCap CRecursion)
       add (singletonCap CEnv)
       mapM_ polytypeRequirements mty
       local @ReqCtx (Ctx.delete x) $ go t1 *> go t2
     -- However, for def, we do NOT assume that the defined expression
     -- will be used at least once in the body; it may not be executed
     -- until later on, when the base robot has more capabilities.
-    TLet LSDef r x mty _ t1 t2 -> do
+    TLet LSDef r x mty _ _ t1 t2 -> do
       add (singletonCap CEnv)
       mapM_ polytypeRequirements mty
       localReqCtx <- ask @ReqCtx
@@ -160,9 +160,9 @@ requirements tdCtx ctx =
 
 polytypeRequirements ::
   (Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>
-  Polytype ->
+  Poly q Type ->
   m ()
-polytypeRequirements (Forall _ ty) = typeRequirements ty
+polytypeRequirements = typeRequirements . ptBody
 
 typeRequirements ::
   (Has (Accum Requirements) sig m, Has (Reader TDCtx) sig m) =>

src/swarm-lang/Swarm/Language/Syntax/AST.hs

@@ -100,10 +100,11 @@ data Term' ty
     --   annotation on the variable. The @Bool@ indicates whether
     --   it is known to be recursive.
     --
-    --   The @Maybe Requirements@ field is only for annotating the
-    --   requirements of a definition after typechecking; there is no
-    --   way to annotate requirements in the surface syntax.
-    SLet LetSyntax Bool LocVar (Maybe Polytype) (Maybe Requirements) (Syntax' ty) (Syntax' ty)
+    --   The @Maybe Polytype@ and @Maybe Requirements@ fields are only
+    --   for annotating the requirements of a definition after
+    --   typechecking; there is no way to annotate requirements in the
+    --   surface syntax.
+    SLet LetSyntax Bool LocVar (Maybe RawPolytype) (Maybe Polytype) (Maybe Requirements) (Syntax' ty) (Syntax' ty)
   | -- | A type synonym definition.  Note that this acts like a @let@
     --   (just like @def@), /i.e./ the @Syntax' ty@ field is the local
     --   context over which the type definition is in scope.
@@ -136,7 +137,7 @@ data Term' ty
   | -- | Record projection @e.x@
     SProj (Syntax' ty) Var
   | -- | Annotate a term with a type
-    SAnnotate (Syntax' ty) Polytype
+    SAnnotate (Syntax' ty) RawPolytype
   | -- | Run the given command, then suspend and wait for a new REPL
     --   input.
     SSuspend (Syntax' ty)

src/swarm-lang/Swarm/Language/Syntax/Pattern.hs

@@ -104,10 +104,10 @@ pattern (:$:) :: Term -> Syntax -> Term
 pattern (:$:) t1 s2 = SApp (STerm t1) s2
 
 -- | Match a TLet without annotations.
-pattern TLet :: LetSyntax -> Bool -> Var -> Maybe Polytype -> Maybe Requirements -> Term -> Term -> Term
-pattern TLet ls r v mty mreq t1 t2 <- SLet ls r (lvVar -> v) mty mreq (STerm t1) (STerm t2)
+pattern TLet :: LetSyntax -> Bool -> Var -> Maybe RawPolytype -> Maybe Polytype -> Maybe Requirements -> Term -> Term -> Term
+pattern TLet ls r v mty mpty mreq t1 t2 <- SLet ls r (lvVar -> v) mty mpty mreq (STerm t1) (STerm t2)
   where
-    TLet ls r v mty mreq t1 t2 = SLet ls r (LV NoLoc v) mty mreq (STerm t1) (STerm t2)
+    TLet ls r v mty mpty mreq t1 t2 = SLet ls r (LV NoLoc v) mty mpty mreq (STerm t1) (STerm t2)
 
 -- | Match a STydef without annotations.
 pattern TTydef :: Var -> Polytype -> Maybe TydefInfo -> Term -> Term
@@ -135,7 +135,7 @@ pattern TProj :: Term -> Var -> Term
 pattern TProj t x = SProj (STerm t) x
 
 -- | Match a TAnnotate without annotations.
-pattern TAnnotate :: Term -> Polytype -> Term
+pattern TAnnotate :: Term -> RawPolytype -> Term
 pattern TAnnotate t pt = SAnnotate (STerm t) pt
 
 -- | Match a TSuspend without annotations.

src/swarm-lang/Swarm/Language/Syntax/Pretty.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 -- We could avoid orphan instances by placing these PrettyPrec
@@ -104,12 +105,12 @@ instance PrettyPrec (Term' ty) where
               ConstMUnOp S -> pparens (p > pC) $ prettyPrec (succ pC) t2 <> ppr t1
               _ -> prettyPrecApp p t1 t2
       _ -> prettyPrecApp p t1 t2
-    SLet LSLet _ (LV _ x) mty _ t1 t2 ->
+    SLet LSLet _ (LV _ x) mty _ _ t1 t2 ->
       sep
         [ prettyDefinition "let" x mty t1 <+> "in"
         , ppr t2
         ]
-    SLet LSDef _ (LV _ x) mty _ t1 t2 ->
+    SLet LSDef _ (LV _ x) mty _ _ t1 t2 ->
       mconcat $
         sep [prettyDefinition "def" x mty t1, "end"]
           : case t2 of
@@ -136,7 +137,7 @@ instance PrettyPrec (Term' ty) where
       pparens (p > 10) $
         "suspend" <+> prettyPrec 11 t
 
-prettyDefinition :: Doc ann -> Var -> Maybe Polytype -> Syntax' ty -> Doc ann
+prettyDefinition :: Doc ann -> Var -> Maybe (Poly q Type) -> Syntax' ty -> Doc ann
 prettyDefinition defName x mty t1 =
   nest 2 . sep $
     [ flatAlt
@@ -153,8 +154,8 @@ prettyDefinition defName x mty t1 =
   eqAndLambdaLine = if null defLambdaList then "=" else line <> defEqLambdas
 
 prettyTydef :: Var -> Polytype -> Doc ann
-prettyTydef x (Forall [] ty) = "tydef" <+> pretty x <+> "=" <+> ppr ty <+> "end"
-prettyTydef x (Forall xs ty) = "tydef" <+> pretty x <+> hsep (map pretty xs) <+> "=" <+> ppr ty <+> "end"
+prettyTydef x (unPoly -> ([], ty)) = "tydef" <+> pretty x <+> "=" <+> ppr ty <+> "end"
+prettyTydef x (unPoly -> (xs, ty)) = "tydef" <+> pretty x <+> hsep (map pretty xs) <+> "=" <+> ppr ty <+> "end"
 
 prettyPrecApp :: Int -> Syntax' ty -> Syntax' ty -> Doc a
 prettyPrecApp p t1 t2 =

src/swarm-lang/Swarm/Language/Syntax/Util.hs

@@ -134,9 +134,9 @@ freeVarsS f = go S.empty
       | otherwise -> f s
     SLam x xty s1 -> rewrap $ SLam x xty <$> go (S.insert (lvVar x) bound) s1
     SApp s1 s2 -> rewrap $ SApp <$> go bound s1 <*> go bound s2
-    SLet ls r x xty xreq s1 s2 ->
+    SLet ls r x xty xpty xreq s1 s2 ->
       let bound' = S.insert (lvVar x) bound
-       in rewrap $ SLet ls r x xty xreq <$> go bound' s1 <*> go bound' s2
+       in rewrap $ SLet ls r x xty xpty xreq <$> go bound' s1 <*> go bound' s2
     STydef x xdef tdInfo t1 -> rewrap $ STydef x xdef tdInfo <$> go bound t1
     SPair s1 s2 -> rewrap $ SPair <$> go bound s1 <*> go bound s2
     SBind mx mty mpty mreq s1 s2 -> rewrap $ SBind mx mty mpty mreq <$> go bound s1 <*> go (maybe id (S.insert . lvVar) mx bound) s2