# Typeclasses

The schema, registry, and diagnostic contract for the typeclass
layer. The resolution/monomorphisation whitepaper lives at
[models/typeclasses](../models/0005-typeclasses.md); the call-site
lookup rule at [method dispatch](0016-method-dispatch.md); the built-in
classes the prelude ships at [prelude classes](0017-prelude-classes.md).

## Form-A schema (the JSON authoring surface)

Three additive schema extensions; no existing module becomes invalid.
The canonical schema for `ClassDef`, `InstanceDef`, and the
`FnDef.type` constraints field lives in
[Data model](0002-data-model.md); this section is the typeclass-layer
narrative.

**`ClassDef`** — top-level definition kind, declares a class:

```
{ "kind": "class",
  "name": "Show",
  "param": "a",
  "superclass": null,
  "methods": [
    { "name": "show",
      "type": { /* full FnSig over `a`, with mode annotations */ },
      "default": null
    }
  ]
}
```

`superclass` is either `null` or `{ "class": <name>, "type": "a" }`
where `"a"` MUST be the same identifier as the class's own `param`.
`default` is either `null` (method is abstract-required at instance
sites) or an AST body (method is optional with the body as fallback).

**`InstanceDef`** — top-level definition kind, declares an instance:

```
{ "kind": "instance",
  "class": "Show",
  "type": "Int",
  "methods": [
    { "name": "show", "body": <AST> }
  ]
}
```

`type` is a concrete type expression, never the class param. `methods`
contains the bodies for every required method plus optional overrides
of default-bearing methods.

**`FnDef.type` extension** — the existing FnSig schema gains a
`constraints` sibling field next to `forall`:

```
"type": {
  "forall": ["a"],
  "constraints": [{ "class": "Show", "type": "a" }],
  "type": ["Fn", [...], "String"]
}
```

When `forall` is empty, `constraints` is also empty (and may be
omitted for hash stability of older definitions). Each constraint's
`type` field MUST reference a type variable bound by the surrounding
`forall`.

**Method invocation sites do NOT get a new node.** A call to a class
method is a normal `Call` node; resolution against a class is the
typechecker's job, not the parser's. The LLM author writes `show x`
exactly as for any free function.

## Cross-module references in synthesised bodies

The unified mono pass (see
[models/typeclasses](../models/0005-typeclasses.md) for the
resolution/monomorphisation algorithm) synthesises mono symbols for
polymorphic free fns and class-method instances in the symbol's
owner module — e.g. `print__Int` lives in `prelude` (because `print`
is defined in the prelude), but a user-ADT call site
`print (MkIntBox 7)` causes synthesis of `prelude.print__IntBox`
whose body references `show_user_adt.show__IntBox` (the user
instance lives in the user-defining module per the
orphan-free-coherence rule documented in
[models/typeclasses](../models/0005-typeclasses.md)). The synthesised
body crosses a module boundary the source template did not.

Three invariants make this work:

1. **`MonoTarget::FreeFn::type_args` carries canonical types
   post-collection.** At every site where `subst.apply(m)` produces a
   concrete substitution that enters `MonoTarget::FreeFn::type_args`
   (`crates/ailang-check/src/mono.rs::collect_mono_targets` and
   `::collect_residuals_ordered`), the resolved `Type` must be passed
   through `Registry::normalize_type_for_lookup(caller_module, &t)`
   before being pushed. The downstream synthesised body's Phase 3
   rewrite cursor (which runs in the OWNER module's context, not the
   caller's) keys lookups in `Registry::entries` by the canonical
   qualified form; a bare type-con reference at the type_args layer
   silently drops the cross-module mono-symbol synthesis and leaves a
   bare `Var "show"` post-mono that codegen later rejects with
   `unknown variable`.

2. **Post-mono synthesised body cross-module references may bypass
   the source template's `import_map`.** `prelude` does not import
   user modules (the auto-injection runs one-way: user workspaces
   import prelude, never the inverse). But a synthesised body for
   `prelude.print__<UserType>` references `<user_module>.show__<UserType>`,
   created by mono — not by the prelude source. Codegen's
   cross-module name-resolution must accept this: at
   `crates/ailang-codegen/src/lib.rs::resolve_top_level_fn` (Var-
   resolution), `::lower_app`'s cross-module call arm, and
   `::synth_with_extras`'s Var arm, the resolution first tries the
   current module's `import_map`, then falls back to a direct
   `module_user_fns` / `module_def_ail_types` lookup against the
   prefix. Both ends were independently typechecked under their own
   module contexts before mono ran; the cross-module reference is a
   post-mono construct, not a source-language one.

3. **FreeFnCall synth pushes one residual per declared forall-
   constraint.** At `crates/ailang-check/src/lib.rs`'s synth Var arm
   for the `prefix.suffix` free-fn path, when the type is a
   `Type::Forall { vars, constraints, body }`, instantiation produces
   fresh metavars for the `vars` AND pushes one `ResidualConstraint`
   per entry in `constraints` (with rigid vars substituted by the
   freshly-generated metavars). The downstream discharge loop at
   `check_fn`'s post-synth phase resolves each residual against the
   workspace registry; if no instance satisfies the residual at the
   unified concrete type, the `NoInstance` diagnostic fires at
   typecheck (correctly), not at codegen (confusingly). Without the
   residual push, polymorphic-helper negative cases (e.g. `print f`
   where `f : Int -> Int`) silently typecheck and surface as
   `unknown variable: show` from codegen instead of the right
   typecheck-phase NoInstance Show.

4. **Bare-prelude-fn calls resolve via implicit-prelude-import at
   typecheck AND at codegen.** A user-module source-level call
   `(app float_eq 1.5 1.5)` writes the bare name `float_eq`, not
   the qualified form `prelude.float_eq`. The typechecker resolves
   this via the auto-injected prelude import (see invariant (2)
   for the one-way auto-injection rule); codegen's
   `lower_app::resolve_callee` + `is_static_callee` + `resolve_top_level_fn`
   each carry a parallel prelude-fallback: when the bare name does
   not resolve in the caller-module's symbol table, fall back to
   `prelude.<name>`. This is the source-level counterpart to
   invariant (2)'s post-mono fallback — both make the implicit-
   prelude-import a workspace invariant rather than a typechecker-
   only feature. The fallback is load-bearing for the surface
   `(app float_eq …)` / `(app float_lt …)` / etc. of the
   operator-routing-eq-ord milestone; without it the LLM-author
   must write `prelude.float_eq` explicitly, which is exactly the
   syntactic noise the implicit import exists to eliminate.

The four invariants are lockstep partners: invariant (1) creates the
cross-module reference, invariant (2) makes codegen able to resolve
post-mono references, invariant (3) makes the typecheck-time
discharge fire correctly when no instance exists, invariant (4)
makes bare prelude-fn names resolve from user modules at the source
level. A future refactor that loosens any one of the four breaks
the user-ADT trajectory or the Float-named-fn surface; the test
pins at
`crates/ail/tests/codegen_import_map_fallback_pin.rs` (invariant 2),
`crates/ail/tests/polyfn_dot_qualified_branch_pin.rs` (invariant 3
+ lockstep), `crates/ail/tests/float_compare_smoke_e2e.rs`
(invariant 4 — drives `(app float_eq …)` end-to-end across the
implicit-prelude-import boundary), and the existing
`crates/ail/tests/show_user_adt` fixture (full trajectory)
collectively protect the contract.

## Defaults and superclasses

**Defaults.** A `ClassDef.methods[i].default` is either `null` (the
method is required at instance level) or an AST body. When an
`InstanceDef` does not specify a method that has a default, the
typechecker uses the default body for that instance, with the class
param substituted to the instance type. Default bodies may call
other methods of the same class (the canonical example is
`default ne x y = not (eq x y)`); the called methods resolve at
monomorphisation time against the same instance.

**Superclasses.** A `ClassDef.superclass` of `{ "class": "Eq",
"type": "a" }` declares that any `instance C T` requires a
corresponding `instance Eq T` to exist. The check fires at
workspace-load time: for each `InstanceDef` whose class declares a
superclass, the registry is queried for the matching superclass
instance. Missing → `MissingSuperclassInstance`.

**Superclass auto-expansion in constraint contexts.** When a function
declares `Ord a` as a constraint, the typechecker treats the constraint
context as `{ Ord a, Eq a }` for the purposes of `MissingConstraint`
checking. This is the one deviation from "alles sichtbar": the
extension is anchored in the class's own `superclass` field, so the
relation is schema-visible at the class declaration even when the
constraint at the function site reads `Ord a` alone.

Superclass chains are linear (single-superclass relation per class)
and auto-expansion closes transitively across the chain.

**No `deriving`.** AILang does not auto-derive instances. `instance Eq
MyType` must be written by hand.

## Diagnostic categories

The typeclass layer introduces three families of diagnostics. Exact
wording is fixed; the categories and their triggers are:

**Workspace-load (registry-build) diagnostics:**

- `OrphanInstance` — instance is not in class's or type's module.
- `DuplicateInstance` — two instances match the same key.
- `MissingSuperclassInstance` — superclass instance absent.
- `MissingMethod` — instance omits a required method.
- `OverridingNonExistentMethod` — instance specifies a method not in
  the class.

Cross-class method sharing is structurally legal; ambiguity surfaces
at the call site via `AmbiguousMethodResolution` or, for class-fn
name overlap, via the `class-method-shadowed-by-fn` warning. See
[Method dispatch](0016-method-dispatch.md).

**Class-schema diagnostics** (validation of class declarations):

- `InvalidSuperclassParam` — superclass `type` differs from the
  class's own `param`.
- `ConstraintReferencesUnboundTypeVar` — a constraint mentions a
  type variable not bound by the surrounding `forall`.

A class param appearing in applied position (e.g., `f a` where `f`
is the class param) is rejected earlier by the canonical-form
validator as `BareCrossModuleTypeRef` — `f` is a bare,
non-primitive name not declared as a `TypeDef` in the owning
module.

**Typecheck diagnostics** (per function body):

- `MissingConstraint` — body's residual constraint is not covered
  by declared (and superclass-expanded) constraints.
- `NoInstance` — fully concrete constraint has no registry entry.
  Carries an optional `candidate_classes` field surfacing the
  multi-candidate set when the bare-method dispatch path's filter
  collapses to zero registry survivors.
- `AmbiguousMethodResolution` — a monomorphic `Term::Var`
  call site survives both type-driven and constraint-driven filters
  with more than one candidate class. LLM-author writes the explicit
  qualifier form `<module>.<Class>.<method>` to disambiguate.
- `UnknownClass` — an explicit class qualifier in
  `Term::Var.name` names a qualified class that is not in the
  workspace's candidate-class index for the method.
- `class-method-shadowed-by-fn` (warning) — a `Term::Var`
  resolved via fn lookup precedence (locals → caller-module-fn →
  imported-fn) while a class method of the same name also exists
  in the workspace. Fn resolution proceeds; the warning surfaces
  the shadow so the LLM-author can disambiguate via explicit
  class-qualified call if the shadow was unintentional.

There is no `AmbiguousInstance` diagnostic at the registry level —
coherence (`DuplicateInstance` at registry build, W2) makes
per-`(class, type)` ambiguity structurally impossible. Cross-class
method ambiguity is a separate concern resolved at the call site
via `AmbiguousMethodResolution` (see [Method dispatch](0016-method-dispatch.md)).

Ratified by: `crates/ail/tests/show_no_instance_e2e.rs`.
