# Floats Iteration 3 — Typecheck + Builtins (Implementation Plan)

> **Parent spec:** `docs/specs/2026-05-10-floats.md` (committed
> `e37366f`, approved 2026-05-10) — section A3 + the
> `crates/ailang-check/` Components subsection.
>
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
> to run this plan. Steps use `- [ ]` checkboxes for tracking.

**Goal:** Widen the existing arithmetic / comparison builtins
(`+`, `-`, `*`, `/`, `!=`, `<`, `<=`, `>`, `>=`) from monomorphic
`(Int, Int) -> {Int,Bool}` to polymorphic `forall a. (a, a) -> a`
(resp. `forall a. (a, a) -> Bool`), install the new Float builtins
(`neg`, `int_to_float`, `float_to_int_truncate`, `float_to_str`,
`is_nan`), install the three Float constants (`nan`, `inf`,
`neg_inf`) and the `io/print_float` effect op, and hard-reject
`Pattern::Lit { lit: Literal::Float { .. } }` at the typechecker.

**Architecture:** The widening uses the same
`Type::Forall { vars: ["a"], body: Type::Fn { params: [a, a], ret:
.. } }` shape `==` already has. The check-side install at
`crates/ailang-check/src/builtins.rs::install` and the codegen-side
parallel table at `crates/ailang-codegen/src/synth.rs::builtin_ail_type`
stay in lockstep. The actual {Int, Float} arg-type filtering happens
at codegen (iter 4) — typecheck accepts any matching pair (mirrors
how `==` works today). The `Pattern::Lit::Float` rejection adds a
new `CheckError::FloatPatternNotAllowed` variant; the iter-1
compile-completeness arm (`Literal::Float { .. } => Type::float()`)
is replaced with an `Err` return. No codegen *lowering* changes —
iter 3 only updates the type metadata the codegen consults.

**Tech Stack:** `crates/ailang-check/` (`builtins.rs`, `lib.rs`),
`crates/ailang-codegen/` (`synth.rs` — type metadata only). No
runtime, no LLVM IR emission.

**No-regression invariant:** `cargo test --workspace` must stay
GREEN after EACH task. The widening must not change the resolved
type of any existing Int-only call site — a polymorphic `+` of
type `forall a. (a, a) -> a` instantiated at `(Int, Int)` returns
`Int`, identical to the pre-widening monomorphic shape. End-to-end
Int fixtures (`examples/*.ail.json`) and the codegen `builtin_binop`
Int table stay untouched.

---

## Files this plan creates or modifies

- Modify: `crates/ailang-check/src/builtins.rs` — widen `install`
  arithmetic / comparison entries, add 5 new builtin-fn entries
  (`neg`, `int_to_float`, `float_to_int_truncate`, `float_to_str`,
  `is_nan`), add 3 new constant entries (`nan`, `inf`, `neg_inf`),
  add 1 new effect-op entry (`io/print_float`); refresh `list()`
  display strings to match.
- Modify: `crates/ailang-codegen/src/synth.rs` — widen
  `builtin_ail_type` arithmetic / comparison entries (lockstep
  mirror), add 5 new builtin-fn entries, add 3 new constant entries,
  extend `builtin_effect_op_ret` to include `io/print_float`.
- Modify: `crates/ailang-check/src/lib.rs` — add
  `CheckError::FloatPatternNotAllowed` variant; replace the
  iter-1 `Literal::Float { .. } => Type::float()` arm at line 2312
  with an `Err(CheckError::FloatPatternNotAllowed)` return.
- Modify: `docs/JOURNAL.md` — append iteration-close entry.

No file outside this list is touched.

---

## Task 1: WIDEN existing arithmetic / comparison builtins to polymorphic

**Files:**
- Modify: `crates/ailang-check/src/builtins.rs:50-70` (install of
  `+`/`-`/`*`/`/`/`%`/`!=`/`<`/`<=`/`>`/`>=`), `:164-183` (list).
- Modify: `crates/ailang-codegen/src/synth.rs:61-114`
  (builtin_ail_type, the `+ | - | * | / | %` and `!= | < | <= | > | >=`
  arms at lines 77-78).

- [ ] **Step 1: Write the RED widening test**

In `crates/ailang-check/src/builtins.rs`, append a `#[cfg(test)] mod
tests` block at the file end (no test mod exists currently per
`grep "^#\[cfg(test)\]\|^mod tests" crates/ailang-check/src/builtins.rs`):

```rust
#[cfg(test)]
mod tests {
    use super::*;
    use crate::Env;
    use ailang_core::ast::{Literal, Term};

    /// Synthesize the type of a small expression in a fresh Env that
    /// has only the builtins installed (no user defs). Returns the
    /// fully-applied result type; effects ignored for this helper.
    fn synth_in_builtins_env(t: &Term) -> Type {
        let mut env = Env::default();
        install(&mut env);
        crate::synth_term(&env, t).expect("synth").0
    }

    fn lit_int(v: i64) -> Term {
        Term::Lit { lit: Literal::Int { value: v } }
    }
    fn lit_float(bits: u64) -> Term {
        Term::Lit { lit: Literal::Float { bits } }
    }
    fn app(callee: &str, args: Vec<Term>) -> Term {
        Term::App {
            callee: Box::new(Term::Var { name: callee.into() }),
            args,
            tail: false,
        }
    }

    /// Iter 22-floats.3: regression — `(+ 1 2)` still resolves to
    /// `Int` after the widening from `(Int, Int) -> Int` to
    /// `forall a. (a, a) -> a`.
    #[test]
    fn widen_plus_keeps_int_int_int() {
        let ty = synth_in_builtins_env(&app("+", vec![lit_int(1), lit_int(2)]));
        assert_eq!(ty, Type::int(), "(+ 1 2) must still type as Int");
    }

    /// Iter 22-floats.3: new acceptance — `(+ 1.5 2.5)` types as
    /// `Float`. Pre-widening this would have failed with
    /// `TypeMismatch`.
    #[test]
    fn widen_plus_accepts_float_float_float() {
        let bits = 1.5_f64.to_bits();
        let ty = synth_in_builtins_env(&app("+", vec![lit_float(bits), lit_float(bits)]));
        assert_eq!(ty, Type::float(), "(+ 1.5 2.5) must type as Float");
    }

    /// Iter 22-floats.3: regression — `(< 1 2)` still resolves to
    /// `Bool` after the widening to `forall a. (a, a) -> Bool`.
    #[test]
    fn widen_lt_keeps_int_int_bool() {
        let ty = synth_in_builtins_env(&app("<", vec![lit_int(1), lit_int(2)]));
        assert_eq!(ty, Type::bool_(), "(< 1 2) must still type as Bool");
    }

    /// Iter 22-floats.3: new acceptance — `(< 1.5 2.5)` types as
    /// `Bool`.
    #[test]
    fn widen_lt_accepts_float_float_bool() {
        let bits = 1.5_f64.to_bits();
        let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits), lit_float(bits)]));
        assert_eq!(ty, Type::bool_(), "(< 1.5 1.5) must type as Bool");
    }
}
```

If `crate::synth_term` is private or has a different signature, use
the lowest-overhead public typecheck entry point — read the top of
`crates/ailang-check/src/lib.rs` to find the right helper. Most
likely `synth_term` is `pub(crate)` and visible to a same-crate
`mod tests`. If not, switch to `crate::check::synth_term` or
construct a minimal `Module` and call `crate::check_module`.

- [ ] **Step 2: Run tests to verify RED**

Run: `cargo test -p ailang-check --lib builtins::tests`
Expected: 2 of 4 tests FAIL — `widen_plus_accepts_float_float_float`
and `widen_lt_accepts_float_float_bool` fail with a
`TypeMismatch { expected: "Int", got: "Float" }` panic. The two
regression tests (`widen_plus_keeps_int_int_int`,
`widen_lt_keeps_int_int_bool`) pass.

- [ ] **Step 3: Widen the check-side install**

In `crates/ailang-check/src/builtins.rs`, replace the block at
lines 51-70 (the `int_int_int` / `int_int_bool` constructors and
the two `for` loops) with:

```rust
    // Iter 22-floats.3: arithmetic and comparison ops are polymorphic.
    // Same shape as `==` below — the {Int, Float}-restriction is
    // enforced at codegen, not at typecheck. `%` stays Int-only
    // (no fmod yet — see spec section A3).
    let poly_a_a_to_a = || 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::Var { name: "a".into() }),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        }),
    };
    let poly_a_a_to_bool = || 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,
        }),
    };
    let int_int_int = Type::Fn {
        params: vec![Type::int(), Type::int()],
        ret: Box::new(Type::int()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ailang_core::ast::ParamMode::Implicit,
    };
    for op in ["+", "-", "*", "/"] {
        env.globals.insert(op.into(), poly_a_a_to_a());
    }
    env.globals.insert("%".into(), int_int_int);
    for op in ["!=", "<", "<=", ">", ">="] {
        env.globals.insert(op.into(), poly_a_a_to_bool());
    }
```

The `int_int_bool` local is gone (its only consumer, the `!=` /
ordering loop, now uses `poly_a_a_to_bool`).

- [ ] **Step 4: Widen the codegen-side type table**

In `crates/ailang-codegen/src/synth.rs`, replace the
`int_int_int` / `int_int_bool` closures and the two arithmetic /
comparison match arms at lines 62-78:

```rust
    // Iter 22-floats.3: same widening as `crates/ailang-check/src/
    // builtins.rs` — `+`/`-`/`*`/`/` and `!=`/`<`/`<=`/`>`/`>=` are
    // polymorphic. `%` stays monomorphic-Int. Codegen lowering for
    // these ops still goes through `builtin_binop` (Int-only) in
    // iter 3; iter 4 converts that to type-dispatched.
    let poly_a_a_to_a = || 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::Var { name: "a".into() }),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        }),
    };
    let poly_a_a_to_bool = || 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: ParamMode::Implicit,
        }),
    };
    let int_int_int = || Type::Fn {
        params: vec![Type::int(), Type::int()],
        ret: Box::new(Type::int()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ParamMode::Implicit,
    };
    Some(match name {
        "+" | "-" | "*" | "/" => poly_a_a_to_a(),
        "%" => int_int_int(),
        "!=" | "<" | "<=" | ">" | ">=" => poly_a_a_to_bool(),
```

The rest of the match (`==`, `not`, `__unreachable__`, fallback)
stays unchanged.

- [ ] **Step 5: Refresh `list()` display strings**

In `crates/ailang-check/src/builtins.rs`, replace lines 165-176
(the arithmetic / comparison rows in `list()`):

```rust
    vec![
        ("+", "forall a. (a, a) -> a"),
        ("-", "forall a. (a, a) -> a"),
        ("*", "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"),
        ("io/print_int", "(Int) -> Unit !IO  [effect op]"),
        ("io/print_bool", "(Bool) -> Unit !IO  [effect op]"),
        ("io/print_str", "(Str) -> Unit !IO  [effect op]"),
    ]
```

- [ ] **Step 6: Verify all four widening tests now GREEN**

Run: `cargo test -p ailang-check --lib builtins::tests`
Expected: all 4 tests PASS.

- [ ] **Step 7: Verify no workspace regression**

Run: `cargo test --workspace`
Expected: 383 passed, 0 failed (matches iter-2-close baseline).
Specifically: every existing `examples/*.ail.json` Int-using
fixture continues to pass — the polymorphic `+` instantiated at
`(Int, Int)` returns `Int`, bit-identical to the pre-widening
shape. Codegen lowering is unchanged (iter 4 widens the
`builtin_binop` table; iter 3 leaves it Int-only).

- [ ] **Step 8: Commit**

```bash
git add crates/ailang-check/src/builtins.rs \
        crates/ailang-codegen/src/synth.rs
git commit -m "floats iter 3.1: widen +/-/*/// and !=/</<=/>/>= to polymorphic forall a"
```

---

## Task 2: INSTALL new Float builtins (`neg`, `int_to_float`, `float_to_int_truncate`, `float_to_str`, `is_nan`)

**Files:**
- Modify: `crates/ailang-check/src/builtins.rs` — `install`
  function and `list` function.
- Modify: `crates/ailang-codegen/src/synth.rs` —
  `builtin_ail_type`.

- [ ] **Step 1: Write the RED test for the five new builtins**

In `crates/ailang-check/src/builtins.rs::tests`, append:

```rust
/// Iter 22-floats.3: `neg` is polymorphic — `forall a. (a) -> a`.
/// Both `(neg 5) : Int` and `(neg 1.5) : Float` typecheck.
#[test]
fn install_neg_is_polymorphic() {
    let ty_int = synth_in_builtins_env(&app("neg", vec![lit_int(5)]));
    assert_eq!(ty_int, Type::int(), "(neg 5) must type as Int");
    let bits = 1.5_f64.to_bits();
    let ty_float = synth_in_builtins_env(&app("neg", vec![lit_float(bits)]));
    assert_eq!(ty_float, Type::float(), "(neg 1.5) must type as Float");
}

/// Iter 22-floats.3: `int_to_float : (Int) -> Float`.
#[test]
fn install_int_to_float_signature() {
    let ty = synth_in_builtins_env(&app("int_to_float", vec![lit_int(5)]));
    assert_eq!(ty, Type::float(), "(int_to_float 5) must type as Float");
}

/// Iter 22-floats.3: `float_to_int_truncate : (Float) -> Int`.
/// Saturating truncation toward zero per spec A4 — typecheck only
/// cares about the signature here; semantics is iter 4's
/// codegen lowering.
#[test]
fn install_float_to_int_truncate_signature() {
    let bits = 1.5_f64.to_bits();
    let ty = synth_in_builtins_env(&app("float_to_int_truncate", vec![lit_float(bits)]));
    assert_eq!(ty, Type::int(), "(float_to_int_truncate 1.5) must type as Int");
}

/// Iter 22-floats.3: `float_to_str : (Float) -> Str`.
#[test]
fn install_float_to_str_signature() {
    let bits = 1.5_f64.to_bits();
    let ty = synth_in_builtins_env(&app("float_to_str", vec![lit_float(bits)]));
    assert_eq!(ty, Type::str_(), "(float_to_str 1.5) must type as Str");
}

/// Iter 22-floats.3: `is_nan : (Float) -> Bool`. Codegen lowers to
/// `fcmp uno double %x, %x` in iter 4.
#[test]
fn install_is_nan_signature() {
    let bits = 1.5_f64.to_bits();
    let ty = synth_in_builtins_env(&app("is_nan", vec![lit_float(bits)]));
    assert_eq!(ty, Type::bool_(), "(is_nan 1.5) must type as Bool");
}
```

- [ ] **Step 2: Run tests to verify RED**

Run: `cargo test -p ailang-check --lib builtins::tests::install`
Expected: 5 tests FAIL with `UnknownIdent` panic (the names are not
yet in `env.globals`).

- [ ] **Step 3: Add the five new builtins to `install`**

In `crates/ailang-check/src/builtins.rs::install`, immediately
AFTER the `__unreachable__` insert (line 119) and BEFORE the
`env.effect_ops.insert("io/print_int", ...)` block, add:

```rust
    // Iter 22-floats.3: Float-conversion and inspection builtins.
    // Codegen lowering lands in iter 4; iter 3 only registers types.
    env.globals.insert("neg".into(), 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: ailang_core::ast::ParamMode::Implicit,
        }),
    });
    env.globals.insert("int_to_float".into(), Type::Fn {
        params: vec![Type::int()],
        ret: Box::new(Type::float()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ailang_core::ast::ParamMode::Implicit,
    });
    env.globals.insert("float_to_int_truncate".into(), Type::Fn {
        params: vec![Type::float()],
        ret: Box::new(Type::int()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ailang_core::ast::ParamMode::Implicit,
    });
    env.globals.insert("float_to_str".into(), Type::Fn {
        params: vec![Type::float()],
        ret: Box::new(Type::str_()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ailang_core::ast::ParamMode::Implicit,
    });
    env.globals.insert("is_nan".into(), Type::Fn {
        params: vec![Type::float()],
        ret: Box::new(Type::bool_()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ailang_core::ast::ParamMode::Implicit,
    });
```

- [ ] **Step 4: Add the same five entries to `synth.rs::builtin_ail_type`**

In `crates/ailang-codegen/src/synth.rs::builtin_ail_type`, immediately
AFTER the `__unreachable__` arm (line 107-111) and BEFORE the
`_ => return None,` fallback, add:

```rust
        // Iter 22-floats.3: Float-conversion and inspection builtins.
        // Same lockstep with `crates/ailang-check/src/builtins.rs`.
        "neg" => 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,
            }),
        },
        "int_to_float" => Type::Fn {
            params: vec![Type::int()],
            ret: Box::new(Type::float()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        "float_to_int_truncate" => Type::Fn {
            params: vec![Type::float()],
            ret: Box::new(Type::int()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        "float_to_str" => Type::Fn {
            params: vec![Type::float()],
            ret: Box::new(Type::str_()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        "is_nan" => Type::Fn {
            params: vec![Type::float()],
            ret: Box::new(Type::bool_()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
```

- [ ] **Step 5: Add the five entries to `list()`**

In `crates/ailang-check/src/builtins.rs::list()`, append the five
new rows immediately after the `__unreachable__` row and before
the effect-op rows (around line 178):

```rust
        ("__unreachable__", "forall a. a"),
        ("neg", "forall a. (a) -> a"),
        ("int_to_float", "(Int) -> Float"),
        ("float_to_int_truncate", "(Float) -> Int"),
        ("float_to_str", "(Float) -> Str"),
        ("is_nan", "(Float) -> Bool"),
        ("io/print_int", "(Int) -> Unit !IO  [effect op]"),
```

- [ ] **Step 6: Verify the RED tests now GREEN**

Run: `cargo test -p ailang-check --lib builtins::tests::install`
Expected: all 5 PASS.

- [ ] **Step 7: Verify no workspace regression**

Run: `cargo test --workspace`
Expected: 383+ tests passed, 0 failed.

- [ ] **Step 8: Commit**

```bash
git add crates/ailang-check/src/builtins.rs \
        crates/ailang-codegen/src/synth.rs
git commit -m "floats iter 3.2: install neg/int_to_float/float_to_int_truncate/float_to_str/is_nan"
```

---

## Task 3: INSTALL new constants (`nan`, `inf`, `neg_inf`) + new effect op (`io/print_float`)

**Files:**
- Modify: `crates/ailang-check/src/builtins.rs` — `install`
  function (constants + effect op) and `list` function.
- Modify: `crates/ailang-codegen/src/synth.rs` —
  `builtin_ail_type` (constants), `builtin_effect_op_ret`
  (effect op).

- [ ] **Step 1: Write the RED test for constants and effect op**

In `crates/ailang-check/src/builtins.rs::tests`, append:

```rust
/// Iter 22-floats.3: `nan`, `inf`, `neg_inf` are bare-value
/// constants of type `Float`. They are NOT functions — reference
/// site is `(var nan)`, not `(app nan)`. Parallel to
/// `__unreachable__` which is `forall a. a`.
#[test]
fn install_float_constants() {
    let ty_nan = synth_in_builtins_env(&Term::Var { name: "nan".into() });
    assert_eq!(ty_nan, Type::float(), "nan must type as Float");
    let ty_inf = synth_in_builtins_env(&Term::Var { name: "inf".into() });
    assert_eq!(ty_inf, Type::float(), "inf must type as Float");
    let ty_neg_inf = synth_in_builtins_env(&Term::Var { name: "neg_inf".into() });
    assert_eq!(ty_neg_inf, Type::float(), "neg_inf must type as Float");
}

/// Iter 22-floats.3: `io/print_float : (Float) -> Unit !IO`.
/// Codegen lowering parallels `io/print_int` in iter 4.
#[test]
fn install_io_print_float_signature() {
    let bits = 1.5_f64.to_bits();
    let mut env = Env::default();
    install(&mut env);
    let do_term = Term::Do {
        op: "io/print_float".into(),
        args: vec![lit_float(bits)],
        tail: false,
    };
    let (ret, effects) = crate::synth_term(&env, &do_term).expect("synth");
    assert_eq!(ret, Type::unit(), "io/print_float returns Unit");
    assert!(
        effects.iter().any(|e| e == "IO"),
        "io/print_float must accumulate IO effect, got {effects:?}"
    );
}
```

If `crate::synth_term`'s second return value (effect set) has a
different type than `Vec<String>`, adjust the assertion accordingly
— read the function's signature at the top of `lib.rs`.

- [ ] **Step 2: Run tests to verify RED**

Run: `cargo test -p ailang-check --lib builtins::tests::install_float_constants builtins::tests::install_io_print_float_signature`
Expected: both FAIL — `install_float_constants` with
`UnknownIdent("nan")`; `install_io_print_float_signature` with
`UnknownEffectOp("io/print_float")`.

- [ ] **Step 3: Install the three constants**

In `crates/ailang-check/src/builtins.rs::install`, immediately
AFTER the five new builtin inserts from Task 2 and BEFORE the
`env.effect_ops.insert("io/print_int", ...)` block, add:

```rust
    // Iter 22-floats.3: Float bit-pattern constants. Bare values,
    // not fns — reference site is `(var nan)`. Codegen emits
    // `double 0x7FF8000000000000` etc. at the use site in iter 4.
    // Parallel to `__unreachable__` but typed as concrete `Float`
    // rather than the polymorphic bottom.
    env.globals.insert("nan".into(), Type::float());
    env.globals.insert("inf".into(), Type::float());
    env.globals.insert("neg_inf".into(), Type::float());
```

- [ ] **Step 4: Install the effect op**

In `crates/ailang-check/src/builtins.rs::install`, after the existing
`env.effect_ops.insert("io/print_str", …)` block (line 137-144) and
before the closing `}` of `install`, add:

```rust
    // Iter 22-floats.3: parallel to io/print_int|bool|str. Codegen
    // lowers via runtime C glue `@ail_print_float` in iter 4.
    env.effect_ops.insert(
        "io/print_float".into(),
        EffectOpSig {
            effect: "IO".into(),
            params: vec![Type::float()],
            ret: Type::unit(),
        },
    );
```

- [ ] **Step 5: Add the constants to `synth.rs::builtin_ail_type`**

In `crates/ailang-codegen/src/synth.rs::builtin_ail_type`,
immediately after the five Task-2 entries (`is_nan` arm) and
BEFORE the `_ => return None,` fallback, add:

```rust
        "nan" | "inf" | "neg_inf" => Type::float(),
```

- [ ] **Step 6: Add `io/print_float` to `builtin_effect_op_ret`**

In `crates/ailang-codegen/src/synth.rs::builtin_effect_op_ret` at
line 118-122, replace the match body:

```rust
pub(crate) fn builtin_effect_op_ret(op: &str) -> Option<Type> {
    Some(match op {
        "io/print_int" | "io/print_bool" | "io/print_str" | "io/print_float" => Type::unit(),
        _ => return None,
    })
}
```

- [ ] **Step 7: Add the four entries to `list()`**

In `crates/ailang-check/src/builtins.rs::list()`, immediately after
the five Task-2 rows and before the existing effect-op rows, add:

```rust
        ("is_nan", "(Float) -> Bool"),
        ("nan", "Float"),
        ("inf", "Float"),
        ("neg_inf", "Float"),
        ("io/print_int", "(Int) -> Unit !IO  [effect op]"),
        ("io/print_bool", "(Bool) -> Unit !IO  [effect op]"),
        ("io/print_str", "(Str) -> Unit !IO  [effect op]"),
        ("io/print_float", "(Float) -> Unit !IO  [effect op]"),
```

(The `is_nan` row is kept unchanged from Task 2; the four new rows
are `nan`, `inf`, `neg_inf`, `io/print_float`.)

- [ ] **Step 8: Verify the RED tests now GREEN**

Run: `cargo test -p ailang-check --lib builtins::tests`
Expected: all builtins-tests PASS (4 widen + 5 install + 2
constants/effect-op = 11 tests).

- [ ] **Step 9: Verify no workspace regression**

Run: `cargo test --workspace`
Expected: 383+ tests passed, 0 failed.

- [ ] **Step 10: Commit**

```bash
git add crates/ailang-check/src/builtins.rs \
        crates/ailang-codegen/src/synth.rs
git commit -m "floats iter 3.3: install Float constants nan/inf/neg_inf + io/print_float effect op"
```

---

## Task 4: REJECT `Pattern::Lit { lit: Literal::Float { .. } }` at typecheck

**Files:**
- Modify: `crates/ailang-check/src/lib.rs` —
  `CheckError` enum (add new variant), Pattern::Lit typecheck arm
  at line 2306-2316.

- [ ] **Step 1: Write the RED test for Float-pattern rejection**

In `crates/ailang-check/src/builtins.rs::tests`, append a NEW test
(uses the same `synth_in_builtins_env` helper):

```rust
/// Iter 22-floats.3: pattern-matching on Float literals is hard-
/// rejected at typecheck per spec line 723-735 recommendation (a).
/// IEEE-`==` semantics make Float patterns semantically dubious
/// (NaN never matches; equality is bit-exact not approximate).
/// Surface lex / parser accept the syntax (iter 2); typecheck
/// surfaces the error here.
#[test]
fn reject_float_pattern_in_match() {
    use ailang_core::ast::{Arm, Pattern};
    let bits = 1.5_f64.to_bits();
    let scrut = lit_float(bits);
    let arm = Arm {
        pat: Pattern::Lit { lit: Literal::Float { bits } },
        body: lit_int(0),
    };
    let term = Term::Match {
        scrutinee: Box::new(scrut),
        arms: vec![arm],
    };
    let mut env = Env::default();
    install(&mut env);
    let err = crate::synth_term(&env, &term).expect_err("must reject");
    assert!(
        matches!(err, crate::CheckError::FloatPatternNotAllowed),
        "expected FloatPatternNotAllowed, got {err:?}"
    );
}
```

If `Arm` has different fields (e.g. additional `guard`, `binding`),
read the AST `Arm` struct in `crates/ailang-core/src/ast.rs` and
adjust accordingly.

- [ ] **Step 2: Run test to verify RED**

Run: `cargo test -p ailang-check --lib builtins::tests::reject_float_pattern_in_match`
Expected: FAIL — currently the iter-1 arm `Literal::Float { .. }
=> Type::float()` makes the typecheck succeed, so `synth_term`
returns `Ok(...)`, the `expect_err` panics with "must reject".

- [ ] **Step 3: Add `CheckError::FloatPatternNotAllowed` variant**

In `crates/ailang-check/src/lib.rs`, in the `pub enum CheckError`
block (around lines 273-420), add a new variant immediately AFTER
`PrimitiveNeedsWildcard` (line 371):

```rust
    /// A `Pattern::Lit` matched against a `Literal::Float`. Float
    /// patterns are semantically dubious (NaN never matches via
    /// IEEE-`==`; equality is bit-exact not approximate), so the
    /// typechecker hard-rejects them. The surface lex / parser
    /// accept the syntax (iter 2); this diagnostic surfaces at
    /// typecheck time. Code: `float-pattern-not-allowed`.
    #[error("float-literal patterns are not allowed: use ordering operators (`<`, `>`, ...) and `is_nan` to discriminate floats")]
    FloatPatternNotAllowed,
```

- [ ] **Step 4: Replace the iter-1 arm in `Pattern::Lit` typecheck**

In `crates/ailang-check/src/lib.rs`, at lines 2306-2316, replace the
`Pattern::Lit { lit }` block:

```rust
        Pattern::Lit { lit } => {
            let lt = match lit {
                Literal::Int { .. } => Type::int(),
                Literal::Bool { .. } => Type::bool_(),
                Literal::Str { .. } => Type::str_(),
                Literal::Unit => Type::unit(),
                Literal::Float { .. } => {
                    return Err(CheckError::FloatPatternNotAllowed);
                }
            };
            expect_eq(expected, &lt)?;
            Ok(vec![])
        }
```

The `match` no longer needs the Float arm to compute `lt` because
the `Float` case takes the early-return path before `lt` is used.

- [ ] **Step 5: Verify RED test now GREEN**

Run: `cargo test -p ailang-check --lib builtins::tests::reject_float_pattern_in_match`
Expected: PASS.

- [ ] **Step 6: Verify no workspace regression**

Run: `cargo test --workspace`
Expected: 383+ tests passed, 0 failed. The new `CheckError`
variant is purely additive — no diagnostic-code uniqueness check
or test enumerates the variants exhaustively beyond the
`#[derive(thiserror::Error)]` machinery.

- [ ] **Step 7: Commit**

```bash
git add crates/ailang-check/src/lib.rs
git commit -m "floats iter 3.4: typecheck rejects Pattern::Lit Float with FloatPatternNotAllowed"
```

---

## Task 5: Iteration close — JOURNAL entry

**Files:**
- Modify: `docs/JOURNAL.md` — append entry at file end.

- [ ] **Step 1: Append the iteration-close entry**

In `docs/JOURNAL.md`, append a new section at the end of the file
(use the orchestrator-authored template; substitute the actual
per-task commit SHAs):

```markdown
## 2026-05-10 — Iteration Floats.3: typecheck + builtins

Widened the existing arithmetic and comparison builtins (`+`, `-`,
`*`, `/`, `!=`, `<`, `<=`, `>`, `>=`) from monomorphic
`(Int, Int) -> {Int,Bool}` to polymorphic `forall a. (a, a) -> a`
(resp. `... -> Bool`). Same shape `==` already had since iter 16e.
The `{Int, Float}` filter is enforced at codegen (iter 4); typecheck
accepts any matching pair, mirroring how `==` works today. `%` stays
monomorphic-Int (no fmod yet — spec section A3). The widening is
type-side only; codegen lowering for `+` etc. continues to use the
monomorphic-Int `synth::builtin_binop` table (iter 4 converts that to
type-dispatched). The lockstep partner table at
`crates/ailang-codegen/src/synth.rs::builtin_ail_type` was widened in
the same commit so no codegen call site sees an out-of-date polymorphic
shape.

Five new Float builtins installed: `neg : forall a. (a) -> a`
(polymorphic; parallel to widened `+`), `int_to_float : (Int) ->
Float`, `float_to_int_truncate : (Float) -> Int`, `float_to_str :
(Float) -> Str`, `is_nan : (Float) -> Bool`. The polymorphic `neg`
rationale: spec section A3 calls out that the `(- 0.0 x)` desugar is
wrong for `-0.0` (returns `+0.0` per IEEE rounding), so Float
negation needs its own builtin name. Reusing the `forall a. (a) -> a`
shape lets Int negation share the symbol.

Three Float bit-pattern constants installed as bare values (parallel
to `__unreachable__` but with concrete `Type::float()` rather than
`forall a. a`): `nan`, `inf`, `neg_inf`. Reference site is `(var
nan)`, not `(app nan)`. Codegen emits `double 0x7FF8000000000000` /
`double 0x7FF0000000000000` / `double 0xFFF0000000000000` at the use
site in iter 4.

One new effect op installed: `io/print_float : (Float) -> Unit !IO`.
Mirrors `io/print_int|bool|str`. Codegen lowering through runtime C
glue `@ail_print_float` lands in iter 4.

Pattern-matching on Float literals is now typecheck-rejected via the
new `CheckError::FloatPatternNotAllowed` variant per spec line
723-735 recommendation (a). The surface lex / parser still ACCEPT
Float patterns (iter 2 left this open); the typecheck diagnostic
fires at the `Pattern::Lit { lit }` arm in
`crates/ailang-check/src/lib.rs`. The error message points the
LLM-author to the documented alternative — ordering operators and
`is_nan` for Float discrimination.

`ail builtins` reflects all twelve new entries (4 widened arithmetic
display strings + 5 Float fn builtins + 3 Float constants + 1
io/print_float effect op) via the refreshed `list()` table.

Per-task commits:

- `<sha-3.1>` floats iter 3.1: widen +/-/*/// and !=/</<=/>/>= to polymorphic forall a
- `<sha-3.2>` floats iter 3.2: install neg/int_to_float/float_to_int_truncate/float_to_str/is_nan
- `<sha-3.3>` floats iter 3.3: install Float constants nan/inf/neg_inf + io/print_float effect op
- `<sha-3.4>` floats iter 3.4: typecheck rejects Pattern::Lit Float with FloatPatternNotAllowed

Known debt deliberately deferred to later iterations of this milestone:

- Codegen LOWERING for the widened `+`/`-`/`*`/`/` etc. — iter 4
  converts the monomorphic-Int `synth::builtin_binop` table to
  type-dispatched; emits `fadd double` / `fcmp olt double` / etc.
  for the Float arm.
- Codegen LOWERING for `neg` (Int → `sub i64 0, %x`, Float →
  `fneg double %x`) — iter 4.
- Codegen LOWERING for `int_to_float` (`sitofp`),
  `float_to_int_truncate` (`@llvm.fptosi.sat.i64.f64`),
  `float_to_str` (runtime C glue), `is_nan` (`fcmp uno`) — iter 4.
- Codegen LOWERING for `nan`/`inf`/`neg_inf` constants (LLVM hex-
  float literals at the use site) — iter 4.
- Codegen LOWERING for `io/print_float` (parallel to `io/print_int`,
  runtime glue `@ail_print_float`) — iter 4.
- Prose round-trip for Float literals — iter 5.
- DESIGN.md §"Float semantics" subsection (A5 determinism contract)
  and the line-2033 "supported primitive types" list update — iter 5.
```

Replace each `<sha-3.N>` placeholder with the actual commit SHA at
write time.

- [ ] **Step 2: Commit**

```bash
git add docs/JOURNAL.md
git commit -m "floats iter 3: JOURNAL — iteration close (typecheck + builtins)"
```

---

## Iteration acceptance

- [ ] `cargo build --workspace` is clean.
- [ ] `cargo test --workspace` is GREEN — pre-existing tests all
  stay GREEN; the 11 new builtins-tests + 1 new typecheck-rejection
  test all PASS.
- [ ] `ail builtins` reflects the widened signatures and the twelve
  new entries.
- [ ] `crates/ailang-check/src/builtins.rs::install` and
  `crates/ailang-codegen/src/synth.rs::builtin_ail_type` are in
  lockstep (same set of names with matching types).
- [ ] No file touched outside the four listed in the file map.
- [ ] JOURNAL entry committed with the actual per-task commit SHAs.

When all five tasks are committed and the acceptance checklist is
green, hand back to the orchestrator. Iteration 4 (Codegen WIDEN +
Float lowering paths) is the next dispatch.
