Refuse kernel scalars at applied type applications

[gunbai-bot]

Closes the shallow-totality blind arm where a non-numeric kernel literal can reach an applied expected type’s compatibility fallback without any premise proving inhabitance (for example, List<Int> receiving a String literal).

This does not peel through applications. It models compiler-domain head exposure as an honest coproduct over the states the implementation actually produces, preserves the outer constructor and every argument identity, and directs non-numeric literal checking by expression form. Target realization is deliberately not consulted.

Numeral introduction is deliberately outside this PR. A full-floor measurement of the earlier combined implementation produced 2,210 refusal sites across existing numeral-bearing carriers, proving that numeral introduction needs its own identity census, authority rows, and enforced landing. The integer judgment, its rows, and its controls were removed together; no modeled-but-unenforced numeral machinery remains.

The exposure census is cached per declaration identity in SymbolIndex. The .dag authority and generated seed mirror are updated together.

Enrolled substrate-only controls cover:

• String literal at List: refuse
• List literal and concat(List, List): accept
• wrong String list element: refuse recursively
• String at std Nat’s applied head: refuse

The concat control is a live corpus specimen from the rejected scalar-only wall: the synthesized shape at the old seam had lost the expression-form premise and could not distinguish a conforming List-producing call from a String literal.

Validation:

• cited-symbol whole-corpus census passed on 3385e5b after use-site head precedence and authored-formal selection
• full required CI on 16b0fb7 passed before the review-scaffolding cleanup
• neutral-seed required regeneration completed after the split and after the cleanup; emitted mirrors installed verbatim
• git diff --check
• pre-commit and pre-push cargo fmt --all --check

The 2,210 figure is a refusal-site count, not a distinct-carrier count and not a final population. The distinct declaration-identity census will be measured on a tree containing #9031 for the numeral follow-up.

[gunbai-bot]

Numeral follow-up evidence carrier: commit 3385e5bfbaa4d2f0d4a8ce7c46b25de82e70bd92 (equivalently c177c149264^) contains the deleted std-Nat numeral positive control and v2 Peano-Nat discriminating red. The follow-up must recover those exact controls by SHA and re-enroll them with the identity-keyed rows and enforced judgment in the same landing; they are not to be reconstructed from memory. — sent from stern-lynx-526

[gunbai-bot]

Addressed review 55417 in deaa9c8: removed the prose-as-data model note, removed the unproduced representational parameter-relation axis (including its constant nominal plumbing), and removed the unreachable cyclic exposure arm. The model now names only exposure states and data that the implementation actually produces; the .dag authority and generated seed mirror were regenerated together. — sent from stern-lynx-526

[gunbai-bot]

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

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

• dag/test/claim/direct_call_argument_type_witness_test.dag
• src/v1/04_env.dag
• src/v1/04_infer.dag
• src/v1/stage0/src/emitted_population.rs
• src/v1/stage0/src/lib.rs
• src/v1/stage0/src/v1_compiler_infer_env.rs
  ... and 1 more

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)