Refuse a product value at a kernel-scalar declared type (re-derives #13391)

[gunbai-bot]

Re-derives gunbc#13391 (history only; its head is not a base) on current main.

What changed

• src/v1/04_infer.dag product_at_scalar_declared_type: a product value where a kernel-scalar type, or a where-refinement of one (std.types EpochMs), is declared now refuses with DeclaredTypeNotInhabited (RefusedProductAtScalar), blocking. It replaces the advisory record_at_scalar_needs_identity (UndecidableProducedIdentityErased). Both heads come from expected_type_head_exposure, which is keyed on declaration identity, so the std.types FilePath / extdeps FilePath homonym that made Enforce decidable application inhabitance arms #9706 decline is judged by declaration. The refined declared type is judged through peel_where_refinement_base. A produced where-refinement of a product stays opaque here and is owned by absence_classifier_default_bucket. The return, local, data and field routes delegate to the same obligation emitter.
• Stage0 mirror v1_compiler_infer.rs regenerated with claim_executor --required-regen.
• The three RED claims in declared_type_product_at_kernel_scalar_formal_witness_test and the sealed-carrier-at-kernel claim are removed from floor_expected_red and stay as permanent regression controls; the direct-call test that required the advisory now requires the refusal. Failure-mode row and gap doc updated.

Receipts

• claim_batch on a seed built from this head: product_at_kernel_scalar_formal 5/5, sole_constructor_type_head_exposure 6/6, declared_type_inhabitance_direct_call 42/43. The one red, w_a_branded_product_refinement_at_an_unrelated_product_formal_still_refuses, is the enrolled expected-red of absence_classifier_default_bucket (a produced refinement of a product, not this arm).
• gunbc test //gunbc/instruments:self-host exit 0 and //gunbc/instruments:v2-native-cli exit 0 at head 06bcaa2. srv1 was not reachable by ssh from this container (no identity), so both ran in this container (cgroup memory.max 24 GiB; no systemd-run).
• Census: the required-regen compile of the whole emitted population (planned=executed=adjudicated=169, 2295 admitted edges) with the new check raised no new refusal, and the infer mirror is at its fixed point. The only remaining drift it reports is extdeps_ietf_http_semantics.rs, which this change does not touch and which I did not regenerate here.

Known unexecuted

• The whole-corpus site census asked for by the old review was NOT produced. I ran the measured whole-root route (gunbc compile --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --source-root dag --source-root src/v2 --dependency-pool-index primary-precedence --target dag --output-dir <empty dir>, seed built from this head). It printed 1414 indexed modules outside the compile-clean closure enter the name census only (not compiled), finished compile.frontend (1 min) and compile.normalize, then the process was killed with exit 137 (OOM; this container's cgroup memory.max is 24 GiB, oom_kill 1). The committed projection's 16 GiB peak was measured on 2026-08-28 against a smaller tree. srv1 (the host the projection was measured on) is not reachable from this container, so I could not rerun with more memory.
• Unjudged population, with counts: of 8327 .dag files under dag/ and src/v2/, the 1414 modules above are not compiled by this route even when it completes, and the remainder was not reached to the typecheck stage in the killed run. No site list exists, so no site is dispositioned beyond the evidence below.
• What does bear on it: the 169-surface required-regen compile (2295 admitted edges) with this check raised no new refusal; both instruments compile their closures with the seed carrying the check; the claim files assert the refusal and the positive controls. That is a lower bound on the corpus, not the census.
• Next step that closes it: run the route above on a host with more than 24 GiB (srv1), list every DeclaredTypeNotInhabited with reason RefusedProductAtScalar, and disposition each.

🤖 Generated with Claude Code

Whole-corpus census (srv1, head 06bcaa2 vs main a9be5ef)

gunbc compile --source-root dag --source-root src/v2 --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --output-dir <empty dir>: 26m50s, 37.7 GB peak. Main 122 blocking errors, the head 126, exactly four new, none removed. Dispositions (fixed at the owning site, no suppression); each entry module recompiled here with 0 blocking errors:

1. gunbc.durable_cas_file_store cas_window_max_generation: the fold seed none carried no type so the accumulator was Unit; seed is now a CasGeneration? binding.
2. gunbc.product.build_selection entry_standing call: sensitivities took no_missing (a List<AxisGap>) where List<NonEmptyStr> is declared; no sensitivities is [] (as std.decision passes).
3. gunbc.roadmap.roadmap_belt_actuate placement record write: unit_properties is List<String> but received List<SystemdRunProperty>; now mapped through new extdeps.systemd.systemd_run systemd_run_property_assignment, the one NAME=VALUE spelling, which the two --property=/-p projection arms also use now (was inlined twice).
4. gunbc.workspace_operator_request release: idempotency_key takes NonEmptyStr, was given the WorkspaceAllocationId wrapper; now id.value.
   Fix head 3dd8b9c. 1414 modules remain name-census only (declared above).

Census of refreshed head 89a5ee8 (run on srv1)

gunbc compile --source-root dag --source-root src/v2 --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --output-dir <empty dir>: 122 blocking errors, the identical set to main 3ee2abc's 122. No error appears only on this head and none only on main, so the four fixed sites are clean and nothing new is introduced. The 1414 modules that stay name-census only are declared under Known unexecuted. Run: 26 min, 37.7 GB peak RSS, MemoryMax 96G, swap 0.

Handoff (successor can continue from origin alone)

State: census confirmed identical to main on srv1 (122 errors); no stage0 drift on either tree; approvals present. Next: when told it is next, merge main once by merge commit, regen to fixed point, drift gate, rerun claims and both instruments, fresh review/witnesses, packet. Traps: same as #13699 (roster.dag deletion, StaleBinary, rebuild seed after last edit).

[gunbai-bot]

Superseded by #13742, reopened from the id-free branch census/product-at-scalar. Closed unmerged.