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

[gunbai-bot]

#8853 repaired one site where a value of a variant's PAYLOAD type was stored in a
field declared as the variant's parent coproduct. The repair was correct and it
established nothing about the class: a declaration fixed is not a wall built, and
the sweep I ran afterward found no second instance of that exact field/type pair,
which is evidence about a spelling rather than about the typing hole.

So I asked the general question by execution. 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, executes, exit 0

NEGATIVE CppHolder { subject: cpp_inner() }
ACCEPTED BY TYPING, then at runtime:
PatternMatchFailure { value: "CppInner { value: 7 }" }

The mechanism is neither Node-specific nor occurrence-specific. An arbitrary
coproduct payload inhabits the field declared as its parent coproduct, the
program compiles, and the failure is deferred to whatever later match reads the
field -- which is exactly how the OccurrenceId defect surfaced 2,000 lines and
one pipeline stage from its cause.

THIS IS BELOW FLOOR, NOT A RUNG. DESIGN section 4b puts values inhabit declared types in the ordinary compiler floor and calls a floor failure a below-baseline
safety regression, never compensated by higher-order capability. So this row does
not claim the class sits at mitigatable; it claims the baseline does not hold.

WHAT THIS CHANGE IS. Not the wall -- I am not repairing the type checker in the
same diff that discovers the hole. It is the executing evidence, enrolled:

cpp_payload_where_coproduct_required_must_refuse FAIL (expecting-red)
cpp_payload_inside_its_own_arm_still_compiles PASS (control)

verified in that state on the remote runner. The witness uses
compile_dag_rust_emit_check on an inline fixture, the same black-box mechanism
method_arg_declared_contract_witness_test already uses to assert a compiler
refusal, rather than a new one.

THE CONTROL IS LOAD-BEARING. Without it, a compiler that refused every record
literal would satisfy the red. It asserts the correct spelling still compiles, so
what the red measures is the distinction rather than a blanket refusal.

The red is held through gunbc.explicit_witness_admission as an expecting-red
probe so the floor reports it as a known red rather than breaking on it, and its
dissolution is exact: the row deletes in the change that lands the wall, and the
witness stays enrolled permanently as the regression control section 4b(4)
requires -- deleting the evidence on the climb would recreate
specification-without-execution one rung up.

— sent from gentle-eagle-360

[gunbai-bot]

Expected floor red on this branch, and it is not this diff. Main's witness floor is red at 90986d194 with 16 failures, all non-exhaustive pattern match on: OccurrenceId across body_lowering.statement_let_bind and fold_lowering. #8853 fixes that root and is green and awaiting merge; every branch cut from main inherits it.

There is a second thing to expect here that is by design, so it is worth stating before it is mistaken for a defect:

cpp_payload_where_coproduct_required_must_refuse   FAIL   expecting-red
cpp_payload_inside_its_own_arm_still_compiles      PASS   control

The red is the point of the change. It is held through gunbc.explicit_witness_admission as a known_red_probe, so the floor should report it as a known red rather than a failure — if it instead shows up in failed=, the admission row is wrong and that is mine to fix.

The one thing that would genuinely falsify this PR is the control going red: that would mean the fixture is refused for some unrelated reason and the red measures nothing.

— sent from gentle-eagle-360

[gunbai-bot]

This finding is NOT the known v2.* exemption, and the distinction should be settled before triage.

#8854 landed the same repair as my (now closed) #8853, and its annotation says nothing mechanical stands at that call site because module_skips_direct_call_arg_check exempts it. A reader could reasonably conclude this PR is just that exemption observed from another angle. It is not, on two independent counts:

1. The exemption does not cover the fixture. module_skips_direct_call_arg_check is exactly module_name beginning with "v2." (v1_compiler_infer.rs). The fixture here is module cpp.probe — outside the exemption entirely, and it is still accepted.

2. It is not a call-argument judgment at all. The negative is a record-literal field:

CppHolder { subject: cpp_inner() }

The check that should fire is does the value assigned to field subject inhabit CppOuter — record-literal field typing, not direct-call argument typing. The exemption is scoped to the latter.

So the two are neighbours, not the same hole: #8854's site is a declared, bounded exemption with a known dissolution, while this is an ordinary module, an ordinary record literal, and no exemption claimed anywhere. If the fix for one closes the other, that is a welcome surprise rather than the plan — and this probe is what would show it, since it goes green the moment the construction refuses.

— sent from gentle-eagle-360

[gunbai-bot]

Two constraints on whoever builds the wall this probe is waiting for. Neither is in the PR body and both change the implementation, so they belong here rather than in a thread.

1. THE FIX MUST NOT INTRODUCE AN IMPLICIT PAYLOAD-TO-PARENT CONVERSION. The tempting repair is to make CppHolder { subject: cpp_inner() } work by lifting the payload into its arm automatically. That would be worse than the hole it closes: the compiler would have to invent WHICH ARM was intended, and it only looks unambiguous because today's coproducts happen to have one arm per payload type. Two arms carrying the same payload type — entirely legal — makes the choice arbitrary, and an arbitrary choice made silently at a construction site is the fabricated-plausible-output failure with a type system's authority behind it. The negative must become a located compile refusal, not a coercion.

2. DO NOT LAND THE WALL BEFORE THE KNOWN PRODUCTION CONSTRUCTIONS ARE WRAPPED. There is at least one live instance — v2.std.materialize storing Fnv1a64Structural into a ContentHash-declared field (receipt and disposition in #8870, repair owned by the fabric lane). Landing the compiler rejection first turns main red on a defect somebody else has to fix under time pressure. Order:

1. wrap the known production constructions   (fabric lane)
2. land the generic compiler rejection
3. compile the corpus
4. triage every newly surfaced site as a latent correctness defect
5. flip this probe from expecting-red to an ordinary enrolled regression control

AND THE POINT WORTH MORE THAN EITHER: do not grep for the other instances. I was about to, and it is the wrong move. Once the compatibility rule is corrected, every payload stored where its parent coproduct is declared becomes a located compile error — so the fixed compiler IS the corpus-wide census, and it is both stronger and cheaper than any syntactic audit I could write. A grep over record literals would be an approximation of a decision the compiler will make exactly. Step 3 above is not a verification step; it is the enumeration.

That also means the population is currently unmeasured, not zero. The v2.std.materialize instance was found by accident, while checking something else entirely — which is the honest reason to expect more rather than fewer.

— sent from gentle-eagle-360

[gunbai-bot]

The floor red was mine, exactly as predicted, and it is fixed.

I said on this PR that if the expecting-red showed up in failed= rather than held, the admission row was wrong and that was mine. Run 32552049526: failed=1 with this identity, known_red_held=206 unchanged.

The cause is that I enrolled in the documenting roster, not the gating one — and the corpus already says so, at floor_expected_red_chunk_13: the explicit_witness_admission row "documents the same red but (per the same ruling) does not itself gate the required floor." v2.workflow.floor_expected_red is the gate. An identity there still executes and its outcome is still asserted; enrolment only changes which outcome counts as agreement.

Both carriers now state which job they do, and they delete together when the wall lands.

I checked eligibility against that roster's own rule rather than assuming it: its header records 101 rows evicted for being enrolled while never reaching their subject — a never-executed row looks identical to progress. This one reaches and answers, since compile_dag_rust_emit_check runs the fixture and returns a verdict.

The positive control stays deliberately unenrolled as an ordinary green, or the pair stops discriminating.

— sent from gentle-eagle-360