@@ -29,6 +29,7 @@ module Swarm.Language.Typecheck (
2929 LocatedTCFrame (.. ),
3030 TCStack ,
3131 withFrame ,
32+ popFrame ,
3233
3334 -- * Typechecking monad
3435 fresh ,
@@ -133,6 +134,13 @@ type TCStack = [LocatedTCFrame]
133134withFrame :: Has (Reader TCStack ) sig m => SrcLoc -> TCFrame -> m a -> m a
134135withFrame l f = local (LocatedTCFrame l f : )
135136
137+ -- | Locally pop a frame from the typechecking stack.
138+ popFrame :: Has (Reader TCStack ) sig m => m a -> m a
139+ popFrame = local @ TCStack pop
140+ where
141+ pop (_ : fs) = fs
142+ pop [] = []
143+
136144------------------------------------------------------------
137145-- Type source
138146
@@ -1214,6 +1222,7 @@ inferConst c = run . runReader @TVCtx Ctx.empty . quantify $ case c of
12141222 Whoami -> [tyQ | Cmd Text |]
12151223 Setname -> [tyQ | Text -> Cmd Unit |]
12161224 Random -> [tyQ | Int -> Cmd Int |]
1225+ Run -> [tyQ | Text -> Cmd Unit |]
12171226 If -> [tyQ | Bool -> {a} -> {a} -> a |]
12181227 Inl -> [tyQ | a -> a + b |]
12191228 Inr -> [tyQ | b -> a + b |]
@@ -1369,52 +1378,57 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
13691378 let Syntax _ tt1 _ _ = t1
13701379 reqs = requirements tdCtx reqCtx tt1
13711380
1372- -- If we are checking a 'def', ensure t2 has a command type. This ensures that
1373- -- something like 'def ... end; x + 3' is not allowed, since this
1374- -- would result in the whole thing being wrapped in pure, like
1375- -- 'pure (def ... end; x + 3)', which means the def would be local and
1376- -- not persist to the next REPL input, which could be surprising.
1377- --
1378- -- On the other hand, 'let x = y in x + 3' is perfectly fine.
1379- when (ls == LSDef ) $ void $ decomposeCmdTy t2 (Expected , expected)
1380-
1381- -- Now check the type of the body, under a context extended with
1382- -- the type and requirements of the bound variable.
1383- t2' <-
1384- withBinding (lvVar x) upty $
1385- withBinding (lvVar x) reqs $
1386- check t2 expected
1387-
1388- -- Make sure none of the generated skolem variables have escaped.
1389- ask @ UCtx >>= traverse_ (noSkolems l skolems)
1390-
1391- -- Annotate a 'def' with requirements, but not 'let'. The reason
1392- -- is so that let introduces truly "local" bindings which never
1393- -- persist, but def introduces "global" bindings. Variables bound
1394- -- in the environment can only be used to typecheck future REPL
1395- -- terms if the environment holds not only a value but also a type
1396- -- + requirements for them. For example:
1397- --
1398- -- > def x : Int = 3 end; pure (x + 2)
1399- -- 5
1400- -- > x
1401- -- 3
1402- -- > let y : Int = 3 in y + 2
1403- -- 5
1404- -- > y
1405- -- 1:1: Unbound variable y
1406- -- > let y = 3 in def x = 5 end; pure (x + y)
1407- -- 8
1408- -- > y
1409- -- 1:1: Unbound variable y
1410- -- > x
1411- -- 5
1412- let mreqs = case ls of
1413- LSDef -> Just reqs
1414- LSLet -> Nothing
1415-
1416- -- Return the annotated let.
1417- return $ Syntax l (SLet ls r x mxTy mqxTy mreqs t1' t2') cs expected
1381+ -- Locally pop the typechecking frame that said we were checking
1382+ -- the definition of a let while typechecking the body. Even
1383+ -- though the body is a syntactic subterm of the let, we don't
1384+ -- want to see a bunch of nested typechecking frames.
1385+ popFrame $ do
1386+ -- If we are checking a 'def', ensure t2 has a command type. This ensures that
1387+ -- something like 'def ... end; x + 3' is not allowed, since this
1388+ -- would result in the whole thing being wrapped in pure, like
1389+ -- 'pure (def ... end; x + 3)', which means the def would be local and
1390+ -- not persist to the next REPL input, which could be surprising.
1391+ --
1392+ -- On the other hand, 'let x = y in x + 3' is perfectly fine.
1393+ when (ls == LSDef ) $ void $ decomposeCmdTy t2 (Expected , expected)
1394+
1395+ -- Now check the type of the body, under a context extended with
1396+ -- the type and requirements of the bound variable.
1397+ t2' <-
1398+ withBinding (lvVar x) upty $
1399+ withBinding (lvVar x) reqs $
1400+ check t2 expected
1401+
1402+ -- Make sure none of the generated skolem variables have escaped.
1403+ ask @ UCtx >>= traverse_ (noSkolems l skolems)
1404+
1405+ -- Annotate a 'def' with requirements, but not 'let'. The reason
1406+ -- is so that let introduces truly "local" bindings which never
1407+ -- persist, but def introduces "global" bindings. Variables bound
1408+ -- in the environment can only be used to typecheck future REPL
1409+ -- terms if the environment holds not only a value but also a type
1410+ -- + requirements for them. For example:
1411+ --
1412+ -- > def x : Int = 3 end; pure (x + 2)
1413+ -- 5
1414+ -- > x
1415+ -- 3
1416+ -- > let y : Int = 3 in y + 2
1417+ -- 5
1418+ -- > y
1419+ -- 1:1: Unbound variable y
1420+ -- > let y = 3 in def x = 5 end; pure (x + y)
1421+ -- 8
1422+ -- > y
1423+ -- 1:1: Unbound variable y
1424+ -- > x
1425+ -- 5
1426+ let mreqs = case ls of
1427+ LSDef -> Just reqs
1428+ LSLet -> Nothing
1429+
1430+ -- Return the annotated let.
1431+ return $ Syntax l (SLet ls r x mxTy mqxTy mreqs t1' t2') cs expected
14181432
14191433 -- Kind-check a type definition and then check the body under an
14201434 -- extended context.
0 commit comments