Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

GREEN: pre-pass/resolver asymmetry — same-module bare + kernel-tier qualifier acceptance (closes F1, F3)

Browse Source 
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
`<this>.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  ≡  <this-module>.T            (F1, same-module rule)
  bare T  ≡  <kernel-module>.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.
This commit is contained in:
Brummel
2026-05-28 19:36:36 +02:00
parent 4d39fdc9c0
commit a163c8c34a
2 changed files with 97 additions and 22 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/lib.rs
+78 -20
View File
@@ -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<String> = ws
.modules
.values()
.filter(|m| m.kernel)
.map(|m| m.name.clone())
.collect();
for m in ws.modules.values() {
let mut import_map: BTreeMap<String, String> = 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 `<this>.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())))
crates/ailang-check/tests/env_construction_pin.rs
+19 -2
View File
@@ -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<String> = ws
.modules
.values()
.filter(|m| m.kernel)
.map(|m| m.name.clone())
.collect();
for m in ws.modules.values() {
let mut import_map: BTreeMap<String, String> = 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);
}