From e580ce69ed9a5a28e066251d8cd7b75225bb063e Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Sat, 19 Oct 2024 13:26:38 -0500
Subject: [PATCH] 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            |   2 +-
 src/swarm-engine/Swarm/Game/Step.hs           |   4 +-
 src/swarm-lang/Swarm/Language/Context.hs      |   4 +
 src/swarm-lang/Swarm/Language/Elaborate.hs    |  11 +-
 src/swarm-lang/Swarm/Language/Kindcheck.hs    |   3 +-
 src/swarm-lang/Swarm/Language/LSP/Hover.hs    |  19 ++-
 src/swarm-lang/Swarm/Language/LSP/VarUsage.hs |   4 +-
 src/swarm-lang/Swarm/Language/Parser/Term.hs  |   8 +-
 src/swarm-lang/Swarm/Language/Parser/Type.hs  |  29 +---
 src/swarm-lang/Swarm/Language/Pipeline.hs     |   4 +-
 .../Swarm/Language/Requirements/Analysis.hs   |   8 +-
 src/swarm-lang/Swarm/Language/Syntax/AST.hs   |  11 +-
 .../Swarm/Language/Syntax/Pattern.hs          |   8 +-
 .../Swarm/Language/Syntax/Pretty.hs           |  11 +-
 src/swarm-lang/Swarm/Language/Syntax/Util.hs  |   4 +-
 src/swarm-lang/Swarm/Language/Typecheck.hs    |  91 +++++-----
 src/swarm-lang/Swarm/Language/Types.hs        | 159 +++++++++++++++---
 src/swarm-lang/Swarm/Language/Value.hs        |   2 +-
 .../Swarm/TUI/Controller/UpdateUI.hs          |   6 +-
 test/unit/TestLanguagePipeline.hs             |  43 ++---
 test/unit/TestPretty.hs                       |  11 +-
 21 files changed, 286 insertions(+), 156 deletions(-)

diff --git a/src/swarm-doc/Swarm/Doc/Command.hs b/src/swarm-doc/Swarm/Doc/Command.hs
index 53dd24496..7e30bfbb5 100644
--- a/src/swarm-doc/Swarm/Doc/Command.hs
+++ b/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
 
diff --git a/src/swarm-engine/Swarm/Game/Step.hs b/src/swarm-engine/Swarm/Game/Step.hs
index 8f32b6e2a..73f458659 100644
--- a/src/swarm-engine/Swarm/Game/Step.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/Context.hs b/src/swarm-lang/Swarm/Language/Context.hs
index f556f7ed9..ac78de5e7 100644
--- a/src/swarm-lang/Swarm/Language/Context.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/Elaborate.hs b/src/swarm-lang/Swarm/Language/Elaborate.hs
index 4b368798d..d07b24140 100644
--- a/src/swarm-lang/Swarm/Language/Elaborate.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/Kindcheck.hs b/src/swarm-lang/Swarm/Language/Kindcheck.hs
index aa0b4fea6..544b692aa 100644
--- a/src/swarm-lang/Swarm/Language/Kindcheck.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/LSP/Hover.hs b/src/swarm-lang/Swarm/Language/LSP/Hover.hs
index c2c1a9f29..92d14470f 100644
--- a/src/swarm-lang/Swarm/Language/LSP/Hover.hs
+++ b/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,7 +273,7 @@ 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
@@ -272,7 +281,7 @@ explainDefinition ls isRecursive (LV _s var) ty maybeTypeAnnotation =
       , (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."
       ]
 
diff --git a/src/swarm-lang/Swarm/Language/LSP/VarUsage.hs b/src/swarm-lang/Swarm/Language/LSP/VarUsage.hs
index 5b2fdd3cc..868770ab6 100644
--- a/src/swarm-lang/Swarm/Language/LSP/VarUsage.hs
+++ b/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]
diff --git a/src/swarm-lang/Swarm/Language/Parser/Term.hs b/src/swarm-lang/Swarm/Language/Parser/Term.hs
index b1eb4a87c..ab275a050 100644
--- a/src/swarm-lang/Swarm/Language/Parser/Term.hs
+++ b/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
 
diff --git a/src/swarm-lang/Swarm/Language/Parser/Type.hs b/src/swarm-lang/Swarm/Language/Parser/Type.hs
index 991e42ce5..1ba7cb5b6 100644
--- a/src/swarm-lang/Swarm/Language/Parser/Type.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/Pipeline.hs b/src/swarm-lang/Swarm/Language/Pipeline.hs
index db07f004f..207d4ab28 100644
--- a/src/swarm-lang/Swarm/Language/Pipeline.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs b/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs
index b04d4e35b..dd0af2671 100644
--- a/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs
+++ b/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs
@@ -109,7 +109,7 @@ 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
@@ -117,7 +117,7 @@ requirements tdCtx ctx =
     -- 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) =>
diff --git a/src/swarm-lang/Swarm/Language/Syntax/AST.hs b/src/swarm-lang/Swarm/Language/Syntax/AST.hs
index 706f149ec..f281bdb3b 100644
--- a/src/swarm-lang/Swarm/Language/Syntax/AST.hs
+++ b/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)
diff --git a/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs b/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs
index 5f564d729..4b3d4772c 100644
--- a/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs
+++ b/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.
diff --git a/src/swarm-lang/Swarm/Language/Syntax/Pretty.hs b/src/swarm-lang/Swarm/Language/Syntax/Pretty.hs
index 6f8d6670a..b48f11af1 100644
--- a/src/swarm-lang/Swarm/Language/Syntax/Pretty.hs
+++ b/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 =
diff --git a/src/swarm-lang/Swarm/Language/Syntax/Util.hs b/src/swarm-lang/Swarm/Language/Syntax/Util.hs
index f3ed8d1a1..bbd1c1b7a 100644
--- a/src/swarm-lang/Swarm/Language/Syntax/Util.hs
+++ b/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
diff --git a/src/swarm-lang/Swarm/Language/Typecheck.hs b/src/swarm-lang/Swarm/Language/Typecheck.hs
index 2f2784fbd..fe46f2f51 100644
--- a/src/swarm-lang/Swarm/Language/Typecheck.hs
+++ b/src/swarm-lang/Swarm/Language/Typecheck.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE QuasiQuotes #-}
@@ -200,9 +201,10 @@ runTC' ::
   TCtx ->
   ReqCtx ->
   TDCtx ->
-  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx m))))) USyntax ->
+  TVCtx ->
+  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx (ReaderC TVCtx m)))))) USyntax ->
   m (Either ContextualTypeErr TSyntax)
-runTC' ctx reqCtx tdctx =
+runTC' ctx reqCtx tdctx tvCtx =
   (>>= finalizeUSyntax)
     >>> runReader (toU ctx)
     >>> runReader []
@@ -210,6 +212,7 @@ runTC' ctx reqCtx tdctx =
     >>> U.runUnification
     >>> runReader reqCtx
     >>> runReader tdctx
+    >>> runReader tvCtx
     >>> fmap reportUnificationError
 
 -- | Run a top-level inference computation, returning either a
@@ -218,9 +221,10 @@ runTC ::
   TCtx ->
   ReqCtx ->
   TDCtx ->
-  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx Identity))))) USyntax ->
+  TVCtx ->
+  ReaderC UCtx (ReaderC TCStack (ErrorC ContextualTypeErr (U.UnificationC (ReaderC ReqCtx (ReaderC TDCtx (ReaderC TVCtx Identity)))))) USyntax ->
   Either ContextualTypeErr TSyntax
-runTC tctx reqCtx tdctx = runTC' tctx reqCtx tdctx >>> runIdentity
+runTC tctx reqCtx tdctx tvCtx = runTC' tctx reqCtx tdctx tvCtx >>> runIdentity
 
 checkPredicative :: Has (Throw ContextualTypeErr) sig m => Maybe a -> m a
 checkPredicative = maybe (throwError (mkRawTypeErr Impredicative)) pure
@@ -236,6 +240,7 @@ lookup ::
   ( Has (Throw ContextualTypeErr) sig m
   , Has (Reader TCStack) sig m
   , Has (Reader UCtx) sig m
+  , Has (Reader TVCtx) sig m
   , Has Unification sig m
   ) =>
   SrcLoc ->
@@ -273,8 +278,8 @@ instance FreeUVars UType where
   freeUVars = U.freeUVars
 
 -- | We can also get the free variables of a polytype.
-instance (FreeUVars t) => FreeUVars (Poly t) where
-  freeUVars (Forall _ t) = freeUVars t
+instance (FreeUVars t) => FreeUVars (Poly q t) where
+  freeUVars = freeUVars . ptBody
 
 -- | We can get the free variables in any polytype in a context.
 instance FreeUVars UCtx where
@@ -305,9 +310,9 @@ noSkolems ::
   ) =>
   SrcLoc ->
   [Var] ->
-  Poly UType ->
+  UPolytype ->
   m ()
-noSkolems l skolems (Forall xs upty) = do
+noSkolems l skolems (unPoly -> (xs, upty)) = do
   upty' <- applyBindings upty
   let tyvs =
         ucata
@@ -361,7 +366,7 @@ instance HasBindings UType where
   applyBindings = U.applyBindings
 
 instance HasBindings UPolytype where
-  applyBindings (Forall xs u) = Forall xs <$> applyBindings u
+  applyBindings = traverse applyBindings
 
 instance HasBindings UCtx where
   applyBindings = mapM applyBindings
@@ -378,10 +383,12 @@ instance (HasBindings u, Data u) => HasBindings (Syntax' u) where
 -- | To 'instantiate' a 'UPolytype', we generate a fresh unification
 --   variable for each variable bound by the `Forall`, and then
 --   substitute them throughout the type.
-instantiate :: Has Unification sig m => UPolytype -> m UType
-instantiate (Forall xs uty) = do
+instantiate :: (Has Unification sig m, Has (Reader TVCtx) sig m) => UPolytype -> m UType
+instantiate (unPoly -> (xs, uty)) = do
   xs' <- mapM (const fresh) xs
-  return $ substU (M.fromList (zip (map Left xs) xs')) uty
+  boundSubst <- ask @TVCtx
+  let s = M.mapKeys Left (M.fromList (zip xs xs') `M.union` unCtx boundSubst)
+  return $ substU s uty
 
 -- | 'skolemize' is like 'instantiate', except we substitute fresh
 --   /type/ variables instead of unification variables.  Such
@@ -389,13 +396,16 @@ instantiate (Forall xs uty) = do
 --   is used when checking something with a polytype explicitly
 --   specified by the user.
 --
---   Returns the list of generated Skolem variables along with the
---   substituted type.
-skolemize :: Has Unification sig m => UPolytype -> m ([Var], UType)
-skolemize (Forall xs uty) = do
+--   Returns a context mapping from instantiated type variables to generated
+--   Skolem variables, along with the substituted type.
+skolemize :: (Has Unification sig m, Has (Reader TVCtx) sig m) => UPolytype -> m (Ctx UType, UType)
+skolemize (unPoly -> (xs, uty)) = do
   skolemNames <- mapM (fmap (mkVarName "s") . const U.freshIntVar) xs
+  boundSubst <- ask @TVCtx
   let xs' = map UTyVar skolemNames
-  pure (skolemNames, substU (M.fromList (zip (map Left xs) xs')) uty)
+      newSubst = M.fromList $ zip xs xs'
+      s = M.mapKeys Left (newSubst `M.union` unCtx boundSubst)
+  pure (Ctx newSubst, substU s uty)
 
 -- | 'generalize' is the opposite of 'instantiate': add a 'Forall'
 --   which closes over all free type and unification variables.
@@ -414,8 +424,8 @@ generalize uty = do
       prettyNames = map T.pack (map (: []) alphabet ++ [x : show n | n <- [0 :: Int ..], x <- alphabet])
       -- Associate each free variable with a new pretty name
       renaming = zip fvs prettyNames
-  return $
-    Forall
+  return . absQuantify $
+    mkPoly
       (map snd renaming)
       (substU (M.fromList . map (Right *** UTyVar) $ renaming) uty')
 
@@ -797,7 +807,7 @@ decomposeProdTy = decomposeTyConApp2 TCProd
 --   types, type synonyms, and a term, either return a type error or a
 --   fully type-annotated version of the term.
 inferTop :: TCtx -> ReqCtx -> TDCtx -> Syntax -> Either ContextualTypeErr TSyntax
-inferTop ctx reqCtx tdCtx = runTC ctx reqCtx tdCtx . infer
+inferTop ctx reqCtx tdCtx = runTC ctx reqCtx tdCtx Ctx.empty . infer
 
 -- | Infer the type of a term, returning a type-annotated term.
 --
@@ -821,6 +831,7 @@ infer ::
   ( Has (Reader UCtx) sig m
   , Has (Reader ReqCtx) sig m
   , Has (Reader TDCtx) sig m
+  , Has (Reader TVCtx) sig m
   , Has (Reader TCStack) sig m
   , Has Unification sig m
   , Has (Error ContextualTypeErr) sig m
@@ -860,7 +871,7 @@ infer s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
   SLam x (Just argTy) body -> do
     adaptToTypeErr l KindErr $ checkKind argTy
     let uargTy = toU argTy
-    body' <- withBinding (lvVar x) (Forall [] uargTy) $ infer body
+    body' <- withBinding @UPolytype (lvVar x) (mkTrivPoly uargTy) $ infer body
     return $ Syntax' l (SLam x (Just argTy) body') cs (UTyFun uargTy (body' ^. sType))
 
   -- Need special case here for applying 'atomic' or 'instant' so we
@@ -962,20 +973,21 @@ infer s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
   -- However, we must be careful to deal properly with polymorphic
   -- type annotations.
   SAnnotate c pty -> do
-    _ <- adaptToTypeErr l KindErr $ checkPolytypeKind pty
-    let upty = toU pty
+    qpty <- quantify pty
+    _ <- adaptToTypeErr l KindErr $ checkPolytypeKind qpty
+    let upty = toU qpty
     -- Typecheck against skolemized polytype.
-    (skolems, uty) <- skolemize upty
+    (skolemSubst, uty) <- skolemize upty
     _ <- check c uty
     -- Make sure no skolem variables have escaped.
-    ask @UCtx >>= mapM_ (noSkolems l skolems)
+    ask @UCtx >>= mapM_ (noSkolems l (Ctx.vars skolemSubst))
     -- If check against skolemized polytype is successful,
     -- instantiate polytype with unification variables.
     -- Free variables should be able to unify with anything in
     -- following typechecking steps.
     iuty <- instantiate upty
     c' <- check c iuty
-    return $ Syntax' l (SAnnotate c' pty) cs iuty
+    return $ Syntax' l (SAnnotate c' (forgetQ qpty)) cs iuty
 
   -- Fallback: to infer the type of anything else, make up a fresh unification
   -- variable for its type and check against it.
@@ -985,7 +997,7 @@ infer s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
 
 -- | Infer the type of a constant.
 inferConst :: Const -> Polytype
-inferConst c = case c of
+inferConst c = run . runReader @TVCtx Ctx.empty . quantify $ case c of
   Wait -> [tyQ| Int -> Cmd Unit |]
   Noop -> [tyQ| Cmd Unit |]
   Selfdestruct -> [tyQ| Cmd Unit |]
@@ -1107,6 +1119,7 @@ check ::
   ( Has (Reader UCtx) sig m
   , Has (Reader ReqCtx) sig m
   , Has (Reader TDCtx) sig m
+  , Has (Reader TVCtx) sig m
   , Has (Reader TCStack) sig m
   , Has Unification sig m
   , Has (Error ContextualTypeErr) sig m
@@ -1144,7 +1157,7 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
           Left _ -> throwTypeErr l $ LambdaArgMismatch (joined argTy xTy)
           Right _ -> return ()
       Nothing -> return ()
-    body' <- withBinding (lvVar x) (Forall [] argTy) $ check body resTy
+    body' <- withBinding @UPolytype (lvVar x) (mkTrivPoly argTy) $ check body resTy
     return $ Syntax' l (SLam x mxTy body') cs (UTyFun argTy resTy)
 
   -- Special case for checking the argument to 'atomic' (or
@@ -1168,27 +1181,29 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
         return $ Syntax' l (SApp atomic' at') cs (UTyCmd argTy)
 
   -- Checking the type of a let- or def-expression.
-  SLet ls r x mxTy _ t1 t2 -> withFrame l (TCLet (lvVar x)) $ do
-    traverse_ (adaptToTypeErr l KindErr . checkPolytypeKind) mxTy
-    (skolems, upty, t1') <- case mxTy of
+  SLet ls r x mxTy _ _ t1 t2 -> withFrame l (TCLet (lvVar x)) $ do
+    mqxTy <- traverse quantify mxTy
+    (skolems, upty, t1') <- case mqxTy of
       -- No type annotation was provided for the let binding, so infer its type.
       Nothing -> do
         -- The let could be recursive, so we must generate a fresh
         -- unification variable for the type of x and infer the type
         -- of t1 with x in the context.
         xTy <- fresh
-        t1' <- withBinding (lvVar x) (Forall [] xTy) $ infer t1
+        t1' <- withBinding @UPolytype (lvVar x) (mkTrivPoly xTy) $ infer t1
         let uty = t1' ^. sType
         uty' <- unify (Just t1) (joined xTy uty)
         upty <- generalize uty'
         return ([], upty, t1')
-      -- An explicit polytype annotation has been provided. Skolemize it and check
-      -- definition and body under an extended context.
+      -- An explicit polytype annotation has been provided. Perform
+      -- implicit quantification, kind checking, and skolemization,
+      -- then check definition and body under an extended context.
       Just pty -> do
+        _ <- adaptToTypeErr l KindErr . checkPolytypeKind $ pty
         let upty = toU pty
         (ss, uty) <- skolemize upty
-        t1' <- withBinding (lvVar x) upty $ check t1 uty
-        return (ss, upty, t1')
+        t1' <- withBinding (lvVar x) upty . withBindings ss $ check t1 uty
+        return (Ctx.vars ss, upty, t1')
 
     -- Check the requirements of t1.
     tdCtx <- ask @TDCtx
@@ -1241,7 +1256,7 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
           LSLet -> Nothing
 
     -- Return the annotated let.
-    return $ Syntax' l (SLet ls r x mxTy mreqs t1' t2') cs expected
+    return $ Syntax' l (SLet ls r x mxTy mqxTy mreqs t1' t2') cs expected
 
   -- Kind-check a type definition and then check the body under an
   -- extended context.
@@ -1447,7 +1462,7 @@ analyzeAtomic locals (Syntax l t) = case t of
 
 -- | A simple polytype is a simple type with no quantifiers.
 isSimpleUPolytype :: UPolytype -> Bool
-isSimpleUPolytype (Forall [] ty) = isSimpleUType ty
+isSimpleUPolytype (unPoly -> ([], ty)) = isSimpleUType ty
 isSimpleUPolytype _ = False
 
 -- | A simple type is a sum or product of base types.
diff --git a/src/swarm-lang/Swarm/Language/Types.hs b/src/swarm-lang/Swarm/Language/Types.hs
index cd91460c8..d1198da9c 100644
--- a/src/swarm-lang/Swarm/Language/Types.hs
+++ b/src/swarm-lang/Swarm/Language/Types.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TemplateHaskell #-}
@@ -83,14 +84,26 @@ module Swarm.Language.Types (
   UnchainableFun (..),
 
   -- * Polytypes
-  Poly (..),
+  ImplicitQuantification (..),
+  Poly,
+  mkPoly,
+  mkQPoly,
+  mkTrivPoly,
+  unPoly,
+  ptVars,
+  ptBody,
   Polytype,
+  RawPolytype,
   pattern PolyUnit,
   UPolytype,
+  quantify,
+  absQuantify,
+  forgetQ,
 
   -- * Contexts
   TCtx,
   UCtx,
+  TVCtx,
 
   -- * User type definitions
   TydefInfo (..),
@@ -280,10 +293,6 @@ instance FromJSON1 TypeF where
 --   with 'Type' as if it were defined in a directly recursive way.
 type Type = Fix TypeF
 
--- | Get all the type variables contained in a 'Type'.
-tyVars :: Type -> Set Var
-tyVars = foldFix (\case TyVarF x -> S.singleton x; f -> fold f)
-
 newtype IntVar = IntVar Int
   deriving (Show, Data, Eq, Ord)
 
@@ -422,42 +431,124 @@ instance (UnchainableFun t, PrettyPrec t, SubstRec t) => PrettyPrec (TypeF t) wh
 -- Generic folding over type representations
 ------------------------------------------------------------
 
+-- | Type class for various type representations (e.g. 'Type',
+--   'UType') and generic operations we can perform on them.  This
+--   helps us avoid code duplication in some cases, by writing a
+--   single generic function which works for any 'Typical' instance.
 class Typical t where
-  foldT :: (TypeF t -> t) -> t -> t
+  -- | Fold a type into a summary value of some type @a@, given an
+  --   "empty" value of type @a@ (for use at e.g. Pure nodes in a
+  --   UType)
+  foldT :: a -> (TypeF a -> a) -> t -> a
+
+  -- | Refold a type into another type.  This is a special case of
+  --   'foldT' when we want to produce another type, since then we can
+  --   do something more sensible with 'Pure' nodes in a 'UType'
+  --   (i.e. preserve them instead of replacing them with a default
+  --   value).
+  refoldT :: (TypeF t -> t) -> t -> t
+
+  -- | Roll up one level of structure.
   rollT :: TypeF t -> t
+
+  -- | It should be possible to convert 'Type' to any type-ish thing.
   fromType :: Type -> t
 
 instance Typical Type where
-  foldT = foldFix
+  foldT _ = foldFix
+  refoldT = foldFix
   rollT = Fix
   fromType = id
 
 instance Typical UType where
-  foldT = ucata Pure
+  foldT e = ucata (const e)
+  refoldT = ucata Pure
   rollT = Free
   fromType = toU
 
+-- | Get all the type variables (/not/ unification variables)
+--   contained in a 'Type' or 'UType'.
+tyVars :: Typical t => t -> Set Var
+tyVars = foldT S.empty (\case TyVarF x -> S.singleton x; f -> fold f)
+
 ------------------------------------------------------------
 -- Polytypes
 ------------------------------------------------------------
 
--- | A @Poly t@ is a universally quantified @t@.  The variables in the
---   list are bound inside the @t@.  For example, the type @forall
---   a. a -> a@ would be represented as @Forall ["a"] (TyFun "a" "a")@.
-data Poly t = Forall {ptVars :: [Var], ptBody :: t}
-  deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, FromJSON, ToJSON)
+data ImplicitQuantification = Unquantified | Quantified
+  deriving (Eq, Ord, Read, Show)
 
--- | A polytype without unification variables.
-type Polytype = Poly Type
+-- | A @Poly q t@ is a universally quantified @t@.  The variables in
+--   the list are bound inside the @t@.  For example, the type @forall
+--   a. a -> a@ would be represented as @Forall ["a"] (TyFun "a"
+--   "a")@.
+--
+--   The type index @q@ is a phantom type index indicating whether the
+--   type has been implicitly quantified.  Immediately after a
+--   polytype is parsed it is 'Unquantified' and unsafe to use.  For
+--   example, the type @a -> a@ would parse literally as @Forall []
+--   (TyFun "a" "a") :: Poly Unquantified Type@, where the type
+--   variable @a@ is not in the list of bound variables.  Later, after
+--   running through 'quantify', it would become a @Poly Quantified
+--   Type@, either @Forall ["a"] (TyFun "a" "a")@ if the type variable
+--   is implicitly quantified, or unchanged if the type variable @a@
+--   was already in scope.
+--
+--   The @Poly@ constructor intentionally unexported, so that the
+--   only way to create a @Poly Quantified@ is through the 'quantify'
+--   function.
+data Poly (q :: ImplicitQuantification) t = Forall {_ptVars :: [Var], ptBody :: t}
+  deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, FromJSON, ToJSON)
 
-instance PrettyPrec Polytype where
+-- | Create a raw, unquantified @Poly@ value.
+mkPoly :: [Var] -> t -> Poly 'Unquantified t
+mkPoly = Forall
+
+-- | Create a polytype while performing implicit quantification.
+mkQPoly :: Typical t => t -> Poly 'Quantified t
+mkQPoly = absQuantify . Forall []
+
+-- | Create a trivial "polytype" with no bound variables.  This is
+--   somewhat unsafe --- only use this if you are sure that the polytype
+--   you want has no type variables.
+mkTrivPoly :: t -> Poly q t
+mkTrivPoly = Forall []
+
+-- | Project out the variables and body of a 'Poly' value.  It's only
+--   possible to project from a 'Poly Quantified' since the list of
+--   variables might be meaningless for a type that has not had
+--   implicit quantification applied.
+unPoly :: Poly 'Quantified t -> ([Var], t)
+unPoly (Forall xs t) = (xs, t)
+
+-- | Project out the variables of a 'Poly Quantified' value.
+ptVars :: Poly 'Quantified t -> [Var]
+ptVars (Forall xs _) = xs
+
+-- | Forget that a polytype has been properly quantified.
+forgetQ :: Poly 'Quantified t -> Poly 'Unquantified t
+forgetQ (Forall xs t) = Forall xs t
+
+-- | A regular polytype (without unification variables).  A @Polytype@
+--   (as opposed to a @RawPolytype@) is guaranteed to have implicit
+--   quantification properly applied, so that all type variables bound
+--   by the forall are explicitly listed.
+type Polytype = Poly 'Quantified Type
+
+-- | A raw polytype (without unification variables), which corresponds
+--   exactly to the way a polytype was written in source code.  In
+--   particular there may be type variables which are used in the type
+--   but not listed explicitly, which are to be implicitly quantified.
+type RawPolytype = Poly 'Unquantified Type
+
+instance PrettyPrec (Poly q Type) where
   prettyPrec _ (Forall [] t) = ppr t
   prettyPrec _ (Forall xs t) = hsep ("∀" : map pretty xs) <> "." <+> ppr t
 
 -- | A polytype with unification variables.
-type UPolytype = Poly UType
+type UPolytype = Poly 'Quantified UType
 
-instance PrettyPrec UPolytype where
+instance PrettyPrec (Poly q UType) where
   prettyPrec _ (Forall [] t) = ppr t
   prettyPrec _ (Forall xs t) = hsep ("∀" : map pretty xs) <> "." <+> ppr t
 
@@ -650,6 +741,34 @@ type TCtx = Ctx Polytype
 --   are in the midst of the type inference process.
 type UCtx = Ctx UPolytype
 
+-- | A @TVCtx@ tracks which type variables are in scope, and what
+--   skolem variables were assigned to them.
+type TVCtx = Ctx UType
+
+------------------------------------------------------------
+-- Implicit quantification of polytypes
+------------------------------------------------------------
+
+-- | Implicitly quantify any otherwise unbound type variables.
+quantify ::
+  (Has (Reader TVCtx) sig m, Typical ty) =>
+  Poly 'Unquantified ty ->
+  m (Poly 'Quantified ty)
+quantify (Forall xs ty) = do
+  inScope <- ask @TVCtx
+  -- Look at all variables which occur in the type but are not
+  -- explicitly bound by the forall, and and are not bound in the
+  -- context.  Such variables must be implicitly quantified.
+  let implicit =
+        (tyVars ty `S.difference` S.fromList xs)
+          `S.difference` M.keysSet (Ctx.unCtx inScope)
+  pure $ Forall (xs ++ S.toList implicit) ty
+
+-- | Absolute implicit quantification, i.e. assume there are no type
+--   variables in scope.
+absQuantify :: Typical t => Poly 'Unquantified t -> Poly 'Quantified t
+absQuantify = run . runReader @TVCtx Ctx.empty . quantify
+
 ------------------------------------------------------------
 -- Type definitions
 ------------------------------------------------------------
@@ -693,7 +812,7 @@ expandTydef userTyCon tys = do
 -- | Given the definition of a type alias, substitute the given
 --   arguments into its body and return the resulting type.
 substTydef :: forall t. Typical t => TydefInfo -> [t] -> t
-substTydef (TydefInfo (Forall as ty) _) tys = foldT @t substF (fromType ty)
+substTydef (TydefInfo (Forall as ty) _) tys = refoldT @t substF (fromType ty)
  where
   argMap = M.fromList $ zip as tys
 
@@ -707,7 +826,7 @@ substTydef (TydefInfo (Forall as ty) _) tys = foldT @t substF (fromType ty)
 --   a term containing a local tydef: since the tydef is local we
 --   can't use it in the reported type.
 elimTydef :: forall t. Typical t => Var -> TydefInfo -> t -> t
-elimTydef x tdInfo = foldT substF
+elimTydef x tdInfo = refoldT substF
  where
   substF = \case
     TyConF (TCUser u) tys | u == x -> substTydef tdInfo tys
diff --git a/src/swarm-lang/Swarm/Language/Value.hs b/src/swarm-lang/Swarm/Language/Value.hs
index 5b8c81072..c1b25e2ca 100644
--- a/src/swarm-lang/Swarm/Language/Value.hs
+++ b/src/swarm-lang/Swarm/Language/Value.hs
@@ -225,7 +225,7 @@ valueToTerm = \case
     M.foldrWithKey
       ( \y v -> case v of
           VIndir {} -> id
-          _ -> TLet LSLet False y Nothing Nothing (valueToTerm v)
+          _ -> TLet LSLet False y Nothing Nothing Nothing (valueToTerm v)
       )
       (TLam x Nothing t)
       (M.restrictKeys (Ctx.unCtx (e ^. envVals)) (S.delete x (setOf freeVarsV (Syntax' NoLoc t Empty ()))))
diff --git a/src/swarm-tui/Swarm/TUI/Controller/UpdateUI.hs b/src/swarm-tui/Swarm/TUI/Controller/UpdateUI.hs
index 236464c97..d43ace238 100644
--- a/src/swarm-tui/Swarm/TUI/Controller/UpdateUI.hs
+++ b/src/swarm-tui/Swarm/TUI/Controller/UpdateUI.hs
@@ -326,6 +326,6 @@ generateNotificationPopups = do
 -- | Strips the top-level @Cmd@ from a type, if any (to compute the
 --   result type of a REPL command evaluation).
 stripCmd :: TDCtx -> Polytype -> Polytype
-stripCmd tdCtx (Forall xs ty) = case whnfType tdCtx ty of
-  TyCmd resTy -> Forall xs resTy
-  _ -> Forall xs ty
+stripCmd tdCtx = fmap $ \ty -> case whnfType tdCtx ty of
+  TyCmd resTy -> resTy
+  _ -> ty
diff --git a/test/unit/TestLanguagePipeline.hs b/test/unit/TestLanguagePipeline.hs
index 6eb772614..5baba5fc1 100644
--- a/test/unit/TestLanguagePipeline.hs
+++ b/test/unit/TestLanguagePipeline.hs
@@ -33,27 +33,27 @@ testLanguagePipeline =
   testGroup
     "Language - pipeline"
     [ testCase "end semicolon #79" (valid "def a = 41 end def b = a + 1 end def c = b + 2 end")
-    , testCase
-        "quantification #148 - implicit"
-        (valid "def id : a -> a = \\x. x end; id move")
-    , testCase
-        "quantification #148 - explicit"
-        (valid "def id : forall a. a -> a = \\x. x end; id move")
-    , testCase
-        "quantification #148 - explicit with free tyvars"
-        ( process
-            "def id : forall a. b -> b = \\x. x end; id move"
-            ( T.unlines
-                [ "1:27:"
-                , "  |"
-                , "1 | def id : forall a. b -> b = \\x. x end; id move"
-                , "  |                           ^"
-                , "  Type contains free variable(s): b"
-                , "  Try adding them to the 'forall'."
-                , ""
-                ]
+    , testGroup
+        "quantification + scope"
+        [ testCase
+            "quantification #148 - implicit"
+            (valid "def id : a -> a = \\x. x end; id move")
+        , testCase
+            "quantification #148 - explicit"
+            (valid "def id : forall a. a -> a = \\x. x end; id move")
+        , testCase
+            "quantification #148 - explicit with free tyvars"
+            (valid "def id : forall a. b -> b = \\x. x end; id move")
+        , testCase
+            "type variable scope #2178"
+            (valid "def f : a -> (a * Int) = \\x. let g : a * Int = (x, 3) in g end")
+        , testCase
+            "type variable scope #2178 - shadowing"
+            ( process
+                "def f : a -> (a * Int) = \\x. let g : forall a. a * Int = (x, 3) in g end"
+                "1:59: Type mismatch:\n  From context, expected `x` to have type `s2`,\n  but it actually has type `s1`"
             )
-        )
+        ]
     , testCase
         "parsing operators #188 - parse valid operator (!=)"
         (valid "1!=(2)")
@@ -376,6 +376,7 @@ testLanguagePipeline =
 
                   isVar (TVar {}) = True
                   isVar _ = False
+                  getVars :: TSyntax -> [(Term' Polytype, Polytype)]
                   getVars = map (_sTerm &&& _sType) . filter (isVar . _sTerm) . universe
                in assertEqual
                     "variable types"
@@ -403,7 +404,7 @@ testLanguagePipeline =
             "type ascription doesn't allow rank 2 types"
             ( process
                 "\\f. (f:forall a. a->a) 3"
-                "1:5: Skolem variable s3 would escape its scope"
+                "1:24: Type mismatch:\n  From context, expected `3` to have type `s3`,\n  but it actually has type `Int`"
             )
         , testCase
             "checking a lambda with the wrong argument type"
diff --git a/test/unit/TestPretty.hs b/test/unit/TestPretty.hs
index 0e61053de..fac55b759 100644
--- a/test/unit/TestPretty.hs
+++ b/test/unit/TestPretty.hs
@@ -91,7 +91,7 @@ testPrettyConst =
     , testCase
         "type ascription"
         ( equalPrettyLine "1 : Int" $
-            TAnnotate (TInt 1) (Forall [] TyInt)
+            TAnnotate (TInt 1) (mkTrivPoly TyInt)
         )
     , testCase
         "lambda precedence (#1468)"
@@ -218,23 +218,22 @@ testPrettyConst =
         "tydef"
         [ testCase "tydef alias" $
             equalPrettyLine "tydef X = Int end" $
-              TTydef "X" (Forall [] TyInt) Nothing (TConst Noop)
+              TTydef "X" (mkTrivPoly TyInt) Nothing (TConst Noop)
         , testCase "tydef Maybe" $
             equalPrettyLine "tydef Maybe a = Unit + a end" $
-              TTydef "Maybe" (Forall ["a"] (TyUnit :+: TyVar "a")) Nothing (TConst Noop)
+              TTydef "Maybe" (mkQPoly (TyUnit :+: TyVar "a")) Nothing (TConst Noop)
         , testCase "tydef multi-arg" $
             equalPrettyLine "tydef Foo a b c d = Unit + ((a * b) + ((c -> d) * a)) end" $
               TTydef
                 "Foo"
-                ( Forall
-                    ["a", "b", "c", "d"]
+                ( mkQPoly
                     (TyUnit :+: (TyVar "a" :*: TyVar "b") :+: ((TyVar "c" :->: TyVar "d") :*: TyVar "a"))
                 )
                 Nothing
                 (TConst Noop)
         , testCase "consecutive tydef" $
             equalPrettyLine "tydef X = Int end\n\ntydef Y = Bool end" $
-              TTydef "X" (Forall [] TyInt) Nothing (TTydef "Y" (Forall [] TyBool) Nothing (TConst Noop))
+              TTydef "X" (mkTrivPoly TyInt) Nothing (TTydef "Y" (mkTrivPoly TyBool) Nothing (TConst Noop))
         ]
     , testGroup
         "recursive types"