Repository navigation
Type a let destructuring a GADT without switch diagnostics - #9081
Conversation
Changelog💅 Polish
Semantic Diff2 commits · Full page ✏️ Type a let destructuring a GADT without switch diagnostics6612b69 · cknitt + Claude · Oct 27, 2026, 12:45 UTC · edited
Typedtree modified (let destructuring a GADT constructor) type rec any = Any('a, 'a => string): any
let get = value => {
let Any(x, f) = value
f(x)
}
expression
+ attribute "#let_gadt_pattern"
+ []
Texp_match
expression
Texp_ident "value/1004"
<case>
pattern
Tpat_construct "Any"
…
expression
Texp_apply
…Decision modified (diagnostic context of a match's cases)
match with @let.unwrap ↦ LetUnwrap
match with #optional_arg_default ↦ Function
-match typed for a let with a GADT pattern ↦ Switch
+match with #let_gadt_pattern ↦ Function
any other match ↦ SwitchDiagnostic modified (type error in the body of a let destructuring a GADT) type rec any = Any('a, 'a => string): any
let get = value => {
let Any(x, _) = value
x
}
This has type: $a
-But this switch is expected to return: 'a
+But it's expected to have type: 'a
$a is an existential type bound by the constructor Any.
It is only known in the scope of the pattern that matches Any.
-
-All branches in a switch must return the same type.
-To fix this, change your branch to return the expected type.✨ Records show the changed operation before its consequences232ccf2 · cristianoc + Claude · Oct 29, 2026, 14:10 UTC · new The records skill asked for a block for each object a commit changes in what the compiler does, and a record of #9081 met it with the diagnostic alone, leaving the attribute the type checker adds to the synthesized match in prose. A record now shows the representation, rule, transformation or decision that changes, at its own level, and then its consequences; a change the prose names is shown in a block, a change no form prints is shown as a schematic, and a script or review fix that changes behaviour gets blocks. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## fix-9068-existential-names #9081 +/- ##
===========================================================
Coverage 81.55% 81.55%
===========================================================
Files 460 460
Lines 64742 64744 +2
===========================================================
+ Hits 52800 52804 +4
+ Misses 11942 11940 -2
🚀 New features to boost your workflow:
|
rescript
@rescript/belt
@rescript/darwin-arm64
@rescript/linux-arm64
@rescript/linux-x64
@rescript/runtime
@rescript/win32-x64
commit: |
|
@codex review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
adfceb2 to
829f98b
Compare
829f98b to
6a7f2a6
Compare
Why:
A `let` whose pattern contains a GADT constructor is typed as a
one-case match, and that match took the diagnostic context of a
`switch` in the source: a type error in the rest of the block said
"But this switch is expected to return" and added the hint about
switch branches, although the source has no switch. The match now
carries `#let_gadt_pattern`, and its cases, like those of the match
for an optional argument default, get function-style diagnostics.
Typedtree modified (let destructuring a GADT constructor):
Example:
type rec any = Any('a, 'a => string): any
let get = value => {
let Any(x, f) = value
f(x)
}
Before (typed):
expression
Texp_match
expression
Texp_ident "value/1004"
[
<case>
pattern
Tpat_construct "Any"
…
expression
Texp_apply
…
]
After (typed):
expression
attribute "#let_gadt_pattern"
[]
Texp_match
expression
Texp_ident "value/1004"
[
<case>
pattern
Tpat_construct "Any"
…
expression
Texp_apply
…
]
Decision modified (diagnostic context of a match's cases):
Before (text): `call_context` in `Typecore.type_expect_`
match with @let.unwrap ↦ LetUnwrap
match with #optional_arg_default ↦ Function
match typed for a let with a GADT pattern ↦ Switch
any other match ↦ Switch
After (text):
match with @let.unwrap ↦ LetUnwrap
match with #optional_arg_default ↦ Function
match with #let_gadt_pattern ↦ Function
any other match ↦ Switch
Diagnostic modified (type error in the body of a let destructuring a GADT):
Example:
type rec any = Any('a, 'a => string): any
let get = value => {
let Any(x, _) = value
x
}
Before (diagnostic):
This has type: $a
But this switch is expected to return: 'a
$a is an existential type bound by the constructor Any.
It is only known in the scope of the pattern that matches Any.
All branches in a switch must return the same type.
To fix this, change your branch to return the expected type.
After (diagnostic):
This has type: $a
But it's expected to have type: 'a
$a is an existential type bound by the constructor Any.
It is only known in the scope of the pattern that matches Any.
Fixes: #9069
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Claude-Session: https://claude.ai/code/session_01Kr4cjoUi2f5VpMvE6wT9bo
Signed-off-by: Christoph Knittel <ck@cca.io>
Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>
The records skill asked for a block for each object a commit changes in what the compiler does, and a record of #9081 met it with the diagnostic alone, leaving the attribute the type checker adds to the synthesized match in prose. A record now shows the representation, rule, transformation or decision that changes, at its own level, and then its consequences; a change the prose names is shown in a block, a change no form prints is shown as a schematic, and a script or review fix that changes behaviour gets blocks. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Signed-off-by: Cristiano Calcagno <cristianoc@users.noreply.github.com>
6a7f2a6 to
232ccf2
Compare
cristianoc
left a comment
There was a problem hiding this comment.
This is Claude, writing on behalf of @cristianoc, who had a little time to look at this rather than rubber-stamp it.
The fix is right. What we changed is the record: the Semantic Diff showed only the effect (the new diagnostic), while the change itself is in the typed tree. The match synthesized for a GADT let now carries #let_gadt_pattern, and call_context maps that attribute to function-style diagnostics. Diffing bsc -dtypedtree before and after the commit shows exactly that attribute and nothing else.
Two commits are pushed to this branch:
- The fix commit is reworded, with its tree unchanged. Its record now has a Typedtree block (the match gaining the attribute), a Decision block (how
call_contextpicks the context for each kind of match) and then the Diagnostic block. - Records show the changed operation before its consequences updates
.agents/skills/records/SKILL.md. The old rule ("one object block for each object it changes") was met by a record of effects alone, so this is a gap in the skill rather than a slip by the author. A record now shows the representation, rule, transformation or decision that changes, at its own level, and then its consequences. A change that the prose names also gets a block, and a change that no form prints gets a schematic. Codex (gpt-6-astra) gave a second opinion on the wording.
Approving.
🤖 Generated with Claude Code
|
Claude again, for @cristianoc: the representation question this PR runs into, where the typed tree records a GADT 🤖 Generated with Claude Code |
Fixes #9069. Stacked on #9080, whose message appears in this fixture.
A
letdestructuring a GADT constructor is typed as a one-case match, so a type error in the rest of the block said "But this switch is expected to return" and added the hint about switch branches. The synthesized match is now marked like the one for optional argument defaults and gets function-style diagnostics.New fixture:
gadt_existential_let.🤖 Generated with Claude Code
https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3