spec: canonical type names — name MethodNameCollision as the workaround it is
This commit is contained in:
@@ -263,39 +263,54 @@ many ambiguity cases are caught earlier by the validator.
|
||||
|
||||
- **Class names** (`ClassDef.name`, `InstanceDef.class`,
|
||||
`SuperclassRef.class`, `Constraint.class`): NOT migrated to the
|
||||
module-scoped canonical form in this milestone. The asymmetry to
|
||||
Type::Con is intentional and rests on a real semantic difference:
|
||||
module-scoped canonical form in this milestone — but we name the
|
||||
reason honestly rather than dressing it as "different semantics".
|
||||
|
||||
- For types, no workspace-global uniqueness rule exists. Two modules
|
||||
may independently declare `type Foo`. Bare cross-module references
|
||||
are therefore genuinely ambiguous; the iter-23.3 bug is the
|
||||
concrete instance of that ambiguity surfacing in unification.
|
||||
The asymmetry is structural, not semantic. AILang's class-method
|
||||
resolution today (`ModuleGlobals::class_methods: IndexMap<String,
|
||||
ClassMethodEntry>`, `crates/ailang-check/src/lib.rs:983`, consumed
|
||||
by `mono::rewrite_class_method_calls`,
|
||||
`crates/ailang-check/src/mono.rs:657-665`) is **name-driven**: the
|
||||
call `eq x y` is resolved by looking up `"eq"` and getting back
|
||||
exactly one `ClassMethodEntry` carrying its `class_name` and
|
||||
`defining_module`. The class is reverse-inferred from the method.
|
||||
|
||||
- For classes, workspace-global uniqueness is enforced one level
|
||||
deeper: `WorkspaceLoadError::MethodNameCollision` (iter 22b.2,
|
||||
`workspace.rs:472`) rejects two classes that share any method
|
||||
name. Two `class Eq`s with the conventional `eq` method cannot
|
||||
coexist; `class_by_name: BTreeMap<String, &ClassDef>` (workspace-
|
||||
flat) is consistent with that invariant. Empirically no
|
||||
`examples/` fixture today has a bare cross-module class
|
||||
reference that resolves ambiguously — the cross-module fixtures
|
||||
that exist (`test_22b3_xmod_e2e_main`) call methods bare and rely
|
||||
on the method→class→instance chain, never on a direct class-name
|
||||
reference.
|
||||
That single-entry guarantee is what `WorkspaceLoadError::MethodNameCollision`
|
||||
(iter 22b.2, `workspace.rs:472`) enforces at load time. The
|
||||
causal chain is:
|
||||
|
||||
Three class-reference fields (`InstanceDef.class`,
|
||||
`SuperclassRef.class`, `Constraint.class`) gain a *defensive*
|
||||
validator check in ct.1: reject qualified forms (containing `'.'`)
|
||||
explicitly, since the schema does not currently model qualified
|
||||
class names. This prevents half-migrated files from silently
|
||||
loading.
|
||||
1. Class names are bare in the AST.
|
||||
2. → Class lookup is `BTreeMap<String, &ClassDef>` (workspace-flat,
|
||||
bare-keyed).
|
||||
3. → For method resolution to be tractable from a bare `Term::Var
|
||||
{ name: "eq" }`, the method name must resolve to a unique class.
|
||||
4. → `MethodNameCollision` enforces uniqueness as a load-time
|
||||
invariant.
|
||||
|
||||
If AILang ever revisits workspace-global method-name uniqueness
|
||||
(e.g. introduces module-qualified method names so two libraries
|
||||
can each declare `class Eq` with its own `eq`), the symmetry to
|
||||
Type::Con returns and class names will need the same module-scoped
|
||||
treatment. That is a separate DESIGN-level milestone and is not
|
||||
this spec's scope.
|
||||
In other words: `MethodNameCollision` is the load-time constraint
|
||||
that makes bare class names viable. Qualifying class names in the
|
||||
AST would not pay off in isolation — it would force step 3 to be
|
||||
replaced with type-driven dispatch (look up `eq` candidates by
|
||||
argument type, Haskell-style), which is a Designfeld of its own
|
||||
with implications for inference, ambiguity rules, and diagnostic
|
||||
shape. That is out of scope here; this milestone is canonical
|
||||
type names, not a typeclass-dispatch overhaul.
|
||||
|
||||
What this spec DOES do for class-reference fields
|
||||
(`InstanceDef.class`, `SuperclassRef.class`, `Constraint.class`):
|
||||
ct.1's validator rejects *qualified* forms (containing `'.'`) on
|
||||
those fields. The schema does not currently model qualified class
|
||||
names; the rejection prevents half-migrated files from silently
|
||||
loading. `ClassDef.name` itself remains bare (the file-top
|
||||
`"name"` is the module context, same as `TypeDef.name`).
|
||||
|
||||
Forward note: if AILang ever revisits name-driven method
|
||||
dispatch — e.g. to allow two libraries to each declare `class
|
||||
Eq` with its own `eq` — the symmetry returns and class names
|
||||
will then need the same module-scoped treatment, along with
|
||||
type-driven method resolution. That is a separate DESIGN-level
|
||||
milestone and is named here so the workaround is visible rather
|
||||
than buried.
|
||||
|
||||
- **Surface notation in `.ailx`**: bare local names continue to be
|
||||
the LLM-author convention. Prose parser/printer bridge — no
|
||||
|
||||
Reference in New Issue
Block a user