Repository navigation
Refuse proven-disjoint kernel types at match-arm joins - #10374
Merged
Merged
Conversation
`fn f(x: Shape) -> Int { match x { A { n } => n, B { s } => s } }` with `s: String` is
Accepted, and executes: forcing the B arm returns the string where the signature says an
Int cannot fail to be.
What makes this a floor defect rather than a missing feature is that the SAME mismatch in
a plain body is refused, located:
type mismatch: expected 'Primitive(Int)', got 'Primitive(String)'
So the wall exists and holds. Match-arm results are simply not routed through it, and one
construct walks past a check the language already performs everywhere else. DESIGN 4b names
"values inhabit declared types" as part of the ordinary compiler floor, so this is a
below-baseline regression, and the failure is silent, which 5 puts outside the ladder
rather than low on it.
Found from the other end: a review of gunbc-private #35 flagged `conflicting_assessment_count`
declaring `-> Int` and returning `k1(...)`, a String, in one arm — a copy-paste from the key
projection beside it. That instance is a private defect and is fixed there. The class is this
one and it is public.
It survived both review and CI because the malformed arm was unreachable from its only caller,
so every executing control passed. An unreachable arm is exactly where this hides: reachable
ones are caught by their values, and the one mechanism that should not have needed execution
to see it did not look.
Ceiling is structurally guaranteed and the trigger is a wall NOW, not after grounding: the arm
result and the declared return type are both modeled, and the plain-body path already performs
this exact check. This commit files the class and its repro; it does not yet land the wall.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
…ducts I filed this class saying match arms "are simply not routed through" the return-type check. That is refuted by the source. `infer_expr`'s `ExprMatch` case computes `arm_join_diags` from `match_arm_join_diagnostics` for every arm — the join runs. It refuses on exactly one relation, `match_arm_types_are_disjoint_coproducts`. So it catches arms yielding disjoint declared coproducts and is silent on kernel scalars. `Int` versus `String` is not a disjoint coproduct, nothing fires, the match's inferred `result_type` stays the unified type taken from the conforming arm, and the declared-return conformance wall downstream compares against that and passes. The corrected diagnosis is worse than the original, which is why it is worth the amend. A missing check ranks for building. A check that exists, executes on every arm, and is scoped narrower than its name claims gets cited as coverage — 4b's rung inflation — and that is precisely how this survived review and CI. It also changes the repair: widen the join relation to the ground-kernel-scalar discipline the declared-return conformance path already uses. Do not add a second join beside it, which would be two authorities answering one question. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
gunbai-bot
Bot
changed the title
added 7 commits
September 4, 2026 10:58
# Conflicts: # docs/design-failure-modes.md
# Conflicts: # docs/design-failure-modes.md # src/v1/stage0/src/v1_compiler_infer.rs
6 tasks
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.
Summary
Widen the existing match-arm join wall from distinct declared coproducts to the ground-type discipline already used by declared-return conformance. This prevents a conforming first arm from hiding a later
Stringarm in a function declared-> Int, and likewise preventsList<Int>from hiding aList<String>arm, while preserving optional, diverging, and same-type controls.The mechanism is representative loss:
prefer_specific_typeselects the conforming arm, so downstream declared-return conformance compares only the winning type; the repair judges every non-diverging arm before that loss. The finding is consolidated into the existingjoin_answers_with_one_arm_others_unjudgedrecurring-failure authority.Test plan
claim_executor --required-regen --source-root dag --source-root src/v2: fixed-point green, 156/156/156.gunbc run ... --function ... --claim-run: 2 attempted, 2 passed.gunbc run ... --function ... --claim-run: 2 attempted, 2 passed.