Genericity is declared, not inferred from a failed lookup

[gunbai-bot]

The state this refuses

At the census-borrowed declaration route, absence from a lookup was standing as positive evidence of generic ownership — and the environment that lookup consulted has no bindings at all, so the evidence was unconditional rather than occasional.

v1.compiler.env census_declaration_type_env builds bindings, str_bindings, ancestry_str_bindings and intern_table as empty maps, seeded only with the declaration's type-parameter bindings. In that environment lookup_binding_by_name_local can only ever find a tp_name. Two sites read a miss there as "this leaf is a generic":

• v1.compiler.lookup declaration_unbound_leaf_names — results concatenated into the generic-name roster;
• v1.compiler.env declaration_substitution_basis — second disjunct, the same test again.

So for every census-borrowed declaration, every unqualified non-kernel concrete type name in every parameter was enrolled as a generic parameter of that declaration and stamped TypeVariable { id: <its own name> }. Always, not sometimes.

Why that is a floor defect

v1.compiler.infer direct_call_argument_inhabitance_diags selects the substitution basis as the declared side whenever it carries an unbound type variable, and declared_type_inhabitance reads that stamp as a generic formal and declines with UndecidableGenericFormal. A value of any constructor reaching a NonEmptyStr or a HostIdentity position was therefore admitted in silence — not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran.

DESIGN §4b puts "values inhabit declared types" in the ordinary compiler floor, and §5 names this shape exactly: unable to resolve, so widen to "generic", so decline. The absorbing arm destroyed the only signal that would have made the deficit rank.

The authority was already in hand, one field over

v1.compiler.lookup borrowed_census_callable_candidate computes borrowed_generic_param_names on its first line and classifies the return type of that same declaration positively with it, through qualify_borrowed_type_names: roster members stay variables, every other bare leaf resolves to its owner module and is qualified. The parameter types, in the next field of the same record literal, went through the guess.

One question, two answers, inside one record literal — DESIGN §3. The parameter side now consumes the same roster, and the absence disjunct is deleted from both sites together, because they were one classification authority written twice.

Scope, deliberately narrow: only the roster moves. declared_type stays param_node_type_expr. Routing it through qualify_borrowed_type_names as well would change the name every consumer of ResolvedFormal.declared_type reads — and one of them, direct_call_generic_type_argument_inhabitance_diags, compares authored_name_at of the declared node against the actual's for equality. That is a second, wider claim, and a population delta after it could not be attributed to this one. If the judgment turns out to need qualification to reach Inhabits on a bare-declared / qualified-produced pair, it returns as its own PR with its own justification.

The roster reads a declared fact, not a naming convention

v1.compiler.parse parse_optional_type_params mints, for each name in the angle-bracket clause, one param whose name and whose type-expr name are that name. The <...> clause has no other carrier. A search for an authored parameter of the form Name: Name across src/v1, src/v2 and dag matches nothing, while fn f<T>(...) matches throughout std — so the spelling this roster recognises is not hand-authorable in the corpus and exists only where the parser minted it from a declared generic clause. fn_type_param_names and param_is_generic_decl already read the same encoding; this adds a fourth reader of one fact, not a second fact. (Consolidating those readers is a real §3 item and deliberately not opened here.)

Cost

The obvious alternative — keep the absence test but consult the census-backed lookup_binding_by_name — is refused on shape, and the shape argument needs no timing: it drags listed_import_required_bare_call_blocked, the global-bare ambiguity list and the nearest-ancestor containment walk onto every leaf of every declaration, where the roster route is a map lookup against a roster already computed for the sibling field. DESIGN §6 bare-minimum-cost refuses the first shape independently of the semantic argument, and the cheaper path is also the correct one — the usual direction when a heuristic is replaced by the fact it was approximating.

(An earlier draft of this paragraph cited a wall-clock figure for that alternative. It is withdrawn: the run that produced it compiled stale stage0 mirrors, so it measured a compiler that did not contain the change. No number is cited here in its place.)

Producer census: is the parser the only site that can mint name == type-expr name?

The source-shape reading above says what nobody has written; the claim the repair depends on is what nothing can produce. make_param_node has twelve call sites (thirteen matches, one the definition), and every one is classified:

producer	can it mint pname == tname?
parse.parse_optional_type_params	yes, by construction — the intended and only structural producer
types.algebra_method_field and the two callable-type builders (×3)	no — name is the literal "_"; would need a type named _
parse at the two name: "" sites (×2)	no — excluded by the pname != "" guard
infer fold-signature params (×2)	no — fixed names acc / elem against computed types
parse record-field → param (×2)	only if an authored field is spelled Name: Name
parse authored value params (×2)	only if an authored param is spelled Name: Name

The last four are authored-dependent, and both authored shapes were censused across src/v1, src/v2 and dag: zero occurrences of a parameter or a record field whose name equals its type name.

So exactly one producer mints the shape structurally; the rest are either name-excluded by construction or need an authored spelling that does not occur. Stated at honest rung: for the eight structural producers this is structurally impossible (§4b(4)) — the shape has no constructor there. For the four authored-dependent ones it is mechanically preventable at best: an author who writes fn f(Vendor: Vendor) would have that parameter read as a generic. That is a pre-existing property of the parser's encoding, shared by all three readers of it below, and is neither introduced nor climbed here.

Recorded §3 fork (not opened here)

Three readers test one fact — "is this param the parser's encoding of a generic clause?" — with three separate predicates:

• v1.compiler.resolve fn_type_param_names
• v1.compiler.infer param_is_generic_decl
• v1.compiler.env borrowed_generic_param_names (the one this PR routes the parameter side through)

They differ in detail (param_is_generic_decl additionally admits a type-expr already stamped a variable). One fact, three tests, is a §3 fork; it is known and deliberately unwritten here so this cut stays one cut. Recording it so the next person to touch any of the three does not re-derive this analysis.

Declared boundary (§4b(2)) — it refuses where it cannot decide

The roster is the declaration's own generic clause. A synthesized or member declaration that borrows an enclosing owner's generic without restating it is not on that roster, so its borrowed leaf stays bare and reaches the judgment with a declared name that resolves to nothing — reported UndecidableFormalUnresolved.

That is the correct disposition, not a gap: the position genuinely is not judgeable from what the declaration carries, and the reason names precisely that. The change refuses where it cannot decide instead of guessing, which is the whole point of it — the state it replaces claimed genericity it could not demonstrate. Next-rung trigger, at capability grain: an owner-generic carrier on the borrowed declaration. Not a census and not a fixture — the carrier.

This PR does not claim the roster is exhaustive over every generic a declaration could mention.

Measured

Re-derived on the current head. Every earlier figure in this body is SUPERSEDED, including the previous "final-head" table: the tree has since taken another origin/main merge and eight commits, and a number that outlives its base is not evidence.

Construction. Same corpus on both halves, same instrument, two binaries differing only in the three stage0 mirrors — the before half built from origin/main's v1_compiler_infer{,_env,_lookup}.rs, the after half from this branch. Both built locally and frozen outside target/ before running. Vary the compiler, hold the corpus.

Transition matrix over site identity (module, span):

from	to	sites
UndecidableGenericFormal	no diagnostic	8425
UndecidableGenericFormal	unchanged	5097
no diagnostic	UndecidableRefinementIntroduction	4944
UndecidableOptionalCarrier	unchanged	1970
UndecidableProducedIdentityErased	unchanged	881
UndecidableGenericFormal	UndecidableProducedIdentityErased	103
UndecidableGenericFormal	UndecidableRefinementIntroduction	45
DeclaredTypeNotInhabited	DeclaredTypeNotInhabited	7
UndecidableFormalUnresolved	unchanged	6
no diagnostic	UndecidableRefinementPeerChains	5
no diagnostic	UndecidableGenericFormal	1

The refusal set is identical BY IDENTITY: the same 7 sites before and after. No refusal gained, none lost. This diff removes a fail-open without adding a single refusal the corpus did not already carry — and that fact does more work in this PR than any other, because it is what answers the freeze question below.

The reason split is visible in the matrix and it was not cosmetic. 5 sites report UndecidableRefinementPeerChains and 4944 report UndecidableRefinementIntroduction. Before the split those were one bucket of 4949 filed under a label saying they were introductions, 5 of which are not. Small, and exactly the population that would have been silently carried past the next climb.

Rung-honest statement. This does not climb the class: no previously-accepted invalid site newly refuses.

False generic classification is removed; the underlying inhabitance deficit remains non-blocking but is now typed, located and enumerable.

The −8425 is not permitted to do rhetorical work the +4949 contradicts.

Every off-diagonal cell, characterised rather than counted:

• The 8425 are the repair: declared types classified as the declaration's own generic parameter because a local-only lookup missed them.
• The 103 are an exhaustive join: all 103 came from UndecidableGenericFormal and none from any other disposition. With the declared identity restored the judgment progresses further and finds the produced identity genuinely unavailable — each a bare identifier bound by a match pattern or let. The next honest deficit, exposed rather than introduced.
• The 4944 and the 5 were silently accepted before, on the local-declaration route that was never stamped. None of them refuses.
• The 45 had their false generic classification removed and then reach the refinement question, declining there instead — a move between two non-blocking dispositions.
• The 1 is a single site in v2.lens.unused_parameters at the generic type argument seam, adjacent in the same call expression to a formal whose false classification this repair cleared. A different seam, not a re-appearance.

One instrument defect found in my own controls, and it generalises

All six controls enrolled in the previous head were false, and they were false for a reason worth stating rather than quietly fixing. violation_count reports every row of the class in the whole census, not the fixture's contribution — the counts run to thousands — while the literals I asserted (== 1, == 0) were copied from a probe delta. That is exactly the shape DESIGN §5 refuses: a merge-blocking test comparing a live population to a numeric literal not grounded in a controlled fixture. They did not merely have wrong numbers; they were comparing two different quantities.

The repair generalises: each arm is now a PAIR of fixtures differing on exactly one axis, so the shared corpus contribution cancels and only the axis is measured. Anyone authoring a witness against a census will reach for the same wrong literal, and the pair form is the answer.

Enrolled controls

No enforcement RED is owed, because no enforcement climb is claimed. An earlier draft carried one — a previously-accepted unrelated-constructor site must newly refuse — and it is retired, not satisfied. Forcing it would make this PR solve the separate literal-introduction question merely to justify the story about why it existed, and an unmet acceptance control in a merged body is worse than none: the next reader takes it as met.

What is owed is a discriminating RED for the classification repair. All five arms below were measured live on this head, and all six of their predecessors were observed RED under the real floor harness before the oracle repair — so they discriminate in the direction that matters.

control	asserts (pair oracle)	discriminating mutation
w_a_concrete_declared_leaf_is_not_classified_generic_through_the_census	sha256_digest_wire_form(digest: Sha256Digest) == a fixture with no call	restore the local-miss classification in either deleted site → stamped TypeVariable { id: "Sha256Digest" } → the pair separates by one
w_a_branded_refinement_at_its_own_declared_base_inhabits	declared NonEmptyStr ← produced HostIdentity: 0 refused, and == its exact-match partner	revert the where-refinement exclusion → refuses, as it did at two live corpus sites
w_two_distinct_brands_over_one_base_are_not_refused_twice	0 refused, and > its exact-match partner: this relation declines, the existing brand wall refuses	measured at the direct-call argument seam, not assumed from the cast path
w_a_nominal_opaque_alias_does_not_ground_through_the_refinement_chain	Secret does not ground to String (1 refused)	follow a nominal_opaque alias in the chain → sibling pair
w_a_bare_literal_at_a_refinement_formal_declines_and_a_cast_one_does_not	bare literal > cast form	separates "we surfaced the introduction question" from "we made every refinement pair undecidable"

The positive census arm is withdrawn because its RED is not authorable

The sixth control was to assert that a declared generic clause is still classified generic through the census route. Measured: that fixture contributes zero rows of the class — equal to a fixture with no call at all — so the seam emits nothing there whether the classification is right or wrong. An arm asserting one is false; an arm asserting zero is green by construction and would later be cited as coverage of something it never measured. DESIGN §4b says to ask whether the RED is authorable before writing the check, so the arm and its now-dangling fixture are removed rather than enrolled as a decoration.

The cause is a harness boundary, not a fixture shape. src/v1 is not a --source-root in any workflow, so no witness under the required floor can observe declaration_substitution_basis's output at all; dag/test/claim/checkpoint_identity_keying_witness_test.dag records the same boundary and exists to work around it black-box. That makes this a §4b missing-harness case, which is a next-rung trigger and explicitly not a permanent ceiling.

Trigger, at capability grain: a floor-executable surface that can observe the substitution basis's classification — either src/v1 on a floor source root, or a black-box seam that renders the stamp distinguishably.

The residue, stated precisely. What is measured is the removal of a false positive, which the negative arm measures directly and discriminatingly. What stays unmeasured is the survival of the positive authority — that a genuine declared generic is still classified as one. The roster union below makes that considerably safer by construction; construction is not evidence, and this body does not blur them.

Review finding taken: the roster is a union again

Deleting the absence disjunct was the repair. Replacing fn_type_param_names with borrowed_generic_param_names alongside it was a second, uncontrolled change, invisible to every control enrolled at the time. The two predicates are not the same — the borrowed roster is wider on one axis and narrower on two, dropping any declared type param whose type expression is not a childless NoConnective leaf — so such a param would have been reclassified as a concrete unresolved name: the exact failure the negative control exists to prevent, arriving through the other door. declaration_generic_names is now concat(tp_names, map_keys(borrowed_generic_param_names(...))), which is what the pre-repair code passed. Only the absence disjunct is deleted. (Review finding, tidy-lynx-804, 2026-09-07.)

I took the union rather than measuring the two predicates for agreement: the union is correct whether or not the sets agree today, so measuring to license a narrowing that is not needed is work priced against elegance (§6).

Admission under the v1 freeze (gunbc.v1_maintenance_standing v1_seed_standing)

This PR changes the frozen v1 seed, so it owes an admission argument, and this section is it. §3's frozen-X carve-out reclassifies v1 as semantics-frozen with maintenance active under a PURPOSE test — a change is admitted when it serves the v2 self-host program — with five refused classes that DOMINATE every admission. The whole diff's source change is in src/v1, so the question is live and was not answered in earlier revisions of this body.

The admitted instance is DefectRepairDiagnosticsMayMove, and the standing draws the line in exactly the terms this change needs: the seed doing something INCORRECT is admitted, repair it, diagnostics may move; the seed FAILING TO DO something it never did is SeedFeatureCompletion, refused. The producer repair is pinned to a specific incorrect behaviour the seed exhibits today, evidenced rather than asserted: a lookup miss against an environment carrying no bindings was read as positive evidence of generic ownership, unconditionally on the census-borrowed route, and 8411 sites are measured moving off that misclassification.

The self-host connection is direct, and it is a measurement rather than a claim: v1 COMPILES v2. Partitioning the moved population by source root:

population	total	in src/v2
cleared false-generic	8425	3707 (44.0%)
advanced to UndecidableProducedIdentityErased	103	98 (95.1%)
refinement introduction	4944	223 (4.5%)

The compiler that builds v2 was overwriting the declared identity at 3707 positions in v2's own sources and admitting any constructor there in silence. That is not a downstream benefit of a seed improvement — it is the self-host program's own files being mis-judged today, so repairing it meets the purpose test at its centre rather than at its edge. The 95.1% is the sharper figure: the population where the judgment now gets far enough to find the produced identity missing is almost entirely v2.

The lane is compiler-guarantee — "the DESIGN §4b ladder climbs" — not v1 exit. A reviewer reading only the v1-exit lane sees lines added to the thing being exited, which is why the lane is named here.

And the seam has no v2 counterpart, so "fix it in v2 instead" is not an available option. Derivable predicate rather than an assertion: lookup_binding_by_name_local, substitution_basis and declaration_unbound_leaf_names have zero occurrences anywhere under src/v2 (they occur only in src/v1). Anyone can re-run that at any later head.

The hardest objection, taken at its strongest

A reviewer applying the refusal precedent — the lane refused as SeedFeatureCompletion for authoring OperatorSpec/TypeCheckpoint rows so the emitter could render constructs it has no row for — could reasonably say that a new inhabitance relation with a new type and two new verdict reasons is NewLanguageBehavior. That is the right objection to raise and it deserves a measurement, not an assurance.

It is answered by the refusal set, which is identical by identity: the same 7 sites before and after. The diff adds no refusal and removes none. Nothing the seed accepted is now rejected, and nothing it rejected is now accepted — so there is no new language behaviour to speak of. What changes is why a non-blocking decline is reported: one coarse reason that was frequently FALSE is replaced by reasons that are true, and the widening arm restores to Inhabits a pair the pre-repair seed also admitted (silently, for the wrong reason).

And the relation is not optional garnish on the repair — it is the repair's integration closure. The producer fix, landed alone, makes the seed newly REFUSE correct code: with the declared identity restored, declared NonEmptyStr <- produced HostIdentity refuses at live corpus sites. Shipping that would be a wrong-closed diff, which §5 makes a hard reject. So the relation exists because the admitted repair exposed a false refusal, and it earns admission on the same instance rather than as capability sought for its own sake. The distinguishing test is the refused-class one: this adds no capability the seed did not already claim — it removes a fabricated judgment and refuses to fabricate its replacement, declining where another authority already decides rather than minting a second one.

What would have made me stop. If the relation had needed to decide pairs the seed never claimed to decide, or had added a refusal the corpus did not already carry, it would be seed capability and I would have said so rather than argued it. The refusal-set identity is what distinguishes those cases, and it is measured on the final head rather than assumed.

The relation fires — proven, because making it unavailable on a miss is exactly the failure that hides

The chain is now discarded whenever any link fails to resolve. A fail-closed collapse is the safe direction, which is precisely why it can hide: if every chain collapsed, the relation would be permanently unavailable — never wrong, never right, never firing — and that is the inert check DESIGN §4b calls worse than absent, because it gets cited as coverage.

Measured on this head, counting emitted reasons over dag + src/v2:

reason	sites
UndecidableRefinementIntroduction	4989
UndecidableRefinementPeerChains	5
DeclaredTypeNotInhabited	7 (unchanged)

Both arms reach verdicts, and the peer arm is inhabited rather than being a variant nothing produces.

The widening arm is proven by an enrolled control, and the mechanism matters. w_a_branded_refinement_at_its_own_declared_base_inhabits asserts NotInhabited(widening) == NotInhabited(exact-match partner). If refinement_inhabitance returned Absent for every pair, the widening pair would fall through to the now-unblinded nominal-product arm, which refuses NonEmptyStr against HostIdentity as distinct constructors, while the exact-match partner would not refuse. The equality breaks and the control reds. It is green, so the relation is reaching RefinementWidensToDeclaredBase and admitting.

That property is new: while the product arm was blinded, a dead relation would have produced 0 == 0 and passed vacuously. Removing the blinding is what turned a control that could pass while the relation was dead into one that cannot.

A review-originated finding that moved to its own PR

Review 62172 reported that a where-refinement exclusion added here reopened a refusal for disjoint pairs — a branded refinement at a true product formal. The conclusion was right and the cause was not: measured on both sides, with two compilers differing only in the three stage0 infer mirrors, that pair is unrefused under origin/main as well. The defect is pre-existing and is not this diff's.

It is therefore enrolled in its own PR — #10817 — as a discriminating control, an ExpectAssertionFalse admission and a recurring_failure_mode row, on the rule that a review-originated finding moves to its own PR when its discriminating RED reproduces on main without the reviewed diff. Discovery provenance is recorded here; implementation ownership follows the demonstrated subject. This PR deliberately keeps no second copy of that control — two owners for one property is the fork this project spends its time removing.

The where-refinement blinding is still removed here, on its own merits: it was unnecessary, since the refinement arm runs before the product arm, and removing it is what makes the widening control discriminating above. It is not claimed to repair the disjoint case.

Status

The five enrolled controls and the whole required floor are green locally on this head; the same harness reproduced all six predecessors as red before the repair. The regenerated stage0 mirror is committed with the .dag change, verified by content. docs/design-failure-modes.md is re-projected — it drifted because the merge resolution took main's projection without re-projecting the new row.

One observed unrelated signal, not chased and not fixed here: the floor emits STALE-COST-DEBT for test.claim.live_deploy.emit.apply_script_and_tree_sync_unit_stay_within_ci_runner_grants, enrolled in v2.workflow.floor_cost_debt. It is not counted in unexpected_failures and is not what refuses the lane. This diff does not touch src/v2/workflow/floor_cost_debt.dag at all.

Two claims withdrawn, both refuted by fixture rather than argued down

• "An explicit cast is not carried at this seam." False: takes_non_empty(s: "x" as NonEmptyStr) produces nothing from this relation.
• "The refinement predicate goes unchecked at introduction." False, and this one changes the story. A three-way pair settles it: takes_non_empty(s: "") is refused by the where-refinement machinery (type mismatch: expected Product(NonEmptyStr), got Primitive(String)), takes_non_empty(s: "x") is admitted by it, and this relation declines both. So the introduction question is already decided by an authority this relation does not consult — the "never undecidable, merely unconsulted" shape the numeric note in the same file records. The next-rung trigger is correspondingly cheaper: consult that verdict, not carry a new elaboration fact to the seam.

The recurring_failure_mode row is corrected the same way: it asserted that the roster residue reports UndecidableFormalUnresolved, and the census moved that population by zero across the repair, so the row now records that boundary as asserted and unexercised.

🤖 Generated with Claude Code

https://claude.ai/code/session_01MuB8wHjijaFwNoyzm78stF

[briansrls]

Exact-head whole-diff review of 774a048: REQUEST_CHANGES.

1. BLOCKER — the v1-freeze admission argument does not discharge PublicSurfaceGrowth, which the standing says DOMINATES purpose admission. The authority explicitly defines PublicSurfaceGrowth as a diff over the emitted seed's exported declarations. This head adds exported declarations in the public v1_compiler_infer module: refinement_chain_link_identities, refinement_chain_names, the new RefinementInhabitance enum, refinement_inhabitance, plus new variants on the public InhabitanceUndecidableReason. The generated mirror renders these as pub. Refusal-set identity is good evidence against NewLanguageBehavior; it is not evidence that the exported surface did not grow. Either restructure the integration closure so it does not grow the frozen seed's exported declaration surface, or obtain an authority ruling that actually changes/discharges this dominating refusal. The current purpose/self-host measurements cannot override it.

2. BLOCKER — the refinement identity repair still loses exact declaration identity before the new site-key comparison, and the 'all links identified' check does not actually prove declaration resolution. refinement_chain_names starts by taking authored_name_at(n) and calling lookup_type_by_name, even though lookup_type_for is the existing node-aware authority and uses node.ident first. Thus a node that already carries identity can be rebound through ambient bare-name/homonym resolution before declaration-site IDs are compared. Inside the chain, where_refinement_chain explicitly falls back to the raw base node when lookup_type_for misses; refinement_chain_link_identities then calls where_refinement_brand_declaration_site and treats the presence of ident_span as proof of identity. But ident_span is not declaration provenance — default_ident_span gives any named node an ident span. An unresolved reference can therefore be assigned a file#name key and survive the completeness check. This is the same class the comments say is forbidden: absence of identity is being repaired by degrading what is compared. Resolve the head and every chain link through an exact declaration-aware carrier (or make the whole relation unavailable on any resolution miss); do not turn reference spelling/location into declaration identity.

Gate note: this head is no longer an integration candidate even apart from the findings. Its base is 100b6e7..., while current main is f69e0a3... (9 commits ahead), including a docs/design-failure-modes projection change. Per exact-head doctrine, merge current main, re-project/regenerate, re-derive the matrix/refusal identity set, and rerun CI before requesting another verdict. Any new head is a new review subject.