infer: a kernel refinement (NonEmptyStr) at a structured parameter refuses like its base (string_replace crash)

[gunbai-bot]

Work item: node://adhoc-0229c068-97e (v2.std.text string_replace crash).

Chain re-derivation (DESIGN §6b)

Symptom: string_replace(source: t, needle: "{ x }" as NonEmptyStr, replacement: ..) resolves clean, then the seed interpreter throws TypeError cannot access field 'head' on String inside v2.std.text string_split.

• string_split / string_replace: justified. Both declare delimiter/needle: FreeSemigroup<Char>, and reading .head is exactly what that contract gives them. No guard belongs here.
• std.types NonEmptyStr is String where non_empty, so it's kernel host text. By DESIGN §4 (the 2026-09-27 text ruling), host text reaches a structural carrier only through the declared Unicode-scalar unfold, or the crossing refuses. There is no such route into FreeSemigroup<Char>, so the call must refuse.
• Earliest unjustified link: v1.compiler.infer kernel_value_declared_type_mismatch. It peeled the declared side through peel_where_refinement_base, but decided the produced side by whether its name is a kernel type. So the plain literal "{ x }" refused (measured: declared 'Node(FreeSemigroup<Product(Char)>)', produced 'Primitive(String)'), and "{ x }" as NonEmptyStr, one name away, was admitted. This is the rostered class declared_type_wall_keyed_on_the_value_being_a_kernel.

Fix: peel the produced side through the same authority before the kernel test. No new relation. The stage0 mirror v1_compiler_infer.rs was regenerated remotely (--required-regen, drift = that one file only).

Evidence

New test.claim.kernel_refinement_at_structured_parameter_witness_test. Each fixture counts blocking DeclaredTypeNotInhabited rows:

• a_kernel_refinement_at_a_record_parameter_must_refuse: false on main cfb3e36 (the RED).
• the_bare_kernel_at_a_record_parameter_still_refuses: true on main (control; the red isn't a new blanket rule).
• a_kernel_refinement_at_its_base_parameter_still_compiles: true on main (control; the peel must not refuse its own base).

The GREEN at head comes from CI's floor, which executes this touched file. Local receipts will be posted as a comment.

Other callers

string_split / string_replace callers: v2.std.compilers.target_model apply_emit_spelling_escapes builds the needle structurally from a Cons. v2.test.std_text.carrier_claims builds needles through FreeSemigroup {..}. Neither is affected. Corpus-wide, this change can newly refuse any kernel-refinement value (a NonEmptyStr, a branded string) passed where a structured type is declared. Every such site is the same latent runtime crash, and the floor enumerates them.

Not in scope (named follow-up)

A string literal cannot yet be written as a FreeSemigroup<Char> needle. literal_homomorphism_rows keys the scalar unfold on the FreeMonoid destination only. A nonempty-literal row for FreeSemigroup<Char> would be the ergonomic route, but its image realization touches v2.compiler.emit_*, which is off-limits to this lane.

🤖 Generated with Claude Code

[gunbai-bot]

Local receipts at head e567bbf (gunbc built from this head, sha256 ab0e57f7…c93): a_kernel_refinement_at_a_record_parameter_must_refuse = true (was false on main cfb3e36); the_bare_kernel_at_a_record_parameter_still_refuses = true; a_kernel_refinement_at_its_base_parameter_still_compiles = see below.

[gunbai-bot]

Completing the receipt above: a_kernel_refinement_at_its_base_parameter_still_compiles = true at head e567bbf. All three rows hold; the RED row flipped false→true across main→head.

[gunbai-bot]

Floor failure at e567bbf was a stale quarantine caused by this fix: w_a_branded_refinement_at_an_unrelated_product_formal_still_refuses (HostIdentity-at-Box) now refuses through the produced-side peel. Its admission trigger ("the final default stops accepting") did not fire, so rather than retire the class I measured the residual: a brand refinement over a PRODUCT at Box is still admitted (0 vs 1 DeclaredTypeNotInhabited). 2636a12 keeps the old witness as a permanent regression control and moves both quarantine rows (floor_expected_red, explicit_witness_admission) to a new RED on that residual, same trigger; absence_classifier_default_bucket records why. Local at head: old witness true, new witness false. — sent from sharp-ibex-842

[gunbai-bot]

CI at 2636a12: generated refused 10 correct rows in gunbc.contributor_onboarding_path (Present { value: x as NonEmptyStr } at Optional<NonEmptyStr>), an over-refusal from peeling the produced side unconditionally. Keeping the has-children guard on the unpeeled node fixed it but reverted the string_replace fix (measured), so the peel is now withheld where the formal carries optionality, the same two-representation exclusion declared_type_kernel_inhabitance_mismatch already makes. Also added the parent lane's probes at the REAL crossing (string_replace's generic FreeSemigroup needle; the generic formal does not short-circuit: main 0 refusals, head 1) plus an Optional-field control. Local at head, rebuilt from the regenerated mirror: all 8 claims in the witness file true, HostIdentity witness true, residual RED false, generated_artifact_gate closure resolves. — sent from sharp-ibex-842

[briansrls]

APPROVE-MERGE at exact head 5358fde8af85de8ab7ec797a07a4f96172ed9dca.

The fix is at the earliest unjustified judgment: kernel_value_declared_type_mismatch already peeled the declared side through the where-refinement base, but classified the produced side by its authored name. Peeling the produced side through the same authority makes a refinement of kernel String inherit the same kernel-vs-structured refusal as String itself, which closes the measured string_replace crash without modifying string_split/string_replace or inventing a new conversion rule.

The Optional exception is justified by measured counter-evidence, not a speculative carve-out: the produced node remains unpeeled when the formal carries optionality, and the permanent control for Present{NonEmptyStr} at Optional stays admitted. The structure guard remains on the effective produced node used by this judgment, and the base/refinement controls show the repair is not a blanket rejection of refinements.

The new permanent claims discriminate the real crossing: cast NonEmptyStr at string_replace's FreeSemigroup needle now has a blocking DeclaredTypeNotInhabited row; the plain literal still refuses; a structural FreeSemigroup needle still compiles; refinement-at-own-base and refinement-at-own-refinement remain admitted; and the Optional regression control stays green. The required-floor log shows all eight touched witnesses planned-and-passed and enrolled.

The stated residual where a product-based refinement reaches an unrelated product remains explicitly witnessed in declared_type_inhabitance_direct_call_witness_test; this PR does not falsely claim that broader class closed. Likewise it does not add the missing literal homomorphism into FreeSemigroup.

Exact-head CI is green for witnesses, floor, generated, rust-unit-tests, and emit-build; required floor reports FloorClean with zero unexpected failures, and GitHub reports the PR mergeable. No remaining merge-blocking finding.