AILang/design/contracts/typeclasses.md

Typeclasses

Form-A schema (the JSON authoring surface)

Three additive schema extensions; no existing module becomes invalid.

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 (per Decision 11's milestone-23.4 reorganisation) 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 Decision 11 coherence). 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, milestone-23-shape 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.

The three invariants are lockstep partners: invariant (1) creates the cross-module reference, invariant (2) makes codegen able to resolve it, invariant (3) makes the typecheck-time discharge fire correctly when no instance exists. A future refactor that loosens any one of the three breaks the user-ADT trajectory; 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), 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" below.

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. mq.2 adds an optional candidate_classes field surfacing the multi-candidate set when the bare-method dispatch path's filter collapses to zero registry survivors.
• AmbiguousMethodResolution (mq.2) — 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 (mq.2) — 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 (mq.3, 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" below).

Method dispatch

Post-mq.3, dispatch is two-mode:

Polymorphic call sites (inside a fn body with forall + constraint set): the constraint names the class via the qualified Constraint.class field (canonical-form per mq.1). Synth's residual carries the class name directly; constraint-discharge at fn-body-end matches against the workspace registry by (class, type_hash) key.

Monomorphic call sites: synth consults the workspace-flat Env.method_to_candidate_classes: BTreeMap<MethodName, BTreeSet<QualifiedClassName>> index, then runs the 5-step dispatch rule:

1. Parse the Term::Var.name for an optional class qualifier (last-dot-segment is the method name; everything before is the qualified class).
2. If method_to_candidate_classes has no entry for the method name, fall through to the existing Var-arm branches (free fn lookup, dot-qualified cross-module).
3. Qualifier present: filter candidates to the named class. Empty result fires UnknownClass. Singleton survivor proceeds.
4. Qualifier empty (bare-method form): singleton candidate proceeds directly; multiple candidates yield a multi-candidate residual for discharge-time refinement.
5. At discharge, refinement runs: concrete type_ filters candidates via the workspace registry; rigid-var type_ filters via the active fn's declared constraints (env.active_declared_constraints). Single survivor discharges; multiple survivors fire AmbiguousMethodResolution (concrete) or MissingConstraint (rigid-var); zero survivors fire NoInstance (concrete) or MissingConstraint (rigid-var).

The method_to_candidate_classes index is the load-bearing data structure for this routing — its construction in build_check_env inverts the per-module class_methods maps (themselves tuple-keyed by (qualified-class, method) post-mq.3) to a workspace-flat method-name-to-class-set map.

Class-fn collisions resolve at the call site, not at workspace load time: the fn lookup precedence (locals → caller-module-fn → imported-fn) runs ahead of the class-method branch. When both sides have a match, the fn wins and a class-method-shadowed-by-fn warning surfaces the shadow.

Prelude (built-in) classes

The prelude ships the Ordering ADT, the Eq and Ord classes, primitive Eq Int/Bool/Str and Ord Int/Bool/Str instances, and the five polymorphic free-fn helpers ne/lt/le/gt/ge. Float has neither Eq nor Ord instance per §"Float semantics"; a polymorphic helper invoked at Float fires NoInstance at typecheck with a Float-aware diagnostic cross-referencing this section.

The prelude ships class Show a where show : (a borrow) -> Str and primitive Show Int, Show Bool, Show Str, Show Float instances. Float is included in Show (unlike Eq/Ord) — IEEE-754 makes structural equality and total ordering semantically dubious, but textual representation of a Float is well-defined modulo the NaN-spelling caveat in §"Float semantics". Each Show <T> instance body is a single-application lambda invoking the corresponding runtime primitive (int_to_str, bool_to_str, str_clone, float_to_str); no codegen intercept is required. The polymorphic helper print : forall a. Show a => a -> () !IO has body \x -> let s = show x in do io/print_str s (explicit let-binder for heap-Str RC discipline per eob.1 Str carve-out). The let-binder is structurally pinned by crates/ail/tests/print_mono_body_shape.rs. Routing through print is the path for non-Str primitives; io/print_str is the only built-in direct-output effect-op.

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