diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 7f2f698..4eaeeb6 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -1653,22 +1653,51 @@ pub fn build_check_env(ws: &Workspace) -> Env { // env.module_imports — per-module alias-or-name -> module-name. // Per-module because aliases collide across modules; sibling // shape to `module_globals`. + // + // Implicit-import set: the literal name `"prelude"` (the + // legacy singleton implicit import, retained unconditionally + // for back-compat with workspaces whose prelude predates the + // kernel-flag) PLUS every workspace module flagged + // `kernel: true`. The kernel-flag half mirrors the loader's + // filter at `crates/ailang-surface/src/loader.rs` + // (`modules.filter(|m| m.kernel)`) that drives + // `implicit_imports` into `build_workspace`. The pre-pass + // `qualify_workspace_types` freely produces qualifiers like + // `kernel_stub.StubT`; without this injection the type- + // validity check at ~line 1968 would reject `kernel_stub` as + // an unknown module prefix. Fieldtest F3 surfaced the gap + // (the previous code force-injected only `prelude`, leaving + // `kernel_stub` and any future kernel-tier module unreachable + // from consumers). The production prelude carries + // `kernel: true`, so the two halves are idempotent for it; the + // `"prelude"` literal stays so unit-test workspaces that + // construct a `kernel: false` prelude still see the contract. + let kernel_modules: Vec = ws + .modules + .values() + .filter(|m| m.kernel) + .map(|m| m.name.clone()) + .collect(); for m in ws.modules.values() { let mut import_map: BTreeMap = BTreeMap::new(); for imp in &m.imports { let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone()); import_map.insert(key, imp.module.clone()); } - // the prelude module is implicitly imported into - // every non-prelude module. A user-declared explicit - // `import { module: "prelude" }` would already place - // "prelude" in the map above (idempotent insert via entry). - // The prelude module itself does not import itself. + // A user-declared explicit `import` of any implicit name + // would already have placed it in the map above + // (idempotent insert via `entry`). A module is not + // auto-imported into its own body. if m.name != "prelude" { import_map .entry("prelude".to_string()) .or_insert_with(|| "prelude".to_string()); } + for k in &kernel_modules { + if &m.name != k { + import_map.entry(k.clone()).or_insert_with(|| k.clone()); + } + } env.module_imports.insert(m.name.clone(), import_map); } @@ -1785,20 +1814,34 @@ fn check_in_workspace( let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone()); import_map.insert(key, imp.module.clone()); } - // the prelude module is implicitly imported into - // every non-prelude module's body-check env. The wiring here - // populates `env.imports` (the active per-module table the - // body-check pass reads); the sibling block in `build_check_env` - // populates `env.module_imports` (the workspace-wide table - // referenced when resolving qualified names across modules). - // Both fields need the prelude-injection rule applied, and they - // are populated from different code paths — hence the apparent - // duplication. The prelude itself does not import itself. + // Implicit-import set for the per-module body-check env + // (mirrors `build_check_env`'s sibling injection into + // `env.module_imports`): the literal name `"prelude"` (legacy + // singleton, kept unconditionally) PLUS every workspace module + // flagged `kernel: true`. The kernel-flag half mirrors the + // loader's filter at `crates/ailang-surface/src/loader.rs` + // that drives `implicit_imports` into `build_workspace`. The + // two halves are populated from different code paths (the + // workspace-wide table in `build_check_env`, the per-module + // table here), hence the apparent duplication. A user-declared + // explicit `import` of the same name is idempotent via + // `entry`. A module is not auto-imported into its own body. + // Fieldtest F3 surfaced that the previous code force-injected + // only `prelude`, leaving `kernel_stub` and any future + // kernel-tier module unreachable from consumers even though + // the pre-pass freely produces such qualifiers. if m.name != "prelude" { import_map .entry("prelude".to_string()) .or_insert_with(|| "prelude".to_string()); } + for km in ws.modules.values().filter(|km| km.kernel) { + if km.name != m.name { + import_map + .entry(km.name.clone()) + .or_insert_with(|| km.name.clone()); + } + } env.imports = import_map; env.current_module = m.name.clone(); @@ -3422,12 +3465,27 @@ pub(crate) fn synth( // pulled across the boundary unify against // qualified-form ctors and types in the consumer // module. - let owner_types = env - .module_types - .get(&target_module) - .cloned() - .unwrap_or_default(); - let qualified = qualify_local_types(&raw_ty, &target_module, &owner_types); + // + // Same-module case: the pre-pass leaves own-module + // names bare (see `qualify_workspace_types`'s + // own-module rule), and the local `Term::Ctor` arm + // (~line 3644) also returns bare names. Qualifying + // here would produce `.T` for sites the rest + // of the resolver represents as bare `T`, tripping + // a phantom type-mismatch on a same-module + // `(app Type.member …)` call. Fieldtest F1 surfaced + // this asymmetry; the fix is to no-op the qualifier + // when `target_module == env.current_module`. + let qualified = if target_module == env.current_module { + raw_ty + } else { + let owner_types = env + .module_types + .get(&target_module) + .cloned() + .unwrap_or_default(); + qualify_local_types(&raw_ty, &target_module, &owner_types) + }; // Dot-qualified `prefix.suffix`: the unqualified name in // the owner module is `suffix`. (qualified, Some((target_module, suffix.to_string()))) diff --git a/crates/ailang-check/tests/env_construction_pin.rs b/crates/ailang-check/tests/env_construction_pin.rs index 4fcf269..c2dc79d 100644 --- a/crates/ailang-check/tests/env_construction_pin.rs +++ b/crates/ailang-check/tests/env_construction_pin.rs @@ -72,8 +72,20 @@ fn build_env_inline_pre_refactor(ws: &ailang_core::workspace::Workspace) -> Env } env.module_types = module_types; - // env.module_imports — per-module alias map. Iter 23.1: every - // non-prelude module implicitly imports the prelude module. + // env.module_imports — per-module alias map. Iter 23.1 added + // the implicit `prelude` import. bugfix-prepass-resolver- + // asymmetry (F3) generalised it: every workspace module flagged + // `kernel: true` is implicitly imported into every non-self + // module (mirrors the loader filter at + // `crates/ailang-surface/src/loader.rs`). The literal + // `"prelude"` injection stays for back-compat with unit-test + // workspaces that construct a `kernel: false` prelude. + let kernel_modules: Vec = ws + .modules + .values() + .filter(|m| m.kernel) + .map(|m| m.name.clone()) + .collect(); for m in ws.modules.values() { let mut import_map: BTreeMap = BTreeMap::new(); for imp in &m.imports { @@ -85,6 +97,11 @@ fn build_env_inline_pre_refactor(ws: &ailang_core::workspace::Workspace) -> Env .entry("prelude".to_string()) .or_insert_with(|| "prelude".to_string()); } + for k in &kernel_modules { + if &m.name != k { + import_map.entry(k.clone()).or_insert_with(|| k.clone()); + } + } env.module_imports.insert(m.name.clone(), import_map); }