AILang/docs/specs/0014-23-eq-ord-prelude.md

23 — Eq / Ord Prelude — Design Spec (revised)

Date: 2026-05-11 Status: Draft — awaiting user spec review Authors: Brummel (orchestrator) + Claude

Supersedes: docs/specs/2026-05-10-23-eq-ord-prelude.md (retired 2026-05-11 in iter gc.1; commit f6d4ba3). Iter 23.1–23.3 shipped under the original spec and remain in effect; this revised spec re-frames the remaining work on a corrected architecture.

Goal

Complete milestone 23 by shipping the five free top-level utility functions ne, lt, le, gt, ge in the auto-loaded prelude, plus the E2E and DESIGN.md amendments that close the Eq/Ord surface. Establish the partial-Eq/Ord story for Float as a lived reality: Float has neither instance, so polymorphic eq x y / compare x y over a Float fires NoInstance at typecheck — exactly what DESIGN.md §"Float semantics" prescribes.

The re-brainstorm exists because the original spec's architecture section silently assumed that polymorphic free fns with class constraints would be mono-specialised the same way class methods are. They are not — the typecheck-time mono pass (crates/ailang-check/src/mono.rs, iter 22b.3) operates only on class methods, while polymorphic free fns are specialised at codegen time by crates/ailang-codegen/src/lib.rs::lower_polymorphic_call (iter 12b). A polymorphic free fn whose body invokes class methods falls between the two passes. Iter 23.4 BLOCKED three times on this seam.

The corrected architecture unifies the two specialisers (see Architecture below) and ships the remaining free fns on top of the unified pass.

Prep-commit status (verified against main 2026-05-11 after iter/23.4 branch teardown): prep1 (linearity + checker bare-name) landed on main on 2026-05-11 via cherry-pick from the stranded iter/23.4 branch; it stays load-bearing. prep2 and prep3 (codegen bare-name fall-throughs) were attempted on the stranded iter/23.4 branch and never reached main; with iter/23.4 deleted, they are abandoned as git history without a rollback step. Their architectural intent — make codegen handle bare polymorphic free-fn names directly — is superseded by the mono-unification. The unified pass rewrites bare polymorphic call sites to mono symbols before codegen runs, making the fall-throughs structurally unnecessary.

Show, operator routing, print-rewire, and the heap-Str ABI remain out of scope; each is its own milestone with substantive reasons (see "Out of scope" — unchanged from original spec).

Architecture

The milestone no longer consumes the 22b.3 typeclass machinery unchanged. Three artefacts:

1. Mono-Pass unification (the corrected centrepiece)

crates/ailang-check/src/mono.rs::monomorphise_workspace is restructured into a single specialiser for every Type::Forall-quantified Def::Fn whose call sites supply fully-concrete substitutions. Two thin source-body entry points:

• Class-method entry: look up the resolved instance body via Registry::entries[(class, type-hash)]. Unchanged behaviour from iter 22b.3.
• Free-fn entry: take the source body directly from the polymorphic Def::Fn, apply rigid-var substitution.

Shared core mechanics — identical for both arms — are: rigid-var substitution via crate::substitute_rigids, fixpoint loop (mono.rs line 88) that keeps collecting targets until a round adds nothing new, dedup cache keyed by (name, type-hash), and the call-site-rewrite walker.

Output: synthesised Def::Fn entries with naming <name>__<typesurfacename> (extended to <name>__<type1>__<type2>__… for N-ary type vars in declaration order; concrete format is an Open commitment), appended to the defining module. The mono pass becomes the only specialiser; codegen sees no class machinery and no polymorphic call sites.

The current codegen-time specialiser is retired in the same iter: crates/ailang-codegen/src/lib.rs::lower_polymorphic_call, module_polymorphic_fns (the per-module FnDef map), and mono_queue (the deduplicated emission queue) are removed. All today's call sites of lower_polymorphic_call (lines 1944, 1972) become direct calls to mono symbols after the typecheck-mono walker has rewritten them.

2. Prelude AILang module

examples/prelude.ail.json already contains, from iters 23.1–23.3: the Ordering ADT, the Eq class with Eq Int/Bool/Str instances, the Ord class with Ord Int/Bool/Str instances. Iter 23.5 adds the five free fns:

• ne : forall a. Eq a => (a borrow, a borrow) -> Bool, body not (eq x y).
• lt, le, gt, ge: forall a. Ord a => (a borrow, a borrow) -> Bool, bodies pattern-matching compare against the appropriate Ordering shapes.

3. C-runtime functions

runtime/str.c shipped its two functions in iter 23.2 and 23.3: ail_str_eq(a, b) -> bool (byte-equality on constant-string layouts) and ail_str_compare(a, b) -> i32 (lex comparison returning -1/0/+1). No further runtime work.

Existing primitive operators (==, <, <=, >, >=) remain primitive and per-type-routed at lowering, unchanged. Routing them through the class methods is the declared P2 follow-up; the redundancy between primitive == and class eq x y on Int/Bool/Str is acknowledged and ratified as transitional.

Components (iterations)

Iter	Status	Scope
23.1	shipped (2026-05-10)	Ordering ADT + prelude skeleton + auto-load via check_workspace.
23.2	shipped (2026-05-10)	class Eq + Eq Int/Bool/Str + ail_str_eq.
23.3	shipped (2026-05-10)	class Ord extends Eq + Ord Int/Bool/Str + ail_str_compare.
23.4-prep	shipped to main 2026-05-11 (cherry-picked from stranded iter/23.4), kept	commits on main: 0caaced (linearity registers Def::Class method types in globals) + 923dd8c (check bare-name fall-through to implicit-imported free fns). Both resolve names before mono; independent of B1.
23.4-prep2 / 23.4-prep3	abandoned 2026-05-11 with iter/23.4 deletion — never reached main	Attempted-but-stranded commits were a06159d + c42a0f5 (codegen bare-name fall-throughs); they were anticipatory patches for an approach (codegen-time bare-name handling) the mono-unification supersedes. No rollback step is needed because no rollback target exists on main.
23.4 (revised)	upcoming	Mono-Pass unification. Restructure crates/ailang-check/src/mono.rs::monomorphise_workspace into one specialiser with two source-body entry points (class-method via Registry::entries, free-fn direct). Extend collect_mono_targets to also produce targets for polymorphic free-fn calls with fully-concrete substitutions. Remove lower_polymorphic_call + module_polymorphic_fns + mono_queue from codegen. Amend DESIGN.md §"Resolution and monomorphisation" to describe the pass as covering all Type::Forall-Defs. Tests: existing polymorphic fixtures (poly_id, poly_apply, poly_rec_capture) green; new fixture cmp_max_smoke proves cross-cutting (cmp_max : forall a. Ord a => (a, a) -> a at Int synthesises both cmp_max__Int and nested compare__Int in one fixpoint).
23.5 (revised)	upcoming	Prelude free fns + E2E. Add ne/lt/le/gt/ge to examples/prelude.ail.json. E2E fixtures: (a) positive polymorphic helper at Int/Bool/Str, (b) negative — eq f g at Float typecheck-rejects with Float-aware diagnostic, (c) user-ADT — IntBox with Eq/Ord instances + polymorphic helper monomorphises to the user instance. Amend DESIGN.md §"Decision 11 / Prelude classes" — Eq/Ord shipped; the "Milestone 22 ships no built-in Prelude classes" wording stays as historical accuracy with a forward-pointing addendum. Roadmap: P1 Post-22 Prelude entry from [~] to [x] for Eq/Ord half; Show half stays.

Data flow

Two trajectories show the unification at work.

Class-method call (eq x y) with x : Int (unchanged)

1. Typecheck. eq resolves to forall a. Eq a => (a borrow, a borrow) -> Bool. Constraint solver matches Eq Int against instance Eq Int; constraint discharged.
2. Mono (class-method entry). Registry::entries[(Eq, Int)] lookup, body from InstanceMethod, rigid-var subst a → Int, synth eq__Int. Call site eq x y → eq__Int x y.
3. Codegen. eq__Int lowers to icmp eq i64 + zext i1 i8.

Polymorphic free-fn call (ne x y) with x : Int (new with B1)

1. Typecheck. ne resolves to a polymorphic Def::Fn with forall a. Eq a => (a borrow, a borrow) -> Bool. Bare-name lookup reaches the prelude via prep1's env.module_globals fall-through. Constraint Eq Int discharged as above.
2. Mono (free-fn entry). Body taken directly from Def::Fn.body, rigid-var subst a → Int, synth ne__Int. In the same fixpoint round, the body walker detects the nested eq call at concrete Int and schedules it as a class-method target. The next round synthesises eq__Int (or cache-hits). ne__Int's body refers directly to eq__Int. Call site ne x y → ne__Int x y.
3. Codegen. ne__Int lowers as any monomorphic fn would; the nested eq__Int is a direct call. No lower_polymorphic_call path involved — the codegen-time specialiser no longer exists.

The fixpoint loop in monomorphise_workspace (line 88) already iterates until a round adds nothing new. The change is in the target collector: it must additionally emit MonoTargets for "call site to polymorphic free-fn Def::Fn with fully-concrete substitution", not only for class-constraint residuals.

Error handling

Unchanged from original spec:

• NoInstance Eq Float / NoInstance Ord Float — fired at typecheck when class resolution selects Float. Diagnostic must cross-reference DESIGN.md §"Float semantics" so the LLM-author immediately learns the partial-Float story.
• NoInstance Eq <UserType> / NoInstance Ord <UserType> — re-uses 22's existing diagnostic path.
• OrphanInstance — Decision 11 unchanged. Prelude instances are non-orphan.

New categories under B1:

• Polymorphic-free-fn specialisation failures are CheckError::Internal. The mono pass runs post-typecheck, so every substitution must have been validated by then. A failure here is a caller-contract violation; mirrors the existing convention in synthesise_mono_fn (mono.rs line 549).
• Recursive polymorphic free fns with concrete substitutions — the existing fixpoint loop closes transitively, same mechanism used for class-method bodies calling other class methods (e.g. default ne x y = not (eq x y)).
• Codegen-side errors remain not expected. The unification reduces codegen's responsibility (removes lower_polymorphic_call), it does not expand it. Any fall-through that survives must be CodegenError::Internal-shaped per the iter-4.4 Floats precedent — never unimplemented!() panic.

Testing strategy

23.4 — Mono unification

• Regression: existing polymorphic fixtures stay green. examples/poly_id.ail.json, examples/poly_apply.ail.json, examples/poly_rec_capture.ail.json, and every 22b.3 typeclass fixture must compile and run unchanged. These are the load-bearing proof that codegen-time specialisation was structurally replaceable.
• New: composition fixture. examples/cmp_max_smoke.ail.json with fn cmp_max : forall a. Ord a => (a, a) -> a (body: match compare x y with LT -> y | _ -> x), invoked at Int. The test asserts that after mono, the workspace contains both cmp_max__Int and compare__Int as Def::Fn, both produced by the unified pass. This pins the cross-cutting case that iter-23.4-prep3 unsuccessfully tried to patch.
• Hash-stability of existing mono symbols. eq__Int, compare__Str, and the four other already-synthesised symbols must produce identical bodies (and therefore identical hashes) under the unified pass. Pin test in the style of crates/ailang-core/src/hash.rs::ct4_migrated_fixtures_have_canonical_form_hashes.
• Rollback proof. cargo test --workspace green after removal of lower_polymorphic_call + module_polymorphic_fns + mono_queue. No test relies on the removed symbols.
• Bench regression check. bench/check.py / bench/compile_check.py re-run after 23.4. The mono pass does more work (two entry points, larger target sets per round); a measurable compile-time shift is expected and ratified per audit convention or rebaselined.

23.5 — Prelude free fns + E2E

• Workspace tests per free fn: ne, lt, le, gt, ge produce correct Bool on Int/Bool/Str, agree with their primitive-operator counterparts on a small smoke suite.
• Positive E2E examples/eq_ord_polymorphic.ail.json: polymorphic helper invoked at three primitives, prints expected output, compiles and runs end-to-end.
• Negative E2E: eq f g at Float typecheck-rejects with a Float-aware diagnostic; gold-standard test pins the message verbatim.
• User-ADT integration: examples/eq_ord_user_adt.ail.json — data IntBox = MkIntBox Int + instance Eq IntBox + instance Ord IntBox + polymorphic helper monomorphises to the user instances.
• Round-trip: prelude module + every new fixture passes Form-A parser + canonicaliser bit-stable.
• Bench regression check at milestone close: the three bench scripts exit 0 or audit-ratified.

Acceptance criteria

The milestone closes when:

1. 23.4 has landed: crates/ailang-check/src/mono.rs::monomorphise_workspace synthesises both class-method and polymorphic-free-fn mono Defs in one fixpoint loop. crates/ailang-codegen/src/lib.rs::lower_polymorphic_call + module_polymorphic_fns + mono_queue are removed. (prep2 + prep3 were never on main; no rollback step in scope.)
2. DESIGN.md §"Resolution and monomorphisation" amended: the pass description covers all Type::Forall-quantified Defs, not only class methods.
3. 23.5 has landed: examples/prelude.ail.json contains ne, lt, le, gt, ge with correct constraint signatures and bodies.
4. DESIGN.md §"Decision 11 / Prelude classes" amended: reflects Eq/Ord shipping in milestone 23; the "Milestone 22 ships no built-in Prelude classes" wording stays as historical accuracy with a forward-pointing addendum.
5. Tests pass: cargo test --workspace green; existing polymorphic fixtures (poly_id, poly_apply, poly_rec_capture) unchanged; new composition fixture (cmp_max_smoke) green; E2E fixtures from 23.5 green.
6. Bench regression ratified: bench/check.py && bench/compile_check.py && bench/cross_lang.py exit 0 or audit-ratified with journal entry.
7. Surface acceptance from original spec: a polymorphic helper forall a. Ord a => (a, a) -> Bool compiles, monomorphises at three primitive types, runs, and prints the expected output for at least Int and Str; the same helper on Float fires NoInstance Ord Float at typecheck with a Float-aware diagnostic.
8. Roadmap update: P1 Post-22 Prelude entry from [~] to [x] for Eq/Ord half; Show half stays as a separate entry.

Out of scope (deferred, with substantive rationale)

Unchanged from original spec:

• Show typeclass. Defers behind a heap-Str-ABI milestone. instance Show Int needs int_to_str to allocate a heap-Str — a runtime primitive AILang does not have today.
• Operator routing through Eq / Ord. ==, <, etc. stay primitive this milestone. Routing them through the class methods is the declared P2 todo, gated on bench rebaseline confirmation.
• print-rewire through Show.show. Same heap-Str dependency.
• Eq / Ord on Float. No instance per DESIGN.md §"Float semantics". A future iter exposing a partial compare : Float -> Float -> Maybe Ordering is a separate brainstorm.
• deriving (Eq, Ord) for user ADTs. No auto-derivation.
• Ord Ordering instance. Cute but no concrete demand.

New under B1 unification:

• Higher-rank polymorphism. Stays out of scope per DESIGN.md §"Polymorphism via Type::Forall" (line 2138-2140). The unified mono pass requires fully-concrete substitution at each call site; the same constraint as today, not weakened.
• Polymorphic constants (Type::Forall on ConstDef). The mono pass operates on Def::Fn; const_as_pseudo_fn (mono.rs line 261) is the only ConstDef bridge and stays unchanged.
• User-customisable mono-symbol naming. The naming format is implementation-finalised in 23.4; no user-facing knob.

Open commitments (23.4 / 23.5 implementer)

• Mono-symbol naming for N-ary type vars. Today's class-method naming <method>__<typesurfacename> is single-type-var. Polymorphic free fns can have N type vars (e.g. poly_apply : forall a b.). Default proposal: <name>__<typename1>__<typename2>__… in Forall-vars declaration order, hash-stable, covered by the canonical-type-names layer. Implementer may raise an alternative via NEEDS_CONTEXT.
• Target-collector heuristic. collect_mono_targets (mono.rs line 422) today filters on residual class-constraints. For polymorphic free fns, the collector must additionally detect "call site to polymorphic free-fn Def::Fn with fully-concrete substitution, regardless of constraints". Implementer decides between extending the existing synth-residual path or adding a separate walker; both shapes are structurally viable.
• Original Free-Fn Def::Fn retention post-mono. Def::Class / Def::Instance are kept in the workspace after mono (mono.rs line 40-42, for ail describe). Polymorphic Free-Fn Def::Fns should be kept analogously — both the source-Def and the synthesised mono-Defs visible.
• Float-NoInstance diagnostic wording. Implementer drafts a one-line Float-aware message; orchestrator reviews in spec-compliance phase.

Known costs

• 23.4 mono refactor: estimated +150 / −50 LOC in crates/ailang-check/src/mono.rs (target-collector extension, source-body entry points, naming helper).
• 23.4 codegen cleanup: estimated −200 LOC in crates/ailang-codegen/src/lib.rs (lower_polymorphic_call, module_polymorphic_fns fields, mono_queue machinery). Net code reduction expected.
• 23.5 prelude additions: examples/prelude.ail.json +30-40 lines (five free fns with Forall-constraint signatures and bodies). Three new E2E .ail.json fixtures, ~60 lines JSON. Diagnostic test ~20 lines Rust.
• Compile-time shift: mono pass does more work (additional body walks over free fns, potentially larger fixpoint convergence). Quantified by bench/compile_check.py post-23.4; audit-ratified or rebaselined.
• DESIGN.md amendments: §"Resolution and monomorphisation" (line 1513+) extends to cover polymorphic free fns; §"Decision 11 / Prelude classes" (line 1659+) reflects Eq/Ord shipping.

Load-bearing assumptions about current behaviour

Surfaced explicitly so the Step 7.5 grounding-check agent has a canonical list to ratify. Each assumption is something this spec relies on as currently-true.

1. crates/ailang-check/src/mono.rs::monomorphise_workspace today is the only typecheck-time specialiser, and it operates exclusively on class-method residuals (no free-fn handling).
2. crates/ailang-codegen/src/lib.rs::lower_polymorphic_call today is the only codegen-time specialiser, and it operates exclusively on polymorphic free-fn calls (no class-method handling).
3. The mono pass produces Def::Fn entries in the workspace; the codegen-time specialiser emits LLVM symbols without corresponding workspace Defs.
4. examples/prelude.ail.json today contains no free fns (only ADT, classes, instances).
5. prep2 and prep3 (the codegen bare-name fall-through patches) never reached main. They lived on the stranded iter/23.4 branch which was deleted on 2026-05-11. The current main contains no codegen bare-name fall-through for polymorphic free-fn calls — codegen rejects bare polymorphic free-fn calls today, which is exactly what makes the original iter-23.4 BLOCK.
6. Commits on main 0caaced (prep.1, linearity registers Def::Class method types in globals) and 923dd8c (prep.2, check bare-name fall-through to implicit-imported free fns) operate at typecheck / linearity time — before any mono pass — and are load-bearing for any prelude free-fn resolution regardless of mono architecture. (Originals from stranded branch: 8d39f13 and aef4ab8; cherry-picked onto main 2026-05-11.)
7. crates/ailang-codegen/src/lib.rs::lower_polymorphic_call is invoked from two call sites today (lines 1944, 1972), both of which become direct mono-symbol calls after 23.4.
8. examples/poly_id.ail.json and examples/poly_apply.ail.json today rely on the codegen-time specialiser path; under B1 they transition to the typecheck-time mono pass without surface behavioural change.
9. The mono pass's fixpoint loop (mono.rs line 88) iterates until a round adds nothing new, and already supports transitive specialisation across nested class-method calls; the same mechanism handles a free-fn body whose specialisation triggers a class-method specialisation.
10. The canonical-form layer (per docs/specs/0007-canonical-type-names.md, ct.4 closure) treats mono Defs as post-typecheck artefacts not in CheckedModule.symbols, so renaming or extending mono symbols does not affect surface-level hash pins.