From a163c8c34a2569c4198370f9b6862b3e280b4506 Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 28 May 2026 19:36:36 +0200 Subject: [PATCH] =?UTF-8?q?GREEN:=20pre-pass/resolver=20asymmetry=20?= =?UTF-8?q?=E2=80=94=20same-module=20bare=20+=20kernel-tier=20qualifier=20?= =?UTF-8?q?acceptance=20(closes=20F1,=20F3)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two minimal edits in ailang-check that bring the resolver's acceptance set into line with what prep.1's workspace pre-pass (`prepare_workspace_for_check`) actually produces. The pre-pass itself is unchanged — its qualification rules are correct per spec § "Realisation mechanism — workspace pre-pass". RED tests landed in 4d39fdc; both turn GREEN, both fieldtest fixtures that surfaced the bugs now `ail check` clean. F1 — same-module type-scoped call (kem_2b_min_repro.ail). The dot-qualified `Term::Var` arm in `synth_term` (`crates/ailang-check/src/lib.rs` ~line 3425) was unconditionally rewriting the resolved fn signature via `qualify_local_types`, so a call like `(app Counter.value c)` from inside Counter's home module produced a return type `.Counter` — but the matching `Term::Ctor` arm (~line 3644) and the pre-pass itself both leave own-module type-names bare. The two halves of the resolver disagreed. Fix: branch on `target_module == env.current_module` — when true, skip the qualification (the raw type is already in the form the rest of the resolver speaks); when false, qualify as before. `owner_types` lookup moved inside the else-branch since it's only consulted when qualification runs. A short comment names the pre-pass and the sibling Term::Ctor arm so a future reader sees the three-way symmetry. F3 — kernel-tier qualifier acceptance (kem_3_stub_consumer.ail). The env-builder paths `build_check_env` (~line 1653) and `check_in_workspace` (~line 1807) force-injected only `"prelude"` into `env.imports` / `env.module_imports`. The loader meanwhile derives the implicit-imports list from `modules.values().filter(|m| m.kernel)` (since prep.3) — so `kernel_stub` flows into runtime resolution but not into the checker's qualifier-validity check (~line 1968). Bare `StubT` got qualified by the pre-pass to `kernel_stub.StubT`, then bounced off the validity check as "unknown module prefix". Fix at both sites: keep the unconditional `"prelude"` literal injection AND additively insert every workspace module with `kernel: true` into the per-module import map (skip self-injection). Idempotent for production (where prelude also carries `kernel: true`) and preserves the `bare_name_resolves_through_implicit_import_to_free_fn` unit-test contract — that test deliberately constructs a prelude module with `kernel: false` to pin the legacy "prelude is always implicit" guarantee per se, independent of the kernel flag. Mirrors the loader's kernel-flag filter, making the env-builder and the loader speak the same set. Sibling pin `crates/ailang-check/tests/env_construction_pin.rs` (the frozen-reproduction copy of `build_check_env`'s `module_imports` loop) updated in lockstep so it remains a meaningful drift detector after the env-builder change. The pin is intentionally designed to track legitimate behavioural changes. Verification: - tests::type_scoped_call_in_same_module_resolves GREEN - tests::kernel_tier_module_qualifier_resolves_… GREEN - examples/fieldtest/kem_2b_min_repro.ail ail check ok - examples/fieldtest/kem_3_stub_consumer.ail ail check ok - cargo test --workspace 666 / 0 (664 prior baseline + 2 RED→GREEN this iter) Implementer notes: one re-loop on the F3 site after the first edit replaced the legacy "prelude" literal injection wholesale with the kernel-flag filter — that broke the unit-test contract above. Restored the literal AND added the filter on top per the "don't adapt tests to bugs" memory. No spec-review or quality-review loops. prep.1's pre-pass design (spec § "Realisation mechanism") was correct as written — the symmetry between owner-side `qualify_local_types` and consumer-side `prepare_workspace_for_check` holds. What was missing was uniform resolver-side acceptance of the qualifiers the pre-pass produces. With these two edits, the following equivalences hold throughout the checker: bare T ≡ .T (F1, same-module rule) bare T ≡ .T (F3, kernel-tier rule) via the loader-driven implicit-imports list that now drives both the checker's import map and the type-validity check. --- crates/ailang-check/src/lib.rs | 98 +++++++++++++++---- .../tests/env_construction_pin.rs | 21 +++- 2 files changed, 97 insertions(+), 22 deletions(-) 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); }