# Module-qualified class names + type-driven method dispatch — Design Spec **Date:** 2026-05-13 **Status:** Draft — awaiting user spec review **Authors:** Brummel (orchestrator) + Claude ## Goal Retire the workspace-global `WorkspaceLoadError::MethodNameCollision` pre-pass (`crates/ailang-core/src/workspace.rs:547`) that today enforces a single class per method name across the entire workspace. After retirement, two libraries (e.g. the prelude and a user module) can each declare `class Show` (or `class Eq`, `class Ord`, …) with their own `show` method, and both can ship instances for overlapping types. The retirement unblocks the deferred milestone 24 (Show + print rewire) by allowing the prelude to ship `class Show` independently of the 14 `examples/test_22b{1,2,3}_*.ail.json` fixtures that today declare a user-class named `Show`. The replacement mechanism is **type-driven, fail-closed dispatch**: - **Polymorphic call sites:** `Constraint.class` (now fully qualified per the canonical-form extension below) names the class; synth's residual is keyed by `(qualified-class, method)`. No ambiguity by construction. - **Monomorphic call sites:** synth emits a residual carrying the candidate-class set; constraint-discharge refines by `(class, type_hash(arg-type)) ∈ Registry`; unique survivor wins; multiple → `CheckError::AmbiguousMethodResolution`; LLM-author writes an explicit qualifier (`.. `) to disambiguate. Three schema fields move from bare to canonical (symmetric to ct.1's `Type::Con.name` rule): `InstanceDef.class`, `Constraint.class`, `SuperclassRef.class`. `ClassDef.name` stays bare (defining-site context, symmetric to `TypeDef.name`). Why this is the right shape: the canonical-type-names milestone explicitly out-of-scoped class-reference fields and named `MethodNameCollision` as the load-bearing workaround that made bare class names viable (`docs/specs/0007-canonical-type-names.md` §"Out of scope: Class names"). This milestone closes that loop. The workaround was honest about being a workaround; this is the milestone that retires it. ## Architecture **Model.** Class names are canonicalised throughout the schema by the same rule ct.1 applies to `Type::Con.name`: bare for same-module references, qualified (`.`) for cross-module references. Method dispatch becomes type-driven: synth's `Term::Var` arm consults a method → candidate-class index, refines by argument type and active constraints, fails closed on genuine ambiguity. **Three schema fields are canonicalised** (Iter 1): - `InstanceDef.class` (`crates/ailang-core/src/ast.rs:314`) — bare → canonical. - `Constraint.class` (`crates/ailang-core/src/ast.rs:345`) — bare → canonical. - `SuperclassRef.class` (`crates/ailang-core/src/ast.rs:279`) — bare → canonical. - `ClassDef.name` (`crates/ailang-core/src/ast.rs:262`) stays bare (defining site, symmetric to `TypeDef.name`). **ct.1's `validate_canonical_type_names` validator (`crates/ailang-core/src/workspace.rs:921`) is extended** with three new field walks symmetric to the existing `Type::Con.name` walk. Existing `BareCrossModuleTypeRef` diagnostic (`workspace.rs:341`) extended OR sibling diagnostic `BareCrossModuleClassRef` added (implementer chooses; both shapes carry the same information — `{module, name, candidates}`). Validator runs BEFORE class-schema validation (already does at `workspace.rs:486`), so a bare cross-module class-ref fires the canonical-form diagnostic before `MissingMethod` or `OrphanInstance`. **Registry key is qualified** (Iter 1). `build_registry` (`workspace.rs:521`): - Pass-1: `class_def_module: BTreeMap` (the bare-class-name → defining-module map) becomes `class_def_module: BTreeMap` keyed by the qualified class name (`.`). - Pass-2: `entries: BTreeMap<(QualifiedClassName, type_hash), RegistryEntry>` ditto. - `RegistryEntry.class` field carries qualified strings. `ClassMethodEntry.class_name` (`crates/ailang-check/src/lib.rs`) carries qualified strings. The `format!("{class} {type}")`-shaped diagnostic messages already include both module and class context in their `Origin::Class { class_name, module }` form, so the user-facing shape stays informative. **Sekundärindex `method_to_candidate_classes`** (Iter 2). New map `BTreeMap>` built in the same pass as `class_methods`. Inverse map: for each method, the set of classes that declare it. In Iter 2 this set has cardinality ≤ 1 by `MethodNameCollision`'s invariant; in Iter 3 cardinality > 1 becomes legal. **Synth Var-arm rewrite** (Iter 2). The single resolution point at `crates/ailang-check/src/lib.rs:1968` is rewritten: 1. Parse `name`: take the last dot-segment as method name, the prefix (possibly empty) as a class qualifier. The prefix is itself a possibly-qualified class name (`prelude.Show` or just `Show`). 2. Consult `method_to_candidate_classes[method]`. If absent → fall through to the existing other Var-arm branches (locals, fns, etc.). 3. **Qualifier present:** filter candidates to the class named by the qualifier. Empty result → `CheckError::UnknownClass`. Single result → continue at (5). 4. **Qualifier empty (bare method form):** if `|candidates| == 1` → continue at (5). Otherwise emit a multi-candidate residual carrying the candidate set + the freshly-instantiated class-param metavar + the method name. Discharge handles refinement (see below). 5. Push `ResidualConstraint { class: , type_: fresh, method }` as today. Return the instantiated method type. **Constraint-discharge refinement** (Iter 2). The discharge path (today: registry lookup at fn-body-end on each residual) is extended to handle the multi-candidate variant: 1. If the residual's `type_` is concrete (resolved to non-var) → filter candidates on `(class, type_hash(type_)) ∈ Registry`. Single survivor → discharge against that registry entry. Zero survivors → `NoInstance` (with a candidate-classes list in the diagnostic, so the LLM-author knows which class lacks an instance). Multiple survivors → `AmbiguousMethodResolution`. 2. If the residual's `type_` is still a rigid type variable (e.g. inside a polymorphic fn body) → filter candidates against the active declared constraints: keep classes `C` such that `Constraint { class: C, type: t }` is in the fn's declared constraint set with `t` unifying with the residual's `type_`. Single survivor → propagate as a single-class declared constraint (today's path). Zero survivors → `MissingConstraint` (with the candidate classes named). Multiple survivors → `MissingConstraint` that names the candidates and instructs the LLM to add one of the declared constraints. **`MethodNameCollision` retirement** (Iter 3). Variant (`workspace.rs:303`), pre-pass (`workspace.rs:547-627`), Display arm (`crates/ail/src/main.rs:1201`), and the two pin tests (`workspace.rs:1931, 1965`) are deleted. The deletions are mechanical; the post-delete workspace-load path is: ```text load_workspace → visit graph → inject prelude → validate_canonical_type_names → validate_classdefs → build_registry ``` No method-collision check between them — the collision is no longer a load-time invariant, it's a per-call-site resolution outcome. **Class-fn collisions** are a special case of method ambiguity in the new model. Today's `MethodNameCollision { kind: "class-fn" }` pre-pass forbids `class C { eq } + fn eq` workspace-wide. Post-retirement, the combination is allowed; at a call site with `Term::Var { name: "eq" }`, synth tries the existing precedence (locals → caller-module-fn → imported-fn) first; if no fn match, falls through to the `method_to_candidate_classes` lookup. If BOTH a fn `eq` and a class candidate for the arg type exist → the existing lookup-precedence rule applies (fn wins) AND a structured warning fires (because the LLM likely didn't realise the shadowing happened — implementer drafts the warning text). Alternatively (implementer choice): hard-error `AmbiguousMethodResolution`-style. Default in this spec: lookup precedence + warning, because (a) the existing precedence rule is already in place for plain free-fn lookup, (b) shadowing is the LLM-natural surface convention (local binding wins over a class method), and (c) the warning surfaces the rare case where the shadowing is accidental. ## Components (iterations) | Iter | Scope | |------|-------| | **1** | **Canonical-form extension for class-ref fields + workspace internal qualification.** Three schema fields move bare → canonical: `InstanceDef.class`, `Constraint.class`, `SuperclassRef.class`. ct.1's `validate_canonical_type_names` validator gets three new field-walks symmetric to the existing `Type::Con.name` walk; diagnostic surface uses the existing `BareCrossModuleTypeRef` or a sibling `BareCrossModuleClassRef` (implementer chooses). Pass-1 of `build_registry` keys `class_def_module` by qualified class name. Pass-2's `entries` keyed by `(QualifiedClassName, type_hash)`. `ClassMethodEntry.class_name` carries qualified strings. All cross-module consumers (mono's instance lookup, the coherence-check `mod_name == class_mod` comparison, the superclass-existence check) read qualified. `MethodNameCollision`'s `Origin::Class.class_name` migrated to qualified (the existing `format!("class {class_name} (in {module})")` shape stays unambiguous). `examples/prelude.ail.json` migration: intra-prelude refs stay bare per the canonical-form rule (the prelude's `Eq`/`Ord` references inside `instance` and `Constraint` are all same-module → no diff in the prelude). 14 test fixtures under `examples/test_22b*` migrated where they carry cross-module refs; intra-fixture-module refs stay bare. `crates/ail/tests/typeclass_22b{2,3}.rs` assertions migrated where they assert on the qualified form. `cargo test --workspace` green. `bench/check.py && bench/compile_check.py && bench/cross_lang.py` exit 0 or audit-ratified. | | **2** | **Type-driven dispatch mechanism installed (mechanism-before-exercise).** New parallel index `method_to_candidate_classes: BTreeMap>` built in `build_check_env` (or sibling) alongside `class_methods`. Synth Var-arm at `crates/ailang-check/src/lib.rs:1968` rewritten per the Architecture's 5-step rule. New residual variant (or `ResidualConstraint`-enum extension; implementer chooses) carrying `{ candidates: BTreeSet, type_: Type, method: String }`. Constraint-discharge extended to handle multi-candidate residuals per the Architecture's refinement rules. New diagnostic variants `CheckError::AmbiguousMethodResolution { method, type_repr, candidate_classes: Vec }` and `CheckError::UnknownClass { name: String }` with structured-diagnostic codes `ambiguous-method-resolution` and `unknown-class`. Existing `CheckError::NoInstance` extended (additive — optional `candidate_classes` field) to surface the candidate set on the unique-class-path miss case. Unit tests on the new `resolve_method_dispatch` function (or equivalent name; implementer chooses): synthetic inputs covering the 6 cases enumerated in Testing strategy. Mono's class-method-residual rewriter (`crates/ailang-check/src/mono.rs:1233` and surrounding) consumes the new index where needed; the existing call-site rewrite shape (`__` with cross-module `.<...>` prefix) is unchanged because qualified class names are already in scope post-iter-1. `cargo test --workspace` green. End-to-end multi-class fixtures NOT yet possible because `MethodNameCollision` still gates real workspaces — the new path is exercised exclusively by unit tests in this iter. Bench-regression ratified or held. | | **3** | **Retire `MethodNameCollision`.** Variant (`workspace.rs:303`) + pre-pass (`workspace.rs:547-627`, including `Origin` enum) + Display arm (`crates/ail/src/main.rs:1201`) + the two pin tests at `workspace.rs:1931` and `workspace.rs:1965` deleted. The two pin tests are REPURPOSED to assert the opposite invariant: same fixtures load without error AND `method_to_candidate_classes` carries the expected multi-entry set. Three new positive E2E fixtures: (a) two-module workspace with two `Show` classes (each with `Show Int`); bare `show 42` at a third call-site module fires `AmbiguousMethodResolution` naming both candidate classes. (b) same workspace; explicit `.Show.show 42` resolves to A's class without diagnostic. (c) two-module workspace with `class Eq` in modA + `fn eq` in modB; bare `eq x y` at a call-site module that imports both resolves to modB's fn per lookup precedence AND emits the new fn-shadows-class-method warning (or fails closed per implementer choice — see Architecture above). DESIGN.md amendment: §"Class-schema diagnostics" loses the `MethodNameCollision` paragraph; gains a paragraph on `AmbiguousMethodResolution` + class-fn lookup-precedence. New DESIGN.md subsection "Method dispatch" anchors the two-mode dispatch (poly via constraint, mono type-driven) and points at `method_to_candidate_classes` as the load-bearing data structure. `WhatsNew.md` entry on milestone close. Roadmap update: P2 entry → `[x]`, milestone 24 `depends on:` line removed, milestone 24 entry annotated "ready for re-brainstorm". `cargo test --workspace` green. Bench-regression ratified. | The milestone closes with the standard `audit` pipeline (architect drift review + three bench scripts). ## Data flow Five trajectories show the dispatch at work post-Iter-3. ### Trajectory A — bare call, unique candidate (most common case) `eq 1 2` in a workspace where only `prelude.Eq` declares method `eq`. 1. Synth Var-arm parses `name = "eq"` → method `"eq"`, qualifier-prefix empty. 2. `method_to_candidate_classes["eq"]` = `{prelude.Eq}`. Singleton. 3. Push `ResidualConstraint { class: "prelude.Eq", type_: fresh, method: "eq" }`. 4. App-arm unification binds `fresh` to `Int` via the arg's type. 5. Discharge: `(prelude.Eq, type_hash(Int)) ∈ Registry` → resolved. Mono synthesises `eq__Int`. ### Trajectory B — bare call, multi-candidate, type-driven refinement to unique `show 42` in a workspace where both `prelude.Show` and `userlib.Show` declare method `show`, but only `prelude.Show` has `Show Int`. 1. Synth Var-arm: method `"show"`, qualifier-prefix empty. 2. `method_to_candidate_classes["show"]` = `{prelude.Show, userlib.Show}`. 3. Push a multi-candidate residual carrying `{candidates, type_: fresh, method}`. 4. App-arm unification binds `fresh` to `Int`. 5. Discharge: filter candidates on `(class, type_hash(Int)) ∈ Registry` → only `prelude.Show` survives. Discharge proceeds. Mono synthesises `show__Int` from `prelude.Show`'s instance body. ### Trajectory C — bare call, multi-candidate, true ambiguity → diagnostic Same workspace as B, but both `prelude.Show` and `userlib.Show` also ship `Show Int`. `show 42` at a monomorphic call site: 1–4 as in B. 5. Discharge: filter survives both `prelude.Show` and `userlib.Show` → `CheckError::AmbiguousMethodResolution { method: "show", type_repr: "Int", candidate_classes: ["prelude.Show", "userlib.Show"] }`. Diagnostic message names both classes and instructs the LLM-author to rewrite as `prelude.Show.show 42` or `userlib.Show.show 42`. ### Trajectory D — bare call inside polymorphic fn body, constraint-driven refinement A free fn `print : forall a. prelude.Show a => (a) -> () !IO` (the qualified-`Constraint.class` form post-Iter-1) with body containing `show x`: 1. Synth Var-arm at the inner `show`: method `"show"`, qualifier-prefix empty. `method_to_candidate_classes["show"]` = `{prelude.Show, userlib.Show}`. 2. Push a multi-candidate residual `{candidates, type_: fresh, method}`. 3. App-arm unification: arg `x : a` → fresh unifies with the rigid var `a`. 4. Discharge: `type_` is the rigid `a`, can't drive registry lookup. Fall back to constraint-driven filter. The fn's declared constraint set is `[{ class: "prelude.Show", type: a }]`. The residual's `type_` unifies with that constraint's `type` (both are `a`). Filter candidates on class-name-matches-a-declared-constraint → `{prelude.Show}`. Unique. Discharge proceeds: the multi-candidate residual collapses into a single-class declared constraint propagation (the existing path). 5. Mono synthesises `print__Int` (or whatever the concrete arg type ends up); inside that body, `show__Int` is scheduled in the same fixpoint round per the 23.4 unification. ### Trajectory E — explicit-qualifier call `prelude.Show.show 42` at a monomorphic call site (the LLM-author's remedy after a Trajectory-C diagnostic): 1. Synth Var-arm parses `name = "prelude.Show.show"` → method `"show"`, qualifier-prefix `"prelude.Show"`. 2. `method_to_candidate_classes["show"]` = `{prelude.Show, userlib.Show}`. Filter on qualifier-equals-class → `{prelude.Show}`. Singleton. 3. Push `ResidualConstraint { class: "prelude.Show", type_: fresh, method: "show" }`. 4–5 as in Trajectory A. If the qualifier names a class not in the workspace (`unknownlib.Show.show 42`) → `CheckError::UnknownClass { name: "unknownlib.Show" }`. ## Error handling - **`BareCrossModuleClassRef`** (or `BareCrossModuleTypeRef` reuse) — ct.1-validator diagnostic for the three class-ref fields when a bare form is used to reference a cross-module class. Same shape as the existing `BareCrossModuleTypeRef` (`workspace.rs:341`): carries `module`, `name`, `candidates`. Implementer chooses whether to reuse the existing variant (extending the `name` field's semantics to cover class refs) or add a sibling. Default: sibling, because the user-facing wording ("type" vs "class") differs. - **`AmbiguousMethodResolution { method, type_repr, candidate_classes }`** — new check-time diagnostic. Fires at constraint-discharge time when the candidate-class set has more than one survivor after type-driven filtering at a monomorphic call site. Message names the candidate classes and instructs the LLM to write the explicit qualifier form. Structured-diagnostic code: `ambiguous-method-resolution`. - **`UnknownClass { name }`** — new check-time diagnostic. Fires when an explicit class qualifier in `Term::Var.name` names a qualified class that's not in the workspace. Structured-diagnostic code: `unknown-class`. - **`NoInstance`** — existing diagnostic shape stays; gains an optional `candidate_classes` field surfacing the candidate set on the unique-class-path miss case (additive change). Existing display wording stays for the singleton case; with `candidate_classes` it surfaces the broader context. - **`MissingConstraint`** — existing diagnostic; in the new model carries the candidate class set when the bare method is ambiguous at a polymorphic site lacking a declared constraint (Trajectory D failure mode). - **`MethodNameCollision`** — variant DELETED in Iter 3. - **Class-fn collision warning** (Iter 3) — new structured warning, fires when a `Term::Var { name }` resolves via fn lookup precedence AND a class method of the same name exists with an instance for the arg type. Structured-diagnostic code: `class-method-shadowed-by-fn`. Implementer drafts the wording. ## Testing strategy ### Iter 1 — canonical-form extension - **Validator pin tests:** symmetric to the existing `class_param_in_applied_position_fires_canonical_form_rejection`. Three new tests: - Bare cross-module `InstanceDef.class` fires `BareCrossModuleClassRef` (or reused variant); message names candidate qualified forms from the owning module's imports. - Bare cross-module `Constraint.class` fires the same. - Bare cross-module `SuperclassRef.class` fires the same. - **Round-trip:** `examples/prelude.ail.json` parses + canonicalises bit-stable post-migration (zero diff for the prelude; all internal class-refs stay bare). - **Cross-module fixture:** a workspace with `instance prelude.Eq` (the qualified form) loads and checks cleanly; mirrors the existing cross-module fixture pattern from milestone 23. - **Migration coverage:** the 14 `examples/test_22b*` fixtures parse + canonicalise post-migration; `cargo test --workspace` green unchanged. ### Iter 2 — type-driven dispatch mechanism - **Unit tests on `resolve_method_dispatch`** (or whatever the implementer names the new function). Six cases, each as an isolated unit test calling into the dispatch logic with synthetic inputs: - Unique candidate: returns the unique class. - Multi-candidate + explicit qualifier matching one: returns that class. - Multi-candidate + explicit qualifier matching none: `UnknownClass`. - Multi-candidate + type-driven filter narrows to one: returns that class. - Multi-candidate + constraint-driven filter narrows to one (rigid var case): returns that class. - Multi-candidate + neither filter narrows: `AmbiguousMethodResolution`. - **Structured-diagnostic pin tests** for the new diagnostic JSON shapes (`ambiguous-method-resolution`, `unknown-class`). - **Existing end-to-end tests unchanged.** `MethodNameCollision` still gates real workspaces. - **Bench regression** held or audit-ratified. ### Iter 3 — `MethodNameCollision` retirement + multi-class E2E - **Repurposed pin tests:** the two `workspace.rs:1931, 1965` tests re-asserting no-error on the same fixtures plus `method_to_candidate_classes` carries 2 entries. - **Three new positive E2E fixtures** (under `examples/`, naming TBD by implementer): - Two-module workspace with two `Show` classes; bare `show 42` fires `AmbiguousMethodResolution`. - Same workspace; explicit `.Show.show 42` resolves cleanly, stdout matches. - Two-module workspace with `class Eq` + `fn eq`; bare `eq x y` resolves per precedence + warning (or fails closed; see Architecture). - **DESIGN.md content audit:** the existing class-schema diagnostics section + the dispatch story are present and accurate. - **Bench regression** at milestone close: three scripts exit 0 or audit-ratified per audit-skill convention. ## Acceptance criteria 1. **Iter 1 landed:** three class-ref fields canonicalised across schema, validator, and consumers; ct.1 validator extended; prelude + 14 test fixtures migrated; existing tests green. 2. **Iter 2 landed:** `method_to_candidate_classes` index installed; synth Var-arm rewritten per the 5-step rule; multi-candidate residual + discharge refinement implemented; `AmbiguousMethodResolution` + `UnknownClass` diagnostic variants shipped; unit tests cover the 6 cases; existing E2E tests unchanged. 3. **Iter 3 landed:** `MethodNameCollision` variant + pre-pass + Display arm struck; pin tests repurposed; three new positive E2E fixtures shipping; DESIGN.md amended with the new dispatch subsection. 4. `cargo test --workspace` green across all three iters. 5. Bench regression: `bench/check.py && bench/compile_check.py && bench/cross_lang.py` exit 0 or audit-ratified with journal entry. 6. **Roadmap update:** P2 entry "Module-qualified class names + type-driven method dispatch" → `[x]`; milestone 24 `depends on:` line removed; milestone 24 entry marked "ready for re-brainstorm"; `WhatsNew.md` entry shipped on Iter-3 close. ## Out of scope (deferred, with substantive rationale) - **Milestone 24 (Show + print rewire).** Re-brainstorms separately against the post-retirement architecture per the deferral note at `docs/specs/0022-24-show-print.md`'s Status header. The re-brainstorm is queued automatically once Iter 3 closes. - **Overlapping instances within a single class.** Already handled by `DuplicateInstance` (`workspace.rs:680`). Not affected by this milestone; two instances `Show Int` from the same class still error out. - **Open type families / functional dependencies.** Substantial feature; not part of this milestone's scope. - **Higher-kinded class params.** Decision 11 axis 5 explicitly excludes higher-kinded class params; this milestone does not change that. - **Renaming or removing `ModuleGlobals::class_methods`.** Stays; the new `method_to_candidate_classes` index lives alongside. `class_methods` continues to serve callers that want quick (method-name → first-class-entry) lookup. Implementer audits in Iter 3 whether the channel becomes dead code post-retirement; if so, retirement is a separate P3 tidy. - **Open commitment on the surface-form question.** The qualified-call form `prelude.Show.show 42` is the canonical (JSON) shape via dotted `Term::Var.name`. The .ail Surface form's lexer/parser already handles dotted identifiers; no surface parser change needed. If a future surface ergonomics question (e.g. dedicated `#`-style or `::`-style class-method syntax) surfaces, it's a separate spec. - **Mass migration of existing fixtures to use cross-module class refs.** Iter 1 migrates only what needs to migrate (cross-module refs); same-module refs stay bare per the canonical-form rule. No proactive rewrite to "demonstrate" qualified refs. ## Open commitments (implementer choices) - **Multi-candidate residual representation.** Spec prescribes "the residual carries the candidate set and the `type_` metavar; discharge filters by `(class, type_hash) ∈ Registry` or by active declared constraints". Implementer chooses: extend `ResidualConstraint` with an optional `candidates: Option>` field, or add a sibling residual type. Constraint: the existing single-class discharge path stays usable. - **Sibling vs extended diagnostic variant for class-ref canonical-form rejection.** Default in this spec: sibling `BareCrossModuleClassRef` (because user-facing wording differs between "type" and "class"). Implementer may collapse into the existing `BareCrossModuleTypeRef` with a `kind` field if the saving is real and the diagnostic text remains clear. - **Class-fn collision behaviour.** Default: lookup precedence (fn wins over class method) + structured warning `class-method-shadowed-by-fn`. Alternative: hard-error `AmbiguousMethodResolution`-style. The default avoids breaking the existing fn-lookup-precedence rule for non-class-method cases (`prelude.ne` shadowing in user code, etc.); the warning surfaces the rare accidental case. If the implementer's prototyping uncovers a concrete case where the warning is annoying or the hard-error is required for correctness, escalate via the per-iter journal. - **Diagnostic wording.** Implementer drafts the user-facing message text for `AmbiguousMethodResolution`, `UnknownClass`, the new ct.1 class-ref diagnostic, and the `class-method-shadowed-by-fn` warning. Orchestrator reviews in spec-compliance phase of each iter. - **`ModuleGlobals::class_methods` retirement.** Iter 3 audits whether any consumer remains after the new index lands. If none, a P3 tidy item gets queued; if real consumers exist (e.g. mono's residual rewriter at `mono.rs:1233`), the channel stays and the new index lives alongside. ## Known costs - **Iter 1:** schema migration touchpoints — `examples/prelude.ail.json` ~0 lines (intra-prelude refs stay bare); 14 test fixtures (only cross-module refs, estimate ~10–20 lines total); two test Rust files (assertions migrated where they reference cross-module class strings, estimate ~10 lines). ct.1 validator: ~50 LOC for three new field walks + 0–1 new diagnostic variant + Display arm. Registry-key migration: ~10 sites across `workspace.rs` + `mono.rs` + `check/lib.rs` reading the class key, all mechanical (qualified-string convention, no type change). - **Iter 2:** new `method_to_candidate_classes` index + builder ~30 LOC. Synth Var-arm rewrite ~40 LOC (replaces existing ~30 LOC at `lib.rs:1968-1996`). New residual variant + discharge logic ~60–80 LOC. Two new `CheckError` variants ~30 LOC. Unit tests for the new dispatch function ~150–200 LOC. - **Iter 3:** variant + pre-pass + Display arm + helper deletion: net −150 LOC. Three new E2E fixtures + assertions ~200 LOC. DESIGN.md amendment ~30 lines. WhatsNew entry ~5 lines. - **Net code:** approximately neutral across the milestone. Iter 1 is mostly migration (small net positive). Iter 2 adds the mechanism. Iter 3 deletes the workaround. The point of the milestone is not size reduction; it's lifting an unjustified workspace-global invariant. - **Compile-time shift:** the new dispatch path consults `method_to_candidate_classes` per `Term::Var` matching a class method. The lookup is `BTreeMap::get` plus filtering of a small set; net cost per class-method call site is O(|candidates|), bounded by the number of classes that declare a same-named method (workspace- wide, currently zero by `MethodNameCollision`; post-retirement, small). Expected within bench tolerance. ## Load-bearing assumptions about current behaviour Surfaced for Step 7.5 grounding-check. 1. ct.1's `validate_canonical_type_names` validator (`crates/ailang-core/src/workspace.rs:921`) is the active gate for the canonical-form rule on `Type::Con.name` and `Term::Ctor.type_name`. Ratified by the canonical-type-names milestone close (`audit-ct-tidy`, journal `docs/journals/2026-05-12-audit-ct-tidy.md`). 2. `WorkspaceLoadError::BareCrossModuleTypeRef` (`workspace.rs:341`) is the existing diagnostic for bare cross-module type refs, ratified by the test `class_param_in_applied_position_fires_canonical_form_rejection` plus the `BareCrossModuleTypeRef` pin tests at `workspace.rs:2114, 2136`. 3. `ClassDef` (`crates/ailang-core/src/ast.rs:260`) has fields `name: String` (the defining class name, bare per the convention), `superclass: Option` (optional single superclass), and `methods: Vec`. 4. `SuperclassRef.class` is a `String` at `crates/ailang-core/src/ast.rs:279`; today carries bare names; the migration target. 5. `InstanceDef.class` is a `String` at `crates/ailang-core/src/ast.rs:314`; today carries bare names; the migration target. 6. `Constraint.class` is a `String` at `crates/ailang-core/src/ast.rs:345`; today carries bare names; the migration target. 7. `WorkspaceLoadError::MethodNameCollision` (`workspace.rs:303`) lives with a `kind: &'static str` discriminator; ratified by the two pin tests at `workspace.rs:1931` and `workspace.rs:1965`. 8. The `MethodNameCollision` pre-pass at `workspace.rs:547–627` is the single workspace-load-time enforcement point of the method-name-uniqueness invariant; nothing else enforces this invariant. 9. `ClassMethodEntry` (in `crates/ailang-check/src/lib.rs`) carries fields `class_name: String`, `class_param: String`, `method_ty: Type`, `defining_module: String`. Today `class_name` is bare. 10. `ModuleGlobals::class_methods: IndexMap` (`crates/ailang-check/src/lib.rs:1075`) is keyed by method name and consumed in synth's Var-arm at `crates/ailang-check/src/lib.rs:1968`. 11. `build_registry` (`workspace.rs:521`) builds `entries: BTreeMap<(String, String), RegistryEntry>` keyed by `(bare_class_name, type_hash)`; consumed by mono's instance lookup and the workspace-load-time coherence check (`workspace.rs:680` for the `DuplicateInstance` check). 12. Synth's Var-arm at `crates/ailang-check/src/lib.rs:1968` is the single resolution point for `Term::Var { name }` where the name resolves to a class method; rewriting this arm covers every class-method call site. 13. `ResidualConstraint` (`crates/ailang-check/src/lib.rs:1692`) discharge happens at function-body check time for monomorphic discharge and via `Type::Forall.constraints` propagation for polymorphic discharge. Discharge sites: `lib.rs:1627` (`MissingConstraint`) and `lib.rs:1651` (`NoInstance`). 14. Mono's class-method residual rewriter (`crates/ailang-check/src/mono.rs:1233` and surrounding) uses the `class_methods` map to identify class-method call sites; this consumer is in scope for Iter 2. 15. The 14 test fixtures named in the deferral note (`examples/test_22b{1,2,3}_*.ail.json`) declare user-classes named `Show`. The prelude (`examples/prelude.ail.json`) has no `Show` class today (only `Eq`/`Ord` per milestone 23). 16. The canonical-form rule at ct.1 fires the validator BEFORE class-schema validation (`validate_classdefs` at `workspace.rs:491`), so the new class-ref canonical-form check fires before downstream class-schema diagnostics. 17. `examples/prelude.ail.json` intra-module class refs (`Eq` referenced from `Ord`, `Eq`/`Ord` referenced from instances and constraints inside the prelude) stay bare under the canonical-form rule; post-Iter-1 the prelude file is unchanged for class-ref fields. 18. `class_def_module` (built in `build_registry` pass-1 at `workspace.rs:526`) is the `BTreeMap` mapping bare class names to defining modules; this map's key type migrates to qualified class names in Iter 1.