spec: module-qualified-class-names — class-ref canonical-form + type-driven dispatch + MethodNameCollision retirement
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.
This commit is contained in:
@@ -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 (`<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/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 (`<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/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<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.
|
||||
Reference in New Issue
Block a user