Repository navigation
Charge no UnlistedImportUse on kernel identities, imported-alias expansions, or listed qualified spellings - #10906
Merged
Conversation
…esolve in the v1-infer partition The UnlistedImportUse advisory exists to charge an authored reference against the referencing module's import list. It also fired on references whose resolved binding is a kernel-minted identity (span <kernel:NAME>) -- synthetic formal nodes of imported generic functions reached through the ancestry overlay, and authored occurrences of lexically-introduced type parameters. No import-list edit can discharge such a row: the binding does not come from the import list, and adding one would rebind the reference rather than fix a listing gap. The emission site in v1.compiler.infer_resolve now consults the existing resolved_node_is_kernel_identity_for_name predicate (v1.compiler.core) and declines to charge kernel-identity bindings. The discriminating witness imported_generic_call_charges_no_unlisted_import_use_on_the_formal was RED pre-fix (one row on the kernel formal) and is GREEN post-fix. The guard widens an exclusion, so it lands with its adjacent false-negative control (review finding 6): authored_reference_spelled_like_a_kernel_formal_still_charges_unlisted_import_use authors the synthetic formal's own spelling as a real declaration and references it bare with no import edge; the binding is the corpus declaration, the identity guard has no purchase, and exactly one charge must fire. Mutation evidence: replacing the identity predicate with a spelling test (type_name != "N") in the generated resolver turns this control RED while the kernel-formal arm stays GREEN. Regenerating the infer_resolve mirror exposed that the mirror had no owning package in the stage0 partition roster, so the priced regen round refused the rebuild with MirrorHasNoOwningPackage. Per the #10037 precedent the module joins the v1-stage0-v1-infer partition (its imports are v1-infer members and std-core only): authority row in v2.workflow.rust_crate_partition, regenerated roster and mirrors, and two enrolled witnesses -- the rebuild-scope owner flip and the host-shell-to-partition-surface move. The owner-flip arm gains the ReleaseScopeEmpty match arm that #10692's new decision variant requires; without it the file does not compile against current main. Regenerated through the declared transaction on current main (50bb0c1): generated-artifact gate main_wet, required-regen emit, install, emit-partition-crates --write, whole rebuild (the partition generation authority changed, so the partitioned rebuild path correctly refused to actuate), then required-regen first_generation_equal=true and required-regen-fixed-point fixed_point_equal=true referenced at 50bb0c1. Co-authored-by: briansrls <briansrls@gmail.com>
…infer stage into the v1-infer partition An imported paramless type alias whose expansion is resolved under the IMPORTER's masked env charged the definer-tree argument names against an import list that could never list them honestly -- the names are the definer's locals, and the definer's own module compiles clean. The masked-boundary authority (v1.compiler.infer_resolve resolve_node_bounded_masked_boundary) states the invariant: grounding recursions descend into DEFINING-module structure with masked=false, because that structure is the defining module's import responsibility, not the use site's. The field-access alias peel in v1.compiler.infer now resolves the expansion with masked=false and accumulates every hop's diagnostics into the NodeResolveResult carrier, so hard refusals (UnresolvedType, ArityMismatch, InternalError) keep flowing to the judgment-producing callers. The repair lands with two adjacent false-negative controls (review finding 6), each naming the mutation it reds: - use_site_type_argument_through_an_imported_alias_still_charges_unlisted_import_use: a use-site type argument is authored by the user, resolved at the use site, and masked there by the standing authority; exactly one charge naming the argument must fire. Measured RED when the generic-args recursion is unmasked one level too high. - diagnostics_from_the_alias_expansion_still_propagate: a field access through an alias whose expansion names a type that exists nowhere refuses with exactly TWO UnresolvedType rows naming the ghost -- one from the definer's own compile (which resolves a paramless alias's right-hand side at definition time; an earlier draft's claim that it does not was probe-measured false), one carried by the peel's accumulation. Measured 2 -> 1 when the peel returns an empty diagnostic list, so the == 2 assertion goes RED. Regenerating the infer mirrors moved the whole infer stage into the v1-stage0-v1-infer partition (the same ownership hole class as the infer_resolve move): authority rows in v2.workflow.rust_crate_partition, regenerated roster, mirrors, and crate projections through the declared transaction -- generated-artifact gate main_wet, required-regen emit, install, emit-partition-crates --write, whole rebuild (partition generation authority changed), required-regen first_generation_equal=true, required-regen-fixed-point fixed_point_equal=true referenced at d625404. Co-authored-by: briansrls <briansrls@gmail.com>
A qualified reference (module.Type) whose module the source declares in an import edge was charged UnlistedImportUse on the LEAF name even when the leaf was listed: build_type_env's source_visible_names fold carried only the bare spellings, so the qualified spelling the author wrote looked unlisted to the visibility check. The fold now also inserts the qualified spelling for every imported item, so the name the text actually wrote is the name the check looks up. The two enrolled arms bound both sides of the boundary: qualified_use_of_a_listed_import_charges_no_unlisted_import_use (the false-positive row disappears) and qualified_use_without_any_import_still_charges_unlisted_import_use (the same qualified spelling with no import edge at all still charges exactly once -- the repair widens recognition of listed spellings, never the silence of unlisted ones, so this arm is the repair's own false-negative boundary). Regenerated through the declared transaction on top of the alias-peel commit: required-regen emit, install, rebuild, required-regen first_generation_equal=true, required-regen-fixed-point fixed_point_equal=true referenced at 8511149. No partition movement: the changed mirror stays inside the v1-infer partition that now owns it. Co-authored-by: briansrls <briansrls@gmail.com>
…t-use-emitter-repairs-4cca Co-authored-by: briansrls <briansrls@gmail.com>
The required-ci parse phase refuses // annotations inside a declaration body (std.source_annotation BodyGrainNotModeled: only module-item grain is modeled). The kernel-collision control carried its refusal-arm note inside the match; move it above the test fn it describes. The annotation-erased projection is unchanged, so no semantic result moves; the interpreter entry path had tolerated the body placement, which is why local control runs stayed green while the floor lane refused. Co-authored-by: briansrls <briansrls@gmail.com>
briansrls
marked this pull request as ready for review
September 10, 2026 04:27
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
briansrls
deleted the
cursor/unlisted-import-use-emitter-repairs-4cca
branch
September 10, 2026 13:45
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
2 participants
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.
Split from #10890 per its HOLD verdict (route A): the three producer-side emission repairs and their witnesses, independently reviewable from the census/ratchet program, which remains on the census branch.
The three repairs
UnlistedImportUseexists to charge an authored reference against the referencing module's import list. Three emission sites charged rows no import-list edit could honestly discharge:d6254046f6) — references whose resolved binding is a kernel-minted identity (span<kernel:NAME>): synthetic formal nodes of imported generic functions reached through the ancestry overlay. The emission site inv1.compiler.infer_resolvenow consults the existingresolved_node_is_kernel_identity_for_namepredicate and declines to charge.8511149029) — the field-access alias peel resolved the definer-owned expansion under the importer's masked env, charging definer-local names to the importer. The peel now resolves the expansion withmasked: falseper the masked-boundary authority, and accumulates every hop's diagnostics so hard refusals keep flowing.a3b7c62156) —build_type_env'ssource_visible_namesfold carried only bare spellings, so a listed import referenced by its qualified spelling looked unlisted. The fold now also inserts the qualified spelling of every imported item.False-negative controls (verdict finding 6)
Each repair widens an exclusion; each lands with an adjacent control proving the nearby true-positive population survives, with the mutation it reds named in the arm:
authored_reference_spelled_like_a_kernel_formal_still_charges_unlisted_import_use— an authored declaration spelledNreferenced bare with no import edge still charges exactly once. Measured RED when the identity predicate is replaced by a spelling test.use_site_type_argument_through_an_imported_alias_still_charges_unlisted_import_use— an unlisted use-site type argument through a listed alias still charges exactly once. Measured RED when the generic-args recursion is unmasked one level too high.diagnostics_from_the_alias_expansion_still_propagate— a field access through an alias whose expansion names a nonexistent type refuses with exactly twoUnresolvedTyperows: one from the definer's own compile (which resolves a paramless alias's right-hand side at definition time — an earlier draft's contrary claim was probe-measured false), one carried by the peel's accumulation. Measured 2 → 1, hence RED, when the peel returns an empty diagnostic list.qualified_use_without_any_import_still_charges_unlisted_import_use— the qualified repair's own boundary arm.All nine arms in
dag/test/claim/undeclared_bare_type_reference_class_witness_test.dagare GREEN on the integrated head (re-run individually, 2026-09-10: 9/9returned true).Forced partition movement
Regenerating the infer mirrors exposed that
v1_compiler_infer_resolve(and then the whole infer stage) had no owning package in the stage0 partition roster, so the priced regen round refused withMirrorHasNoOwningPackage. Per the #10037 precedent the modules join thev1-stage0-v1-inferpartition: authority rows inv2.workflow.rust_crate_partition, regenerated roster/mirrors/crate projections, and two enrolled witnesses (rebuild-scope owner flip, host-shell-to-partition-surface move). The owner-flip arm carries theReleaseScopeEmptymatch arm required by #10692's new decision variant.The required-floor failure, investigated (2026-09-10 review)
The exact-head CI run on
a3b7c62156failedrequired-witnesses-floor. Reproduced locally on the integrated head: the lane refused at the parse phase —The kernel-collision control carried its refusal-arm note inside the
matchbody; the interpreter entry path tolerates body placement (which is why the individual control runs stayed green) while the floor's parse phase refuses it. The claim name quoted in the review (test.claim.bdt_openapi_quotation::basis_points_in_product) does not exist anywhere in this repository's history (git log --all -Sfinds nothing); the parse refusal is the failure the lane actually records, and zero claims reportobserved=failedin the retained run. Repaired by cherry-picking the module-item-grain hoist already reviewed on the census branch (cfa628aebb→ here90c5887eb4); the annotation-erased projection is unchanged, so no semantic result moves.Integration receipts (current-main integration head, 2026-09-10)
d238928ca2) — zero overlapping files between the branch's diff and main's seven new commits, so no generated-mirror hunks needed discarding; the merge took both sides cleanly.claim_executor --regen-round-cost→changed_paths=0,convergence_stages=0, exit 0 (one intermediate self-reference refusal when the seed build replaced the running executable post-cherry-pick; re-ran with the built seed per the refusal's own recipe).cargo clippy --all-targets -- -D warningsgreen;cargo fmt --all --checkgreen.phases_run=3 phases_failed=0, exit 0, measurement receiptblockers: []— including both self-host witness claims.90c5887eb4: 4/4 green —required-witnesses-build,required-witnesses-floor,heal-generated-artifacts, and the aggregating requiredwitnessescontext allsuccesson the exact head. The merge HOLD's CI condition is discharged.Out of scope here (still on the census branch): the raw severity-independent census, the immutable source/compiler/policy receipt, the closed class roster / bijection witness, and the Step 0 binding census that replaces
AddImportclassification.