AILang/docs/specs/0023-module-qualified-class-names.md

# 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 (`<module>.<Class>.<method> <args>`) 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 (`<module>.<Class>`) 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<String, String>` (the
  bare-class-name → defining-module map) becomes
  `class_def_module: BTreeMap<QualifiedClassName, String>` keyed by the
  qualified class name (`<defining_module>.<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<MethodName, BTreeSet<QualifiedClassName>>` 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: <qualified>, 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<String, BTreeSet<QualifiedClassName>>` 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<QualifiedClassName>, 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<String> }` 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 (`<method>__<typesurfacename>` with cross-module `<defining_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 `<modA>.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 `<modA>.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<BTreeSet<...>>` 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<SuperclassRef>` (optional single
   superclass), and `methods: Vec<ClassMethod>`.

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<String, ClassMethodEntry>`
    (`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<String, String>` mapping bare
    class names to defining modules; this map's key type migrates to
    qualified class names in Iter 1.