floats iter 3.1: widen +/-/*/// and !=/</<=/>/>= to polymorphic forall a

crates/ailang-check/src/builtins.rs

@@ -48,6 +48,38 @@ pub struct EffectOpSig {
 /// [`list()`] is resolvable in `env`. Idempotent for a fresh `Env`; calling
 /// it twice would shadow the same entries with identical types.
 pub fn install(env: &mut crate::Env) {
+    // 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()),
@@ -55,18 +87,12 @@ pub fn install(env: &mut crate::Env) {
         param_modes: vec![],
         ret_mode: ailang_core::ast::ParamMode::Implicit,
     };
-    let int_int_bool = Type::Fn {
-        params: vec![Type::int(), Type::int()],
-        ret: Box::new(Type::bool_()),
-        effects: vec![],
-        param_modes: vec![],
-        ret_mode: ailang_core::ast::ParamMode::Implicit,
-    };
-    for op in ["+", "-", "*", "/", "%"] {
-        env.globals.insert(op.into(), int_int_int.clone());
+    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(), int_int_bool.clone());
+        env.globals.insert(op.into(), poly_a_a_to_bool());
     }
 
     // Iter 16e: `==` is polymorphic — `forall a. (a, a) -> Bool`.
@@ -163,17 +189,17 @@ pub fn value_names() -> Vec<&'static str> {
 /// `ail builtins`, when the LLM wants to check expected signatures.
 pub fn list() -> Vec<(&'static str, &'static str)> {
     vec![
-        ("+", "(Int, Int) -> Int"),
-        ("-", "(Int, Int) -> Int"),
-        ("*", "(Int, Int) -> Int"),
-        ("/", "(Int, Int) -> Int"),
+        ("+", "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"),
-        ("!=", "(Int, Int) -> Bool"),
-        ("<", "(Int, Int) -> Bool"),
-        ("<=", "(Int, Int) -> Bool"),
-        (">", "(Int, Int) -> Bool"),
-        (">=", "(Int, Int) -> 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]"),
@@ -181,3 +207,99 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
         ("io/print_str", "(Str) -> Unit !IO  [effect op]"),
     ]
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::{Env, Subst};
+    use ailang_core::ast::{Literal, Term};
+    use indexmap::IndexMap;
+    use std::collections::BTreeSet;
+
+    /// Synthesize the type of a small expression in a fresh Env that has
+    /// only the builtins installed (no user defs). Returns the fully-
+    /// applied (substitution-resolved) result type; effects ignored for
+    /// this helper. Wraps `crate::synth` with the boilerplate state
+    /// (locals, effects sink, subst, counter, residuals) the real
+    /// typechecker entry points (`check_module`) would otherwise own.
+    fn synth_in_builtins_env(t: &Term) -> Type {
+        let mut env = Env::default();
+        install(&mut env);
+        let mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals = Vec::new();
+        let ty = crate::synth(
+            t,
+            &env,
+            &mut locals,
+            &mut effects,
+            "<test>",
+            &mut subst,
+            &mut counter,
+            &mut residuals,
+        )
+        .expect("synth");
+        subst.apply(&ty)
+    }
+
+    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`. Protects the no-regression invariant
+    /// for every existing Int-using fixture: the polymorphic `+`
+    /// instantiated at `(Int, Int)` must still return `Int`,
+    /// bit-identical to the pre-widening monomorphic shape.
+    #[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` because
+    /// `+` was monomorphic `(Int, Int) -> Int`. The widening to
+    /// `forall a. (a, a) -> a` makes Float arithmetic a typecheck-clean
+    /// shape; codegen filtering of the {Int, Float} arg-type set
+    /// happens in iter 4.
+    #[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`. Mirrors the
+    /// `+` regression check for the comparison-op path.
+    #[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`.
+    /// Pre-widening this would have failed with `TypeMismatch`. The
+    /// widening to `forall a. (a, a) -> Bool` lets Float ordering
+    /// typecheck cleanly; codegen lowers to `fcmp olt double` in iter 4.
+    #[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");
+    }
+}

crates/ailang-codegen/src/synth.rs

@@ -59,6 +59,39 @@ pub(crate) fn fn_sig_from_type(t: &Type) -> Option<FnSig> {
 /// `synth_arg_type` for arg-type inference at polymorphic call sites.
 /// Mirrors what the typechecker installs in its env via `builtins`.
 pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
+    // 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()),
@@ -66,16 +99,10 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
         param_modes: vec![],
         ret_mode: ParamMode::Implicit,
     };
-    let int_int_bool = || Type::Fn {
-        params: vec![Type::int(), Type::int()],
-        ret: Box::new(Type::bool_()),
-        effects: vec![],
-        param_modes: vec![],
-        ret_mode: ParamMode::Implicit,
-    };
     Some(match name {
-        "+" | "-" | "*" | "/" | "%" => int_int_int(),
-        "!=" | "<" | "<=" | ">" | ">=" => int_int_bool(),
+        "+" | "-" | "*" | "/" => poly_a_a_to_a(),
+        "%" => int_int_int(),
+        "!=" | "<" | "<=" | ">" | ">=" => poly_a_a_to_bool(),
         // Iter 16e: `==` is polymorphic — `forall a. (a, a) -> Bool`.
         // The mono pipeline asks `synth_arg_type` for the actual arg
         // types at the call site; `lower_app` then dispatches to the