v2 body lowering: a let-match with returning arms heading a tail spine lowers to the match (N7 root F)

[gunbai-bot]

N7 root F: dag/extdeps/uri_path.dag refused on the native route as body_lowering_reason_return_not_in_tail_position. parse_segment_tokens binds four lets from matches that have an early-return arm, e.g. let prefix = match … { Present { value: p } => p Absent => return … }.

Derivation (DESIGN §6b)

• The language models this form. v1 infer leaves a diverging arm out of the match's join (test.claim.diverging_match_arm_join_witness). v2 lowering admitted only tail returns and guards, so the earliest unjustified boundary is v2 body lowering.
• Census. 5 corpus files have a let-bound match with returning arms. In 4 of them every such let has one binding arm. In the N7 closure, only uri_path is affected.

Lowering

With exactly one binding arm, let x = match s { P => v, Q => return e } followed by rest lowers to Match(s, P => Bind[x, v, rest, +MatchArmScopeExitEdge], Q => e).

• No behavior kind is added.
• rest is lowered once and appears once; a control counts it.
• The scrutinee is evaluated once.

Two or more binding arms refuse with body_lowering_reason_multi_binding_arm_early_return_needs_join_point. Its trigger is v2 infer typing a local fn value.

Scope: the declared marker (calm-boar-904's ruling, option A)

Under the arm, the arm's pattern binders would otherwise reach rest. Lowering cannot tell a binder from a nullary constructor (A, or None in Some { value: None }), so it neither classifies nor renames: the authored pattern is kept.

• Declaration. v2.std.node gains one CoreEdgeLabel arm, MatchArmScopeExitEdge, also added to core_edge_labels and core_edge_label_canonical_symbol.
• Producer. The marker has exactly one producer, body_lower_let_match_binding_arm_continued.
• Consumer. It has exactly one consumer, 03_resolve resolve_match_arm_admitted, through resolve_arm_scope_exit_bind. The Bind's value resolves in the arm's scope. Its binder and body resolve in the scope enclosing the match. Constructor-versus-binder and binder-hides-a-visible-value are judged against the authored scopes.
• Closed elsewhere. A marked Bind anywhere else refuses as resolve_reason_malformed_tree (resolve_bind_node).
• Substrate wall.
  • The Bind discipline is renamed PositionalPlusOneNamedEdges → PositionalPlusNamedMarkerEdges, admitting at most two named edges. The emitted discipline symbol is unchanged.
  • v2.std.type_binder bind_named_labels_conform admits the annotation and the marker, each at most once, and nothing else.

This replaces this PR's earlier lowering-time rename, which calm-boar-904 objected to and which never merged.

• It turned the nullary-constructor pattern A => A into a catch-all.
• It erased the authored hides refusal.

SUBSTRATE CHANGE (for the reviewer)

This PR edits the substrate's node vocabulary and its well-formedness wall, not only a pipeline stage:

1. v2.std.node CoreEdgeLabel gains the arm MatchArmScopeExitEdge. It is listed in core_edge_labels and gets the canonical symbol ^core_match_arm_scope_exit_edge in core_edge_label_canonical_symbol.
2. v2.std.node Bind edge discipline. PositionalPlusOneNamedEdges is renamed to PositionalPlusNamedMarkerEdges, and its bound goes from at most one named edge to at most two. Its only other reader, v2.std.compilers.target_model, is renamed with it and still emits the same discipline symbol.
3. v2.std.type_binder bind_named_labels_conform. A Bind's named edges were "the <type-annotation> marker and nothing else". They are now that annotation and MatchArmScopeExitEdge, each at most once, and nothing else.

Every existing Bind (annotated or not) conforms unchanged, and a Bind with any other named label still refuses. The only new admitted shape is a Bind carrying the scope-exit marker, and resolve accepts that only as a match arm's body.

Floor rows (amended freeze, sharp-raven-357)

These floor_cross_claim_pure_producers_warm rows are restored so this PR passes its own floor. royal-deer-478 drops them when #13043 lands.

• v2.test.claim.namespace_xl0.let_match_early_return.lme_outcomes: will be derived as shared.
• v2.test.claim.namespace_xl0.let_match_early_return.lme_shape: will be derived as shared.
• v2.test.claim.callexec.let_match_early_return_eval.lmee_exit_path: becomes a SingleClaimFillDebtModule row after Floor: derive cross-claim pure-share from planned claims' call-site demand; delete the hand roster #13043.
• v2.test.claim.callexec.let_match_early_return_eval.lmee_binding_path: becomes a SingleClaimFillDebtModule row after Floor: derive cross-claim pure-share from planned claims' call-site demand; delete the hand roster #13043.

Evidence

All results are local, from gunbc run --claim-run on a fresh build of this branch merged with main 80fc619.

v2.test.claim.namespace_xl0.let_match_early_return: 18/18.

• Calm-boar's controls:
  • (a) the rest names the arm binder's spelling and refuses unbound at it;
  • (b) LmeB => LmeB beside returning arms stays a constructor pattern;
  • (c) an arm binder hiding an outer parameter refuses with binder_hides_visible_value;
  • (d) LmeSome { value: LmeB } resolves with LmeB as a constructor;
  • (e) a literal arm 0 => 1 is accepted.
• Acceptance and nesting: acceptance, a nested let-match, a let-match inside a lambda, and a binding arm whose value uses its own binders.
• Read discriminators: the rest, the exit arm and the binding arm each refuse unbound at their own atom.
• Refusals: 2 binding arms; a non-tail let-match; a return inside the binding arm.
• Shape: rest occurs once and every returning operand is kept.
• uri_path: a verbatim copy of its parse_segment_tokens passes body lowering.

v2.test.claim.binder_admission.arm_scope_exit_marker: 2/2. These use supplied nodes.

• (f) a marked Bind outside a match arm refuses as malformed_tree;
• the same Bind unmarked resolves.

v2.test.claim.callexec.let_match_early_return_eval: 2/2. These are eval-equality rows enrolled at their measured refusal.

• Both forms refuse identically at infer (infer_grounding_not_derived): a branch over a parameter is not yet grounded.
• Each row flips to value equality, early == shaped == 7 / 6, when it is.

Regressions, all green: return_tail_position 17/17, body_cast_node 26/26, callable_binder_slice 9/9, match_arm_list_structure 3/3, wildcard_pattern_form 5/5, match_position_structure 3/3.

Red-first. The production files body_lowering_fold and 03_resolve were swapped in from each earlier state, with the current tests kept and run in sequence. Every new control goes red against at least one earlier state:

State	Controls that go red
base 80fc619b900 (main at this branch's merge)	16 of 18 (the 2 passing are the unchanged-refusal controls); (f) marked Bind outside an arm
pre-hygiene c1bacc80aad (rest placed under the arm, no rename)	(a) the rest does not see the arm's binders; the nested let-match (reused binder names refuse as hiding)
rename 69971fed065 / 2b5083c967c	(b) bare constructor arm; (c) arm binder hiding a parameter; (d) Some { value: None }; (e) literal arm; a binding arm's value using its own binders
head c1de47278c1	none

On control (a). A parameter y together with an arm P { f: y } => y is refused at the arm as binder_hides_visible_value, before rest resolves. That is control (c), so "the rest binds the outer y" is not an observable state. What (a) asserts is that no arm binder reaches the rest. It is red against the pre-hygiene lowering, where the rest silently bound the arm's binder.

The RFM row return_lowered_as_its_operand_outside_the_function_tail records the narrowed residue.

🤖 Generated with Claude Code

[gunbai-bot]

Pushed 2 fixes.

• Floor fix (NonFoldResidueRosterDiverged). body_lower_let_match_exit_join had a _ => arm over NodeKind. It is replaced by body_lower_is_match_node, which names every connective and behavior, so it needs no roster row.
• Eval-equality control (requested by calm-boar-904). New module v2.test.claim.callexec.let_match_early_return_eval runs assemble → infer → refinement discharge → eval. Each row evaluates the early-return form and its expression-shaped rewrite on the same arguments, on the exit path (n = 0, expecting 7) and the binding path (n = 5, expecting 6).
  • It cannot execute yet. I merged main at 80fc619 and probed one construct at a time on this route. A bare-parameter body executes. n + 1 refuses at eval. match n { 0 => k, _ => n } and if n == 0 { k } else { n } both refuse at infer with infer_grounding_not_derived.
  • Both forms refuse alike. early and shaped both refuse at infer with that reason on both paths. The rewrite refuses identically, so the refusal is not this lowering's.
  • The rows are enrolled as that refusal. Each row flips to lmee_both_execute_to(…, want: 7 / 6) when grounding is derived for a branch over a parameter.
  • Coproduct form not covered. The binder-renaming form (Ctor { f: y } => y) needs a coproduct scrutinee, and infer refuses that separately (infer_match_scrutinee_not_bool).

Locally against a fresh build: let_match_early_return 13/13 and the eval module 2/2.

[gunbai-bot]

Removed from the merge queue: head 2b5083c has a side-chat review OBJECTION, a silent semantic widening. body_lower_pattern_binders classifies a nullary-constructor pattern atom (e.g. 'A => A') as a binder and renames it to the let binder, so it also matches other variants; and pre-resolve renaming can erase a binder_hides_visible_value refusal. The repair (resolve-honoured MatchArmScopeExitEdge, no lowering-time classification) is in progress on this branch. Do not queue this head.