experiment: infer label type from its fallthrough default (#6163)#6176
Draft
ggreif wants to merge 2 commits into
Draft
experiment: infer label type from its fallthrough default (#6163)#6176ggreif wants to merge 2 commits into
ggreif wants to merge 2 commits into
Conversation
Builds on the parser desugaring: `label x = <default> <body>` now takes the
label's type from the default (the body block's final expression) when there
is no annotation, so the compact form needs no `: T` and works in synthesis
positions too (`let v = label found = false …` ⟹ `v : Bool`).
`LabelE` grows a bool flag, set by the parser action only when a default is
present and no annotation is written (the accepted grammar is unchanged). The
typechecker, for that flag:
- infers the block's final expression (the default — it cannot mention the
label) under a new `env.commit_notes = false`, which makes the central
exp/dec note-setters skip committing, so the whole block is then checked
intact and the body's `break`s check against that type;
- if the default diverges (`return`/trap : None) the inference is discarded
and the label falls back to the unit default, so unit `break`s still work.
An annotation, when present, wins (the flag is not consulted) — `label punt :
?Int = null …` keeps working, and sentinels are widened by annotating the
default itself: `label r = (null : ?Nat) …`.
`env.commit_notes` threads inward via the usual `{env with …}` (one literal
construction, in env_of_scope); record-completeness means no note-setter can
silently skip it. Desugaring takes the IR label type from the LabelE's own
inferred note rather than the annotation's (the unit placeholder in the infer
case).
Tests: test/run/label-default.mo (compact infer in synthesis + checking,
annotation-wins, annotated-default sentinel, bottom-default fallback, laziness,
bare label); test/fail/label-default-compact.mo (bare narrow sentinel rejects a
wider break). All backends green.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
Cursor AI review👍 APPROVE — looks safe to merge
VerdictDecision: APPROVE Generated for commit c95e053 |
Contributor
Group the annotation and the infer-from-default flag: `LabelE of id * (typ * bool) * exp` instead of `… * typ * exp * bool`. Every site that ignores the middle field — the wildcard matches in definedness, effect, traversals, interpret, and the `is_explicit_exp` arm — keeps its original 3-pattern form (no `, _` churn). Only the sites that read or build the type spec are touched: parser (construct the pair), typing (destructure), desugar (construct + lower), arrange/astjs (extract the typ). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
ggreif
commented
Jun 7, 2026
| | LoopE (e1, Some e2, _) -> "LoopE" $$ [exp e1; exp e2] | ||
| | ForE (p, e1, e2, _) -> "ForE" $$ [pat p; exp e1; exp e2] | ||
| | LabelE (i, t, e) -> "LabelE" $$ [id i; typ t; exp e] | ||
| | LabelE (i, (t, b), e) -> "LabelE" $$ [id i; typ t; exp e; Atom (string_of_bool b)] |
Contributor
Author
There was a problem hiding this comment.
the , defaulted should not be at the end
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Experimental, stacked on #6174 (the parser desugaring). #6174 makes the annotated
label x : T = <dflt> <body>work; this completes the issue by letting the compactlabel x = <dflt> <body>take its type from the default — no: T, and it works in synthesis positions too:Mechanism
LabelEgrows abool, set by the parser action only when a default is present and no annotation is written (accepted grammar unchanged). For that flag the typechecker infers the block's final expression (the default — it can't mention the label) and uses it as the label type;breaks check against it.To infer that sub-expression without committing its type notes (so the whole block is then checked intact),
envgrowscommit_notes : bool(defaulttrue, cleared for that one inference). It threads inward via the usual{env with …}; record-completeness means no note-setter can silently skip it. No global state.Semantics ("type wins")
label x = false …; break x trueBool(from the default)label r = (null : ?Nat) …; break r (?x)?Nat— annotate the default to widen a sentinellabel p : ?Int = null …; break p (?1)?Int— annotation wins (flag not consulted)label r = null …; break r (?x)?Nat ⊄ Null(Nullisn't bottom)label s = (return …) …; break sNo lub over break sites; the default (optionally annotated) is authoritative — like a
var/letinitializer.Tests
test/run/label-default.mo(compact infer in synthesis + checking, annotation-wins, annotated-default sentinel, bottom-default fallback, laziness, bare label) — all backends;test/fail/label-default-compact.mo(bare narrow sentinel rejects a wider break).🤖 Generated with Claude Code