RED: same-module type-scoped call + kernel-tier qualifier — pre-pass/resolver asymmetry (refs F1, F3)

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
      <this>.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
      `<this>.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 (`<this>.T` for F1, `<kernel_mod>.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

@@ -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 `<Type>.<member>` made from inside `<Type>`'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 `<this_module>.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
+    /// `<this_module>.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:?}"
+        );
+    }
 }