Resolver: refuse an import that collides with a kernel mint name

[gunbai-bot]

Summary

• One rule, decided once: an authored import of a type declaration whose name has a kernel_mint_declaration_rows row, from a module that is not that mint, refuses at the import (ImportCollidesWithKernelName). Unifying overlay_skips_kernel_name (kernel wins) with lookup_binding (import can win) would pick one lie consistently; the two Optional types would still exist. Refusal is the construction (§6b).
• Census before the cut (dag + src/v1 + src/v2): kernel-named imports are ordinary (String 3757, List 3294, Bool 3169, Int 1989, Present 997, Absent 965, Optional 372 of which 359 are v2.std.optional). Type declarations of those names are few (Optional: v2.std.optional + this collision fixture). A blanket refuse of every kernel-named import would take the floor down. Dual-rep imports (v2.std.text String) stay with carrier_by_spelling.
• Native broker 2K-b: identity-keyed type_summaries; Host-Option decided by declaration #13454's collision type is re-authored here (native_emission_controls_optional_collision). The importer fixture is fixtures/native_emission_controls_optional_importer.dag (not ingested: a wall is not installable over a corpus that violates it) and is compiled by test.claim.infer_kernel_import_collision_witness (test.claim.infer_ is on the required gate). Positive controls: a non-kernel name from the same module; importing the mint itself.
• Did not merge Native broker 2K-b: identity-keyed type_summaries; Host-Option decided by declaration #13454: generated-artifact concurrent divergence on compiler_tests.rs. The resolver wall does not need the identity-keyed type_summaries cut.

Test plan

• Floor: test.claim.infer_kernel_import_collision_witness three claims green
• cargo check -p v1-compiler (done remotely)
• Regen of v1.compiler.resolve / v1.std.core mirrors when a required-regen lane runs (seed rust was updated in lockstep)

Made with Cursor

[briansrls]

NO-LAND at exact head 93af325.

The requested scope judgment passes: this is not a blanket kernel_type_set wall. KernelMintDeclarationAbsent admits the import, so String remains outside this class and stays explicitly owned by carrier_by_spelling; the new failure-mode row names that divergence and does not claim it closed.

One identity blocker remains. imported_type_collides_with_kernel_mint decides that the imported type IS the mint owner by comparing only (d.module_path as String) == import_path. But KernelMintDeclaration names an exact DeclarationRef: minted_name and declaration.decl_name are separate modeled facts, and no invariant requires them to be equal. The imported declaration is identified by (import_path, name). If a mint row maps spelling Optional to owner.Maybe, and module owner also declares a different type Optional, this code admits importing owner.Optional merely because the module matches, although that exact declaration is not the mint. That recreates the collision the wall claims structurally impossible.

Compare the exact declaration identity: both module path and declaration name. If the intended model is instead that minted_name == declaration.decl_name is mandatory, encode and enforce that invariant rather than depending on the current row by convention, and add a discriminating control.

The helper also collapses KernelMintDeclarationAmbiguous into Present { value: import_path }, causing the diagnostic to claim a specific kernel declaration module that the authority explicitly could not decide. Keep the ambiguity as a typed arm/refusal rather than fabricating an owner.

Small control correction while touching this: importing_the_kernel_mint_optional_is_accepted currently proves only that this one diagnostic class is absent; FixtureCompileRefused for any other cause still passes. Either require outcome_clean(compile_mint_import()) or rename the claim so it does not assert acceptance.

[gunbai-bot]

review 76934 asked for one authority for the discriminating importer (and the collision RED aligned with the corpus declaration). That was the previous head (93af3259): importer_source / collision_source were a second copy of the files.

Current head ca07d88eee deletes those strings. compile_importer filesystem_reads dag/gunbc/instruments/native_emission_controls_optional_collision.dag and fixtures/native_emission_controls_optional_importer.dag and hands those bytes to compile_fixture. The positive control that imports collision_seven reads the same collision file. Drift between file and claim is now a failed read, not a silent fork.

— sent from swift-ram-681

[briansrls]

NO-LAND at exact head ca07d88.

Review 76934 is correctly addressed: the RED now reads and compiles the committed collision module and importer fixture, so there is no second authored copy of either specimen. That improves the evidence, but this commit changes only the witness and a fixture comment; the resolver rule is unchanged from 93af325.

The three substantive blockers therefore remain:

1. Mint ownership is still compared only at module grain. KernelMintDeclaration names an exact DeclarationRef, but imported_type_collides_with_kernel_mint admits the import whenever d.module_path == import_path. It must also require d.decl_name == name (or enforce an equivalent model invariant). Otherwise a row minted_name=Optional, declaration=owner.Maybe wrongly exempts importing a different owner.Optional.

2. KernelMintDeclarationAmbiguous still returns Present { value: import_path }, which fabricates a unique kernel declaration module from the imported module precisely when the authority says the mint owner is ambiguous. Give ambiguity its own typed refusal/result arm; do not populate kernel_declaration_module with a guessed module.

3. importing_the_kernel_mint_optional_is_accepted still passes for any FixtureCompileRefused that merely lacks ImportCollidesWithKernelName. Require outcome_clean(compile_mint_import()), or rename the test to claim only absence of this diagnostic.

The mint-row-only scope and the bounded String divergence remain acceptable. CI is currently queued on this exact head.

[gunbai-bot]

review 76940 is against the pre-785270a4ac resolver (the cited 03_resolve.dag:235-236 / :238 module-path shortcut and Present { value: import_path } arm). Current head 785270a4ac already lands both findings:

1. Ownership is no longer module grain. imported_type_collides_with_kernel_mint delegates to std.literal_elaboration kernel_named_import_standing, which admits only when (d.module_path as String) == import_path && (d.decl_name as String) == imported_name. A row Optional → owner.Maybe therefore collides for import owner { Optional }; that case is enrolled as a_mint_row_for_owner_maybe_does_not_exempt_importing_owner_optional. That is the review's allowed arm ("or compare both module_path and decl_name"). kernel_mint_ownership remains the arm-identity question; this standing is the import-exemption question over the same DeclarationRef fields.

2. Ambiguous mint rows are KernelNamedImportMintAmbiguous, emitted as KernelMintDeclarationAmbiguousAtImport (gate-blocking). kernel_declaration_module is not filled with the imported path.

importing_the_kernel_mint_optional_is_accepted is outcome_clean(compile_mint_import()) on this head as well.

— sent from swift-ram-681

[briansrls]

LAND at exact head 785270a.

All three blockers from ca07d88 are closed at the shared decision authority:

1. kernel_named_import_standing exempts an import only when the mint row's full DeclarationRef agrees with the imported declaration: both module_path == import_path and decl_name == imported_name. The owner.Maybe/owner.Optional control discriminates the former module-only bug.
2. Duplicate mint rows produce KernelNamedImportMintAmbiguous; the resolver maps that arm to the separate blocking, located KernelMintDeclarationAmbiguousAtImport diagnostic. No owner module is guessed.
3. importing_the_kernel_mint_optional_is_accepted now requires outcome_clean, so any refused or dirty compilation fails the control rather than passing merely because this one class is absent.

The source-backed RED remains sound: the enrolled witness filesystem-reads the actual collision declaration and importer fixture, so the specimen cannot drift behind a copied source string.

The scope remains coherent. This wall is parameterized by kernel_mint_declaration_rows, not by the broad kernel spelling set; names with no mint-declaration row do not enter it. String therefore remains an explicit, measured divergence under carrier_by_spelling, not an accidental exemption. The resolver owns whether the imported module declares a type of the name; std.literal_elaboration owns the mint-row judgment; one result is exhaustively consumed at the import seam.

The PR is open and mergeable. Exact-head CI is still in progress, so landing should wait for the required non-unit lanes and generated fixed-point check to complete successfully.

[briansrls]

LAND at exact head c13efd6.

Re-reviewed the five commits since the approval at 785270a. No new blocker is present.

• Mint-owner admission now uses full declaration_ref_eq against a WholeDeclaration decl_ref; the field-ref control proves that matching module/name alone cannot exempt a different declaration field.
• The generated stage0 mirrors are installed and exact-head generated CI, including all-target lint and fixed-point verification, is green.
• The collision Optional and importer are fixture-only. The discriminating RED reads those real fixture files, while the positive non-kernel-import control is intentionally self-contained so an unrelated missing std.types module cannot satisfy it by refusal.
• Moving the colliding Optional out of the source-root corpus is correct: the wall is tested by explicit fixture compilation without injecting a second Optional declarer into every floor closure.
• d851c41's three roster retirements are exactly reversed by c13efd6; the net PR no longer changes that roster, and retaining ActiveDebt is the honest final state.
• Exact-head emit-build, generated, rust-unit-tests, floor, and aggregate witnesses all succeeded.

No merge action taken.

[gunbai-bot]

Dequeued: this PR ADDS import v2.std.optional, a module #13388 removed. In a merge group it fails to resolve (as #13440 did at the queue head, run 37544005485) and ejects every group behind it. Fix: merge main, repoint with tools.source_reference_repoint (v2.std.optional -> std.optional), re-green, and re-enqueue.

— sent from sharp-raven-357

[briansrls]

LAND at exact head d6e32f4.

The approved resolver rule is unchanged. Since c13efd6, the branch merged current main and the final commit only repoints this PR's Optional mint receipts/control from v2.std.optional to std.optional. The executable authority now binds kernel_mint_declaration_rows to the exact DeclarationRef std.optional.Optional; the clean mint-import fixture, direct standing control, census prose, and resolver comment agree with that identity. The exact declaration_ref_eq exemption, ambiguous-mint refusal, source-backed collision witness, and typed import refusal remain intact.

Exact-head generated passed all-target lint and the stage0 fixed-point check; rust-unit-tests, emit-build, floor, and aggregate witnesses also succeeded.

One handoff correction, non-blocking: at this composed head the uri, rust_crate_package_ident, and evaluation_budget Optional roster rows are Retired { ImportsFixed }, not ActiveDebt. That is coherent with current main because each file now explicitly imports Optional from std.optional; this PR does not modify the roster. Also, structural_realization_bindings still has one stale prose sentence saying v2.std.optional immediately above the authoritative std.optional row; clean that up separately, but it does not change the modeled identity or this verdict.

[gunbai-bot]

review 77339: fixed. resolve_import now builds module_type_declaration_names once per target_mod. The import-all arm calls kernel_named_import_standing with module_declares_type: true and binds each name once from that set. The specific-names arm queries the same set through kernel_named_import_child_diags, which binds the authored name once.

— sent from swift-ram-681

[gunbai-bot]

review 77445 is right: imported_type_collides_with_kernel_mint / module_declares_type_named were unused wrappers. resolve_import already refuses through kernel_named_import_standing + kernel_named_import_diags / kernel_named_import_child_diags over one module_type_declaration_names scan. Deleted the pair from 03_resolve.dag and the stage0 mirror, and pointed the RFM evidence and the witness header at that executing path.

— sent from swift-ram-681

[gunbai-bot]

Follow-up on the same head path: deleting the unused wrappers surfaced that module_type_declaration_names still used fold(..., f: (acc, item) => ...), which this file's parser refuses (expected RParen, found Comma at the map_insert argument list). Rewrote that fold as f: fn(acc, item) { ... }, the form check_duplicate_modules already uses.

— sent from swift-ram-681

[gunbai-bot]

From gentle-dove-36: this PR was approved at d6e32f4427, then manually dequeued and pushed to f4f0a56dda and now 0a9ecf0079, with no explanation. Please state what changed since d6e32f4427 and why. If it isn't needed, restore the branch to d6e32f4427 so it can be re-queued under the existing approval.

— sent from gentle-dove-36

[briansrls]

LAND at exact head a4f1a32084a5cf467188791526671410b60bf5e6.

The one-scan fold is equivalent to the approved per-name predicate at the decision boundary. For any imported name n, map_has(module_type_declaration_names(target), n) is true exactly when the former module_items(target) |> any(item => item is a type declaration && authored_name(item) == n) was true. A selective import therefore reaches the same kernel_named_import_standing arm with the same child span. For import all, every type-declaration name is still judged with module_declares_type: true; the only bounded representational difference is that duplicate declarations of the same name collapse to one collision diagnostic, while the target is already refused separately as DuplicateDeclaration. The import wall is properly keyed per imported name, so this is not a weakening.

The cost shape is improved from a target-module rescan per imported name to one target scan plus map membership per requested name. The import-all path likewise stops rescanning the target for each declaration. No second semantic authority was introduced: both paths still feed the same kernel_named_import_standing and kernel_named_import_diags functions.

Deleting module_declares_type_named and imported_type_collides_with_kernel_mint is correct after the callers moved to the shared declaration-name map. The recurring-failure evidence and witness comments now cite the live refusal path, and the emitted v1_compiler_resolve.rs mirror matches the source rule.

Exact-head rust-unit-tests, generated (including all-target clippy and mirror fixed point), floor, emit-build, and aggregate witnesses all succeeded. No new blocker found.