Fix refinement wall: base-type mismatch through refined-alias chains composes (arbitrary depth)

[briansrls]

Worker attestation

• Title describes the change (not the session id or branch).
• PR body summarises what and why (replace the TODO below).
• Tests run: name the command (e.g. npm test, cargo test) and the result.
• If this closes a work item, the body contains a Closes #N directive.
• No commits on this branch are surprises (no fork/cherry-pick I did not make).
• No secrets / credentials / large binaries staged.

Closes node://adhoc-2ccd029d-c1d

Summary

The v1 where-refinement type-checking wall silently degraded to an advisory diagnostic (WhereRefinementUnenforced, compile-clean green) instead of a hard TypeMismatch refusal when a value's base type disagreed with a refined alias whose own base is itself refined — i.e. a depth-≥2 refinement chain (type S1 = String where non_empty; type S2 = S1 where brand("S2"); data d: S2 = 0). This is DESIGN.md §5's named absorbing fallback anti-pattern reaching the type wall itself: a decidable, structurally-detectable base-type mismatch was silently downgraded to "I couldn't tell" rather than refused.

Two independent instances of the same shape were found and fixed at their single authority in src/v1/04_infer.dag and src/v1/00_core.dag, both proven generic over arbitrary depth (no depth-2-specific code):

(a) kernel_value_declared_type_mismatch (record-field inits, call args) carried its own duplicate one-level peel of the formal's refinement wrapper, instead of reusing the already-correct arbitrary-depth peel_where_refinement_base. Past depth 1 this peel landed on an intermediate alias name rather than the ground kernel type, so the base-type-mismatch check itself never fired and the value silently fell through to the advisory arm. Fix: call peel_where_refinement_base directly (single authority, DESIGN §3) — one change closes both call sites (record-field init and call-arg checking).

(b) where_refinement_diags_for_predicate (direct returns, data inits — these never reach kernel_value_declared_type_mismatch at all, so this was the only wall covering them) used expr_literal_int_optional/expr_literal_string_optional's Absent arm to mean "non-literal value, defer to advisory." But Absent also fires for a literal of the wrong kind (a String literal at an Int-refined position, or vice versa) — a decidable case, not an unknown one. This is the state-space conflation DESIGN.md §3/§5 names: two distinct states (genuinely not a literal vs a literal of the wrong kind) were collapsed onto one Absent signal and both routed to the same silent-defer arm. Fix: a new expr_is_any_literal(expr) predicate in 00_core.dag distinguishes "any literal, of any kind" (refuse on mismatch) from "genuinely not a literal" (unchanged advisory), checked identically in both the int- and string-predicate branches. expr_is_any_literal itself also had to exclude LitNull (total absence of value) from "any literal" — treating the null sentinel as a literal value is the same conflation one layer down, and was independently reachable via dag/extdeps/container/oci/digest.dag:62.

Root cause (a) and root cause (b) are the same shape at different layers — not one bug with two symptoms, but two instances of one absorbing fallback shape: a decidable mismatch signal (a resolved-but-wrong base type; a literal of the wrong kind) getting funneled into the single catch-all "unknown, defer" arm instead of its own refusal arm. The expr_is_any_literal/LitNull fix is a third instance of the identical shape one layer further down (the null sentinel vs. an absent value).

Both fixes are proven generic over arbitrary refinement depth by construction: peel_where_refinement_base walks where_refinement_chain, which recurses on the resolved base type until it hits a non-refinement ground type — there is no depth-2-specific branch anywhere in either fix.

Reachability / denominator

The advisory arm (where_refinement_unenforced_error) is reachable from exactly two call sites in 04_infer.dag — the int-literal branch and the string-literal branch of where_refinement_diags_for_predicate — both of which route through the same Absent-conflation shape described in (b), and both are fixed identically in this PR. kernel_value_declared_type_mismatch is a third, structurally distinct seam (record-field/call-arg admission, not the predicate-diagnostic path) covered by fix (a). No other predicate-kind branches (where_refinement_is_deferred_predicate, e.g. brand/Pattern) route through this Absent-conflation at all — they always emit the advisory unconditionally, which is the correct behavior for a genuinely undecidable predicate (wall-after-grounding, not a bug).

Test plan

dag/test/claim/long/where_refinement_enforcement_witness_test.dag — 38 tests, extended in this PR with dedicated depth-2 and depth-3 specimens beside their depth-1 positive controls:

• where_refinement_depth2_wrong_base_type_record_field_refuses / _accepts — depth-2 specimen (S2 where brand → S1 where non_empty → String), red (base-type mismatch refuses) beside its green positive control (correct base type still accepted).
• where_refinement_depth3_wrong_base_type_record_field_refuses / _accepts — depth-3 specimen, proving the fix composes past depth 2 rather than being special-cased to it.
• where_refinement_depth2_wrong_base_type_call_arg_refuses / _accepts — same depth-2 shape at the call-arg seam (fix (a)'s second call site).
• where_refinement_depth2_wrong_base_type_data_init_refuses / _accepts — same depth-2 shape at the data-init seam (fix (b)'s path, since data inits never reach kernel_value_declared_type_mismatch).
• w_wrong_kind_literal_int_pred_data_init_* / w_wrong_kind_literal_string_pred_data_init_* / w_wrong_kind_literal_direct_return_* — the wrong-kind-literal conflation from fix (b), independent of depth.
• Depth-1 positive/negative controls (w_positive_int_record_field_red/green, etc.) — pre-existing, unchanged, still passing, establishing that depth-1 behavior (which was already correct) is not regressed by generalizing the peel.

All 38 tests run via compile_dag_rust_emit_check against the currently-built seed binary's compile-clean pipeline, which is the same hard authority CI uses (compile_clean_diagnostic_is_hard).

Required-floor coverage (parent review follow-up — attempted, reverted; structural budget finding disclosed)

Parent flagged that the 4 new cause-pinning specimens live in dag/test/claim/long/where_refinement_enforcement_witness_test.dag, whose module (test.claim.long.where_refinement_enforcement_witness) matches long_home_prefixes() — excluded from CI's required floor independent of local execution. Parent's explicit preference: ask whether the cause-pinning assertion genuinely needs the host compile-pipeline file, or whether a minimal fixture crosses the same seam without the long/ exclusion.

A first attempt at this (dag/test/claim/where_refinement_seam_unit_test.dag, calling kernel_value_declared_type_mismatch/expr_is_any_literal directly via import v1.compiler.infer { ... } / import v1.std.core { ... }) passed locally but failed real CI (witnesses check, run 32231028216): unresolved import: module 'v1.std.core' not found (imported by 'test.claim.where_refinement_seam_unit'), likewise for v1.compiler.infer/v1.compiler.infer_env. Root cause: CI's required-floor invocation is claim_executor --required-floor --source-root dag --source-root src/v2 (.github/workflows/witnesses.yml) — it never scans src/v1, so a static .dag-level import of any v1.compiler.* or v1.std.core module from a dag/-rooted witness is structurally unresolvable under CI regardless of correctness. My local runs passed only because I had manually added --source-root src/v1 myself — extra source roots CI does not pass — which is exactly the "local execution is not coverage" gap parent warned about, now caught by CI rather than by review.

This turns out to be a known instance of the same constraint: dag/test/claim/trait_bound_witness_test.dag (a sibling PR, unrelated to this fix) carries a note recording an identical import failure, and its route around it — call through a host builtin that runs the real v1 pipeline over source text (compile_dag_rust_emit_check / compile_dag_diagnostic_census), never a static v1.compiler.* import. This PR does not touch .github/workflows/witnesses.yml — widening the required-floor source-root list to include src/v1 is a shared-CI-workflow decision owned by PR #8526 (session tidy-lark-471), which has measured it directly from CI (run 32219326621) at 12 last-segment collisions and 532 diagnostics, rooted in bare cross-module reference binding rather than a renameable-name list, with a named dissolution (namespace-only resolution) — not a bounded disambiguation question, and not this PR's to resolve.

A separate, sibling PR (#8526) adds a per-PR parse gate over src/v1/*.dag, run outside the hermetic required-floor fold (v1_src_dag_parse.rs, invoked directly by witnesses.yml, not through claim_executor). Checked whether it closes the gap this section discloses: it does not. That binary tokenizes and parses each src/v1/*.dag file independently against an empty environment (v1_compiler_parse::parse(tokenize(...), Rc::new(HashMap::new()))) and reports only a parse diagnostic if one fires — no import resolution, no cross-module binding, no type inference. It is a real, adjacent development (it would have caught the earlier trait_bound_witness.dag-class corruption at the syntax level) but it answers a strictly weaker question than the one this section discloses as open: whether kernel_value_declared_type_mismatch/expr_is_any_literal's type-checking decision logic is correct on a depth-2/3 refinement chain. Parse-clean is necessary but not sufficient for that; the coverage gap below stands unchanged by #8526.

The budget finding stands independent of that question, and is the actual blocker here. The only sanctioned way to witness src/v1 emitter/type-checker behavior from a dag/-rooted witness today is the compile-pipeline host-builtin route, and it costs ~100-200s per assertion (measured directly, this PR) against required_floor_claim_budget_ms()'s 1552ms — two orders of magnitude over the only budget that admits a required-floor claim. That is not "no fixture was found"; the sanctioned route does not exist at the floor's cost ceiling, for this seam, today. A hand-built-Node-literal approach (bypass the compile pipeline, drive the decision function directly on constructed inputs) was in fact the original shape of the reverted witness, and it does not dissolve this particular blocker: kernel_value_declared_type_mismatch and expr_is_any_literal are themselves declared in src/v1 (04_infer.dag, 00_core.dag), so reaching them at all — literal-driven or not — requires the same unresolvable v1.compiler.*/v1.std.core import. Cheap hand-built-literal witnessing is only available on a seam whose decision function already lives in a floor-scanned root (dag/ or src/v2); this fix's decision functions do not.

Disposition: reverted. where_refinement_seam_unit_test.dag is removed from this PR. The required-floor coverage gap parent raised is not resolved by this PR — it is pre-existing debt (the long/ file's structural exclusion, unrelated to this fix's correctness) that this PR discloses but does not expand. Closing it for real needs either src/v1 becoming a scanned required-floor source root (parent's active, separately-owned investigation) or a decision-function relocation/duplication that would itself violate DESIGN §3 single-authority — both out of this PR's scope.

Cause-pinning (parent review follow-up, answered)

Parent asked whether the depth-2/3 reds assert the specific refusal cause or merely "something failed" — a total can't be told apart from a reviewer's read. Answer: four of the reds now pin cause explicitly, added as where_refinement_depth{2,3}_wrong_base_type_{record_field,call_arg,data_init}_pins_type_mismatch_cause, using compile_dag_diagnostic_census (not the coarse compile_dag_rust_emit_check Bool) to assert the red source produces exactly one blocking TypeMismatch row and the green source produces zero, via depth_wrong_base_type_mismatch_count (census_rows_of_class(..., "TypeMismatch") filtered through census_blocking_rows, where_refinement_cause_pinning_note documents the scope decision). This is deliberately scoped to the base-type-mismatch specimens this PR introduces, not retrofitted across all 38 pre-existing tests (a larger, separately-scoped census migration).

Verified by direct execution, per DESIGN §4b rung-honesty, that the assertion logic itself is sound and pins the right cause — not by reading the code. Built and ran ad hoc debug probes (removed before this push) directly against compile_dag_diagnostic_census for the depth-2 record-field red specimen and confirmed the exact row set the currently-built (pre-regen) binary produces: 2 rows, both WhereRefinementUnenforced, both non-blocking; 0 TypeMismatch rows; 0 UnresolvedType rows. That is precisely the pre-fix state the cause-pinning assertion is built to detect and refuse (depth_wrong_base_type_mismatch_count(red) == 1 is false today; it will read 1 once the .dag fix is regenerated into the running binary). All four _pins_type_mismatch_cause tests were then run directly (gunbc run --function <name> --claim-run) against this branch's built binary and all four currently FAIL, for the same already-disclosed reason as the pre-existing boolean reds below: the seed binary has not been regenerated from the fixed .dag sources (see "Verification limitation" below), so TypeMismatch genuinely does not fire yet in the running pipeline. This is the same limitation surfacing at finer (cause) grain rather than a new defect in the new tests' logic.

One correction to a mid-investigation false alarm, kept here for the record rather than silently dropped: these census-based tests were initially suspected of hanging (a prior local run was killed after 100s with no output). Re-run with a longer timeout, each completes in roughly 100-200s and reports a clean PASS/FAIL — not a hang. The cost is real (each assertion drives two full nested compile_sources calls, one per red/green source, against an already-large witness-suite host program) but bounded; a 100s timeout was simply too tight for this specific test shape, not evidence of a defect.

Verification limitation — disclosed

Full required-regen fixed-point verification (regenerated src/v1/stage0/src/*.rs from the fixed .dag sources, rebuilt, witness suite run against that rebuilt binary) was attempted and could not be completed in this PR. Two independent, unrelated blockers, neither introduced by this fix and neither in this PR's scope:

1. A pre-existing population-reconciliation gap in required-regen itself, already found and being fixed separately by smart-ram-730 in gunbc#8518 (fix/required-regen-can-execute): 10 real rows of committed/emitted basename drift (emitted_not_committed=["v1_compiler_trait_bound_witness.rs"], committed_not_emitted=[9 files]) that cause run_required_regen to refuse before completing a fixed point, on main, independent of this branch. Reproduced independently this session with required-regen: the population gate compared two key spaces and refused vacuously on every run #8518's two patches applied — identical 10-row result. Per required-regen: the population gate compared two key spaces and refused vacuously on every run #8518's own framing: this population mismatch was blocked on a population reconciliation nobody has done, which was invisible until the vacuous gate was repaired.
2. A second, distinct defect discovered independently this session: run_required_regen never writes its candidate tree to disk at all when it refuses on the population mismatch above (the write step in write_emitted_tree/copy_hand_maintained_support runs after the population check, so a refused run leaves nothing on disk to build from). Working around that locally (a diagnostic-only, never-committed reordering) surfaced a third, further-unrelated defect: the whole-workspace self-compile's emitted output includes at least one entry whose content is not valid Rust (a parse failure on [package]-shaped content, consistent with a Cargo.toml being routed through the Rust-target emit/write path), which aborts the tree write partway through and produced a partial, non-representative candidate tree. All three of these are pre-existing defects in required-regen/compile_stage0 infrastructure, orthogonal to the where-refinement fix in this PR, and outside this PR's ownership (required_regen_host.rs, trait_bound_witness.dag, and compile_stage0/compile_sources internals are required-regen: the population gate compared two key spaces and refused vacuously on every run #8518's territory). No changes to those files are part of this PR — both were touched only via local, uncommitted, immediately-reverted diagnostic patches during investigation, confirmed via git status/git diff --stat HEAD to leave a clean tree matching this branch's committed HEAD.

What verification WAS achieved, honestly stated: the fix compiles and typechecks as .dag source; the 38-test witness suite (including the new depth-2/depth-3/wrong-kind-literal specimens) is proven correct by direct code-path tracing of the fix against peel_where_refinement_base/where_refinement_chain's existing, unmodified, already-generic recursion, and against the exact Absent-conflation each fix closes; and the tests execute today against the currently-built seed binary's compile-clean pipeline (pre-fix, establishing the regression baseline the depth-2/3 reds document). What was not achieved: witness-suite execution against a binary that has the .dag fix regenerated into its compiled Rust — that step is blocked on the three infrastructure defects above, is not achievable without unbounded scope creep into required-regen/compile_stage0 repair (outside both this task's brief and #8518's already-claimed ownership), and is disclosed here rather than silently omitted, per DESIGN.md §4b's rung-honesty requirement (the reported rung must equal the rung established by executed evidence — this PR does not claim a full-regen green that never executed).

No generated src/v1/stage0/src/*.rs files are part of this commit; that is deliberate and matches the above — landing hand-edited or partially-regenerated Rust here would itself be an unmodeled realization / manual-application-committed-as-source violation (DESIGN.md §6).

[gunbai-bot]

Already disclosed in the PR body under "Verification limitation — disclosed": the stage0 Rust seed regen is blocked on two pre-existing, unrelated required-regen infra defects (population-reconciliation gap owned by smart-ram-730's gunbc#8518, plus a write-ordering bug and a non-Rust-content emit defect found independently this session). No hand-edited or partially-regenerated Rust is included here on purpose — landing that would itself be a manual-application-committed-as-source violation (DESIGN §6). Once #8518 lands, regenerating stage0 to close this fixed point is a mechanical follow-up, not new design work.

— sent from snappy-seal-402