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

dag/gunbc/recurring_failure_mode/import_collides_with_a_kernel_name.dag

@@ -0,0 +1,29 @@
+module gunbc.recurring_failure_mode.import_collides_with_a_kernel_name
+
+import std.types { NonEmptyStr }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data import_collides_with_a_kernel_name: RecurringFailureMode = RecurringFailureMode {
+  identity: "import_collides_with_a_kernel_name" as NonEmptyStr,
+
+  receipts: [
+    "**import collides with a kernel name** (INVALID STATE: a module authors `import M \{ Optional \}` where M declares a type named Optional that is not the kernel mint, while the kernel Optional (`std.optional`, minted by `v1.compiler.infer` `kernel_optional_type_node`) is also in the closure. The type environment's by-name overlay (`overlay_skips_kernel_name`: kernel wins) and the interned-identity lookup (`lookup_binding`: import can win) then type the same spelling two ways. The emitted module rendered `HeldChoice<present_value>`, a leaked kernel type variable. Silent wrongness on the source path; rustc was the only wall.",
+
+    "MEASURED by bright-swift-722 on gunbc#13454 (lane 2K-b). The collision declaration and its importer live under fixtures/ (`native_emission_controls_optional_collision`, `native_emission_controls_optional_importer`) and are compiled only as a fixture. A second Optional type must not sit in a source-root: leaf-keyed Optional typing then follows the last declarer in every floor closure.",
+
+    "CHAIN RE-DERIVATION (§6b). The symptom is at emit (HeldChoice). The two lookups already disagree at resolve/infer. Unifying them under one precedence would pick one referent consistently and leave the other Optional type in the closure unused or mis-typed -- a second lie, not one rule. The earliest unjustified boundary is the authored import of a non-mint type that shares the mint's spelling. Refusal at that import is the construction.",
+
+    "SCOPE OF THE WALL, from the census before the cut. Kernel-named IMPORTS are the ordinary corpus: String 3757, List 3294, Bool 3169, Int 1989, Present 997, Absent 965, Optional 372 (359 of them from `std.optional`). Refusing every kernel-named import would refuse the floor. TYPE DECLARATIONS of those names are few: Optional in the accepted corpus is `std.optional`; the colliding declaration is a fixture only; String is `v2.std.node` and `v2.std.text`; Int is `std.integer` and `v2.std.integer`. The wall fires only when the imported module DECLARES a type of that name AND a `kernel_mint_declaration_rows` row names a different DeclarationRef as the mint (module_path AND decl_name). A row for owner.Maybe does not exempt importing owner.Optional. Ambiguous mint rows refuse as KernelMintDeclarationAmbiguousAtImport, not as a guessed module. Dual-representation imports (`v2.std.text` String) stay with `carrier_by_spelling`.",
+
+    "CURRENT RUNG: mechanically preventable. Discriminating RED: `test.claim.infer_kernel_import_collision_witness` `importing_a_non_mint_optional_refuses_at_the_import` (ImportCollidesWithKernelName at the import). Positive controls: a non-kernel name imported from the same collision module is accepted; importing the mint (`std.optional` Optional) compiles clean. The Maybe-row exemption hole is refused by `a_mint_row_for_owner_maybe_does_not_exempt_importing_owner_optional`. CEILING: structurally guaranteed -- an Accepted program cannot contain the colliding import. NEXT-RUNG TRIGGER: the same refusal is derived on the v2 resolve path for every kernel-mint spelling, so the two compilers cannot disagree on whether the import is writable.",
+  ],
+
+  evidence: [
+    DeclarationRef { module_path: "std.literal_elaboration", decl_name: "kernel_named_import_standing", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.resolve", decl_name: "kernel_named_import_diags", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.resolve", decl_name: "resolve_import", field: WholeDeclaration },
+    DeclarationRef { module_path: "test.claim.infer_kernel_import_collision_witness", decl_name: "importing_a_non_mint_optional_refuses_at_the_import", field: WholeDeclaration },
+    DeclarationRef { module_path: "gunbc.structural_realization_bindings", decl_name: "kernel_mint_declaration_rows", field: WholeDeclaration },
+  ],
+}

dag/std/literal_elaboration.dag

@@ -1,7 +1,7 @@
 module std.literal_elaboration
 
 import std.types { List, String, Bool, Int, NonEmptyStr }
-import std.decl_ref { DeclarationRef, declaration_ref_eq }
+import std.decl_ref { DeclarationRef, decl_ref, declaration_ref_eq }
 import std.syntax { LiteralValue, LitStr, LitInt, LitFloat, LitBool, LitNull, LitSymbol }
 
 // THE EXPECTED-TYPE-DIRECTED LITERAL INTRODUCTION JUDGMENT, as a model (DESIGN section 4: one
@@ -304,3 +304,33 @@ fn kernel_mint_ownership(rows: List<KernelMintDeclaration>, minted_name: String,
     KernelMintDeclarationAmbiguous { row_count: n } => KernelMintOwnershipAmbiguous { row_count: n }
   }
 }
+
+// WHETHER AN AUTHORED IMPORT OF A KERNEL-MINTED SPELLING IS THE MINT ITSELF. The exemption is the
+// full DeclarationRef, not the module path: a row for owner.Maybe does not admit importing
+// owner.Optional. Ambiguous mint rows are their own arm so the consumer cannot guess a module.
+type KernelNamedImportStanding
+  = KernelNamedImportAdmitted
+  | KernelNamedImportCollides { kernel_declaration_module: String }
+  | KernelNamedImportMintAmbiguous { row_count: Int }
+
+fn kernel_named_import_standing(
+  imported_name: String,
+  import_path: String,
+  module_declares_type: Bool,
+  rows: List<KernelMintDeclaration>
+) -> KernelNamedImportStanding {
+  if module_declares_type == false {
+    KernelNamedImportAdmitted
+  } else {
+    match kernel_mint_declaration_for(rows: rows, minted_name: imported_name) {
+      KernelMintDeclarationFound { declaration: d } =>
+        if declaration_ref_eq(a: d, b: decl_ref(module_path: import_path, decl_name: imported_name)) {
+          KernelNamedImportAdmitted
+        } else {
+          KernelNamedImportCollides { kernel_declaration_module: d.module_path as String }
+        }
+      KernelMintDeclarationAbsent => KernelNamedImportAdmitted
+      KernelMintDeclarationAmbiguous { row_count: n } => KernelNamedImportMintAmbiguous { row_count: n }
+    }
+  }
+}

dag/test/claim/infer_kernel_import_collision_witness_test.dag

@@ -0,0 +1,189 @@
+module test.claim.infer_kernel_import_collision_witness
+
+import extdeps.filesystem.filesystem_io
+import std.types { String, Bool, Int, List, NonEmptyStr }
+import std.decl_ref { decl_ref, decl_field_ref }
+import std.literal_elaboration {
+  KernelMintDeclaration,
+  kernel_named_import_standing,
+  KernelNamedImportAdmitted,
+  KernelNamedImportCollides,
+  KernelNamedImportMintAmbiguous,
+}
+import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }
+import tools.multi_module_compile_fixture {
+  MultiModuleCompileFixture,
+  MultiModuleCompileFixtureOutcome,
+  FixtureInstrumentRefused,
+  FixtureCompileRefused,
+  FixtureCompileCompleted,
+  FixtureSource,
+  fixture_source,
+  compile_fixture,
+  fixture_has_class
+}
+import gunbc.compile_diagnostic_census { CompileDiagnosticCensusRow }
+
+data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree
+
+// ONE RULE: an authored import of a type that shares a kernel-mint spelling, and is not the
+// mint's own declaration, REFUSES at the import (v1.compiler.resolve resolve_import via
+// kernel_named_import_standing and kernel_named_import_diags). Unifying the two lookups would still leave two
+// Optional types in the closure; the kernel overlay would keep winning by name and the
+// imported declaration would keep winning by interned identity. Refusal is the construction.
+//
+// THE RED BYTES ARE THE FILES. Both live under fixtures/ (not a source-root): a second
+// Optional type in the accepted corpus is itself a leaf-name fork. This witness reads
+// those files and hands the bytes to compile_fixture (review 76934).
+
+data collision_path: String = "fixtures/native_emission_controls_optional_collision.dag"
+data importer_path: String = "fixtures/native_emission_controls_optional_importer.dag"
+
+fn file_text(path: String) -> String {
+  filesystem_read(path: path).content
+}
+
+fn file_source(path: String) -> FixtureSource {
+  fixture_source(path: path, content: file_text(path: path))
+}
+
+// SAME MODULE PATH as the collision file, but no `import std.types` — compile_fixture
+// does not supply that module. The module still DECLARES Optional so the control is
+// "import a non-kernel name from a module that also declares the colliding type".
+data collision_fn_source: String = "module gunbc.instruments.native_emission_controls_optional_collision\n\ntype Optional\n  = CollisionWrapped \{ value: Int \}\n  | CollisionEmpty\n\nfn collision_seven() -> Int \{\n  7\n\}\n"
+
+data non_kernel_import_source: String = "module probe_kernel_import_ok\n\nimport gunbc.instruments.native_emission_controls_optional_collision \{ collision_seven \}\n\nfn uses_fn() -> Int \{\n  collision_seven()\n\}\n"
+
+data mint_import_source: String = "module probe_kernel_mint_import\n\nimport std.optional \{ Optional \}\n\nfn uses_mint(o: Optional<Int>) -> Int \{\n  match o \{\n    Present \{ value: v \} => v\n    Absent => 0\n  \}\n\}\n"
+
+data mint_decl_source: String = "module std.optional\n\ntype Optional<T>\n  = Absent\n  | Present \{ value: T \}\n"
+
+data collision_class: String = "ImportCollidesWithKernelName"
+
+fn compile_importer() -> MultiModuleCompileFixtureOutcome {
+  compile_fixture(MultiModuleCompileFixture {
+    sources: [
+      file_source(path: collision_path),
+      file_source(path: importer_path)
+    ],
+    entry: importer_path
+  })
+}
+
+fn compile_non_kernel_import() -> MultiModuleCompileFixtureOutcome {
+  compile_fixture(MultiModuleCompileFixture {
+    sources: [
+      fixture_source(collision_path, collision_fn_source),
+      fixture_source("probe_kernel_import_ok.dag", non_kernel_import_source)
+    ],
+    entry: "probe_kernel_import_ok.dag"
+  })
+}
+
+fn compile_mint_import() -> MultiModuleCompileFixtureOutcome {
+  compile_fixture(MultiModuleCompileFixture {
+    sources: [
+      fixture_source("std/optional.dag", mint_decl_source),
+      fixture_source("probe_kernel_mint_import.dag", mint_import_source)
+    ],
+    entry: "probe_kernel_mint_import.dag"
+  })
+}
+
+fn outcome_rows(o: MultiModuleCompileFixtureOutcome) -> List<CompileDiagnosticCensusRow>? {
+  match o {
+    FixtureCompileRefused { module_count: _, diagnostics: rows, source_digest: _, compiler_digest: _ } => Present { value: rows }
+    FixtureCompileCompleted { module_count: _, emitted_files: _, resolved_rust_functions: _, diagnostics: rows, source_digest: _, compiler_digest: _ } => Present { value: rows }
+    FixtureInstrumentRefused { cause: _ } => none
+  }
+}
+
+fn outcome_clean(o: MultiModuleCompileFixtureOutcome) -> Bool {
+  match o {
+    FixtureCompileCompleted { module_count: n, emitted_files: files, resolved_rust_functions: _, diagnostics: rows, source_digest: _, compiler_digest: _ } =>
+      count(rows) == 0 && count(files) > 0 && n > 0,
+    FixtureCompileRefused { module_count: _, diagnostics: _, source_digest: _, compiler_digest: _ } => false,
+    FixtureInstrumentRefused { cause: _ } => false
+  }
+}
+
+test fn importing_a_non_mint_optional_refuses_at_the_import() -> Bool {
+  match outcome_rows(o: compile_importer()) {
+    Absent => false
+    Present { value: rows } => fixture_has_class(rows: rows, wanted: collision_class)
+  }
+}
+
+test fn importing_a_non_kernel_name_from_the_same_module_is_accepted() -> Bool {
+  outcome_clean(o: compile_non_kernel_import())
+}
+
+test fn importing_the_kernel_mint_optional_is_accepted() -> Bool {
+  outcome_clean(o: compile_mint_import())
+}
+
+fn owner_maybe_mint_rows() -> List<KernelMintDeclaration> {
+  [KernelMintDeclaration {
+    minted_name: "Optional" as NonEmptyStr,
+    declaration: decl_ref(module_path: "owner", decl_name: "Maybe")
+  }]
+}
+
+test fn a_mint_row_for_owner_maybe_does_not_exempt_importing_owner_optional() -> Bool {
+  match kernel_named_import_standing(
+    imported_name: "Optional",
+    import_path: "owner",
+    module_declares_type: true,
+    rows: owner_maybe_mint_rows()
+  ) {
+    KernelNamedImportCollides { kernel_declaration_module: m } => m == "owner"
+    KernelNamedImportAdmitted => false
+    KernelNamedImportMintAmbiguous { row_count: _ } => false
+  }
+}
+
+test fn importing_the_mint_declaration_itself_is_admitted() -> Bool {
+  match kernel_named_import_standing(
+    imported_name: "Optional",
+    import_path: "std.optional",
+    module_declares_type: true,
+    rows: [KernelMintDeclaration {
+      minted_name: "Optional" as NonEmptyStr,
+      declaration: decl_ref(module_path: "std.optional", decl_name: "Optional")
+    }]
+  ) {
+    KernelNamedImportAdmitted => true
+    KernelNamedImportCollides { kernel_declaration_module: _ } => false
+    KernelNamedImportMintAmbiguous { row_count: _ } => false
+  }
+}
+
+test fn a_mint_row_on_a_field_does_not_exempt_the_whole_declaration() -> Bool {
+  match kernel_named_import_standing(
+    imported_name: "Optional",
+    import_path: "owner",
+    module_declares_type: true,
+    rows: [KernelMintDeclaration {
+      minted_name: "Optional" as NonEmptyStr,
+      declaration: decl_field_ref(module_path: "owner", decl_name: "Optional", field_name: "value")
+    }]
+  ) {
+    KernelNamedImportCollides { kernel_declaration_module: m } => m == "owner"
+    KernelNamedImportAdmitted => false
+    KernelNamedImportMintAmbiguous { row_count: _ } => false
+  }
+}
+
+test fn an_ambiguous_mint_row_set_is_its_own_refusal() -> Bool {
+  let doubled = concat(owner_maybe_mint_rows(), owner_maybe_mint_rows())
+  match kernel_named_import_standing(
+    imported_name: "Optional",
+    import_path: "owner",
+    module_declares_type: true,
+    rows: doubled
+  ) {
+    KernelNamedImportMintAmbiguous { row_count: n } => n == 2
+    KernelNamedImportAdmitted => false
+    KernelNamedImportCollides { kernel_declaration_module: _ } => false
+  }
+}

fixtures/native_emission_controls_optional_collision.dag

@@ -0,0 +1,25 @@
+module gunbc.instruments.native_emission_controls_optional_collision
+
+import std.types { Int }
+
+// A NON-KERNEL COPRODUCT THAT HAPPENS TO BE NAMED Optional. Not a source-root
+// module: a second Optional in the accepted corpus poisons leaf-keyed Optional
+// typing in every floor closure. The RED compiles THIS file with the importer.
+type Optional
+  = CollisionWrapped { value: Int }
+  | CollisionEmpty
+
+data collision_wrapped_row: Optional = CollisionWrapped { value: 7 }
+
+data collision_empty_row: Optional = CollisionEmpty
+
+fn collision_row_value(o: Optional) -> Int {
+  match o {
+    CollisionWrapped { value: v } => v
+    CollisionEmpty => 0
+  }
+}
+
+fn collision_seven() -> Int {
+  collision_row_value(o: CollisionWrapped { value: 7 })
+}

fixtures/native_emission_controls_optional_importer.dag

@@ -0,0 +1,13 @@
+module gunbc.instruments.native_emission_controls_optional_importer
+
+import std.types { Int }
+import gunbc.instruments.native_emission_controls_optional_collision { Optional }
+
+// THE DISCRIMINATING IMPORTER. Not ingested as corpus (fixtures/ is not a source root).
+// test.claim.infer_kernel_import_collision_witness reads THIS file and compiles its bytes.
+fn imported_optional_value(o: Optional) -> Int {
+  match o {
+    CollisionWrapped { value: v } => v
+    CollisionEmpty => 0
+  }
+}

src/v1/00_core.dag

@@ -373,6 +373,8 @@ type CompilerDiagnostic
   = UnresolvedImport   { module_path: String, importing_module: String, span: SourceSpan }
   | MissingExport      { name: String, module_path: String, importing_module: String, span: SourceSpan }
   | ImportShadowedByLocalDefinition { name: String, module_path: String, importing_module: String, span: SourceSpan }
+  | ImportCollidesWithKernelName { name: String, module_path: String, importing_module: String, kernel_declaration_module: String, span: SourceSpan }
+  | KernelMintDeclarationAmbiguousAtImport { name: String, module_path: String, importing_module: String, row_count: Int, span: SourceSpan }
   | UnresolvedType     { name: String, span: SourceSpan }
   | UnitVariantPhantomIdentityEvidenceUnavailable { name: String, span: SourceSpan }
   | TypeMismatch       { expected: String, got: String, span: SourceSpan }
@@ -604,6 +606,8 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
     UnresolvedImport   { module_path: _, importing_module: _, span: s } => s
     MissingExport      { name: _, module_path: _, importing_module: _, span: s } => s
     ImportShadowedByLocalDefinition { name: _, module_path: _, importing_module: _, span: s } => s
+    ImportCollidesWithKernelName { name: _, module_path: _, importing_module: _, kernel_declaration_module: _, span: s } => s
+    KernelMintDeclarationAmbiguousAtImport { name: _, module_path: _, importing_module: _, row_count: _, span: s } => s
     UnresolvedType     { name: _, span: s }                    => s
     UnitVariantPhantomIdentityEvidenceUnavailable { name: _, span: s } => s
     TypeMismatch       { expected: _, got: _, span: s }        => s
@@ -689,6 +693,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
     UnresolvedImport   { module_path: m, importing_module: i, span: _ } => concat("unresolved import: module '", m, "' not found (imported by '", i, "')")
     MissingExport      { name: n, module_path: m, importing_module: i, span: _ } => concat("name '", n, "' not found in module '", m, "' (imported by '", i, "')")
     ImportShadowedByLocalDefinition { name: n, module_path: m, importing_module: i, span: _ } => concat("import of '", n, "' from module '", m, "' is discarded: '", i, "' also defines '", n, "' at module scope, and the LOCAL DEFINITION binds every bare use of the name. The import you wrote is not the binding you get. Qualify the call as '", m, ".", n, "(...)' to reach the imported one, or rename one of the two.")
+    ImportCollidesWithKernelName { name: n, module_path: m, importing_module: i, kernel_declaration_module: k, span: _ } => concat("import of '", n, "' from module '", m, "' (imported by '", i, "') collides with the kernel name whose mint is the declaration in '", k, "'. An authored import of a different type of that name is refused so the type environment and the field binding cannot type the same spelling two ways.")
+    KernelMintDeclarationAmbiguousAtImport { name: n, module_path: m, importing_module: i, row_count: c, span: _ } => concat("import of '", n, "' from module '", m, "' (imported by '", i, "') cannot be judged against the kernel mint: ", to_string(value: c), " kernel_mint_declaration_rows bind that minted name, so the owning declaration is undecidable and the import is refused rather than bound to a guessed module.")
     UnresolvedType     { name: n, span: _ }                       => concat("unresolved type '", n, "'")
     UnitVariantPhantomIdentityEvidenceUnavailable { name: n, span: _ } => concat("unit-variant marker identity evidence unavailable for '", n, "'")
     TypeMismatch       { expected: e, got: g, span: _ }           => concat("type mismatch: expected '", e, "', got '", g, "'")
@@ -851,6 +857,8 @@ fn diagnostic_disposition(d: CompilerDiagnostic) -> DiagnosticDisposition {
     UnresolvedImport { module_path: _, importing_module: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
     MissingExport { name: _, module_path: _, importing_module: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
     ImportShadowedByLocalDefinition { name: _, module_path: _, importing_module: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
+    ImportCollidesWithKernelName { name: _, module_path: _, importing_module: _, kernel_declaration_module: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
+    KernelMintDeclarationAmbiguousAtImport { name: _, module_path: _, importing_module: _, row_count: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
     UnresolvedType { name: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
     UnitVariantPhantomIdentityEvidenceUnavailable { name: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }
     TypeMismatch { expected: _, got: _, span: _ } => DiagnosticDisposition { severity: SeverityError, gate: GateBlocking }