Seed floor: a collection and a nominal product are no longer mutually admitted at a declared position

[gunbai-bot]

Seed floor: a collection and a nominal product are no longer mutually admitted at a declared position

DESIGN §4b floor ("values inhabit declared types"), in the v1 seed. It is admitted under gunbc.v1_maintenance_standing because every v2 claim that "the type makes this unwritable" rests on this wall.

The grid (measured by neat-boar-16 on main ff2110b, gunbc run over a probe entry)

declared ← produced	main	this PR
Rec ← List<String>	admitted (the body ran)	refused
List<Int> ← Rec	admitted (the body ran)	refused
Int ← String	refused	refused
Int ← List<Int>	refused	refused
Rec ← Other (a record)	refused	refused
Rec ← Optional<Int>	refused	refused

The first row is the loyal-swift-608 discovery: lively-bat-737's quiet-builder record wall was defeated by passing a List<String> that carried --quiet.

The chain (§6b)

v1.compiler.infer declared_type_inhabitance, with declared=Rec and produced=List<String>:

• collection_at_scalar_declared_type refused only when the declared base peeled to a kernel scalar.
• kernel_value_declared_type_mismatch judges only a kernel actual.
• nominal_product_inhabitance_refusal answers none for a collection, by design.

So the pair reached the terminal Inhabits arm by fallthrough, and the dual pair did the same. Every arm keyed on the kind of ONE side. The earliest unjustified boundary is that the relation's terminal arm is acceptance, while no arm ever judged whether a collection and a nominal product are disjoint.

The repair

collection_at_scalar_declared_type is replaced, not joined by a sibling arm, with collection_disjoint_from_established_identity, a relation over both sides:

• Collection side: exactly one side is an element or keyed collection (node_is_element_collection / node_is_keyed_collection), read on the authored node and on its peel_nominal_alias_identity peel, so type Words = List<String> still counts as a collection.
• Other side: it must be an established non-generic identity.
  • Against a kernel scalar, any collection refuses. This is the prior reach, unchanged.
  • Against a product or coproduct (expected_type_head_exposure), the collection side must be established too, with no unbound type variables. See the false refusal below.
• New refusal reason: RefusedCollectionAgainstNonCollectionIdentity, named for the relation. RefusedKernelAtStructured would be the wrong name for record-vs-collection. Downstream code matches reasons with a wildcard, so no rendered diagnostic changes.

No per-position code was added: the refusal surfaces through declared_type_obligation_diags.

False refusal found and guarded

The v2 self-compile inside claim_executor --required-regen refused a correct record update: with(emit_info, { movable: .. }) passed to emit_info: EmitGraphInfo in src/v1/05_emit_rust.dag. The cause is that v1.compiler.infer_method gives the with builtin the signature Map<map_key, map_value>, which is a placeholder container with unbound type arguments. The establishedness guard above eliminates that false refusal, and it is enrolled as the positive control w_a_record_update_at_a_record_argument_is_admitted. 05_emit_rust.dag itself is not touched.

Census: NOT RUN

The whole-tree false-refusal census has not been run, for this exact reason: gunbc compile --dependency-pool-index primary-precedence --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --source-root dag --source-root src/v2 --target dag refuses on BuildBuddy with WholeCorpusCompileBudgetUnreadable. That happens even on a 48 GB runner with GUNBC_BIND_MEMORY_CGROUP_BYTES forwarded, because no memory.max binds the process. The main baseline refused the same way. Where to run it has been escalated to neat-boar-16 and the operator (srv1/srv2). This PR is not green until that census runs. The only corpus evidence so far is the v2 self-compile inside --required-regen, which covers src/v1 and src/v2, not dag/.

Controls (test.claim.declared_type_inhabitance_direct_call_witness)

• RED w_collection_at_a_nominal_product_argument_is_refused: List<String> at Rec, at the direct-call position.
• RED w_nominal_product_at_a_collection_argument_is_refused: Rec at List<Int>.
• RED w_the_declared_record_refuses_a_smuggled_argv_list: the loyal-swift shape. The DECLARED QuietInvocation refuses the smuggled --quiet list, which gives lively-bat-737's next-rung trigger something to fire on.
• RED w_collection_at_a_list_element_of_record_type_is_refused: the second position. Deviation: the brief asked for the record-literal field, but that position has no obligation producer. v1.compiler.infer DeclaredTypePosition names it among the nine positions still awaiting one, so a control there would measure the missing producer, not this relation. The list-element position shows the same thing, one emitter with no per-position code.
• Positives: w_conforming_collection_and_record_arguments_are_admitted, w_list_at_an_aliased_list_formal_is_admitted (guards the peel), w_a_record_update_at_a_record_argument_is_admitted.

Mutation: claim_batch built on main's mirrors (the relation reverted) fails all four REDs, and the positives plus the existing w_list_typed_value_at_non_empty_str_argument_is_refused stay PASS. On this head every claim in the file passes except w_a_branded_refinement_at_an_unrelated_product_formal_still_refuses, which is an enrolled ExpectAssertionFalse RED and fails identically on main's compiler.

Failure-mode row

Specimen three is appended to gunbc.recurring_failure_mode.declared_type_wall_keyed_on_the_value_being_a_kernel, with both directions, the grid and the chain. This PR does not land that row's trigger: the relation still dispatches on the kind of each side, rather than deciding from the formal's declaration for an actual of any kind. No second row was minted.

v2 path, measured

Probed v2.std.inhabitance declared_type_inhabitance with the infer_application_argument_inhabitance witness pattern, using a probe that is not committed. inhabitance_node_undecidable_reason classes any Instantiation type node (which is how List<String> is represented) as UndecidableGenericFormal:

• Rec ← List<Int>: admitted, with an undecidable advisory.
• List<String> ← Rec: neither refused nor marked undecided.
• My atom-vs-atom control (Other ← Rec) was also not refused, so my synthetic argument shapes may not carry the types I intended. The v2 grid is reported as partly measured.

This is not the same one-relation change: v2 must distinguish applied types with concrete arguments from generic formals. It is reported to neat-boar-16 rather than fixed here.

Emission

Not measured. No claim is made about the emitted route.

Stage0 mirrors

Regenerated through claim_executor --required-regen. The bootstrap was taken from main's mirrors, because a compiler carrying the unguarded relation refuses to self-compile the guarded source. That produced gen1; gen1 was installed and rebuilt, and the gen2 regen reports all three installed mirrors byte-identical to their candidates (the fixed point). The gen2 regen's only drift is the two pre-existing std_* files.

• Installed: v1_compiler_infer.rs, plus v1_compiler_emit.rs and v1_compiler_infer_resolve.rs. Those two were already stale on main at 0be6287, and the regenerated infer mirror adds a struct field that the emit mirror must supply. The emit mirror change is two generated lines; 05_emit_rust.dag is untouched.
• Not installed: std_integer.rs and std_machine_constraints.rs are also stale on main, but their regenerated candidates do not compile (PointerWidth is a variant, not a type). They are left at main's copies as pre-existing drift, outside this PR.

🤖 Generated with Claude Code

[gunbai-bot]

CI note on 2b7843a: emit-build fails with error[E0573]: expected type, found variant PointerWidth in the emitted std_integer.rs. This is pre-existing on main. emit-build fails with the identical error at 0be6287 (this PR's base), 45286d6 and fb859cf. It is the same std_integer / std_machine_constraints emission defect that makes those two stage0 candidates uncompilable, which is why this PR leaves those mirrors at main's copies. This PR's own defect, the clippy failure on the hand-built InferScope in infer_semantics_witness, is fixed in 2b7843a, and clippy is now green.

[gunbai-bot]

Superseded by #12045 (merged as 9fd525e). It establishes everything this draft carried: the symmetric collection-vs-established-identity relation, both REDs, the smuggled-argv claim, the conforming and alias positives, the with() record-update repair (with a genuine-Map control this draft lacked), specimen three on declared_type_wall_keyed_on_the_value_being_a_kernel, the v2 counted-frontier witnesses, and the whole-tree census. The only item not in #12045 is a list-element-position RED (w_collection_at_a_list_element_of_record_type_is_refused), which shows the relation fires at a second wired position. It is reported to neat-boar-16 as an optional follow-up, not carried here.