From 512fc9d5fd341c294021236009c60479cb1a37f1 Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 00:30:37 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20module-qualified-class-names=20?= =?UTF-8?q?=E2=80=94=20class-ref=20canonical-form=20+=20type-driven=20disp?= =?UTF-8?q?atch=20+=20MethodNameCollision=20retirement?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Retires the workspace-global MethodNameCollision pre-pass (crates/ailang-core/src/workspace.rs:547) via a phased three-iter milestone. Iter 1 canonicalises InstanceDef.class, Constraint.class, and SuperclassRef.class (extends ct.1's validator); Iter 2 installs type-driven dispatch (method_to_candidate_classes index + multi- candidate residual + AmbiguousMethodResolution / UnknownClass diagnostics) while the workaround still gates real workspaces; Iter 3 deletes the pre-pass and ships multi-class E2E plus DESIGN.md sync. Unblocks the deferred milestone 24 (Show + print rewire). Step 7.5 grounding-check PASS: all 18 load-bearing assumptions ratified by named, currently-green tests. --- ...2026-05-13-module-qualified-class-names.md | 617 ++++++++++++++++++ 1 file changed, 617 insertions(+) create mode 100644 docs/specs/2026-05-13-module-qualified-class-names.md diff --git a/docs/specs/2026-05-13-module-qualified-class-names.md b/docs/specs/2026-05-13-module-qualified-class-names.md new file mode 100644 index 0000000..4afc946 --- /dev/null +++ b/docs/specs/2026-05-13-module-qualified-class-names.md @@ -0,0 +1,617 @@ +# 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/2026-05-10-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/2026-05-12-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.