Refuse non-exhaustive imported coproduct matches

[gunbai-bot]

Outcome

Restores the compiler-floor guarantee for closed coproduct matches across module and record-projection boundaries, then makes gunbc.discovery_census total over all five RequiredFloorDisposition arms.

Why the four-arm match compiled

Producer: v1.compiler.infer_patterns.check_match_exhaustiveness, authority revision src/v1/04_patterns.dag at base f1f9dd8a077 (generated seed mirror v1_compiler_infer_patterns.rs). For a structurally unresolved scrutinee leaf, it discarded the node's binding identity and called lookup_type_by_name on its spelling. A record field typed as an imported coproduct can retain the imported binding identity while its spelling is not a local declaration key. The lookup miss fell back to the nominal leaf; because that leaf was neither Disj, optional, nor witness, the producer returned zero diagnostics. This was an absent/fail-open exhaustiveness check, not an advisory and not a declared rung drop.

The repair calls the existing identity-aware lookup_type_for. No new language carrier and no hand-authored Rust behavior were added; the Rust mirror is regenerated from src/v1/04_patterns.dag.

Evidence

Cross-module compile_dag_multi_module_fixture controls (provider Trio, importing consumer, record-field projection):

• provider A/B/C + consumer A/B: one blocking NonExhaustiveMatch (the compiler diagnostic's missing roster is derived from the provider and therefore names C)
• provider A/B/C + consumer A/B/C: clean
• provider A/B/C + consumer A/_: clean
• provider widened to A/B/C/D without changing the complete consumer: one blocking NonExhaustiveMatch (names D)
• unresolved scrutinee type: blocking UnresolvedType, never a clean “not a coproduct” result

Command (regenerated local seed):

./target/release/claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/match_exhaustiveness_coproduct_witness_test.dag --functions w_cross_module_missing_c_reports_one_non_exhaustive,w_cross_module_complete_match_is_clean,w_cross_module_catch_all_is_permitted,w_cross_module_provider_growth_reports_one_non_exhaustive,w_unresolved_scrutinee_refuses_instead_of_becoming_not_a_coproduct

Result: 5/5 PASS.

Census repair:

• DeclinedOutsideRequiredGate is a distinct declined partition arm and count field.
• The mixed fixture inhabits all five dispositions.
• A two-row population control proves one planned and one outside-gate identity partition exactly once, with union cardinality equal to the census.
• Disposition receives the qualified module.function identity required by the cost-debt authority; the Bazel label remains the census/duplicate key.

Interlock

Draft until XL-0 merges. Then this branch will integrate the resulting main, regenerate/reverify the seed, and run the requested #9664 installed-diff / closure-emission / emitted-crate convergence controls before marking ready.

Post-XL-0A regression receipt (680cc49)

Integrated main at ecdeb49. On srv1, a full release workspace build produced gunbc e3aea038937a8fb0 from installed tree 0551f3433211e0fa. One required-regen round planned/executed 139 files, cmp found zero changed regen-population files, and the final canonical installed-tree digest remained 0551f3433211e0fa. BuildBuddy invocation d695d9fc-73bb-4edb-8fbf-7624726c0703 independently completed the same round with an empty generated-file status.

The emitted closure retained the exact 175-member identity population: 174 Rust sources plus Cargo.toml. rustc reached and completed type checking. Its 2,779 diagnostic class table is code-for-code identical to XL-0A: E0308 2671; E0277 34; E0599 16; E0618 12; E0369 12; E0282 9; E0004 9; E0061 6; E0310 2; E0271 2; E0631/E0560/E0533/E0223 1 each. Every XL-0A pre-typecheck class remains closed: E0425/E0603/E0121/E0107/E0391/E0728 all zero.

Identity relation comparison normalized each rendered diagnostic to file x line x column x rustc code x message, sorted uniquely. XL-0A baseline and this head each contain 2,777 unique identities; removed=0 and added=0. The coarser file x line x code relation is also 0/0. Therefore ExhaustivenessRepairExposedLatent=0, RepairLocalRegression=0, UnrelatedBaselineMovement=0, and Unclassified=0. Emitted-tree diff is exactly one of 174 Rust files, v2_std_live_tree.rs, whose only difference is a prose annotation string; Cargo.toml and every diagnostic locus are unchanged.

On the same installed tree, cargo test --release -p v1-compiler --lib reports 552 passed, 0 failed, 140 ignored. The required floor separately executes the cross-module missing/complete/catch-all/provider-growth/unresolved controls. Full srv1 outputs: /tmp/sr147.log, /tmp/sr147-check.txt, emitted crate /tmp/sr147emit.