spec: revise canonical type names — AST is context-free

docs/specs/2026-05-10-canonical-type-names.md

@@ -1,220 +1,320 @@
-# Canonical Type Names — Internal Qualification — Design Spec
+# Canonical Type Names — AST is Context-Free — Design Spec
 
-**Date:** 2026-05-10
+**Date:** 2026-05-10 (revised 2026-05-11 after user clarification)
 **Status:** Draft — awaiting user spec review
 **Authors:** Brummel (orchestrator) + Claude
 
 ## Goal
 
-Establish a single, unambiguous canonical form for `Type::Con` names
-inside AILang's internal AST: every non-primitive `Type::Con` carries
-its defining-module prefix (`prelude.Ordering`, not bare `Ordering`).
-Bare names are accepted only in the `.ail.json` surface form as an
-LLM-author convenience; the loader resolves them once into canonical
-form. All downstream phases (typecheck, monomorphisation, codegen,
-content-hash) see the canonicalised AST.
+Establish the invariant that every AST object stands alone, hashable
+and reasonable about without an external module context. Concretely:
+**every non-primitive `Type::Con` in `.ail.json` is fully qualified
+(`module.Type`).** Bare names are a schema violation in JSON. The
+LLM-author surface (`.ailx` prose) continues to allow bare-local
+names, because the surrounding module context is right there in the
+source — the prose parser qualifies on read, the prose printer trims
+on write. The bare-vs-qualified divergence is resolved at the
+surface/JSON boundary, not inside the compiler.
 
-This closes a long-running design ambiguity in AILang: the language
-has accumulated five separate "imports-fallback" or "qualifier-helper"
-mechanisms over iters 15a / 23.1.3 / 23.1.4 / 23.2 / 23.2.4, each
-papering over the bare-vs-qualified divergence at a specific consumer
-site. The most recent symptom (iter 23.3 Task 4: prelude's
-`compare` returning bare `Ordering` to a user module, mismatching
-the qualified `prelude.Ordering` produced by the user-side
-Pattern::Ctor fallback) is a direct consequence: as long as some sites
-produce qualified names and others stay bare, values crossing module
-boundaries inevitably misalign.
+The user's directive on 2026-05-11: *"You can omit full qualification
+of local names in `.ailx` files because it follows directly from the
+module name — that's source code. But in the AST, i.e. in the data
+structure, i.e. in the `.ail.json` files, everything must be fully
+qualified. Every AST object must stand alone, without a module
+context."*
 
-The user's directive on 2026-05-10 (German, paraphrased): *"Bare names
-make sense as surface convention because the qualifier can always be
-omitted. But if qualifiers are MISSING internally, you have a problem."*
-This spec formalises that principle.
+This closes the long-running design ambiguity that produced five
+separate in-tree imports-fallback / qualifier-helper mechanisms
+(iters 15a / 23.1.3 / 23.1.4 / 23.2 / 23.2.4). Each existed because
+some sites carried bare type names while others produced qualified
+ones; values crossing module boundaries misaligned. With the new
+invariant, the divergence cannot occur — there is one canonical form
+for type names in the AST, and it is qualified.
 
 ## Architecture
 
-A single canonicalisation pass runs in `load_workspace`, between
-prelude injection (iter 23.1) and registry build:
+The `.ail.json` schema becomes stricter:
+
+- Every `Type::Con { name }` is either a primitive (`Int`, `Bool`,
+  `Str`, `Unit`, `Float`) or carries a single `.` separator
+  (`module.Type`). Bare non-primitive names are **a schema
+  violation**, rejected by `load_workspace` with a clear diagnostic.
+- `Type::Var` is unchanged — a different AST variant via the `"k"`
+  tag in JSON, never a qualifier candidate.
+- `Term::Ctor.type_name` follows the same rule — it's a Type::Con name.
+
+The Form-B prose surface (`.ailx`) is the bridge between LLM-author
+convenience and AST canonicality:
 
 ```
-.ail.json (surface — bare-tolerant)
+.ailx  (Form-B, bare-tolerant surface for the LLM)
+        |
+        | prose parser: bare local → qualified  (qualification at parse)
+        v
+.ail.json  (Form-A, canonical — all Type::Con qualified)
         |
         v
 load_workspace
         |
         +-- parse + import DFS  (existing)
         +-- prelude inject       (existing, iter 23.1)
-        +-- canonicalise         <-- NEW (this milestone)
-        +-- validate_classdefs   (existing, now sees canonical types)
-        +-- build_registry       (existing, now sees canonical types)
+        +-- schema validation: reject bare non-primitive Type::Con  <-- NEW
+        +-- validate_classdefs   (existing)
+        +-- build_registry       (existing — sees canonical types)
         |
         v
-check_workspace        (sees canonical AST — no fallbacks needed)
-        v
-monomorphise_workspace (sees canonical AST)
-        v
-lower_workspace        (sees canonical AST)
+check_workspace  (sees canonical AST — no fallbacks needed)
+check / mono / codegen / hash
 ```
 
-The pass operates per module against the (already-loaded) workspace
-map. Each `Type::Con { name, args }` is rewritten using these rules,
-applied in order:
+The prose printer (when writing `.ailx` from a `.ail.json`) trims a
+qualifier when it equals the current module name — so the surface
+stays compact for the LLM author. The prose parser (when reading
+`.ailx` into a `.ail.json`) qualifies bare names. Round-trip is
+semantics-preserving.
 
-1. **Already qualified** (`name.contains('.')`): unchanged.
-2. **Primitive** (`Int`, `Bool`, `Str`, `Unit`, `Float` — via
-   `ailang_core::primitives::primitive_surface_name`): unchanged.
-3. **Local hit** (current module's `Def::Type` names contain `name`):
-   rewrite to `{current_module}.{name}`.
-4. **Imports-fallback hit** (exactly one of the module's imports —
-   including the implicit `prelude` import for non-prelude modules
-   per iter 23.1 — defines a `Def::Type` called `name`): rewrite to
-   `{owning_module}.{name}`.
-5. **Zero / 2+ matches**: leave `name` bare. Downstream typechecker
-   fires `UnknownType` (zero) or `AmbiguousType` (2+) using the
-   existing diagnostic paths. No new diagnostic variants.
-
-`Type::Var` is untouched — the AST's tagged-enum representation
-distinguishes `Type::Con` from `Type::Var` via the `k` field, so
-the canonicaliser's `match` arm sees only the right variant.
-A bare identifier that names both a local type def and an in-scope
-`Type::Var` (e.g. `forall a. (Foo) -> a` where the module also
-defines `data Foo = ...`) is not ambiguous: the AST records
-quantification explicitly, so a `Type::Con { name: "Foo" }` is
-never a quantified variable. No additional disambiguation needed.
-
-After the pass, the invariant holds: **every `Type::Con` in the
-workspace AST is either a primitive name (bare) or a fully qualified
-`module.Type` name. Mixed bare-local-with-context never occurs.**
+There is **no internal canonicalisation pass** in `load_workspace`.
+The AST is canonical because the JSON is canonical, enforced by
+schema validation at the workspace boundary.
 
 ## Components
 
-The milestone decomposes into five iterations. Each iter's scope is
-deliberately narrow so per-iter commits remain reviewable.
+The milestone decomposes into four iterations.
 
 | Iter | Scope |
 |------|-------|
-| **ct.1** | Loader canonicalise pass. New file `crates/ailang-core/src/canonicalise.rs`. Walks every `Def`'s declared types (fn signatures, const types, class method types, instance types, type-def ctor field types) plus every `Term`'s nested types (`Term::Lam`'s `paramTypes` / `retType`, `Term::Ctor`'s `type_name`, any annotated `Term::Let`). Wires into `load_workspace` between prelude inject and `validate_classdefs`. Unit tests cover the five resolution rules. |
-| **ct.2** | Workspace-flat `env.types`. The per-module overlay in `check_in_workspace` (~`crates/ailang-check/src/lib.rs:1247-1287` — clears workspace-flat env.types, rebuilds per-module-local) is replaced by a single workspace-flat env.types keyed on the qualified canonical name. All `env.types.get(name)` call sites in `synth` adjust to look up by qualified name (which is what they already receive post-canonicalisation). The `env.module_types` workspace-flat-per-module map stays — its consumers are the obsolete fallbacks being deleted in ct.3/ct.4. |
-| **ct.3** | Remove obsolete typechecker mechanisms: `Pattern::Ctor`'s imports-fallback (iter 15a, ~lib.rs:2486-2521), `Term::Ctor`'s synth imports-fallback (iter 23.1.3, ~lib.rs:1979-2025), and `qualify_local_types` (iter 15a, ~lib.rs:1848). Each removal is RED-tested against an existing fixture that exercised the fallback path (the fixture still passes — its scrutinee/result types are now pre-canonicalised). |
-| **ct.4** | Remove obsolete codegen + mono mechanisms: `lookup_ctor_by_type`'s imports-fallback (iter 23.1.4, `crates/ailang-codegen/src/lib.rs`) and `apply_per_module_ctor_index_overlay` (iter 23.2 fix `84dcc46`, `crates/ailang-check/src/mono.rs`). The codegen `lower_workspace_inner` implicit-prelude import_map entry (iter 23.2.4 fix `be882c4`) STAYS — that's about fn-name resolution for mono symbols, not Type::Con names. |
-| **ct.5** | DESIGN.md amendments + re-baseline. Decision 2 amended to name the canonical form explicitly. Sections cross-referenced in lines 1067 / 1121 / 1137 / 1302 / 1335 / 1709 / 1719 / 2229 of DESIGN.md re-read and adjusted: their "hashes stay bit-identical" promises are recontextualised as promises within the canonical-form version. Hash-pinned regression tests (`iter19b_empty_suppress_preserves_pre_19b_hashes`, `iter19b_schema_extension_preserves_pre_19b_hashes`, and any other named pin) re-baselined to new hashes. IR snapshot fixtures under `crates/ail/tests/snapshots/` refreshed. JOURNAL entry documents the canonical-form transition. |
+| **ct.1** | `.ail.json` schema validation: reject bare non-primitive `Type::Con` names at `load_workspace` time with `WorkspaceLoadError::BareTypeNameInJson { module, name }`. Plus the one-time migration: a workspace-walker (e.g. `ail migrate-types` or a small Rust binary in `crates/ail/src/bin/`) that reads every `.ail.json` under `examples/`, looks up each bare non-primitive Type::Con's defining module via the import graph + the existing imports-fallback logic, rewrites to qualified form, and writes back. Run once, commit the rewritten fixtures. After this iter, the entire `examples/` corpus is canonical. |
+| **ct.2** | Remove the obsolete typechecker mechanisms: `Pattern::Ctor`'s imports-fallback (iter 15a, lib.rs:2486-2521), `Term::Ctor`'s synth imports-fallback (iter 23.1.3, lib.rs:1979-2025), and `qualify_local_types` (iter 15a, lib.rs:1848). Each removal is RED-tested against an existing fixture that exercised the fallback path (now passes through the qualified-AST path). The per-module `env.types` overlay in `check_in_workspace` (~lib.rs:1247-1287) may also collapse — `env.types` becomes workspace-flat with qualified keys. |
+| **ct.3** | Remove obsolete codegen + mono mechanisms: `lookup_ctor_by_type`'s imports-fallback (iter 23.1.4) and `apply_per_module_ctor_index_overlay` in mono (iter 23.2 fix `84dcc46`). The codegen `lower_workspace_inner` implicit-prelude import_map entry (iter 23.2.4 fix `be882c4`) STAYS — that's fn-name resolution for mono symbols, not Type::Con names. |
+| **ct.4** | DESIGN.md amendments + JOURNAL migration entry + re-baseline of hash-pinned regression tests + IR snapshot refresh. Decision 2 amended to name the canonical-form rule explicitly. Form-B prose printer/parser verified to round-trip cleanly across the bare/qualified boundary (write a round-trip test if not already covered). |
 
-After ct.5, iter 23.3 Task 4+5 resume (recreate `examples/compare_primitives_smoke.ail.json` + the e2e test from the iter-23.3 plan; expected to pass without further compiler changes).
+After ct.4, iter 23.3 Task 4+5 resume (recreate
+`examples/compare_primitives_smoke.ail.json` per the iter 23.3 plan;
+expected to pass without further compiler changes).
 
 ## Data flow
 
-### Example 1: user-module Term::Ctor against a prelude-defined ADT
+### Example 1: surface → JSON → AST
 
-Surface form (`.ail.json` in user module `foo`):
-```json
-{ "t": "ctor", "type": "Ordering", "ctor": "LT", "args": [] }
+LLM-author writes in `.ailx` (module `foo`):
+```
+fn main : () -> Unit ![IO] {
+  let result = compare(1, 2);
+  match result { LT -> 1; EQ -> 2; GT -> 3 }
+}
 ```
 
-**Pre-milestone** (today):
-1. AST: `Term::Ctor { type_name: "Ordering", ctor: "LT" }`.
-2. Term::Ctor synth (iter 23.1.3 fallback) scans `env.imports.values()` × `env.module_types`, finds `Ordering` in prelude, sets `result_type_name = "prelude.Ordering"`.
-3. Inferred expression type: `Type::Con { name: "prelude.Ordering" }`.
+Prose parser produces `.ail.json` for module `foo`. The `compare` call
+returns `Ordering` (defined in prelude). The match arm patterns
+`LT/EQ/GT` are ctor names — the parser knows they belong to
+`prelude.Ordering` because `compare` resolves to a prelude method, but
+**the JSON doesn't need to encode where they came from**. Pattern
+ctor names continue to be bare (their parent type is reconstructible
+from the scrutinee's type at typecheck).
 
-**Post-milestone**:
-1. Loader canonicalise pass rewrites the Term::Ctor: `type_name: "Ordering"` → `"prelude.Ordering"`.
-2. AST after load: `Term::Ctor { type_name: "prelude.Ordering", ctor: "LT" }`.
-3. Term::Ctor synth uses local ctor-resolution against the qualified name; no fallback needed.
-4. Inferred expression type: `Type::Con { name: "prelude.Ordering" }`.
+What the parser DOES qualify: any standalone `Type::Con` reference.
+If `foo` declares `fn helper : (Ordering) -> Int { ... }`, the prose
+parser writes:
+```json
+{
+  "name": "helper",
+  "type": {
+    "k": "fn",
+    "params": [{ "k": "con", "name": "prelude.Ordering" }],
+    "ret": { "k": "con", "name": "Int" },
+    "effects": []
+  },
+  ...
+}
+```
 
-Result identical, mechanism removed.
+`prelude.Ordering` qualified, `Int` (primitive) bare.
 
-### Example 2: cross-module value flowing into a match (the iter 23.3 bug)
+### Example 2: AST already canonical — no resolution needed downstream
 
-Prelude declares `class Ord a where compare : (a borrow, a borrow) -> Ordering`. User module calls `compare 1 2` and matches on the result.
+`load_workspace` reads the qualified JSON. Schema validation passes
+(every non-primitive Type::Con has the qualifier). `build_registry`
+indexes instances by qualified type name. `check_workspace` runs;
+when it encounters `Type::Con { name: "prelude.Ordering" }` it looks
+up the type in workspace-flat `env.types["prelude.Ordering"]` directly.
+Pattern::Ctor against `LT`: the scrutinee's type (already qualified)
+gives the TypeDef directly; check ctor name match against its
+ctors list. No fallback. No imports walking.
 
-**Pre-milestone**:
-1. Prelude's `compare` method signature AST: `(a, a) -> Type::Con { name: "Ordering" }` — bare.
-2. User-side typechecker resolves `compare`, propagates bare `Ordering` to the match scrutinee.
-3. Pattern::Ctor's iter 15a fallback resolves `LT` to `prelude.Ordering`.
-4. Equality check at lib.rs:2526: `"Ordering" == "prelude.Ordering"` → false → **`pattern-type-mismatch`**.
+### Example 3: the iter 23.3 bug, post-migration
 
-**Post-milestone**:
-1. Loader canonicalise pass rewrites prelude's `compare` method type: ret `"Ordering"` → `"prelude.Ordering"` (the local-hit rule applies — `Ordering` IS local to prelude, so prelude's own module name is the prefix).
-2. User-side typechecker propagates `prelude.Ordering` to the match scrutinee.
-3. Pattern::Ctor uses local ctor-name resolution (the user's `env.ctor_index` doesn't have `LT`, but `env.types.get("prelude.Ordering")` returns the TypeDef directly; check ctor name match against td.ctors). No fallback needed.
-4. Equality check trivially succeeds. **Bug closed by construction.**
+Prelude's `compare` method's return type in `.ail.json`:
+```json
+{ "name": "compare", "type": { "k": "fn", ..., "ret": { "k": "con", "name": "prelude.Ordering" }, ... } }
+```
 
-The bug was structural: as long as prelude's own method signature carried bare `Ordering` while user-side resolution produced qualified `prelude.Ordering`, no per-site fix could close the gap. Canonicalising the loader-time AST is the only place the invariant unifies.
+User-module call `compare 1 2` returns `prelude.Ordering`. Pattern
+`LT` resolves against the qualified scrutinee. Trivial match.
+**The bug is structurally impossible** because there's no bare
+form internally that could mismatch.
 
 ## Error handling
 
-No new diagnostics. The canonicaliser delegates errors to the existing typechecker paths:
+One new diagnostic, fired at workspace-load time:
 
-- **Truly unknown type name** (zero matches, neither local nor imported): canonicaliser leaves the name bare. Downstream `synth` / `check_type_well_formed` fires `CheckError::UnknownType` exactly as today.
-- **Ambiguous type name** (2+ imports define a type with the same bare name): canonicaliser leaves the name bare. Downstream `synth` fires `CheckError::AmbiguousType` (added in iter 23.1.3) via its imports-walking path. After ct.3 removes the imports-fallback, an ambiguous bare name reaching downstream is itself a `UnknownType` — but the canonicalise pass can detect ambiguity locally and emit a workspace-load-time `WorkspaceLoadError::AmbiguousTypeName` to keep the diagnostic at the right phase. This is a design choice within the canonicaliser; not load-bearing on the spec.
+- `WorkspaceLoadError::BareTypeNameInJson { module, name }`:
+  "Module `M` contains a bare type name `T`; AST type names must be
+  fully qualified (`<module>.T`). Primitive names (`Int`, `Bool`,
+  `Str`, `Unit`, `Float`) are the only bare names allowed in
+  `.ail.json`. Run the migration tool to fix legacy fixtures."
 
-The canonicaliser is otherwise total — it never fails. Unrecognised names just pass through bare.
+The diagnostic message points the LLM-author at the migration tool
+explicitly, so a stale `.ail.json` produces a self-explanatory error.
+
+The existing typechecker diagnostics (`UnknownType`, `AmbiguousType`,
+`UnknownCtor`, `PatternTypeMismatch`) keep their semantics but their
+underlying mechanism simplifies: they fire on qualified-name lookup
+failures, never on bare-vs-qualified mismatches.
 
 ## Testing strategy
 
-- **Unit tests** in `crates/ailang-core/src/canonicalise.rs::mod tests`:
-  - Bare local → qualified-local (e.g. fixture `data Foo` in module `m`, declared fn `(Foo) -> Int` rewrites to `(m.Foo) -> Int`).
-  - Bare imported-single → qualified-import.
-  - Bare imported-ambiguous (2+) → left bare (or workspace-load error, see Error handling).
-  - Bare primitive (`Int`, `Bool`, `Str`, `Unit`, `Float`) → bare.
-  - Already-qualified `mod.Type` → unchanged.
-  - `Type::Var` (e.g. `forall a. (a) -> a`) → untouched.
+- **Schema validator unit tests** in `crates/ailang-core/src/workspace.rs`:
+  - JSON with `Type::Con { name: "Foo" }` (bare non-primitive) is rejected with `BareTypeNameInJson`.
+  - JSON with `Type::Con { name: "Int" }` (primitive bare) is accepted.
+  - JSON with `Type::Con { name: "M.Foo" }` (qualified) is accepted.
+  - JSON with nested qualification in args (e.g. `List<m.Foo>`) walks correctly.
 
-- **Workspace integration tests**:
-  - Iter 23.3 Task 4's E2E fixture (`examples/compare_primitives_smoke.ail.json`, recreated after ct.5) compiles, runs, and prints `1\n2\n3\n1\n2\n3\n1\n2\n3\n`.
-  - Every existing E2E test still passes (with re-baselined hashes / snapshots).
-  - The five obsolete-mechanism removals (ct.3 + ct.4) each pinned by an existing fixture that exercised the fallback (e.g. iter-23.1.4's bare-ctor E2E `ordering_match_via_prelude_prints_1`).
+- **Migration tool tests**: a small synthetic 2-module workspace with
+  bare type names; the migration tool produces a workspace where every
+  Type::Con is qualified. Idempotent (running twice produces the same
+  result).
 
-- **Hash regression tests**: re-baselined once in ct.5. They continue to pin form stability ("schema additions don't change hashes") but at the new canonical-form's hashes.
+- **Form-B round-trip tests** (extend existing prose round-trip
+  coverage if needed): `.ailx` with bare local names → parsed
+  `.ail.json` with qualified names → printed `.ailx` with bare-trimmed
+  local names. The `.ailx` text round-trips byte-stable; the `.ail.json`
+  text is canonical (qualified).
 
-- **Bench scripts**: run at milestone close to confirm no IR-shape regression caused by the loader pass. Hypothesis: canonicalisation adds a constant per-workspace-load overhead, no per-call regression. If regression fires, dispatch `ailang-bencher`.
+- **Existing workspace integration tests** pass with re-baselined
+  hashes / snapshots. The five obsolete-mechanism removals in ct.2/ct.3
+  each pinned by an existing fixture (e.g. iter-23.1.4's
+  `ordering_match_via_prelude_prints_1`, iter-15a's
+  cross-module Cons pattern fixture).
+
+- **Iter 23.3 Task 4 fixture** (`examples/compare_primitives_smoke.ail.json`,
+  recreated post-migration) compiles, runs, prints
+  `"1\n2\n3\n1\n2\n3\n1\n2\n3\n"`.
+
+- **Bench scripts** (the three regression harnesses) run at milestone
+  close. Hypothesis: no measurable regression — the new schema check
+  is constant-time per load, the removed fallbacks are dead code paths
+  not in the hot path.
 
 ## Acceptance criteria
 
-1. After `load_workspace` completes, the invariant holds workspace-wide: every `Type::Con` in every `Def`'s signatures and every nested `Type` in every `Term` is either a primitive name (bare) or a fully qualified `module.Type` name. No mixed forms.
+1. `.ail.json` schema validation rejects bare non-primitive
+   `Type::Con` names at `load_workspace`. Every accepted workspace's
+   AST is canonical (qualified everywhere except primitives) by
+   construction — no internal canonicalisation pass.
 
-2. The five obsolete mechanisms in Components are deleted entirely (NOT retained as defensive guards):
-   - `Pattern::Ctor` imports-fallback (iter 15a, lib.rs:2486-2521)
-   - `Term::Ctor` synth imports-fallback (iter 23.1.3, lib.rs:1979-2025)
-   - `qualify_local_types` helper (iter 15a, lib.rs:1848)
-   - `lookup_ctor_by_type` codegen imports-fallback (iter 23.1.4)
-   - `apply_per_module_ctor_index_overlay` in mono (iter 23.2 fix `84dcc46`)
+2. Every existing fixture under `examples/` is migrated to canonical
+   form. Code-search for `"name": "Ordering"` (or any other
+   non-primitive bare reference) in `examples/*.ail.json` returns
+   zero matches. The migration is a single bulk commit produced by
+   the migration tool, not hand-edited.
+
+3. The five obsolete mechanisms are deleted (NOT retained as defensive
+   guards):
+   - `Pattern::Ctor` imports-fallback (iter 15a, `crates/ailang-check/src/lib.rs:2486-2521`)
+   - `Term::Ctor` synth imports-fallback (iter 23.1.3, `~lib.rs:1979-2025`)
+   - `qualify_local_types` helper (iter 15a, `~lib.rs:1848`)
+   - `lookup_ctor_by_type` codegen imports-fallback (iter 23.1.4, `crates/ailang-codegen/src/lib.rs`)
+   - `apply_per_module_ctor_index_overlay` in mono (iter 23.2 fix `84dcc46`, `crates/ailang-check/src/mono.rs`)
    
-   Code search for `imports-fallback` or `imports.values().*module_types` in the typechecker + codegen returns ZERO matches related to Type::Con resolution.
+   Code search confirms.
 
-3. The codegen implicit-prelude import_map fix (`lower_workspace_inner`, iter 23.2.4 `be882c4`) STAYS — different problem (fn-name resolution for mono symbols, not Type::Con).
+4. The codegen `lower_workspace_inner` implicit-prelude import_map
+   entry (`be882c4`) STAYS — different problem (fn-name resolution
+   for mono symbols).
 
-4. `cargo build --workspace && cargo test --workspace` is FULL green at milestone close.
+5. `cargo build --workspace && cargo test --workspace` is FULL green
+   at milestone close.
 
-5. Iter 23.3 Task 4+5 resume after this milestone closes and complete without any further canonical-form-related compiler changes.
+6. Iter 23.3 Task 4+5 resume after this milestone and complete
+   without any further canonical-form-related compiler changes.
 
-6. DESIGN.md amended:
-   - Decision 2 (content-addressed defs) gains an explicit canonical-form rule for type names.
-   - The "hashes stay bit-identical" promises at lines 1067, 1121, 1137, 1302, 1335, 1709, 1719, 2229 are reviewed and adjusted where they implicitly relied on the old canonical form.
-   - The JOURNAL entry documents the migration as a versioned canonical-form transition (one-time hash shift, deliberate, ratified by this spec's acceptance).
+7. DESIGN.md amended:
+   - Decision 2 (content-addressed defs) names the rule explicitly:
+     "AST Type::Con names are fully qualified (`module.Type`) except
+     for primitives. Each AST object is context-free — it can be
+     reasoned about and hashed without external module information."
+   - The "hashes stay bit-identical" promises across DESIGN.md (lines
+     1067, 1121, 1137, 1302, 1335, 1709, 1719, 2229) are reviewed and
+     re-contextualised as promises within the new canonical-form
+     version.
 
-7. The three bench scripts (`bench/check.py`, `bench/compile_check.py`, `bench/cross_lang.py`) exit 0, or any non-zero is ratified per the audit-skill rules with a JOURNAL entry naming the iter that moved the metric.
+8. JOURNAL entry documents the migration as a versioned canonical-form
+   transition: one-time hash shift, deliberate, ratified by this
+   spec's acceptance.
+
+9. The three bench scripts exit 0 or any non-zero is ratified per
+   audit-skill rules.
 
 ## Out of scope
 
-- **Term-level names** (function names, var names, ctor names in patterns): unchanged. Their resolution mechanisms (Term::Var with `prefix.name` form, Pattern::Ctor's local ctor_index, etc.) work correctly — bare ctor names like `LT` are looked up against the now-qualified scrutinee's type, which provides unambiguous resolution.
+- **Term-level names** (function names, var names, ctor names in
+  patterns): unchanged. Bare ctor names in `Pattern::Ctor` continue
+  to work — they're resolved against the (now-qualified) scrutinee's
+  type, which gives unambiguous resolution.
 
-- **Surface notation**: bare names in `.ail.json` continue to be the LLM-author convention. The loader resolves them. The Form-A prose printer continues to display bare local names (`Ordering` not `prelude.Ordering`) for readability — that's pretty-printing, not canonical form.
+- **Class names** (`class Eq`, `instance Eq Int`, `class Ord extends Eq`):
+  same conceptual problem as type names but separate namespace. Today
+  class names are bare in JSON; the `MethodNameCollision` check
+  enforces global uniqueness across all classes. Whether class names
+  should also be qualified is a related question deferred to a future
+  spec — out of scope here. This spec touches Type::Con only.
 
-- **Schema version bump**: the canonical form is internal; the `.ail.json` schema (`ailang/v0`) is unchanged. Existing fixtures continue to parse without rewriting.
+- **Surface notation in `.ailx`**: bare local names continue to be
+  the LLM-author convention. The prose parser qualifies on read; the
+  prose printer trims on write. Round-trip is semantics-preserving.
 
-- **Effects, modes, type-def schema, ctor field shape**: unchanged.
+- **Schema version bump**: the `.ail.json` schema field stays
+  `"ailang/v0"`. The canonical form change is a strictening of the
+  existing schema (rejecting previously-tolerated input), not a new
+  schema version. Migration is one-time and tool-assisted.
+
+- **External clients**: AILang is pre-1.0 and not yet consumed by
+  anything outside the repo.
 
 ## Migration impact (one-time)
 
-This is a versioned canonical-form transition. The previous canonical
-form (bare-local-with-context) was structurally incomplete; the new
-form (qualified-everywhere-internal) is complete. The migration:
+The migration is bounded and deliberate:
 
-- **Every canonical-JSON hash in the codebase shifts** (because `canonical::type_hash` walks the AST including Type::Con names). One-time, intentional, ratified by this spec. The pre-transition hashes are not preserved — they were artefacts of an incomplete canonical form.
-- **Hash-pinned regression tests are re-baselined once** at ct.5. They continue to pin form stability under future schema additions, just at new hash values.
-- **IR snapshot fixtures** under `crates/ail/tests/snapshots/` shift if the IR text depends on type names (it does, via mangling). Re-baselined at ct.5.
-- **No external clients are affected** — AILang is pre-1.0 and not yet consumed by anything outside the repo.
+- **Every `.ail.json` fixture under `examples/` is rewritten** by the
+  migration tool. The diff is mechanical — each bare non-primitive
+  `Type::Con.name` gains its qualifier; every other byte stays the
+  same. Commit as a single bulk migration in ct.1.
+
+- **Every canonical-JSON hash shifts** as a consequence. Re-baselined
+  once in ct.4. Hash-pinned regression tests continue to pin form
+  stability under future schema additions, at the new hashes.
+
+- **IR snapshot fixtures** under `crates/ail/tests/snapshots/` may
+  shift if the IR text depends on type names (it does, via mangling).
+  Re-baselined at ct.4.
+
+- **Prose snapshots** (`.prose.txt` round-trip baselines): if the
+  prose printer correctly trims bare-local on output, the prose
+  side of the round-trip stays byte-stable across the migration —
+  only the `.ail.json` side changes.
+
+This is a versioned canonical-form transition. The previous form
+(bare-tolerant) was structurally incomplete; the new form
+(qualified-mandatory in JSON) is complete and the canonical-form
+invariant holds by construction.
 
 ## Note on canonical-hash stability promises in DESIGN.md
 
-The repeated promises across DESIGN.md (`hashes stay bit-identical when feature X is added`) are not absolute promises about the bit-sequence of hashes for all time. They are conditional promises within a given canonical-form version: when feature X is added, the canonical-form rule is unchanged, so existing modules emit the same bytes and hash to the same values. This spec changes the canonical-form rule itself, so the promises are correctly re-interpreted as: "within the new canonical form, future feature additions continue to preserve hashes". Ct.5's DESIGN.md amendment makes this explicit.
+The "hashes stay bit-identical when feature X is added" promises
+distributed across DESIGN.md are not promises about a specific
+bit-sequence for all time. They are promises within a canonical-form
+version: feature additions that preserve the canonical-form rule
+don't change hashes. This spec changes the canonical-form rule
+itself, so the promises are re-interpreted as: within the new
+canonical form, future feature additions continue to preserve
+hashes. Ct.4's DESIGN.md amendment makes this explicit.