From a68d7b635352207cf5f403d2cba47319ced205b3 Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 20 May 2026 23:43:13 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20operator-routing-eq-ord=20=E2=80=94=20d?= =?UTF-8?q?rop=20comparator=20builtins,=20route=20through=20Eq/Ord?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves Gitea #1. Realises the "P2 follow-up" called out in examples/prelude.ail line 9. Approach A (single-iter atomic milestone): one cohesive cut across seven layers in one iter, plus the regenerated prelude module hash pin. Three design forks resolved with the user via brainstorm Q&A: (1) Operator-name surface: `==` `!=` `<` `<=` `>` `>=` die from the language. The LLM-author writes only the class-method names `eq` `ne` `lt` `le` `gt` `ge` `compare`. One mental model: AILang has class-dispatch, operators are not a separate concept. Option 2 (keep names as surface aliases) was rejected because it adds a second spelling for an identical operation — the redundancy the milestone is supposed to remove gets reintroduced syntactically. Option 3 (two-track: primitive Built-in for Int/Bool/Str/Unit, class for user-types) was rejected because the two-pathy state is precisely what this milestone exists to dismantle. (2) Float comparison surface: Float keeps comparison capability via six named prelude fns (`float_eq` `float_ne` `float_lt` `float_le` `float_gt` `float_ge`), no `Eq Float` / `Ord Float` instance. Motivation: all three feature-acceptance clauses simultaneously satisfied — clause 1 (LLM-natural via Library-Convention-Pattern like Python's `math.isclose` or Rust's `approx`-crates), clause 2 (within the polymorphic surface there is one path; Float is honestly stamped "non-polymorphic"), clause 3 (the NaN-comparison anti-pattern stays visible in code as `float_eq` rather than hiding behind `eq`). Option A (Float loses all comparison) was rejected as overstretch — workarounds via `is_nan` + arithmetic are more bug-prone than a named fn that emits the right fcmp directly. Option C (Eq Float with IEEE semantics) was rejected as clause-3 violation — it would reintroduce the silent NaN-comparison bug class that the existing Float-no-Eq/Ord design exists to prevent. (3) Codegen mechanism for primitive Eq/Ord instances: option β (always-call through dispatch, with `alwaysinline` attribute on intercept-emitted bodies as pre-emptive `-O0` mitigation, and option α — call-site intercept — held as the bench-gate fallback if measurements show real regression). Motivation: semantic honesty (class methods ARE calls, optimiser folds primitives uniformly at Int and User-Point alike), parity with `Show` (which is also full-call today with no intercept), smaller IR-shape contract for the existing pins. Under `-O2` the inliner deterministically collapses 2- instruction bodies; bench corpus runs `-O2`. Under `-O0` `alwaysinline` overrides the no-inline default, giving the same per-call IR shape as today. α was the initial-framed Recommendation but was scrutinised in user pushback ("spricht irgendwas FÜR β?") and after substantive re-balancing β came out coherent. Grounding-check (ailang-grounding-check) PASS on re-dispatch — 11 load-bearing assumptions ratified by: `crates/ail/tests/e2e.rs::eq_demo` + `::lit_pat_demo`, `crates/ail/tests/eq_ord_e2e.rs::eq_ord_polymorphic_runs_end_to_end` + `::eq_ord_user_adt_runs_end_to_end` + `::eq_ord_user_adt_eq_intbox_hash_stable`, `crates/ail/tests/eq_float_noinstance.rs::eq_at_float_fires_float_aware_noinstance`, `crates/ail/tests/prelude_free_fns.rs::ne_at_int_produces_mono_symbol` (+4 siblings), `crates/ailang-surface/tests/prelude_module_hash_pin.rs::prelude_parse_yields_canonical_hash`, plus in-source `#[cfg(test)] mod tests` ratifiers in `crates/ailang-check/src/lib.rs` (`eq_typechecks_at_int/bool/str/unit`, `mq2_env_method_to_candidate_classes_built`) and `crates/ailang-codegen/src/lib.rs` (`lower_eq_str_calls_strcmp_with_bytes_pointer`). The `alwaysinline` LLVM attribute is correctly classified as new feature-work commitment (no live occurrences today), not as a load-bearing assumption about present state. First grounding-check pass BLOCKED on one spec defect — the spec mischaracterised `crates/ailang-core/src/desugar.rs:2414` as "a separate desugar pass" when it is in fact a `#[cfg(test)] mod tests` AST-literal scaffold. Fixed inline: §Architecture and §Components/4 now enumerate only `build_eq` (desugar.rs:1099) as the sole production desugar site; `desugar.rs:2414`, `lib.rs:6092`, `lib.rs:6220` are framed as test-scaffold migrations alongside the production change, not as desugar-pass work. Re-dispatch PASS. Out of scope (tracked separately): - Deriving for Eq/Ord — `typeclasses.md:177` "No deriving" stands; instance bodies remain hand-written. - Parameterised-ADT instances (`instance Eq (List a)` etc.) — requires constraint-propagation infrastructure, belongs to Gitea #2 ("22c typeclass corpus expansion"). - Eq/Ord for the `Ordering` ADT itself — no use case; consumed via match, not compared. - `and` / `or` as Builtins — north-star fixture uses `(if … … false)` for short-circuit conjunction; separate concern. refs #1 --- .../2026-05-20-operator-routing-eq-ord.md | 546 ++++++++++++++++++ 1 file changed, 546 insertions(+) create mode 100644 docs/specs/2026-05-20-operator-routing-eq-ord.md diff --git a/docs/specs/2026-05-20-operator-routing-eq-ord.md b/docs/specs/2026-05-20-operator-routing-eq-ord.md new file mode 100644 index 0000000..523f36a --- /dev/null +++ b/docs/specs/2026-05-20-operator-routing-eq-ord.md @@ -0,0 +1,546 @@ +# Operator routing through Eq / Ord — Design Spec + +**Date:** 2026-05-20 +**Status:** Draft — awaiting user spec review +**Authors:** Brummel (orchestrator) + Claude + +Resolves Gitea #1. Realises the "P2 follow-up" called out in +`examples/prelude.ail:9` — routing the surface comparator names +through the `prelude.Eq` / `prelude.Ord` classes instead of the +hard-coded built-in comparator table. + +## Goal + +Today AILang has two parallel paths for comparison: + +- **Built-in operators** `==`, `!=`, `<`, `<=`, `>`, `>=` — special- + cased in codegen with hardcoded polymorphism over fixed primitive + type sets (`==` over `{Int, Bool, Str, Unit, Float}`; the other + five over `{Int, Float}`). User ADTs are rejected at codegen with + a generic error. +- **Typeclass methods** `prelude.Eq.eq` and `prelude.Ord.compare` + with instances for `{Int, Bool, Str}`, plus the polymorphic free- + fn helpers `ne`/`lt`/`le`/`gt`/`ge`. Float and Unit have no Eq/Ord + instance by design (Float: partial orderability per + [float-semantics](../../design/contracts/float-semantics.md); + Unit: oversight that today's `(app == () ())` builtin path hides). + +The two paths are redundant — `instance Eq Int` body literally +calls `(app == x y)`, so the class layer today delegates back to +the builtin. The redundancy is structurally observable: every +release pays the cost of maintaining both. User ADTs cannot +participate in `==` at all, even when the LLM-author has written +`instance Eq Point` — the operator is sealed at the primitive +types. + +After this milestone, the LLM-author writes `(app eq p1 p2)` for +user types and gets the natural typeclass-dispatched behaviour; +`==`/`!=`/`<`/`<=`/`>`/`>=` as identifiers are gone from the +language; Float comparison is named explicitly via `float_eq` / +`float_lt` / etc. (no IEEE-NaN-bug-class smuggled in via a +polymorphic `eq`). + +## Architecture + +Three layers shift in lockstep: + +**Surface / parser:** unchanged. The Form-A tokens `==` / `!=` / `<` +/ `<=` / `>` / `>=` remain legal identifier strings at the parser +level — there is no syntactic change. They are simply not +recognised at typecheck or codegen. + +**Typechecker:** the entries for `==` / `!=` / `<` / `<=` / `>` / +`>=` in the builtin signature table +(`crates/ailang-check/src/builtins.rs::install` — comparator loop +at lines 96-98, polymorphic `==` Forall block at lines 109-125, +list-side mirror at lines 303-308) are removed. Surface use of these +names resolves like any other unknown identifier — first via the +class-method-dispatch index per +[method-dispatch](../../design/contracts/method-dispatch.md), which +finds no candidate (the method name is `eq`, not `==`), then via +fn lookup, which also finds none, then fails with the standard +`unknown variable` diagnostic. The diagnostic does NOT special-case +the comparator names with a "did you mean `eq`?" hint — the +milestone is a clean break, not a transition aid; AILang has no +external users requiring migration. + +All `(app eq …)` / `(app compare …)` / `(app ne …)` / `(app lt …)` +/ etc. resolve through the existing class-method-dispatch machinery +documented in +[method-dispatch](../../design/contracts/method-dispatch.md). +No new dispatch rule. + +**Codegen:** `try_emit_primitive_instance_body` in +`crates/ailang-codegen/src/lib.rs` (the intercept already used for +`eq__Str`, `compare__Int`, `compare__Bool`, `compare__Str`) +gains three new arms — `eq__Int`, `eq__Bool`, `eq__Unit`. Every +primitive instance body emitted via this intercept carries an +`alwaysinline` attribute on the generated LLVM function so the +`-O0` build path collapses the trivial body to its single +`icmp`/`fcmp`/`call` instruction at every use site, matching +today's direct-emit IR shape under `-O0` as well as `-O2`. + +Six new prelude free functions ship for Float comparison: +`float_eq`, `float_ne`, `float_lt`, `float_le`, `float_gt`, +`float_ge`, each `Float -> Float -> Bool` without a class +constraint. Their bodies are intercept-lowered to the corresponding +`fcmp` instruction (`oeq` / `une` / `olt` / `ole` / `ogt` / `oge`), +preserving the bit-exact IEEE semantics +[float-semantics](../../design/contracts/float-semantics.md) +guarantees today for `==` / `<` etc. on Float — the guarantee is +transferred from the deleted operator names to the named Float +fns. + +The lit-pattern desugar in +`crates/ailang-core/src/desugar.rs::build_eq` (line 1099) rewrites +`(pat-lit "hi")` to `(if (eq sv "hi") body fall_k)` instead of the +current `(if (== sv "hi") body fall_k)` — the literal symbol +`Term::Var { name: "==" }` at line 1109 becomes `name: "eq"`. +This is the single live `==`-emitting desugar site; everything +else mechanically migrates as fixture or test-scaffold work, not +as desugar-pass changes. This is the non-obvious mechanical +follow: lit patterns inherit equality dispatch by construction. + +## Concrete code shapes + +### The LLM-author program this milestone enables + +``` +(module eq_user_adt_smoke + (data Point + (ctor Point (con Int) (con Int))) + (instance + (class Eq) + (type (con Point)) + (method eq + (body (lam (params (typed p1 (con Point)) (typed p2 (con Point))) (ret (con Bool)) + (body (match p1 + (case (pat-ctor Point a1 b1) + (match p2 + (case (pat-ctor Point a2 b2) + (if (app eq a1 a2) + (app eq b1 b2) + false)))))))))) + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let p1 (term-ctor Point 1 2) + (let p2 (term-ctor Point 1 2) + (let p3 (term-ctor Point 1 3) + (seq (app print (app eq p1 p2)) + (app print (app eq p1 p3))))))))) +``` + +Expected stdout: `true\nfalse\n`. This is the feature-acceptance +clause-1 evidence: the LLM-natural form that is **structurally +impossible to write today**. Today `(app == p1 p2)` is rejected at +codegen (Point is not in the polymorphic `==` type set); +`(app eq p1 p2)` fires `NoInstance Eq Point` even after the author +writes the instance, because the body's nested `(app eq a1 a2)` on +Int delegates to `(app == x y)` which then has to thread back via +the polymorphic-`==` mechanism — the chain works but the author +gets the same outcome as writing `==` directly, no gain. + +After this milestone, both the outer `(app eq p1 p2)` and the +nested `(app eq a1 a2)` resolve via the canonical class-dispatch +path: the outer to `eq_user_adt_smoke.eq__Point` (the user +instance), the nested to `prelude.eq__Int` (the primitive +instance, intercept-lowered to `icmp eq i64` and inlined back to +the call site). + +### The Klausel-3 discriminator (must fail at typecheck) + +``` +(module eq_float_must_fail + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body (app print (app eq 1.5 1.5))))) +``` + +Must produce a typecheck-time diagnostic — `NoInstance Eq Float` +with a follow-up sentence `Float has no Eq instance by design +(partial orderability per design/contracts/float-semantics.md); use +float_eq for explicit IEEE-aware comparison`. The diagnostic is the +existing `NoInstance` channel; the Float-aware addendum is the +existing Float-specific hint in `crates/ailang-check/src/lib.rs` +around line 860 (which already special-cases Eq/Ord-at-Float +diagnostics), extended to name `float_eq` / `float_lt` as the +explicit alternative. + +### The Float-with-named-fn happy path + +``` +(module float_compare_smoke + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (seq (app print (app float_eq 1.5 1.5)) + (seq (app print (app float_lt 1.0 2.0)) + (app print (app float_eq 1.0 0.0))))))) +``` + +Expected stdout: `true\ntrue\nfalse\n`. Demonstrates that Float +comparison remains available via the named-fn route. The +implementation lowers each `float_*` call to a single `fcmp` +instruction via the intercept mechanism — IR-byte-equivalent to +today's `(app == 1.5 1.5)` after the operator name is removed. + +### Migration pattern for existing fixtures + +``` +; examples/eq_demo.ail (current) +(seq (app print (app == 5 5)) +(seq (app print (app == true false)) + (app print (app == "hi" "hi")))) + +; examples/eq_demo.ail (after this milestone) +(seq (app print (app eq 5 5)) +(seq (app print (app eq true false)) + (app print (app eq "hi" "hi")))) +``` + +≈10 fixtures under `examples/` use one or more of the deleted +operator names. Each migrates to the corresponding class-method +or named-fn (Float case): `==` → `eq`, `!=` → `ne`, `<` → `lt`, +`<=` → `le`, `>` → `gt`, `>=` → `ge`. The Float-operator uses in +`bench_compute_collatz.ail` (and any other Float-touching bench +fixture) migrate to `float_lt` / `float_eq` / etc. The exact +fixture list is enumerated by the planner via +`grep -rln '(app == \|(app != \|(app < \|(app <= \|(app > \|(app >=' examples/`. + +### Implementation shape (secondary — supporting detail) + +The load-bearing code changes (planner derives exact paths/line +numbers; this section establishes shape): + +`crates/ailang-codegen/src/synth.rs::builtin_binop_typed` — the +comparator arms vanish: + +```rust +// Before — 10 arms for ==/!=//>= over Int+Float +match (name, is_int, is_float) { + ("+", true, _) => Some(("add", "i64", "i64")), + ("+", _, true) => Some(("fadd", "double", "double")), + // ... arithmetic ... + ("!=", true, _) => Some(("icmp ne", "i64", "i1")), + ("<", true, _) => Some(("icmp slt", "i64", "i1")), + ("<=", true, _) => Some(("icmp sle", "i64", "i1")), + (">", true, _) => Some(("icmp sgt", "i64", "i1")), + (">=", true, _) => Some(("icmp sge", "i64", "i1")), + ("!=", _, true) => Some(("fcmp une", "double", "i1")), + ("<", _, true) => Some(("fcmp olt", "double", "i1")), + ("<=", _, true) => Some(("fcmp ole", "double", "i1")), + (">", _, true) => Some(("fcmp ogt", "double", "i1")), + (">=", _, true) => Some(("fcmp oge", "double", "i1")), + _ => None, +} + +// After — arithmetic only +match (name, is_int, is_float) { + ("+", true, _) => Some(("add", "i64", "i64")), + ("+", _, true) => Some(("fadd", "double", "double")), + ("-", true, _) => Some(("sub", "i64", "i64")), + ("-", _, true) => Some(("fsub", "double", "double")), + ("*", true, _) => Some(("mul", "i64", "i64")), + ("*", _, true) => Some(("fmul", "double", "double")), + ("/", true, _) => Some(("sdiv", "i64", "i64")), + ("/", _, true) => Some(("fdiv", "double", "double")), + ("%", true, _) => Some(("srem", "i64", "i64")), + _ => None, +} +``` + +`crates/ailang-codegen/src/lib.rs` — the `==`-polymorphic-dispatch +special case (lib.rs around 2947 plus the Int/Bool/Str/Unit +matching) is gone; replaced by `try_emit_primitive_instance_body` +arms for the new symbol set: + +```rust +// New arms in try_emit_primitive_instance_body's match +match instance_key { + "eq__Int" => emit_icmp_eq("i64"), // new + "eq__Bool" => emit_icmp_eq("i1"), // new + "eq__Unit" => emit_const_i1_true(), // new + "eq__Str" => /* existing — @ail_str_eq */, + "compare__Int" | "compare__Bool" | "compare__Str" => /* existing */, + // 6 new Float-named-fn arms + "float_eq" => emit_fcmp("oeq", "double"), + "float_ne" => emit_fcmp("une", "double"), + "float_lt" => emit_fcmp("olt", "double"), + "float_le" => emit_fcmp("ole", "double"), + "float_gt" => emit_fcmp("ogt", "double"), + "float_ge" => emit_fcmp("oge", "double"), + _ => return None, +} +``` + +Each emit_* helper adds `attributes #N = { alwaysinline … }` to +the generated function header so the `-O0` build path inlines the +single-instruction body at every call site, matching today's +direct-emit shape. + +`examples/prelude.ail` — three additions, three rewrites: + +``` +; New: Eq Unit instance (preserves today's `==`-on-Unit capability). +(instance + (class Eq) + (type (con Unit)) + (doc "Eq Unit. Body is constant true — Unit is single-inhabitant + so all values compare equal. Lowered via + try_emit_primitive_instance_body::eq__Unit to `ret i1 1`.") + (method eq + (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) + (body true))))) + +; Eq Int — body becomes a placeholder (lambda returning false); +; codegen intercept overrides to icmp eq i64. Matches Ord Int's +; existing placeholder pattern. +(instance + (class Eq) + (type (con Int)) + (doc "Eq Int. Body is placeholder for round-trip stability; + codegen intercept emits `icmp eq i64` with alwaysinline.") + (method eq + (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) + (body false))))) + +; Eq Bool — same placeholder shape. +; Eq Str — body unchanged in shape (already placeholder-style), +; intercept already exists. + +; New Float-fns: six entries. +(fn float_eq + (doc "IEEE-aware Float equality. `float_eq x y` returns true iff + both operands are non-NaN and bit-equal. Lowered to + `fcmp oeq double`. Replaces the milestone-deleted `(app == x y)` + on Float.") + (type (fn-type (params (con Float) (con Float)) (ret (con Bool)))) + (params x y) + (body (lam (params (typed x (con Float)) (typed y (con Float))) (ret (con Bool)) + (body false)))) +; ... float_ne / float_lt / float_le / float_gt / float_ge analogous. + +; Line-9 comment on `class Eq` (the "P2 follow-up" note) is removed — +; routing-through-Eq.eq is no longer follow-up, it's the present. +``` + +## Components + +The milestone touches seven layers, all in one cohesive iter: + +1. **Typechecker builtin table** (`crates/ailang-check/src/builtins.rs`) + — six operator-name entries removed (`install` lines 96-98 + + 109-125); list-side mirror at lines 303-308 trimmed; the in- + source `mod tests` helpers `eq_app` and the polymorphic-`==` + regression tests (lib.rs:6092, lib.rs:6220 — both inside + `#[cfg(test)]`) migrate to the `eq` symbol so the test suite + stays green over the new dispatch path. +2. **Codegen builtin binop table** (`crates/ailang-codegen/src/synth.rs`) + — ten comparator arms removed from `builtin_binop_typed`; the + table reduces to the arithmetic core. +3. **Codegen primitive-instance intercept** + (`crates/ailang-codegen/src/lib.rs`) — `try_emit_primitive_instance_body` + gains three Eq arms (`eq__Int`, `eq__Bool`, `eq__Unit`) and six + Float-fn arms (`float_eq`/`float_ne`/`float_lt`/`float_le`/`float_gt`/ + `float_ge`); each generated function header carries `alwaysinline`. + The existing `==`-polymorphic-dispatch lowering (lib.rs around + 2947, the Int/Bool/Str/Unit/Float matching for `==`) is deleted. +4. **Lit-pattern desugar** (`crates/ailang-core/src/desugar.rs`) + — `build_eq` (line 1099) substitutes `eq` for `==` in the + generated `(if … body fall_k)` form. This is the only live + desugar-pass change. Float-pattern rejection per + `float-semantics.md` is unaffected (still hard-rejected at + typecheck, before desugar runs). + + *In-source test scaffolds* in the same file + (`desugar.rs:2414`, inside `#[cfg(test)] mod tests`) and in + `crates/ailang-check/src/lib.rs` (lines 6092 and 6220, also + `#[cfg(test)]`) construct hand-built `Term::Var { name: "==" }` + in AST literals to drive `==`-specific assertions; these + migrate to `name: "eq"` alongside the production change. + Counted as test-scaffold migration, not desugar-pass work. +5. **Prelude module** (`examples/prelude.ail`) — adds `instance Eq Unit`; + rewrites `Eq Int` / `Eq Bool` bodies to placeholder pattern + (codegen intercept does the work); adds six `float_*` free fns; + removes the "P2 follow-up" comment on `class Eq`. Prelude module + hash will shift; the hash pin in + `crates/ailang-surface/tests/prelude_module_hash_pin.rs` + regenerates as part of the iter. +6. **Fixture migration** — ≈10 files under `examples/` rewritten + from operator-form to method-form. The planner enumerates the + exact set via grep and assigns it as a discrete task. +7. **Contracts** — three updates: + - `design/contracts/float-semantics.md` lines 10-14: the + guarantees about `+`/`-`/etc. and `==`/`<`/`!=` lowering to + single LLVM instructions are retained for arithmetic but + transferred from `==`/`<`/`!=` to `float_eq`/`float_lt`/`float_ne`/etc. + for the comparison set. The NaN-spelling caveat is unchanged. + - `design/contracts/prelude-classes.md`: instance list extends + with `Eq Unit`; a new paragraph documents the six `float_*` fns + as the Float-comparison surface; the Float-no-Eq/Ord clause + gains a `→ use float_eq` cross-reference. + - `design/contracts/typeclasses.md`: no change. Class schema, + dispatch rule, and diagnostics are stable; the milestone only + activates existing machinery for `eq`/`compare` over more + types. + +## Data flow + +A surface `(app eq p1 p2)` flows through the existing pipeline: + +1. **Parse** — `Term::App { fn: Var "eq", args: [p1, p2] }`. No + change from today. +2. **Typecheck** — class-method-dispatch (per + `design/contracts/method-dispatch.md`) consults + `method_to_candidate_classes["eq"]` → `{prelude.Eq}`. Singleton + class survivor; type-driven filter against the workspace + registry for the resolved type: + - `p1, p2 : Int` → `prelude.eq__Int` + - `p1, p2 : Point` → `eq_user_adt_smoke.eq__Point` + - `p1, p2 : Float` → no instance → `NoInstance Eq Float` with + Float-aware hint pointing at `float_eq`. +3. **Mono** — synth produces the instance-body symbol (existing + pass; per `design/contracts/typeclasses.md` invariants 1-3). +4. **Codegen** — emits a call to the resolved instance fn. For + primitive instances, the body is intercept-lowered to a single + icmp/fcmp/call; `alwaysinline` attribute ensures the call folds + at every use site under `-O0` as well as `-O2`. For user-ADT + instances, codegen emits the full lambda body normally; the + call to the instance fn is normal (no intercept). + +The data-flow is conceptually identical to today's `show` / +`compare` paths — the milestone unifies `eq` into the same shape. + +## Error handling + +Three diagnostic situations: + +**`NoInstance Eq Float` / `NoInstance Ord Float`** — fires at +typecheck for any `(app eq …)` or `(app compare …)` (or +`ne`/`lt`/`le`/`gt`/`ge`) on Float. The existing Float-aware +addendum (lib.rs:860-873) is extended: + +``` +Eq has no instance at Float — Float has no Eq/Ord instance by +design (partial orderability per design/contracts/float-semantics.md); +use float_eq for explicit IEEE-aware comparison. +``` + +`compare`/`Ord` use case names `float_lt` / `float_compare` (the +latter doesn't ship as a fn — `compare` returns `Ordering`, no +Float equivalent — so the hint says "use float_lt / float_eq for +explicit IEEE-aware comparison"). + +**`NoInstance Eq `** — fires when the LLM-author calls +`(app eq p1 p2)` on a user type without having written the +instance. Standard `NoInstance` channel; no special-case wording. +The author writes `instance Eq ` by hand (no deriving). + +**`unknown variable: ==` (et al.)** — fires when the LLM-author +writes `(app == 5 5)` after the milestone. The diagnostic does +NOT carry a "did you mean `eq`?" hint. This is a clean break, not +a transition; AILang has no external users to migrate. The lack of +hint is documented in the `prelude-classes.md` contract update +("comparator-operator names are not part of the language"). + +## Testing strategy + +Five test artefacts, all in `crates/ail/tests/`: + +1. **`eq_user_adt_smoke_e2e.rs`** — drives the north-star fixture + `examples/eq_user_adt_smoke.ail` through `ail build` + binary + execution; asserts stdout `"true\nfalse\n"`. This is the + milestone-defining E2E. Protects: user-ADT-Eq path works end-to- + end, including cross-module reference from user-instance body + to `prelude.eq__Int`. +2. **`eq_float_must_fail_pin.rs`** — drives the must-fail fixture + `examples/eq_float_must_fail.ail`; asserts `ail check` exits + non-zero with stderr containing `NoInstance Eq Float` AND + `float_eq`. Protects: the Klausel-3 discriminator stays + discriminative; Float-aware diagnostic stays informative. +3. **`float_compare_smoke_e2e.rs`** — drives the Float-named-fn + fixture; asserts stdout `"true\ntrue\nfalse\n"`. Protects: the + six `float_*` fns lower correctly to fcmp; replacement surface + for the deleted Float operators stays functional. +4. **`operator_names_unbound_pin.rs`** — drives a minimal fixture + `(app == 5 5)`; asserts `ail check` exits non-zero with stderr + containing `unknown variable: ==`. Protects: the operator-name + removal is durable; no codegen path silently re-introduces + them. +5. **`prelude_eq_alwaysinline_ir_pin.rs`** — compiles + `(app eq 5 5)` with `--emit-ir --opt=O0`; asserts the resulting + IR contains either `icmp eq i64` directly at the call site OR + the `alwaysinline` attribute on `@prelude_eq__Int` such that the + inliner is guaranteed to fold under `-O2`. Protects: the + `alwaysinline` mitigation is wired (not silently dropped); the + bench-gate risk is structurally bounded. + +Plus: the bench corpus (latency + throughput + cross-lang) runs as +the acceptance gate. The expectation is 0/0/0 regressions; if +regressions appear, the `alwaysinline`-mitigation needs +investigation (likely codegen-bug) or the spec needs revisiting +toward α (call-site intercept). + +Existing tests stay green by virtue of the fixture migration — +every `==`/`<`/etc. in test fixtures is rewritten alongside the +language change. The lit-pattern regression suite +(if exists in `crates/ailang-check/tests/` per planner-recon) +exercises `(case (pat-lit "hi") …)` paths after the desugar +rewrites to `eq`; these stay green provided the desugar is updated +correctly. + +## Acceptance criteria + +The milestone ships when all of the following hold: + +1. `cargo test --workspace --quiet` — all binaries `0 failed`. +2. `examples/eq_user_adt_smoke.ail` exists and builds and runs and + prints `"true\nfalse\n"`; the corresponding E2E is green. +3. `examples/eq_float_must_fail.ail` exists and `ail check` rejects + it with `NoInstance Eq Float` and a `float_eq` hint. +4. `examples/float_compare_smoke.ail` exists and runs and prints + `"true\ntrue\nfalse\n"`. +5. `grep -rn '"=="\|"<"\|"<="\|">"\|">="\|"!="' crates/ailang-check/src/builtins.rs crates/ailang-codegen/src/synth.rs crates/ailang-codegen/src/lib.rs crates/ailang-core/src/desugar.rs` + returns matches only in comment / doc context, not as live + `env.globals.insert(...)`, `Type::Var { name: "==" }`, or + `Some((..., "...))` table entries. + Documentation comments referring historically to the removed + names are permitted only in commit-bodies and contract-history + sections, not as live code paths. +6. `grep -rln '(app == \|(app != \|(app < \|(app <= \|(app > \|(app >=' examples/` + returns zero matches (full fixture migration complete). +7. `examples/prelude.ail` contains `instance Eq Unit` and the six + `float_*` fns; the line-9 "P2 follow-up" comment on `class Eq` + is removed. +8. `bench/check.py` exit 0; `bench/compile_check.py` exit 0; + `bench/cross_lang.py` exit 0 (full bench-corpus green against + the post-milestone baseline regenerated by the iter). +9. `design/contracts/float-semantics.md` updated to name `float_eq` + / `float_lt` / `float_ne` / etc. as the comparison guarantees + (comparison guarantees on `==`/`<`/`!=` removed; arithmetic + guarantees on `+`/`-`/`*`/`/` unchanged). +10. `design/contracts/prelude-classes.md` updated: `Eq Unit` in the + instance list; new section on the six Float-named comparison + fns; the Float-no-Eq/Ord clause carries a `→ use float_eq` + cross-reference. +11. Closes Gitea #1 via the iter-commit `closes #1` trailer. + +Out of scope (tracked separately): + +- **Deriving for Eq/Ord** — `typeclasses.md:177` "No deriving" + stands. LLM-author writes instance bodies by hand. If deriving + becomes a real friction point post-milestone, that is its own + spec (likely tied to Gitea #2 "22c typeclass corpus expansion"). +- **Parameterised-ADT instances** (`instance Eq (List a)`, etc.) + — requires multi-parameter-class / constraint-propagation + infrastructure, part of Gitea #2. +- **`Eq` / `Ord` for the `Ordering` ADT itself** — no use case; + `Ordering` is consumed via `match`, not compared. +- **`and` / `or` as Builtins** — north-star fixture uses + `(if … … false)` for short-circuit conjunction. Adding `and` / + `or` as separate fns or operators is a separate concern; no + forcing here.