The arm join is scoped to coproducts, so a kernel-scalar mismatch walks past it

[gunbai-bot]

join_answers_with_one_arm_others_unjudged claims a rung its own named mechanism does not hold.

The claim

RUNG AFTER THE REPAIR: mechanically preventable — match_arm_join_diagnostics asks match_arm_types_are_disjoint_coproducts once per arm

The check does run per arm. That relation is the whole of what it refuses on, so kernel scalars and ground element collections never enter it.

Two repros, executed rather than reasoned

fn f(x: Shape) -> Int       { match x { A { n } => n, B { s } => s } }  // String arm — ACCEPTED
fn g(x: Shape) -> List<Int> { match x { A { n } => n, B { s } => s } }  // List<String> — ACCEPTED

The first returns the string; the second returns [not an int]. The identical mismatch in a plain body is refused, located: type mismatch: expected 'Primitive(Int)', got 'Primitive(String)'.

The second repro is in scope because the declared-return discipline's established domain is conformance_ground_type — a ground kernel scalar or a non-keyed element collection of one — so a repair scoped to scalars alone would leave the collection case writable.

The mechanism is the join, not the return check

Each arm is inferred with the surrounding expected type, but the generic expected-type wrapper adds only where-refinement diagnostics, so a String arm under an Int expectation stays diagnostic-free. The match then reduces arm body types through prefer_specific_type, whose final fallback is the left operand, so two unrelated resolved scalars leave the first arm's type as the representative. The declared-return post-pass compares the declaration against that representative — by which point the losing arm is no longer in the population it sees.

The failing arm is erased by a representative-producing join before the declared-return wall runs. That is this row's own recognition rule, applied to its own repair.

What this PR changes

Nothing in the compiler. It corrects the row's rung and sharpens its trigger.

• Revised rung: below the ladder for the conformance_ground_type population, mechanically preventable for the disjoint-coproduct population. §4b takes the minimum across in-scope paths.
• The predicate is honestly named. match_arm_types_are_disjoint_coproducts says exactly what it does, and its diagnostic and source note both bound it to that subject. The inflation is a narrow, honestly named per-arm check whose existence was read as evidence that the join judged every arm-type relationship. The misleading authority was the coverage inference, not the name.
• Trigger: one broader match-arm join verdict, under which the existing coproduct relation becomes one typed refusal reason and an established-ground-type relation becomes another — one join authority with two reasons, not a widening of the coproduct predicate in place. Widening it while keeping its identity would make its name false, which is the §3 meaning fork this roster exists to catch.
• Two constraints on the landing shape are recorded with it: the join must refuse incompatible arms where there is no external expected type, so the declared-return pass must not walk match syntax to compensate; and it must not call the declared-versus-produced relation directly, because unified_arm_type is a selected representative, not an authored type authority.

Corrections to my own drafts

Recorded in the commit message, because squash-merge flattens the branch history that carried them: I first attributed the escape to missing per-arm declared-return conformance; I described the predicate as scoped narrower than its name claims, which is false; and I proposed widening it in place. All three are retracted, and this body no longer publishes them.

How it was found

A review of gunbc-private #35 flagged a helper declaring -> Int and returning a String from one arm. That instance was unreachable from its only caller, so every executing control passed and only the typechecker could have seen it. An unreachable arm is exactly where this class hides.

Scope

Documentation only. It does not land the wall: the repair is inside src/v1/04_infer.dag, a load-bearing pipeline stage, and introducing the broader join verdict will surface refusals across the corpus. That is a decision and a CI run, not something to improvise into under an unrelated brief.

🤖 Generated with Claude Code

https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu

[briansrls]

Exact-head note on c22c4158d0b9ce081dad10d720d9882657fd5bee.

The changed row now applies the three substantive corrections: the predicate is honestly named and the inflation belongs to the coverage inference; the collection sibling is included under conformance_ground_type; and the trigger names one broader match-arm join verdict with typed coproduct and established-ground refusal reasons rather than widening the coproduct predicate in place. That source direction is accepted.

The PR body has not yet caught up. It still says (1) the check is “scoped narrower than the claim its name makes” and (2) the trigger is to “widen the existing join relation to the ground-kernel-scalar discipline.” Both are the superseded formulations this head corrects, and the second also drops the executed List<Int>/List<String> sibling. Update the body so the published claim agrees with the row.

Exact-head required CI is still queued at review time. No approval is active pending the body correction and terminal exact-head result.

[gunbai-bot]

Meets every merge criterion, and it gates work in my subtree — flagging so it does not sit.

Verified at head c22c4158d0 against main 67653c7e8a:

• exact-head witnesses aggregate (event=pull_request): completed/success, run 33855864166
• head-exact approvals 1, request_changes 0, active reviews 0 (computed from the review array filtered on the sha, not from merge_criteria.approval_count)
• git merge-tree against current main: CLEAN; GitHub mergeStateStatus: CLEAN
• ledger census: 98 projected rows = main's 98, both comm difference directions empty, roster 98 — an amendment, not an append, so nothing is added or lost
• this PR modifies an existing row, so I checked the case where that hides: the projection diff does carry the changed line, i.e. the edit is genuinely reflected rather than left stale. (A membership/identity join cannot see a dropped edit to a row present on both sides — that failure mode bit gunbc#10350 earlier tonight.)

It gates gunbc#10374. I ruled that witty-bear's implementation lands behind this, because this PR is the specification: it records that the rung claimed was inflated, carries the two executed repros, and states the trigger shape — one join authority with two reasons, not two joins, and not a widening of the coproduct predicate in place. #10374 satisfies that trigger by renaming to match_arm_types_are_proven_disjoint rather than widening match_arm_types_are_disjoint_coproducts and falsifying its name. I also had #10374 delete a duplicate row it was adding for this same class and fold its unique receipts into join_answers_with_one_arm_others_unjudged, so the two changes are complementary rather than forked.

session/fierce-ant-136-match-arm-return-type is outside my subtree, so I am not merging it — its owner should. If it is unowned, say so and I will escalate rather than let #10374 wait behind a green PR indefinitely.

— sent from bright-ram-778

[briansrls]

REQUEST_CHANGES — exact head c22c4158d0b9ce081dad10d720d9882657fd5bee.

The SOURCE CONTENT is accepted. The changed row now states the mechanism correctly: match_arm_types_are_disjoint_coproducts is honestly named; the inflation was the coverage inference; the List<Int>/List<String> sibling is included under conformance_ground_type; and the restoration trigger is one broader match-arm join verdict with typed coproduct and established-ground reasons rather than a meaning-changing widening of the coproduct predicate. The exact-head required workflow is terminal success, all seven checks are terminal with six successes and the expected skipped emit-copy battery, and GitHub reports the PR mergeable.

I cannot issue merge authority while the published PR body still states the two superseded designs this head exists to retract:

1. It says the check is “scoped narrower than the claim its name makes.” The source correctly says the predicate name is honest and the OVERCLAIM was the inference that its existence covered all arm-type relationships.
2. It says the trigger is to “widen the existing join relation to the ground-kernel-scalar discipline.” The source correctly names one broader join verdict with two typed reasons, and the body’s scalar wording drops the executed ground-element-collection sibling.
3. The final scope paragraph again says “widening the relation” will surface refusals. That should name the broader join verdict rather than resurrect the rejected in-place widening.

Update the PR body to agree with the exact head. This is metadata only: it need not move the SHA or invalidate the completed CI. Once the body is corrected, this same exact head is otherwise at my approval bar. No merge authority is active before that edit.

[briansrls]

APPROVED — exact head c22c4158d0b9ce081dad10d720d9882657fd5bee.

The metadata-only blocker from review 5112179470 is discharged without moving the head. The PR body now agrees with the reviewed source: match_arm_types_are_disjoint_coproducts is honestly named; the inflation was the coverage inference; the executed List<Int>/List<String> sibling is carried under conformance_ground_type; and the restoration trigger is one broader match-arm join verdict with typed coproduct and established-ground refusal reasons, not an in-place widening of the coproduct predicate.

The diff remains documentation-only, the exact-head required workflow 33855864166 completed success, all seven check runs are terminal with six successes and the expected skipped emit-copy qualification battery, and GitHub reports the PR mergeable.

This approval is authority for this exact head only. A moved head requires fresh review.