spec: floats — operators polymorphic over {Int, Float} + NaN/Inf constants + is_nan

Mainstream-aligns the Float surface: + - * / < <= > >= become
forall-quantified with codegen-dispatch on Int|Float (parallel to
today's == path), instead of the original draft's wort-style
fadd/flt/etc. Adds nan/inf/neg_inf as builtin constants and
is_nan : (Float) -> Bool. % stays Int-only (no fmod yet).

Iteration plan now flags iter 3 and iter 4 as widening passes
that must hold the no-Int-regression line.

docs/specs/2026-05-10-floats.md

@@ -101,54 +101,121 @@ Negative float literals follow today's negative-int rule
 digit as part of a numeric token), so `-1.5` lexes as a single
 `Tok::Float`.
 
-### A3 — Builtin operators: no overloading, explicit f-prefix
+### A3 — Builtin operators: polymorphic over `{Int, Float}` via codegen-dispatch
 
-| Domain | Int (existing) | Float (new) |
+The arithmetic and comparison operators that today are
+monomorphic-Int (`+`, `-`, `*`, `/`, `<`, `<=`, `>`, `>=`) are
+**widened to polymorphic** with the same shape and dispatch
+mechanism the existing `==` / `!=` already use:
+
+```
++   : forall a. (a, a) -> a       -- Int|Float; reject otherwise
+-   : forall a. (a, a) -> a       -- Int|Float
+*   : forall a. (a, a) -> a       -- Int|Float
+/   : forall a. (a, a) -> a       -- Int|Float
+<   : forall a. (a, a) -> Bool    -- Int|Float
+<=  : forall a. (a, a) -> Bool    -- Int|Float
+>   : forall a. (a, a) -> Bool    -- Int|Float
+>=  : forall a. (a, a) -> Bool    -- Int|Float
+==  : forall a. (a, a) -> Bool    -- existing; Float arm added
+!=  : forall a. (a, a) -> Bool    -- existing; Float arm added
+%   : (Int, Int) -> Int            -- stays monomorphic (no fmod yet)
+```
+
+Codegen dispatches on the resolved argument type at the call
+site, parallel to today's `==` path (`crates/ailang-codegen/src/
+lib.rs:2244-2266`):
+
+| Op | Int arm | Float arm |
 |---|---|---|
-| Arithmetic | `+ - * / %` | `fadd fsub fmul fdiv fneg` |
+| `+` | `add i64` | `fadd double` |
-| Equality | `== !=` (polymorphic, codegen-dispatched) | (same — codegen arm extended) |
+| `-` | `sub i64` | `fsub double` |
-| Ordering | `< <= > >=` (Int-only) | `flt fle fgt fge` |
+| `*` | `mul i64` | `fmul double` |
+| `/` | `sdiv i64` | `fdiv double` |
+| `==` | existing `icmp eq i64` / `i1` / `@strcmp` / `i1 1` | `fcmp oeq double` |
+| `!=` | derived from `==` | `fcmp one double` |
+| `<` | `icmp slt i64` | `fcmp olt double` |
+| `<=` | `icmp sle i64` | `fcmp ole double` |
+| `>` | `icmp sgt i64` | `fcmp ogt double` |
+| `>=` | `icmp sge i64` | `fcmp oge double` |
+
+Non-{Int,Float} resolutions for `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=`
+get rejected at codegen with the same diagnostic shape the `==`
+path uses today (`"+ not supported for type X"`). The reject
+keeps the polymorphism honest — there is no silent fallback,
+no string-concatenation-via-`+`, no boolean-arithmetic-via-`+`.
 
 Rationale:
 
-- AILang already rejects operator overloading
+- **Mainstream alignment.** Every LLM-relevant programming
-  (`docs/DESIGN.md` "Feature-acceptance criterion"). A
+  language (Rust, Java, C, Python, JavaScript, Haskell, Swift,
-  polymorphic `+ : forall a. (a, a) -> a` would either need
+  OCaml-via-typeclass-like-extension) accepts `1.5 + 2.5`. An
-  ad-hoc constraints (the typeclass story, out of scope here) or
+  AILang where the LLM-author has to write `(fadd 1.5 2.5)` is
-  a hard-coded Int|Float type spec-case in the typechecker. Both
+  a high-friction first-try-error surface. The user-facing
-  cost more than two-name disambiguation.
+  decision (this conversation, 2026-05-10) chose Mainstream
-- The `==`/`!=` codegen-dispatch path already exists
+  alignment over the explicit-naming purity of an earlier draft.
-  (`crates/ailang-check/src/builtins.rs:78`,
+- **Precedent already in tree.** The `==` builtin is
-  `crates/ailang-codegen/src/lib.rs:2244-2266`). Extending the
+  `forall a. (a, a) -> Bool` with a hardcoded Int|Bool|Str|Unit
-  arm is one branch addition; introducing `feq`/`fne` would be a
+  codegen dispatch and explicit reject for ADT/Fn equality
-  duplication of an already-polymorphic site for no semantic
+  (`builtins.rs:75-77`). The widening of `+`/`-`/etc. uses the
-  gain. IEEE-conformant `==` (NaN == NaN ⇒ false) falls out of
+  *same* mechanism — no new architectural surface, just more
-  LLVM `fcmp oeq` directly.
+  arms in the existing dispatch helper.
-- `<`/`<=`/`>`/`>=` on Int are monomorphic today, so widening
+- **Typeclass migration story.** When typeclasses ship
-  them to polymorphic-Int|Float would require a *new* dispatch
+  (Post-22 Prelude + 22c), the hardcoded `Int|Float` spec-case
-  path. Cheaper and more honest to add `flt`/`fle`/`fgt`/`fge`
+  in the typechecker can be cleanly replaced by a `Num a`
-  alongside.
+  constraint. Surface (`(+ 1.5 2.5)`) does not change. The
-- `fmod` is **excluded** for this milestone. IEEE 754-2008
+  spec-case is transitional, not load-bearing.
-  remainder semantics (`fmod` vs `remainder`) are subtle enough
+- **`%` stays monomorphic.** IEEE `frem` (LLVM op for `fmod`)
-  to deserve their own decision; not blocking the milestone on
+  has subtle semantics (sign-of-result-follows-dividend,
-  it.
+  ±0 / ±Inf edge cases) that deserve their own decision; out
+  of scope for this milestone.
 
-Builtin signatures (added to
+Other new builtins:
-`crates/ailang-check/src/builtins.rs::install`):
 
 ```
-fadd : (Float, Float) -> Float
+neg                   : forall a. (a) -> a       -- Int|Float; reject otherwise
-fsub : (Float, Float) -> Float
-fmul : (Float, Float) -> Float
-fdiv : (Float, Float) -> Float
-fneg : (Float) -> Float
-flt  : (Float, Float) -> Bool
-fle  : (Float, Float) -> Bool
-fgt  : (Float, Float) -> Bool
-fge  : (Float, Float) -> Bool
 int_to_float          : (Int) -> Float
 float_to_int_truncate : (Float) -> Int
 float_to_str          : (Float) -> Str
+is_nan                : (Float) -> Bool          -- LLVM `fcmp uno double %x, %x`
+```
+
+The unary `neg` is widened the same way arithmetic ops are
+(today there is no `neg` builtin — unary minus is desugared from
+the surface lexer's `-<digits>` rule into a literal or via
+`(- 0 x)`-style desugar; the spec adds an explicit `neg` so
+Float negation has a name without the `(- 0.0 x)` workaround,
+which is wrong for `-0.0`). The plan picks the desugar/builtin
+boundary.
+
+New builtin float constants (always-in-scope `Term::Var`
+references, parallel to today's `__unreachable__`):
+
+```
+nan      : Float    -- bits 7ff8000000000000 (canonical quiet NaN)
+inf      : Float    -- bits 7ff0000000000000
+neg_inf  : Float    -- bits fff0000000000000
+```
+
+Rationale for the constants:
+
+- Every Mainstream language exposes them (`f64::NAN`,
+  `Double.NaN`, `float('nan')`, `NaN`, `Double.nan`).
+  Withholding them while shipping the IEEE-conformant
+  semantics that *make them necessary* is a pointless friction.
+- Hex bits via Form-A still works as the ground truth, but
+  surface-level `(var nan)` lets the LLM-author write code that
+  reads like every other language's float code.
+- Names are lowercase (`nan`, not `NaN`) so they're regular
+  identifiers, no surface-lex special-case. `neg_inf` instead
+  of `-inf` because `-` cannot start a value identifier (the
+  surface-lex `-<digits>` rule applies to numeric literals
+  only).
+
+Effect ops (added):
+
+```
+io/print_float : (Float) -> Unit !IO    -- new
 ```
 
 ### A4 — Conversions: total, foot-gun-free
@@ -269,37 +336,66 @@ the plan for iteration boundaries.
 - `lib.rs` (4457 LoC) — `Literal::Float` is well-typed at
   `Type::float()`. Add the one-arm extension to whatever
   `Term::Lit` typing helper exists.
-- `builtins.rs` (183 LoC) — install all twelve new entries (per
+- `builtins.rs` (183 LoC) — three classes of change:
-  A3). Extend `list()` accordingly so `ail builtins` reflects
+  1. **Widen** the existing arithmetic and comparison entries
-  them. The `==` polymorphic entry needs no change here — the
+     `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=` from monomorphic Int to
-  signature stays `forall a. (a, a) -> Bool`; the codegen
+     `forall a. (a, a) -> a` (or `... -> Bool`) — same shape
-  side (below) handles the new Float arm.
+     as today's `==` entry. Existing `==`/`!=` entries
+     unchanged in signature; their dispatch arm gets extended
+     codegen-side.
+  2. **Install** the new builtins: `neg` (polymorphic),
+     `int_to_float`, `float_to_int_truncate`, `float_to_str`,
+     `is_nan`, plus the three constants `nan`, `inf`,
+     `neg_inf` (each a `Term::Var`-resolvable global at
+     `Type::float()`, parallel to `__unreachable__`).
+  3. **Install** the new effect op `io/print_float`.
+
+  Extend `list()` accordingly so `ail builtins` reflects every
+  added entry. The `list()` strings serve as the LLM-author's
+  contract — they must be accurate after this iteration.
 
 ### `crates/ailang-codegen/`
 
-- `lib.rs` (2877 LoC) — six new lowering paths:
+- `lib.rs` (2877 LoC) — six lowering changes:
   1. **Float literal** (`Literal::Float { bits }`) → emit
      `double` constant via LLVM hex-float syntax
      `0x1p+0`-style or via `bitcast i64 0x... to double`.
      Sites: every place `Literal::Int { value }` is matched
      today (lines 918, 1215).
-  2. **Arithmetic builtins** `fadd/fsub/fmul/fdiv/fneg` →
+  2. **Widen arithmetic dispatch.** `+`/`-`/`*`/`/` are
-     LLVM `fadd double`, `fsub double`, `fmul double`,
+     today lowered as monomorphic Int instructions
-     `fdiv double`, `fneg double`. Site: parallel to the
+     (line 1745 region). Convert the lowering site into a
-     `t_add` / `+` lowering (line 1745 region).
+     type-dispatched helper analogous to the existing `==`
-  3. **Comparison builtins** `flt/fle/fgt/fge` → LLVM
+     dispatch (`lib.rs:2244-2266`): Int arm emits
-     `fcmp olt`, `fcmp ole`, `fcmp ogt`, `fcmp oge`
+     `add/sub/mul/sdiv i64`, Float arm emits
-     (ordered, so NaN compares yield `false`).
+     `fadd/fsub/fmul/fdiv double`, anything else fails with
+     `"<op> not supported for type X"`.
+  3. **Widen comparison dispatch.** `<`/`<=`/`>`/`>=` get the
+     same treatment: Int arm `icmp s{lt,le,gt,ge} i64`, Float
+     arm `fcmp o{lt,le,gt,ge} double`, reject otherwise.
   4. **`==` / `!=` Float arm** in the existing dispatch
      (line 2263 region) → `fcmp oeq` / `fcmp one` for the
-     `Float` case. Add the case alongside the existing
+     `Float` case, alongside the existing arms.
-     `"Int"` / `"Bool"` / `"Str"` / `"Unit"` arms.
+  5. **`neg` polymorphic** — Int arm `sub i64 0, %x`, Float
-  5. **Conversions** `int_to_float` → `sitofp i64 to double`;
+     arm `fneg double %x` (correct for `-0.0`, unlike a
-     `float_to_int_truncate` → `call double @llvm.fptosi.sat.i64`
+     hypothetical `(- 0.0 x)` desugar). Reject other types.
-     (or the legalised equivalent).
+  6. **Conversions and IO**:
-  6. **`io/print_float`** effect-op lowering parallel to
+     - `int_to_float` → `sitofp i64 ... to double`.
-     `io/print_int` (line 2150 region) → call into runtime C
+     - `float_to_int_truncate` → `@llvm.fptosi.sat.i64.f64`
-     glue.
+       intrinsic (or the legalised cast sequence if the
+       target backend doesn't expose it directly).
+     - `is_nan` → `fcmp uno double %x, %x` (returns `i1`,
+       which already coerces to AILang `Bool`).
+     - `float_to_str` → call into runtime C glue
+       `@ail_float_to_str`.
+     - `io/print_float` → parallel to `io/print_int`
+       (line 2150 region) → call into runtime C glue
+       `@ail_print_float`.
+  7. **Float constants** `nan`/`inf`/`neg_inf` lower as
+     `Term::Var` references resolving to compile-time `double`
+     constants (the codegen path that resolves `Var "x"` to
+     the SSA value of a global gets a builtin-constant arm,
+     same way `__unreachable__` resolves to `unreachable`).
 - ADT / container layout — `double` is 8 bytes, fits the
   existing 8-byte slot used for `i64` and `ptr`. **No layout
   change.** Confirm this by inspecting how `List<Int>` lowers
@@ -315,13 +411,21 @@ the plan for iteration boundaries.
 ### `runtime/`
 
 - New file `runtime/print_float.c` (or extend an existing C
-  file) — `void ail_print_float(double v)` that writes the
+  file) — two functions:
-  shortest round-trippable decimal followed by a newline. We
+  - `void ail_print_float(double v)` — write shortest
-  vendor a small `ryu`-style implementation, or — if simpler —
+    round-trippable decimal + newline.
-  use `printf("%.17g\n", v)` for the milestone and revisit if
+  - `const char *ail_float_to_str(double v)` — return a
-  the redundancy is a problem.
+    heap-allocated AILang `Str` of the shortest
-- The RC runtime (`rc.c`, `bump.c`) is **not touched**. Float
+    round-trippable decimal (no newline). Refcounted as any
-  is a value type with no heap allocation per literal.
+    other `Str` in the runtime.
+
+  Implementation: vendor a small `ryu`-style routine, or — if
+  simpler — use `snprintf("%.17g", v)` for the milestone and
+  revisit if the redundancy is a problem. Plan-time call.
+- The RC runtime (`rc.c`, `bump.c`) is **not touched** by the
+  Float value path itself. Float is a value type with no heap
+  allocation per literal. The `ail_float_to_str` glue allocates
+  a `Str`, but uses the existing `Str` runtime path.
 
 ### `crates/ail/` (CLI)
 
@@ -437,20 +541,20 @@ fixes the *property set* that must be covered.
 
 ### IEEE-conformance properties
 
-- `(fadd 0.1 0.2)` produces the exact `bits` of
+- `(+ 0.1 0.2)` produces the exact `bits` of
   `0.1_f64 + 0.2_f64` (i.e. `bits == 0x3fd3333333333334`, not
   `0x3fd3333333333333`). A single `fadd` cannot be FMA-contracted
   (no `c` operand to absorb), so the result is bit-stable per A5.
-- `==` on the same NaN bit pattern (passed in as a Float literal)
+- `(== nan nan)` returns `false`. `(!= nan nan)` returns `true`.
-  returns `false`. `!=` on the same NaN literal returns `true`.
+- `<`, `<=`, `>`, `>=` all return `false` when either
-- `flt`, `fle`, `fgt`, `fge` all return `false` when either
+  argument is NaN (ordered comparisons via `fcmp o*`).
-  argument is NaN (ordered comparisons).
+- `(/ 1.0 0.0)` produces `+inf` (bits `7ff0000000000000`);
-- `(fdiv 1.0 0.0)` produces `+inf` (bits `7ff0000000000000`);
+  `(/ -1.0 0.0)` produces `-inf` (bits `fff0000000000000`);
-  `(fdiv -1.0 0.0)` produces `-inf` (bits `fff0000000000000`);
+  `(/ 0.0 0.0)` produces *some* NaN (test asserts
-  `(fdiv 0.0 0.0)` produces *some* NaN (test asserts
+  `(is_nan result) == true`, **not** specific NaN bits —
-  `(fne result result) == true` per IEEE NaN-detection idiom,
+  A5 leaves the qNaN payload unspecified).
-  **not** specific NaN bits — A5 leaves the qNaN payload
+- `(is_nan nan) == true`. `(is_nan 1.0) == false`.
-  unspecified).
+  `(is_nan inf) == false`. `(is_nan neg_inf) == false`.
 - `+0.0` and `-0.0` hash distinctly in Form-A but compare equal
   via `==`.
 
@@ -491,8 +595,14 @@ The milestone is closeable when **all** of the following hold:
 2. `Literal::Float { bits: u64 }` is serialised as
    `{"bits":"<16-hex>","kind":"float"}` in canonical JSON. The
    round-trip test passes.
-3. The twelve new builtins (per A3) appear in
+3. `ail builtins` output reflects:
-   `ail builtins` output.
+   (a) widened signatures for `+`, `-`, `*`, `/`, `<`, `<=`,
+       `>`, `>=` (now `forall a. (a, a) -> a` /
+       `forall a. (a, a) -> Bool`);
+   (b) new builtins: `neg`, `int_to_float`,
+       `float_to_int_truncate`, `float_to_str`, `is_nan`;
+   (c) new constants: `nan`, `inf`, `neg_inf`;
+   (d) new effect op: `io/print_float`.
 4. `examples/floats.ail.json` builds, runs, and produces the
    expected stdout (printed floats round-trip the literal
    forms).
@@ -519,15 +629,12 @@ Out of scope, explicitly:
   gets `Show` in the next milestone; `Eq` and `Ord` will
   *intentionally* not exist for `Float` because of A5 +
   user-fixed constraint #2.)
-- Polymorphic numeric class (`Num`).
+- Polymorphic numeric class (`Num`). The hardcoded
+  `{Int, Float}` spec-case in the typechecker is transitional
+  scaffolding; replaced by a proper `Num a` constraint when
+  typeclass machinery picks up arithmetic in 22c.
 - `f32`.
-- `fmod` / IEEE-`remainder`.
+- `fmod` / IEEE-`remainder`. `%` stays Int-only this milestone.
-- NaN-detection builtin (`is_nan`); NaN-construction builtin.
-  Workaround in scope: `(fne x x)` is `true` iff `x` is NaN
-  (the canonical IEEE NaN test). Documented in
-  §"Float semantics".
-- `Float.nan` / `Float.infinity` named constants — these come
-  with the eventual Float stdlib, not the primitive milestone.
 - `print` rewiring through `Show.show` — that is Post-22
   Prelude.
 - Pattern-matching on Float literals (`Pattern::Lit { lit:
@@ -540,25 +647,40 @@ Out of scope, explicitly:
   IEEE-`==` semantics, which the LLM-author has to remember.
   Either way: this milestone explicitly does NOT introduce a
   Float-pattern *idiom* — the documented way to discriminate
-  Floats is via the comparison builtins (`flt`/`fle`/...) and
+  Floats is via the comparison operators (`<`/`>`/...) and
-  the NaN-detection idiom `(fne x x)`.
+  `(is_nan x)`.
 
 ## Notes for the plan
 
 The plan should sequence iterations roughly:
 
 - **Iteration 1**: AST + canonical + primitives (the schema
-  layer). Pure schema, RED-first by canonical-bytes test.
+  layer). Pure schema, RED-first by canonical-bytes test for
+  `Literal::Float`.
 - **Iteration 2**: Surface lex + parse + print round-trip.
   RED-first by `lex(print(L)) == L` property.
-- **Iteration 3**: Type + builtins install. RED-first by
+- **Iteration 3**: Type + builtins install. Two distinct
-  typecheck unit test on `(fadd 1.0 2.0) : Float`.
+  sub-tasks:
-- **Iteration 4**: Codegen (literal + arithmetic + comparison +
+  (a) **widen** existing `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=` to
-  conversion + IO). RED-first by E2E
+      polymorphic; **don't break** existing Int-only fixtures;
-  `examples/floats.ail.json`.
+  (b) install new builtins (`neg`, conversions, `is_nan`,
+      constants) and `io/print_float`.
+  RED-first by typecheck unit test on `(+ 1.0 2.0) : Float`
+  AND `(+ 1 2) : Int` (regression).
+- **Iteration 4**: Codegen widening + Float lowering paths.
+  Same widen-vs-add split as iteration 3 — codegen for
+  `+`/`-`/`*`/`/` becomes type-dispatched, plus Float arms for
+  comparison, conversion, IO, and constants. RED-first by E2E
+  `examples/floats.ail.json` AND existing Int E2E fixtures
+  staying GREEN (regression gate).
 - **Iteration 5**: Prose + DESIGN.md + drift-test extension +
   rustdoc.
 
+Note the regression-gate emphasis on iterations 3 and 4: this
+milestone *widens* operators that are today monomorphic. Every
+existing Int-using fixture must keep working bit-identical.
+The plan should pin a "no Int regression" property explicitly.
+
 Iteration boundaries are the plan's call. The five-cluster
 shape above is the spec's scope estimate, not a binding
 sequence.