Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix type inference for recursive let bindings #2187

Merged
merged 2 commits into from
Oct 19, 2024
Merged

Fix type inference for recursive let bindings #2187

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b40fc1d
fix type inference for recursive let bindings
byorgey Oct 19, 2024
9175c93
Merge branch 'main' into fix/2186-infer-recursive-let
mergify[bot] Oct 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions src/swarm-lang/Swarm/Language/Typecheck.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ import Data.Set qualified as S
import Data.Text (Text)
import Data.Text qualified as T
import Prettyprinter
import Swarm.Effect.Unify (Unification, UnificationError, (=:=))
import Swarm.Effect.Unify (Unification, UnificationError)
import Swarm.Effect.Unify qualified as U
import Swarm.Effect.Unify.Fast qualified as U
import Swarm.Language.Context hiding (lookup)
Expand Down Expand Up @@ -342,7 +342,7 @@ unify ::
TypeJoin ->
m UType
unify ms j = do
res <- expected =:= actual
res <- expected U.=:= actual
case res of
Left _ -> do
j' <- traverse U.applyBindings j
Expand Down Expand Up @@ -1135,7 +1135,7 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
traverse_ (adaptToTypeErr l KindErr . checkKind) mxTy
case toU mxTy of
Just xTy -> do
res <- argTy =:= xTy
res <- argTy U.=:= xTy
case res of
-- Generate a special error when the explicit type annotation
-- on a lambda doesn't match the expected type,
Expand Down Expand Up @@ -1179,8 +1179,8 @@ check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of
xTy <- fresh
t1' <- withBinding (lvVar x) (Forall [] xTy) $ infer t1
let uty = t1' ^. sType
_ <- xTy =:= uty
upty <- generalize uty
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.
Expand Down
6 changes: 6 additions & 0 deletions test/unit/TestLanguagePipeline.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -556,6 +556,12 @@ testLanguagePipeline =
"(\\f. f 3) 2"
"1:11: Type mismatch:\n From context, expected `2` to have a type like `Int -> _`"
)
, testCase
"inferring type of bad recursive function - #2186"
( process
"def bad = \\acc.\\n. if (n <= 0) {fst acc} {bad (fst acc + 1) (n - 1)} end"
"1:1: Type mismatch:\n From context, expected `\\acc. \\n. if (n <= 0) {fst acc} {\n bad (fst acc + 1) (n - 1)\n }` to have type `Int -> Int -> Int`,\n but it actually has a type like `(Int * _) -> Int -> Int`"
)
]
, testGroup
"generalize top-level binds #351 #1501"
Expand Down