Scoped type variables

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

@@ -18,6 +18,7 @@ import Data.Aeson (FromJSON (..), ToJSON (..), genericParseJSON, genericToJSON)
 import Data.Data (Data)
 import Data.Map (Map)
 import Data.Map qualified as M
+import Data.Maybe (isJust)
 import Data.Text (Text)
 import GHC.Generics (Generic)
 import Prettyprinter (brackets, emptyDoc, hsep, punctuate)
@@ -69,6 +70,10 @@ singleton x t = Ctx (M.singleton x t)
 lookup :: Var -> Ctx t -> Maybe t
 lookup x (Ctx c) = M.lookup x c
 
+-- | Check whether a context contains a certain variable as a key.
+member :: Var -> Ctx t -> Bool
+member x = isJust . lookup x
+
 -- | Look up a variable in a context in an ambient Reader effect.
 lookupR :: Has (Reader (Ctx t)) sig m => Var -> m (Maybe t)
 lookupR x = lookup x <$> ask
@@ -81,6 +86,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

@@ -108,15 +108,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
@@ -159,9 +159,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 =