A coproduct payload can inhabit its parent coproduct field, and nothing refuses it

dag/gunbc/explicit_witness_admission.dag

@@ -158,6 +158,14 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
     reason: "NO LONGER THE CLOSING VALIDATION FOR roadmap node v1-test-migration as of 2026-08-11 (gunbc#8146, review 51212) — that node rebound to test_migration_debt_test.dag retained_rust_kernel_wall_holds_against_live_tree when the authority inverted from classifying departures to declaring residents, and gunbc.roadmap_authority is the single authority for that binding. RETAINED as an expecting-red probe only: it still measures a real derived quantity and greening it would still be progress. It was: the discriminating closing validation for roadmap node v1-test-migration, RED BY DESIGN while any independently discovered legacy #[test] function has no typed behavior disposition. Unlike the diff-scoped deletion guard it cannot pass on zero progress; stale, duplicate, unresolved and unclassified identities all refuse.",
     dissolution: unbound_dissolution(description: "the derived unclassified legacy-behavior set reaches zero with every disposition admitted — this row deletes in the completing change, promoting the unchanged acceptance witness to ordinary DiscoverySelection as the permanent migration regression wall")
   ),
+  known_red_probe(
+    entry: "dag/test/claim/coproduct_payload_soundness_witness_test.dag",
+    f: "cpp_payload_where_coproduct_required_must_refuse",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "A COPRODUCT PAYLOAD CAN INHABIT ITS PARENT COPRODUCT FIELD AND NOTHING REFUSES IT -- the general form of the defect #8853 repaired at one site. There, a std.occurrence_identity.OccurrenceId (the payload carried inside MintedOccurrence) was declared as a parameter and assigned into Node.occurrence_id, whose type is the NodeOccurrenceId coproduct; nothing refused it, and the consequence surfaced one pipeline stage away as `non-exhaustive pattern match on: OccurrenceId` in sixteen floor claims. MEASURED GENERALLY, minimal pair, no Node and no compiler internals: CppHolder { subject: cpp_inner() } is ACCEPTED BY TYPING and dies at runtime with PatternMatchFailure, while the correct spelling CppHolder { subject: CppWrapped { inner: cpp_inner() } } compiles and executes -- so the mechanism is neither Node-specific nor occurrence-specific. This is BELOW FLOOR, not a rung: DESIGN section 4b places `values inhabit declared types` in the ordinary compiler floor, and a floor failure is a below-baseline safety regression rather than a class sitting at mitigatable. Red BY DESIGN and not relaxable: the only edit that may green it is making the ill-typed construction refuse. Its positive control (cpp_payload_inside_its_own_arm_still_compiles) is enrolled as an ordinary green claim so the red measures the distinction rather than a blanket refusal. Owner: the compiler type-soundness lane. THIS ROW DOCUMENTS THE RED AND ITS DISSOLUTION; the required floor is gated by the identity's row in v2.workflow.floor_expected_red, per the ruling at floor_expected_red_chunk_13. Both rows delete together when the wall lands.",
+    dissolution: unbound_dissolution(description: "the construction refuses with a located, blocking type diagnostic -- this row deletes in the change that lands the wall, promoting the witness to ordinary DiscoverySelection as the permanent regression control DESIGN section 4b(4) requires stay enrolled")
+  ),
   known_red_probe(
     entry: "dag/test/claim/observation_raw_print_retirement_acceptance_test.dag",
     f: "observation_emit_frontier_is_zero",

dag/test/claim/coproduct_payload_soundness_witness_test.dag

@@ -0,0 +1,87 @@
+module test.claim.coproduct_payload_soundness_witness_test
+
+// A COPRODUCT PAYLOAD CAN INHABIT ITS PARENT COPRODUCT FIELD, AND NOTHING REFUSES IT.
+//
+// This is the general form of the defect repaired in #8853 at one site. There,
+// `dag_int_literal_node_from_magnitude` declared its parameter as
+// `std.occurrence_identity.OccurrenceId` -- the PAYLOAD carried inside `MintedOccurrence` -- and
+// assigned it straight into `Node.occurrence_id`, whose type is the `NodeOccurrenceId` coproduct.
+// Nothing refused the assignment. The consequence surfaced 2,000 lines and one pipeline stage away
+// as `non-exhaustive pattern match on: OccurrenceId { value: 79 }` in sixteen floor claims, because
+// the total match over that field had no arm for a value that is not in its type.
+//
+// The declaration fix closed the live instance. It established nothing about the class, and the
+// targeted sweep that found no second instance of that exact field/type pair is evidence about a
+// spelling, not about the typing hole. So the question this file asks is the general one: can an
+// ARBITRARY coproduct payload inhabit the field declared as its parent coproduct?
+//
+// MEASURED ANSWER, by direct execution before this witness was written -- minimal pair, no Node, no
+// occurrence, no compiler internals:
+//
+//   type CppInner  { value: Int }
+//   type CppOuter  = CppWrapped { inner: CppInner }
+//   type CppHolder { subject: CppOuter }
+//
+//   POSITIVE   CppHolder { subject: CppWrapped { inner: cpp_inner() } }   accepted, exit 0
+//   NEGATIVE   CppHolder { subject: cpp_inner() }                         ACCEPTED BY TYPING,
+//                                                                        then at runtime:
+//                                                                        PatternMatchFailure
+//                                                                        { value: "CppInner { value: 7 }" }
+//
+// So the mechanism is not Node-specific and not occurrence-specific. It is a floor-class soundness
+// hole -- values inhabit declared types -- and DESIGN section 4b puts a floor failure below the
+// ladder rather than on a rung of it: this is not a class sitting at `mitigatable`, it is the
+// baseline guarantee not holding.
+//
+// WHAT IS ASSERTED. compile_dag_rust_emit_check must REFUSE the fixture below: placing a variant's
+// payload where the variant's own type is declared must be a located, blocking type diagnostic, not
+// a program that compiles and dies at its first match. The witness returns false today, which is why
+// it is enrolled as an expecting-red identity rather than asserted green here.
+//
+// ENROLLED IN TWO PLACES, AND THEY ARE NOT THE SAME FACT -- I got this wrong on the first attempt
+// and the floor caught it. `v2.workflow.floor_expected_red` is what GATES the required floor: an
+// identity there still executes and its outcome is still asserted, but a failure counts as
+// agreement. `gunbc.explicit_witness_admission` DOCUMENTS the red and its dissolution and, per the
+// ruling recorded at floor_expected_red_chunk_13, does not itself gate the floor. Enrolling only in
+// the second is what reds a build.
+//
+// THE POSITIVE CONTROL IS NOT OPTIONAL AND IS NOT COSMETIC. Without it, a compiler that refused
+// EVERY record literal would satisfy the claim above. The control asserts that the correct spelling
+// -- payload inside its arm -- still compiles, so what the red measures is the distinction and not
+// the mechanism's blanket refusal.
+//
+// dissolve-on: none. Per DESIGN section 4b(4), a climb deletes the redundant lower-rung production
+// machinery but never the evidence: when the wall lands, this probe's admission row deletes and the
+// witness stays enrolled as a permanent regression control. Deleting it on the climb would recreate
+// specification-without-execution one rung up.
+
+fn cpp_soundness_negative_fixture_source() -> String {
+  "module cpp.probe\n\nimport std.types { Int }\n\ntype CppInner { value: Int }\n\ntype CppOuter\n  = CppWrapped { inner: CppInner }\n\ntype CppHolder {\n  subject: CppOuter\n}\n\nfn cpp_inner() -> CppInner {\n  CppInner { value: 7 }\n}\n\nfn cpp_payload_where_coproduct_required() -> CppHolder {\n  CppHolder { subject: cpp_inner() }\n}\n"
+}
+
+fn cpp_soundness_positive_fixture_source() -> String {
+  "module cpp.control\n\nimport std.types { Int }\n\ntype CppInner { value: Int }\n\ntype CppOuter\n  = CppWrapped { inner: CppInner }\n\ntype CppHolder {\n  subject: CppOuter\n}\n\nfn cpp_inner() -> CppInner {\n  CppInner { value: 7 }\n}\n\nfn cpp_wrapped_holder() -> CppHolder {\n  CppHolder { subject: CppWrapped { inner: cpp_inner() } }\n}\n"
+}
+
+// THE DISCRIMINATING RED. `CppInner` is the payload inside `CppWrapped`, not a member of `CppOuter`,
+// so this assignment must refuse at typing. It does not: the program compiles and the failure is
+// deferred to whatever later match reads the field.
+test fn cpp_payload_where_coproduct_required_must_refuse() -> Bool {
+  !compile_dag_rust_emit_check(
+    cpp_soundness_negative_fixture_source(),
+    "src/cpp_probe.rs",
+    [],
+    []
+  )
+}
+
+// THE POSITIVE CONTROL. The correct spelling must still compile, or the red above is satisfied by a
+// compiler that refuses everything and measures nothing.
+test fn cpp_payload_inside_its_own_arm_still_compiles() -> Bool {
+  compile_dag_rust_emit_check(
+    cpp_soundness_positive_fixture_source(),
+    "src/cpp_control.rs",
+    [],
+    []
+  )
+}

src/v2/workflow/floor_expected_red.dag

@@ -389,8 +389,19 @@ fn floor_expected_red_chunk_13() -> List<String> {
   Cons { head: "test.claim.method_arg_declared_contract_witness_test.w_method_arg_infers_against_declared_contract_not_element_type_test", tail: Empty {} }
 }
 
+// The record-literal seam of the payload-as-coproduct soundness class (gunbc#8865). ELIGIBLE under
+// this roster's own rule: it reaches its subject and answers -- compile_dag_rust_emit_check runs the
+// fixture and returns, so the red is a real verdict, not a route gap. Its positive control
+// (cpp_payload_inside_its_own_arm_still_compiles) is deliberately NOT enrolled: it must stay an
+// ordinary green, or the pair stops discriminating.
+//
+// This row deletes in the change that lands the wall. The roster's passing-row arm is what makes
+// that self-announcing rather than something anyone has to remember.
 fn floor_expected_red_chunk_14() -> List<String> {
-  Empty {}
+  Cons {
+    head: "test.claim.coproduct_payload_soundness_witness_test.cpp_payload_where_coproduct_required_must_refuse",
+    tail: Empty {}
+  }
 }
 
 fn floor_expected_red_chunk_15() -> List<String> {