Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

spec: operator-routing-eq-ord — drop comparator builtins, route through Eq/Ord

Browse Source 
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
This commit is contained in:
Brummel
2026-05-20 23:43:13 +02:00
parent 86dd7d7b60
commit a68d7b6353
1 changed files with 546 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/specs/2026-05-20-operator-routing-eq-ord.md
+546
View File
@@ -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 <UserType>`** — 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 <UserType>` 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.