Type annotated binders #150
Conversation
|
This is passing all tests locally. Thank you so much @yiming-fang and @leoqiao18 for helping me port this! Since the changes are quite large, I'm just going to go ahead and format all the files we touched. In particular, I think the typechecker and |
|
Oh right, @yiming-fang is still working on getting lambda lifting working with recursive functions (which should also close #111). Since that's orthogonal to this PR, maybe you could merge that in on a separate PR? |
Sure, I can open a separate PR for lambda lifting mutually recursive lets. |
| -- consDefs <- constrainDefs defs finalConstraint | ||
| -- let annsVarPairs = map (uncarryAttachment . fst) binderDefs | ||
| -- -- vars = map snd annsVarPairs | ||
| -- exprTyps = map (TVarN . snd . uncarryAttachment . snd) binderDefs | ||
| -- forBinders ((ann, var), exprTyp) = | ||
| -- exists [var] <$> do | ||
| -- Ann.withAnnotations ann (TVarN var) \varExp -> | ||
| -- return $ CEqual varExp exprTyp | ||
| -- constraints <- mapM forBinders (zip annsVarPairs exprTyps) | ||
| -- return $ CAnd (consDefs : constraints) | ||
|
|
There was a problem hiding this comment.
I forgot to remove this commented-out block of code when I committed my fix. Could you help me clean this up @yiming-fang
There was a problem hiding this comment.
Other than this, I have no other suggestions. This PR is looking good!
There was a problem hiding this comment.
I forgot to remove this commented-out block of code when I committed my fix. Could you help me clean this up @yiming-fang
Done!
This PR adds type annotations/holes to all binders in lets, lambdas, and patterns, which get filled during the elaboration pass of type inference.