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

dag/test/claim/diverging_match_arm_join_witness_test.dag

@@ -0,0 +1,324 @@
+module test.claim.diverging_match_arm_join_witness
+
+// The discriminating RED for the diverging-arm join defect, kept verbatim as the
+// reproduction that found it. Before `v1.compiler.infer` excluded diverging arms
+// from the match's join, `probe_cell` below could not be authored at all: the
+// `let` bound from a match whose sibling arm `return`s was typed as the union of
+// the binding AND the function's return coproduct, so passing the binding to a
+// parameter declared `Cell` refused with `value does not inhabit its declared
+// type at the direct call argument ... declared 'Product(Cell)', produced
+// 'Coproduct(ProbeResult)'`. The file is therefore its own regression control:
+// if the join ever re-admits a diverging arm, this module stops resolving and
+// every witness here goes red at resolve rather than at assertion (DESIGN 4b(4)
+// -- the evidence stays enrolled after the climb).
+
+type ProbeCell { n: Int }
+
+type ProbeResult
+  = ProbeOk { cell: ProbeCell }
+  | ProbeUnknown { why: Int }
+
+fn probe_cell_of(xs: List<ProbeCell>) -> Optional<ProbeCell> {
+  first(xs)
+}
+
+fn probe_takes_cell(cell: ProbeCell) -> Int {
+  cell.n
+}
+
+fn probe_cell(xs: List<ProbeCell>) -> ProbeResult {
+  let cell = match probe_cell_of(xs: xs) {
+    Absent => return ProbeUnknown { why: 0 }
+    Present { value } => value
+  }
+  ProbeOk { cell: ProbeCell { n: probe_takes_cell(cell: cell) } }
+}
+
+// The diverging arm must not widen the binding, and the surviving arm's own type
+// must still be the one that flows: a present cell reaches the parameter declared
+// `ProbeCell` and its field is read.
+test fn a_diverging_arm_does_not_widen_the_binding_type() -> Bool {
+  match probe_cell(xs: [ProbeCell { n: 7 }]) {
+    ProbeOk { cell } => cell.n == 7
+    ProbeUnknown { why: _ } => false
+  }
+}
+
+// The diverging arm is still REACHED and still returns early -- excluding it from
+// the type join must not exclude it from evaluation. Without this the fix could be
+// satisfied by dropping the arm entirely.
+test fn the_diverging_arm_still_returns_early() -> Bool {
+  match probe_cell(xs: []) {
+    ProbeOk { cell: _ } => false
+    ProbeUnknown { why } => why == 0
+  }
+}
+
+// A block whose terminal statement is the `return` diverges too, so the join must
+// look through the block rather than at its expr_data alone.
+fn probe_cell_block(xs: List<ProbeCell>) -> ProbeResult {
+  let cell = match probe_cell_of(xs: xs) {
+    Absent => {
+      return ProbeUnknown { why: 1 }
+    }
+    Present { value } => value
+  }
+  ProbeOk { cell: ProbeCell { n: probe_takes_cell(cell: cell) } }
+}
+
+test fn a_block_terminating_in_return_also_diverges() -> Bool {
+  match probe_cell_block(xs: [ProbeCell { n: 3 }]) {
+    ProbeOk { cell } => cell.n == 3
+    ProbeUnknown { why: _ } => false
+  }
+}
+
+// POSITIVE CONTROL, and it is the one that keeps the fix from being a hole: a
+// match with NO diverging arm still joins every arm, so both arms must agree.
+// This is the ordinary path the change must leave untouched.
+fn probe_no_divergence(xs: List<ProbeCell>) -> Int {
+  let cell = match probe_cell_of(xs: xs) {
+    Absent => ProbeCell { n: 0 }
+    Present { value } => value
+  }
+  probe_takes_cell(cell: cell)
+}
+
+test fn a_match_without_a_diverging_arm_still_joins_every_arm() -> Bool {
+  probe_no_divergence(xs: []) == 0 && probe_no_divergence(xs: [ProbeCell { n: 5 }]) == 5
+}
+
+// REVIEW 58314 (codex/gpt-5.6-sol, REQUEST_CHANGES on #9964): the first version of
+// `arm_body_diverges` hand-walked ExprReturn and ExprBlock and forked a traversal
+// `v1.compiler.ownership` `fold_terminal_expr` already owns. The predicate now routes
+// through that fold, which handles ExprLet by recursing into `let_body`.
+//
+// THESE TWO WITNESSES DO NOT DISCRIMINATE THAT, and saying so is the point of this
+// note. Measured, not assumed: the pre-fix predicate was rebuilt and both PASS
+// against it. `{ 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. No surface shape found so far produces an arm whose terminal is an ExprLet
+// node. They are kept as BEHAVIOUR-PRESERVATION controls -- the fold must not change
+// what the block and bare forms answer -- never as evidence that an ExprLet hole was
+// live.
+fn probe_cell_let_terminal(xs: List<ProbeCell>) -> ProbeResult {
+  let cell = match probe_cell_of(xs: xs) {
+    Absent => {
+      let why = 2
+      return ProbeUnknown { why: why }
+    }
+    Present { value } => value
+  }
+  ProbeOk { cell: ProbeCell { n: probe_takes_cell(cell: cell) } }
+}
+
+test fn a_return_behind_a_terminal_let_also_diverges() -> Bool {
+  match probe_cell_let_terminal(xs: [ProbeCell { n: 9 }]) {
+    ProbeOk { cell } => cell.n == 9
+    ProbeUnknown { why: _ } => false
+  }
+}
+
+test fn the_let_hidden_diverging_arm_still_returns_early() -> Bool {
+  match probe_cell_let_terminal(xs: []) {
+    ProbeOk { cell: _ } => false
+    ProbeUnknown { why } => why == 2
+  }
+}
+
+// ---------------------------------------------------------------------------
+// REVIEW 5083893018 (REQUEST_CHANGES on #9964), blocker 1: the filter created a
+// state the old code could not reach -- arms nonempty, NON-DIVERGING arms empty --
+// which fell through to `Absent => scrut_rt` and typed the match as the value it
+// CONSUMES rather than the value it produces. I had verified that case does not
+// CRASH; I had not verified it types correctly. Those are different claims.
+//
+// `all_arms_diverge` is that case: every arm returns, so the match's own type must
+// still be the arms' join (ProbeResult), never the scrutinee's (ProbeFlag).
+//
+// THESE TWO DO NOT DISCRIMINATE THE REPAIR, MEASURED -- but the one at the bottom of
+// this file DOES, so the repair is not evidence-free. The pre-repair code
+// (unconditional filter) was rebuilt -- binary hash 8c7e053c1bbc, confirmed by hash
+// change -- and both witnesses below PASS against it. A `Bool`-scrutinee variant is
+// not authorable at all: Bool literals do not parse as patterns.
+//
+// WHY TERMINAL POSITION CANNOT SEE IT. `v1.compiler.infer` `DeclaredTypePosition`
+// declares TWELVE positions; `DeclaredTypeObligation` is constructed at TWO, carrying
+// `PositionDirectCallArgument` and `PositionListElement`. `PositionDeclaredReturn`
+// occurs only in the unwired-position comment, the variant declaration, and a display
+// string -- it has NO PRODUCER. So at terminal position nothing consults the match's
+// own type, whatever it is computed to be. That is a real gap and it is why these two
+// are green under both binaries; it is NOT a ceiling on the class, because a WIRED
+// position observes the same state (see `an_all_diverging_match_in_argument_position`).
+// These two are behaviour controls.
+
+type ProbeFlag = ProbeYes | ProbeNo
+
+fn all_arms_diverge(f: ProbeFlag) -> ProbeResult {
+  match f {
+    ProbeYes => return ProbeUnknown { why: 10 }
+    ProbeNo => return ProbeUnknown { why: 11 }
+  }
+}
+
+test fn a_match_whose_arms_all_diverge_types_as_the_arms_not_the_scrutinee() -> Bool {
+  match all_arms_diverge(f: ProbeYes) {
+    ProbeUnknown { why } => why == 10
+    ProbeOk { cell: _ } => false
+  }
+}
+
+test fn the_second_all_diverging_arm_is_reached_too() -> Bool {
+  match all_arms_diverge(f: ProbeNo) {
+    ProbeUnknown { why } => why == 11
+    ProbeOk { cell: _ } => false
+  }
+}
+
+// Blocker 3: the ordinary-arm control returned ProbeCell from BOTH arms, so a
+// mutation keeping only the FIRST non-diverging arm and discarding the rest left
+// every witness green. `prefer_specific_type` is selective and order-sensitive, so
+// the discriminating shape is PAIRED ORDERINGS whose arms contribute differently:
+// `Absent` carries no element type, `Present { value: 5 }` carries Int. Keeping
+// only the first arm therefore yields a different join in one ordering than the
+// other, and one of the two should red under "keep first, discard the rest".
+//
+// IT DOES NOT, MEASURED. A keep-first mutant (`.take(1)` on the non-diverging arm
+// results) was built -- binary hash cd33904dbf9a, rebuild confirmed -- and this
+// witness PASSES against it. So this control has the SAME defect review 5083893018
+// found in the one it replaces: it certifies without discriminating. Kept as a
+// behaviour control and labelled, never cited as evidence that arm-join order is
+// enforced.
+
+fn joined_absent_first(f: ProbeFlag) -> Optional<Int> {
+  match f {
+    ProbeYes => Absent
+    ProbeNo => Present { value: 5 }
+  }
+}
+
+fn joined_present_first(f: ProbeFlag) -> Optional<Int> {
+  match f {
+    ProbeYes => Present { value: 5 }
+    ProbeNo => Absent
+  }
+}
+
+fn probe_unwrap_or_zero(o: Optional<Int>) -> Int {
+  match o {
+    Present { value } => value
+    Absent => 0
+  }
+}
+
+test fn both_orderings_of_a_two_arm_join_carry_the_element_type() -> Bool {
+  probe_unwrap_or_zero(o: joined_absent_first(f: ProbeNo)) == 5
+    && probe_unwrap_or_zero(o: joined_present_first(f: ProbeYes)) == 5
+    && probe_unwrap_or_zero(o: joined_absent_first(f: ProbeYes)) == 0
+    && probe_unwrap_or_zero(o: joined_present_first(f: ProbeNo)) == 0
+}
+
+// THE DISCRIMINATING RED FOR BLOCKER 1 OF review 5083893018, and the one that reaches
+// a WIRED seam. MEASURED IN BOTH DIRECTIONS: PASS on the repair (binary 01a53030eafa),
+// and under the pre-repair unconditional filter (binary 8c7e053c1bbc) the module
+// REFUSES at resolve with
+//   error: value does not inhabit its declared type at the direct call argument for
+//   parameter 'r': declared 'Coproduct(ProbeResult)', produced 'Coproduct(ProbeFlag)'
+// -- the match typed as the value it CONSUMES rather than the value it produces,
+// exactly the defect the review named. The difference
+// from `all_arms_diverge` above is one thing: the all-diverging match sits in a
+// DIRECT-CALL ARGUMENT position rather than terminal position.
+// `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
+// positions that IS wired. So the match's own computed type is compared here,
+// where at terminal position nothing consults it.
+//
+// The scrutinee must NOT be Optional: `declared_type_inhabitance` bails to
+// `InhabitanceUndecidable { UndecidableOptionalCarrier }` when either side carries
+// CardOptional, which would swallow the comparison before it happens. A plain
+// coproduct scrutinee walks past that bail.
+fn probe_consume(r: ProbeResult) -> Int {
+  match r {
+    ProbeOk { cell } => cell.n
+    ProbeUnknown { why } => why
+  }
+}
+
+fn probe_all_diverge_as_arg(fl: ProbeFlag) -> ProbeResult {
+  let n = probe_consume(r: match fl {
+    ProbeYes => return ProbeUnknown { why: 30 }
+    ProbeNo => return ProbeUnknown { why: 31 }
+  })
+  ProbeUnknown { why: n }
+}
+
+test fn an_all_diverging_match_in_argument_position_types_as_the_arms() -> Bool {
+  match probe_all_diverge_as_arg(fl: ProbeYes) {
+    ProbeUnknown { why } => why == 30
+    ProbeOk { cell: _ } => false
+  }
+}
+
+// review 58384 (codex/gpt-5.6-sol, REQUEST_CHANGES on #9964) and the case that
+// refuted the previous fallback BY EXECUTION. An all-diverging match produces NO
+// VALUE, so its arms' return-payload types must not become the match's type either.
+// The earlier fallback restored them, and this shape refused with
+//   declared 'Coproduct(ProbeResult)', produced 'Coproduct(ProbeOther)'
+// on an argument that never returns -- a FABRICATED REFUSAL, the DESIGN 5 sign-flip
+// this PR exists to remove, relocated from the scrutinee to the return payload.
+//
+// The rule is now contextual: when every arm diverges the match takes the EXPECTED
+// type, because a value that is never produced inhabits whatever the context needs.
+// `scrut_rt` survives only for a match with no arms at all.
+//
+// The types here are deliberately three-way distinct: the formal is ProbeResult, the
+// arms return ProbeOther, and the scrutinee is ProbeFlag. So this witness reds if the
+// match is typed as EITHER the scrutinee (the original defect) or the arm payloads
+// (the over-correction). A third variant carries the tail because the ownership pass
+// counts a repeated nullary constructor as two consumers of one binding.
+type ProbeOther = ProbeOtherA | ProbeOtherB | ProbeOtherC
+
+fn probe_all_diverge_other_context(fl: ProbeFlag) -> ProbeOther {
+  let ignored = probe_consume(r: match fl {
+    ProbeYes => return ProbeOtherA
+    ProbeNo => return ProbeOtherB
+  })
+  ProbeOtherC
+}
+
+test fn an_all_diverging_match_takes_the_expected_type_not_the_arm_payloads() -> Bool {
+  match probe_all_diverge_other_context(fl: ProbeYes) {
+    ProbeOtherA => true
+    ProbeOtherB => false
+    ProbeOtherC => false
+  }
+}
+
+// review 58406 (codex/gpt-5.6-sol): the contextual rule above only fires where an
+// expected type EXISTS. An ordinary non-tail `let` initializer passes `expected: none`
+// (`v1.compiler.infer` ExprLet, `val_expected`), so the residual fallback still handed
+// back the arms' return payloads and unreachable code was refused against a fabricated
+// type. Reproduced on the pre-repair binary 16a3739a7352:
+//   declared 'Coproduct(B4Res)', produced 'Coproduct(B4Other)'
+//
+// The divergence fact now survives INDEPENDENTLY of a contextual type: an all-diverging
+// match takes `divergent_type()`, a deliberately NAMELESS node. There is no type to
+// report for a value that is never produced, so consumers asking its name get "" and
+// DECLINE rather than refusing against something invented.
+fn probe_all_diverge_unconstrained_let(fl: ProbeFlag) -> ProbeOther {
+  let unreachable = match fl {
+    ProbeYes => return ProbeOtherA
+    ProbeNo => return ProbeOtherB
+  }
+  let ignored = probe_consume(r: unreachable)
+  ProbeOtherC
+}
+
+test fn an_all_diverging_match_in_an_unconstrained_let_fabricates_no_type() -> Bool {
+  match probe_all_diverge_unconstrained_let(fl: ProbeNo) {
+    ProbeOtherB => true
+    ProbeOtherA => false
+    ProbeOtherC => false
+  }
+}

src/v1/00_core.dag

@@ -65,16 +65,38 @@ type FieldSummary {
   value_shape: FieldValueShape
 }
 
+// Divergent is the fourth answer to what inference knows about a node, and it is
+// deliberately NOT a shape of Resolved: an expression that never produces a value
+// has no type to resolve, and an expression whose type the walk could not establish
+// has one it failed to find. Collapsing them -- which a nameless Resolved node does,
+// since the only feature distinguishing it is an absent name -- makes every consumer
+// that declines on a missing name decline on both, and the second is a state that
+// must still be judged. review 5085499375 (D1).
 type InferredNode
   = Resolved { node: Node }
   | CompilerError { message: String, span: SourceSpan }
   | TypeVariable { id: String }
+  | Divergent
+
+// The type of an expression that never produces a value. The divergence is carried
+// as an EXPLICIT FACT in `inferred` (InferredNode Divergent), not inferred from the
+// absent name: namelessness is shared with a type the walk merely failed to resolve,
+// so a consumer keyed on it cannot tell the two apart and silences the second.
+// review 58406: the divergence fact has to survive independently of whether a
+// contextual expected type happens to exist -- an ordinary non-tail `let` initializer
+// passes `expected: none`, so a fallback to the arms return payloads fabricates a
+// type for unreachable code. The name stays empty because there is genuinely no type
+// to name; what consumers match on is the fact, via type_is_divergent.
+fn divergent_type() -> Node {
+  Node { occurrence_identity: OccurrenceSynthetic, name: "", span: no_span(), ident_span: Present { value: no_span() }, children: [], connective: NoConnective, params: [], inferred: Present { value: Divergent }, return_cardinality: Required, uses: [], body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, expr_data: NoExprData }
+}
 
 fn inferred_to_node(inferred: InferredNode) -> Node? {
   match inferred {
     Resolved { node: n } => Present { value: n }
     CompilerError { message: _, span: _ } => none
     TypeVariable { id: _ } => none
+    Divergent => none
   }
 }
 
@@ -83,6 +105,7 @@ fn is_compiler_error(inferred: InferredNode) -> Bool {
     Resolved { node: _ } => false
     CompilerError { message: _, span: _ } => true
     TypeVariable { id: _ } => false
+    Divergent => false
   }
 }
 

src/v1/02_parse.dag

@@ -1252,6 +1252,7 @@ fn occurrence_allocator_after_inferred_node(
     Present { value: Resolved { node: node } } => occurrence_allocator_after_node(alloc: alloc, node: node)
     Present { value: CompilerError { message: _, span: _ } } => alloc
     Present { value: TypeVariable { id: _ } } => alloc
+    Present { value: Divergent } => alloc
     Absent => alloc
   }
 }