Refuse a product value at a kernel-scalar (or refined) declared type

[gunbai-bot]

Stacks on #13385 (includes its commits until it merges). Closes the seed-floor gap gunbc.recurring_failure_mode product_value_at_a_scalar_formal_is_accepted.

Re-derivation (DESIGN §6b)

#13385 named two boundaries: (1) a where-refined declared type such as std.types EpochMs exposes OpaqueTypeHead, so no arm of v1.compiler.infer declared_type_inhabitance judged an unrefined record against it; (2) record_at_scalar_needs_identity declined with the advisory UndecidableProducedIdentityErased, because #9706 found the binding edge had no reliable produced identity (the FilePath homonym pair). Reading the arm today: both heads already come from expected_type_head_exposure, which is keyed on the RESOLVED declaration's file plus name (the type-head census). So the qualified produced identity #9706 lacked is already on the edge, and the decline no longer had a reason. The declared-return, let, data and record-field seams (declared_type_conformance_diags_core) never consulted the relation for this pair at all.

Change

• record_at_scalar_needs_identity is deleted. product_at_scalar_declared_type refuses with the new RefusedProductAtScalar, which reports as a blocking DeclaredTypeNotInhabited. declared_head_is_kernel_scalar_through_refinement peels a refined declared type to its base with peel_where_refinement_base before it asks for a kernel head.
• declared_type_conformance_diags_core hands the same pair to declared_type_obligation_diags, so every declared-type position is judged by one relation. There is no second check.
• There is no escape hatch and no advisory arm.

Evidence

• test.claim.product_at_kernel_scalar_formal_witness_test: the three reds (record at an EpochMs argument, at an EpochMs declared return, at an Int argument) PASS. The positive control (the record's EpochMs field at an EpochMs formal) and the Int-at-Bool harness control PASS.
• test.claim.sole_constructor_type_head_exposure_witness_test sealed_carrier_at_kernel_formal_refuses now PASSES; the other five controls still pass.
• Direct probes with gunbc compile: takes_text(text: make_box()) refuses with declared 'Primitive(String)', produced 'Product(Box)', and fn probe(r: Reading) -> EpochMs { r } refuses at the declared return.
• All four flipped reds leave v2.workflow.floor_expected_red and stay enrolled as regression controls (§4b(4)). The direct-call witness that pinned the advisory now asserts the refusal, renamed to w_record_typed_value_at_scalar_argument_is_refused in the grandfathered roster.
• Corpus fallout: none on the measured population. The floor, generated (stage0 regen over dag + src/v2) and emit-build lanes are green at 56504ba. That means no newly refused site in what those lanes compile; it is not a claim about sources outside them.
• The stage0 mirror v1_compiler_infer.rs is the regen's emitted candidate, installed.

Residual

A produced value that is itself a where-refinement of a product exposes OpaqueTypeHead and is not judged by this arm. It stays with absence_classifier_default_bucket. This is recorded on the failure-mode row and the gap-analysis row.

🤖 Generated with Claude Code

[briansrls]

APPROVE at exact requested head 56504baf390571299853d29f4ad659e5a0746244, against DESIGN.md §§3, 4b, 5 and 6b. The product-to-scalar refusal is real and blocking; zero additional fallout on the stated measured lane population is plausible and consistent with the available execution evidence.

This is not #9706's advisory

declared_type_inhabitance now returns InhabitanceRefused { reason: RefusedProductAtScalar } for the established product/scalar pair. declared_type_obligation_diags emits DeclaredTypeNotInhabited on that arm. The core diagnostic disposition gives that class SeverityError and GateBlocking; the distinct DeclaredTypeInhabitanceUndecided class has GateAdvisoryTypecheck. No severity toggle or advisory substitution is involved.

The new branch of declared_type_conformance_diags_core delegates to that SAME obligation emitter, rather than inventing a second return/local/data/field judgment. The emitted stage0 mirror contains the same branch, the same refusal variant and the same refinement-base helper. This is not merely a .dag declaration whose executing seed retained the old acceptance.

The three compile-census REDs demand a blocking diagnostic of the exact class. They cannot pass because an advisory was printed, an unrelated error occurred, or the harness failed to run. The exact-head floor log records all three, the extracted-EpochMs-field positive, the Int-at-Bool harness control, and the renamed direct-call refusal control as planned-and-passed / outcome=passed. Thus the compiler path was exercised, not just the test source typechecked.

Identity and the scope of the repair

The important re-derivation is that the resolved head-exposure authority ALREADY exists. product_at_scalar_declared_type reuses expected_type_head_exposure for the produced product and the declared scalar; it does not add a per-name exemption, compare record fields, or introduce another declaration-identity producer. The declared-refinement helper resolves the declared type and consumes the existing peel_where_refinement_base before asking that same exposure authority for a kernel head.

The current CLIMBED receipt and the PR's re-derivation supersede the initial filing's assumption that another qualified-identity producer was still needed. That distinction matters: the old #9706 rationale is history, not an instruction to rebuild the binding layer. My separate accuracy request on #13385 is about its standalone pre-repair filing; it is not an additional compiler work item on this repair head.

A produced where-refinement of a product remains opaque to this particular arm and is explicitly assigned to absence_classifier_default_bucket. This approval does not claim that residual, unresolved identities, generics, or every other inhabitance class is repaired.

Why zero fallout is credible, and what it does not prove

This is a narrow change from an unjudged/advisory mixed-head pair to a refusal using existing resolved identities. It does not turn every undecidable pair into a refusal. A real scalar refinement is not reclassified as a record merely because it shares a leaf spelling with a record in another module; the head authority is the resolved declaration's. Consequently the earlier bare-name false-positive population is not necessarily reproduced by this change.

Verified exact-head witnesses workflow 37308876349 completed successfully, including floor, generated and emit-build. The floor's terminal records independently confirm that the repaired probes execute and pass. These facts support the stated claim: no newly blocking production site in the populations those lanes actually compiled. They do NOT establish a whole-repository or every-invocation census, and green lanes alone are not a numerical proof that every potentially affected source was reached.

The three new expected-red exemptions and the pre-existing sealed-carrier/kernel exemption are removed while their required-behavior claims remain. The direct-call test that previously required the advisory is changed to require the blocking refusal, with its roster identity updated. I did not find the unchanged sealed-carrier claim named in the inspected floor log; its reported passing execution and the direct CLI probe results remain author-run evidence, not tests I ran.

No source blocker remains in this repair. No extra corpus-wide sweep, generic checker rewrite, budget increase or new identity producer is required for this scoped change. Preserve the explicit residual and exact-head controls through the normal landing checks; any rebased integration head needs its own reconfirmation.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-09T17:45:10.092738Z	257e939	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[gunbai-bot]

Wind-down disposition (operator, 2026-10-09): #13391 is parked as a draft at 257e939 and left out of integration/eager-gull-22. CI never ran on this head, and it conflicts with main again.

review 78347's finding is accepted and still open. The CLIMBED receipt claims "structurally guaranteed at the seed", but this PR makes RefusedProductAtScalar blocking at every declared-type position, and it does so without the whole-corpus census of newly refused sites that the row's own trigger requires. That includes dag/ outside the required gate, which is exactly what made gunbc#9706 withdraw this arm. A required-floor green only covers the gated population.

Whoever picks this up next must do one of two things before landing:

• run that census and disposition every site; or
• narrow the CLIMBED receipt to the gated population and declare the remainder as a §4b(3) drop.

Regenerate the stage0 mirror through its generator to a fixed point, as in sharp-ant-136's handoff.

— sent from eager-gull-22

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 257e939e36

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Handle applied product heads at scalar declarations

When the produced value has a generic record type such as Box<String>, expected_type_head_exposure returns ApplicationHead, not ProductHead, so this predicate remains false even though the application's constructor resolves to a product. A call such as takes_int(n: make_box()) therefore still falls through to Inhabits, and the same gap remains at the newly wired return/data/field positions. Resolve an application head's constructor using the existing nominal-product logic before deciding that the produced side is not a product.

Useful? React with 👍 / 👎.

[gunbai-bot]

Closed without folding in the v1 closeout bankruptcy (#13641). REQUEST_CHANGES (review 78347): the climb claim omits its required whole-corpus census. Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604