Skip to content

Commit

Permalink
also generalize local binds
Browse files Browse the repository at this point in the history
  • Loading branch information
byorgey committed Sep 9, 2023
1 parent 1bb1a23 commit f58e2a6
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 7 deletions.
9 changes: 2 additions & 7 deletions src/Swarm/Language/Typecheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -680,14 +680,9 @@ infer s@(Syntax l t) = addLocToTypeErr l $ case t of
SBind mx c1 c2 -> do
c1' <- withFrame l TCBindL $ infer c1
a <- decomposeCmdTy c1 (Actual, c1' ^. sType)
-- We do not need to generalize the type 'a' here (unlike
-- top-level binds) because a variable bound here (mx) can only
-- have local scope. In other words, when we generalize at the
-- very end, the variable will no longer be in the context, so we
-- will be able to safely generalize over any unification
-- variables that occurred in its type.
genA <- generalize a
c2' <-
maybe id ((`withBinding` Forall [] a) . lvVar) mx
maybe id ((`withBinding` genA) . lvVar) mx
. withFrame l TCBindR
$ infer c2
_ <- decomposeCmdTy c2 (Actual, c2' ^. sType)
Expand Down
3 changes: 3 additions & 0 deletions test/unit/TestLanguagePipeline.hs
Original file line number Diff line number Diff line change
Expand Up @@ -389,6 +389,9 @@ testLanguagePipeline =
, testCase
"top-level bind is polymorphic"
(valid "f <- return (\\x.x); return (f 3, f \"hi\")")
, testCase
"local bind is polymorphic"
(valid "def foo : cmd (int * text) = f <- return (\\x.x); return (f 3, f \"hi\") end")
]
]
where
Expand Down

0 comments on commit f58e2a6

Please sign in to comment.