feat(typecheck): module-qualified type/effect path resolution (ADR-014, Refs #228) (#447)

## Summary

Symmetric to #178 (`Resolve.lower_qualified_value_paths`) at the
value-path layer: when a folded `Mod::T` reaches `lower_type_expr` /
`lower_effect_expr`, the leading `Mod::` qualifier is stripped iff `Mod`
was introduced by `use Mod;`. Otherwise a clear `UnknownModule` error is
raised — replacing the pre-existing silent typecheck-pass (type
position) and misleading `declare \`effect ...\`` hint (effect
position).

Closes the resolution half of the #228 work whose parser half landed in
#241 (ADR-014).

## What changes

- `type_error`: `UnknownModule of string` constructor + formatter (cites
ADR-014/#228, suggests `use M;` / `use M::{Item};`)
- `Module_resolution_error` exception caught at `check_program` boundary
(mirrors `Effect_validation_error`)
- `context.module_quals`: populated at `check_program` entry from
`prog.prog_imports` (`ImportSimple` only — matches value-path semantics
in `Resolve.import_qualifiers`)
- `strip_module_qualifier` helper applied in `TyCon` / `TyApp` arms of
`lower_type_expr` and the `resolve` helper of `lower_effect_expr`. No
AST walk — the lowering chokepoints already visit every type/effect
site.

## Before / after

| Source | Before | After |
|---|---|---|
| `pub fn f(x: NoSuchMod.Thing) -> ()` | silently passes typecheck |
`Unknown module 'NoSuchMod' in qualified type/effect reference (ADR-014,
#228). Add \`use NoSuchMod;\` ...` |
| `pub fn f() -{NoSuchMod.IO}-> ()` | `Unknown effect 'NoSuchMod::IO'.
... declare it with \`effect NoSuchMod::IO;\`` | same `UnknownModule`
text as above |
| `use Ajv; pub fn f(x: Ajv.Schema) -> ()` | passes (TyCon lenient) |
passes (strip → bare lenient lookup, unchanged outcome) |
| `pub fn f(x: Int) -> ()` | passes | passes (regression guard) |

## Tests

`test/test_qualified_paths.ml` — 6 alcotest cases, all green:
- qualified type + `use` (both `.` and `::`) → passes
- qualified type, no `use` → `UnknownModule`
- qualified effect, no `use` → `UnknownModule` (not `UnknownEffect`)
- bare TyCon unchanged
- qualified reserved effect (`Net`) + `use` → strips & resolves into the
reserved-effect path

Full suite: `dune build @test/runtest` → **352/352 OK**.

## Out of scope (surfaced in #228 design comment)

These are real but separate; I'll file follow-ups if the seam-analyst
note isn't already tracked elsewhere:
- lowercase-module qualified refs (`json.Value`) still parse-error —
`qualified_type_name` head requires `upper_ident` while stdlib has
lowercase `module json;` / `option;` / `prelude;`
- `use A.B;` registers only `B` as the qualifier (last segment)
- `use A::{Item}` (multi-segment + brace-list) parse-errors
- bare unknown TyCons silently pass typecheck — pre-existing leniency,
much broader than #228; would change behaviour for many existing files

## Refs

Refs #228 (this is the resolution slice; parser slice was #241)
Refs hyperpolymath/standards#124 (estate proof-debt / language-readiness
umbrella)

Author: hyperpolymath

lib/typecheck.ml

@@ -112,6 +112,11 @@ type type_error =
           function's explicitly declared effect row (issue #59). Only
           raised when a row is declared; an undeclared row stays
           permissive under tracking-only v1. *)
+  | UnknownModule of string
+      (** A module-qualified type/effect reference (`Mod.T` / `Mod::E`)
+          named a module qualifier not introduced by any `use` in the
+          current program (ADR-014, #228). Symmetric to the value-path
+          resolution check done by #178. *)
 
 (* Known exports of stdlib/prelude.affine. Mirrors the same list in
    lib/face.ml — when an UnboundVariable fires at type-check time with
@@ -176,6 +181,12 @@ let show_type_error = function
        performs `Partial` — add it to the row, e.g. /{%s}."
       inferred declared
       (if declared = "" then "Partial" else declared ^ ", Partial")
+  | UnknownModule m ->
+    Printf.sprintf
+      "Unknown module '%s' in qualified type/effect reference (ADR-014, #228). \
+       Add `use %s;` to bring the module into scope, or `use %s::{Item};` to \
+       import items unqualified."
+      m m m
 
 let format_type_error = show_type_error
 
@@ -184,6 +195,12 @@ let format_type_error = show_type_error
     (lowering is not in the result monad). *)
 exception Effect_validation_error of string
 
+(** Raised by [strip_module_qualifier] when a qualified type/effect
+    reference names a module that no `use` decl introduced; caught at
+    [check_program] and converted to [UnknownModule]. Mirrors the
+    [Effect_validation_error] exception/boundary pattern. *)
+exception Module_resolution_error of string
+
 (** {1 Context} *)
 
 (** Type checking context.
@@ -217,6 +234,15 @@ type context = {
       NOT yet consulted by codegen — S3 threads & switches the WasmGC
       CPS boundary predicate onto it (the structural recogniser remains
       the sound table-miss fallback). *)
+  module_quals : (string, unit) Hashtbl.t;
+  (** ADR-014 / #228: set of module-name qualifiers introduced by
+      [`use Mod;`] (ImportSimple) decls in the current program. Used by
+      [lower_type_expr]/[lower_effect_expr] to strip a qualified
+      `Mod::T` reference back to `T` when `Mod` is in scope, or raise
+      [Module_resolution_error] when it isn't. Symmetric to the
+      value-path lowering done by [Resolve.lower_qualified_value_paths]
+      (#178). Populated at [check_program] entry from
+      [prog.prog_imports]. *)
 }
 
 type 'a result = ('a, type_error) Result.t
@@ -248,8 +274,31 @@ let create_context (symbols : Symbol.t) : context =
     trait_registry = Trait.create_registry ();
     declared_effects = Hashtbl.create 16;
     call_effects = Hashtbl.create 64;
+    module_quals = Hashtbl.create 4;
   }
 
+(** ADR-014 / #228. Strip a leading `Mod::` qualifier from a folded
+    type/effect name. Returns the unqualified tail when `Mod` was
+    introduced by a `use Mod;` decl; raises [Module_resolution_error]
+    when the qualifier is unknown; passes the name through unchanged
+    when not qualified. Only the first `::`-separated head is treated
+    as a module qualifier — deeper segments (`A::B::T`) carry through
+    unchanged so a nested module reference still errors symmetrically
+    when its head isn't in scope. *)
+let strip_module_qualifier (ctx : context) (name : string) : string =
+  match String.index_opt name ':' with
+  | None -> name
+  | Some _ ->
+    let parts = String.split_on_char ':' name
+                |> List.filter (fun s -> s <> "") in
+    (match parts with
+     | head :: (_ :: _ as rest) ->
+       if Hashtbl.mem ctx.module_quals head then
+         String.concat "::" rest
+       else
+         raise (Module_resolution_error head)
+     | _ -> name)
+
 (** Enter a deeper let-level. *)
 let enter_level (ctx : context) : unit =
   ctx.level <- ctx.level + 1
@@ -428,6 +477,7 @@ let rec lower_type_expr (ctx : context) (te : type_expr) : ty =
         tv
     end
   | TyCon { name; _ } ->
+    let name = strip_module_qualifier ctx name in
     begin match name with
       | "Int" -> ty_int
       | "Float" -> ty_float
@@ -443,6 +493,7 @@ let rec lower_type_expr (ctx : context) (te : type_expr) : ty =
         end
     end
   | TyApp ({ name; _ }, args) ->
+    let name = strip_module_qualifier ctx name in
     let head = match Hashtbl.find_opt ctx.type_env name with
       | Some ty -> ty
       | None -> TCon name
@@ -485,6 +536,7 @@ and lower_effect_expr (ctx : context) (ee : effect_expr) : eff =
      user-declared (`effect <name>;`) → kept as written; anything else
      is rejected so contributors cannot silently invent effect names. *)
   let resolve (name : string) : eff =
+    let name = strip_module_qualifier ctx name in
     if name = "Pure" then EPure
     else match Effect.canonical_effect_name name with
       | Some canonical -> ESingleton canonical
@@ -1909,6 +1961,20 @@ let check_program ?(import_types : (string, scheme) Hashtbl.t option)
   try
   let ctx = create_context symbols in
   register_builtins ctx;
+  (* ADR-014 / #228: record `use Mod;` qualifiers so qualified type/effect
+     references can be stripped & resolved (or rejected with a clear
+     UnknownModule error). Only [ImportSimple] binds a qualifier; List/Glob
+     imports bring names unqualified, matching [Resolve.import_qualifiers]
+     for value paths. *)
+  List.iter (fun imp -> match imp with
+    | Ast.ImportSimple (path, alias) ->
+      let name = match alias with
+        | Some id -> id.name
+        | None -> (match List.rev path with id :: _ -> id.name | [] -> "")
+      in
+      if name <> "" then Hashtbl.replace ctx.module_quals name ()
+    | Ast.ImportList _ | Ast.ImportGlob _ -> ()
+  ) prog.prog_imports;
   Option.iter (fun tbl ->
     Hashtbl.iter (fun name sc -> Hashtbl.replace ctx.name_types name sc) tbl
   ) import_types;
@@ -1957,4 +2023,6 @@ let check_program ?(import_types : (string, scheme) Hashtbl.t option)
       Error (QuantityError (qerr, span))
     end
   | Error e -> Error e
-  with Effect_validation_error name -> Error (UnknownEffect name)
+  with
+  | Effect_validation_error name -> Error (UnknownEffect name)
+  | Module_resolution_error m -> Error (UnknownModule m)

test/test_main.ml

@@ -13,4 +13,5 @@ let () =
       ("Effects (#59)", Test_effects.tests);
       ("Effect-sites (#234, ADR-016)", Test_effect_sites.tests);
       ("TW L13 isolation (#10)", Test_tw_isolation.tests);
+      ("Qualified paths (#228, ADR-014)", Test_qualified_paths.tests);
     ] @ Test_e2e.tests @ Test_stdlib_aot.tests)

test/test_qualified_paths.ml

@@ -0,0 +1,119 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Copyright (c) 2026 Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk> *)
+
+(** ADR-014 / #228 — module-qualified type/effect path resolution.
+
+    The parser (after #241) accepts `Pkg.T` / `Pkg::T` (mixed seps) at
+    type and effect positions, folding the segments into a canonical
+    `::`-joined name. This test module exercises the *resolution*
+    counterpart shipped here: the typechecker strips the leading `Mod::`
+    qualifier when `Mod` was introduced by `use Mod;`, and raises a
+    clear [UnknownModule] error when it was not. Symmetric to
+    [Resolve.lower_qualified_value_paths] (#178, value position).
+*)
+
+open Affinescript
+
+(** parse -> resolve -> typecheck an inline source string. *)
+let frontend (src : string) : (unit, string) result =
+  let open Result in
+  let ( let* ) = bind in
+  let* prog =
+    try Ok (Parse_driver.parse_string ~file:"<test_qualified_paths>" src)
+    with
+    | Parse_driver.Parse_error (m, sp) ->
+      Error (Printf.sprintf "Parse error at %s: %s" (Span.show sp) m)
+    | e -> Error (Printf.sprintf "Unexpected: %s" (Printexc.to_string e))
+  in
+  let loader = Module_loader.create (Module_loader.default_config ()) in
+  let* resolve_ctx =
+    match Resolve.resolve_program_with_loader prog loader with
+    | Ok (rc, _) -> Ok rc
+    | Error (e, _) -> Error ("Resolution error: " ^ Resolve.show_resolve_error e)
+  in
+  match Typecheck.check_program resolve_ctx.symbols prog with
+  | Ok _ -> Ok ()
+  | Error e -> Error ("Type error: " ^ Typecheck.format_type_error e)
+
+let contains ~needle s =
+  let nl = String.length needle and sl = String.length s in
+  let rec go i = i + nl <= sl && (String.sub s i nl = needle || go (i + 1)) in
+  nl = 0 || go 0
+
+(* `use Mod;` + qualified type ref → strips back to bare name, passes
+   typecheck. `Ajv.Schema` lowers to `Schema` (current TyCon leniency
+   keeps the unknown name as an abstract `TCon` — that is the
+   pre-existing behaviour we deliberately do not change here). *)
+let qualified_type_with_use_passes () =
+  let src = "use Ajv;\npub fn f(x: Ajv.Schema) -> () { () }\n" in
+  match frontend src with
+  | Ok () -> ()
+  | Error m -> Alcotest.failf "expected Ok, got: %s" m
+
+(* `::` separator works the same as `.` (parser folds both). *)
+let qualified_type_with_double_colon_passes () =
+  let src = "use Ajv;\npub fn f(x: Ajv::Schema) -> () { () }\n" in
+  match frontend src with
+  | Ok () -> ()
+  | Error m -> Alcotest.failf "expected Ok, got: %s" m
+
+(* No `use`, qualified type ref → UnknownModule error mentioning the
+   exact qualifier and ADR-014 / #228 attribution. *)
+let qualified_type_unknown_module_rejected () =
+  let src = "pub fn f(x: NoSuchMod.Thing) -> () { () }\n" in
+  match frontend src with
+  | Ok () -> Alcotest.fail "expected UnknownModule error, got Ok"
+  | Error m ->
+    Alcotest.(check bool) "names the missing module" true
+      (contains ~needle:"NoSuchMod" m);
+    Alcotest.(check bool) "cites ADR-014 / #228" true
+      (contains ~needle:"#228" m);
+    Alcotest.(check bool) "suggests use" true
+      (contains ~needle:"use NoSuchMod" m)
+
+(* No `use`, qualified effect ref → same UnknownModule path (not the
+   permissive `Unknown effect` message). Pre-this-change the misleading
+   `declare \`effect NoSuchMod::IO;\`` hint was emitted. *)
+let qualified_effect_unknown_module_rejected () =
+  let src = "pub fn f() -{NoSuchMod.IO}-> () { () }\n" in
+  match frontend src with
+  | Ok () -> Alcotest.fail "expected UnknownModule error, got Ok"
+  | Error m ->
+    Alcotest.(check bool) "names the missing module" true
+      (contains ~needle:"NoSuchMod" m);
+    Alcotest.(check bool) "is the UnknownModule error not UnknownEffect" true
+      (contains ~needle:"#228" m)
+
+(* Bare (unqualified) type refs are unaffected — the strip helper is a
+   no-op when no `::` is present. Regression guard: this change must
+   not perturb existing single-name lookup behaviour. *)
+let bare_typecon_unaffected () =
+  let src = "pub fn f(x: Int) -> Int { x }\n\
+             pub fn g(y: SomeAbstract) -> () { () }\n" in
+  match frontend src with
+  | Ok () -> ()
+  | Error m -> Alcotest.failf "expected permissive Ok on bare names, got: %s" m
+
+(* Qualified ref with `use` but to a name that *is* a v1 effect after
+   stripping (`Net` is reserved) resolves into the reserved-effect path,
+   confirming the strip happens *before* the canonical-name lookup. *)
+let qualified_reserved_effect_with_use_passes () =
+  let src = "use Network;\npub fn f() -{Network.Net}-> () { () }\n" in
+  match frontend src with
+  | Ok () -> ()
+  | Error m -> Alcotest.failf "expected Ok, got: %s" m
+
+let tests = [
+  Alcotest.test_case "qualified type + use → passes" `Quick
+    qualified_type_with_use_passes;
+  Alcotest.test_case "qualified type + use (`::`) → passes" `Quick
+    qualified_type_with_double_colon_passes;
+  Alcotest.test_case "qualified type, no use → UnknownModule" `Quick
+    qualified_type_unknown_module_rejected;
+  Alcotest.test_case "qualified effect, no use → UnknownModule" `Quick
+    qualified_effect_unknown_module_rejected;
+  Alcotest.test_case "bare TyCon unaffected (regression)" `Quick
+    bare_typecon_unaffected;
+  Alcotest.test_case "qualified reserved effect + use → passes" `Quick
+    qualified_reserved_effect_with_use_passes;
+]