v2 resolve: a kernel type spelling is read by its declaration (own Int shadows, imported user Int refuses)

[gunbai-bot]

Why. Before the Symbol row lands (node adhoc-3b197e76-012), neat-boar-16 asked for a control to decide whether it could go into a spelling-keyed table. The control showed that table could be silently wrong, so this re-key lands first.

What happened on main. v2.compiler.body_lowering_fold body_lower_canonical_type_binding_optional rewrote every type atom spelled Int or Bool to the kernel binding during lowering, before any scope existed. Take type Int = | Mine followed by let y: Int = 1. The annotation became the kernel Int, and infer judged the let matched (DESIGN §5). The same happened when the user's Int was imported from another module.

Earliest unjustified boundary (§6b). Lowering answered a name-binding question with no scope to answer it from. The decision moves into v2.compiler.resolve resolve_atom, after a door has selected a declaration. Infer got no guard.

How a kernel spelling now resolves:

• v2.extdeps.languages.dag dag_kernel_type_declaration_binding_optional lists the declarations a kernel spelling denotes: v2.std.integer / std.integer Int, and v2.std.logic / std.types Bool. A hit on one of these takes the canonical binding, as before.
• The module's own declaration shadows the kernel name. Resolve refuses redeclarations nowhere else, and a user non-kernel type already binds this way.
• Any other declaration refuses with resolve_reason_kernel_type_spelling_names_a_foreign_declaration, typed and located. This covers a declaration reached through an import or through another module. Binding the kernel type there would be silent. Binding the user's type is the next rung. (Ruled by neat-boar-16.)
• An ambiguous name binds the kernel type only when every candidate is a kernel declaration of it. Otherwise it refuses with the ordinary resolve_reason_ambiguous_symbol.
• An unbound name takes the kernel binding through the spelling table dag_kernel_type_binding_optional. That is the correct answer when no declaration of the spelling is in scope.

v2.compiler.reference_conservation now reads the same table instead of importing the lowering function.

Evidence (v2.test.claim.body_let_annotation, section 5c). Run locally with a gunbc built from this tree, then again with the compiler files reverted to main 9ce039421d0:

claim	main	this PR
bla_module_declared_int_shadows_the_kernel_int	F	T
bla_module_declared_bool_shadows_the_kernel_bool	F	T
bla_imported_user_int_refuses_rather_than_binding_the_kernel_int (two-module fixture)	F	T
bla_ambiguous_imported_int_refuses_rather_than_defaulting_to_the_kernel (p imports Int from q and r)	F	T
bla_ambiguous_kernel_declarations_bind_the_kernel_type (control: both kernel Ints)	T	T
bla_undeclared_kernel_spelling_binds_the_kernel_type (route control)	T	T
bla_infer_admits_int_literal_ascribed_int / ..._refuses_..._bool (controls)	T	T

The shadow rows assert the route (the annotation is not the kernel binding) as well as the verdict. The imported row asserts the typed resolve reason. The new specimens are enrolled in v2.workflow.floor_pure_producer_share.

RFM row gunbc.recurring_failure_mode kernel_type_spelling_captured_a_module_declaration:

• Current rung: refused.
• Residual: the four kernel declarations are listed by path, a second record of what their declarations should carry. No binding case is silent.
• Trigger, at capability grain: kernel bindings read from a mark on the kernel declarations themselves, at every resolution door. On that climb the imported row flips from refusing to judging against Mine, and the path list is deleted.

🤖 Generated with Claude Code

[briansrls]

Verdict: REQUEST_CHANGES 32194a7

Blocker [P2]: the same-module shadowing decision uses a namespace field that is deliberately empty on the real single-tree resolve door, so an own declaration is misclassified as foreign.

File: src/v2/compiler/03_resolve.dag. Symbols: resolve_atom_declared, build_program_namespace, root_binding_origin, resolve.

resolve_atom_declared passes declared_here = (qualified_name_init(path) == ctx.namespace.module_qn). But resolve(tree, lm) calls build_program_namespace, which explicitly sets module_qn = Empty and separately stores namespace_tree_module_qn(tree) in declared_in. Its comment explains this single-tree distinction. For a root binding, root_binding_origin returns declared_in when there is no imported origin.

Source-trace counterexample, not locally executed: send the normalized form of this PR's own module-p specimen (type Int = | Mine; fn f(x: Bool) -> Bool { let y: Int = 1; x }) through resolve(tree, dag_language_model()), rather than tpb_assemble. The root-bound Int receives declaration path [p, Int]; its parent [p] is compared with module_qn = Empty. declared_here is false, [p, Int] is not a kernel declaration, and the helper returns resolve_reason_kernel_type_spelling_names_a_foreign_declaration. It should resolve to the module's own type and leave any initializer/annotation mismatch to infer. The Bool-shadow specimen has the same defect. This is a wrong refusal, not a demonstrated silent kernel capture.

The new own-name controls call tpb_assemble, and the peer controls call assemble_program_from_ingest; they do not cover this different namespace construction. The existing reordered-Bind tests demonstrate that the direct resolve door is live, but do not declare a same-spelled local type.

Required repair: determine same-module ownership from the existing declaration provenance (declared_in, or a shared ownership predicate correct for both namespace construction routes), not module_qn's lexical-search coordinate. Do not alter every namespace's module_qn merely to mask this comparison. Add a real normalize -> resolve control for the local Int/Bool shadow cases that requires resolution to the local declaration, not merely 'not the canonical atom' on a refused result. Retain the foreign-import refusal, mixed/non-kernel ambiguity refusal, all-kernel ambiguity positive and unbound-kernel controls.

Moving the decision out of lowering and preserving raw type spellings is otherwise the correct boundary repair. The declared kernel-path list remains an explicit residual; reading canonical bindings from declaration marks at every door and deleting that list is a capability trigger. This review does not demand that whole next-rung migration now. It does require the currently promised own-declaration arm to work on both existing resolve routes.

Source and recorded-evidence review; no independent local rerun or merge action.

[gunbai-bot]

Re GitHub review 5342739525 (wrong-refusal arm on the single-tree route). Fixed at b55b8a7.

Ownership: namespace_owns_declaration now reads declared_in, not module_qn. It is the owner on both namespace routes, and it is the field root_binding_origin already reads.

The earlier boundary, found by running the route: on normalize → resolve(tree, dag_language_model()) the local type Int was not refused as foreign. It was silently bound to the kernel Int, and type Myint refused as unbound. The reason: build_program_namespace harvested only the root's named edges, while a normalized module keeps its declarations under captured → <module path>, so no module-level declaration was bound on that route. The namespace now also harvests the module body, which it finds by declared_in. So the local Int and Bool bind the module's declaration.

Controls on that route (v2.test.claim.body_let_annotation, enrolled share points):

• bla_single_tree_module_declared_int_and_bool_bind_the_local_declaration: F before, T now.
• bla_single_tree_undeclared_int_binds_the_kernel_type: T on both.

The foreign-import refusal, both ambiguity dispositions, and every earlier row still hold locally. The fix is merged into #12549 at ba77453.

— sent from neat-ibex-696

[briansrls]

Verdict: HOLD / REQUEST_CHANGES at exact head 32194a7, after green CI.

CI is green: witnesses run 36445686143 completed successfully; generated, clippy, floor, compiler, emit-build, and witnesses all concluded success. The PR head remains 32194a7.

The advertised repair is NOT in that head. I re-fetched src/v2/compiler/03_resolve.dag at the exact SHA: resolve_atom_declared still compares qualified_name_init(path) with ctx.namespace.module_qn. Comment 5877107479 identifies the repair as b55b8a7, carried by #12549 at ba77453. A fix in that descendant stack cannot clear or approve this unchanged commit.

Correction to my prior review: I withdraw its stated direct-route symptom of a foreign-declaration refusal. The author's executed investigation found the EARLIER boundary: build_program_namespace did not harvest the declarations beneath the normalized module body, so local Int was not bound at all and fell through to the kernel spelling; a non-kernel Myint refused unbound. My earlier trace incorrectly assumed a root hit before reasoning about ownership. The silent capture is the actual reported old-route failure, and changing the ownership comparison alone is insufficient.

I also reviewed the proposed broader-harvest repair rather than stopping at the SHA mismatch. The declared_in ownership predicate and shallow successful harvest are the right direction, but namespace_tree_module_body has a new path-selection blocker. On a header-shaped module root, the QName need not be a containment path. A missing segment resets the traversal to root and later segments can select an unrelated declaration; its record fields are then harvested into the module namespace. The single-segment header/declaration-name collision requires representation-aware selection too. The full source-trace counterexample and narrow repair request are posted on the tree that actually contains the change: #12549 comment 5877487002, scoped to repair b55b8a7 and verified in ba77453. This new helper is not being attributed to the unchanged 32194a7 head.

Required before rebinding: publish the completed repair on the reviewed PR head (or explicitly supersede this PR with the corrected stack), preserve flat/header root-only harvesting, make missing-path traversal absorbing, and retain the real single-tree local Int/Bool plus undeclared-kernel controls alongside the new no-field-leak controls. Then qualify that new SHA in CI. No next-rung declaration-mark migration is demanded here.

Source and recorded-evidence review; I did not independently execute the .dag claims or the new source-trace counterexample. No merge action.

[gunbai-bot]

Re GitHub review 5343957887 / comment 5877487002 (P2: namespace_tree_module_body restarted at the root on a missing step). Fixed: #12540 at e519bda, #12549 at 6384e52.

The walk by names is deleted. The body is now selected by the graft's own mark. v2.compiler.namespace_graft namespace_graft_module_body_optional works like this:

• It descends the containment spine (namespace_graft_spine_segment_edge_optional) until a step is not a segment, and never restarts.
• It answers only when that stop is the marked body (namespace_graft_node_is_module_body).
• Header and flat representations have no grafted body, so they keep root-only harvesting.

One spine reader. Name-resolve admission had its own copy of the same descent (admit_named_exports_body_root / _descend_spine). It now calls namespace_graft_module_body_root from the same module.

Controls in a new module, v2.test.claim.resolve.single_tree_module_body. Source text cannot author these roots, because normalize always emits a well-formed graft; I measured that my first source-text versions passed on b55b8a7 too. So these supply emit-shaped roots:

• a_record_matching_the_path_suffix_is_not_a_module_body_holds (module m.t with a root record t): F on b55b8a7, T now.
• a_record_named_like_a_flat_module_is_not_its_body_holds (module t with a record t): F on b55b8a7, T now.

Each asserts the field leaked is not bound and t still is. The local Int/Bool, undeclared-kernel, foreign-import and ambiguity rows, and the symbol-literal rows on #12549, all still hold locally.

— sent from neat-ibex-696

[briansrls]

Verdict: APPROVE 658ca0f

Review 5343957887's P2 is closed. build_program_namespace keeps the prior root harvest and adds the module-body harvest only when v2.compiler.namespace_graft namespace_graft_module_body_optional returns the producer-marked graft body. That helper descends the existing graft spine without restart and returns Present only when the stopping node carries namespace_graft_node_is_module_body; header/flat representations therefore remain root-only.

The two supplied-tree controls discriminate the prior bug: prefix-miss/suffix-hit and flat header-name collision both require the record declaration itself to remain root-bound while its field does not become a module binding. The plain normalize->resolve controls separately establish that a real grafted local Int/Bool declaration is bound locally and that an undeclared Int still takes the kernel binding.

I found no new wrong binding from broadening the single-tree namespace harvest. The added harvest is shallow over the marked body's direct named edges; it does not recursively sweep record fields or nested binders. The body provenance edge uses the same grammar_production_identity_node_projection key already present on the module shell, so this does not introduce an additional authored binding identity.

Exact-head workflow 36484127887 is green: compiler, clippy, emit-build, floor, generated, and witnesses all succeeded. Source/evidence review only; I did not independently rerun the local F->T controls. No merge action.