Key the declared constructor and the pattern with one identity

[gunbai-bot]

Coproduct exhaustiveness compared a keyed pattern name against an unkeyed declared constructor, so a declared arm carrying a dotted authored name matched no pattern spelling and was reported missing under its dotted name. This change restores the key to the side it was dropped from.

The mechanism is narrower than the work item's title says, and the title is wrong. variant_pattern_coverage_key is not a bare-name normalization minted in exhaustiveness beside a qualified declaration identity. git log -S on that symbol over src/v1/04_patterns.dag gives two commits. It was introduced in f135ed0 (#8931) applied symmetrically — once on the pattern side, once in the declaration-side filter, and once mapping the missing list, which is why infer_semantics_witness coproduct_exhaustiveness_missing_arm_names_only_gap requires missing[0] == "Beta" bare. Both of that bin's coproduct assertions were green as authored. 8f8e513 (#10028, the nested-pattern matrix rewrite) deleted both declaration-side applications and kept only the pattern-side one, inlined at pattern_matches_constructor. So the class is the coverage key is applied to one side, not two identities disagree.

The identity, therefore, is the seed's incumbent one: the bare leaf. symbol_index.global_bare is keyed on it, and qualified_last_segment is the join at roughly twenty sites across v1.compiler.infer — variant lookup at a Disj, coproduct arm resolution, formal/actual name compatibility. variant_pattern_coverage_key is that same identity under a local name. Re-applying it to the declaration side mints nothing. Moving exhaustiveness to a scope-carrying identity instead would be the namespace program's own root cut (the SymbolIndex/OccurrenceBinding cutover, #11264) performed in the wrong place, would reverse both assertions above, and would require global_bare and every qualified_last_segment join to move in the same motion. The work item's "no leaf-name key" instruction was written on the inverted premise and was overridden by swift-bat-902 on the PHASE 1 finding.

PURPOSE admission. gunbc.v1_maintenance_standing v1_seed_standing. Seed inference correctness blocks the v2 self-host program. No language feature is added.

The edit, in full. Two mechanisms, one identity, three declarations touched in v1.compiler.infer_patterns.

Coverage — pattern_matches_constructor keys both operands. Every coverage comparison in the fold routes through this one predicate (constructor_appears_at_row_head and specialize_pattern_row both call it), so this is the whole of the matching repair. The absent-constructor witness cell in exhaustiveness_witnesses carries the key, because that cell is what names the gap.

Ambiguity — find_variant_child_keyed refuses when more than one declared child keys equal, rather than taking the first. Keying by leaf makes a.b.Alpha | Alpha possible, which exact-name matching could not produce, so this change creates the collision and owes it an arm. Measured on the first-match revision, that source compiles clean: the bare arm binds the first child and the match is called exhaustive while the second declared variant is unhandled. More than one match now resolves to no match, which the three call sites already carry into variant_not_found_result — a typed, located refusal in existing vocabulary. No ambiguity diagnostic is minted; the frontier is the missing scope-carrying identity, and inventing a spelling for it would model the gap rather than refuse over it. Found in gatekeeper review by eager-raven-113 on 3671563.

Variant lookup — lookup_variant_in_type compared a name against a child's raw authored name at all three of its variant-lookup sites: the qualified branch reduced only the pattern through qualified_last_segment, the bare branch reduced neither. A bare arm therefore could not resolve against a child declared under a dotted authored name, and refused with VariantNotFound. find_variant_child_keyed keys both operands and is used at exactly those three sites.

The two mechanisms have different causes, and the PR does not blur them. The coverage key lost a symmetric application at #10028. The lookup asymmetry is as old as the function: git log -S on both branches returns only f135ed0, and the pre-deletion lookup_variant_in_type at eebdeca^ already shows the same shape — pattern reduced, child raw. One is a regression; the other has never been right.

What is deliberately left alone. find_child_named is unchanged: it also resolves fields at lookup_field_in_variant, so keying it would widen what a field name may match rather than repair an identity. constructor_roster_for stays raw. render_constructor_witness renders a constructor that is covered, naming a nested gap beneath it, and is outside this scope.

Reachability, stated at its real grain and not inflated. An arm-level scan of authored .dag under dag/ and src/ — splitting each type ... = ... right-hand side on its top-level | and testing each arm head, rather than matching lines — finds no arm head spelled as a dotted name. That is a source search, not a compiler judgment: it establishes that no author wrote one, not that none can be constructed, and it is not asserted as zero exposure. The compiler-grade answer is the probe below. The real cross-module case is already green and permanently controlled by test.claim.match_exhaustiveness_coproduct_witness w_cross_module_complete_match_is_clean and w_cross_module_provider_growth_reports_one_non_exhaustive, because an import binds the leaf name and the provider's children keep their bare declared names. In v1.compiler.parse parse_type_body_after_eq a dotted arm is reachable only as the first arm of the no-leading-pipe form, through parse_dotted_ident shared with the type-alias lookahead; every later arm goes through expect_ident. Executed receipt for that pair pending.

Declared frontier (§4b(2)), not fixed here. A leaf-keyed identity collides when two variants share a leaf name under different containment. That is the namespace program's class, not this one's. Trigger: the scope-carrying binding cutover (#11264) answering by execution. Consumer: variant_pattern_coverage_key. Row ownership is being settled with crisp-carp-634, whose row for this class lives on the unmerged #11277 — one row, not two.

Evidence, executed. The reduction is enrolled in the existing test.claim.match_exhaustiveness_coproduct_witness, not a second file. Both columns are measured runs of a locally built claim_batch — baseline on the committed seed, after on the regenerated one.

witness	baseline	regenerated
w_dotted_declared_arm_covered_by_bare_patterns_compiles_clean	RED	PASS
w_dotted_declared_arm_is_not_reported_missing	RED	PASS
w_bare_pattern_resolves_against_a_dotted_declared_arm	RED	PASS
w_dotted_declaration_with_a_genuinely_missing_arm_still_refuses	green	PASS
w_dotted_arm_in_later_position_refuses_at_parse	green	PASS
w_cross_module_complete_match_is_clean	green	PASS
w_cross_module_missing_c_reports_one_non_exhaustive	green	PASS
w_cross_module_provider_growth_reports_one_non_exhaustive	green	PASS
w_two_declared_arms_sharing_a_leaf_key_refuse_rather_than_bind_the_first	RED	PASS

The whole-source witness is the reduction. The two class-scoped witnesses beneath it keep either site from being credited with the other's repair: the coverage edit closes the NonExhaustiveMatch half, the lookup edit closes the VariantNotFound half, and a change fixing only one cannot green this section. The negative control was green on baseline and stays green — keying both sides does not make a real gap disappear, which is the difference between repairing the checker and widening it. The later-position witness asserts a refusal rather than an exhaustiveness count, because a parse refusal and a clean compile both report zero rows of any later class.

The whole file runs clean on the final seed: claim_batch reports 26 requested, 26 PASS, 0 FAIL, and infer_semantics_witness exits 0.

The collision witness had to be measured, not reasoned about. Its first draft used a.b.Alpha | c.d.Alpha and was green under both revisions: parse_more_variants_acc takes every arm after the first through expect_ident, so the second dotted arm refuses at parse and the collision is never reached. That check could never fail, and would have stood as coverage for the arm it never exercised. The discriminating shape puts the dotted name first and the colliding one bare; the witness annotation records that constraint so it cannot silently stop testing anything.

infer_semantics_witness, and the provenance of its baseline. On the regenerated seed the binary exits 0, so coproduct_exhaustiveness_qualified_declared_names_accept_bare_arms and coproduct_exhaustiveness_missing_arm_names_only_gap pass and become permanent controls. Stated precisely: the after is executed here; the before is crisp-carp-634's receipt 5655408711 as relayed in the work item, not a run of mine — that binary was never built against the unmodified mirror in this lane. The end-to-end evidence for the before is the reduction's baseline column above, which exercises the same defect through the whole front end rather than calling check_match_exhaustiveness directly.

Regeneration receipt. claim_executor --required-regen --regen-affected-scope selected WholePopulationScope (v1.compiler. is a generation input): 155 planned, executed and adjudicated, elapsed 495192 ms, sampled peak RSS 11,266,652 KiB. The bound in force was a 22 GiB address-space ceiling (ulimit -v). GUNBC_BIND_MEMORY_CGROUP_BYTES declined to tighten, because the container cgroup already bound the process, and the tool's own diagnostic reports admitted budget=33578549248, source=cgroup memory.max — so 22 GiB bounded the process; it was not the budget the tool admitted, and this receipt does not claim otherwise. The run ends in the expected pre-installation drift refusal naming one path; a whole-candidate comparison across candidate/src finds that same single file, and its diff is exactly the five source edits. Only that mirror is installed; no generated file is hand-edited. An earlier attempt refused with MemoryStallRefusedPageThrash under host memory pressure and is recorded here as an environmental refusal, not a result.

Out-of-scope extdeps edit, forced by the refusal arm

dag/extdeps/systemd/systemd.dag is edited by this PR and is not v1 seed work. Meet it here rather than in the diff.

extdeps.systemd SystemdUnitProperty declared SubState twice — two identical declaration arms and two identical wire arms — on origin/main since #9761/#10443. One name, two declarations in one coproduct: a §3 single-authority defect. It was invisible because variant lookup took the first exact match and never asked whether a second existed, so it survived every required run in that window without a diagnostic.

This PR's refusal arm is what surfaced it. Both children key equal, so find_variant_child_keyed refuses, and required-witnesses-floor and heal-generated-artifacts both refused with ChangedWitnessObservationFailed naming that declaration. That is the wall's first live encounter, and a stronger argument for the arm than the synthetic collision witness is.

The population was measured before the edit, by the arm-level duplicate-leaf census over every coproduct declaration under dag/ and src/ — splitting each type declaration's right-hand side on its top-level | and counting duplicate leaf keys per declaration, rather than matching lines. SystemdUnitProperty was its sole member. Run the census rather than trusting a transcribed count.

The repair is the deletion of the duplicate declaration arm and its duplicate wire arm. Behaviour is identical — SubState still maps to "SubState" — and the seven witnesses of test.claim.systemd_property_directive_overlap pass. It is admitted here as a forced consequence of a correct refusal with a measured population, on swift-bat-902's ruling that splitting it would only serialize this PR's green behind a one-line PR.

The declaration-time wall is a ledger row, not this PR's scope

Nothing refuses a duplicate variant at declaration. This one was caught at lookup, and only because this change happened to key. A declaration-time refusal is a strictly better rung — structurally impossible rather than mechanically preventable-by-accident — so it is filed as gunbc.recurring_failure_mode.a_coproduct_declares_one_variant_twice with SystemdUnitProperty as its receipt and the census as its population instrument, rather than built here. Its trigger names the capability: the declaration fold refusing a Disj whose children lack pairwise distinct authored names. A lookup-side refusal does not retire it.

Still owed. eager-raven-113's re-clearance of the ambiguity finding, and the srv2 closure receipt (slot queued behind the M fold and #11195/#11290).

The v2 arm is ABSENCE, and it is a different trigger. Measured by fierce-swift-182 on that lane's prepared src/v2/compiler/04_infer.dag (not a native-emitted binary): Match derivation is infer_match_bool, and exhaustiveness is InferBoolLiteralExhaustiveness over two arms classified by infer_bool_literal_pattern_classify, refusing through infer_match_non_exhaustive for a missing true/false. A non-bool-literal pattern is infer_match_pattern_not_bool_literal, not a coproduct-arm census. There is no variant_pattern_coverage_key, no declaration-side key, and no walk of coproduct constructors. So v2 does not share the one-sided-key defect — it does not produce the judgment at all, and the Bool missing-literal RED is a different subject. Because v2 keys no variant on this path, the leaf-collision frontier above does not reach it either. The v2 arm's trigger is therefore a coproduct exhaustiveness judgment existing and being measured, not this change's symmetric-key repair. No native-route execution of that pair is claimed.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Xa46zVYGRz2PUMouekjznP

[gunbai-bot]

Wind-down handoff — held at 9a9b2e61cefd556beaadd5107a277212ebd02792, not enqueued.

At the floor: CI run 34784517640 green on all four required jobs; 1 dashboard approval on head (cursor, review 65706; earlier cursor 65668 / claude 65681 on prior heads); 0 request-changes; GitHub CLEAN. Held because under the be0a86fc landing protocol a change to a seed stage (src/v1/04_patterns.dag + its stage0 mirror v1_compiler_infer_patterns.rs) owes a pre-landing exact-head native M↔T receipt, and no receipt pair ran for this head before the wind-down; no ChatGPT landing thread was reachable to rule otherwise.

To resume: run the receipt pair (claim_executor --v2-native-route at main M and at merge(M, head) T; keyed driver-rows.jsonl comparison must show only this PR's own declared subject), then enqueue head-pinned. If a later seed PR lands first, one merge of main plus a bounded regen (install only the adjudicated mirror set, never hand-edit) precedes the receipt. The arm-level facts worth keeping: the ambiguity arm closes a found fail-open (type T = a.b.Alpha | Alpha compiled clean with a variant unhandled); find_child_named is deliberately untouched because it also resolves fields.

[gunbai-bot]

Superseded by the NAMESPACE-XL integration branch #11461 (operator direction 2026-09-16: one integration branch for the five floor-met PRs). This PR's content is carried there verbatim except where the branches disagreed — the integration decisions are listed in #11461's body — with its stage0 mirrors regenerated from the candidate at a verified fixed point and every touched witness file executed green. Review history stays here; branch kept. — sent from swift-bat-902