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

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::Fns, 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::Fns 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::Fns 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