v2: one roster of kernel value types; a declared Bool is judged (dag_binding_type_bool deleted)

[gunbai-bot]

DRAFT, stacked on #12763 (which is stacked on #12566 + #12714 + #12629). The diff against main shows all of them until they land; this PR's own change is 15 files. Do not merge.

What it does

v2.extdeps.languages.dag had three hand-written if-chains that each restated which symbol a kernel type has: the resolver's spelling table (dag_kernel_type_binding_optional), its declaration table (dag_kernel_type_declaration_binding_optional) and the denotation join (dag_binding_denotation). For Bool they disagreed.

They are replaced by one roster, dag_kernel_value_type_roster. A row is a value-type node owned by a std authority, an optional spelling, and the declaring paths that spelling may resolve to. A kernel type's canonical binding is the atom identity of its value-type node, derived from the row and written nowhere else. The three functions are now folds over the roster, so they cannot disagree.

Kernel type	Value-type node	Spelling row
Int	v2.std.integer integer_int_type_node	yes (v2.std.integer.Int, std.integer.Int)
Bool	v2.std.logic bool_node	yes (v2.std.logic.Bool, std.types.Bool)
Symbol	v2.std.compilers.target_model symbol_kernel_type_node	no
Char	v2.std.compilers.target_model char_kernel_type_node	no

The defect (DESIGN 6b)

The symptom was in infer: a declared Bool was never judged. fn f(x: Int) -> Bool { 3 } and a Bool-declared record field holding 3 were accepted with a counted UndecidableFormalUnresolved.

Measured on the real route, the earliest unjustified boundary was the language model, not infer. Resolve bound a declared Bool to bool_node_symbol (bool_node's own identity). The join denoted dag_binding_type_bool, a second symbol that only hand-built fixtures and infer's literal typing carried. So the resolved atom reached every declared-type judgment as something the join answered Absent for. Int had one symbol on both sides, which is why it worked.

dag_binding_type_bool is deleted in this change, as a replacement cut: infer's infer_literal_type_binding, six fixture sites in the language model and four test files move to bool_node's identity. No reader of the old name remains.

Scope decisions

• Symbol and Char are a fork, recorded here and not resolved. Each has two authorities: a kernel value-type node in v2.std.compilers.target_model, and a declaration its authored spelling resolves to (v2.std.node Symbol, std.types Char). That is the same fork class as Int and Bool, where the ruling is one authority, the declaration visible in scope. The corpus does spell both in type positions, so binding either spelling to the kernel atom here would change what every such reference resolves to. Their rows therefore carry no spelling row and name, in converges_on, the declaration each converges on once de-forked. Nothing binds through that field; There is a second fork underneath: the one roster of kernel names is std.types kernel_type_set, and Symbol and Char are not in it, so target_model calls them kernel atoms while the kernel name roster does not know them. kvr_symbol_and_char_are_a_recorded_fork_that_binds_no_spelling_holds holds both sides as they are (no spelling, no declaration binding, not in kernel_type_set; Int and Bool are) and goes red if either side changes without the other. The de-fork lane (wise-dove-693) has taken both names and decides per name whether it is genuinely kernel or declaration-backed.
• Float, Secret, Json, Unit, Bytes get no row. None has a value-type node in a v2 std authority, so there is nothing for a row to point at, and I did not invent one. Each is filed as its own failure-mode row (kernel_type_<name>_has_no_v2_value_type_node) with that node as its trigger. Unit is the most exposed: v2 sources outside tests spell it in 14 type positions.
• String is excluded. By the text ruling, v2 String is FreeMonoid<Char>, not a kernel atom.
• Relation to De-fork Float: binary64 authority in extdeps (IEEE 754-2019); kernel Float denotes it #12547 (std.kernel_type_denotation), agreed with wise-dove-693. Three separate facts: what a kernel name means (De-fork Float: binary64 authority in extdeps (IEEE 754-2019); kernel Float denotes it #12547's table), which v2 node carries the type in resolve and infer (this roster, a realization checked against the meaning, as Rust f64 is there), and converges_on (a provisional de-fork pointer, deleted when the fork closes). This roster adds no meaning. After De-fork Float: binary64 authority in extdeps (IEEE 754-2019); kernel Float denotes it #12547 lands, the Int and Bool rows are keyed by its std.kernel_type_name admission instead of a bare spelling, so a row for a non-kernel name is refused by construction and the five failure-mode rows become an identity join. Whichever lands second does that.
• No single kernel type authority exists in v2 for the carrier. std.types kernel_type_set lists the kernel names only. The roster derives from the per-type node authorities that do exist.

Evidence

v2.test.claim.compiler.kernel_value_type_roster_witness_test, 6 claims, 6/6 locally.

• Red, real route (source text through the production front end into infer): a declared Bool return holding an Int refuses arrow_body_does_not_inhabit_declared_return. Control: true at the same return is accepted and decided.
• Record field: v2 infer: a record construct's field values are judged against the fields its record declares #12763's pinned claim is rewritten to the refusal, rcf_a_bool_declared_field_value_of_the_wrong_type_refuses_holds.
• Formal: not a red this route can fire yet. A named call's callee is a declaration reference that infer does not type by its declaration (v2 resolve/infer: the dotted-path decision keeps its binding kind, and projection inference stops calling an unretrievable declaration a fieldless receiver #12506), so its formals are unresolved whatever they declare. Pinned as counted by kvr_a_named_calls_bool_formal_is_counted_not_judged_holds; it goes red when v2 resolve/infer: the dotted-path decision keeps its binding kind, and projection inference stops calling an unretrievable declaration a fieldless receiver #12506's capability lands.
• Roster laws: every row's binding denotes that row's node; a spelling and each listed declaration bind what the join denotes; the Symbol and Char fork binds no spelling and no declaration.

Neighbouring suites on this head, same binary: record-field witness 13/13, denotation 3/3, declared-return 12/12, arrow-elimination 7/7, application-argument 10/10, refinement-discharge 4/4, body-let-annotation 22/22, branch-infer 4/4 and 2/2, match fail-open 7/7, atom-grounding 11/11, self-grounding wall 12/12, data-decl grounding 9/9, qualified-construct 9/9, declaration-graft 18/18, call-argument mention survival 18/18, match-arm binder frame 15/15.

Coordination

• De-fork Bool: v2.std.logic Bool retired, std.types Bool the single declaration (replacement migration) #12583 (warm-wolf-234, Bool de-fork) retires v2.std.logic Bool. It touches neither Bool symbol nor these functions. Whichever lands second updates the Bool row's declaring paths, and confirms where bool_node's identity lives once that declaration is gone.

Census of newly refused sites

Instrument: claim_executor --v2-native-route --source-root dag --source-root src/v2, the route that runs v2 resolve -> infer -> eval over real modules. One BuildBuddy dispatch per sha, each verified at its pin; both exited 0.

• base 09b5bf8923 = v2 infer: a record construct's field values are judged against the fields its record declares #12763's head (main merged)
• head a0ec30eeea = this PR. One later commit (91b819a) changes only which node one witness claim infers.

	base	head
modules in the universe	832	833
refused before infer — not measured	767	768
reached v2 infer (N)	65	65
of those, accepted	35	35
of those, infer_refused	30	30

• M = 0 newly refused, and 0 newly accepted. Every module has the same outcome at base and head. Every test has the same (identity, stage, cause) at base and head, apart from this PR's own claims: the new witness module's six, and the renamed record-field claim. Those are refused before infer on this route (a dag/std/algebra.dag import does not lower natively) and run on the seed-interpreted floor route instead.
• What did change: 27 refusal chains got one link shorter. In 27 tests across 12 modules that were already refused at infer, the chain at base began infer_grounding_not_derived @ <node "bool_node_symbol">: a declared Bool type atom the join could not denote, left on the frontier. At head that link is gone in all 27, and bool_node_symbol appears in no verdict chain at all (27 at base, 0 at head). Each of those tests is still refused, at the same stage, for the same cause, by the next underived node in its chain. So the roster removes a frontier node; on this population it does not yet change a verdict.
  • By module: computation_identity_test 5, self_host.frontier_probe_semantic_family_receipt 5, namespace_graft.zero_metadata_test 3, self_host.v2_emitter_direct_rust_door_contract 2, the go/kotlin/python/typescript grammar claims 2 each, and 1 each in infer_transform_binary_infix_witness_test, claim_pipeline.infer, sg5_set_non_ordable_falsification, compiler_frontier_emit_probe.

Limits. N is 65 of 833, and they are v2.test.* modules, not the product corpus. The other 768 are not measured, not zero. As on #12763, the census obligation carries forward to when the v2 front end reaches the floor path for a wider population.

An earlier dispatch of this pair returned only its base half (the head run's output stopped after checkout with no build or exit line), so it was discarded and both were run again.

Still owed

• CI. The first floor run on this PR passed every claim and refused one for cost: the pinned formal claim measured 81,329 eval steps against the 72,300 new-witness budget. It now infers the calling member only (about 41k locally). Rerunning.
• Bases. v2 infer: a record construct's field values are judged against the fields its record declares #12763, and under it MQ PR2: construct tag is a declaration reference — qualified construction, patterns and nullary lower (unblocks 01_tokenize) #12714, must land first.

🤖 Generated with Claude Code