iter 23.5: prelude free fns + E2E — Eq/Ord milestone close

Five polymorphic prelude free fns (ne/lt/le/gt/ge) plus three E2E
fixtures: positive composition over Int/Bool/Str, user-ADT with
user-written Eq/Ord on IntBox, and Float-NoInstance with a
Float-aware diagnostic addendum cross-referencing DESIGN.md §"Float
semantics".

Two checker-side fixes were needed alongside the prelude additions,
both symmetric to the iter 23.4-prep visibility fix:
- linearity::check_module_with_visible — workspace-aware callee-mode
  resolution so a Borrow-mode user fn forwarding into a prelude poly
  fn (e.g. `at_most x y = not (gt x y)`) doesn't false-fire
  consume-while-borrowed.
- mono::collect_mono_targets — distinguish rigid forall vars from
  unbound metavars; rigid-bearing free-fn targets skip (they get
  re-collected with concrete subst when the enclosing fn itself
  monomorphises). Without this, a polymorphic body calling another
  polymorphic free fn produced a spurious __Unit specialisation
  whose body referenced compare at Unit.

Roadmap split: shipped Eq/Ord half checked, Show + print-rewire half
remains pending behind the heap-Str ABI prerequisite. DESIGN.md
§"Prelude classes" amended.

One pre-existing fixture (test_22b1_missing_method) renamed its
class method ne → tne to avoid collision with the new prelude `ne`.

Bench: check.py + cross_lang.py exit 0; compile_check.py exits 1
with one sub-ms check_ms.local_rec_capture at +26% (tolerance 25%) —
prelude-growth-related noise-band fluctuation, ratifiable per spec
§248-249 and journal Concerns.

docs/DESIGN.md

@@ -1701,6 +1701,16 @@ end-to-end path is the milestone's typeclass acceptance gate
 `instance Foo IntBox`); see `docs/specs/2026-05-09-22-typeclasses.md`
 "Amendments" for the substantive rationale.
 
+Milestone 23 amends the above: the prelude now ships the `Ordering`
+ADT, the `Eq` and `Ord` classes, primitive `Eq Int/Bool/Str` and
+`Ord Int/Bool/Str` instances, and the five polymorphic free-fn helpers
+`ne` / `lt` / `le` / `gt` / `ge`. `Show`, operator routing through
+`Eq`/`Ord`, and `print`-rewire remain out of scope per their original
+substantive reasons (heap-`Str` ABI, bench rebaseline). Float has
+neither `Eq` nor `Ord` instance per §"Float semantics"; a polymorphic
+helper invoked at Float fires `NoInstance` at typecheck with a
+Float-aware diagnostic cross-referencing this section.
+
 Primitive output goes through `io/print_int` / `io/print_bool` /
 `io/print_str` directly.
 

docs/journals/2026-05-12-iter-23.5.md

@@ -0,0 +1,200 @@
+# iter 23.5 — Prelude free fns + E2E (Eq/Ord milestone close)
+
+**Date:** 2026-05-12
+**Started from:** 35c6eb5
+**Status:** DONE
+**Tasks completed:** 8 of 8
+
+## Summary
+
+Closes milestone 23. Ships the five polymorphic prelude free fns
+`ne` / `lt` / `le` / `gt` / `ge` (Tasks 1-2), three end-to-end
+fixtures covering primitive composition + user-ADT integration +
+the Float negative case (Tasks 3-5), the Float-aware `NoInstance`
+diagnostic addendum (Task 5), the DESIGN.md §"Prelude classes"
+amendment (Task 6), and the roadmap split between shipped Eq/Ord
+and the pending Show + print-rewire half (Task 7). Bench check
+runs clean except a noisy sub-millisecond `check_ms.local_rec_capture`
+regression that sits just over the 25% tolerance — ratifiable per
+the audit-tolerance rule (the prelude grew by 5 polymorphic
+`Def::Fn`s, so the typecheck workload per workspace measurably
+shifts).
+
+Two implementer-phase fixes were needed beyond the plan, both
+symmetric to existing precedent (iter 23.4-prep). They surfaced
+when the natural test fixtures (user-defined `at_most x y = not (gt
+x y)` composing prelude poly fns) hit two distinct false-positive
+shapes:
+
+1. **Linearity check needed workspace-wide visibility** for
+   imported polymorphic free fns + class methods. Previously the
+   linearity pass only saw the current module's globals, so a
+   user `at_most` forwarding its borrow params into `gt` (defined
+   in the prelude) hit `callee_arg_modes("gt", 2) → []` →
+   default-Consume → `consume-while-borrowed` false positive. Fix
+   extends `linearity::check_module` to a `check_module_with_visible`
+   entry that takes additional Module references whose top-level fns
+   + class methods are registered in globals; the workspace-side
+   driver passes all sibling modules. Pure precedent extension of
+   23.4-prep, which added class-method visibility for the same
+   reason.
+
+2. **Mono pass needed to skip rigid-var-bearing free-fn targets.**
+   When a polymorphic free fn's body calls another polymorphic
+   free fn (e.g. `at_most`'s body calls `gt x y` with x, y of
+   type rigid `a`), the synth-channel observer recorded a
+   FreeFnCall whose type args were rigid `Type::Var { name: "a"
+   }`. The existing Unit-default fallback (correct for
+   `is_empty(Nil)`-shape unobservable metavars) was unsound here:
+   it produced `gt__Unit` whose body referenced `compare`, which
+   has no Unit instance → "unknown variable: compare" at the
+   synthesised body. Fix discriminates rigid vars
+   (Type::Var without `$m` prefix) from unbound metavars (`$m`
+   prefix) — rigids skip (they get re-collected with concrete
+   substitution when the enclosing fn itself monomorphises),
+   metavars keep their Unit-default.
+
+One existing fixture (`examples/test_22b1_missing_method.ail.json`)
+had to rename its class method `ne → tne` because `ne` is now a
+top-level prelude free fn and the workspace registry's
+method-name uniqueness check rejected the collision. The
+fixture's docstring already foreshadowed this case ("Class is
+`TEq` rather than `Eq` to avoid colliding…"); extended to also
+cover the `ne → tne` rename rationale.
+
+## Per-task notes
+
+- iter 23.5.1: `ne` free fn — added `Def::Fn ne` to prelude (body
+  `not (eq x y)`); created `crates/ail/tests/prelude_free_fns.rs`
+  with helpers `fixture()` and `mono_symbol_names()` + first test;
+  smoke fixture `examples/ne_at_int_smoke.ail.json`. RED→GREEN.
+  Adjusted `mono.modules.iter()` → `.values()` per the actual
+  `BTreeMap<String, Module>` shape (Boss pre-flight flagged).
+- iter 23.5.2: `lt` / `le` / `gt` / `ge` free fns — four
+  `Def::Fn`s in prelude (each pattern-matches on `compare x y`
+  against one of LT/GT plus a wildcard); four extending tests in
+  the same `prelude_free_fns.rs`; four smoke fixtures. RED→GREEN
+  per fn.
+- iter 23.5.3: positive E2E — `examples/eq_ord_polymorphic.ail.json`
+  with user-defined `at_most a a → Bool` composing prelude `not`
+  + `gt`; `crates/ail/tests/eq_ord_e2e.rs` with helpers
+  `fixture_path()` + `build_and_run()` plus
+  `eq_ord_polymorphic_runs_end_to_end`. Two implementer-phase
+  fixes (linearity + mono rigid-skip) landed during this task to
+  unblock the GREEN. Final stdout pinned at `"1\n0\n1"` (matches
+  `io/print_int`'s actual newline-separator behaviour; plan text
+  had `"101"` based on an incorrect concatenation assumption).
+- iter 23.5.4: user-ADT E2E — `examples/eq_ord_user_adt.ail.json`
+  with `type IntBox = MkIntBox Int` + user-written
+  `instance Eq IntBox` + `instance Ord IntBox` + `main` calling
+  `eq` twice. Two extending tests:
+  `eq_ord_user_adt_runs_end_to_end` (stdout `"1\n0"`) and
+  `eq_ord_user_adt_eq_intbox_hash_stable` (record-then-pin).
+  Mono symbol name is `eq__cde77856` (8-hex-prefix mangling for
+  compound types per DESIGN.md §"Mangling scheme"); body hash
+  pinned at `9daaffa7528d2a1c`. The Ord-IntBox instance's
+  retType needed qualifying as `prelude.Ordering` per the
+  canonical-type-names rule.
+- iter 23.5.5: Float-aware `NoInstance` addendum — implemented in
+  `CheckError::to_diagnostic()` (the per-iter spec-§"NoInstance"
+  conversion path; option-a from the plan's structural-choice
+  list). Addendum fires when `class ∈ {Eq, Ord}` AND `at_type ==
+  "Float"`: appends `— Float has no Eq/Ord instance by design
+  (partial orderability per IEEE-754); see DESIGN.md §"Float
+  semantics".` New `examples/eq_float_noinstance.ail.json` +
+  `crates/ail/tests/eq_float_noinstance.rs`. RED→GREEN.
+- iter 23.5.6: DESIGN.md amendment — inserted Milestone-23
+  amendment paragraph in §"Prelude (built-in) classes". Grep
+  gate RED→GREEN.
+- iter 23.5.7: roadmap split — replaced the single Post-22
+  Prelude entry with two: `[x]` Eq/Ord (shipped 23.5) and `[ ]`
+  Show + print rewire (gated on heap-`Str` ABI). Also
+  disambiguated the `depends on: Post-22 Prelude` reference at
+  line 73 to point specifically at the Eq/Ord half (Op routing's
+  actual dependency).
+- iter 23.5.8: bench gate — `bench/check.py` exit 0 (clean),
+  `bench/compile_check.py` exit 1 (one sub-ms `check_ms`
+  regression at the tolerance line — see Concerns), `bench/cross_lang.py`
+  exit 0 (clean).
+
+## Concerns
+
+- `bench/compile_check.py` exited 1 with one regression:
+  `check_ms.local_rec_capture` measured +26.36% over baseline
+  (1.1ms → 1.4ms, tolerance 25.0%). This is a sub-millisecond
+  noise-band metric, and the prelude grew by 5 polymorphic
+  `Def::Fn`s in this iter so a measurable typecheck-workload
+  shift is expected per the Boss-noted audit tolerance. Two
+  other check_ms metrics in the first run (`borrow_own_demo`,
+  `bench_list_sum`) crossed the line on one sample but stayed
+  inside on the rerun, confirming this is noise-band fluctuation
+  rather than a structural regression. Recommend ratifying at
+  iter close via `--update-baseline`; flagged as a Boss
+  judgement call.
+- The mono-pass rigid-var skip (Task 3 inline fix) preserves
+  the existing Unit-default for unbound metavars exactly (the
+  `is_empty(Nil)` shape from iter 23.4.8 is untouched). The
+  discrimination is by name prefix (`$m`) which is the same
+  convention `Subst::meta_id` uses; a future schema refactor
+  that drops the prefix convention would silently break the
+  skip rule. Code comment names this.
+- The linearity-side `check_module(&Module)` standalone entry
+  is now `#[cfg(test)]`-gated because production code uses
+  `check_module_with_visible(m, &visible_extra)` instead. Unit
+  tests still call the no-extra path. Acceptable; flagging in
+  case a future caller wants the standalone form back.
+
+## Known debt
+
+- The `eq_ord_user_adt` mono-symbol name (`eq__cde77856`) is
+  pinned by literal string match in the test. If the canonical
+  type-bytes encoding for `IntBox` ever changes (e.g. via a new
+  schema field on `TypeDef`), the test fails with a clear
+  type-mangling-regression message. That is the intended drift
+  alarm; no immediate debt.
+
+## Files touched
+
+- `crates/ailang-check/src/lib.rs` — Float-aware `NoInstance`
+  addendum in `to_diagnostic()`; linearity call site updated to
+  pass workspace siblings as visible-extra.
+- `crates/ailang-check/src/linearity.rs` — new
+  `check_module_with_visible(m, visible_extra)` entry;
+  `check_module(&Module)` made test-only.
+- `crates/ailang-check/src/mono.rs` — free-fn target collection
+  now distinguishes rigid `Type::Var` from `$m`-prefixed
+  metavars; rigid-bearing targets are skipped; new helper
+  `contains_rigid_var`.
+- `crates/ailang-core/src/workspace.rs` — docstring update on
+  the `iter22b1_missing_method` test naming the new `ne` reason
+  for the `TEq`/`tne` rename.
+- `crates/ail/tests/prelude_free_fns.rs` (new) — five workspace-level
+  tests, one per prelude free fn, plus helpers.
+- `crates/ail/tests/eq_ord_e2e.rs` (new) — three E2E tests:
+  polymorphic composition, user-ADT integration, mono-symbol
+  hash stability.
+- `crates/ail/tests/eq_float_noinstance.rs` (new) — Float-aware
+  NoInstance pin.
+- `examples/prelude.ail.json` — five new `Def::Fn` entries
+  (ne / lt / le / gt / ge).
+- `examples/ne_at_int_smoke.ail.json` (new), `lt_at_int_smoke.ail.json`
+  (new), `le_at_str_smoke.ail.json` (new), `gt_at_bool_smoke.ail.json`
+  (new), `ge_at_int_smoke.ail.json` (new) — five workspace-level
+  smoke fixtures.
+- `examples/eq_ord_polymorphic.ail.json` (new) — positive E2E:
+  polymorphic helper composing prelude fns at Int / Bool / Str.
+- `examples/eq_ord_user_adt.ail.json` (new) — user-ADT E2E:
+  `IntBox` with user-written Eq + Ord instances.
+- `examples/eq_float_noinstance.ail.json` (new) — negative-Float
+  fixture firing the addended diagnostic.
+- `examples/test_22b1_missing_method.ail.json` — `ne → tne`
+  rename to avoid collision with the new prelude `ne` free fn.
+- `docs/DESIGN.md` — Milestone-23 amendment paragraph inserted
+  in §"Prelude (built-in) classes".
+- `docs/roadmap.md` — Post-22 Prelude entry split into shipped
+  Eq/Ord + pending Show; Op-routing depends-on reference
+  disambiguated.
+
+## Stats
+
+bench/orchestrator-stats/2026-05-12-iter-23.5.json

docs/roadmap.md

@@ -41,27 +41,23 @@ context. Pick the next milestone from P1.)_
 
 ## P1 — Next
 
-- [ ] **\[milestone\]** Post-22 Prelude — ship `Show` / `Eq` / `Ord`
-  with the three total-orderable primitive instances (Int, Bool, Str);
-  rewire `print` through `Show.show`. Float gets `Show` but **not**
-  `Eq` / `Ord` (partial — see Floats milestone). Originally queued
-  as 22b.4 in the typeclass milestone, kept on hold pending demand.
-  - context: JOURNAL 2026-05-09 ("JOURNAL queue"). Floats milestone
-    closed 2026-05-10 — partial-Eq/Ord-for-Float story is documented
-    in DESIGN.md §"Float semantics", so the Prelude can decide
-    what's instanced (Show: yes, Eq/Ord: no for Float).
-  - context: Iter 23.1-23.3 shipped Ordering ADT, Eq / Ord classes,
-    primitive instances on Int / Bool / Str, and runtime helpers
-    (`ail_str_eq` / `compare`). Remaining: polymorphic free fns
-    (`ne` / `lt` / `le` / `gt` / `ge`), `Show` class, `print`
-    rewire. The original Spec-23 draft was retired 2026-05-11
-    because it silently assumed polymorphic free fns are
-    mono-specialised the same way as class methods; that assumption
-    is false today. Re-brainstorm pending — `ailang-grounding-check`
-    (gc.1) will be the gating mechanism on the new draft.
-  - depends on: polymorphic-free-fn mono-specialisation (symmetric
-    to class-method monomorphisation in 22b.3) — not currently
-    ratified by any green test.
+- [x] **\[milestone\]** Post-22 Prelude — Eq/Ord — shipped milestone
+  23 (2026-05-12). `Ordering` ADT, `Eq`/`Ord` classes, primitive
+  instances on Int / Bool / Str, polymorphic free fns
+  `ne`/`lt`/`le`/`gt`/`ge`, runtime `ail_str_eq` + `ail_str_compare`,
+  end-to-end coverage including user-ADT-instance integration. Float
+  has neither instance by design; polymorphic helpers at Float fire
+  Float-aware `NoInstance` per DESIGN.md §"Float semantics".
+
+- [ ] **\[milestone\]** Post-22 Prelude — Show + print rewire — ship
+  `Show` typeclass with `Show Int/Bool/Str/Float` instances; rewire
+  `print` through `Show.show`. Gated on heap-`Str` ABI runtime work
+  (`int_to_str` needs to allocate). Originally queued as 22b.4 in
+  the typeclass milestone, kept on hold pending demand and the
+  heap-`Str` prerequisite.
+  - context: brainstorm 2026-05-12 (iter 23.5 wrap). Heap-`Str` ABI
+    is the load-bearing prerequisite; until it ships, `Show Int`
+    cannot allocate a `Str` to return.
 
 ## P2 — Medium-term
 
@@ -70,7 +66,7 @@ context. Pick the next milestone from P1.)_
   primitive comparators. No commitment; gated on bench re-baselining
   to make sure the indirection doesn't tank latency.
   - context: JOURNAL 2026-05-09
-  - depends on: Post-22 Prelude
+  - depends on: Post-22 Prelude — Eq/Ord (shipped 23.5)
 - [ ] **\[todo\]** `types` / `ctor_index` overlay shape question —
   decide whether the env's two parallel ctor maps should collapse
   into one overlay, or stay split. Surfaced during the