Skip to content

Carry a let expression's type annotation through to elaboration - #154

Merged
simonspies merged 1 commit into
mainfrom
let-annotation
Aug 1, 2026
Merged

Carry a let expression's type annotation through to elaboration#154
simonspies merged 1 commit into
mainfrom
let-annotation

Conversation

@simonspies

Copy link
Copy Markdown
Owner

parseLet parsed the annotation in let x : T = e in ... and discarded it, so let b : bool = n in 0 typechecked. AST.Expr.letIn now carries it, and elaboration uses it: with no arguments it is the bound value's own type and lands on the binder, so the bound expression is checked against it; with arguments it is the function's return type and lands on the fix. A destructuring let has no binder to carry it, so an annotation there is now rejected rather than dropped.

Found while writing a test that built a value at an annotated type. Independent of that work, so it is on its own.

@simonspies
simonspies merged commit 11135c2 into main Aug 1, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant