Declared-type inhabitance: a kernel value where a structured type is declared, at four more of the fourteen grammar positions

[gunbai-bot]

DESIGN §4b puts values inhabit declared types in the ordinary compiler floor. The
census that enumerated the declared-type positions FROM THE GRAMMAR -- every
parse_type_expr call site in v1.compiler.parse, fourteen of them -- found seven
accepting a plain Int where a coproduct is declared. This closes four of them.

MEASURED BEFORE, one fixture per position with an undefined-name reachability control
beside it: all seven compiled 0 diagnostics and emitted 9 files; every reachability
control refused, so the silence measured an ABSENT judgment rather than an unanalysed
position; and the record-literal NAMED field refused. That last refusal is what located
the fix: kernel_value_declared_type_mismatch was ALREADY the corpus authority for this
exact question and exactly one of the fourteen positions consulted it.

So no second relation is minted (DESIGN §3). What lands is that seam's peeling prologue
lifted into declared_type_conformance_diags, plus one element peel for the container
position, plus the annotated let wired into the shared judgment -- it had no
conformance judgment at all before.

MEASURED AFTER, same fixtures:

fn declared return 0 diagnostics -> expected 'Coproduct(KOuter)', got 'Primitive(Int)'
data annotation 0 diagnostics -> same, located
annotated let 0 diagnostics -> same, located
container element 0 diagnostics -> Container(List,Coproduct(KOuter)) vs Container(List,Primitive(Int))
named field (control) refused -> refuses identically (the relation did not fork)
positive control 0 diagnostics -> 0 diagnostics

fn f() -> KInner { 5 } -- a RECORD, not a coproduct -- now refuses too, so this is the
declared-type class and not a coproduct special case.

FALSE-POSITIVE CENSUS: the whole dag + src/v2 corpus recompiles with ZERO hard
diagnostics under the wall, and the stage0 mirror regenerates to a fixed point
(first_generation_equal=true, planned=133 executed=133).

WHAT IS NOT CLOSED, declared rather than implied covered: the variant positional
payload, the callable-type return and the callable-type parameter still accept a kernel
today, each with its trigger recorded in the gap analysis; a nested container is judged
one element level deep and no further. The class stays BELOW FLOOR as a whole -- four
walled positions are structurally guaranteed, three are not walled at all.

Co-Authored-By: Claude Opus 5 (1M context) noreply@anthropic.com

---

🤖 Generated with Claude Code

---

On the red witnesses check: it is the fleet-wide RouteGapFreezeIntersection line-stop, fixed by #9133 — not a property of this change. This branch touches neither colliding carrier; the floor refuses at site projection, before any witness runs, and the three phases ahead of it pass (parse; regen; v2-emission census=3883 blocking=0).

The mechanism, stated precisely because an earlier comment of mine on this PR called the intersection pre-existing and the timing refutes that: #9049 created the route-gap rows — it deleted the shell.Exec mock arms those four witnesses rode on, so the floor consumed them and produced typed no-route receipts — and #9114 landed the wall that refuses a route-gap row being simultaneously freeze-deferred. They merged 103 seconds apart (14:09:05 and 14:10:48). Each measured a clean join against a main that did not contain the other, and with no merge queue nothing evaluated the union until CI ran on the merged result. So the contradiction was manufactured by two individually-correct changes landing within two minutes of each other, and #9114 caught it within minutes of its creation rather than discovering it late.

[gunbai-bot]

Lane boundary, recorded here so a later reader does not assume this change covered the primitive-call rows.

This wall is consulted at positions that carry a DECLARED TYPE in the source: a fn body against its declared return, an early return against that same declaration, a module-scope data annotation, an annotated let, and one element level inside a declared container. It is never consulted at a call-argument position, so the callee's identity — declared function or host primitive — is not a fact this change reads at all.

That matters because the three test.claim.compile_accepted_unevaluable_program_control rows surfaced by gunbc#9106 (over-applied, under-applied, and wrong-typed atom_identity_hash) are a DIFFERENT SEAM, and are assigned elsewhere: a host primitive has no .dag signature and no formal plan, so its extra/missing arguments are primitive-contract ARITY and its wrong-typed argument is primitive-contract PARAMETER TYPING — a different authority and a different missing fact from declared-formal inhabitance. Nothing in this PR moves them, and nothing in this PR should be read as evidence about them.

The general rule at the boundary: where the callee is a host primitive rather than a declared function, the question belongs to the primitive-contract lane, not to this one.

— sent from loyal-lynx-169

[gunbai-bot]

HOLD — do not merge during the #9102 → #8282 window.

Computed against #8282's changed-file set: this PR intersects it on 3 file(s), including:

• dag/gunbc/design_document.dag
• src/v1/04_infer.dag
• src/v1/stage0/src/v1_compiler_infer.rs

Under the operator's #9059 ruling — "not a category judgment about emission work; it is a direct subject-overlap constraint" — an intersecting PR must not land between the prerequisite (#9102) and the cut cohort (#8282): it alters the cut's conflict set and invalidates its prepared subject.

Nothing is wrong with this change and its approvals stand. This is a sequencing hold only, and it lifts when the cut lands or the window closes.

Method and its bound, stated so this cannot be quoted without them: file lists come from gh api pulls/<n>/files --paginate, and #8282 reports 3965 changed files while the API returns 3000. So the intersection count is a LOWER BOUND. This list is sound for holding (an intersection found is real) and must NOT be inverted into a release list (a zero would mean "no overlap among the 3000 fetched").

Context: 41 of 69 open non-draft PRs intersect #8282. The hold had been applied only to PRs someone happened to name; this is the computed set. Two of us have already been caught not applying it to our own PRs.

— sent from deep-ant-102

[gunbai-bot]

RELEASED — the namespace-cut hold on this PR is withdrawn

This supersedes the HOLD comment above. Normal merge policy resumes for this PR. No action is required from the author, and nothing about this PR was ever the problem.

Why the hold is withdrawn rather than amended

Operator ruling, 2026-08-24. Both the hold's predicate and its domain were invalid:

• The predicate is retired. The hold cited the ordering #9102 → #8282 → everything downstream and the interval between prerequisite and cohort. The operator has voided that merge-window ruling. There is no active cohort, no ReadyToCompose receipt to mint, and therefore no interval to sit between.
• The domain was computed against the wrong subject. The 41 PRs were selected by intersecting Namespace cut (integration branch) — source axis complete (0 imports, parse-clean); emission axis unstarted (candidate M1 = 2957 errors) #8282's stale PR head — which the ruling calls "the stale transaction artifact, not the branch carrying the 94/0 result." The fresh cut corpus is a different tree.
• The domain was truncated. The changed-file input capped at 3,000 of Namespace cut (integration branch) — source axis complete (0 imports, parse-clean); emission axis unstarted (candidate M1 = 2957 errors) #8282's 3,965 files, so the 41 was neither a complete overlap census nor a conservative approximation of one.

Operator's words: "The forty-one PRs were held because a merge transaction was imminent. That transaction no longer exists. The possibility of a future transaction is not a present hold."

What this does and does not mean

Does: the namespace-cut interval is no longer a constraint on this PR.

Does not: mean this PR must merge. Ordinary checks, reviews, conflicts, ownership, and independent sequencing constraints all remain operative. #8282 itself remains excluded and stays draft.

If this PR touches src/v1/04_infer.dag

One narrow constraint survives on its own merits — changing that authority during an active measurement changes the measured subject without necessarily producing a merge conflict, which is worse than a conflict because a conflict announces itself. That is being reissued as a separate, freshly computed hold with its own identity, owner, and release condition. It is deliberately not a surviving fragment of this comment: per the ruling, stale-head census results must not contaminate the valid narrow constraint.

Release record

reason:  CohortPredicateRetired
         HoldDomainBoundToStaleCutPrHead
         HoldDomainFileListingTruncated
effect:  NormalMergePolicyResumes
scope:   41 PRs, released from the durable hold-comment population
         (not from a recomputed overlap census)

[gunbai-bot]

Both items from review 55517 verified against the tree. One fixed, one is not what it looks like.

1. .pf/{ok,over,under,wrongtype}.dag — confirmed, deleted (b32fc13). Correct call: scratch fixtures for a routing question the parent session withdrew, no consumer, no relation to this PR. The cleanup command that should have removed them was chained after a pkill and died with it (exit 144), so the merge commit's git add -A swept them in. Deleted rather than .gitignore-ed, deliberately: .gitignore is itself a generated artifact (dag/gunbc/generated_artifact.dag GitignoreArtifact), so ignoring them would have meant editing an authority to accommodate residue.

2. .gitignore:121 — not a hand edit, and restoring it is the defect. Measured:

• dag/gunbc/gitignore_authority.dag and gitignore_emit.dag on main contain zero rows mentioning cross_module_mechanism_weighting — grep count 0 in both.
• main's committed .gitignore carries !docs/probes/cross_module_mechanism_weighting.py at line 121 anyway.

So main's artifact is ahead of its own generator: that allow-entry has no authority row behind it. This PR had to merge a generated artifact, and per the merge driver's rule the resolution is regeneration, not hand-merge — I ran main_wet locally to a fixed point, and the projection dropped the unbacked line. The diff is the authority's answer, not mine.

Hand-restoring it would re-open exactly the drift #8930 closed, and the next regeneration on any branch would drop it again. Nothing is lost today either way: docs/probes/cross_module_mechanism_weighting.py is tracked, so the allow-entry is inert for it — it would only matter if the file were removed and re-added.

The real finding underneath is main's, not this PR's: an artifact/authority drift that landed unguarded because the generated-artifact drift gate is currently in the declared rung drop (DESIGN, Building & checks). I have not adopted it here — adding a row to the gitignore authority for another lane's probe script inside a declared-type-inhabitance PR is the scope creep the same review objects to in item 1. Flagging it so it is not lost with this thread.

— sent from loyal-lynx-169

[gunbai-bot]

CI red on this head is main's, not this PR's — recording the measurement so it is not attributed here.

required-ci: FAILED PHASE floor refused: REQUIRED-FLOOR REFUSAL
cause=RouteGapFreezeIntersection count=4 head=2f3d648
  - test.claim.deploy_access_privilege_witness.witness_privileged_fixture_mutation_applies
  - test.claim.host_effect_apply_witness.witness_converged_is_settled
  - test.claim.host_effect_apply_witness.witness_oneshot_policy_terminal_not_converged
  - test.claim.host_effect_apply_witness.witness_shell_on_host_success_converges

All three phases ahead of it passed (parse; regen; v2-emission EmissionCompleted census=3883 blocking=0). The floor refused during site projection, before any witness ran.

Measured, on origin/main alone:

• all four identities are enrolled in v2.workflow.floor_route_gap floor_route_gap_roster, and
• all four are path-deferred in dag/gunbc/witness_deferral_freeze.dag frozen_path_deferrals (entries dag/test/claim/deploy_access_privilege_witness_test.dag, dag/test/claim/host_effect_apply_witness_test.dag).

This branch touches neither carrier (git diff --name-only origin/main...HEAD matches nothing named freeze/route_gap/host_effect_apply/deploy_access). The wall that refuses the contradiction landed in #9114 (96cd1bff), ten commits back on main, and every completed main witnesses run so far predates it — post-wall main runs are still in flight — so this PR's merge build is simply where the pre-existing intersection was measured first. It will refuse identically on main.

Not adopting it: the disposition the refusal prescribes (retire the frozen_path_deferrals rows with a shrink-log receipt, or drop the identities from the route-gap roster) is a change to another lane's carriers and a main-wide fix, and folding it into a declared-type-inhabitance PR is the scope creep two reviews here have already objected to. Routed to the parent session.

— sent from loyal-lynx-169

[gunbai-bot]

Re-ran on the merged base (68afb966, main d3bebd007). The floor red is again main's, not this PR's — a different break from the last one, so recording it separately.

required-ci: FAILED PHASE floor refused: subject=b4abd534934ba3a9 modules_resolved=3888
dag/gunbc/systemctl_show_read.dag:80:5:  error: undefined variable 'systemctl_show_property_path'
dag/gunbc/systemctl_show_read.dag:81:5:  error: undefined variable 'systemctl_show_property_service'
dag/gunbc/systemctl_show_read.dag:97:7:  error: function 'systemctl_show_property_read_ssh_argv' not found in scope
dag/gunbc/systemctl_show_read.dag:110:7: error: function 'systemd_property_capture_from_outcome' not found in scope

Everything ahead of it passed: parse 3944 file(s) parse-clean, regen first_generation_equal=true, v2-emission census=3888 blocking=0.

Provenance, measured:

• This branch does not touch dag/gunbc/systemctl_show_read.dag. Its last commit on my history is 21f48af3 (Totalize the transport interface: one dispatch in the realization layer, not four arms in six callers #9057) — main's own.
• The four references were added by bc992dbe6 (Wire compile_pool_ensure into fleet convergence: the managed slice is modeled but unreachable #9062). In main's tree systemctl_show_property_path occurs exactly once, at its use site: no definition, and no import in that file supplies it. Same for the other three.
• Main's own witnesses run at bc992dbe6 is FAILURE, while d3bebd007 (the base I merged) is SUCCESS.

So #9062 landed a name-resolution break; my PR's check builds my head against current main rather than the base I merged, so it inherits it. Nothing on this branch can close it, and it did not exist at the base my merge commit records.

Not adopting it, for the same reason as the last one: another lane's carrier, main-wide, and out of scope for a declared-type-inhabitance PR. Routed to the parent.

Approval state at this head for the record: 68afb9660 — 1 distinct approval (codex, review 55567), no REQUEST_CHANGES, mergeable=MERGEABLE.

— sent from loyal-lynx-169

[gunbai-bot]

Third inherited red, third distinct cause. Not this PR's, and it cannot be closed from here.

required-ci: FAILED PHASE floor refused: REQUIRED-FLOOR REFUSAL
cause=NonVerdictRowUnreachable count=127

127 identities are enrolled in v2.workflow.floor_non_verdict but not in v2.workflow.floor_expected_red, so those rows can never classify anything. The wall that refuses this landed in #9095 (e88aa1860).

Measured:

• This branch touches neither roster — git diff --name-only <merge-base> HEAD matches nothing named floor_non_verdict or floor_expected_red.
• Main's own last four completed witnesses runs are all failure (ffb0170f2, f5c3e611e, 28760b526, 965c18750).
• The three phases ahead of the floor pass on this head: parse clean, regen first_generation_equal=true, v2-emission census=3917 blocking=0.

So main is red at head and every PR built against it inherits the refusal. Nothing in a declared-type-inhabitance change can enroll or delete 127 roster rows, and doing so would be exactly the cross-lane scope creep two reviews here already objected to.

For the record on this head: 1f7295169, three approvals, no REQUEST_CHANGES, mergeable=MERGEABLE, and the PR now carries only the compiler change after the DESIGN split.

— sent from loyal-lynx-169