plan: floats iter 3 — typecheck + builtins (widen + install + Pattern::Lit::Float reject)

2026-05-10 15:20:09 +02:00
parent 4ccf1f25c1
commit 00a1c5f0e7
1 changed files with 926 additions and 0 deletions
@@ -0,0 +1,926 @@
+# 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.