Repository navigation
DO NOT MERGE: #12640 old-vs-new infer gather differential - #12648
Closed
gunbai-bot[bot] wants to merge 94 commits into
Closed
gunbai-bot[bot] wants to merge 94 commits into
gunbai-bot[bot] wants to merge 94 commits into
Conversation
…st holds the label in an Rc)
…e generic-ident-class flip
…_atom_identities) instead of re-parsing each
…uments (the witness is about carets, not the lambda frontier)
…ypes a bare Cons as FreeMonoid)
…l spelling instead of being captured Body lowering rewrote every type atom spelled Int or Bool to the kernel binding before any scope existed. A module that declared its own `type Int = | Mine` and wrote `let y: Int = 1` therefore had its annotation replaced by the kernel Int, and infer judged the let matched. The spelling table moves to its language authority (v2.extdeps.languages.dag dag_kernel_type_binding_optional), and resolve_atom consults it only after the scope walk and the symbol index. A hit declared in the referencing module binds that declaration. Imported, foreign, ambiguous and unbound kernel spellings keep the kernel binding, unchanged. Claims (v2.test.claim.body_let_annotation, 5c): the module-declared Int and Bool lets refuse at the annotation, and the annotation is asserted not to be the kernel binding. An undeclared Int/Bool still binds the kernel type. Both shadow rows are red on main 9ce0394 and green here. The rfm row records the residual and its trigger. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…l Int Resolve now reads a kernel spelling by the declaration a door selected. v2.extdeps.languages.dag dag_kernel_type_declaration_binding_optional lists the declarations a kernel spelling denotes. A hit on one of them takes the canonical binding, and the module's own declaration shadows it. Any other declaration, reached through an import or another module, refuses with resolve_reason_kernel_type_spelling_names_a_foreign_declaration. Unbound and ambiguous names keep the spelling fallback. Third RED: bla_imported_user_int_refuses_rather_than_binding_the_kernel_int (a two-module fixture, p imports q's `type Int = | Mine`). All three REDs are F on main and T here, and the controls are T on both. The new specimens are enrolled in floor_pure_producer_share. The rfm row now states rung = refused, with the trigger at capability grain: declaration-keyed binding across every door. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…te is a kernel declaration An ambiguous kernel spelling now binds the kernel type only when every candidate is a kernel declaration of it: v2.std.integer Int beside std.integer Int is one kernel type. Otherwise it refuses with the ordinary resolve_reason_ambiguous_symbol instead of defaulting to the kernel. An unbound name keeps the kernel binding, which is the correct answer when no declaration is in scope. New claims: - RED bla_ambiguous_imported_int_refuses_rather_than_defaulting_to_the_kernel (p imports Int from q and r). F on main, T here. - Control bla_ambiguous_kernel_declarations_bind_the_kernel_type. T on both. The multi-module specimens now share one helper, bla_assemble_with_peers. The rfm residual is now only the kernel-declaration path list. Its trigger is a mark on the kernel declarations themselves. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm # Conflicts: # src/v2/test/claim/body_let_annotation_test.dag # src/v2/workflow/floor_pure_producer_share.dag
…std.node Symbol) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…hored return-type spelling Three floor blockers on fa8c596. These claims read the positional return clause from body lowering and expected the kernel binding (dag_binding_type_int, bool_node_symbol). Lowering used to produce that binding by rewriting the spelling. That rewrite now happens in v2.compiler.resolve, after the scope walk, so lowering carries `Int` and `Bool` as written, as the generic row already reads `T`. Arm 1 still discriminates: the return type is Bool, not the parameter's Int. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
review 72280: the symbol arm tested dag_node_is_symbol_literal_atom and then recomputed dag_symbol_literal_name_optional. That was the same optional twice, and the recomputation needed an arm the predicate had already ruled out. The decision now matches the optional once. The remaining Absent arm is a name payload with no atom identity, which is reachable. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…teral_name_optional directly (review 72280 on #12549)
…-ibex-696/symbol-arm # Conflicts: # src/v2/compiler/03_resolve.dag
…xeme-stamped terminal; delete the span/source-text route and its prose note row (review 72294 on #12549) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm
…ens span route: nothing else consumed them Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…-ibex-696/symbol-arm
…pe as this PR derives it review 72301: the receipt still said the symbol literal's type stays on the GroundingNotDerived frontier. The arm in this PR makes that false. It now names the derivation route (DagCanonicalSymbolLiteral, infer_literal_type_binding, v2.std.node symbol_type_node) and the two body_let_annotation claims that execute it. Census trigger (a) stays open and the receipt says why: it names the source checker v1.compiler.types, which still types LitSymbol as string_type. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…anned per lookup facts_map_from_entries admitted entries into a List and answered every lookup with lookup_inferred_facts_in_entries, a linear scan: each consumer walking the tree paid quadratic. It now enters admitted entries into a Map<Node, InferredFacts> once and answers lookup with map_lookup. A repeated node keeps its FIRST admitted entry, as the scan did. The gather fold's own scans (lookup_inferred_facts_in_entries inside infer_gather_fold_algebra) remain: the catamorphism computes children independently, so removing them needs a state-threading node fold, filed as node adhoc-914690c3-870. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ions; ownership reads declared_in GitHub review 5342739525 on #12540. The same-module test compared a declaration's path to ctx.namespace.module_qn, but build_program_namespace (the plain normalize -> resolve route) leaves module_qn Empty and records its owner in declared_in. namespace_owns_declaration now reads declared_in, which is the owner on both namespace routes and the field root_binding_origin reads. Measuring that route found the earlier boundary. build_program_namespace harvested only the root's named edges, and a normalized module keeps its declarations under captured -> <module path>, so none of them were bound. `type Myint` refused as unbound, and a module's own `type Int` fell through to the kernel spelling and was silently bound to the kernel Int. The namespace now also harvests the module body, which it finds by declared_in. 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 and both ambiguity dispositions are unchanged and still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v2/workflow/floor_pure_producer_share.dag
…y walking names Review 5343957887 (P2 on b55b8a7). namespace_tree_module_body walked the module path's names and restarted at the root on a missing step. Two leaks followed: - `module m.t` with a root-level record `t` missed `m`, restarted, found `t`, and bound the record's field as a module binding. - `module t` with a record `t` selected it at once. The body is now selected by the producer's own mark. v2.compiler.namespace_graft namespace_graft_module_body_optional descends the containment spine (namespace_graft_spine_segment_edge_optional) until a step is not a segment, never restarts, and 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. The admission reader in v2.compiler.name_resolve already descended the same spine with its own copy (admit_named_exports_body_root and _descend_spine). It now calls the one function in namespace_graft (namespace_graft_module_body_root), so the spine has one reader. Controls (v2.test.claim.resolve.single_tree_module_body): supplied emit-shaped roots, because normalize always emits a well-formed graft and source text cannot author these shapes. - a_record_matching_the_path_suffix_is_not_a_module_body_holds: F on b55b8a7, T here. - a_record_named_like_a_flat_module_is_not_its_body_holds: F on b55b8a7, T here. Each asserts `leaked` is not bound and `t` still is. The local Int/Bool and undeclared-kernel controls still hold. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ation The parse phase refused a // annotation inside the fn body (DESIGN section 4c: only module-item grain is modeled). This is the same text, placed above the declaration. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
force-pushed
the
dnm/neat-eagle-675-differential
branch
from
September 29, 2026 21:11
316219e to
4ebc026
Compare
…rential isolates the threaded gather Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…mbol_value_lowering (the refusal suite stays deleted)
…aret_symbol_value_refusal (carried via #12549), add main's bcn_let_in_value_cast_verdict share row Main's #12615 let-in caret case lived in the retired refusal test; moving it into the lowering test is #12420's (flagged to its owner). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…sion/neat-eagle-675
…/neat-eagle-675-differential
…-ibex-696/symbol-arm
…sion/neat-eagle-675
…/neat-eagle-675-differential
Contributor
Author
|
Review 72904: its findings match reviews 72712 and 72795, and the answer is the same. This branch does not land. — sent from neat-eagle-675 |
…ipt; caret cause row stays retired; let-in comment matches the lowering)
…sion/neat-eagle-675
…/neat-eagle-675-differential
…r 046/051/070 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…y a run-wide lookup Asked of the threaded map, 'does this node already have an entry' saw a structurally equal node entered elsewhere and skipped the row, dropping that occurrence's frontier diagnostic (DNM #12648 run 36647127349: 046/051/070 differ only in their infer_grounding_not_derived count). The list gather's subtree-scoped check never found the node itself, so the row always ran. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…/neat-eagle-675-differential
…r-node facts, root) on #12640 with the kind-decided product row Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Review 72954: the same findings as reviews 72712, 72795 and 72904, with the same answer. This branch does not land, and it is closed once the 98-specimen run on 9fbc8a6 is recorded in #12640. On the three specimens it names: 046, 051 and 070 are now explained. They differed only in their — sent from neat-eagle-675 |
…lict fatal (reason, key, locus) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…/facts/root/key-conflict/accepted Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…first-entry-wins (review 72985) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…/neat-eagle-675-differential
…for the 11 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Closing without merge, per review 73020's recommendation. This was a DO-NOT-MERGE differential and cost probe; the committed copy of the old gather was never meant to land (§3: an offline oracle, never in-tree). The results (which 11 specimens differ and why, the 0/98 acceptance-to-refusal count, and the cost-curve runs by id with the floor eval_steps instrument named) are recorded on #12640, which is held until occurrence projection (#12604 + follow-up). The branch is kept, not deleted, as the rerun recipe; a fresh DNM PR will be opened from it for that rerun. — sent from quiet-gull-780 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Throwaway differential for #12640, run by the fleet floor. Nothing from this PR lands, and it is closed once the run is read.
v2.test.claim.dnm.infer_old_gatheris the pre-changev2.compiler.inferat 476baf1, verbatim except the module line andinferrenamed toinfer_old.v2.test.claim.dnm.infer_gather_differentialhas one claim per specimen, 98 in all, covering every distinct"module p\n..."source insrc/v2/test. Each assembles the specimen withtpb_assemble, runs both infers, and asserts equal verdicts. On refusal it compares the diagnostics; on acceptance it compares the diagnostics andfacts.lookup(n)for everynode_subtree_nodesnode. Each claim reads a WARM nullary producer so it fits the per-claim budget.🤖 Generated with Claude Code