iter operator-routing-eq-ord.1 (DONE 13/13): drop comparator builtins, route through Eq/Ord

Closes Gitea #1. Realises the "P2 follow-up" called out in
examples/prelude.ail:9 — removes the surface comparator names
`==` / `!=` / `<` / `<=` / `>` / `>=` from the language entirely,
routes the LLM-author's `(app eq …)` / `(app compare …)` /
`(app ne|lt|le|gt|ge …)` through prelude.Eq / prelude.Ord class-
dispatch, ships six named Float-comparison fns
(`float_eq`/`float_ne`/`float_lt`/`float_le`/`float_gt`/`float_ge`)
so Float keeps comparability without an Eq/Ord instance, and emits
primitive instance bodies with `alwaysinline` so the -O0 IR shape
stays at one instruction per comparison.

Plan-task journal (13 tasks, single atomic iter per Approach A):

  Task 1 — Bootstrap: 4 new fixtures (eq_user_adt_smoke.ail,
    eq_float_must_fail.ail, float_compare_smoke.ail,
    operator_unbound_check.ail) + 5 new E2E/pin tests as RED
    starting state. All 5 confirmed RED at start: north-star
    fixed `NoInstance Eq Unit` (preserved by Unit-eq opening line
    intentionally added in plan-self-review); float_compare unknown
    `float_eq`; operator-name typechecked (== still polymorphic);
    must-fail diagnostic lacked `float_eq`; alwaysinline absent
    from IR.

  Task 2 — Codegen alwaysinline + intercept arms: introduced
    `intercept_emit_wants_alwaysinline` allowlist + appended
    ` alwaysinline` between `)` and `{` of the `define` line in
    `emit_fn`; added 9 new intercept arms to
    `try_emit_primitive_instance_body` — `eq__Int`/`eq__Bool`/
    `eq__Unit` + the six `float_*` arms.

  Task 3 — Prelude reshape: `instance Eq Unit` added; Eq Int/Bool
    bodies become placeholder-`false` (intercept overrides); six
    `float_*` free fns added; line-9 P2-follow-up comment removed.
    Lockstep hash re-pins: prelude_module_hash_pin (3abe0d3fa3c11c99
    → new), mono_hash_stability six body-hash literals
    (eq__Int/Bool/Str + compare__Int/Bool/Str all shifted because
    placeholder body changes the canonical hash). IR-snapshot
    regen (hello/list/max3/sum/ws_main) rolled forward into this
    task at orchestrator's pragmatic call — prelude shift forces
    the snapshots immediately.

  Task 4 — Fixture migration: 58 .ail fixtures rewritten
    (`(app == …)` → `(app eq …)`, etc.; Float-typed operand sites
    to `(app float_eq …)` / `(app float_lt …)`). eq_ord_user_adt.ail:21
    inner `==` → `eq` migration with lockstep eq_ord_e2e.rs:134
    body-hash re-pin (3c4cf040cb4e8bb2 → new). Two prose snapshots
    accepted; deps test + 5 hash_pin literals updated as cascading
    consequences.

  Task 5 — Test-scaffold migration: all 8 in-source
    `#[cfg(test)] mod tests` AST-literal sites threaded
    (desugar.rs:2414, check/lib.rs:5656/6092/6220, codegen/lib.rs
    sites). 7 obsolete in-source tests deleted (5 eq_typechecks +
    2 lower_eq ADT/Fn rejection — coverage moves to E2E
    eq_user_adt_smoke + eq_float_must_fail). 2 additional letrec
    tests deleted (single-module check env can't resolve eq/ge
    without prelude auto-import; covered by workspace E2E).

  Task 6 — Lit-pattern desugar: build_eq emits
    `Term::Var { name: "eq" }` instead of `"=="` at desugar.rs:1109;
    doc-comment rewritten to describe class-dispatch.

  Task 7 — Dead-machinery deletion sweep (compile-gated): typchecker
    builtins (install + list comparator entries deleted); codegen
    builtin_binop_typed (10 comparator arms deleted from synth.rs,
    table reduced to arithmetic core); lower_eq fn entirely
    deleted; `==` short-circuit in lower_app deleted;
    `is_static_callee` `==` clause deleted;
    `is_arithmetic_or_comparison_op` renamed to `is_arithmetic_op`
    + caller-update at codegen/lib.rs:2152 + :2529. Dead
    `poly_a_a_to_bool` helpers also removed. Workspace build green
    after compile gate — every caller of the deleted surface was
    migrated by Tasks 4-6.

  Task 8 — Float-aware NoInstance diagnostic: check/lib.rs:856-880
    addendum extended to name `float_eq` / `float_lt` as the
    explicit alternative for Eq/Ord at Float;
    eq_float_noinstance.rs:32-44 assertion extended.

  Task 9 — IR snapshot regen: subsumed by Task 3 (prelude shift
    forced immediate snapshot regen; deferring to Task 9 would
    have left the workspace red between tasks).

  Task 10 — Prose-projection cleanup: 6 comparator arms deleted
    from binop_info; 3 in-source mod-tests updated/deleted
    (comparator-infix rendering would be dishonest now that the
    operators are no longer language identifiers).

  Task 11 — Contract updates: 5 design files rewritten to the
    class-dispatch present —
      float-semantics.md (arithmetic guarantees retained on
        +/-/*/; comparison guarantees transferred from ==/!=/<
        to float_eq/float_ne/float_lt/etc.);
      prelude-classes.md (Eq Unit added to instance list;
        new paragraph on six float_* fns; Float-no-Eq/Ord clause
        gains `→ use float_eq` cross-reference);
      str-abi.md (clause "REMAIN primitive operators" rewritten
        to describe class-method dispatch);
      scope-boundaries.md (multiple operator-name and
        Pattern::Lit-desugar clauses rewritten);
      authoring-surface.md (==, <= dropped from operator-example
        list).

  Task 12 — Initial acceptance gate: workspace 638/0 GREEN;
    bench/compile_check + cross_lang 0 regressed; bench/check.py
    flagged 4 regressions on bench_closure_chain (+29% bump_s,
    +47% rc_s, +29% bump_rss_kb, +48% rc_rss_kb). Orchestrator
    initially classified as DONE-with-concerns; Boss reclassified
    as PARTIAL-via-acceptance-#8-fail after independent re-run,
    extended iter scope to Task 13.

  Task 13 — Direct icmp intercept arms (Boss-extension):
    try_emit_primitive_instance_body gains direct-icmp arms for
    lt__Int / le__Int / gt__Int / ge__Int / ne__Int, bypassing
    the compare__Int → Ordering → match indirection that allocated
    one Ordering ctor per call in tight loops. Each new arm
    inherits `alwaysinline` via the existing allowlist (extended
    accordingly). New IR pin test `ord_int_intercept_ir_pin.rs`
    + smoke fixture `ord_int_intercept_smoke.ail` ratify the
    optimization — opt -O2 -S confirms zero `call
    @ail_prelude_lt__Int` in optimized IR; the icmp folds directly
    at every use site. Bool variants (lt__Bool/etc.) deliberately
    NOT added — no bench/example calls Ord at Bool; spec-extension
    permits skipping if unreachable at bench level. Family can be
    extended symmetrically when first Bool-ordered perf workload
    appears.

Bench-gate post-Task-13: bench_closure_chain bump_s -6.05%,
rc_s -2.67%, bump_rss_kb -0.77%, rc_rss_kb +0.46% — all four
previously-regressed metrics back inside tolerance. Full bench
corpus: 36 metrics, 0 regressed, 0 improved beyond tolerance,
36 stable. bench/check.py exit 0 ✓; bench/compile_check.py exit
0 ✓; bench/cross_lang.py exit 0 ✓.

Workspace: 640 passed, 0 failed across all binaries (delta vs.
milestone start: +5 new E2E/pin tests added in Task 1 + 1 IR pin
added in Task 13 − 9 in-source mod tests deleted as obsolete net
≈ −3). The eq_user_adt_smoke fixture's Unit-opening line was
the deliberate RED-first device added in planner self-review so
the north-star wouldn't accidentally GREEN at start (user-ADT-Eq
on Point with hand-written instance was already operable today;
the milestone's actual delivery is operator-name death + Eq Unit
+ Float-named-fns + cleanup of the two-pathy primitive
comparator machinery).

Net delta: 96 files changed, 1760 insertions, 1101 deletions;
12 net-new files (6 new fixtures, 5 new E2E/pin tests, 1 stats
file). main passes-test-count: 640 (was 633 pre-iter, accounting
for the deletions).

Spec-vs-acceptance addendum: spec §Testing strategy anticipated
the bench-gate-regression case with two recovery paths
(`alwaysinline` investigation or "spec needs revisiting toward α").
Task 13 is the third path — direct intercept arms for `lt`/etc.
that bypass the compare→match path entirely. The spec's contingency
clause was thus generous enough to absorb Task 13 without spec
revision, but a future iter that hits a class-method primitive
where the body shape introduces a similar codegen cost (Ordering
allocation, RC tax, deferred-init) should expect a parallel
extension. The pattern is "primitive instance whose canonical body
indirects through other class methods that allocate" → add a
direct-emit intercept arm + alwaysinline + IR-shape pin.

Concerns absorbed:
  - Codegen lower_app / resolve_top_level_fn gained a
    prelude-fallback lookup so bare monomorphic prelude fns
    (`float_eq` etc.) resolve from non-prelude modules without
    explicit `prelude.float_eq` qualifier. Mirrors the
    typechecker's implicit prelude import — not in plan but
    necessary infra for the named-fn surface to be callable.
  - Recon's "≈10 fixtures" estimate was 6× too low — 58 actual.
    Mechanical migration; no design impact.
  - Recon caught 4 in-source AST-literal sites the spec missed
    (lib.rs:5656 `>=` site + three codegen/lib.rs sites);
    Task 5 covered all.
  - Recon caught 2 contract files outside the spec's update set
    that directly contradicted the milestone (str-abi.md +
    scope-boundaries.md "REMAIN primitive operators" /
    "Pattern::Lit desugar to ==" clauses); Task 11 covered all 5.

Stats file:
`bench/orchestrator-stats/2026-05-21-iter-operator-routing-eq-ord.1.json`.

closes #1

bench/orchestrator-stats/2026-05-21-iter-operator-routing-eq-ord.1.json

@@ -0,0 +1,28 @@
+{
+  "iter_id": "operator-routing-eq-ord.1",
+  "date": "2026-05-21",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 13,
+  "tasks_completed": 13,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 0,
+    "5": 1,
+    "6": 0,
+    "7": 0,
+    "8": 0,
+    "9": 0,
+    "10": 0,
+    "11": 0,
+    "12": 1,
+    "13": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "bench_gate": "0 regressed (36 metrics stable)",
+  "notes": "Task 13 added post-Task-12 to remediate the bench_closure_chain regression (Task 12 was reported DONE but bench/check.py exit 1 on 4 metrics: +29% bump_s, +47% rc_s, +29% bump_rss_kb, +48% rc_rss_kb). Task 13 added direct-icmp intercept arms for lt__Int/le__Int/gt__Int/ge__Int/ne__Int in try_emit_primitive_instance_body, bypassing the compare__Int -> Ordering -> match indirection. Post-Task-13 bench/check.py exits 0; bench_closure_chain back to baseline (-6% bump_s, -3% rc_s)."
+}

crates/ail/tests/e2e.rs

@@ -1030,8 +1030,10 @@ fn describe_workspace_resolves_qualified_name() {
 
 /// Guards Iter 6: `ail deps` no longer surfaces built-ins, params, or
 /// let-bindings as edges. The single-module `sum` def in `sum.ail.json`
-/// uses `+`, `-`, `==`, the param `n`, and the recursive call `sum`.
+/// uses `+`, `-`, `eq` (class-method dispatch via prelude.Eq), the param
-/// Only the recursive call must remain.
+/// `n`, and the recursive call `sum`. Arithmetic builtins (`+`/`-`) and
+/// the local param drop out; what remains are the recursive call and
+/// the class-method `eq` cross-module reference.
 #[test]
 fn deps_filters_builtins_params_locals() {
     let manifest_dir = env!("CARGO_MANIFEST_DIR");
@@ -1063,8 +1065,8 @@ fn deps_filters_builtins_params_locals() {
         .collect();
     assert_eq!(
         refs,
-        vec!["sum"],
+        vec!["eq", "sum"],
-        "expected only the recursive call `sum`; got {refs:?}"
+        "expected the class-method `eq` reference and the recursive call `sum`; got {refs:?}"
     );
 }
 
@@ -1348,16 +1350,17 @@ fn borrow_own_demo_modes_are_metadata_only() {
     assert_eq!(lines, vec!["3", "6"]);
 }
 
-/// polymorphic `==`. Properties protected:
+/// Class-dispatched `eq` over Int / Bool / Str / Unit. Properties protected:
-/// (1) `==` typechecks at Int / Bool / Str / Unit (the fixture
+/// (1) `eq` resolves via `prelude.Eq.eq` for every supported primitive
-///     uses every supported case directly via `(app == ...)`);
+///     type (the fixture uses every case directly via `(app eq ...)`);
-/// (2) codegen dispatches each arg-type to the right LLVM shape
+/// (2) the codegen intercept `try_emit_primitive_instance_body` emits
-///     — `icmp eq i64`, `icmp eq i1`, `@strcmp + icmp eq i32 0`,
+///     the right single-instruction body per type — `icmp eq i64`,
-///     constant `i1 true` — and the binary's stdout matches the
+///     `icmp eq i1`, `@ail_str_eq`, constant `i1 1` — and the binary's
-///     boolean truth-table for those operators;
+///     stdout matches the boolean truth-table for those equalities;
-/// (3) 16c's `build_eq` desugar of `(pat-lit "hi")` over a `Str`
+/// (3) `build_eq`'s desugar of `(pat-lit "hi")` over a `Str`
-///     scrutinee now goes through, since `==` no longer rejects
+///     scrutinee routes through the class-method `eq` (not the
-///     non-Int args at typecheck.
+///     deleted operator `==`), exercising the same Eq Str instance
+///     body via the lit-pattern path.
 #[test]
 fn eq_demo() {
     let stdout = build_and_run("eq_demo.ail");

crates/ail/tests/eq_float_must_fail_pin.rs

@@ -0,0 +1,37 @@
+//! Pin: `(app eq 1.5 1.5)` must fail typecheck with NoInstance
+//! Eq Float AND the diagnostic must mention `float_eq` as the
+//! explicit alternative. Today the NoInstance fires (per
+//! eq_float_noinstance.rs) but `float_eq` is not in the message
+//! — the milestone adds that hint.
+
+use std::path::PathBuf;
+use std::process::Command;
+
+#[test]
+fn eq_float_must_fail_diagnostic_names_float_eq() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let repo_root = PathBuf::from(manifest_dir).join("../..");
+    let fixture = repo_root.join("examples/eq_float_must_fail.ail");
+
+    let out = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .arg("check")
+        .arg(&fixture)
+        .output()
+        .expect("ail check failed to spawn");
+
+    assert!(
+        !out.status.success(),
+        "expected typecheck failure, got success: stdout={}",
+        String::from_utf8_lossy(&out.stdout)
+    );
+
+    let stderr = String::from_utf8_lossy(&out.stderr);
+    assert!(
+        stderr.contains("no-instance") && stderr.contains("Float"),
+        "expected no-instance diagnostic + Float, got: {stderr}"
+    );
+    assert!(
+        stderr.contains("float_eq"),
+        "expected diagnostic to name `float_eq` as the explicit alternative; got: {stderr}"
+    );
+}

crates/ail/tests/eq_float_noinstance.rs

@@ -42,4 +42,13 @@ fn eq_at_float_fires_float_aware_noinstance() {
         "expected NoInstance message to cross-reference the float-semantics contract, got: {:?}",
         no_inst.message
     );
+    // 2026-05-21 operator-routing-eq-ord: the addendum names the
+    // explicit IEEE-aware alternative `float_eq` (and siblings)
+    // alongside the contract cross-reference, so the LLM author
+    // learns the named-fn surface from the diagnostic itself.
+    assert!(
+        no_inst.message.contains("float_eq"),
+        "expected NoInstance message to name `float_eq` as the explicit IEEE-aware alternative, got: {:?}",
+        no_inst.message
+    );
 }

crates/ail/tests/eq_ord_e2e.rs

@@ -129,9 +129,14 @@ fn eq_ord_user_adt_eq_intbox_hash_stable() {
     // through rigid substitution. Eq's class method declares
     // `param_modes: ["borrow", "borrow"]` — the user-instance
     // mono synthesis used to silently strip those.
+    //
+    // 2026-05-21 operator-routing-eq-ord re-pinned (prior:
+    // 3c4cf040cb4e8bb2): the user-instance body's inner `(app == ai bi)`
+    // migrates to `(app eq ai bi)` per the operator-name deletion
+    // sweep — the call site symbol name shifts, body hash follows.
     let h = def_hash(&Def::Fn(eq_intbox.clone()));
     assert_eq!(
-        h, "3c4cf040cb4e8bb2",
+        h, "ceb466964df0e8d1",
         "eq__IntBox body hash drifted — see mono_hash_stability.rs for the resolution pattern; captured: {h}"
     );
 }

crates/ail/tests/eq_user_adt_smoke_e2e.rs

@@ -0,0 +1,42 @@
+//! North-star E2E for the operator-routing-eq-ord milestone:
+//! exercises Eq Unit (new instance), user-ADT Eq Point with a
+//! hand-written instance, and nested-Int Eq dispatch — all
+//! through the class-method path with no `==` callee anywhere.
+//!
+//! Today this test fires `NoInstance Eq Unit` at typecheck
+//! (Unit lacks an Eq instance), proving RED-first before the
+//! milestone lands.
+
+use std::path::PathBuf;
+use std::process::Command;
+
+#[test]
+fn eq_user_adt_smoke_prints_unit_then_point_eq_then_neq() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let repo_root = PathBuf::from(manifest_dir).join("../..");
+    let fixture = repo_root.join("examples/eq_user_adt_smoke.ail");
+    let bin = repo_root.join("target/debug/eq_user_adt_smoke_test_bin");
+
+    let build = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .arg("build")
+        .arg(&fixture)
+        .arg("-o")
+        .arg(&bin)
+        .output()
+        .expect("ail build failed to spawn");
+    assert!(
+        build.status.success(),
+        "ail build failed: stderr={}",
+        String::from_utf8_lossy(&build.stderr)
+    );
+
+    let run = Command::new(&bin)
+        .output()
+        .expect("binary failed to spawn");
+    assert!(run.status.success(), "binary failed: stderr={}", String::from_utf8_lossy(&run.stderr));
+    assert_eq!(
+        String::from_utf8_lossy(&run.stdout).as_ref(),
+        "true\ntrue\nfalse\n",
+        "expected Unit-eq then Point-eq then Point-neq"
+    );
+}

crates/ail/tests/float_compare_smoke_e2e.rs

@@ -0,0 +1,39 @@
+//! E2E for the six float_* named comparison fns. After the
+//! milestone, Float comparability survives via float_eq / float_lt
+//! / etc. (no Eq Float instance, no `==` callee). Today this test
+//! fires `unknown variable: float_eq` since the symbol does not
+//! exist — RED-first.
+
+use std::path::PathBuf;
+use std::process::Command;
+
+#[test]
+fn float_compare_smoke_prints_true_true_false() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let repo_root = PathBuf::from(manifest_dir).join("../..");
+    let fixture = repo_root.join("examples/float_compare_smoke.ail");
+    let bin = repo_root.join("target/debug/float_compare_smoke_test_bin");
+
+    let build = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .arg("build")
+        .arg(&fixture)
+        .arg("-o")
+        .arg(&bin)
+        .output()
+        .expect("ail build failed to spawn");
+    assert!(
+        build.status.success(),
+        "ail build failed: stderr={}",
+        String::from_utf8_lossy(&build.stderr)
+    );
+
+    let run = Command::new(&bin)
+        .output()
+        .expect("binary failed to spawn");
+    assert!(run.status.success(), "binary failed: stderr={}", String::from_utf8_lossy(&run.stderr));
+    assert_eq!(
+        String::from_utf8_lossy(&run.stdout).as_ref(),
+        "true\ntrue\nfalse\n",
+        "expected float_eq then float_lt then float_eq mismatch"
+    );
+}

crates/ail/tests/mono_hash_stability.rs

@@ -46,10 +46,16 @@ fn primitive_eq_ord_mono_symbol_hashes_stay_bit_identical() {
     // the mono-synthesised `eq__T` / `compare__T` symbols now carry
     // those modes in their `Type::Fn` — canonical-JSON bytes drift,
     // bodies are semantically identical.
+    // 2026-05-21 operator-routing-eq-ord re-pinned the three `eq__*`
+    // hashes after the prelude reshape: the Eq Int/Bool/Str instance
+    // bodies became placeholder `false` lambdas (codegen intercept
+    // emits the actual `icmp` / `@ail_str_eq` call). The three
+    // `compare__*` hashes were unchanged — those bodies were already
+    // placeholder Ordering ctors.
     let pins: &[(&str, &str)] = &[
-        ("eq__Int",       "8bf7bec502487a57"),
+        ("eq__Int",       "86ed4988438924d3"),
-        ("eq__Bool",      "e46d7e6cd2ec459c"),
+        ("eq__Bool",      "d62d4d8c51f433f8"),
-        ("eq__Str",       "2a92935174182d2f"),
+        ("eq__Str",       "3d32f377c66b03e0"),
         ("compare__Int",  "6d6c20520766368b"),
         ("compare__Bool", "02b64e8fadc913eb"),
         ("compare__Str",  "9645929d53cd3cc9"),

crates/ail/tests/operator_names_unbound_pin.rs

@@ -0,0 +1,33 @@
+//! Pin: the operator names `==` / `!=` / `<` / `<=` / `>` / `>=`
+//! are NOT part of the language. Surface use of any of them must
+//! resolve as `unknown variable: ==` (et al.). Today they all
+//! typecheck (== polymorphic, the others monomorphic-Int) —
+//! RED-first.
+
+use std::path::PathBuf;
+use std::process::Command;
+
+#[test]
+fn comparator_operator_name_is_unbound() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let repo_root = PathBuf::from(manifest_dir).join("../..");
+    let fixture = repo_root.join("examples/operator_unbound_check.ail");
+
+    let out = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .arg("check")
+        .arg(&fixture)
+        .output()
+        .expect("ail check failed to spawn");
+
+    assert!(
+        !out.status.success(),
+        "expected typecheck failure for `(app == 5 5)`; got success: stdout={}",
+        String::from_utf8_lossy(&out.stdout)
+    );
+
+    let stderr = String::from_utf8_lossy(&out.stderr);
+    assert!(
+        stderr.contains("unbound-var") && stderr.contains("=="),
+        "expected `[unbound-var] ... ==` diagnostic, got: {stderr}"
+    );
+}

crates/ail/tests/ord_int_intercept_ir_pin.rs

@@ -0,0 +1,140 @@
+//! Pin: the `lt__Int` / `le__Int` / `gt__Int` / `ge__Int` /
+//! `ne__Int` mono symbols lower to a single direct `icmp` (no
+//! `compare__Int` call, no `match` over `Ordering`), carrying the
+//! `alwaysinline` attribute. The polymorphic prelude bodies are
+//! `(match (app compare x y) ...)`; without the direct intercept
+//! arm, each `lt`-at-Int call site goes through
+//! `compare__Int` → allocate an `Ordering` ctor → match. At `-O2`
+//! `alwaysinline` plus `icmp slt i64` lets clang inline the
+//! comparison to the use site; without it, bench/check.py
+//! regresses on bench_closure_chain (+29% bump_s, +47% rc_s,
+//! +29% bump_rss_kb, +48% rc_rss_kb — observed 2026-05-21 before
+//! Task 13 of iter operator-routing-eq-ord.1 added these intercept
+//! arms).
+//!
+//! The test reads pre-optimization IR (`ail emit-ir`'s output —
+//! emit-ir runs codegen without clang's opt pipeline) and
+//! structurally pins the intercept body shape. Post-opt verification
+//! lives in `bench/check.py`.
+
+use std::path::PathBuf;
+use std::process::Command;
+
+fn fixture_path(name: &str) -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("../../examples")
+        .join(name)
+}
+
+fn emit_ir(fixture: &str) -> String {
+    let src = fixture_path(fixture);
+    let out = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .args(["emit-ir", src.to_str().unwrap()])
+        .output()
+        .expect("ail emit-ir");
+    assert!(
+        out.status.success(),
+        "ail emit-ir failed:\nstdout: {}\nstderr: {}",
+        String::from_utf8_lossy(&out.stdout),
+        String::from_utf8_lossy(&out.stderr),
+    );
+    String::from_utf8_lossy(&out.stdout).to_string()
+}
+
+/// Locate a `define ... @ail_prelude_<sym>(...) <attrs> { ... }`
+/// block in the IR and return the body text between the opening
+/// `{\n` and the matching closing `}\n`. Anchors on `define` so
+/// call sites (which also mention `@ail_prelude_<sym>(`) don't
+/// match.
+fn extract_fn_body(ir: &str, sym: &str) -> (String, String) {
+    let needle = format!("define ");
+    let mut cursor = 0;
+    let sym_marker = format!("@ail_prelude_{sym}(");
+    loop {
+        let rel = ir[cursor..]
+            .find(&needle)
+            .unwrap_or_else(|| panic!("no `define` line carrying @ail_prelude_{sym}"));
+        let define_start = cursor + rel;
+        // The `define` line runs to the next `\n`; check whether the
+        // symbol marker appears on that line.
+        let line_end = ir[define_start..]
+            .find('\n')
+            .expect("define line not terminated");
+        let line = &ir[define_start..define_start + line_end];
+        if line.contains(&sym_marker) {
+            // Found the right define. Pull attrs (between `)` and `{`)
+            // and body (between `{\n` and `\n}\n`).
+            let after_paren = line
+                .rfind(')')
+                .expect("malformed define line: no close-paren");
+            let brace = line
+                .find('{')
+                .expect("malformed define line: no open-brace");
+            let attrs = line[after_paren + 1..brace].trim().to_string();
+            let body_start = define_start + brace + 1;
+            let body_end = ir[body_start..]
+                .find("\n}\n")
+                .expect("fn body not terminated by `\\n}\\n`");
+            return (attrs, ir[body_start..body_start + body_end].to_string());
+        }
+        cursor = define_start + line_end + 1;
+    }
+}
+
+#[test]
+fn lt_int_intercept_emits_direct_icmp_slt() {
+    let ir = emit_ir("bench_closure_chain.ail");
+    let (attrs, body) = extract_fn_body(&ir, "lt__Int");
+    assert!(
+        attrs.contains("alwaysinline"),
+        "lt__Int missing `alwaysinline`; got attrs `{attrs}`"
+    );
+    assert!(
+        body.contains("icmp slt i64"),
+        "lt__Int body lacks direct `icmp slt i64`; body:\n{body}"
+    );
+    assert!(
+        !body.contains("@ail_prelude_compare__Int"),
+        "lt__Int still routes through compare__Int (intercept arm missing); body:\n{body}"
+    );
+}
+
+/// `le__Int`, `gt__Int`, `ge__Int`, `ne__Int` — the same intercept
+/// family. They are not reachable from bench_closure_chain itself,
+/// so this test uses a synthesised fixture that calls each of them
+/// once on Int operands. Keeping all five intercept arms on a
+/// single bench-style code path under one assertion fence guards
+/// the family symmetrically.
+#[test]
+fn ord_int_intercept_family_emits_direct_icmp() {
+    let ir = emit_ir("ord_int_intercept_smoke.ail");
+    for (sym, want_op) in &[
+        ("lt__Int", "icmp slt i64"),
+        ("le__Int", "icmp sle i64"),
+        ("gt__Int", "icmp sgt i64"),
+        ("ge__Int", "icmp sge i64"),
+        ("ne__Int", "icmp ne i64"),
+    ] {
+        let (attrs, body) = extract_fn_body(&ir, sym);
+        assert!(
+            attrs.contains("alwaysinline"),
+            "{sym} missing `alwaysinline`; got attrs `{attrs}`"
+        );
+        assert!(
+            body.contains(want_op),
+            "{sym} body lacks `{want_op}`; body:\n{body}"
+        );
+        assert!(
+            !body.contains("@ail_prelude_compare__Int"),
+            "{sym} still routes through compare__Int; body:\n{body}"
+        );
+        // ne__Int specifically must not be `not (eq x y)` — the spec
+        // explicitly rejected the indirection.
+        if *sym == "ne__Int" {
+            assert!(
+                !body.contains("@ail_prelude_eq__Int"),
+                "ne__Int uses `not (eq x y)` indirection (forbidden by spec); body:\n{body}"
+            );
+        }
+    }
+}

crates/ail/tests/prelude_eq_alwaysinline_ir_pin.rs

@@ -0,0 +1,50 @@
+//! Pin: the codegen mechanism that emits primitive Eq/Ord
+//! instance bodies (try_emit_primitive_instance_body) MUST
+//! attach an `alwaysinline` attribute to the generated LLVM
+//! function definition so the `-O0` build path inlines the
+//! single-instruction body at every use site, matching the IR
+//! shape the deleted `lower_eq` direct-emit produced. Without
+//! `alwaysinline`, `ail run` (which defaults to -O0) pays a
+//! function-call overhead per comparison.
+
+use std::path::PathBuf;
+use std::process::Command;
+
+#[test]
+fn prelude_eq_int_carries_alwaysinline_attribute_in_emitted_ir() {
+    let manifest_dir = env!("CARGO_MANIFEST_DIR");
+    let repo_root = PathBuf::from(manifest_dir).join("../..");
+    // Use a fixture that already invokes the class-method `eq` path
+    // (so prelude.eq__Int gets monomorphised into the emitted IR).
+    // `eq_demo.ail` calls `(app == …)` directly which today uses the
+    // `lower_eq` direct-emit short-circuit and never references the
+    // prelude eq__Int symbol; `eq_ord_user_adt.ail` calls `(app eq …)`
+    // on an IntBox whose user instance internally calls `(app eq ai bi)`
+    // on Int, monomorphising `eq__Int` into the IR.
+    let fixture = repo_root.join("examples/eq_ord_user_adt.ail");
+
+    let out = Command::new(env!("CARGO_BIN_EXE_ail"))
+        .arg("emit-ir")
+        .arg(&fixture)
+        .output()
+        .expect("ail emit-ir failed to spawn");
+    assert!(
+        out.status.success(),
+        "ail emit-ir failed: stderr={}",
+        String::from_utf8_lossy(&out.stderr)
+    );
+
+    let ir = String::from_utf8_lossy(&out.stdout);
+    // Either form is acceptable:
+    //   define i1 @ail_prelude_eq__Int(i64, i64) alwaysinline { ... }
+    // (attribute appended to the define line). The grep checks for
+    // both the symbol presence and the alwaysinline annotation in
+    // the same line as the define.
+    let saw_define_with_alwaysinline = ir
+        .lines()
+        .any(|line| line.contains("define") && line.contains("eq__Int") && line.contains("alwaysinline"));
+    assert!(
+        saw_define_with_alwaysinline,
+        "expected `define … eq__Int … alwaysinline` in emitted IR; full IR follows:\n{ir}"
+    );
+}

crates/ail/tests/snapshots/hello.ll

@@ -24,6 +24,12 @@ declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
 @ail_hello_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_hello_main_adapter, ptr null }
+@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
+@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
+@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
+@ail_prelude_float_le_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_le_adapter, ptr null }
+@ail_prelude_float_gt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_gt_adapter, ptr null }
+@ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
 define i8 @ail_hello_main() {
 entry:
   %v1 = getelementptr inbounds i8, ptr getelementptr inbounds (<{ i64, [15 x i8] }>, ptr @.str_hello_str_0, i32 0, i32 0), i64 8
@@ -37,6 +43,78 @@ entry:
   ret i8 %r
 }
 
+define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oeq double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_eq_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_eq(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ne(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp une double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ne_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ne(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_lt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp olt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_lt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_lt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_le(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ole double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_le_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_le(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_gt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ogt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_gt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_gt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ge(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oge double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ge_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ge(double %a0, double %a1)
+  ret i1 %r
+}
+
 define void @drop_prelude_Ordering(ptr %p) {
 entry:
   %is_null = icmp eq ptr %p, null

crates/ail/tests/snapshots/list.ll

@@ -23,6 +23,12 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
 
 @ail_list_sum_list_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_sum_list_adapter, ptr null }
 @ail_list_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_main_adapter, ptr null }
+@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
+@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
+@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
+@ail_prelude_float_le_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_le_adapter, ptr null }
+@ail_prelude_float_gt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_gt_adapter, ptr null }
+@ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
 @ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
 define i64 @ail_list_sum_list(ptr %arg_xs) {
@@ -146,6 +152,78 @@ ret:
   ret void
 }
 
+define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oeq double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_eq_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_eq(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ne(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp une double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ne_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ne(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_lt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp olt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_lt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_lt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_le(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ole double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_le_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_le(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_gt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ogt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_gt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_gt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ge(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oge double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ge_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ge(double %a0, double %a1)
+  ret i1 %r
+}
+
 define ptr @ail_prelude_show__Int(i64 %arg_x) {
 entry:
   %v1 = call ptr @ailang_int_to_str(i64 %arg_x)

crates/ail/tests/snapshots/max3.ll

@@ -24,11 +24,19 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
 @ail_max3_max_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max_adapter, ptr null }
 @ail_max3_max3_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max3_adapter, ptr null }
 @ail_max3_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_main_adapter, ptr null }
+@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
+@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
+@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
+@ail_prelude_float_le_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_le_adapter, ptr null }
+@ail_prelude_float_gt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_gt_adapter, ptr null }
+@ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
+@ail_prelude_compare__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_compare__Int_adapter, ptr null }
+@ail_prelude_gt__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_gt__Int_adapter, ptr null }
 @ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
 define i64 @ail_max3_max(i64 %arg_a, i64 %arg_b) {
 entry:
-  %v1 = icmp sgt i64 %arg_a, %arg_b
+  %v1 = call i1 @ail_prelude_gt__Int(i64 %arg_a, i64 %arg_b)
   br i1 %v1, label %then.2, label %else.2
 then.2:
   br label %join.2
@@ -47,10 +55,10 @@ entry:
 
 define i64 @ail_max3_max3(i64 %arg_a, i64 %arg_b, i64 %arg_c) {
 entry:
-  %v1 = icmp sgt i64 %arg_a, %arg_b
+  %v1 = call i1 @ail_prelude_gt__Int(i64 %arg_a, i64 %arg_b)
   br i1 %v1, label %then.2, label %else.2
 then.2:
-  %v3 = icmp sgt i64 %arg_a, %arg_c
+  %v3 = call i1 @ail_prelude_gt__Int(i64 %arg_a, i64 %arg_c)
   br i1 %v3, label %then.4, label %else.4
 then.4:
   br label %join.4
@@ -60,7 +68,7 @@ join.4:
   %v5 = phi i64 [ %arg_a, %then.4 ], [ %arg_c, %else.4 ]
   br label %join.2
 else.2:
-  %v6 = icmp sgt i64 %arg_b, %arg_c
+  %v6 = call i1 @ail_prelude_gt__Int(i64 %arg_b, i64 %arg_c)
   br i1 %v6, label %then.7, label %else.7
 then.7:
   br label %join.7
@@ -93,6 +101,117 @@ entry:
   ret i8 %r
 }
 
+define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oeq double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_eq_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_eq(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ne(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp une double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ne_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ne(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_lt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp olt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_lt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_lt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_le(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ole double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_le_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_le(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_gt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ogt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_gt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_gt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ge(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oge double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ge_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ge(double %a0, double %a1)
+  ret i1 %r
+}
+
+define ptr @ail_prelude_compare__Int(i64 %arg_x, i64 %arg_y) alwaysinline {
+entry:
+  %v1 = icmp slt i64 %arg_x, %arg_y
+  br i1 %v1, label %cmp_lt_2, label %cmp_after_lt_2
+cmp_lt_2:
+  %v3 = call ptr @ailang_rc_alloc(i64 8)
+  store i64 0, ptr %v3, align 8
+  ret ptr %v3
+cmp_after_lt_2:
+  %v4 = icmp eq i64 %arg_x, %arg_y
+  br i1 %v4, label %cmp_eq_2, label %cmp_gt_2
+cmp_eq_2:
+  %v5 = call ptr @ailang_rc_alloc(i64 8)
+  store i64 1, ptr %v5, align 8
+  ret ptr %v5
+cmp_gt_2:
+  %v6 = call ptr @ailang_rc_alloc(i64 8)
+  store i64 2, ptr %v6, align 8
+  ret ptr %v6
+}
+
+define ptr @ail_prelude_compare__Int_adapter(ptr %_env, i64 %a0, i64 %a1) {
+entry:
+  %r = call ptr @ail_prelude_compare__Int(i64 %a0, i64 %a1)
+  ret ptr %r
+}
+
+define i1 @ail_prelude_gt__Int(i64 %arg_x, i64 %arg_y) alwaysinline {
+entry:
+  %v1 = icmp sgt i64 %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_gt__Int_adapter(ptr %_env, i64 %a0, i64 %a1) {
+entry:
+  %r = call i1 @ail_prelude_gt__Int(i64 %a0, i64 %a1)
+  ret i1 %r
+}
+
 define ptr @ail_prelude_show__Int(i64 %arg_x) {
 entry:
   %v1 = call ptr @ailang_int_to_str(i64 %arg_x)

crates/ail/tests/snapshots/sum.ll

@@ -21,10 +21,101 @@ declare ptr @ailang_str_clone(ptr)
 declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
+@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
+@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
+@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
+@ail_prelude_float_le_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_le_adapter, ptr null }
+@ail_prelude_float_gt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_gt_adapter, ptr null }
+@ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
+@ail_prelude_eq__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_eq__Int_adapter, ptr null }
 @ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
 @ail_sum_sum_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_sum_adapter, ptr null }
 @ail_sum_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_main_adapter, ptr null }
+define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oeq double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_eq_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_eq(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ne(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp une double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ne_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ne(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_lt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp olt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_lt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_lt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_le(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ole double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_le_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_le(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_gt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ogt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_gt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_gt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ge(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oge double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ge_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ge(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_eq__Int(i64 %arg_x, i64 %arg_y) alwaysinline {
+entry:
+  %v1 = icmp eq i64 %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_eq__Int_adapter(ptr %_env, i64 %a0, i64 %a1) {
+entry:
+  %r = call i1 @ail_prelude_eq__Int(i64 %a0, i64 %a1)
+  ret i1 %r
+}
+
 define ptr @ail_prelude_show__Int(i64 %arg_x) {
 entry:
   %v1 = call ptr @ailang_int_to_str(i64 %arg_x)
@@ -106,7 +197,7 @@ ret:
 
 define i64 @ail_sum_sum(i64 %arg_n) {
 entry:
-  %v1 = icmp eq i64 %arg_n, 0
+  %v1 = call i1 @ail_prelude_eq__Int(i64 %arg_n, i64 0)
   br i1 %v1, label %then.2, label %else.2
 then.2:
   br label %join.2

crates/ail/tests/snapshots/ws_main.ll

@@ -21,10 +21,88 @@ declare ptr @ailang_str_clone(ptr)
 declare ptr @ailang_str_concat(ptr, ptr)
 declare i64 @llvm.fptosi.sat.i64.f64(double)
 
+@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
+@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
+@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
+@ail_prelude_float_le_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_le_adapter, ptr null }
+@ail_prelude_float_gt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_gt_adapter, ptr null }
+@ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
 @ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
 @ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
 @ail_ws_lib_add_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_lib_add_adapter, ptr null }
 @ail_ws_main_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_main_main_adapter, ptr null }
+define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oeq double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_eq_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_eq(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ne(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp une double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ne_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ne(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_lt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp olt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_lt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_lt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_le(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ole double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_le_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_le(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_gt(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp ogt double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_gt_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_gt(double %a0, double %a1)
+  ret i1 %r
+}
+
+define i1 @ail_prelude_float_ge(double %arg_x, double %arg_y) alwaysinline {
+entry:
+  %v1 = fcmp oge double %arg_x, %arg_y
+  ret i1 %v1
+}
+
+define i1 @ail_prelude_float_ge_adapter(ptr %_env, double %a0, double %a1) {
+entry:
+  %r = call i1 @ail_prelude_float_ge(double %a0, double %a1)
+  ret i1 %r
+}
+
 define ptr @ail_prelude_show__Int(i64 %arg_x) {
 entry:
   %v1 = call ptr @ailang_int_to_str(i64 %arg_x)

crates/ailang-check/src/builtins.rs

@@ -68,20 +68,11 @@ pub fn install(env: &mut crate::Env) {
             ret_mode: ailang_core::ast::ParamMode::Implicit,
         }),
     };
-    let poly_a_a_to_bool = || Type::Forall {
+    // 2026-05-21 operator-routing-eq-ord: the `poly_a_a_to_bool`
-        vars: vec!["a".into()],
+    // helper produced the `forall a. (a, a) -> Bool` shape used by
-        constraints: vec![],
+    // the six comparator builtins (`==`/`!=`/`<`/`<=`/`>`/`>=`).
-        body: Box::new(Type::Fn {
+    // Those builtins are gone (class-method dispatch via prelude.Eq
-            params: vec![
+    // / Ord replaces them); the helper is dead.
-                Type::Var { name: "a".into() },
-                Type::Var { name: "a".into() },
-            ],
-            ret: Box::new(Type::bool_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ailang_core::ast::ParamMode::Implicit,
-        }),
-    };
     let int_int_int = Type::Fn {
         params: vec![Type::int(), Type::int()],
         ret: Box::new(Type::int()),
@@ -93,36 +84,13 @@ pub fn install(env: &mut crate::Env) {
         env.globals.insert(op.into(), poly_a_a_to_a());
     }
     env.globals.insert("%".into(), int_int_int);
-    for op in ["!=", "<", "<=", ">", ">="] {
+    // 2026-05-21 operator-routing-eq-ord: the six comparator names
-        env.globals.insert(op.into(), poly_a_a_to_bool());
+    // `==` / `!=` / `<` / `<=` / `>` / `>=` are no longer part of the
-    }
+    // language. Equality / ordering go through the class methods
-
+    // `eq` / `compare` (and the free helpers `ne` / `lt` / `le` /
-    // `==` is polymorphic — `forall a. (a, a) -> Bool`. Codegen
+    // `gt` / `ge`) dispatched via prelude.Eq / prelude.Ord; Float
-    // dispatches on the resolved arg type at the call site:
+    // comparison goes through the named fns `float_eq` / `float_ne`
-    // `Int` → `icmp eq i64`, `Bool` → `icmp eq i1`, `Str` → `@strcmp`,
+    // / `float_lt` / `float_le` / `float_gt` / `float_ge`.
-    // `Unit` → constant `i1 1`, `Float` → `fcmp oeq double`. ADT/Fn
-    // equality is rejected at codegen with a clear "== not supported
-    // for type X" error. The ordering ops (`<`, `<=`, `>`, `>=`, `!=`)
-    // share the same polymorphic shape but with `Bool` return; `==`
-    // stays in its own arm only because the codegen-side dispatch
-    // table has historically been per-op.
-    env.globals.insert(
-        "==".into(),
-        Type::Forall {
-            vars: vec!["a".into()],
-            constraints: vec![],
-            body: Box::new(Type::Fn {
-                params: vec![
-                    Type::Var { name: "a".into() },
-                    Type::Var { name: "a".into() },
-                ],
-                ret: Box::new(Type::bool_()),
-                effects: vec![],
-                param_modes: vec![],
-                ret_mode: ailang_core::ast::ParamMode::Implicit,
-            }),
-        },
-    );
     env.globals.insert(
         "not".into(),
         Type::Fn {
@@ -300,12 +268,6 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
         ("*", "forall a. (a, a) -> a"),
         ("/", "forall a. (a, a) -> a"),
         ("%", "(Int, Int) -> Int"),
-        ("==", "forall a. (a, a) -> Bool"),
-        ("!=", "forall a. (a, a) -> Bool"),
-        ("<", "forall a. (a, a) -> Bool"),
-        ("<=", "forall a. (a, a) -> Bool"),
-        (">", "forall a. (a, a) -> Bool"),
-        (">=", "forall a. (a, a) -> Bool"),
         ("not", "(Bool) -> Bool"),
         ("__unreachable__", "forall a. a"),
         ("neg", "forall a. (a) -> a"),
@@ -408,26 +370,15 @@ mod tests {
         assert_eq!(ty, Type::float(), "(+ 1.5 2.5) must type as Float");
     }
 
-    /// regression — `(< 1 2)` still resolves to `Bool`
+    // 2026-05-21 operator-routing-eq-ord: the two `widen_lt_*` smoke
-    /// after the widening to `forall a. (a, a) -> Bool`. Mirrors the
+    // tests (Int-Int-Bool + Float-Float-Bool) lived inside the builtin
-    /// `+` regression check for the comparison-op path.
+    // env and pinned `<` as a builtin. With `<` deleted from the
-    #[test]
+    // builtin table, the tests are unreachable — comparison is now a
-    fn widen_lt_keeps_int_int_bool() {
+    // class-method (`lt` via prelude.Ord) for Int/Bool/Str and a
-        let ty = synth_in_builtins_env(&app("<", vec![lit_int(1), lit_int(2)]));
+    // named fn (`float_lt`) for Float, neither of which is in the
-        assert_eq!(ty, Type::bool_(), "(< 1 2) must still type as Bool");
+    // `synth_in_builtins_env`-visible namespace. Coverage of the new
-    }
+    // surface lives in `eq_ord_e2e.rs` (Ord class-dispatch) and in
-
+    // `float_compare_smoke_e2e.rs` (named-fn Float path).
-    /// new acceptance — `(< 1.5 2.5)` types as `Bool`.
-    /// Pre-widening this would have failed with `TypeMismatch`. The
-    /// widening to `forall a. (a, a) -> Bool` lets Float ordering
-    /// typecheck cleanly; codegen lowers to `fcmp olt double` in iter 4.
-    #[test]
-    fn widen_lt_accepts_float_float_bool() {
-        let bits_a = 1.5_f64.to_bits();
-        let bits_b = 2.5_f64.to_bits();
-        let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits_a), lit_float(bits_b)]));
-        assert_eq!(ty, Type::bool_(), "(< 1.5 2.5) must type as Bool");
-    }
 
     /// `neg` is polymorphic — `forall a. (a) -> a`.
     /// Both `(neg 5) : Int` and `(neg 1.5) : Float` typecheck. The

crates/ailang-check/src/lib.rs

@@ -871,7 +871,10 @@ impl CheckError {
             if (class == "prelude.Eq" || class == "prelude.Ord") && at_type == "Float" {
                 d.message = format!(
                     "{} — Float has no Eq/Ord instance by design (partial \
-                     orderability per IEEE-754); see design/contracts/float-semantics.md.",
+                     orderability per IEEE-754); use float_eq / float_lt \
+                     (and siblings float_ne / float_le / float_gt / float_ge) \
+                     for explicit IEEE-aware comparison. \
+                     See design/contracts/float-semantics.md.",
                     d.message
                 );
             } else if class == "prelude.Show" {
@@ -5618,88 +5621,15 @@ mod tests {
         check(&m).expect("tail-call in tail position should typecheck");
     }
 
-    /// a `Term::LetRec` that captures a `Term::Let`-bound
+    // 2026-05-21 operator-routing-eq-ord: the
-    /// name (whose type is known only after typecheck) reaches `synth`
+    // `letrec_with_let_binding_capture_typechecks` test relied on
-    /// because the desugar pass leaves it in place. The new typing
+    // the builtin `>=` to express its `if (>= i threshold) ...`
-    /// rule for `Term::LetRec` accepts it: extends locals with `name`
+    // condition. With `>=` deleted from the builtin table, the test
-    /// and the params, synths the body, unifies against the declared
+    // cannot be reconstructed inside this single-module check_module
-    /// return type, then synths the in-clause.
+    // env (which has no prelude auto-import, so `ge` is unbound).
-    #[test]
+    // The LetRec-captures-Let-binding property remains pinned by
-    fn letrec_with_let_binding_capture_typechecks() {
+    // the workspace e2e tests `local_rec_let_capture` (and siblings)
-        // fn outer : (Int) -> Int = \n.
+    // which DO carry the auto-imported prelude.
-        //   let threshold = + 5 5
-        //   in let-rec loop : (Int) -> Int = \i.
-        //        if (>= i threshold) then 0 else loop (+ i 1)
-        //      in loop 0
-        let body = Term::Let {
-            name: "threshold".into(),
-            value: Box::new(Term::App {
-                callee: Box::new(Term::Var { name: "+".into() }),
-                args: vec![
-                    Term::Lit { lit: Literal::Int { value: 5 } },
-                    Term::Lit { lit: Literal::Int { value: 5 } },
-                ],
-                tail: false,
-            }),
-            body: Box::new(Term::LetRec {
-                name: "loop".into(),
-                ty: Type::Fn {
-                    params: vec![Type::int()],
-                    ret: Box::new(Type::int()),
-                    effects: vec![],
-                    param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
-                },
-                params: vec!["i".into()],
-                body: Box::new(Term::If {
-                    cond: Box::new(Term::App {
-                        callee: Box::new(Term::Var { name: ">=".into() }),
-                        args: vec![
-                            Term::Var { name: "i".into() },
-                            Term::Var { name: "threshold".into() },
-                        ],
-                        tail: false,
-                    }),
-                    then: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
-                    else_: Box::new(Term::App {
-                        callee: Box::new(Term::Var { name: "loop".into() }),
-                        args: vec![Term::App {
-                            callee: Box::new(Term::Var { name: "+".into() }),
-                            args: vec![
-                                Term::Var { name: "i".into() },
-                                Term::Lit { lit: Literal::Int { value: 1 } },
-                            ],
-                            tail: false,
-                        }],
-                        tail: false,
-                    }),
-                }),
-                in_term: Box::new(Term::App {
-                    callee: Box::new(Term::Var { name: "loop".into() }),
-                    args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
-                    tail: false,
-                }),
-            }),
-        };
-        let m = Module {
-            schema: SCHEMA.into(),
-            name: "t".into(),
-            imports: vec![],
-            defs: vec![fn_def(
-                "outer",
-                Type::Fn {
-                    params: vec![Type::int()],
-                    ret: Box::new(Type::int()),
-                    effects: vec![],
-                    param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
-                },
-                vec!["n"],
-                body,
-            )],
-        };
-        check(&m).expect("LetRec with Let-binding capture should typecheck");
-    }
 
     /// a LetRec whose body returns the wrong type (Bool
     /// instead of the declared Int) is caught by the new typing rule.
@@ -6024,262 +5954,29 @@ mod tests {
         assert_eq!(synth.params, vec!["z".to_string(), "x".to_string()]);
     }
 
-    /// post-typecheck `lift_letrecs` lifts a deferred
+    // 2026-05-21 operator-routing-eq-ord: the
-    /// LetRec inside a polymorphic enclosing fn into a `Forall`-typed
+    // `lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn`
-    /// synthetic top-level fn, mirroring the enclosing fn's type
+    // test (originally here) relied on the builtin `==` to express
-    /// vars. Property protected:
+    // its `if (== k 0) ...` condition. With `==` deleted from the
-    ///
+    // builtin table the test cannot be reconstructed inside this
-    /// 1. The fast-path desugar lift handles the `KnownType`-only
+    // single-module check env (`eq` from prelude.Eq is not visible
-    ///    case end-to-end (see desugar's
+    // without auto-import). The lift-letrec-under-polymorphic-fn
-    ///    `let_rec_capture_under_polymorphic_enclosing_fn_lifts_to_forall_fn`).
+    // property remains exercised by the workspace e2e tests
-    /// 2. The defer path (some capture is `Term::Let`-bound) goes
+    // `local_rec_let_capture` and siblings, which DO carry the
-    ///    through `lift_letrecs`. This test forces that path by
+    // implicit prelude import.
-    ///    introducing a `Term::Let { z = 7 }` inside the body and
-    ///    capturing `z`. The lifted fn must still be `Forall(a). Fn(...)`,
-    ///    even though the lift happens post-typecheck rather than
-    ///    in desugar.
-    ///
-    /// Without 16b.6, lift_letrecs would have panicked on the
-    /// `Type::Forall` match arm at lift-construction time.
-    #[test]
-    fn lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn() {
-        // fn outer : Forall(a). (a) -> a = \x.
-        //   let z = 7
-        //   in let-rec helper : (Int) -> a = \k. if k == 0 then x else helper(k-1) + z (impossible — types don't match)
-        //
-        // Simpler shape: capture z (Let-bound, Int) in a polymorphic
-        // enclosing fn, with a body that returns x (the polymorphic
-        // capture).
-        //
-        // fn outer : Forall(a). (a) -> a = \x.
-        //   let z = 7
-        //   in let-rec helper : (Int) -> a = \k.
-        //     if k == 0 then x else helper(k - z)
-        //   in helper 1
-        let m = Module {
-            schema: SCHEMA.into(),
-            name: "t".into(),
-            imports: vec![],
-            defs: vec![fn_def(
-                "outer",
-                Type::Forall {
-                    vars: vec!["a".into()],
-                    constraints: vec![],
-                    body: Box::new(Type::Fn {
-                        params: vec![Type::Var { name: "a".into() }],
-                        ret: Box::new(Type::Var { name: "a".into() }),
-                        effects: vec![],
-                        param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
-                    }),
-                },
-                vec!["x"],
-                Term::Let {
-                    name: "z".into(),
-                    value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
-                    body: Box::new(Term::LetRec {
-                        name: "helper".into(),
-                        ty: Type::Fn {
-                            params: vec![Type::int()],
-                            ret: Box::new(Type::Var { name: "a".into() }),
-                            effects: vec![],
-                            param_modes: vec![],
-                            ret_mode: ParamMode::Implicit,
-                        },
-                        params: vec!["k".into()],
-                        body: Box::new(Term::If {
-                            cond: Box::new(Term::App {
-                                callee: Box::new(Term::Var { name: "==".into() }),
-                                args: vec![
-                                    Term::Var { name: "k".into() },
-                                    Term::Lit { lit: Literal::Int { value: 0 } },
-                                ],
-                                tail: false,
-                            }),
-                            then: Box::new(Term::Var { name: "x".into() }),
-                            else_: Box::new(Term::App {
-                                callee: Box::new(Term::Var { name: "helper".into() }),
-                                args: vec![Term::App {
-                                    callee: Box::new(Term::Var { name: "-".into() }),
-                                    args: vec![
-                                        Term::Var { name: "k".into() },
-                                        Term::Var { name: "z".into() },
-                                    ],
-                                    tail: false,
-                                }],
-                                tail: false,
-                            }),
-                        }),
-                        in_term: Box::new(Term::App {
-                            callee: Box::new(Term::Var { name: "helper".into() }),
-                            args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
-                            tail: false,
-                        }),
-                    }),
-                },
-            )],
-        };
-        // Typecheck succeeds.
-        check(&m).expect("typecheck before lift");
-        let desugared = ailang_core::desugar::desugar_module(&m);
-        // After desugar the LetRec should still be present (the
-        // capture set is `{x: KnownType, z: LetBound}` and any
-        // LetBound forces deferral).
-        let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
-        assert_eq!(
-            lifted.defs.len(),
-            2,
-            "expected one synthetic fn appended; got {:?}",
-            lifted.defs.iter().map(|d| d.name()).collect::<Vec<_>>()
-        );
-        let synth = match &lifted.defs[1] {
-            Def::Fn(f) => f,
-            _ => panic!("expected synthetic FnDef"),
-        };
-        assert!(
-            synth.name.starts_with("helper$lr_"),
-            "lifted name `{}` should start with `helper$lr_`",
-            synth.name
-        );
-        // Lifted ty must be Forall(a). Fn(Int, a, Int) -> a.
-        // Original LetRec params: [Int]; captures (BTreeSet order):
-        // x: a then z: Int (alphabetical). Ret: a.
-        match &synth.ty {
-            Type::Forall { vars, constraints: _, body } => {
-                assert_eq!(
-                    vars,
-                    &vec!["a".to_string()],
-                    "Forall vars must mirror enclosing fn's vars; got {:?}",
-                    vars
-                );
-                match body.as_ref() {
-                    Type::Fn { params, ret, .. } => {
-                        assert_eq!(params.len(), 3, "expected k + x + z params");
-                        assert!(
-                            matches!(&params[0], Type::Con { name, .. } if name == "Int"),
-                            "first param: original k:Int; got {:?}",
-                            params[0]
-                        );
-                        // Captures are in BTreeSet order, so x (a-typed) comes before z (Int).
-                        assert!(
-                            matches!(&params[1], Type::Var { name } if name == "a"),
-                            "second param: x: a; got {:?}",
-                            params[1]
-                        );
-                        assert!(
-                            matches!(&params[2], Type::Con { name, .. } if name == "Int"),
-                            "third param: z: Int; got {:?}",
-                            params[2]
-                        );
-                        assert!(
-                            matches!(ret.as_ref(), Type::Var { name } if name == "a"),
-                            "ret: a; got {:?}",
-                            ret
-                        );
-                    }
-                    other => panic!("Forall body must be Fn; got {:?}", other),
-                }
-            }
-            other => panic!(
-                "lifted type must be Forall (mirroring enclosing); got {:?}",
-                other
-            ),
-        }
-        assert_eq!(
-            synth.params,
-            vec!["k".to_string(), "x".to_string(), "z".to_string()]
-        );
-    }
 
-    /// helper that wraps `body` in a fn whose return type is
+    // 2026-05-21 operator-routing-eq-ord: the five `eq_*` tests
-    /// `Bool`, runs `check`, and returns the diagnostics. Used by the
+    // formerly here (`eq_typechecks_at_int` / `_bool` / `_str` /
-    /// polymorphic-`==` typecheck tests below.
+    // `_unit` and `eq_rejects_mixed_int_bool`) pinned the
-    fn check_eq_body_returns_bool(body: Term) -> Vec<Diagnostic> {
+    // polymorphic-`==` builtin shape (`forall a. (a, a) -> Bool`
-        let m = Module {
+    // resolves at any concrete arg pair, type-mismatch on Int+Bool).
-            schema: SCHEMA.into(),
+    // With `==` deleted from the builtin table, the surface
-            name: "t".into(),
+    // equivalent is the class method `eq` dispatched via prelude.Eq
-            imports: vec![],
+    // — which is not visible in this single-module check_module test
-            defs: vec![fn_def(
+    // env (no prelude auto-import). The properties move to
-                "f",
+    // `eq_user_adt_smoke_e2e` (Eq Unit), `eq_demo` (Int/Bool/Str
-                Type::Fn {
+    // dispatch via class-method), and `eq_float_noinstance` (the
-                    params: vec![],
+    // "no instance" rejection for an unsupported type).
-                    ret: Box::new(Type::bool_()),
-                    effects: vec![],
-                    param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
-                },
-                vec![],
-                body,
-            )],
-        };
-        check_module(&m)
-    }
-
-    fn eq_app(a: Term, b: Term) -> Term {
-        Term::App {
-            callee: Box::new(Term::Var { name: "==".into() }),
-            args: vec![a, b],
-            tail: false,
-        }
-    }
-
-    /// `==` accepts Int args (regression — the pre-16e
-    /// behaviour stays identical).
-    #[test]
-    fn eq_typechecks_at_int() {
-        let body = eq_app(
-            Term::Lit { lit: Literal::Int { value: 1 } },
-            Term::Lit { lit: Literal::Int { value: 2 } },
-        );
-        assert!(check_eq_body_returns_bool(body).is_empty());
-    }
-
-    /// `==` accepts Bool args. Pre-16e this was a typecheck
-    /// error because `==` was declared `(Int, Int) -> Bool`.
-    #[test]
-    fn eq_typechecks_at_bool() {
-        let body = eq_app(
-            Term::Lit { lit: Literal::Bool { value: true } },
-            Term::Lit { lit: Literal::Bool { value: false } },
-        );
-        assert!(check_eq_body_returns_bool(body).is_empty());
-    }
-
-    /// `==` accepts Str args. Same story as Bool.
-    #[test]
-    fn eq_typechecks_at_str() {
-        let body = eq_app(
-            Term::Lit { lit: Literal::Str { value: "hi".into() } },
-            Term::Lit { lit: Literal::Str { value: "ho".into() } },
-        );
-        assert!(check_eq_body_returns_bool(body).is_empty());
-    }
-
-    /// `==` accepts Unit args.
-    #[test]
-    fn eq_typechecks_at_unit() {
-        let body = eq_app(
-            Term::Lit { lit: Literal::Unit },
-            Term::Lit { lit: Literal::Unit },
-        );
-        assert!(check_eq_body_returns_bool(body).is_empty());
-    }
-
-    /// `==`'s type still demands the two sides to agree —
-    /// `(== 1 true)` must fail to unify the second arg's `Bool`
-    /// against the metavar already pinned to `Int` by the first.
-    #[test]
-    fn eq_rejects_mixed_int_bool() {
-        let body = eq_app(
-            Term::Lit { lit: Literal::Int { value: 1 } },
-            Term::Lit { lit: Literal::Bool { value: true } },
-        );
-        let diags = check_eq_body_returns_bool(body);
-        assert!(
-            !diags.is_empty(),
-            "(== 1 true) must fail to typecheck; got no diagnostics"
-        );
-    }
 
     /// a `(reuse-as xs 42)` where the body is a literal
     /// (not a `Term::Ctor` and not `Term::Lam`) must emit

crates/ailang-codegen/src/lib.rs

@@ -57,18 +57,17 @@ use synth::{
     fn_sig_from_type, ll_string_literal, llvm_type,
 };
 
-/// Floats iter 4.2 fixup: classify a builtin name as a polymorphic
+/// Classifies a builtin name as a polymorphic arithmetic op (the
-/// arithmetic or comparison op (the set `+`, `-`, `*`, `/`, `%`,
+/// set `+`, `-`, `*`, `/`, `%`). After iter operator-routing-eq-ord.1
-/// `!=`, `<`, `<=`, `>`, `>=`). `==` is NOT in this set — it goes
+/// the comparator names `==` / `!=` / `<` / `<=` / `>` / `>=` are
-/// through `lower_eq` separately. Used by `lower_app` to decide
+/// no longer surface-level identifiers (comparison goes through the
-/// whether to call `builtin_binop_typed`, and by `is_static_callee`
+/// `eq` / `compare` class methods and the `float_*` named fns), so
-/// (in combination with `==` and `not`) to recognise built-in
+/// only the five arithmetic ops live here. Used by `lower_app` to
-/// callees during the global-resolution pass.
+/// decide whether to call `builtin_binop_typed`, and by
-fn is_arithmetic_or_comparison_op(name: &str) -> bool {
+/// `is_static_callee` (in combination with `not`) to recognise
-    matches!(
+/// built-in callees during the global-resolution pass.
-        name,
+fn is_arithmetic_op(name: &str) -> bool {
-        "+" | "-" | "*" | "/" | "%" | "!=" | "<" | "<=" | ">" | ">="
+    matches!(name, "+" | "-" | "*" | "/" | "%")
-    )
 }
 
 /// Failure modes of [`emit_ir`] / [`lower_workspace`].
@@ -1150,6 +1149,51 @@ impl<'a> Emitter<'a> {
         Ok(())
     }
 
+    /// Returns `true` when the codegen should emit the LLVM
+    /// `alwaysinline` attribute on this fn's `define` line. The
+    /// allowlist is the set of primitive-instance bodies emitted by
+    /// `try_emit_primitive_instance_body` whose IR is so trivial
+    /// (one `icmp` / `fcmp` / `call` plus a `ret`) that `-O0` build
+    /// paths pay an unacceptable per-call overhead without inlining,
+    /// while `-O2` would inline these unconditionally anyway. The
+    /// list mirrors the intercept arm set in
+    /// `try_emit_primitive_instance_body` for the equality /
+    /// ordering / Float-comparison primitives. Checked against the
+    /// unmangled fn name; these symbols only live in the prelude
+    /// module so cross-module collisions are not a concern.
+    fn intercept_emit_wants_alwaysinline(symbol: &str) -> bool {
+        if matches!(
+            symbol,
+            "eq__Int" | "eq__Bool" | "eq__Str" | "eq__Unit"
+                | "compare__Int" | "compare__Bool" | "compare__Str"
+                | "float_eq" | "float_ne"
+                | "float_lt" | "float_le"
+                | "float_gt" | "float_ge"
+        ) {
+            return true;
+        }
+        // The polymorphic free helpers `ne` / `lt` / `le` / `gt` /
+        // `ge` mono into per-type bodies. At `_Int` (iter
+        // operator-routing-eq-ord.1 Task 13) they are intercepted as
+        // single direct `icmp` instructions in
+        // `try_emit_primitive_instance_body` — same shape as
+        // `eq__Int`, ie. one `icmp` + one `ret`. At other types
+        // (`_Bool`, `_Str`, user ADTs) they keep their polymorphic
+        // body — a one-arm-deep `match (compare x y) (case LT ... )
+        // (case _ ... )` — which still folds at `-O2` provided the
+        // mono symbol carries `alwaysinline`. Both shapes benefit
+        // from the attribute; the stem-prefix match covers all T the
+        // mono pass produces uniformly so the bench-perf parity with
+        // the pre-milestone arithmetic-comparator emission is
+        // preserved end-to-end.
+        if let Some(stem) = symbol.split("__").next() {
+            if matches!(stem, "ne" | "lt" | "le" | "gt" | "ge") {
+                return true;
+            }
+        }
+        false
+    }
+
     fn emit_fn(&mut self, f: &FnDef) -> Result<()> {
         // also lift `param_modes` out of the fn type. The
         // fn-return Own-param dec emission below consults it to decide
@@ -1241,7 +1285,17 @@ impl<'a> Emitter<'a> {
                 self.ssa_fn_sigs.insert(pssa, fs);
             }
         }
-        sig.push_str(") {\n");
+        if Self::intercept_emit_wants_alwaysinline(&f.name) {
+            // Append the `alwaysinline` attribute between the close-paren
+            // of the parameter list and the `{` opening the body. Symbols
+            // matched here are emitted by `try_emit_primitive_instance_body`;
+            // forcing inlining keeps the single `icmp` / `fcmp` body folded
+            // at every use site under `-O0` (matching the IR shape the
+            // deleted `lower_eq` direct-emit path produced).
+            sig.push_str(") alwaysinline {\n");
+        } else {
+            sig.push_str(") {\n");
+        }
         self.body.push_str(&sig);
         self.start_block("entry");
 
@@ -2124,32 +2178,19 @@ impl<'a> Emitter<'a> {
     }
 
     fn lower_app(&mut self, name: &str, args: &[Term], tail: bool) -> Result<(String, String)> {
-        // `==` is polymorphic (`forall a. (a, a) -> Bool`).
+        // 2026-05-21 operator-routing-eq-ord: the `if name == "=="`
-        // Dispatch on the resolved AIL arg type — the LLVM `ptr` shape
+        // short-circuit that routed through `lower_eq` is gone. `==`
-        // aliases multiple AIL types (Str vs ADT vs Fn), so we cannot
+        // is no longer a surface identifier; the typechecker
-        // dispatch on the LLVM type alone. ADT/Fn equality is rejected
+        // intercepts `(app == …)` as `unknown variable` long before
-        // here with a clear error; `Unit` evaluates both sides for
+        // codegen. Equality dispatch lives in
-        // their side effects then returns constant `i1 1`.
+        // `try_emit_primitive_instance_body` for the primitive Eq
-        if name == "==" {
+        // instance bodies (Int/Bool/Str/Unit), called via the
-            if args.len() != 2 {
+        // class-method `eq` from prelude.Eq.
-                return Err(CodegenError::Internal(
-                    "builtin `==` expected 2 args".into(),
-                ));
-            }
-            let arg_ty = self.synth_arg_type(&args[0])?;
-            let (a, a_ll) = self.lower_term(&args[0])?;
-            let (b, _b_ll) = self.lower_term(&args[1])?;
-            let _ = tail;
-            return self.lower_eq(&arg_ty, &a, &b, &a_ll);
-        }
 
-        // Floats iter 4.2: arithmetic / comparison are now polymorphic
+        // Arithmetic ops `+`/`-`/`*`/`/`/`%` are still polymorphic
-        // over `{Int, Float}`. Resolve the arg type, then dispatch via
+        // over `{Int, Float}`. Resolve the arg type, then dispatch
-        // `builtin_binop_typed`. Same shape as the `==` dispatch above.
+        // via `builtin_binop_typed`.
-        // Comparison ops are matched here in iter 4.2 with Int-only
+        if is_arithmetic_op(name) {
-        // dispatch (preserving pre-iter-4 behaviour) so the workspace
-        // stays green; iter 4.3 adds the Float comparison arms.
-        if is_arithmetic_or_comparison_op(name) {
             if args.len() != 2 {
                 return Err(CodegenError::Internal(format!(
                     "builtin `{name}` expected 2 args"
@@ -2389,6 +2430,21 @@ impl<'a> Emitter<'a> {
             return self.emit_call(self.module_name, name, &sig, args, tail);
         }
 
+        // operator-routing-eq-ord.1: prelude fallback for monomorphic
+        // prelude fns called bare from a non-prelude module (e.g.
+        // `(app float_eq …)`). Mirrors the fallback already in
+        // `is_static_callee` and `resolve_top_level_fn`.
+        if self.module_name != "prelude" {
+            if let Some(sig) = self
+                .module_user_fns
+                .get("prelude")
+                .and_then(|m| m.get(name))
+                .cloned()
+            {
+                return self.emit_call("prelude", name, &sig, args, tail);
+            }
+        }
+
         Err(CodegenError::Internal(format!(
             "unknown callee: `{name}`"
         )))
@@ -2526,7 +2582,7 @@ impl<'a> Emitter<'a> {
     /// `prefix.def`. Locals shadow this — the caller checks for
     /// that first.
     fn is_static_callee(&self, name: &str) -> bool {
-        if is_arithmetic_or_comparison_op(name) || name == "==" || name == "not" {
+        if is_arithmetic_op(name) || name == "not" {
             return true;
         }
         // Floats iter 4.4: new fn-builtins (`neg`, `int_to_float`,
@@ -2554,9 +2610,35 @@ impl<'a> Emitter<'a> {
         // iter 23.4: poly-def arm dropped — post-mono there are no
         // `Type::Forall` defs in `module_user_fns` to begin with, and
         // `module_polymorphic_fns` no longer exists.
-        self.module_user_fns
+        if self
+            .module_user_fns
             .get(self.module_name)
             .is_some_and(|m| m.contains_key(name))
+        {
+            return true;
+        }
+        // operator-routing-eq-ord.1: the typechecker auto-imports
+        // prelude into every non-prelude module so a bare reference
+        // like `(app float_eq …)` typechecks against the prelude's
+        // monomorphic `float_eq` fn. The codegen needs the matching
+        // resolution: if the name is not in the current module but
+        // IS in prelude's monomorphic fn table, treat it as a static
+        // callee — the call lowers to `@ail_prelude_<name>` directly.
+        // Without this fallback, post-mono polymorphic-prelude calls
+        // (e.g. `print`) work because the mono pass synthesises a
+        // mono arm `print__T` into the user's module, but monomorphic
+        // prelude fns (no Forall to instantiate) never get a mirror
+        // arm in user modules and would otherwise fail at codegen
+        // with `unknown variable`.
+        if self.module_name != "prelude"
+            && self
+                .module_user_fns
+                .get("prelude")
+                .is_some_and(|m| m.contains_key(name))
+        {
+            return true;
+        }
+        false
     }
 
     /// resolve `name` to a top-level fn-value, i.e. the address
@@ -2587,15 +2669,32 @@ impl<'a> Emitter<'a> {
             let sig = self.module_user_fns.get(target)?.get(suffix)?.clone();
             return Some((format!("@ail_{target}_{suffix}_clos"), sig));
         }
-        let sig = self
+        if let Some(sig) = self
             .module_user_fns
-            .get(self.module_name)?
+            .get(self.module_name)
-            .get(name)?
+            .and_then(|m| m.get(name))
-            .clone();
+            .cloned()
-        Some((
+        {
-            format!("@ail_{module}_{name}_clos", module = self.module_name),
+            return Some((
-            sig,
+                format!("@ail_{module}_{name}_clos", module = self.module_name),
-        ))
+                sig,
+            ));
+        }
+        // operator-routing-eq-ord.1: fall back to prelude (mirrors
+        // the auto-import the typechecker performs for non-prelude
+        // modules). Needed for monomorphic prelude fns (e.g. `float_eq`)
+        // which have no mono mirror in the user's module.
+        if self.module_name != "prelude" {
+            if let Some(sig) = self
+                .module_user_fns
+                .get("prelude")
+                .and_then(|m| m.get(name))
+                .cloned()
+            {
+                return Some((format!("@ail_prelude_{name}_clos"), sig));
+            }
+        }
+        None
     }
 
     /// resolve a `Term::Var` reference to a const def. Returns
@@ -2794,10 +2893,241 @@ impl<'a> Emitter<'a> {
                 )?;
                 Ok(true)
             }
+            "eq__Int" => {
+                if param_tys != ["i64", "i64"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "eq__Int body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (i64, i64) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = icmp eq i64 {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "eq__Bool" => {
+                if param_tys != ["i1", "i1"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "eq__Bool body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (i1, i1) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = icmp eq i1 {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "eq__Unit" => {
+                // Unit is single-inhabitant: all values compare equal.
+                // The fn signature still carries the operand slots; we
+                // discard them and return true unconditionally.
+                if ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "eq__Unit body intercept: unexpected return type \
+                         ({param_tys:?}) -> {ret_ty} (want -> i1)"
+                    )));
+                }
+                self.body.push_str("  ret i1 1\n");
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "float_eq" => {
+                if param_tys != ["double", "double"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "float_eq body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (double, double) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = fcmp oeq double {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "float_ne" => {
+                // `fcmp une` ("unordered or not-equal"), not `one`,
+                // mirroring float-semantics.md: NaN != NaN must be true.
+                if param_tys != ["double", "double"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "float_ne body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (double, double) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = fcmp une double {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "float_lt" => {
+                if param_tys != ["double", "double"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "float_lt body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (double, double) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = fcmp olt double {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "float_le" => {
+                if param_tys != ["double", "double"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "float_le body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (double, double) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = fcmp ole double {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "float_gt" => {
+                if param_tys != ["double", "double"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "float_gt body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (double, double) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = fcmp ogt double {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            "float_ge" => {
+                if param_tys != ["double", "double"] || ret_ty != "i1" {
+                    return Err(CodegenError::Internal(format!(
+                        "float_ge body intercept: unexpected signature \
+                         ({param_tys:?}) -> {ret_ty} (want (double, double) -> i1)"
+                    )));
+                }
+                let n = self.locals.len();
+                let a_ssa = self.locals[n - 2].1.clone();
+                let b_ssa = self.locals[n - 1].1.clone();
+                let r = self.fresh_ssa();
+                self.body.push_str(&format!(
+                    "  {r} = fcmp oge double {a_ssa}, {b_ssa}\n"
+                ));
+                self.body.push_str(&format!("  ret i1 {r}\n"));
+                self.body.push_str("}\n\n");
+                self.block_terminated = true;
+                Ok(true)
+            }
+            // Ord/Eq Int direct-icmp arms (iter operator-routing-eq-ord.1
+            // Task 13). The polymorphic prelude bodies are
+            // `(match (app compare x y) ...)`; without these intercept
+            // arms, each `lt`-at-Int call site goes through
+            // `compare__Int` → allocate an `Ordering` ctor → match.
+            // At `-O2` even with `alwaysinline` on the helpers, clang
+            // does not always collapse the Ordering allocation across
+            // the helper boundary (observed: +29% bump_s, +47% rc_s
+            // bench_closure_chain regression before this arm shipped).
+            // Direct `icmp slt i64` at the helper body lets clang fold
+            // the comparison to the use site reliably.
+            //
+            // `ne__Int` uses `icmp ne i64` directly, NOT the
+            // `not (eq x y)` indirection — that would re-introduce one
+            // call boundary and one `xor i1 %r, true` per comparison
+            // that contributes no semantic value beyond the direct
+            // `icmp ne`.
+            //
+            // Bool variants (`lt__Bool`, `le__Bool`, etc.) are not
+            // emitted as intercept arms here because no current
+            // bench fixture or example reaches them; the polymorphic
+            // body via `compare__Bool` remains correct, just slightly
+            // slower per call. The next fixture that needs Bool-ordered
+            // perf can extend this family symmetrically.
+            "lt__Int" => self.emit_direct_int_icmp_intercept("lt__Int", "icmp slt i64", param_tys, ret_ty),
+            "le__Int" => self.emit_direct_int_icmp_intercept("le__Int", "icmp sle i64", param_tys, ret_ty),
+            "gt__Int" => self.emit_direct_int_icmp_intercept("gt__Int", "icmp sgt i64", param_tys, ret_ty),
+            "ge__Int" => self.emit_direct_int_icmp_intercept("ge__Int", "icmp sge i64", param_tys, ret_ty),
+            "ne__Int" => self.emit_direct_int_icmp_intercept("ne__Int", "icmp ne i64", param_tys, ret_ty),
             _ => Ok(false),
         }
     }
 
+    /// Emit a direct `<icmp_op> i64` body for the `lt__Int` /
+    /// `le__Int` / `gt__Int` / `ge__Int` / `ne__Int` intercept arms.
+    /// All five share the same shape: pull the two operand SSAs from
+    /// `self.locals` (populated by `emit_fn` before dispatch), emit
+    /// `%r = <icmp_op> %a, %b` and `ret i1 %r`, close the body.
+    /// `icmp_op` is the full instruction-and-operand-type prefix
+    /// (e.g. `"icmp slt i64"`); the operand SSAs are appended.
+    fn emit_direct_int_icmp_intercept(
+        &mut self,
+        fn_name: &str,
+        icmp_op: &str,
+        param_tys: &[String],
+        ret_ty: &str,
+    ) -> Result<bool> {
+        if param_tys != ["i64", "i64"] || ret_ty != "i1" {
+            return Err(CodegenError::Internal(format!(
+                "{fn_name} body intercept: unexpected signature \
+                 ({param_tys:?}) -> {ret_ty} (want (i64, i64) -> i1)"
+            )));
+        }
+        let n = self.locals.len();
+        let a_ssa = self.locals[n - 2].1.clone();
+        let b_ssa = self.locals[n - 1].1.clone();
+        let r = self.fresh_ssa();
+        self.body.push_str(&format!(
+            "  {r} = {icmp_op} {a_ssa}, {b_ssa}\n"
+        ));
+        self.body.push_str(&format!("  ret i1 {r}\n"));
+        self.body.push_str("}\n\n");
+        self.block_terminated = true;
+        Ok(true)
+    }
+
     /// emit one arm of the `compare__T` branch ladder.
     /// Starts a fresh basic block labelled `label`, constructs the
     /// matching `Ordering` ctor (LT / EQ / GT) via `lower_ctor`, and
@@ -2869,99 +3199,16 @@ impl<'a> Emitter<'a> {
         Ok(())
     }
 
-    /// lower a `==` call after the two operands have been
+    // 2026-05-21 operator-routing-eq-ord: `lower_eq` is deleted.
-    /// emitted. Dispatches on the resolved AIL type of the arg side
+    // Equality is no longer a direct-emit codegen path; it flows
-    /// (both sides have the same type after typecheck). The `_a_ll`
+    // through the class method `eq` (prelude.Eq) whose primitive
-    /// hint is the LLVM type the lowering produced for `a`; we use
+    // instance bodies are emitted by
-    /// it as a sanity check against `arg_ty`'s expected LLVM shape.
+    // `try_emit_primitive_instance_body` (Eq Int/Bool/Str/Unit
-    ///
+    // arms, each lowering to a single `icmp` / call /
-    /// Supported:
+    // constant-`i1`-`1` plus the alwaysinline attribute on the
-    /// - `Int` → `icmp eq i64`
+    // generated fn definition). The deleted fn handled Int / Bool /
-    /// - `Bool` → `icmp eq i1`
+    // Str / Unit / Float branches plus the ADT/Fn rejection arms;
-    /// - `Str` → `@strcmp` then `icmp eq i32 0`
+    // none of those code paths are now reachable.
-    /// - `Unit` → constant `i1 true` (both sides already evaluated
-    ///   for any side effects; Unit has a single inhabitant).
-    ///
-    /// Rejected with `CodegenError::Internal` for ADT, `Fn`, and any
-    /// other type — those would need either a structural-equality
-    /// scheme (ADT) or a fn-pointer compare (Fn) that the language
-    /// does not yet specify.
-    fn lower_eq(
-        &mut self,
-        arg_ty: &Type,
-        a: &str,
-        b: &str,
-        _a_ll: &str,
-    ) -> Result<(String, String)> {
-        match arg_ty {
-            Type::Con { name, .. } => match name.as_str() {
-                "Int" => {
-                    let dst = self.fresh_ssa();
-                    self.body.push_str(&format!(
-                        "  {dst} = icmp eq i64 {a}, {b}\n"
-                    ));
-                    Ok((dst, "i1".into()))
-                }
-                "Bool" => {
-                    let dst = self.fresh_ssa();
-                    self.body.push_str(&format!(
-                        "  {dst} = icmp eq i1 {a}, {b}\n"
-                    ));
-                    Ok((dst, "i1".into()))
-                }
-                "Str" => {
-                    // IR-Str pointers now land on the
-                    // `len`-field of the packed-struct slab; @strcmp
-                    // needs the bytes pointer 8 bytes further on.
-                    // Parallel to the `eq__Str` and `compare__Str`
-                    // intercepts in `try_emit_primitive_instance_body`.
-                    let a_bytes = self.fresh_ssa();
-                    let b_bytes = self.fresh_ssa();
-                    self.body.push_str(&format!(
-                        "  {a_bytes} = getelementptr inbounds i8, ptr {a}, i64 8\n"
-                    ));
-                    self.body.push_str(&format!(
-                        "  {b_bytes} = getelementptr inbounds i8, ptr {b}, i64 8\n"
-                    ));
-                    let cmp = self.fresh_ssa();
-                    self.body.push_str(&format!(
-                        "  {cmp} = call i32 @strcmp(ptr {a_bytes}, ptr {b_bytes})\n"
-                    ));
-                    let dst = self.fresh_ssa();
-                    self.body.push_str(&format!(
-                        "  {dst} = icmp eq i32 {cmp}, 0\n"
-                    ));
-                    Ok((dst, "i1".into()))
-                }
-                "Unit" => {
-                    // Both sides have already been evaluated above for
-                    // any side effects; Unit has a single inhabitant,
-                    // so equality is `true` by definition.
-                    let _ = a;
-                    let _ = b;
-                    Ok(("true".into(), "i1".into()))
-                }
-                "Float" => {
-                    let dst = self.fresh_ssa();
-                    self.body.push_str(&format!(
-                        "  {dst} = fcmp oeq double {a}, {b}\n"
-                    ));
-                    Ok((dst, "i1".into()))
-                }
-                other => Err(CodegenError::Internal(format!(
-                    "`==` not supported for type `{other}` \
-                     (ADT and user-defined types lack a structural-equality scheme)"
-                ))),
-            },
-            Type::Fn { .. } => Err(CodegenError::Internal(
-                "`==` not supported for function types (no canonical fn-pointer equality)".into(),
-            )),
-            other => Err(CodegenError::Internal(format!(
-                "`==` not supported for type `{}`",
-                ailang_core::pretty::type_to_string(other)
-            ))),
-        }
-    }
 
     pub(crate) fn fresh_ssa(&mut self) -> String {
         self.counter += 1;
@@ -3327,119 +3574,15 @@ mod tests {
         );
     }
 
-    /// codegen rejects `==` on ADT-typed args with a clear
+    // 2026-05-21 operator-routing-eq-ord: the two
-    /// error. The typechecker accepts the call (the rigid var of
+    // `eq_on_adt_rejected_at_codegen` / `eq_on_fn_rejected_at_codegen`
-    /// `forall a. (a, a) -> Bool` unifies with the ADT type), so the
+    // tests pinned the `lower_eq` direct-emit rejection path for ADT /
-    /// rejection has to happen here. The diagnostic must mention the
+    // Fn args. With `lower_eq` deleted in Task 7 and `==` no longer a
-    /// `==` symbol and the ADT type name.
+    // builtin, the rejection path is gone by structure: `(app eq ADT
-    #[test]
+    // ADT)` is rejected at typecheck as `NoInstance Eq <ADT>` (the
-    fn eq_on_adt_rejected_at_codegen() {
+    // user did not provide an instance), and `(app eq Fn Fn)` is
-        // Tiny ADT `data K = Mk` (nullary).
+    // similarly rejected. Coverage of the ADT no-instance case lives
-        let mk = Term::Ctor {
+    // in `eq_ord_e2e.rs` (negative path on a missing user instance).
-            type_name: "K".into(),
-            ctor: "Mk".into(),
-            args: vec![],
-        };
-        let m = Module {
-            schema: SCHEMA.into(),
-            name: "t".into(),
-            imports: vec![],
-            defs: vec![
-                Def::Type(TypeDef {
-                    name: "K".into(),
-                    vars: vec![],
-                    ctors: vec![Ctor {
-                        name: "Mk".into(),
-                        fields: vec![],
-                    }],
-                    doc: None,
-                    drop_iterative: false,
-                }),
-                Def::Fn(FnDef {
-                    name: "main".into(),
-                    ty: Type::Fn {
-                        params: vec![],
-                        ret: Box::new(Type::unit()),
-                        effects: vec![],
-                        param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
-                    },
-                    params: vec![],
-                    body: Term::Let {
-                        name: "_b".into(),
-                        value: Box::new(Term::App {
-                            callee: Box::new(Term::Var { name: "==".into() }),
-                            args: vec![mk.clone(), mk],
-                            tail: false,
-                        }),
-                        body: Box::new(Term::Lit { lit: Literal::Unit }),
-                    },
-                    suppress: vec![],
-                    doc: None,
-                export: None,
-                }),
-            ],
-        };
-        let err = emit_ir(&m).expect_err(
-            "`==` on ADT must be rejected at codegen; emit_ir succeeded",
-        );
-        let msg = format!("{err:?}");
-        assert!(
-            msg.contains("==") && msg.contains("not supported"),
-            "expected error mentioning `==` not supported; got: {msg}"
-        );
-    }
-
-    /// same negative-path guard for function-typed args.
-    /// `==` on `Fn` is rejected with a "not supported for function
-    /// types" message.
-    #[test]
-    fn eq_on_fn_rejected_at_codegen() {
-        // `let f = main in (== f f)` — `main` is in scope as a fn-value.
-        let m = Module {
-            schema: SCHEMA.into(),
-            name: "t".into(),
-            imports: vec![],
-            defs: vec![Def::Fn(FnDef {
-                name: "main".into(),
-                ty: Type::Fn {
-                    params: vec![],
-                    ret: Box::new(Type::unit()),
-                    effects: vec![],
-                    param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
-                },
-                params: vec![],
-                body: Term::Let {
-                    name: "f".into(),
-                    value: Box::new(Term::Var { name: "main".into() }),
-                    body: Box::new(Term::Let {
-                        name: "_b".into(),
-                        value: Box::new(Term::App {
-                            callee: Box::new(Term::Var { name: "==".into() }),
-                            args: vec![
-                                Term::Var { name: "f".into() },
-                                Term::Var { name: "f".into() },
-                            ],
-                            tail: false,
-                        }),
-                        body: Box::new(Term::Lit { lit: Literal::Unit }),
-                    }),
-                },
-                suppress: vec![],
-                doc: None,
-            export: None,
-            })],
-        };
-        let err = emit_ir(&m).expect_err(
-            "`==` on Fn must be rejected at codegen; emit_ir succeeded",
-        );
-        let msg = format!("{err:?}");
-        assert!(
-            msg.contains("==") && msg.contains("function"),
-            "expected error mentioning `==` and function types; got: {msg}"
-        );
-    }
 
     #[test]
     fn missing_entry_main_is_error() {
@@ -3676,73 +3819,17 @@ mod tests {
         );
     }
 
-    /// Floats iter 4.3 RED: `(< 1.5 2.5)` lowers as `fcmp olt double`;
+    // 2026-05-21 operator-routing-eq-ord: the
-    /// `(!= 1.5 1.5)` lowers as `fcmp UNE double` (NOT `one`); `(== 1.5
+    // `lowers_float_comparison_dispatched` test pinned the direct-emit
-    /// 1.5)` lowers as `fcmp oeq double`. Int regressions still emit
+    // `builtin_binop_typed` comparator arms for `==`/`!=`/`<` over
-    /// `icmp slt i64` / `icmp ne i64` / `icmp eq i64`.
+    // Int and Float. Those arms are deleted in Task 7 (comparison is
-    #[test]
+    // now class-method dispatch for Int/Bool/Str via prelude.Eq/Ord
-    fn lowers_float_comparison_dispatched() {
+    // and named-fn dispatch for Float via float_eq / float_lt / etc.);
-        use ailang_core::ast::*;
+    // the test's premise is gone. Replacement coverage of the new
-        fn fn_def(name: &str, body: Term) -> Def {
+    // IR shape lives in the intercept-arm machinery exercised by
-            Def::Fn(FnDef {
+    // `prelude_eq_int_carries_alwaysinline_attribute_in_emitted_ir`
-                name: name.into(),
+    // (Eq Int → icmp eq + alwaysinline) and indirectly via the
-                ty: Type::Fn {
+    // workspace e2e tests for the Float-named-fn surface.
-                    params: vec![],
-                    ret: Box::new(Type::bool_()),
-                    effects: vec![],
-                    param_modes: vec![],
-                    ret_mode: ParamMode::Implicit,
-                },
-                params: vec![],
-                body,
-                suppress: vec![],
-                doc: None,
-            export: None,
-            })
-        }
-        fn cmp(op: &str, a: Term, b: Term) -> Term {
-            Term::App {
-                callee: Box::new(Term::Var { name: op.into() }),
-                args: vec![a, b],
-                tail: false,
-            }
-        }
-        let f1 = Term::Lit { lit: Literal::Float { bits: 0x3ff8_0000_0000_0000u64 } };
-        let f2 = Term::Lit { lit: Literal::Float { bits: 0x4004_0000_0000_0000u64 } };
-        let i1 = Term::Lit { lit: Literal::Int { value: 1 } };
-        let i2 = Term::Lit { lit: Literal::Int { value: 2 } };
-        let main_def = Def::Fn(FnDef {
-            name: "main".into(),
-            ty: Type::Fn {
-                params: vec![], ret: Box::new(Type::unit()), effects: vec![],
-                param_modes: vec![], ret_mode: ParamMode::Implicit,
-            },
-            params: vec![], body: Term::Lit { lit: Literal::Unit },
-            suppress: vec![], doc: None,
-        export: None,
-        });
-        let m = Module {
-            schema: ailang_core::SCHEMA.to_string(),
-            name: "t".into(),
-            imports: vec![],
-            defs: vec![
-                fn_def("flt_f", cmp("<", f1.clone(), f2.clone())),
-                fn_def("fne_f", cmp("!=", f1.clone(), f1.clone())),
-                fn_def("feq_f", cmp("==", f1.clone(), f1.clone())),
-                fn_def("flt_i", cmp("<", i1.clone(), i2.clone())),
-                fn_def("fne_i", cmp("!=", i1.clone(), i2.clone())),
-                fn_def("feq_i", cmp("==", i1.clone(), i2.clone())),
-                main_def,
-            ],
-        };
-        let ir = emit_ir(&m).unwrap();
-        assert!(ir.contains("fcmp olt double"), "missing `fcmp olt double`: {ir}");
-        assert!(ir.contains("fcmp une double"), "missing `fcmp une double` (note: `une` not `one`): {ir}");
-        assert!(ir.contains("fcmp oeq double"), "missing `fcmp oeq double`: {ir}");
-        assert!(ir.contains("icmp slt i64"), "Int `<` regressed: {ir}");
-        assert!(ir.contains("icmp ne i64"), "Int `!=` regressed: {ir}");
-        assert!(ir.contains("icmp eq i64"), "Int `==` regressed: {ir}");
-    }
 
     /// Floats iter 4.4 RED: four new fn-builtins lower to the spec'd
     /// LLVM ops. `neg` polymorphic dispatches to `sub i64 0, %x` for
@@ -4325,75 +4412,15 @@ mod tests {
         );
     }
 
-    /// the `==` operator on `Str` lowers via an inline
+    // 2026-05-21 operator-routing-eq-ord: the
-    /// `@strcmp` call (separate from the `eq__Str` instance-method
+    // `lower_eq_str_calls_strcmp_with_bytes_pointer` test pinned the
-    /// intercept used by the dictionary path). Both operand pointers
+    // `lower_eq` direct-emit Str path that used an inline `@strcmp`
-    /// must be `+8` GEP'd to land on the bytes pointer before
+    // call. With `lower_eq` deleted in Task 7 and `==` no longer a
-    /// `@strcmp`, symmetric to the `eq__Str` and `compare__Str`
+    // builtin, the only Str-equality path is class-method dispatch
-    /// fixes. Without this, `==` on Str literals reads the 8-byte
+    // via prelude.Eq.eq, which the intercept lowers via the existing
-    /// `len`-field as bytes and never finds the NUL terminator
+    // `eq__Str` arm (call to `@ail_str_eq`, not `@strcmp`). That
-    /// within the expected range, breaking string equality.
+    // path's GEP-+8 / bytes-pointer correctness is pinned by
-    #[test]
+    // `eq_str_mono_symbol_emits_ail_str_eq_call` below.
-    fn lower_eq_str_calls_strcmp_with_bytes_pointer() {
-        let m = Module {
-            schema: SCHEMA.into(),
-            name: "t".into(),
-            imports: vec![],
-            defs: vec![
-                Def::Fn(FnDef {
-                    name: "test".into(),
-                    ty: Type::Fn {
-                        params: vec![],
-                        ret: Box::new(Type::bool_()),
-                        effects: vec![],
-                        param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
-                    },
-                    params: vec![],
-                    body: Term::App {
-                        callee: Box::new(Term::Var { name: "==".into() }),
-                        args: vec![
-                            Term::Lit { lit: Literal::Str { value: "a".into() } },
-                            Term::Lit { lit: Literal::Str { value: "b".into() } },
-                        ],
-                        tail: false,
-                    },
-                    suppress: vec![],
-                    doc: None,
-                export: None,
-                }),
-                Def::Fn(FnDef {
-                    name: "main".into(),
-                    ty: Type::Fn {
-                        params: vec![],
-                        ret: Box::new(Type::unit()),
-                        effects: vec![],
-                        param_modes: vec![],
-                        ret_mode: ParamMode::Implicit,
-                    },
-                    params: vec![],
-                    body: Term::Lit { lit: Literal::Unit },
-                    suppress: vec![],
-                    doc: None,
-                export: None,
-                }),
-            ],
-        };
-        let ir = emit_ir(&m).unwrap();
-        let body_idx = ir.find("define i1 @ail_t_test").expect("test body");
-        let body = &ir[body_idx..];
-        let cmp_idx = body.find("@strcmp(").expect("@strcmp call present");
-        let before_cmp = &body[..cmp_idx];
-        let gep_count = before_cmp.matches("getelementptr inbounds i8, ptr ").count();
-        assert_eq!(
-            gep_count, 2,
-            "expected 2 +8 GEPs before @strcmp (one per operand); ir body was:\n{body}"
-        );
-        assert!(
-            before_cmp.matches(", i64 8").count() >= 2,
-            "expected both GEPs to be `, i64 8`; ir body was:\n{body}"
-        );
-    }
 
     /// a `Term::App` calling `int_to_str` lowers to
     /// `call ptr @ailang_int_to_str(i64 %a)`. Pins the new builtin's

crates/ailang-codegen/src/synth.rs

@@ -79,20 +79,9 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
             ret_mode: ParamMode::Implicit,
         }),
     };
-    let poly_a_a_to_bool = || Type::Forall {
+    // 2026-05-21 operator-routing-eq-ord: `poly_a_a_to_bool` was
-        vars: vec!["a".into()],
+    // shared by the six comparator builtins. With those names
-        constraints: vec![],
+    // deleted from the surface, the helper is dead.
-        body: Box::new(Type::Fn {
-            params: vec![
-                Type::Var { name: "a".into() },
-                Type::Var { name: "a".into() },
-            ],
-            ret: Box::new(Type::bool_()),
-            effects: vec![],
-            param_modes: vec![],
-            ret_mode: ParamMode::Implicit,
-        }),
-    };
     let int_int_int = || Type::Fn {
         params: vec![Type::int(), Type::int()],
         ret: Box::new(Type::int()),
@@ -103,26 +92,13 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
     Some(match name {
         "+" | "-" | "*" | "/" => poly_a_a_to_a(),
         "%" => int_int_int(),
-        "!=" | "<" | "<=" | ">" | ">=" => poly_a_a_to_bool(),
+        // 2026-05-21 operator-routing-eq-ord: the six comparator
-        // `==` is polymorphic — `forall a. (a, a) -> Bool`.
+        // names (`==` / `!=` / `<` / `<=` / `>` / `>=`) are no
-        // The mono pipeline asks `synth_arg_type` for the actual arg
+        // longer surface identifiers. Equality / ordering route
-        // types at the call site; `lower_app` then dispatches to the
+        // through the class methods `eq` / `compare` (prelude.Eq /
-        // right LLVM instruction (icmp eq i64 / i1, @strcmp, or
+        // Ord); Float comparison routes through the named fns
-        // constant i1 1) on those resolved types.
+        // `float_eq` / `float_lt` / etc. Neither path needs an
-        "==" => Type::Forall {
+        // entry in this codegen-side mirror table.
-            vars: vec!["a".into()],
-            constraints: vec![],
-            body: Box::new(Type::Fn {
-                params: vec![
-                    Type::Var { name: "a".into() },
-                    Type::Var { name: "a".into() },
-                ],
-                ret: Box::new(Type::bool_()),
-                effects: vec![],
-                param_modes: vec![],
-                ret_mode: ParamMode::Implicit,
-            }),
-        },
         "not" => Type::Fn {
             params: vec![Type::bool_()],
             ret: Box::new(Type::bool_()),
@@ -237,10 +213,14 @@ pub(crate) fn builtin_effect_op_ret(op: &str) -> Option<Type> {
 /// longer has to second-guess which arm fired.
 ///
 /// Comparison-op Int arms are kept here in iter 4.2 to preserve
-/// the no-regression invariant — pre-iter-4 codegen routed
+/// `builtin_binop_typed` is now arithmetic-only. Comparators
-/// `<`/`<=`/`>`/`>=`/`!=` through the same Int-only `builtin_binop`
+/// (`==` / `!=` / `<` / `<=` / `>` / `>=`) were removed in iter
-/// table. Iter 4.3 adds the Float arms (`("fcmp olt", "double", "i1")`
+/// operator-routing-eq-ord.1 — surface comparison routes through
-/// and friends).
+/// the prelude.Eq / Ord class-method dispatch, with primitive
+/// instance bodies emitted via `try_emit_primitive_instance_body`
+/// in lib.rs (Eq Int / Bool / Str / Unit → `icmp`; Ord Int / Bool
+/// / Str → `icmp` + Ordering ctor; float_eq / float_ne / float_lt
+/// / float_le / float_gt / float_ge → `fcmp`).
 pub(crate) fn builtin_binop_typed(
     name: &str,
     arg_ty: &Type,
@@ -257,23 +237,6 @@ pub(crate) fn builtin_binop_typed(
         ("/", true, _) => Some(("sdiv", "i64", "i64")),
         ("/", _, true) => Some(("fdiv", "double", "double")),
         ("%", true, _) => Some(("srem", "i64", "i64")),
-        // Comparison ops: operand types differ, result is always `i1`.
-        // Int-arm comparisons preserved from pre-iter-4 `builtin_binop`;
-        // Float arms land in iter 4.3.
-        ("!=", 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")),
-        // Float comparison arms (Floats iter 4.3). Note: `!=` Float
-        // uses `fcmp une` ("unordered or not equal") — NOT `one`
-        // ("ordered and not equal"), which would return `false` for
-        // `nan != nan` and violate IEEE / spec A5.
-        ("!=", _, 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,
     }
 }

crates/ailang-core/src/desugar.rs

@@ -1087,15 +1087,20 @@ fn is_flat(p: &Pattern) -> bool {
 }
 
 /// Build an equality-test term for a lit pattern. The shape is
-/// `(app == scrutinee lit_term)` for Int/Bool/Str. Unit literals are
+/// Builds the equality-test AST node for a literal pattern. Lowers
-/// degenerate — every Unit value is equal — so an emitted `true` literal
+/// `(pat-lit <lit>)` to `(if (eq sv <lit>) <body> <fall_k>)`. The
-/// stands in.
+/// emitted `eq` resolves via prelude.Eq's class-method dispatch
+/// (per design/contracts/method-dispatch.md) — Int/Bool/Str/Unit
+/// patterns all route through the corresponding primitive instance.
 ///
-/// Note: as of Iter 16c, the `==` builtin is typed `(Int, Int) -> Bool`
+/// Float-Literal patterns are hard-rejected at typecheck
-/// only. Bool- and Str-lit patterns therefore reach typecheck as a
+/// (`CheckError::FloatPatternNotAllowed`, per
-/// type error rather than a clean rewrite. They remain authorable at the
+/// design/contracts/float-semantics.md) before this fn is reached,
-/// AST level (the desugar never refuses) but are not yet usable end-to-
+/// so the `eq`-dispatch never encounters Float at runtime; the
-/// end. Lifting that gate is bound to extending `==` to those types.
+/// Float arm of the match below remains for AST-level totality.
+///
+/// Unit literals are degenerate — every Unit value is equal — so an
+/// emitted `true` literal stands in (no `eq` call needed).
 fn build_eq(scrutinee: Term, lit: &Literal) -> Term {
     match lit {
         Literal::Unit => Term::Lit {
@@ -1106,7 +1111,7 @@ fn build_eq(scrutinee: Term, lit: &Literal) -> Term {
         | Literal::Str { .. }
         | Literal::Float { .. } => Term::App {
             callee: Box::new(Term::Var {
-                name: "==".to_string(),
+                name: "eq".to_string(),
             }),
             args: vec![scrutinee, Term::Lit { lit: lit.clone() }],
             tail: false,
@@ -2409,6 +2414,12 @@ mod tests {
                 ret_mode: ParamMode::Implicit,
             },
             params: vec!["k".into()],
+            // 2026-05-21 operator-routing-eq-ord: keep `==` here (vs
+            // migrating to `eq`) because this AST literal sits in an
+            // in-source mod test for desugar with no prelude
+            // injection; `eq` would be unbound. After Task 7 deletes
+            // `==`, this test gets deleted as obsolete; the desugar
+            // shape is exercised end-to-end via the workspace flow.
             body: Box::new(Term::If {
                 cond: Box::new(Term::App {
                     callee: Box::new(Term::Var { name: "==".into() }),

crates/ailang-core/tests/hash_pin.rs

@@ -73,6 +73,12 @@ fn hash_changes_with_content() {
 /// definition. Recorded hashes were captured from on-disk modules
 /// before the schema extension; if this fires, a
 /// `skip_serializing_if` is missing or wrong.
+///
+/// 2026-05-21 operator-routing-eq-ord re-pinned (prior:
+/// db33f57cb329935e): sum.ail's body migrates `(app == n 0)` →
+/// `(app eq n 0)` per the operator-name deletion; hash follows the
+/// content change. Pin remains a schema-extension guard against
+/// future drift from the new content baseline.
 #[test]
 fn iter13a_schema_extension_preserves_pre_13a_hashes() {
     let examples = examples_dir();
@@ -80,7 +86,7 @@ fn iter13a_schema_extension_preserves_pre_13a_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "db33f57cb329935e");
+    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
         .expect("examples/list.ail loads");
@@ -102,7 +108,7 @@ fn loop_recur_schema_extension_preserves_pre_loop_recur_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "db33f57cb329935e");
+    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
         .expect("examples/list.ail loads");
@@ -156,7 +162,7 @@ fn iter19b_schema_extension_preserves_pre_19b_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "db33f57cb329935e");
+    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
 }
 
 /// adding `Def::Class` and `Def::Instance` must
@@ -171,7 +177,7 @@ fn iter22b1_schema_extension_preserves_pre_22b_hashes() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "db33f57cb329935e");
+    assert_eq!(def_hash(sum_def), "25343a2e5927a257");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))
         .expect("examples/list.ail loads");
@@ -277,7 +283,7 @@ fn ct4_unmigrated_fixtures_remain_bit_identical() {
     let sum_mod = ailang_surface::load_module(&examples.join("sum.ail"))
         .expect("examples/sum.ail loads");
     let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap();
-    assert_eq!(def_hash(sum_def), "db33f57cb329935e",
+    assert_eq!(def_hash(sum_def), "25343a2e5927a257",
         "sum.sum hash drifted across canonical-form tightening — unexpected");
 
     let list_mod = ailang_surface::load_module(&examples.join("list.ail"))

crates/ailang-prose/src/lib.rs

@@ -538,28 +538,30 @@ fn write_type(out: &mut String, t: &Type, owning_module: &str) {
 
 // ---- terms ----------------------------------------------------------------
 
-// Precedence ladder for paren elision (Iter 20b, Polish 2). Higher = binds
+// Precedence ladder for paren elision. Higher = binds tighter; an
-// tighter; an atomic form (var / literal / call / ctor / lambda / match /
+// atomic form (var / literal / call / ctor / lambda / match / if /
-// if / let / do / clone / reuse-as) sits at PREC_ATOMIC and never needs
+// let / do / clone / reuse-as) sits at PREC_ATOMIC and never needs
 // to wrap itself. PREC_NONE is the top-level (caller asks for no
-// outer parens).
+// outer parens). After iter operator-routing-eq-ord.1 the only
+// infix-rendered ops are the arithmetic builtins; comparison /
+// equality go through the class-method `eq` / `compare` / `lt` /
+// etc. and render as fn calls.
 const PREC_NONE: u8 = 0;
-const PREC_EQ: u8 = 1; //  == !=          (non-assoc)
+const PREC_ADD: u8 = 1; // +  -           (left-assoc)
-const PREC_REL: u8 = 2; // <  <= >  >=    (non-assoc)
+const PREC_MUL: u8 = 2; // *  /  %        (left-assoc)
-const PREC_ADD: u8 = 3; // +  -           (left-assoc)
+const PREC_ATOMIC: u8 = 3;
-const PREC_MUL: u8 = 4; // *  /  %        (left-assoc)
-const PREC_ATOMIC: u8 = 5;
 
 /// Precedence + associativity of a canonical binary op name. Returns
-/// `None` for any non-canonical name. Three-tuple: (level, left_assoc).
+/// `None` for any non-canonical name. Two-tuple: (level, left_assoc).
-/// Non-assoc ops report `left_assoc = false`; for them we additionally
+/// After iter operator-routing-eq-ord.1, only the five arithmetic
-/// bump both sides to `level + 1` so same-level chains always wrap.
+/// ops `+` / `-` / `*` / `/` / `%` are infix-rendered; the six
+/// comparator names (`==` / `!=` / `<` / `<=` / `>` / `>=`) are no
+/// longer surface identifiers, so their AST forms (only reachable
+/// via error paths) fall through to the standard fn-call rendering.
 fn binop_info(name: &str) -> Option<(u8, bool)> {
     Some(match name {
         "*" | "/" | "%" => (PREC_MUL, true),
         "+" | "-" => (PREC_ADD, true),
-        "<" | "<=" | ">" | ">=" => (PREC_REL, false),
-        "==" | "!=" => (PREC_EQ, false),
         _ => return None,
     })
 }
@@ -1948,8 +1950,10 @@ mod tests {
 
     #[test]
     fn binop_renders_infix_for_every_canonical_op() {
-        // All 11 operators must collapse to `lhs op rhs` shape.
+        // 2026-05-21 operator-routing-eq-ord: the six comparator
-        let ops = ["+", "-", "*", "/", "%", "==", "!=", "<", "<=", ">", ">="];
+        // names are no longer surface identifiers; only the five
+        // arithmetic ops infix-render.
+        let ops = ["+", "-", "*", "/", "%"];
         for op in ops {
             let t = binop(op, ivar("a"), ivar("b"));
             let expected = format!("a {op} b");
@@ -2013,21 +2017,21 @@ mod tests {
         assert_eq!(render_term(&t), "a + (b + c)");
     }
 
-    #[test]
+    // 2026-05-21 operator-routing-eq-ord: removed
-    fn non_assoc_same_level_keeps_parens_on_both_sides() {
+    // `non_assoc_same_level_keeps_parens_on_both_sides` —
-        // `a < b < c` is forbidden in Rust; we keep parens regardless of
+    // `< < <` chains were the only sub-case where non-assoc
-        // which side carries the same-level sub.
+    // precedence mattered; with `<` no longer a surface op, the
-        let t = binop("<", binop("<", ivar("a"), ivar("b")), ivar("c"));
+    // remaining (arithmetic) infix ops are all left-assoc so the
-        assert_eq!(render_term(&t), "(a < b) < c");
+    // non-assoc path is no longer reachable from any AST a user
-        let t2 = binop("<", ivar("a"), binop("<", ivar("b"), ivar("c")));
+    // could produce.
-        assert_eq!(render_term(&t2), "a < (b < c)");
-    }
 
     #[test]
     fn atomic_subexpr_never_wraps() {
-        // A var on either side of any op never picks up parens.
+        // A var on either side of an arithmetic op never picks up
-        let t = binop("==", ivar("n"), Term::Lit { lit: Literal::Int { value: 0 } });
+        // parens. (Pre-eq-ord this fixture used `==`; with `==` no
-        assert_eq!(render_term(&t), "n == 0");
+        // longer infix-rendered, the same property holds for `+`.)
+        let t = binop("+", ivar("n"), Term::Lit { lit: Literal::Int { value: 0 } });
+        assert_eq!(render_term(&t), "n + 0");
     }
 
     #[test]
@@ -2057,15 +2061,17 @@ mod tests {
 
     #[test]
     fn not_of_binop_keeps_parens() {
-        // `not(a == b)` → `!(a == b)`. The arg's prec is 1; the unary
+        // `not(a + b)` → `!(a + b)`. The arg's prec is below the
-        // floor is PREC_ATOMIC=5; 1 < 5 means wrap.
+        // unary floor `PREC_ATOMIC`, so the wrap stays. (Pre-eq-ord
-        let inner = binop("==", ivar("a"), ivar("b"));
+        // this exercised `==`; with `==` no longer infix-rendered,
+        // `+` is the parallel case for arithmetic.)
+        let inner = binop("+", ivar("a"), ivar("b"));
         let t = Term::App {
             callee: Box::new(ivar("not")),
             args: vec![inner],
             tail: false,
         };
-        assert_eq!(render_term(&t), "!(a == b)");
+        assert_eq!(render_term(&t), "!(a + b)");
     }
 
     #[test]

crates/ailang-surface/tests/prelude_module_hash_pin.rs

@@ -12,8 +12,12 @@ fn prelude_parse_yields_canonical_hash() {
     let h = module_hash(&m);
     // The expected hex updates intentionally on prelude-content
     // changes; record the why in the commit body.
+    // 2026-05-21 operator-routing-eq-ord re-pinned (prior:
+    // 3abe0d3fa3c11c99): Eq Int/Bool/Str bodies flip to placeholder
+    // `false`; Eq Unit added; six float_* fns added; class-Eq doc
+    // rewritten away from the "P2 follow-up" comment.
     assert_eq!(
-        h, "3abe0d3fa3c11c99",
+        h, "6d0577ff0d4e50ac",
         "prelude module hash drifted; if intentional, capture the new \
          hex below + record the why in the commit body."
     );

design/contracts/float-semantics.md

@@ -7,28 +7,35 @@ no `f32` variant. The runtime / codegen contract:
 
 **Guaranteed:**
 
-- Every individual builtin (`+`/`-`/`*`/`/`/`neg`/`<`/`==`/...) lowers
+- Every individual arithmetic builtin (`+`/`-`/`*`/`/`/`neg`) lowers
-  to a single LLVM IR instruction on the Float arm:
+  to a single LLVM IR instruction on the Float arm: `fadd / fsub /
-  `fadd/fsub/fmul/fdiv double`, `fneg double`, `fcmp olt/ole/ogt/oge
+  fmul / fdiv double`, `fneg double`. Float comparison goes through
-  double`, `fcmp oeq double`, `fcmp une double` (for `!=`). On a
+  the named prelude fns `float_eq` / `float_ne` / `float_lt` /
-  fixed `(target triple, LLVM version)` pair, the bit pattern of
+  `float_le` / `float_gt` / `float_ge` (Float has no Eq/Ord instance
-  the result of any single op is reproducible.
+  — see [Prelude (built-in) classes](prelude-classes.md)); each fn
+  lowers to a single `fcmp` instruction (`oeq` / `une` / `olt` /
+  `ole` / `ogt` / `oge` respectively) via the codegen intercept
+  `try_emit_primitive_instance_body`, with the `alwaysinline`
+  attribute on the generated `define` so the call folds to one
+  instruction at every use site. On a fixed `(target triple, LLVM
+  version)` pair, the bit pattern of the result of any single op is
+  reproducible.
 - NaN and ±Inf propagate per IEEE 754 — no silent collapse to zero,
   no trap. Arithmetic on a NaN operand produces NaN; division by
   zero produces ±Inf; `0.0 / 0.0` produces NaN.
 - `-0.0` and `+0.0` are distinct bit patterns at the canonical-JSON
   hash level (`{"bits":"0000000000000000",...}` vs
   `{"bits":"8000000000000000",...}` — distinct `def_hash`s) but
-  compare equal via `==` per IEEE (`fcmp oeq double` returns true
+  compare equal via `float_eq` per IEEE (`fcmp oeq double` returns
-  for `+0 == -0`). This asymmetry is the correct IEEE behaviour;
+  true for `+0 == -0`). This asymmetry is the correct IEEE
-  it does mean `def_hash`-equality is finer than `==`-equality on
+  behaviour; it does mean `def_hash`-equality is finer than
-  Float.
+  `float_eq` on Float.
-- `==` returns `false` whenever either operand is NaN
+- `float_eq` returns `false` whenever either operand is NaN
   (`fcmp oeq` is the ordered-equal predicate; ordered = both
   operands non-NaN).
-- `!=` returns `true` whenever either operand is NaN (`fcmp une`
+- `float_ne` returns `true` whenever either operand is NaN
-  is the unordered-or-not-equal predicate). This matches Rust
+  (`fcmp une` is the unordered-or-not-equal predicate). This matches
-  `f64::ne` and IEEE-`!=` exactly.
+  Rust `f64::ne` and IEEE-`!=` exactly.
 - `is_nan` (`fcmp uno double %x, %x`) returns `true` iff `x` is
   NaN. Bit-pattern-based NaN detection without dependence on the
   payload bits.
@@ -95,8 +102,9 @@ This bits-hex encoding is what keeps Floats inside the
 [Data model](data-model.md) for the pattern schema) is hard-
 rejected at typecheck (`CheckError::FloatPatternNotAllowed`). IEEE
 semantics make Float patterns semantically dubious — NaN never
-matches via IEEE-`==`, and bit-exact equality is rarely what an
+matches via `float_eq` (its `fcmp oeq` lowering is `false` for
-LLM-author wants. Use ordering operators (`<`, `>`, ...) and
+NaN), and bit-exact equality is rarely what an LLM-author wants.
+Use the explicit comparison fns (`float_lt`, `float_gt`, ...) and
 `is_nan` to discriminate Floats.
 
 `float_to_str` (Float → Str) and `int_to_str` (Int → Str) are

design/contracts/prelude-classes.md

@@ -3,14 +3,34 @@
 ## Prelude (built-in) classes
 
 The prelude ships the `Ordering` ADT, the `Eq` and `Ord`
-[classes](typeclasses.md), primitive `Eq Int/Bool/Str` and
+[classes](typeclasses.md), primitive `Eq Int/Bool/Str/Unit` and
 `Ord Int/Bool/Str` instances, and the five polymorphic free-fn
-helpers `ne`/`lt`/`le`/`gt`/`ge`. Float has neither `Eq` nor `Ord`
+helpers `ne`/`lt`/`le`/`gt`/`ge`. The primitive `Eq` / `Ord`
-instance per [Float semantics](float-semantics.md); a polymorphic
+instance bodies are placeholder lambdas in `examples/prelude.ail`;
-helper invoked at Float fires `NoInstance` at typecheck with a
+the codegen intercept `try_emit_primitive_instance_body` overrides
-Float-aware diagnostic cross-referencing this section. The lookup
+them with single-instruction bodies (`icmp eq i64` for `eq__Int`,
-machinery that turns a `show x` call site into the right monomorphic
+`icmp eq i1` for `eq__Bool`, `@ail_str_eq` for `eq__Str`,
-instance is documented in [method dispatch](method-dispatch.md).
+`ret i1 1` for `eq__Unit`; a three-way `icmp` ladder constructing
+`LT`/`EQ`/`GT` for `compare__T`) and attaches `alwaysinline` so
+the call folds to the single instruction at every use site.
+
+Float has neither `Eq` nor `Ord` instance per [Float semantics](
+float-semantics.md); a polymorphic helper invoked at Float fires
+`NoInstance` at typecheck with a Float-aware diagnostic that names
+the explicit `float_eq` / `float_lt` alternatives and
+cross-references this section. The lookup machinery that turns a
+`show x` call site into the right monomorphic instance is
+documented in [method dispatch](method-dispatch.md).
+
+Float comparison is a separate surface: the six monomorphic prelude
+fns `float_eq` / `float_ne` / `float_lt` / `float_le` / `float_gt`
+/ `float_ge` each carry the type `(Float, Float) -> Bool` without
+a class constraint. They lower via the same intercept machinery as
+the primitive `Eq` instances (single `fcmp` instruction with the
+matching predicate `oeq` / `une` / `olt` / `ole` / `ogt` / `oge`,
+plus `alwaysinline`). They replace what would otherwise be a
+polymorphic `==` / `<` on Float — Float gets full comparability
+via explicit named fns, not via an implicit class instance.
 
 The prelude ships `class Show a where show : (a borrow) -> Str` and
 primitive `Show Int`, `Show Bool`, `Show Str`, `Show Float`

design/contracts/scope-boundaries.md

@@ -39,9 +39,7 @@ What **is** supported (and used as the smoke test for the pipeline):
 - **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type
   `forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
   `%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
-  Float deferred); ordering operators and `!=` (`!=`, `<`, `<=`,
+  Float deferred); polymorphic `neg : forall a. (a) -> a`
-  `>`, `>=`) of type `forall a. (a, a) -> Bool` (codegen-restricted
-  to `{Int, Float}`); polymorphic `neg : forall a. (a) -> a`
   (codegen-restricted to `{Int, Float}`; Float arm uses LLVM
   `fneg double` for correct `-0.0` handling); logical
   `not : (Bool) -> Bool`; conversions
@@ -55,25 +53,28 @@ What **is** supported (and used as the smoke test for the pipeline):
   `fcmp uno`); Float bit-pattern constants `nan : Float`,
   `inf : Float`, `neg_inf : Float` (resolved as bare values, lower
   to direct hex-float `double` SSA constants at use site); the IO
-  effect op `io/print_str`; **`==` : forall a.
+  effect op `io/print_str`; and **`__unreachable__ : forall a. a`**.
-  (a, a) -> Bool**; and **`__unreachable__ : forall a. a`**.
+  - **Equality + ordering** are not builtins. The class method
-  - **`==` is polymorphic.** The typechecker accepts
+    `eq` (`prelude.Eq`) dispatches via the per-type Eq instance;
-    `==` at any type whose two sides agree (the rigid `a` of the
+    the class method `compare` (`prelude.Ord`) dispatches via the
-    `Forall` is unified by HM at the use site). Codegen
+    per-type Ord instance, returning a three-ctor `Ordering` ADT
-    monomorphises and dispatches on the resolved AIL arg type:
+    (`LT` / `EQ` / `GT`). The five free helpers `ne` / `lt` /
-    `Int` → `icmp eq i64`; `Bool` → `icmp eq i1`;
+    `le` / `gt` / `ge` are defined in the prelude in terms of
-    `Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0`
+    `eq` / `compare`. The primitive Eq/Ord instance bodies are
-    (`@strcmp` is declared in the LLVM IR header alongside
+    emitted by the codegen intercept
-    `@printf` / `@ailang_rc_alloc`); `Unit` → constant `i1 true`
+    `try_emit_primitive_instance_body`: Eq Int → `icmp eq i64`,
-    (Unit has a single inhabitant; both sides are still
+    Eq Bool → `icmp eq i1`, Eq Str → `call @ail_str_eq(...)`,
-    evaluated for any side effects); `Float` → `fcmp oeq double`.
+    Eq Unit → `ret i1 1`, Ord Int / Bool / Str → three-way
-    ADT and `Fn` arg types are rejected at codegen with a
+    `icmp slt` / `icmp eq` ladder constructing the `Ordering`
-    `CodegenError::Internal` mentioning `==` and the offending
+    ctor; every primitive instance body carries the
-    type — neither has a canonical structural-equality scheme
+    `alwaysinline` attribute so the call folds at every use site.
-    yet, and the language deliberately does not silently elide
+    Float has no Eq / Ord instance (see
-    the check. **`!=` for Float uses `fcmp UNE double` (NOT
+    [Float semantics](float-semantics.md)); explicit comparison
-    `one`)** — `one` is "ordered and not equal" and would return
+    is via the named fns `float_eq` / `float_ne` / `float_lt` /
-    false for `nan != nan`, violating IEEE-`!=`.
+    `float_le` / `float_gt` / `float_ge`, each lowering to a
+    single `fcmp` with the matching predicate. `float_ne` uses
+    `fcmp une double` (NOT `one`) so `nan != nan` returns `true`
+    per IEEE.
   - **`__unreachable__`** is a polymorphic bottom value: a use of
     `__unreachable__` typechecks against any expected type at
     the use site and codegens to the LLVM `unreachable`
@@ -88,15 +89,19 @@ What **is** supported (and used as the smoke test for the pipeline):
 - **ADTs + pattern matching.** Sub-patterns of a Ctor pattern may be `Var`, `Wild`,
   another `Ctor`, or a literal. The desugar pass flattens
   nested Ctor patterns into a chain of let + match and rewrites every
-  `Pattern::Lit` (top-level or sub-) to a `Term::If` on `==` before
+  `Pattern::Lit` (top-level or sub-) to a `Term::If` on `eq` (the
-  typecheck/codegen — see [desugar](../../crates/ailang-core/src/desugar.rs) and [Pipeline](../models/pipeline.md).
+  class method `prelude.Eq.eq`) before typecheck/codegen — see
+  [desugar](../../crates/ailang-core/src/desugar.rs) and
+  [Pipeline](../models/pipeline.md).
 - Literal patterns at top level and inside Ctor sub-patterns (via desugar).
   `(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both
-  parse and lower; the rewrite is to `Term::If { cond = (== sv lit) }`,
+  parse and lower; the rewrite is to `Term::If { cond = (eq sv lit) }`,
-  so any literal kind whose `==` is supported is authorable. With `==`
+  so any literal kind whose `eq` dispatch resolves to a known
-  polymorphic over `Int`/`Bool`/`Str`/`Unit`, that
+  primitive Eq instance is authorable. The primitive instances
-  covers every lit kind the AST ships — including `(pat-lit "hi")`
+  cover `Int` / `Bool` / `Str` / `Unit`; `Float` lit-patterns are
-  over a `Str` scrutinee, exercised by `examples/eq_demo.ail.json`.
+  hard-rejected at typecheck (`CheckError::FloatPatternNotAllowed`,
+  see [float-semantics](float-semantics.md)). `(pat-lit "hi")` over
+  a `Str` scrutinee is exercised by `examples/eq_demo.ail.json`.
 - **Imports + qualified cross-module references** via dotted names.
   Extends to **types and constructors**: a foreign
   module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as

design/contracts/str-abi.md

@@ -37,11 +37,18 @@ directly; values of other primitive types route through the
 polymorphic `print` helper (see [prelude classes](prelude-classes.md)),
 which feeds the heap-Str result of `show x` into `io/print_str`.
 
-`==`, `<`, `<=`, `>`, `>=` REMAIN primitive operators. Class methods
+Equality on `Str` dispatches via `prelude.Eq.eq` (Str instance,
-are accessed by name (`eq x y`, `lt x y`, …), not via these
+lowered by `try_emit_primitive_instance_body::eq__Str` to a call
-operators.
+into `@ail_str_eq` with the `alwaysinline` attribute). Ordering on
+`Str` dispatches via `prelude.Ord.compare` (Str instance, lowered
+by `try_emit_primitive_instance_body::compare__Str` to a call into
+`@ail_str_compare` then a three-way branch ladder constructing
+`LT`/`EQ`/`GT`). The polymorphic helpers `ne` / `lt` / `le` / `gt`
+/ `ge` resolve via the class layer on top of `eq` / `compare`.
+There are no primitive operator names `==` / `<` / `!=` / etc. in
+the language.
 
-Arithmetic operators (`+`, `-`, `*`, `/`) stay primitive and
+Arithmetic operators (`+`, `-`, `*`, `/`, `%`) stay primitive and
 per-type.
 
 **Str ABI.** A `Str` is a pointer to a structure with `i64 len` at

design/models/authoring-surface.md

@@ -55,12 +55,15 @@ Every other maximal token is classified post-hoc:
 - `"`-delimited run → string atom.
 - Otherwise → ident.
 
-Consequence: operators like `+`, `==`, `<=`, `**`, qualified
+Consequence: arithmetic operators like `+` / `-` / `*` / `/` / `%`,
-names like `io/print_str`, and cross-module references like
+qualified names like `io/print_str`, and cross-module references
-`std_list.map` are all single ident tokens with no special lex
+like `std_list.map` are all single ident tokens with no special
-rule. The only reserved tokens are `(`, `)`, and whitespace.
+lex rule. The only reserved tokens are `(`, `)`, and whitespace.
 Bool literals (`true`, `false`) and unit (`(lit-unit)`) are
-disambiguated by parser context, not by lex.
+disambiguated by parser context, not by lex. Comparison and
+equality are class methods (`eq` / `compare`) and named fns
+(`float_eq` / `float_lt` / etc.), not operators — see
+[Prelude classes](../contracts/prelude-classes.md).
 
 Every AST node form has a unique head keyword (`module`, `data`,
 `fn`, `forall`, `fn-type`, `con`, `var`, `app`, `lam`, `match`,

examples/bench_closure_chain.ail

@@ -43,7 +43,7 @@
         (ret (con Int))))
     (params i acc)
     (body
-      (if (app < i 0)
+      (if (app lt i 0)
         acc
         (let-rec helper
           (params x)

examples/bench_compute_collatz.ail

@@ -31,9 +31,9 @@
         (ret (con Int))))
     (params n acc)
     (body
-      (if (app == n 1)
+      (if (app eq n 1)
         acc
-        (if (app == (app % n 2) 0)
+        (if (app eq (app % n 2) 0)
           (tail-app collatz_steps (app / n 2)            (app + acc 1))
           (tail-app collatz_steps (app + (app * n 3) 1)  (app + acc 1))))))
 
@@ -45,7 +45,7 @@
         (ret (con Int))))
     (params i total)
     (body
-      (if (app == i 0)
+      (if (app eq i 0)
         total
         (tail-app sum_steps_loop
           (app - i 1)

examples/bench_compute_intsum.ail

@@ -28,7 +28,7 @@
         (ret (con Int))))
     (params i acc)
     (body
-      (if (app == i 0)
+      (if (app eq i 0)
         acc
         (tail-app intsum_loop
           (app - i 1)

examples/bench_hof_pipeline.ail

@@ -40,7 +40,7 @@
         (ret (con List (con Int)))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app build_n
           (app - n 1)

examples/bench_latency_explicit.ail

@@ -49,7 +49,7 @@
         (ret (own (con Tree)))))
     (params depth)
     (body
-      (if (app == depth 0)
+      (if (app eq depth 0)
         (term-ctor Tree TLeaf)
         (term-ctor Tree TNode
           1
@@ -78,7 +78,7 @@
         (ret (own (con IntList)))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app cons_n_acc
           (app - n 1)
@@ -138,9 +138,9 @@
         (effects IO)))
     (params remaining print_countdown chunk_len print_k t)
     (body
-      (if (app == remaining 0)
+      (if (app eq remaining 0)
         (app print 9999)
-        (if (app == print_countdown 0)
+        (if (app eq print_countdown 0)
           (seq
             (app print (app one_op chunk_len t))
             (tail-app loop

examples/bench_latency_implicit.ail

@@ -73,7 +73,7 @@
         (ret (con Tree))))
     (params depth)
     (body
-      (if (app == depth 0)
+      (if (app eq depth 0)
         (term-ctor Tree TLeaf)
         (term-ctor Tree TNode
           1
@@ -103,7 +103,7 @@
         (ret (con IntList))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app cons_n_acc
           (app - n 1)
@@ -197,9 +197,9 @@
         (effects IO)))
     (params remaining print_countdown chunk_len print_k t)
     (body
-      (if (app == remaining 0)
+      (if (app eq remaining 0)
         (app print 9999)
-        (if (app == print_countdown 0)
+        (if (app eq print_countdown 0)
           (seq
             (app print (app one_op chunk_len t))
             (tail-app loop

examples/bench_list_sum.ail

@@ -44,7 +44,7 @@
         (ret (con IntList))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app cons_n_acc
           (app - n 1)

examples/bench_list_sum.prose.txt

@@ -4,7 +4,7 @@ data IntList = INil | ICons(Int, IntList)
 
 /// Tail-recursive list builder. Result = accumulator-prepended list.
 fn cons_n_acc(n: Int, acc: IntList) -> IntList {
-  if n == 0 {
+  if eq(n, 0) {
     acc
   } else {
     tail cons_n_acc(n - 1, ICons(n - 1, acc))

examples/bench_list_sum_explicit.ail

@@ -41,7 +41,7 @@
         (ret (own (con IntList)))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app cons_n_acc
           (app - n 1)

examples/bench_mono_dispatch.ail

@@ -16,7 +16,7 @@
     (class Looper)
     (type (con Int))
     (method loop_call
-      (body (lam (params (typed i a) (typed acc (con Int))) (ret (con Int)) (body (if (app == i 0) acc (tail-app loop_call (app - i 1) (app + acc (app foo (app + acc i))))))))))
+      (body (lam (params (typed i a) (typed acc (con Int))) (ret (con Int)) (body (if (app eq i 0) acc (tail-app loop_call (app - i 1) (app + acc (app foo (app + acc i))))))))))
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)

examples/bench_tree_walk.ail

@@ -42,7 +42,7 @@
         (ret (con Tree))))
     (params depth)
     (body
-      (if (app == depth 0)
+      (if (app eq depth 0)
         (term-ctor Tree Leaf)
         (term-ctor Tree Node
           1

examples/ct_4_qualified_class.ail

@@ -23,4 +23,4 @@
               (case (pat-ctor MkBox a)
                 (match y
                   (case (pat-ctor MkBox b)
-                    (app == a b)))))))))))
+                    (app eq a b)))))))))))

examples/eq_demo.ail

@@ -1,26 +1,29 @@
-; Iter 16e — `==` extends from Int-only to Int/Bool/Str/Unit (polymorphic
+; Equality dispatch via the prelude.Eq class for Int/Bool/Str/Unit.
-; dispatch). The builtin's declared type became
+; Each `(app eq x y)` call resolves to the matching primitive Eq
-;   forall a. (a, a) -> Bool
+; instance, lowered via try_emit_primitive_instance_body in the
-; and codegen monomorphises on the resolved arg type:
+; codegen:
 ;   Int  → icmp eq i64
 ;   Bool → icmp eq i1
-;   Str  → @strcmp + icmp eq i32 0
+;   Str  → @ail_str_eq (strcmp-based)
 ;   Unit → constant i1 true (single-inhabitant type)
-;   ADT/Fn → rejected at codegen with a clear error.
+;
+; Float has no Eq instance; partial-Float comparison is done via
+; the explicit float_eq / float_lt / etc. fns (see
+; design/contracts/float-semantics.md).
 ;
 ; This fixture exercises all four supported types, both directly via
-; `(app == ...)` and indirectly via 16c's lit-pattern desugar (which
+; `(app eq ...)` and indirectly via the lit-pattern desugar (which
-; rewrites `(pat-lit "hi")` → `(if (== sv "hi") body fall_k)` and
+; rewrites `(pat-lit "hi")` → `(if (eq sv "hi") body fall_k)` and
-; therefore inherits 16e's polymorphic `==`).
+; therefore inherits the same class-dispatch path).
 ;
 ; Expected stdout (one per line):
-;   true   ; (== 5 5)
+;   true   ; (eq 5 5)
-;   false  ; (== 5 6)
+;   false  ; (eq 5 6)
-;   false  ; (== true false)
+;   false  ; (eq true false)
-;   true   ; (== true true)
+;   true   ; (eq true true)
-;   true   ; (== "hi" "hi")
+;   true   ; (eq "hi" "hi")
-;   false  ; (== "hi" "ho")
+;   false  ; (eq "hi" "ho")
-;   true   ; (== () ())
+;   true   ; (eq () ())
 ;   1      ; classify_str "hi"   (lit-pattern hits 1 arm)
 ;   2      ; classify_str "ho"   (lit-pattern hits 2 arm)
 ;   0      ; classify_str "??"   (default arm)
@@ -30,7 +33,7 @@
 (module eq_demo
 
   (fn classify_str
-    (doc "Lit-pattern over Str; exercises 16c's build_eq for non-Int.")
+    (doc "Lit-pattern over Str; exercises build_eq's class-dispatch lowering for non-Int.")
     (type (fn-type (params (con Str)) (ret (con Int))))
     (params s)
     (body
@@ -40,17 +43,17 @@
         (case _ 0))))
 
   (fn main
-    (doc "Drive == at Int/Bool/Str/Unit; then drive classify_str.")
+    (doc "Drive eq at Int/Bool/Str/Unit; then drive classify_str.")
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)
     (body
-      (seq (app print (app == 5 5))
+      (seq (app print (app eq 5 5))
-      (seq (app print (app == 5 6))
+      (seq (app print (app eq 5 6))
-      (seq (app print (app == true false))
+      (seq (app print (app eq true false))
-      (seq (app print (app == true true))
+      (seq (app print (app eq true true))
-      (seq (app print (app == "hi" "hi"))
+      (seq (app print (app eq "hi" "hi"))
-      (seq (app print (app == "hi" "ho"))
+      (seq (app print (app eq "hi" "ho"))
-      (seq (app print (app == (lit-unit) (lit-unit)))
+      (seq (app print (app eq (lit-unit) (lit-unit)))
       (seq (app print (app classify_str "hi"))
       (seq (app print (app classify_str "ho"))
            (app print (app classify_str "??"))))))))))))))

examples/eq_float_must_fail.ail

@@ -0,0 +1,6 @@
+(module eq_float_must_fail
+  (fn main
+    (doc "Klausel-3 discriminator. After operator-routing-eq-ord, `(app eq 1.5 1.5)` must fire `NoInstance Eq Float` with a follow-up sentence naming `float_eq` as the explicit IEEE-aware alternative. Today the diagnostic already fires (no Eq Float instance) but does not name `float_eq` — the milestone adds that hint.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body (app print (app eq 1.5 1.5)))))

examples/eq_ord_user_adt.ail

@@ -9,7 +9,7 @@
     (method eq
       (body (lam (params (typed a (con IntBox)) (typed b (con IntBox))) (ret (con Bool)) (body (match a
         (case (pat-ctor MkIntBox ai) (match b
-          (case (pat-ctor MkIntBox bi) (app == ai bi))))))))))
+          (case (pat-ctor MkIntBox bi) (app eq ai bi))))))))))
   (instance
     (class prelude.Ord)
     (type (con IntBox))

examples/eq_user_adt_smoke.ail

@@ -0,0 +1,28 @@
+(module eq_user_adt_smoke
+  (data Point
+    (doc "Two-Int-field record. The milestone-defining north-star: an LLM author writes `instance Eq Point` and calls `(app eq p1 p2)` end-to-end through class-dispatch.")
+    (ctor Point (con Int) (con Int)))
+  (instance
+    (class prelude.Eq)
+    (type (con Point))
+    (doc "Eq Point by structural comparison of the two Int fields. The nested `(app eq a1 a2)` calls dispatch to prelude.Eq.eq's Int instance.")
+    (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 Point 1 2)
+        (let p2 (term-ctor Point Point 1 2)
+          (let p3 (term-ctor Point Point 1 3)
+            (seq (app print (app eq (lit-unit) (lit-unit)))
+              (seq (app print (app eq p1 p2))
+                (app print (app eq p1 p3))))))))))

examples/escape_local_demo.ail

@@ -41,7 +41,7 @@
     (type (fn-type (params (con Int)) (ret (con Int))))
     (params n)
     (body
-      (if (app <= n 0)
+      (if (app le n 0)
         0
         (let b (term-ctor Box MkBox n)
           (match b

examples/fieldtest/floats_1_newton_sqrt.ail

@@ -18,7 +18,7 @@
         (ret (con Float))))
     (params n x k)
     (body
-      (if (app == k 0)
+      (if (app eq k 0)
         x
         (tail-app newton_iter
           n

examples/fieldtest/floats_3_safe_division.ail

@@ -37,9 +37,9 @@
     (body
       (if (app is_nan x)
         -1
-        (if (app > x 1.0e308)
+        (if (app float_gt x 1.0e308)
           0
-          (if (app < x -1.0e308)
+          (if (app float_lt x -1.0e308)
             0
             1)))))
 

examples/fieldtest/forma_1_factorial.ail

@@ -8,7 +8,7 @@
         (ret (con Int))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app fact_acc (app - n 1) (app * acc n)))))
 

examples/fieldtest/forma_4_intmath_lib.ail

@@ -17,6 +17,6 @@
     (type (fn-type (params (con Int)) (ret (con Int))))
     (params x)
     (body
-      (if (app < x 0)
+      (if (app lt x 0)
         (app - 0 x)
         x))))

examples/fieldtest/loop_recur_1_isqrt_newton.ail

@@ -12,12 +12,12 @@
     (type (fn-type (params (con Int)) (ret (con Int))))
     (params n)
     (body
-      (if (app < n 2)
+      (if (app lt n 2)
           n
           (loop (x (con Int) n) (prev (con Int) 0)
-            (if (app == x prev)
+            (if (app eq x prev)
                 x
                 (let next (app / (app + x (app / n x)) 2)
-                  (if (app == next x)
+                  (if (app eq next x)
                       next
                       (recur next x)))))))))

examples/fieldtest/loop_recur_2_collatz.ail

@@ -13,7 +13,7 @@
     (params start)
     (body
       (loop (n (con Int) start) (steps (con Int) 0)
-        (if (app == n 1)
+        (if (app eq n 1)
             steps
             (match (app % n 2)
               (case (pat-lit 0) (recur (app / n 2) (app + steps 1)))

examples/fieldtest/loop_recur_3a_recur_outside_loop.ail

@@ -7,7 +7,7 @@
     (type (fn-type (params (con Int)) (ret (con Int))))
     (params n)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
           0
           (recur (app - n 1)))))
   (fn main

examples/fieldtest/loop_recur_3b_recur_arity.ail

@@ -8,7 +8,7 @@
     (params n)
     (body
       (loop (acc (con Int) 0) (i (con Int) 1)
-        (if (app > i n)
+        (if (app gt i n)
             acc
             (recur (app + acc i))))))
   (fn main

examples/fieldtest/loop_recur_3c_recur_type.ail

@@ -8,9 +8,9 @@
     (params start)
     (body
       (loop (i (con Int) start)
-        (if (app == i 0)
+        (if (app eq i 0)
             i
-            (recur (app > i 0))))))
+            (recur (app gt i 0))))))
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)

examples/fieldtest/loop_recur_3d_recur_not_tail.ail

@@ -9,7 +9,7 @@
     (params n)
     (body
       (loop (i (con Int) n)
-        (if (app == i 1)
+        (if (app eq i 1)
             1
             (app * i (recur (app - i 1)))))))
   (fn main

examples/fieldtest/loop_recur_3e_binder_captured.ail

@@ -13,7 +13,7 @@
     (params n)
     (body
       (loop (acc (con Int) 0) (i (con Int) 1)
-        (if (app > i n)
+        (if (app gt i n)
             acc
             (recur (app apply_int (lam (params (typed d (con Int))) (ret (con Int)) (body (app + acc d))) i)
                    (app + i 1))))))

examples/fieldtest/loop_recur_4_gcd_value_pos.ail

@@ -14,7 +14,7 @@
     (params x y)
     (body
       (loop (a (con Int) x) (b (con Int) y)
-        (if (app == b 0)
+        (if (app eq b 0)
             a
             (recur b (app % a b))))))
   (fn main

examples/fieldtest/loop_recur_5_event_loop_noterm.ail

@@ -10,7 +10,7 @@
     (params)
     (body
       (loop (tick (con Int) 0) (parity (con Int) 0)
-        (if (app == (app % tick 2) 0)
+        (if (app eq (app % tick 2) 0)
             (recur (app + tick 1) 1)
             (recur (app + tick 1) 0)))))
   (fn main

examples/fieldtest/loop_recur_5b_event_loop_noterm.ail

@@ -12,7 +12,7 @@
     (params start)
     (body
       (loop (tick (con Int) start) (parity (con Int) 0)
-        (if (app == (app % tick 2) 0)
+        (if (app eq (app % tick 2) 0)
             (recur (app + tick 1) 1)
             (recur (app + tick 1) 0)))))
   (fn main

examples/fieldtest/mut-local_2_classify_temp.ail

@@ -7,7 +7,7 @@
     (doc "Return category code 0..3 for temperature t in degrees C.")
     (type (fn-type (params (con Int)) (ret (con Int))))
     (params t)
-    (body (let code 0 (let code (if (app < t 0) 0 (if (app < t 15) 1 (if (app < t 28) 2 3))) code))))
+    (body (let code 0 (let code (if (app lt t 0) 0 (if (app lt t 15) 1 (if (app lt t 28) 2 3))) code))))
 
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))

examples/fieldtest/mut-local_4_has_small_factor.ail

@@ -7,7 +7,7 @@
   (fn has_small_factor
     (type (fn-type (params (con Int)) (ret (con Bool))))
     (params n)
-    (body (let found false (let found (if (app == (app % n 2) 0) true found) (let found (if (app == (app % n 3) 0) true found) (let found (if (app == (app % n 5) 0) true found) (let found (if (app == (app % n 7) 0) true found) found)))))))
+    (body (let found false (let found (if (app eq (app % n 2) 0) true found) (let found (if (app eq (app % n 3) 0) true found) (let found (if (app eq (app % n 5) 0) true found) (let found (if (app eq (app % n 7) 0) true found) found)))))))
 
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))

examples/fieldtest/remove-mut_1_sum_of_squares.ail

@@ -18,7 +18,7 @@
     (params n)
     (body
       (loop (i (con Int) 1) (acc (con Int) 0)
-        (if (app > i n)
+        (if (app gt i n)
             acc
             (recur (app + i 1) (app + acc (app * i i)))))))
 

examples/fieldtest/remove-mut_2_grade_cascade.ail

@@ -23,10 +23,10 @@
     (params score)
     (body
       (let g 0
-        (let g (if (app >= score 60) 1 g)
+        (let g (if (app ge score 60) 1 g)
-          (let g (if (app >= score 70) 2 g)
+          (let g (if (app ge score 70) 2 g)
-            (let g (if (app >= score 80) 3 g)
+            (let g (if (app ge score 80) 3 g)
-              (let g (if (app >= score 90) 4 g)
+              (let g (if (app ge score 90) 4 g)
                 g)))))))
 
   (fn main

examples/fieldtest/remove-mut_4_bracket_scanner.ail

@@ -45,13 +45,13 @@
     (body
       (match rest
         (case (pat-ctor Nil)
-          (if ok (app == depth 0) false))
+          (if ok (app eq depth 0) false))
         (case (pat-ctor Cons t more)
           (match t
             (case (pat-lit 1)
               (tail-app scan more (app + depth 1) ok))
             (case (pat-lit 2)
-              (if (app == depth 0)
+              (if (app eq depth 0)
                   (tail-app scan more depth false)
                   (tail-app scan more (app - depth 1) ok)))
             (case _

examples/float_compare_smoke.ail

@@ -0,0 +1,9 @@
+(module float_compare_smoke
+  (fn main
+    (doc "Float comparison via the named-fn surface that replaces the deleted operator names. Each float_* call lowers to a single fcmp via try_emit_primitive_instance_body.")
+    (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)))))))

examples/local_rec_as_value.ail

@@ -27,7 +27,7 @@
         (params n)
         (type (fn-type (params (con Int)) (ret (con Int))))
         (body
-          (if (app <= n 1)
+          (if (app le n 1)
             1
             (app * n (app factorial (app - n 1)))))
         (in (app print (app apply5 factorial)))))))

examples/local_rec_as_value_capture.ail

@@ -29,7 +29,7 @@
         (params n)
         (type (fn-type (params (con Int)) (ret (con Int))))
         (body
-          (if (app <= n 1)
+          (if (app le n 1)
             (app + 1 base)
             (app * n (app factorial_plus (app - n 1)))))
         (in (app apply5 factorial_plus)))))

examples/local_rec_capture.ail

@@ -20,7 +20,7 @@
         (params i)
         (type (fn-type (params (con Int)) (ret (con Int))))
         (body
-          (if (app >= i n)
+          (if (app ge i n)
             0
             (app + i (app loop (app + i 1)))))
         (in (app loop 1)))))

examples/local_rec_demo.ail

@@ -17,7 +17,7 @@
         (params n)
         (type (fn-type (params (con Int)) (ret (con Int))))
         (body
-          (if (app <= n 1)
+          (if (app le n 1)
             1
             (app * n (app fact (app - n 1)))))
         (in

examples/local_rec_let_capture.ail

@@ -31,9 +31,9 @@
           (params i)
           (type (fn-type (params (con Int)) (ret (con Int))))
           (body
-            (if (app > i n)
+            (if (app gt i n)
               0
-              (if (app < i threshold)
+              (if (app lt i threshold)
                 (app + 1 (app loop (app + i 1)))
                 (app loop (app + i 1)))))
           (in (app loop 1))))))

examples/local_rec_match_capture.ail

@@ -42,9 +42,9 @@
             (params i)
             (type (fn-type (params (con Int)) (ret (con Int))))
             (body
-              (if (app > i n)
+              (if (app gt i n)
                 0
-                (if (app < i threshold)
+                (if (app lt i threshold)
                   (app + 1 (app loop (app + i 1)))
                   (app loop (app + i 1)))))
             (in (app loop 1)))))))

examples/loop_sum_to.ail

@@ -4,6 +4,6 @@
     (params n)
     (body
       (loop (acc (con Int) 0) (i (con Int) 1)
-        (if (app > i n)
+        (if (app gt i n)
             acc
             (recur (app + acc i) (app + i 1)))))))

examples/loop_sum_to_deep.ail

@@ -9,6 +9,6 @@
     (params n)
     (body
       (loop (acc (con Int) 0) (i (con Int) 1)
-        (if (app > i n)
+        (if (app gt i n)
             acc
             (recur (app + acc i) (app + i 1)))))))

examples/loop_sum_to_run.ail

@@ -9,6 +9,6 @@
     (params n)
     (body
       (loop (acc (con Int) 0) (i (con Int) 1)
-        (if (app > i n)
+        (if (app gt i n)
             acc
             (recur (app + acc i) (app + i 1)))))))

examples/loop_sum_to_run.prose.txt

@@ -7,7 +7,7 @@ fn main() -> Unit with IO {
 
 fn sum_to(n: Int) -> Int {
   loop(acc = 0, i = 1) {
-    if i > n {
+    if gt(i, n) {
       acc
     } else {
       recur(acc + i, i + 1)

examples/max3.ail

@@ -2,12 +2,12 @@
   (fn max
     (type (fn-type (params (con Int) (con Int)) (ret (con Int))))
     (params a b)
-    (body (if (app > a b) a b)))
+    (body (if (app gt a b) a b)))
   (fn max3
     (doc "Demonstriert verschachteltes if (statt max-call) zum Test des Block-Trackings.")
     (type (fn-type (params (con Int) (con Int) (con Int)) (ret (con Int))))
     (params a b c)
-    (body (if (app > a b) (if (app > a c) a c) (if (app > b c) b c))))
+    (body (if (app gt a b) (if (app gt a c) a c) (if (app gt b c) b c))))
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)

examples/mut_counter.ail

@@ -12,6 +12,6 @@
     (type (fn-type (params (con Int) (con Int) (con Int)) (ret (con Int))))
     (params lo hi acc)
     (body
-      (if (app > lo hi)
+      (if (app gt lo hi)
         acc
         (tail-app sum_helper (app + lo 1) hi (app + acc lo))))))

examples/mut_sum_floats.ail

@@ -12,6 +12,6 @@
     (type (fn-type (params (con Float) (con Float) (con Float)) (ret (con Float))))
     (params lo hi acc)
     (body
-      (if (app > lo hi)
+      (if (app float_gt lo hi)
         acc
         (tail-app sum_helper (app + lo 1.0) hi (app + acc lo))))))

examples/nested_let_rec.ail

@@ -29,14 +29,14 @@
         (params i)
         (type (fn-type (params (con Int)) (ret (con Int))))
         (body
-          (if (app > i n)
+          (if (app gt i n)
             0
             (app +
               (let-rec inner
                 (params j)
                 (type (fn-type (params (con Int)) (ret (con Int))))
                 (body
-                  (if (app > j i)
+                  (if (app gt j i)
                     0
                     (app + 1 (app inner (app + j 1)))))
                 (in (app inner 1)))

examples/operator_unbound_check.ail

@@ -0,0 +1,6 @@
+(module operator_unbound_check
+  (fn main
+    (doc "Pin fixture. After operator-routing-eq-ord, `(app == 5 5)` must fail typecheck with `unknown variable: ==` — the operator names are no longer in the language. Today this typechecks (== is polymorphic over Int) — RED-first.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body (app print (app == 5 5)))))

examples/ord_int_intercept_smoke.ail

@@ -0,0 +1,27 @@
+; Smoke fixture for the `lt__Int` / `le__Int` / `gt__Int` /
+; `ge__Int` / `ne__Int` intercept-arm family (operator-routing-eq-ord.1
+; Task 13). Forces the mono pass to instantiate each of the five
+; Ord/Eq free helpers at Int by calling each one once; the linked
+; pin test (ord_int_intercept_ir_pin.rs) reads the resulting IR and
+; asserts each body lowers to a single direct `icmp` carrying
+; `alwaysinline`. The body is not perf-relevant — only the symbol
+; set and the IR shape are pinned.
+
+(module ord_int_intercept_smoke
+
+  (fn drive
+    (doc "Touches each of lt/le/gt/ge/ne at Int once. Returns 0 unconditionally; we care only about which mono symbols the call graph forces the unified mono pass to emit.")
+    (type (fn-type (params (con Int) (con Int)) (ret (con Int))))
+    (params a b)
+    (body
+      (let r1 (app lt a b)
+      (let r2 (app le a b)
+      (let r3 (app gt a b)
+      (let r4 (app ge a b)
+      (let r5 (app ne a b)
+        0)))))))
+
+  (fn main
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body (app print (app drive 1 2)))))

examples/poly_rec_capture.ail

@@ -43,7 +43,7 @@
         (params k acc)
         (type (fn-type (params (con Int) a) (ret a)))
         (body
-          (if (app == k 0)
+          (if (app eq k 0)
             acc
             (app loop (app - k 1) (app f acc))))
         (in (app loop n x)))))

examples/prelude.ail

@@ -6,27 +6,33 @@
     (ctor GT))
   (class Eq
     (param a)
-    (doc "Structural equality. Ships in milestone 23 alongside Ord. The primitive `==` operator stays as the surface-level comparator this iter; routing `==` through `Eq.eq` is the declared P2 follow-up (see docs/specs/2026-05-10-23-eq-ord-prelude.md, `Out of scope`).")
+    (doc "Structural equality. The class-method `eq` is the surface-level comparator; `==` as a surface name is not part of the language. Primitive instances Eq Int / Bool / Str / Unit are lowered via try_emit_primitive_instance_body in the codegen.")
     (method eq
       (type (fn-type (params (borrow a) (borrow a)) (ret (con Bool))))))
   (instance
     (class Eq)
     (type (con Int))
-    (doc "Eq Int. Body lowers to `icmp eq i64` via the existing primitive `==` dispatch in `lower_eq`.")
+    (doc "Eq Int. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Int emits `icmp eq i64` with the alwaysinline attribute.")
     (method eq
-      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
+      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
   (instance
     (class Eq)
     (type (con Bool))
-    (doc "Eq Bool. Body lowers to `icmp eq i1` via the existing primitive `==` dispatch in `lower_eq`.")
+    (doc "Eq Bool. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Bool emits `icmp eq i1` with the alwaysinline attribute.")
     (method eq
-      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
+      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
   (instance
     (class Eq)
     (type (con Str))
-    (doc "Eq Str. The lambda body shape mirrors Int/Bool for round-trip stability, but the codegen intercept in `emit_fn` overrides the body to call `@ail_str_eq` directly — see `try_emit_primitive_instance_body` in `crates/ailang-codegen/src/lib.rs`.")
+    (doc "Eq Str. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Str overrides it with a call to `@ail_str_eq` and attaches the alwaysinline attribute.")
     (method eq
-      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
+      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
+  (instance
+    (class Eq)
+    (type (con Unit))
+    (doc "Eq Unit. Unit is single-inhabitant so all values compare equal. Body is placeholder; codegen intercept try_emit_primitive_instance_body::eq__Unit emits `ret i1 1`.")
+    (method eq
+      (body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body true)))))
   (class Ord
     (param a)
     (superclass (class Eq) (type a))
@@ -113,4 +119,34 @@
     (doc "Polymorphic console-print helper. `print x` ≡ `do io/print_str (show x)` with an explicit let-binder around `show x` for heap-Str RC discipline per eob.1 Str carve-out. Ships in milestone 24 as the second half of the Show prelude.")
     (type (forall (vars a) (constraints (constraint Show a)) (fn-type (params (borrow a)) (ret (con Unit)) (effects IO))))
     (params x)
-    (body (let s (app show x) (do io/print_str s)))))
+    (body (let s (app show x) (do io/print_str s))))
+  (fn float_eq
+    (doc "IEEE Float equality. `float_eq x y` returns true iff both operands are non-NaN and bit-equal. Lowered to `fcmp oeq double` via try_emit_primitive_instance_body::float_eq with alwaysinline. Replaces the milestone-deleted polymorphic `==` on Float.")
+    (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
+    (params x y)
+    (body false))
+  (fn float_ne
+    (doc "IEEE Float disequality. `float_ne nan nan` returns true (unordered-or-not-equal per IEEE-754). Lowered to `fcmp une double`.")
+    (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
+    (params x y)
+    (body false))
+  (fn float_lt
+    (doc "IEEE Float strict less-than. `float_lt nan x` returns false for any x (unordered). Lowered to `fcmp olt double`.")
+    (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
+    (params x y)
+    (body false))
+  (fn float_le
+    (doc "IEEE Float less-than-or-equal. Lowered to `fcmp ole double`.")
+    (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
+    (params x y)
+    (body false))
+  (fn float_gt
+    (doc "IEEE Float strict greater-than. Lowered to `fcmp ogt double`.")
+    (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
+    (params x y)
+    (body false))
+  (fn float_ge
+    (doc "IEEE Float greater-than-or-equal. Lowered to `fcmp oge double`.")
+    (type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
+    (params x y)
+    (body false)))

examples/rc_drop_iterative_long_list.ail

@@ -7,7 +7,7 @@
     (doc "Tail-recursive list builder. acc-prepended.")
     (type (fn-type (params (con Int) (con IntList)) (ret (con IntList))))
     (params n acc)
-    (body (if (app == n 0) acc (tail-app cons_n_acc (app - n 1) (term-ctor IntList ICons n acc)))))
+    (body (if (app eq n 0) acc (tail-app cons_n_acc (app - n 1) (term-ctor IntList ICons n acc)))))
   (fn cons_n
     (doc "Build [1, 2, ..., n] :: IntList. Order is reverse of build but immaterial for head/sum.")
     (type (fn-type (params (con Int)) (ret (con IntList))))

examples/rc_let_alias_implicit_param.ail

@@ -36,7 +36,7 @@
         (ret (own (con Tree)))))
     (params d)
     (body
-      (if (app == d 0)
+      (if (app eq d 0)
         (term-ctor Tree TLeaf)
         (term-ctor Tree TNode 1
           (app build (app - d 1))
@@ -66,7 +66,7 @@
         (ret (con Int))))
     (params n t)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         0
         (let _v (app pin_aliased t)
           (app loop (app - n 1) t)))))

examples/rc_let_owned_app_leak.ail

@@ -28,7 +28,7 @@
         (ret (own (con Tree)))))
     (params d)
     (body
-      (if (app == d 0)
+      (if (app eq d 0)
         (term-ctor Tree TLeaf)
         (term-ctor Tree TNode 1
           (app build (app - d 1))

examples/rc_pin_recurse_implicit.ail

@@ -24,7 +24,7 @@
     (type (fn-type (params (con Int)) (ret (con Tree))))
     (params d)
     (body
-      (if (app == d 0)
+      (if (app eq d 0)
         (term-ctor Tree TLeaf)
         (term-ctor Tree TNode 1
           (app build (app - d 1))
@@ -42,7 +42,7 @@
     (type (fn-type (params (con Int) (con Tree)) (ret (con Int))))
     (params n t)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         0
         (let _v (app pin t)
           (app loop (app - n 1) t)))))

examples/rc_tail_sum_explicit_leak.ail

@@ -26,7 +26,7 @@
         (ret (own (con IntList)))))
     (params n acc)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         acc
         (tail-app cons_n_acc
           (app - n 1)

examples/sort.ail

@@ -9,7 +9,7 @@
     (params y xs)
     (body (match xs
       (case (pat-ctor Nil) (term-ctor IntList Cons y (term-ctor IntList Nil)))
-      (case (pat-ctor Cons h t) (if (app <= y h) (term-ctor IntList Cons y (term-ctor IntList Cons h t)) (term-ctor IntList Cons h (app insert y t)))))))
+      (case (pat-ctor Cons h t) (if (app le y h) (term-ctor IntList Cons y (term-ctor IntList Cons h t)) (term-ctor IntList Cons h (app insert y t)))))))
   (fn sort
     (doc "Insertion sort: build the result by inserting each head into the sorted tail.")
     (type (fn-type (params (con IntList)) (ret (con IntList))))

examples/std_list.ail

@@ -172,7 +172,7 @@
           (ret (con List a)))))
     (params n xs)
     (body
-      (if (app <= n 0)
+      (if (app le n 0)
         (term-ctor List Nil)
         (match xs
           (case (pat-ctor Nil) (term-ctor List Nil))
@@ -188,7 +188,7 @@
           (ret (con List a)))))
     (params n xs)
     (body
-      (if (app <= n 0)
+      (if (app le n 0)
         xs
         (match xs
           (case (pat-ctor Nil) (term-ctor List Nil))

examples/std_list_demo.ail

@@ -24,7 +24,7 @@
     (doc "Predicate: x mod 2 == 0.")
     (type (fn-type (params (con Int)) (ret (con Bool))))
     (params x)
-    (body (app == (app % x 2) 0)))
+    (body (app eq (app % x 2) 0)))
 
   (fn double
     (doc "Multiply by 2. Used as the map arg.")

examples/std_list_stress.ail

@@ -17,7 +17,7 @@
         (ret (con std_list.List (con Int)))))
     (params n)
     (body
-      (if (app == n 0)
+      (if (app eq n 0)
         (term-ctor std_list.List Nil)
         (term-ctor std_list.List Cons
           n

examples/sum.ail

@@ -3,7 +3,7 @@
     (doc "rekursive Summe 0..=n")
     (type (fn-type (params (con Int)) (ret (con Int))))
     (params n)
-    (body (if (app == n 0) 0 (app + n (app sum (app - n 1))))))
+    (body (if (app eq n 0) 0 (app + n (app sum (app - n 1))))))
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)

examples/test_mono_recursive_fn_bug.ail

@@ -11,7 +11,7 @@
   (fn loop
     (type (fn-type (params (con Int) (con Int)) (ret (con Int))))
     (params acc i)
-    (body (if (app == i 0) acc (tail-app loop (app + acc i) (app - i 1)))))
+    (body (if (app eq i 0) acc (tail-app loop (app + acc i) (app - i 1)))))
   (fn main
     (type (fn-type (params) (ret (con Unit)) (effects IO)))
     (params)

examples/unreachable_demo.ail

@@ -22,7 +22,7 @@
     (type (fn-type (params (con Int) (con Int)) (ret (con Int))))
     (params a b)
     (body
-      (if (app == b 0)
+      (if (app eq b 0)
           __unreachable__
           (app / a b))))