infer: a diverging match arm contributes nothing to the match's join

[gunbai-bot]

The defect: a fabricated refusal against correct .dag

v1.compiler.infer builds a match expression's type by folding every arm's body type with
prefer_specific_type. An arm whose body is a return has the function's return type as its
body type. So a let bound from such a match is typed as the union of the binding and the
function's return coproduct, and passing that binding to a parameter declared with the binding's
own type refuses:

fn f(xs: List<Cell>) -> Res {
  let cell = match cell_of(xs: xs) {
    Absent => return Unknown { why: 0 }
    Present { value } => value
  }
  Ok { cell: Cell { n: takes_cell(cell: cell) } }
}
error: value does not inhabit its declared type at the direct call argument for parameter 'cell':
       declared 'Product(Cell)', produced 'Coproduct(Res)'

That is DESIGN §5's fabricated plausible output with the sign flipped — not a wrong answer that
looks right, but a wrong refusal that looks principled. And it sits on the ordinary compiler floor
§4b says must be held before any differentiating claim: values inhabit their declared types.

The idiom is load-bearing, not a corner. => return appears across merge_admission_current_context,
secret_access_ensure, ci_heal_dispatch, bmc_read_telemetry, bmc_onboard, roadmap_forecast,
srv3_seeded_install_media and srv3_os_install_actuate — spark, srv3, bmc, ci_heal and roadmap.

The fix: one line of authority

src/v1/04_infer.dag — arm_body_types excludes arms whose body diverges, via a new
arm_body_diverges that sees both a bare return and a block whose terminal statement is one.

Two things checked rather than assumed:

• If every arm diverges the list is empty and the existing Absent => scrut_rt arm stands, so
  no type is invented and no new arm is introduced.
• The re-inference pass below it re-runs only arms whose body_type is not fully resolved. A
  diverging arm's type is resolved, so it is never re-checked against the unified type and no
  second edit is needed there.

Measured, on a compiler built from this change

probe	before	after
the 22-line reproduction above	refuses at resolve	resolves
dag/gunbc/roadmap/roadmap_forecast.dag as it stands on main, not edited here	three inhabitance refusals	PASS witness_empty_calibration_cell_refuses
corpus parse	—	4493 file(s) parse-clean

Those three refusals are exactly what required-witnesses-floor refused on run 33556389758. They
clear here without editing roadmap_forecast.dag at all, which is the discriminating evidence
that the checker was the cause rather than the corpus. An earlier attempt migrated all three call
sites and the errors survived verbatim — that hypothesis is refuted by execution, and it is why this
PR exists instead of a migration.

The evidence stays enrolled (§4b(4))

dag/test/claim/diverging_match_arm_join_witness_test.dag carries the reproduction verbatim, now
12 witnesses, all green. It is its own regression control in the strong sense: if the join ever
re-admits a diverging arm, the module stops RESOLVING, so its witnesses go red at resolve rather
than at assertion. Beyond the original four it covers a let-terminal return, an all-diverging
match in argument position (the discriminating RED for blocker 1), an all-diverging match taking the
expected type rather than the arm payloads, and an all-diverging match in an unconstrained let
fabricating no type.

Divergence is an explicit fact, not an absent name (review 5085499375, D1)

The first repair let divergence survive as a nameless node. That conflated two different states:
an expression that produces NO value, and a type the walk COULD NOT RESOLVE. The only feature
distinguishing the sentinel was its empty name, so every consumer that declines on a missing name
declined on both — and the second is a state that must still be judged. That is silencing, and it
was structural rather than hypothetical.

Divergence now has a carrier:

• InferredNode gains Divergent — a fourth answer to what inference knows about a node,
  deliberately not a shape of Resolved.
• TypeResolutionVerdict gains DivergentExpression, and type_is_divergent(n) is the
  reader consumers match on. is_fully_resolved still answers false, but by its own arm rather
  than by sharing the unresolved path.
• divergent_type() moves to 00_core beside InferredNode: resolution as well as inference
  must now construct and recognize it, and leaving it in 04_infer would have forced 04_resolve
  to mint a second nameless node for the same concept.

Making the fact structural is what produced the census. Adding the variant refused 10 sites, each
answered deliberately rather than defaulted:

site	arm	why
inferred_to_node	none	no node to hand back
is_compiler_error	false	divergence is a fact, not a failure
resolve_optional_node	carry divergent_type()	unit_type would fabricate a type for unreachable code; a diagnostic would refuse a program that is not wrong
inferred_to_outputs	[]	no value means no output fields
05_emit_rust wire-contract ×2	rust_serde_error_policy	a diverging initializer names no alias — refuse, do not widen
serialize_inferred_node_ref	Divergent kind	the serialized form must not lose the fact
cli_run initializer	typed error	a diverging initializer names no declared type
inferred_fingerprint, occurrence_allocator_after_inferred_node	see below	repaired at the .dag authority

The mirror IS a measured fixed point now

The running compiler is the Rust mirror, not the .dag. Every mirror in this PR is installed from
target/stage0-regen-candidate, never hand-shaped — the two hand-shapes earlier in this branch both
missed something the emitter derives. Measured, not claimed:

12/12 witnesses PASS
first_generation_equal=true  declared_divergent=1 [main.rs]
fixed_point_equal=true  referenced_first_generation_equal=true
4493 file(s) parse-clean   cargo fmt --all --check clean

Two findings this PR does NOT fix, stated because they were measured here

1. The join already answers with the FIRST arm. Blocker 3 asked for a control proving a later
non-diverging contributor is necessary to the join. Seven fixture shapes and two independent mutants
(keep-first, and a purpose-built contamination mutant that makes the divergent sentinel win) all
failed to discriminate. The narrower shape — the later contributor alone satisfies the formal —
found the reason, and it is an ordered pair:

arms, in order	verdict
FResA then FOthA (satisfying arm first)	accepted — and FOthA really is passed to a FRes formal
FOthA then FResA (satisfying arm later)	refused: declared 'Coproduct(FRes)', produced 'Coproduct(FOth)'

The verdict flips with arm order, so prefer_specific_type tie-breaks to the first arm for
disjoint coproducts. That is why keep-first was unobservable: the compiler is already behaving like
the mutant at this seam. One of those two rows is wrong and it is the accepted one — a floor
violation (values inhabit declared types) with a corpus-wide blast radius. It is a different defect
in the same function and folding it in would make a bounded PR unbounded, so it gets its own subject.

2. The .dag exhaustiveness checker is blind through nested patterns. Adding the InferredNode
variant, the checker flagged all 7 flat matches and missed both matches over
Optional<InferredNode> written as Present { value: Resolved { .. } } — rustc caught those.
Accepted .dag source emitted Rust that does not compile: accepted_source_emits_uncompilable_target.
Repaired here at the .dag authority so the arms come from the emitter, but the checker gap is the
finding, not the patch, and it is filed separately.

What is measured and what is not

D2's propagation control — a divergence born in an unconstrained let feeding an outer selector —
is not enrolled, deliberately. It greens under its own purpose-built contamination mutant, and a
probe that is permanently green by construction carries no information and would later be cited as
coverage (§4b). It is recorded here as a measurement with a named enrolment trigger: it becomes
discriminating the moment the join stops answering with the first arm, i.e. when finding 1 is fixed.

So, in the two claims kept apart: this PR establishes that diverging arms contribute no produced
value to the join, and that the divergence fact survives independently of context, by execution.
It does not establish that the all-arms map is exercised at any judging seam — no authorable
input distinguishes it today, and finding 1 says why.

[gunbai-bot]

One clarification on the approving review's wording, because the distinction is load-bearing and I would rather narrow my own evidence than let it be read wider than it is.

Which part of this diff is a discriminating RED, and which part is not.

• Discriminating. The reproduction module itself. Before the fix, probe_cell could not be authored at all — the let bound from a match with a return arm refused with declared 'Product(ProbeCell)', produced 'Coproduct(ProbeResult)'. That is measured in both directions on binaries I built, and it stays enrolled in the strong form: if the join ever re-admits a diverging arm the module stops resolving, so its witnesses go red at resolve rather than at assertion.
• NOT discriminating, and now labelled as such at the witness. The two ExprLet cases added for review 58314. I rebuilt the pre-fix hand-walker and ran them against it: both pass on the old predicate too. { let why = 2 return X } puts the return as the block's last child with the let as a preceding sibling, so children |> last already reached it. I have no surface shape that produces an arm whose terminal is an ExprLet node.

So review 58314's objection stands on the ground it actually named — the predicate forked a traversal that v1.compiler.ownership fold_terminal_expr already owns — and routing through that fold is the repair. The ExprLet arm is covered because the canonical fold owns it, not because I demonstrated a live red. The two witnesses are kept as behaviour-preservation controls.

If anyone knows a .dag surface form whose match-arm terminal really is an ExprLet node, I would like it: that would turn a preservation control into a discriminating one.

Regen, run locally as a three-step chain rather than stopping at the install:

--required-regen              first_generation_equal=true planned=149 executed=149
                              adjudicated=149 declared_divergent=1 [main.rs]
--required-regen-fixed-point  fixed_point_equal=true referenced_first_generation_equal=true

The fixed-point pass is not ceremony here: pass 1 runs a binary built from the seed it emits, and this change alters the inference the emitter itself runs on — precisely the case where one pass can self-verify for the wrong reason.

The mirror is the emitter's own bytes, installed from target/stage0-regen-candidate, not hand-shaped. Worth recording why: my hand-written arm_body_diverges was byte-identical to the emitted one, and the drift was a single line — pub use crate::v1_compiler_ownership::fold_terminal_expr;, a re-export the emitter derives from the import structure. Two hand-shapes, two misses.

— sent from still-swift-363

[briansrls]

REQUEST_CHANGES at exact head 83f7087bc423760022073d2c90e8f11a9eb1468a.

The central causal finding is accepted: a return arm does not produce a value for the enclosing match, the three roadmap_forecast refusals are checker-caused rather than corpus-caused, and clearing them without editing that corpus file is the discriminating evidence. Routing terminal discovery through the existing fold and installing emitted mirror bytes are also the right directions.

Three blockers remain.

1. Filtering makes the old no-arms fallback reachable for an all-diverging match, and that fallback fabricates the scrutinee type. Before this change, arm_body_types was empty only when the match had no arms. After the filter, a match whose every arm returns also reaches Absent => scrut_rt; the emitted code then assigns result_type = unified_arm_type. That is not “no type invented”: it types an expression that produces no value as the type of the value it consumes.

A direct counterexample is a function whose terminal expression is a match and both arms return the function result. Before the filter both body types join as the function return type. After it, the match becomes the scrutinee type and can fabricate a function-return mismatch. Required repair: represent divergence/bottom explicitly, or conservatively preserve the previous all-arm join when the original arm list is nonempty but the non-diverging list is empty. Keep scrut_rt only for the genuinely empty-arm case. Add an executing all-arms-return fixture.

2. The re-inference claim is measured on the current specimens, not structural. The second pass still re-infers every arm whose original body_type is not fully resolved against unified_arm_type; it does not exclude arms already proven divergent. A diverging arm in a generic or otherwise under-resolved function can therefore re-enter through this pass and be judged against the surviving match type. Either exclude diverging arms from that expected-type re-inference, or supply a discriminating fixture proving a diverging arm's body type is necessarily fully resolved for the entire accepted language. The present examples establish only the concrete-return case.

3. The claimed ordinary-join positive control does not discriminate. probe_no_divergence returns ProbeCell from both arms. A mutation that retains only the first non-diverging arm before map(ar => ar.body_type) leaves that witness, the original one-survivor reproductions, and both behavior-preservation controls green. Add a mutation-checked control in which omitting a real non-diverging arm changes the joined type and makes the downstream program refuse; use paired orderings if necessary because prefer_specific_type is selective/left-biased.

The exact-head CI cycle started after composing with c4e498652fcf, but these are source/evidence blockers independent of that run's eventual result.

[briansrls]

LANDING-MECHANISM ADDENDUM to review 5083893018: this PR changes an authority and its committed generated mirror, so repairing the three source/evidence blockers and receiving a later technical approval will not authorize an ordinary GitHub merge while the projection-composition mechanism remains unresolved. Its tested base was c4e498652fcf5522200a118079c50586349b38c2; main has already advanced to 7810e68b3ea12d29ad811a2f2a0e1023f0dcd241. A merge-group candidate or atomic expected-base/exact-tree actuation must still compose and test the actual landing tree.

[gunbai-bot]

Following up on review 5083893018 with results rather than a claim. All three blockers are repaired at 849b9857103; none of the three has a discriminating RED, and I would rather say that than let nine green witnesses imply one.

What is repaired

• B1 — arm_body_types falls back to the full arm join when non-diverging arms are empty; scrut_rt survives only for the genuinely zero-arm match.
• B2 — the re-inference pass returns original for a diverging arm, so divergence governs both stages. To be precise about what that is worth: your objection was a universal claim (every accepted diverging-arm shape resolves early), and I have not refuted it — I removed the dependency on it. Unnecessary, not proven.
• B3 — paired orderings whose arms contribute differently.

Two mutants, both green — the controls certify without discriminating

mutant	binary hash	result
pre-B1 unconditional filter	8c7e053c1bbc	2/2 PASS
keep first non-diverging arm (.take(1))	cd33904dbf9a	2/2 PASS

Each rebuild confirmed by a changed binary hash, so the controls ran. My replacements therefore have the same defect you identified in the originals.

Two failed B1 instantiations, each with a named reason

1. ProbeFlag scrutinee, terminal-expression position, disjoint types — authorable, does not discriminate:

fn all_arms_diverge(f: ProbeFlag) -> ProbeResult {
  match f { ProbeYes => return ProbeUnknown { why: 10 }   ProbeNo => return ProbeUnknown { why: 11 } }
}

The match is the whole body (no binding) and ProbeFlag is disjoint from ProbeResult, so under the mutant it should type as ProbeFlag against a declared ProbeResult and refuse. It is accepted. That suggests the return-position check is satisfied by the return statements and never consults the terminal match's own type when every arm diverges.

2. Bool scrutinee — not authorable. match b { true => … false => … } does not parse as patterns; the file stops resolving and the diagnostic surfaces ~90 lines away as source annotation names no subject at line 3, the untouched header. Reverting the fixture restores resolution.

The question

Is there a .dag shape where an all-diverging match's own type is actually consumed? If every path leaves through a return, the value never reaches a consumer, and the enclosing declaration is satisfied by the returns — in which case the invalid state may be unobservable from source and B1 is correctness with no authorable RED (a §4b ceiling question rather than a missing test). I am not asserting that: "I could not find a red" is not "no red exists", and per §4b the fixture boundary is where this should be tested, since a compiler's regression probes are allowed to be invalid programs.

Same question for B3: under the keep-first mutant both orderings are accepted, so no arrangement of Absent / Present { value: 5 } discriminates. Arms whose join is genuinely order-dependent would be needed, and I do not know a pair that is.

Both fixtures are labelled at the witness as behaviour controls, with the mutant hashes recorded, so neither can be cited as proof of a wall.

— sent from still-swift-363

[gunbai-bot]

Blocker 1's RED is unauthorable today, and I can now name why rather than assert it. Pushed at 92af40e8e63.

v1.compiler.infer DeclaredTypePosition declares twelve positions. DeclaredTypeObligation is constructed at two sites, carrying PositionDirectCallArgument and PositionListElement. PositionDeclaredReturn occurs three times in that module — the comment listing unwired positions, the variant declaration, and a display string — and has no producer.

So the declared-return seam is not checked. My terminal-expression fixture was correct in shape (the match is the whole function body) and disjoint in types (ProbeFlag scrutinee against a declared ProbeResult), and it was accepted under the mutant because nothing consults that position, whatever the match is computed to type as. A second instantiation with a Bool scrutinee is not authorable at all — Bool literals do not parse as patterns.

That makes B1 a §4b row rather than an argument, and it is now written at the witness:

invalid state	a match typed as the value it consumes (the scrutinee) rather than the value it produces, when every arm diverges
rung found at	unguarded on the source-acceptance path — no obligation producer observes the declared-return position
ceiling	mechanically preventable once that position is wired; the state is decidable, so this is a wall after grounding
next-rung trigger	the capability, not an artifact: an obligation producer for PositionDeclaredReturn, sufficient to make a terminal expression's inferred type a checked contract against the declaration

Ten of the twelve positions are unwired; this is one of them, and no fixture in this file can retire the row — which is why I stopped at two instantiations rather than guessing a third.

If you think a different position does observe this state, naming it would settle it — my reading is that the answer requires wiring first.

B3 stands as reported: under the keep-first mutant both orderings are accepted, so no arrangement of Absent / Present { value: 5 } discriminates; it needs arms whose join is genuinely order-dependent. B2 is unnecessary rather than proven — divergence now governs both stages by construction, which removes the dependency on the universal claim instead of refuting it.

— sent from still-swift-363

[gunbai-bot]

Retracting the §4b row from my previous comment: blocker 1 DOES have a discriminating RED. Pushed at 037ac9f70f8.

I said the RED was unauthorable because PositionDeclaredReturn has no producer. The premise is true; the conclusion was wrong. You do not need the return seam if you can reach a wired one.

direct_call_argument_inhabitance_diags builds its obligation with produced: resolved_type(n: arg_value(n: ta)) — the resolved type of the argument expression — and PositionDirectCallArgument is one of the two wired positions. So an all-diverging match in argument position has its own computed type compared, where the same match in terminal position is consulted by nothing.

Measured in both directions, which neither previous instantiation could do:

FIXED    binary 01a53030eafa   PASS an_all_diverging_match_in_argument_position_types_as_the_arms
MUTANT-1 binary 8c7e053c1bbc   resolve REFUSED:
  value does not inhabit its declared type at the direct call argument for parameter 'r':
  declared 'Coproduct(ProbeResult)', produced 'Coproduct(ProbeFlag)'

produced 'Coproduct(ProbeFlag)' is your defect in your own terms — the match typed as the value it consumes rather than the value it produces. Each binary rebuilt and confirmed by hash change.

One constraint the fixture had to respect, and it is the defect protecting itself: the scrutinee must not be Optional. declared_type_inhabitance bails to InhabitanceUndecidable { UndecidableOptionalCarrier } whenever either side carries CardOptional, which swallows the comparison before it happens. A plain coproduct scrutinee walks past it. (That bail, and a second one at the same seam that returns a bare false, are the subject of separate work — they are one wall with two guards, and repairing either alone would certify a gap that the other still admits.)

What stands and what does not:

• The two terminal-position witnesses remain, still labelled as behaviour controls that do not discriminate.
• The PositionDeclaredReturn finding remains as the explanation for why they cannot — 2 of 12 positions wired — but is no longer a ceiling claim about the class.
• B3 is unchanged: under the keep-first mutant both orderings are accepted, so no arrangement of Absent / Present { value: 5 } discriminates.
• B2 is unchanged: unnecessary rather than proven.

10/10 witnesses pass; 4493 file(s) parse-clean. No .dag authority changed in this commit, so the mirror is untouched.

— sent from still-swift-363

[briansrls]

REQUEST_CHANGES on exact head 037ac9f70f85c3ca772f864a0cf46c57a32960d5.

Two of review 5083893018's three bars are now closed.

B1 CLOSED. The new an_all_diverging_match_in_argument_position_types_as_the_arms specimen is the missing discriminator. It observes the match expression itself at the wired PositionDirectCallArgument seam and records the expected two-direction result: PASS on the repair, resolve refusal under unconditional filtering (ProbeResult formal versus ProbeFlag produced). This also correctly narrows the real PositionDeclaredReturn gap to terminal position instead of widening it to the whole all-diverging-match class.

B2 CLOSED. The second pass now returns the original result for every arm classified as diverging before considering unresolved-body re-inference. The same divergence judgment governs both stages.

B3 REMAINS OPEN. The committed witness says the keep-first mutant cd33904dbf9a still passes. Therefore it does not meet the prior bar: a control that remains green when all later ordinary contributors are discarded is not evidence that ordinary-arm joining was retained.

The present pair is masked by contextual typing: each match is the terminal expression of a function declared -> Optional<Int>, and ExprMatch passes that enclosing expected type into both arms before the join. Move the join into an unannotated let and observe its inferred payload before any expected type can replace it. One bounded shape is:

fn ordinary_join_retains_later_payload(f: ProbeFlag) -> Int {
  let joined = match f {
    ProbeYes => Absent
    ProbeNo => Present { value: ProbeCell { n: 5 } }
  }
  match joined {
    Present { value } => value.n
    Absent => 0
  }
}

ExprLet gives that initializer expected: none; the outer match then binds value from the initializer's computed optional element type, and value.n reads it through field access with an uncontextualized base. On the correct join the later Present<ProbeCell> supplies the specific element type. Under keep-first, the Absent arm's nonspecific/unit payload remains and value.n must refuse. Mutation-run this or an equivalent actual-use shape and retain the exact red receipt.

The nine green witnesses and exact-head CI do not close this finding while the named mutant remains green. Re-review bar: one executing ordinary-arm retention fixture that is green on the repaired compiler and red under cd33904dbf9a, with the current honest behavior controls retained or relabeled as desired.

Landing is independently held. This review grants no ordinary-merge authority. Even after B3 closes and source is accepted, this authority+generated-mirror PR must land only through the commissioned merge queue or an operator-authorized atomic expected-base/tree-CAS route. A GitHub APPROVE, when source is ready, will not supersede that mechanism requirement.

[gunbai-bot]

review 58384 is correct and is now fixed, pushed at 6850ba93e5a. It also caught an over-correction that review 5084758663 had approved, so the executed counterexample decided this rather than the tally.

Confirmed by execution

The previous fallback restored the arms' body types when every arm diverged. Those are return payload types, and an all-diverging match produces no value, so they are not the match's type either:

error: value does not inhabit its declared type at the direct call argument for
parameter 'r': declared 'Coproduct(B3Res)', produced 'Coproduct(B3Other)'

on an argument that never returns — a fabricated refusal, the §5 sign-flip this PR exists to remove, relocated from the scrutinee to the return payload.

The rule is now contextual (one of the two repairs you allow): when every arm diverges the match takes the expected type, since a value that is never produced inhabits whatever the context requires. scrut_rt survives only for a match with no arms at all. The probe above flips from refused to accepted.

Why my first run of your counterexample appeared to refute it

I ran your shape with an Int formal and it was accepted, which reads as "the objection is wrong." The control says otherwise: b3_take_int(x: B3Ok { n: 1 }) — a plainly wrong argument, no match involved — is also accepted, and the function declared -> Int then returned a B3Res at runtime. The Int formal is not judged at that seam, so the probe was blind. Re-running with a coproduct formal (which the earlier ProbeFlag/ProbeResult measurement proved is checked) reproduced your refusal immediately.

That Int-formal hole is a separate live silent-wrongness defect, not introduced by this PR and not fixed in it; it is reported upward rather than widened into this subject.

Evidence

• 11/11 witnesses pass on binary 16a3739a7352, rebuilt and hashed in the same command as the run. An earlier run of this same set reported two refusals off a stale mutant binary, so the rebuild is no longer trusted to memory.
• B1's discriminating RED survives: under mutant 8c7e053c1bbc it still refuses with declared 'Coproduct(ProbeResult)', produced 'Coproduct(ProbeFlag)'.
• regen first_generation_equal=true declared_divergent=1 [main.rs], fixed_point_equal=true, 4493 file(s) parse-clean.

The new witness is three-way distinct on purpose — formal ProbeResult, arms return ProbeOther, scrutinee ProbeFlag — so it reds if the match is typed as the scrutinee (the original defect) or as the arm payloads (this over-correction).

B3 remains open and is unchanged: under the keep-first mutant both orderings of Absent / Present { value: 5 } are accepted, so those arms cannot discriminate. I am measuring candidate arm pairs under both binaries before authoring another control, rather than writing a fourth fixture on reasoning.

— sent from still-swift-363

[gunbai-bot]

review 58406 identified a real defect. Its attribution to this diff was wrong. Both halves are measured, and I want to state them together rather than lead with the one that favours me. Pushed at b45adfc83a3.

The case is INHERITED, with a receipt

origin/main built in its own worktree with its own target dir — binary 3b040239a0e2, and grep -c arm_body_diverges on main's mirror = 0, proving it is a compiler without this PR's predicate. Main refuses the same shape:

b4.dag:14:32: error: value does not inhabit its declared type at the direct call argument
for parameter 'r': declared 'Coproduct(B4Res)', produced 'Coproduct(B4Other)'

So an all-diverging match bound by an ordinary non-tail let, whose unreachable binding flows onward, is falsely refused on main. This PR neither introduces nor worsens it.

My first attempt at that control was invalid and nearly produced the opposite conclusion: I swapped only main's v1_compiler_infer.rs into my tree, it failed to compile (17 errors), no binary was produced, and the probe then ran against my repaired compiler and passed — which reads as "main accepts it, therefore I introduced the regression." The unchanged binary hash caught it.

Repaired here rather than declared

divergent_type() — a deliberately nameless node. A value that is never produced has no type to report, so consumers asking its name get "" and decline.

This is the first implementation that matches this PR's own title. The arm-join fallback and the expected-type fallback were both approximations of "a diverging arm contributes nothing to the join" that leak in contexts the sentence covers: the first fabricated the arms' return payloads, the second only worked where a contextual type existed — and an ordinary non-tail let passes expected: none, which is exactly the hole you found.

The silencing control, because "it declines" is one character from an absorbing fallback

A genuine inhabitance violation must still refuse in the presence of a divergent binding. Two arms, one file, binary 4fcbc484bbb7:

arm	body	result
baseline_violation	the violation, no divergence present	refuses — b5.dag:12:28
violation_beside_divergence	the same violation, sharing a body with an all-diverging match whose nameless-typed binding is consumed first	refuses — b5.dag:25:28

Both declared 'Coproduct(B5Res)', produced 'Coproduct(B5Other)'. The baseline refusing is what makes the second row evidence rather than an assurance. And the line between them — the divergent binding's own consumption — produced no diagnostic, which is the correct discrimination: it declines where there is no value to judge, and nowhere else. The line still stops for real errors.

Evidence: 12/12 witnesses pass; B1's discriminating RED still refuses under mutant 8c7e053c1bbc; regen first_generation_equal=true declared_divergent=1 [main.rs]; fixed_point_equal=true; 4493 file(s) parse-clean.

B3 remains the one open blocker and is unchanged: under the keep-first mutant both orderings of Absent / Present { value: 5 } are accepted, so those arms cannot discriminate. Measuring candidate pairs under both binaries before authoring another control.

— sent from still-swift-363

[briansrls]

REQUEST_CHANGES on exact head b45adfc83a3b6b507830948bed3c5f364b0ebf22.

This supersedes my B1 closure at 037ac9f70f85: the representation changed after that review, so the old closure cannot authorize the new design.

Attribution and scope

Codex review 58406 found a real all-diverging / expected: none false refusal. The isolated-main measurement is sufficient to correct the attribution: it is inherited, not introduced here. The failed first setup must be treated as NOT RUN; continuing to the probe after the build failed and the binary hash stayed unchanged would have inverted the result. Keep the setup-success/hash guard as part of every mutation receipt.

I also agree with repairing the inherited member here rather than filing a 4b row. The PR's semantic claim is that a diverging arm contributes no value to the join; the unconstrained-let case is inside that claim, and the repair capability is in hand.

D1 OPEN — a nameless resolved node is not a divergence/bottom model

The current divergent_type() carries no divergence identity. It is an ordinary synthetic Node with name: "" and inferred: none; the enclosing match then publishes it through Resolved { node: result_type }. At the wired obligation, declared_type_inhabitance does not recognize divergence. It recognizes only produced_name == "" and returns InhabitanceUndecidable { UndecidableProducedIdentityErased }.

Those are different facts:

• known: this expression produces no value because it diverges;
• unknown: a produced value exists but its type identity was erased.

Using the second verdict to admit the first is authority substitution. Empty name is already used by non-divergence states such as type-variable and error carriers, so absence of a name cannot be the identity of bottom. It also emits a counted undecidable judgment whose explanation says the produced identity is unrecoverable, which is false for this case: the compiler knows why there is no produced value.

The branch still loses divergence when expected is present as well: the all-diverging arm set becomes [expected_type]. That may supply a contextual type, but it does not preserve the independent flow fact review 58406 required.

Required repair: carry a typed Diverges / ProducesNoValue fact, or a canonical bottom identity, independently of optional contextual type. An exact divergence state may produce a named positive judgment such as InhabitsByDivergence, or suppress construction of a value-inhabitance obligation through a named no-value outcome. It must not route through UndecidableProducedIdentityErased, an empty spelling, or another generic unknown-state bail. Unknown/erased non-diverging types must retain their existing distinct disposition.

D2 OPEN — the current divergence predicate is not compositional, and the proposed adjacent control is insufficient

arm_body_diverges asks whether fold_terminal_expr(body).expr_data is ExprReturn. The canonical fold descends through ExprLet and ExprBlock only; for every other expression it returns the expression itself. Therefore an arm whose terminal expression is an all-diverging nested match is classified as an ordinary contributor.

That gives a direct anti-silencing counterexample:

1. an outer match's first arm is a nested match whose every arm returns;
2. its second arm produces Bad;
3. the outer result is consumed where Good is required.

The legitimate Bad -> Good refusal must remain in both outer-arm orderings. On the present design, the nested first arm contributes the nameless sentinel as an ordinary type; prefer_specific_type can retain that left value, and the later obligation declines as identity-erased instead of refusing the real Bad path.

The reported b5 sibling-statement pair is directionally useful, but it proves only that diagnostic chunks from separate statements are concatenated after a divergent binding. It does not make the divergent value and the genuine mismatch meet in the same type flow, and it is not enrolled in the exact-head witness file.

Re-review evidence for this bar:

• mixed outer match, nested-divergent first + incompatible ordinary arm second: located refusal;
• same pair reversed: the same located refusal;
• positive counterpart with a conforming ordinary arm, both orders: admitted;
• an explicit-tag-erasure or any nameless node == divergence mutant: RED;
• the controls committed to the witness, not only reported from a temporary probe.

A structural divergence carrier plus this one nested/alias composition is enough; I am not asking for a census of every downstream expression form. With the nameless proxy, however, no adjacent fixture can prove confinement because every consumer of node name/shape is part of the implicit protocol.

The original B2 re-entry repair remains accepted for arms that the classifier actually identifies: the second pass returns original before unresolved-body re-inference. The new carrier must preserve that result compositionally.

B3 OPEN — use a selector discriminator, not a synthesized-third-type premise

prefer_specific_type always returns either left or right; it does not synthesize a third joined type. Therefore there is no pair for which the join satisfies the formal while neither arm alone does. The right discriminator is:

• first contributor alone is insufficient;
• later contributor alone is sufficient;
• the full fold selects the later contributor;
• keep-first cd33904dbf9a retains the insufficient first one and goes red.

A more promising pair than Optional is the selector's explicit same_kind && left_is_unit_inner => right arm:

fn ordinary_join_retains_later_list_payload(f: ProbeFlag) -> Int {
  let xs = match f {
    ProbeYes => []
    ProbeNo => [ProbeCell { n: 5 }]
  }
  match first(xs) {
    Present { value } => value.n
    Absent => 0
  }
}

The unannotated initializer removes an expected result. The full fold should replace List<Unit> with List<ProbeCell>; keep-first should leave List<Unit>, and the downstream value.n should refuse. This observes the selected payload directly and avoids the separate Optional bail and the generic list-typed-value direct-call boundary. Execute it before relying on it; the bar remains repaired compiler GREEN and exact rebuilt cd33904dbf9a RED.

Current gate

old B1 mutant discriminator: still useful for the original scrutinee fabrication
new bottom/divergence representation: OPEN
nested anti-silencing/composition: OPEN
B2 direct second-pass re-entry: CLOSED
B3 ordinary contributor retention: OPEN

The in-progress exact-head CI cannot close these source/evidence findings.

Landing remains independently unchanged: this review grants no ordinary-merge authority. After source acceptance, #9964 still requires the commissioned merge queue or an operator-authorized atomic expected-base/exact-tree CAS.

[briansrls]

PR-BODY ADDENDUM on exact b45adfc83a3b6b507830948bed3c5f364b0ebf22.

The PR body is materially stale after the two redesigns and must be rewritten before source acceptance. It still says:

• all-diverging arms leave arm_body_types empty and reach the existing Absent => scrut_rt fallback;
• the second re-inference pass needs no edit;
• the evidence population is four witnesses.

The exact source now makes arm_body_types nonempty in every branch: a nonempty ordinary population maps to a nonempty list, while an empty population yields either [expected_type] or [divergent_type()]. Therefore the later Absent => scrut_rt arm is currently unreachable, including for a genuinely zero-arm match. The second-pass divergence exclusion is present, and the witness population is now twelve.

Do not preserve the old body as a history lesson. Replace it with the current claimed semantics, exact evidence dispositions, inherited-versus-introduced attribution, and the remaining bars. In particular, do not say scrut_rt "survives only for zero arms" unless source once again contains an explicit original-arm-count branch that makes that statement true.

[gunbai-bot]

Marked draft while I repair the merge. 6e6eb2a merged origin/main in — necessary because this branch was verified against a tree that predates #10045 ("Judge every match arm, not just the one the join answered with"), which touches the same join this PR changes, and #10006, which touches the same files. A green measured before those landed is evidence about a tree that will not exist after the squash.

The current red is expected and its cause is known: the generated stage0 mirrors are mid-repair. The merge conflicted in four of them, and they cannot be resolved — they are derived, so the only sound resolution is regeneration from the merged .dag authority. Neither parent's copy is valid on its own: main's v1_std_core.rs has no Divergent, mine has no declaration_provenance_of. Each wrong seed failed loudly at the build rather than compiling a hand-merged approximation into the seed, which is the outcome that would actually have been dangerous.

Regenerating with a compiler built from pristine main, then re-verifying — including the #10045 interaction specifically, which a compiling tree does not establish.

— sent from still-swift-363

[gunbai-bot]

Recording what review 58772's APPROVE covers, because it cannot cover the defect this branch is currently being repaired for — and I would rather say so than let the approval stand unqualified.

The review is fair on the diff's content: Divergent as a fourth InferredNode variant, threaded exhaustively, combine_resolution_verdicts enumerating all four arms without a wildcard. No disagreement.

What it cannot have covered is a defect that is invisible to reading. Merging current origin/main in surfaced this from the compiler, not from the diff:

call shape mismatch calling 'arm_body_diverges': no parameter named 'n' (declared: [body])

#10045 and this PR independently declared the same function in the same file. Git merged both cleanly — different regions, no textual conflict — leaving two declarations of arm_body_diverges and call sites binding inconsistently. Reviewing either side alone sees nothing wrong; only compiling the merged authority fails.

The convergence was not arbitrary, and it went against me:

• Mine hand-rolled the block-tail recursion, handling ExprBlock only.
• Judge every match arm, not just the one the join answered with #10045's delegates to ownership.fold_terminal_expr, which folds through ExprLet and ExprBlock.

So an arm shaped let x = ...; return y genuinely diverges and my predicate answered false — the fabricated refusal my own annotation warns against, in the code that annotation sits above. Re-inventing a walk the codebase already owned is the DESIGN §2 failure, and here it cost correctness as well. Theirs survives; my declaration is deleted, my call site rewired, and my rationale (which carries a measured receipt) moved onto the surviving declaration with a note recording why two met and which won.

The lesson I am taking, stated plainly: this PR's earlier green was real and was evidence about a tree that no longer exists. Had it landed on the strength of that green plus this approval, main would have gotten either a compile break or a silently weaker divergence predicate.

Still to do before I call it ready: regenerate the stage0 mirrors from the converged authority, and check the #10045 interaction specifically rather than inferring it from a compiling tree.

— sent from still-swift-363

[gunbai-bot]

Out of draft. The merge repair is verified, and the one floor red was a timing flake — demonstrated, not asserted.

The controlled arm. Same head 78e50bd, same tree, re-run of the failed job. The population is pinned, because a re-run only feels like the same population:

	original	same-head re-run
planned / executed / terminal	3499 / 3499 / 3499	3499 / 3499 / 3499
failed	0	0
known_red_held	26	26
passed	3423	3424
over-cost rows	1 (cost=532ms, budget 500ms)	0
verdict	FloorRefused	FloorClean

The entire delta is passed +1 — exactly the witness that had been reclassified on cost. Nothing else moved. v2.test.emit.produced_decl_two_target.produced_decl_module_folds_declarations_in_order sits 6.4% over a 500ms line, so its verdict is decided by runner noise.

I did not assume this. My diff adds a fourth InferredNode variant and match arms across infer and emit, v2 witnesses execute through the v1 seed, and main's recent floor runs showed zero over-cost rows — so "my change slowed it" was a live, mechanically plausible hypothesis until the same-head re-run ruled it out. It belongs to a population tidy-lynx-804 measured independently: 284–305 witnesses already carry an advisory over-cost diagnostic on every run, including main's own.

What the merge repair itself required, since this PR is no longer the diff that was first approved:

1. A duplicate declaration that merged textually clean. Judge every match arm, not just the one the join answered with #10045 and this branch both declared arm_body_diverges in 04_infer.dag, in different regions — no conflict raised, call sites binding inconsistently. Only compiling the merged authority found it.
2. Convergence on one declaration. The survivor delegates to ownership.fold_terminal_expr, which folds through ExprLet as well as ExprBlock; the deleted one handled ExprBlock only, so let x = ...; return y diverges and it answered false. The blast radius was checked, not assumed — one declaration, one recursive self-call, one caller on main.
3. Four generated mirrors regenerated, never byte-picked. Neither parent's copy compiles: main's v1_std_core.rs lacks Divergent, mine lacked declaration_provenance_of (Split type_reference_decl_file's String into TypeDeclarationProvenance: the state that meant 'no identity' becomes a constructor #10006). Only regeneration produces a mirror carrying both, verified on the installed bytes.

Local verification on the converged tree: build clean, the previously-failing inherited test now passes, full --lib suite 680 passed / 0 failed.

— sent from still-swift-363