From 4d39fdc9c01586ad066cead1983c03c2bc96d3dd Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 28 May 2026 19:29:02 +0200 Subject: [PATCH] =?UTF-8?q?RED:=20same-module=20type-scoped=20call=20+=20k?= =?UTF-8?q?ernel-tier=20qualifier=20=E2=80=94=20pre-pass/resolver=20asymme?= =?UTF-8?q?try=20(refs=20F1,=20F3)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two failing in-source tests added to ailang-check, both pinning the pre-pass / resolver mismatch surfaced by the fieldtest: tests::type_scoped_call_in_same_module_resolves F1: `(app Counter.value c)` from inside Counter's own home module must check clean. Currently fails with `[type-mismatch] main: type mismatch: expected .Counter, got Counter` because the dot-qualified Term::Var arm at lib.rs ~3430 unconditionally calls qualify_local_types on the resolved fn signature even when target_module == env.current_module, while the matching local Term::Ctor branch (~3644) returns bare `Counter`. The two halves of the resolver disagree on whether `.T` and bare `T` denote the same type. tests::kernel_tier_module_qualifier_resolves_without_explicit_import F3: `(con StubT (con Int))` in a consumer type signature must resolve without `(import kernel_stub)`. Currently fails with `[unknown-module] … unknown module prefix `kernel_stub` …` because env.imports / env.module_imports (built at ~1797 and ~1667) force-inject only `prelude` from the kernel-tier set; the pre-pass freely produces `kernel_stub.StubT` qualifiers that then bounce off the qualifier-validity check at ~1968. Shared root: in both bugs the workspace pre-pass synthesises a qualifier (`.T` for F1, `.T` for F3) that some downstream consumer of the resolver does not accept. The fix surface is the resolver-acceptance side in both cases — the pre-pass's qualification rules are correct per the spec's § "Realisation mechanism — workspace pre-pass". Implementation will be two minimal edits to distinct files-and-functions (no sweeping refactor). GREEN side handed to implement mini-mode in the next dispatch. --- crates/ailang-check/src/lib.rs | 142 +++++++++++++++++++++++++++++++++ 1 file changed, 142 insertions(+) diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index d40a949..7f2f698 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -8043,4 +8043,146 @@ mod tests { "expected NO param-not-in-restricted-set diagnostic, got {diags:?}" ); } + + /// Fieldtest F1 (kernel-extension-mechanics, 2026-05-28): + /// a type-scoped call `.` made from inside ``'s + /// own home module must check cleanly. The receiver `value` is a + /// `Def::Fn` in the same module as `Counter`; calling it via + /// `(app Counter.value c)` is the canonical form per + /// `docs/specs/0048-kernel-extension-mechanics.md` § "Iteration + /// prep.1 — Canonical form decision", which does NOT carve out + /// same-module sites as forbidden. Today this rejects with + /// `[type-mismatch] expected kem.Counter, got Counter` because the + /// dot-qualified arm at `synth` qualifies the resolved fn's param + /// type to `.Counter` via `qualify_local_types`, while + /// the local `Term::Ctor` synth (`Term::Ctor` arm in `synth_term`) + /// returns the bare `Counter` form for the same-module type — the + /// two halves of the resolver disagree on whether + /// `.T` and bare `T` are the same type. + #[test] + fn type_scoped_call_in_same_module_resolves() { + // Exact shape of examples/fieldtest/kem_2b_min_repro.ail — + // local Counter ADT with a `value` projector, called from + // `main` via `(app Counter.value c)` where `c` is built by + // `(term-ctor Counter MkCounter 41)`. + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "kem", + "imports": [], + "defs": [ + {"kind": "type", "name": "Counter", "ctors": [ + {"name": "MkCounter", "fields": [{"k": "con", "name": "Int"}]} + ]}, + // `value` projects a Counter to Int. Body is a + // constant — the bug is at the call site, the body + // shape is irrelevant. + {"kind": "fn", "name": "value", + "type": {"k": "fn", + "params": [{"k": "con", "name": "Counter"}], + "ret": {"k": "con", "name": "Int"}, + "effects": []}, + "params": ["c"], + "body": {"t": "lit", "lit": {"kind": "int", "value": 0}}}, + // `main` builds a Counter locally via term-ctor and + // calls `Counter.value` on it from the same module. + // Per spec § prep.1 "Canonical form decision" this + // is the canonical form and must check. + {"kind": "fn", "name": "main", + "type": {"k": "fn", "params": [], + "ret": {"k": "con", "name": "Int"}, + "effects": []}, + "params": [], + "body": {"t": "let", "name": "c", + "value": {"t": "ctor", "type": "Counter", + "ctor": "MkCounter", + "args": [{"t": "lit", + "lit": {"kind": "int", "value": 41}}]}, + "body": {"t": "app", + "fn": {"t": "var", "name": "Counter.value"}, + "args": [{"t": "var", "name": "c"}]}}} + ] + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("kem".to_string(), m); + let ws = Workspace { + entry: "kem".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + let diags = check_workspace(&ws); + assert!( + diags.is_empty(), + "same-module type-scoped call `Counter.value c` must check \ + cleanly (the canonical-form rule does not carve out \ + same-module sites); got {diags:?}" + ); + } + + /// Fieldtest F3 (kernel-extension-mechanics, 2026-05-28): + /// a `(con StubT (con Int))` reference in a consumer's type + /// signature, where `StubT` lives in a kernel-tier module + /// (`kernel: true`) and the consumer has NO explicit + /// `(import kernel_stub)`, must check cleanly. Spec §"Iteration + /// prep.3" promises kernel-tier types are accessible bare in + /// type position. The workspace pre-pass `qualify_workspace_types` + /// rewrites bare `StubT` to qualified `kernel_stub.StubT`; the + /// type-validity check at `synth_type` (line ~1968) then rejects + /// `kernel_stub` because only `prelude` is force-injected into + /// `env.imports` / `env.module_imports` (lines 1667–1671 and + /// 1797–1800) — kernel-tier modules OTHER than prelude are not + /// added to the per-module import map, so the qualifier they + /// receive from the pre-pass is unresolvable. + #[test] + fn kernel_tier_module_qualifier_resolves_without_explicit_import() { + let kernel_stub: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "kernel_stub", + "kernel": true, + "imports": [], + "defs": [ + {"kind": "type", "name": "StubT", "vars": ["a"], + "ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}]} + ] + })).unwrap(); + // Consumer references `StubT` bare in a type signature — no + // `(import kernel_stub)` declaration. Per spec § prep.3 the + // kernel-tier flag should make this resolve. + let consumer: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "consumer", + "imports": [], + "defs": [ + // The bug fires in the type-validity check on the + // declared param type `(con StubT (con Int))` — the + // body shape is irrelevant. A trivial Int-returning + // body keeps the test focused on the qualifier- + // resolution path. + {"kind": "fn", "name": "unwrap_int", + "type": {"k": "fn", + "params": [{"k": "con", "name": "StubT", + "args": [{"k": "con", "name": "Int"}]}], + "ret": {"k": "con", "name": "Int"}, + "effects": []}, + "params": ["s"], + "body": {"t": "lit", "lit": {"kind": "int", "value": 0}}} + ] + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("kernel_stub".to_string(), kernel_stub); + modules.insert("consumer".to_string(), consumer); + let ws = Workspace { + entry: "consumer".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + let diags = check_workspace(&ws); + assert!( + diags.is_empty(), + "kernel-tier `StubT` referenced bare in a consumer type \ + signature must resolve without an explicit \ + `(import kernel_stub)` declaration; got {diags:?}" + ); + } }