feat(grammar): sound module-qualified type & effect paths, dot separator (Refs #228)

The type/effect grammar had no module-qualified path production, so
`Externs.Res` / `prelude.Option` / any `Pkg.Type` in type or effect
position failed `parse error` at the `.` — contradicting ADR-011 (real
modules with qualified paths). This adds full, SOUND module-qualified
paths in type and effect position, with `.` as the canonical separator
(`::` stays value/import per ADR-011); decision recorded as ADR-014.

Resolution is by sound module-scoped member lookup, never flat scope:
load module `[A;B]` through the loader, resolve+typecheck it as an
import would, then look the member up *inside that module's own
resolved symbols*, requiring Public/PubCrate and the right kind
(SKType / SKEffect). Unknown/wrong module, missing member, private
member, or wrong-kind member is a resolution error at the use-site
span — never a parse error and never silently accepted.

- lib/ast.ml: `ident` gains `modpath : string list` ([]=unqualified);
  add `mk_ident` helper so synthetic idents set the field in one place.
- lib/parser.mly: `mk_qualified_ident`; `path_seg`/`module_prefix`/
  `qualified_type_path` helpers; qualified bare/[args]/<args> forms for
  types and bare/[args] for effects. Module-prefix segments accept
  lower OR upper case (stdlib modules are `prelude`/`option` as well as
  `Network`/`Http`); member segment is upper_ident.
- lib/typecheck.ml: `lower_type_expr`/`lower_effect_expr` validate the
  qualified case via a loader-backed `qualified_member_check` threaded
  into the context; `Qualified_path_error` -> `QualifiedPathError` at
  the check_program boundary (same pattern as Effect_validation_error).
  A validated qualified effect's name is admitted as a declared effect
  (issue #59) so a sibling module's public effect is usable like a
  local one. Resolved representation is the canonical nominal
  type/effect — identical to the bare/imported form; the validation,
  not the representation, is the soundness gate. Typecheck/codegen
  otherwise unchanged.
- lib/resolve.ml: `make_qualified_member_check` built where the loader
  lives, inside the `resolve_and_typecheck_module` recursive group so
  transitively-qualified stdlib paths resolve too.
- bin/main.ml: thread the validator into the 6 patterned check_program
  calls (via the type_ctx returned by resolve_program_with_loader).
- Fixed ~10 internal direct `ident` record literals (trait/codegen_gc/
  borrow/verilog) to route through `Ast.mk_ident`.
- docs/specs/SETTLED-DECISIONS.adoc + .machine_readable/6a2/META.a2ml:
  ADR-014 (full stanza, same shape as ADR-011/012/013).
- tests/conformance/qualified-paths/{valid,invalid}: 5 conformance
  fixtures wired into the e2e gate (valid qualified type+effect;
  unknown module; private member; absent member).

Parser-conflict delta: ZERO. menhir --explain summary is byte-identical
to the pre-change parser — 21 shift/reduce states, 1 reduce/reduce
state, 68 s/r + 7 r/r arbitrarily resolved. The `upper_ident` vs
`upper_ident DOT ...` decision is the expected benign DOT shift
(Menhir shifts, disclosed per ADR-012); no new unexplained conflict.

Test gate: 258 -> 263 (5 new #228 cases), zero regressions. Adding
`modpath` to `ident` reflows every golden .expected AST dump;
regenerated — the span-normalised golden harness confirms no
structural change.

STAGE-C peer of #225 (typed-wasm Http) and #160 (C-spine). Language
decision is human-gated (ISSUE-CLOSURE): Refs #228, not Closes.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: claude

.machine_readable/6a2/META.a2ml

@@ -872,3 +872,94 @@ references = [
   "stdlib/Vscode.affine + packages/affine-vscode/mod.js (#205 thenableThen)",
   "typed-wasm ADR-004 (convergence / aggregate library; Ephapax)",
 ]
+
+[[adr]]
+id = "ADR-014"
+status = "accepted"
+date = "2026-05-18"
+title = "Module-qualified type & effect paths: dot separator, sound module-scoped member lookup"
+context = """
+The type/effect grammar had NO module-qualified path production.
+`Externs.Res` / `Pkg.Type` in type or effect position failed
+`parse error` at the `.`. `type_expr_primary` only had
+`upper_ident -> TyCon` / `upper_ident [..]/<..> -> TyApp`;
+`effect_term` only `ident -> EffVar` / `ident [..] -> EffCon`.
+`module_path` already parsed `ident (DOT ident)*` for module/use.
+ADR-011 settled real modules with qualified paths; the estate's
+Frontier-playbook ports pervasively write `Externs.Foo` in type/effect
+position, contradicting a grammar that could not represent it. An
+oracle audit (28 repos / 1176 .affine files) measured 498 DRIFT-SYNTAX
+files, dominated by exactly this unrepresentable qualified-path shape.
+"""
+decision = """
+A module-qualified path `A.B.C` is admissible in TYPE and EFFECT
+position. The dot `.` is the canonical separator for these paths;
+`::` remains value/import (ADR-011 unchanged). Module-prefix segments
+may be lower- OR upper-case (stdlib modules are `prelude`/`option`/
+`string`/`result` as well as `Network`/`Http`); the final segment is
+the type/effect member and is `upper_ident`.
+
+`A.B.C` resolves by SOUND MODULE-SCOPED MEMBER LOOKUP, never flat
+current scope:
+- load module `[A;B]` through the module loader;
+- resolve + type-check it exactly as an import would
+  (`Resolve.resolve_and_typecheck_module`);
+- look `C` up INSIDE that module's own resolved symbol table,
+  requiring `Public`/`PubCrate` and the right kind (`SKType` for
+  types, `SKEffect` for effects).
+An unknown/wrong module, a missing member, a private member, or a
+member of the wrong kind is a *resolution* error at the use-site span
+— not a parse error, never silently accepted. A validated qualified
+effect's name is admitted as a declared effect (issue #59) so a
+sibling module's public effect is usable like a local one.
+
+Design (ripple-minimised):
+- `ast.ml`: `ident` gains `modpath : string list` ([] = unqualified).
+- `parser.mly`: `mk_qualified_ident`; a `qualified_type_path` helper
+  (`module_prefix DOT upper_ident`); bare / [args] / <args> applied
+  forms for types, bare / [args] for effects.
+- `typecheck.ml`: `lower_type_expr`/`lower_effect_expr` handle the
+  qualified case via a loader-backed validator threaded into the
+  context (`qualified_member_check`), raising `Qualified_path_error`
+  -> `QualifiedPathError` at the `check_program` boundary (same
+  pattern as `Effect_validation_error`). Resolved representation is
+  the canonical nominal type/effect — identical to the bare/imported
+  form; the validation, not the representation, is the soundness gate.
+- `resolve.ml`: `make_qualified_member_check` built where the loader
+  lives; in the `resolve_and_typecheck_module` recursive group so
+  transitively-qualified stdlib paths resolve too.
+
+The `upper_ident` vs `upper_ident DOT …` choice is the expected
+benign DOT shift (Menhir shifts, ADR-012). Verified: parser-conflict
+summary UNCHANGED — 21 shift/reduce states, 1 reduce/reduce state,
+68 s/r + 7 r/r arbitrarily resolved, identical to the pre-change
+parser. No new unexplained conflict.
+"""
+consequences = """
+- Estate Frontier-playbook ports that write `Externs.Foo` /
+  `prelude.Option` in type/effect position now resolve soundly; the
+  oracle re-audit shows a large DRIFT-SYNTAX -> PASS/TYPE-ONLY shift.
+- Typecheck/codegen unchanged: a qualified ident is treated by its
+  resolved symbol exactly like an unqualified one.
+- Adding `modpath` to `ident` reflows every golden `.expected` AST
+  dump (regenerated; the span-normalised gate confirms no structural
+  change). 5 conformance cases added under
+  tests/conformance/qualified-paths/{valid,invalid}; the full gate is
+  green (258 -> 263, zero regressions).
+- STAGE-C peer of #225 (typed-wasm Http) and #160 (C-spine). Language
+  decision is human-gated (ISSUE-CLOSURE): Refs #228, NOT Closes.
+- Settled; do not reopen without amending this ADR.
+"""
+references = [
+  "https://github.com/hyperpolymath/affinescript/issues/228",
+  "https://github.com/hyperpolymath/affinescript/issues/225",
+  "https://github.com/hyperpolymath/affinescript/issues/160",
+  "docs/specs/SETTLED-DECISIONS.adoc (ADR-014 section)",
+  "lib/ast.ml (ident.modpath)",
+  "lib/parser.mly (qualified_type_path; mk_qualified_ident)",
+  "lib/typecheck.ml (lower_type_expr/lower_effect_expr; qualified_member_check)",
+  "lib/resolve.ml (make_qualified_member_check; module-scoped lookup)",
+  "tests/conformance/qualified-paths/{valid,invalid}",
+  "ADR-011 (real modules with qualified paths)",
+  "ADR-012 (parser-conflict disclosure; benign DOT shift)",
+]

bin/main.ml

@@ -187,6 +187,7 @@ let check_file face json path =
         resolve_refs := List.rev resolve_ctx.references;
         (match Affinescript.Typecheck.check_program
                  ~import_types:type_ctx.Affinescript.Typecheck.name_types
+                 ?qualified_member_check:type_ctx.Affinescript.Typecheck.qualified_member_check
                  resolve_ctx.symbols prog with
         | Error e ->
           add (Affinescript.Json_output.of_type_error e)
@@ -234,6 +235,7 @@ let check_file face json path =
       | Ok (resolve_ctx, type_ctx) ->
         (match Affinescript.Typecheck.check_program
                  ~import_types:type_ctx.Affinescript.Typecheck.name_types
+                 ?qualified_member_check:type_ctx.Affinescript.Typecheck.qualified_member_check
                  resolve_ctx.symbols prog with
         | Error e ->
           Format.eprintf "@[<v>%s@]@."
@@ -497,6 +499,7 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc
       | Ok (resolve_ctx, import_type_ctx) ->
         (match Affinescript.Typecheck.check_program
                  ~import_types:import_type_ctx.Affinescript.Typecheck.name_types
+                 ?qualified_member_check:import_type_ctx.Affinescript.Typecheck.qualified_member_check
                  resolve_ctx.symbols prog with
         | Error e ->
           add (Affinescript.Json_output.of_type_error e)
@@ -716,6 +719,7 @@ let compile_file face json wasm_gc vscode_ext vscode_adapter vscode_no_lc
       | Ok (resolve_ctx, import_type_ctx) ->
         (match Affinescript.Typecheck.check_program
                  ~import_types:import_type_ctx.Affinescript.Typecheck.name_types
+                 ?qualified_member_check:import_type_ctx.Affinescript.Typecheck.qualified_member_check
                  resolve_ctx.symbols prog with
         | Error e ->
           Format.eprintf "@[<v>%s@]@."
@@ -1060,6 +1064,7 @@ let compile_to_wasm_module face path
     | Ok (resolve_ctx, import_type_ctx) ->
       match Affinescript.Typecheck.check_program
               ~import_types:import_type_ctx.Affinescript.Typecheck.name_types
+                 ?qualified_member_check:import_type_ctx.Affinescript.Typecheck.qualified_member_check
               resolve_ctx.symbols prog with
       | Error e ->
         Format.eprintf "%s: %s@." path
@@ -1120,6 +1125,7 @@ let verify_file face path =
     | Ok (resolve_ctx, import_type_ctx) ->
       (match Affinescript.Typecheck.check_program
                ~import_types:import_type_ctx.Affinescript.Typecheck.name_types
+                 ?qualified_member_check:import_type_ctx.Affinescript.Typecheck.qualified_member_check
                resolve_ctx.symbols prog with
       | Error e ->
         Format.eprintf "%s@."

docs/specs/SETTLED-DECISIONS.adoc

@@ -243,3 +243,38 @@ agreed async ABI for the typed-wasm convergence layer; Ephapax is a
 co-stakeholder (typed-wasm ADR-004). Delivered as 4 incremental,
 gated PRs. Full design in `docs/specs/async-on-wasm-cps.adoc`; full ADR
 in `.machine_readable/6a2/META.a2ml` (ADR-013).
+
+== Module-Qualified Type & Effect Paths: Dot Separator, Sound Member Lookup (ADR-014)
+
+A module-qualified path `A.B.C` is admissible in *type* and *effect*
+position, not only value/import position. The dot `.` is the canonical
+separator for these paths; `::` remains the value/import separator
+(ADR-011 is unchanged). Module-prefix segments may be lower- or
+upper-case (real stdlib modules are `prelude`, `option`, `string`,
+`result` as well as `Network`, `Http`); the final member segment is
+the type/effect name.
+
+`A.B.C` resolves by *sound module-scoped member lookup*, never by flat
+current scope: the compiler loads module `[A;B]` through the module
+loader, resolves and type-checks it exactly as an import would, then
+looks `C` up *inside that module's own resolved symbol table*,
+requiring it to be `Public`/`pub(crate)` and of the right kind
+(`SKType` for types, `SKEffect` for effects). An unknown or wrong
+module, a missing member, a private member, or a member of the wrong
+kind is a *resolution* error reported at the use-site span — not a
+parse error and never silently accepted. Soundness comes from looking
+the member up within the named module, so importing `C` flatly does
+not make a bogus `A.B.C` resolve. A validated qualified effect's name
+is admitted as a declared effect (issue #59), so a sibling module's
+public effect is usable exactly like a locally declared one.
+
+This is consistent with ADR-011 (real modules with qualified paths)
+and ADR-012 (the `upper_ident` vs `upper_ident DOT …` choice is the
+expected benign DOT shift; the masked-conflict count is unchanged —
+21 shift/reduce states, 1 reduce/reduce state, identical to the
+pre-change parser). Typecheck/codegen are unchanged: a qualified
+ident is treated by its resolved symbol exactly like an unqualified
+one (the validation, not the representation, is the soundness gate).
+
+Refs issue #228 (language decision human-gated; not auto-closed). Full
+ADR in `.machine_readable/6a2/META.a2ml` (ADR-014).

lib/ast.ml

@@ -3,13 +3,31 @@
 
 (** Abstract Syntax Tree for AffineScript *)
 
-(** Identifiers *)
+(** Identifiers.
+
+    [modpath] holds a module-qualified prefix for type/effect paths
+    (issue #228, ADR-014).  [modpath = []] means the identifier is
+    unqualified (the overwhelming majority of idents).  A qualified
+    type/effect path like [A.B.C] is represented as
+    [{ name = "C"; modpath = ["A"; "B"]; span }], where [name] is the
+    final member segment and [modpath] is the module path that the
+    member must be looked up *within* (sound module-scoped resolution,
+    not flat-scope). The dot [.] is the canonical separator; [::]
+    remains value/import per ADR-011. *)
 type ident = {
   name : string;
   span : Span.t;
+  modpath : string list;
 }
 [@@deriving show, eq]
 
+(** Construct an unqualified identifier ([modpath = []]). Used by
+    compiler-internal synthetic idents (trait desugaring, codegen
+    helpers, …) so the [modpath] field (issue #228) is set in exactly
+    one place rather than scattered as record literals. *)
+let mk_ident ?(span : Span.t = Span.dummy) (name : string) : ident =
+  { name; span; modpath = [] }
+
 (** Quantity annotations for QTT *)
 type quantity =
   | QZero    (** Erased - compile time only *)

lib/borrow.ml

@@ -573,7 +573,7 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr :
     let borrow_span = expr_span (ExprLambda lam) in
     let* () = List.fold_left (fun acc name ->
       let* () = acc in
-      match expr_to_place symbols (ExprVar { name; span = borrow_span }) with
+      match expr_to_place symbols (ExprVar (mk_ident ~span:borrow_span name)) with
       | Some place ->
         (* Check the place is not already moved before we borrow it. *)
         let* _borrow = record_borrow state place Shared borrow_span in

lib/codegen_gc.ml

@@ -430,7 +430,7 @@ let rec gen_gc_expr (ctx : gc_ctx) (expr : expr) : (gc_ctx * gc_instr list) cg_r
           | Some e -> e
           | None   ->
             let i = List.length rev_codes in
-            ExprVar { name = List.nth field_names i; span = Span.dummy }
+            ExprVar (mk_ident (List.nth field_names i))
         in
         let* (c', code) = gen_gc_expr c fexpr in
         Ok (c', code :: rev_codes)

lib/parser.mly

@@ -18,7 +18,15 @@ let mk_span startpos endpos =
   Span.make ~file ~start_pos ~end_pos
 
 let mk_ident name startpos endpos =
-  { name; span = mk_span startpos endpos }
+  { name; span = mk_span startpos endpos; modpath = [] }
+
+(* issue #228 / ADR-014: a module-qualified type/effect path `A.B.C`.
+   [path] is the module prefix (["A"; "B"]) and [name] is the final
+   member segment ("C") that resolution must look up *within* that
+   module's resolved public symbols (sound module-scoped lookup, not
+   flat current scope). The span covers the whole dotted path. *)
+let mk_qualified_ident (path : string list) name startpos endpos =
+  { name; span = mk_span startpos endpos; modpath = path }
 
 (* issue #122 v2: inherent-impl support. The old grammar pre-committed to
    `impl_trait_ref? self_ty` where both alternatives start with an ident,
@@ -450,6 +458,26 @@ type_expr_primary:
   | MUT ty = type_expr_primary { TyMut ty }
   | name = lower_ident { TyVar (mk_ident name $startpos $endpos) }
   | name = upper_ident { TyCon (mk_ident name $startpos $endpos) }
+  /* issue #228 / ADR-014: module-qualified type path `A.B.C`. The
+     prefix segments `A.B` are the module path; the last segment `C`
+     is the type member, resolved *within* that module's public
+     symbols (sound module-scoped lookup — see lib/typecheck.ml
+     lower_type_expr / lib/resolve.ml). `.` is canonical (ADR-011
+     keeps `::` for value/import). The `upper_ident` vs
+     `upper_ident DOT ...` choice is the expected benign shift on
+     DOT (Menhir shifts; disclosed per ADR-012). Bare / [args] /
+     <args> applied forms all supported. */
+  | qp = qualified_type_path
+    { let (prefix, last, sp, ep) = qp in
+      TyCon (mk_qualified_ident prefix last sp ep) }
+  | qp = qualified_type_path
+    LBRACKET args = separated_nonempty_list(COMMA, type_arg) RBRACKET
+    { let (prefix, last, sp, ep) = qp in
+      TyApp (mk_qualified_ident prefix last sp ep, args) }
+  | qp = qualified_type_path
+    LT args = separated_nonempty_list(COMMA, type_arg) GT
+    { let (prefix, last, sp, ep) = qp in
+      TyApp (mk_qualified_ident prefix last sp ep, args) }
   | name = upper_ident LBRACKET args = separated_nonempty_list(COMMA, type_arg) RBRACKET
     { TyApp (mk_ident name $startpos(name) $endpos(name), args) }
   /* Angle-bracket alias for type application: `Option<T>` ≡ `Option[T]`,
@@ -569,6 +597,19 @@ effect_term:
   | name = ident { EffVar name }
   | name = ident LBRACKET args = separated_list(COMMA, type_arg) RBRACKET
     { EffCon (name, args) }
+  /* issue #228 / ADR-014: module-qualified effect path `A.B.Eff`.
+     Same module-scoped soundness as qualified types: the prefix is a
+     module path, the last segment the effect member resolved within
+     it. Reuses `qualified_type_path` (module + member both upper —
+     stdlib effects are `IO`/`Mut`/`Throws`, module names upper). The
+     applied `[args]` form mirrors the parametric-effect rule above. */
+  | qp = qualified_type_path
+    { let (prefix, last, sp, ep) = qp in
+      EffVar (mk_qualified_ident prefix last sp ep) }
+  | qp = qualified_type_path
+    LBRACKET args = separated_list(COMMA, type_arg) RBRACKET
+    { let (prefix, last, sp, ep) = qp in
+      EffCon (mk_qualified_ident prefix last sp ep, args) }
 
 /* ========== Traits ========== */
 
@@ -1062,6 +1103,32 @@ pattern_rest:
 
 /* ========== Helpers ========== */
 
+/* issue #228 / ADR-014: a module-qualified type/effect path
+   `A.B.C`. Returns (module-prefix, member, startpos, endpos). The
+   member (last segment) is the type/effect name and is always
+   `upper_ident` (stdlib types `Option`/`Result`/… and effects
+   `IO`/`Mut`/`Throws` are uppercase; a lowercase final segment is
+   not a valid type/effect anyway). The module-prefix segments may be
+   *either* case because real stdlib module names are lowercase
+   (`prelude`, `option`, `string`, `result`) as well as uppercase
+   (`Network`, `Http`) — this mirrors `module_path`/`use`, which
+   accept `ident` (both cases). Length is >=2 (>=1 prefix segment +
+   the member), enforced by the `module_prefix DOT upper_ident`
+   shape. Left-recursive prefix. The `upper_ident` vs
+   `upper_ident DOT ...` decision is the expected benign DOT shift
+   (Menhir shifts; disclosed per ADR-012). */
+path_seg:
+  | s = lower_ident { s }
+  | s = upper_ident { s }
+
+module_prefix:
+  | s = path_seg { [s] }
+  | p = module_prefix DOT s = path_seg { p @ [s] }
+
+qualified_type_path:
+  | p = module_prefix DOT m = upper_ident
+    { (p, m, $startpos, $endpos) }
+
 ident:
   | name = lower_ident { mk_ident name $startpos $endpos }
   | name = upper_ident { mk_ident name $startpos $endpos }