XL-2: if-arms lower through the statement authority; a statement followed by another refuses located

[gunbai-bot]

XL-2 continuation, gaps 1 and 2 of body_lowering_fold. Gap 3 (the Optional accessor) is not claimed fixed; see §4.

1. What was wrong, and the repair

If-arms were read by the operand reader alone. body_lower_try_if_from_captured lowered the condition with body_lower_value_lowered, but read each arm with body_lower_if_arm_operand_optional. That operand reader reads a call g(p: x) as g. So on main, an undeclared x in either arm resolved, and a block arm kept only its first statement.

An arm is { stmt_seq }, and body_lower_stmt_spine is already the one authority for a statement sequence. The new body_lower_if_arm_lowered lowers each arm through it:

• one statement is folded whole, a let binds the rest, and any other statement followed by another refuses;
• its refusal is the arm's refusal;
• an else if arm is an if_expr, not a brace body, so it keeps the if reader;
• the operand reader remains the fallback only when the lowered statement leaves no lowered node behind its shells.

Three readers were tried before this one, and the reasons they failed are recorded in the code comment:

• the condition's reader (value_lowered) deep-unwraps and folds a match spine bottom-up, which reads the pattern _ as a reference;
• the top-down walker keeps the call narrowing;
• folding the brace shell leaves an unpeelable wrapper.

A statement spine went to body_lower_stmt_spine only when let-headed. The guard body_lower_stmt_spine_is_let_headed let every other multi-statement body fall to the expression walkers, which lowered the first statement and dropped the rest, so { c \n x } resolved with x undeclared. It is replaced by body_lower_stmt_spine_has_successor: any spine with a following statement goes to the authority, which already refuses a non-binding statement that precedes another as statement_precedes_without_binding. A one-statement spine keeps its path.

This is the existing verdict applied, not a new rule: { 1 \n c } now refuses even with every name declared. No module in the stratified sample refuses this way (§3).

No stage0 file embeds these functions, so there is no stage0 install. #12173 changed the same fold without one.

2. Witness: red on main 57f5b94, green on this head

The witness is v2.test.claim.namespace_xl0.if_arm_and_statement_lowering_refusal, 13 claims. It runs on the same native front end + resolve route as call_argument_value_resolve_refusal. Its producer iasl_outcomes is enrolled WARM in v2.workflow.floor_pure_producer_share.

claim	main	head
a_call_argument_in_a_then_arm_refuses_at_resolve_at_its_atom	FAIL	PASS
a_call_argument_in_an_else_arm_refuses_at_resolve_at_its_atom	FAIL	PASS
a_call_argument_in_a_nested_if_arm_refuses_at_resolve_at_its_atom	FAIL	PASS
a_statement_followed_by_another_in_a_fn_body_refuses_at_normalize	FAIL	PASS
a_statement_followed_by_another_in_an_if_arm_refuses_at_normalize	FAIL	PASS
a_literal_statement_followed_by_a_declared_name_refuses_at_normalize	FAIL	PASS
a_bare_name_in_an_if_arm_refuses_at_resolve_at_its_atom (neighbour control)	PASS	PASS
a_statement_after_a_let_followed_by_another_refuses_at_normalize (neighbour control)	PASS	PASS
declared_call_arguments_in_if_arms_resolve	PASS	PASS
declared_call_arguments_in_nested_if_arms_resolve	PASS	PASS
a_let_block_in_an_if_arm_resolves	PASS	PASS
a_let_followed_by_its_body_resolves	PASS	PASS
a_match_in_an_if_arm_resolves	PASS	PASS

The witness deliberately avoids list literals and lambdas, so #12198 and #12208 do not flip it. CI still has to plan and pass these claims on this head; the table above is from direct remote runs.

3. Census: main 57f5b94 vs this head

Instrument: v2.compiler.reference_conservation_census reference_conservation_census_for_paths over the 315 files of reference_conservation_stratified_sample_paths plus expression_bodied_fn_decl_parse_test.dag. Only body_lowering_fold.dag differs between the two runs. Refusal reasons come from native_test_context_from_ingest file_refusals for every module that refuses on either side (100 modules).

Added or changed refusal identities (path, fatal reason), each with a disposition:

module	main	head	disposition
dag/extdeps/time/rfc3339.dag	normalizes	list_literal_unlowered	enumerated list-literal refusal. A list in an if-arm call argument (join([...], "")) was silently dropped on main. #12208 lowers it.
src/v2/workflow/compiler_closure_ingest_transport.dag	normalizes	list_literal_unlowered	enumerated list-literal refusal, same shape
dag/test/claim/external_model_scope_live_cover_witness_test.dag	normalizes	list_literal_unlowered	enumerated list-literal refusal, same shape
dag/gunbc/instruments/cheap_gate_pool.dag	call_argument_unread	list_literal_unlowered	refused on both sides; the first refusal is now the list it reaches
dag/gunbc/accelerator_demo/accelerator_demo_eval.dag	list_literal_unlowered	match_arm_navigation_refused	refused on both sides. On main its else-arm (three nested matches) was dropped whole; on head it lowers, and the nested match arm refuses first. The navigation reason is less specific than the list it hides: that loss is the accessor gap of §4, not new.

Removed: none. src/v2/std/cross_tree/resolution.dag refused with match_arm_navigation_refused under an intermediate version of this change; on this head it normalizes.

Atom conservation outside those modules: 15 modules drop fewer atoms, for example host_effect_plan 73→53, ci_compile_jobs 34→13 and cross_tree/resolution 170→128. No module drops more. compiler_closure_emit_driver, systemctl_status_read and runtime_config move one or two atoms from conserved to locus_erased: they reach the normalized tree without their occurrence, and none is dropped.

4. Gap 3, the Optional accessor: not fixed, RFM row stays open

I could not build a probe that isolates body_lower_operand_ref_optional answering Absent instead of a located refusal, meaning red on main and green on a head that fixes it. lowering_accessor_collapses_a_sequence_operand is therefore not retired.

Three specimens were found in the same silent-narrowing family. They are recorded here for the owner of that row; I did not edit the row, because #12198 appends to it:

• if c { c } else if c && (x => x) { c } else { c }: an unreadable lambda operand in an else if condition resolves on main and on this head. The same operand at the top of a fn body refuses with paren_group_unread.
• a multi-line match directly in a match arm, whose call argument is [c] (BlgB { r: y } =>\n match s { BlgA => cc(a: c, b: [c]) ... }): resolves on main and on this head, so the list is dropped silently.
• accelerator_demo_eval.dag above: a list-literal refusal inside nested match arms surfaces as match_arm_navigation_refused, and the cause is lost.

5. New RFM row: a pre-existing resolve defect, exposed and not fixed

gunbc.recurring_failure_mode.a_wildcard_match_arm_resolves_as_an_unbound_name:

• a top-level match s { BlgA => c \n _ => c } refuses on main 57f5b94 as resolve_reason_unbound_symbol at _;
• the if-arm repair makes a match inside an arm reach resolve, so if c { s } else { match s { .. _ => .. } } now refuses the same way, where main had dropped that match whole;
• it is a resolve defect, and it is left for its own change.

Proposed carrier wording

compiler_frontend_program_status.dag is not edited here. Proposed wording for its owner: "If-arms lower through the statement authority (body_lower_stmt_spine): a call argument in either arm reaches resolve, and a statement followed by another refuses as statement_precedes_without_binding at any depth. The Optional accessor's Absent (lowering_accessor_collapses_a_sequence_operand) remains open; its specimens are in #12221."

🤖 Generated with Claude Code

[gunbai-bot]

Review 70856 (stale symbol): fixed in 8dfa610. The witness header cited body_lower_if_part_lowered, which came from an earlier revision of this change. It now names v2.compiler.body_lowering_fold body_lower_if_arm_lowered, which lowers the arm through body_lower_stmt_spine, and it describes the else if and fallback behaviour. git grep body_lower_if_part_lowered now finds nothing in the tree.

— sent from zesty-dove-429

[briansrls]

APPROVE on exact head 8dfa610 for MERGE-QUEUE landing only.

This closes XL-2 gaps 1 and 2 at the claimed grain. The if-arm path now sends ordinary arm bodies through the complete statement-spine lowerer before extracting the lowered value, while the explicit nested else-if route retains the existing if reader. That addresses the silent narrowing demonstrated by the call-argument specimens without broadening the claim to Optional-member access.

The statement-spine change is likewise appropriately bounded: it dispatches any spine with a successor to the existing reducer, so a non-let predecessor reaches the already-located body_lowering_reason_statement_precedes_without_binding refusal instead of silently discarding the tail. Single-statement and nested-if neighbour controls preserve the old accepted cases.

Review 70856's requested discriminators are present on this exact head. The 13-claim witness is enrolled and passes on the floor; the six targeted claims discriminate against main and the two neighbour controls stay green. All five exact-head checks are green.

The main-to-head identity census is adequately dispositioned: no refusing identity is removed; the three added refusing identities are the enumerated list-literal class owned by #12208; two common identities change reason; 15 modules lose dropped atoms and none drop more. Keep those facts separate from the local repair claim.

The Optional accessor remains explicitly outstanding with its three specimens. The wildcard-match-arm RFM is correctly entered as a pre-existing resolve defect exposed here, not repaired by this PR.

Carrier impact after landing: mark XL-2 gaps 1 and 2 delivered only. Leave the Optional accessor gap open. Enqueue this exact head; do not direct-merge it. Require the merge_group candidate and its checks against then-current main.

[briansrls]

Approved for merge-queue landing at exact head c351015.

This refreshes my approval at 8dfa610. The new head is a merge commit whose first parent is that exact approved head and whose other parent is the main revision merged after the queue conflict. The merge commit records one conflict resolution in src/v2/workflow/floor_pure_producer_share.dag, retaining both enrolment comments; src/v2/compiler/body_lowering_fold.dag and the XL-2 implementation merged cleanly.

Revalidated on c351015:

• all five exact-head checks pass;
• all 13 if_arm_and_statement_lowering_refusal claims were planned and passed;
• the required floor is clean;
• the PR is currently mergeable/clean.

Review 70899's operand-reader fallback remark is explicitly not a finding and remains scoped to the declared accessor follow-up. The XL-2 gaps 1 and 2 approval therefore stands unchanged.

Approval is for merge-queue landing only, with the merge_group candidate required to revalidate against then-current main.