Iter 16e: == polymorphic over Int / Bool / Str / Unit

Lifts the Int-only restriction on `==`. Declared type becomes
forall a. Fn(a, a) -> Bool; codegen monomorphises and dispatches:

  Int  → icmp eq i64
  Bool → icmp eq i1
  Str  → call @strcmp + icmp eq i32 0
  Unit → constant true (operands still emitted for side effects)
  ADT / Fn / other → CodegenError::Internal

This unblocks 16c's build_eq for non-Int lit patterns. == joins
__unreachable__ as the second polymorphic builtin (same Forall
machinery).

- check/builtins.rs: == registered as Forall(a, Fn(a, a) -> Bool).
- codegen: lower_eq dispatch table; @strcmp declared in IR header
  alongside @printf/@GC_malloc/@puts.
- examples/eq_demo.{ailx,ail.json}: covers all four supported
  scalars including a Str-lit-pattern match.
- IR snapshots refreshed: only +declare i32 @strcmp(ptr, ptr) in
  the header; every define body bit-identical.
- e2e + check + codegen tests: 124 → 133 (+9, of which +1 is the
  e2e fixture and the rest exercise the new dispatch / typecheck
  surface).

Other comparison ops (<, <=, >, >=, !=) remain Int-only — out of
scope for this iter.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

crates/ail/tests/e2e.rs

@@ -1137,3 +1137,29 @@ fn unreachable_demo() {
     let lines: Vec<&str> = stdout.lines().collect();
     assert_eq!(lines, vec!["4", "5"]);
 }
+
+/// Iter 16e: polymorphic `==`. Properties protected:
+/// (1) `==` typechecks at Int / Bool / Str / Unit (the fixture
+///     uses every supported case directly via `(app == ...)`);
+/// (2) codegen dispatches each arg-type to the right LLVM shape
+///     — `icmp eq i64`, `icmp eq i1`, `@strcmp + icmp eq i32 0`,
+///     constant `i1 true` — and the binary's stdout matches the
+///     boolean truth-table for those operators;
+/// (3) 16c's `build_eq` desugar of `(pat-lit "hi")` over a `Str`
+///     scrutinee now goes through, since `==` no longer rejects
+///     non-Int args at typecheck.
+#[test]
+fn eq_demo() {
+    let stdout = build_and_run("eq_demo.ail.json");
+    let lines: Vec<&str> = stdout.lines().collect();
+    assert_eq!(
+        lines,
+        vec![
+            "true", "false", // == on Int
+            "false", "true", // == on Bool
+            "true", "false", // == on Str
+            "true", // == on Unit
+            "1", "2", "0", // classify_str: Str lit-pattern desugar
+        ]
+    );
+}

crates/ail/tests/snapshots/hello.ll

@@ -7,6 +7,7 @@ target triple = "<NORMALIZED>"
 declare i32 @printf(ptr, ...)
 declare i32 @puts(ptr)
 declare ptr @GC_malloc(i64)
+declare i32 @strcmp(ptr, ptr)
 
 @ail_hello_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_hello_main_adapter, ptr null }
 define i8 @ail_hello_main() {

crates/ail/tests/snapshots/list.ll

@@ -7,6 +7,7 @@ target triple = "<NORMALIZED>"
 declare i32 @printf(ptr, ...)
 declare i32 @puts(ptr)
 declare ptr @GC_malloc(i64)
+declare i32 @strcmp(ptr, ptr)
 
 @ail_list_sum_list_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_sum_list_adapter, ptr null }
 @ail_list_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_main_adapter, ptr null }

crates/ail/tests/snapshots/max3.ll

@@ -7,6 +7,7 @@ target triple = "<NORMALIZED>"
 declare i32 @printf(ptr, ...)
 declare i32 @puts(ptr)
 declare ptr @GC_malloc(i64)
+declare i32 @strcmp(ptr, ptr)
 
 @ail_max3_max_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max_adapter, ptr null }
 @ail_max3_max3_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max3_adapter, ptr null }

crates/ail/tests/snapshots/sum.ll

@@ -7,6 +7,7 @@ target triple = "<NORMALIZED>"
 declare i32 @printf(ptr, ...)
 declare i32 @puts(ptr)
 declare ptr @GC_malloc(i64)
+declare i32 @strcmp(ptr, ptr)
 
 @ail_sum_sum_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_sum_adapter, ptr null }
 @ail_sum_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_main_adapter, ptr null }

crates/ail/tests/snapshots/ws_main.ll

@@ -7,6 +7,7 @@ target triple = "<NORMALIZED>"
 declare i32 @printf(ptr, ...)
 declare i32 @puts(ptr)
 declare ptr @GC_malloc(i64)
+declare i32 @strcmp(ptr, ptr)
 
 @ail_ws_lib_add_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_lib_add_adapter, ptr null }
 @ail_ws_main_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_main_main_adapter, ptr null }

crates/ailang-check/src/builtins.rs

@@ -61,9 +61,30 @@ pub fn install(env: &mut crate::Env) {
     for op in ["+", "-", "*", "/", "%"] {
         env.globals.insert(op.into(), int_int_int.clone());
     }
-    for op in ["==", "!=", "<", "<=", ">", ">="] {
+    for op in ["!=", "<", "<=", ">", ">="] {
         env.globals.insert(op.into(), int_int_bool.clone());
     }
+
+    // Iter 16e: `==` is polymorphic — `forall a. (a, a) -> Bool`.
+    // Codegen dispatches on the resolved arg type at the call site:
+    // `Int` → `icmp eq i64`, `Bool` → `icmp eq i1`, `Str` → `@strcmp`,
+    // `Unit` → constant `i1 1`. ADT/Fn equality is rejected at codegen
+    // with a clear "== not supported for type X" error. The other
+    // comparison ops (`<`, `<=`, `>`, `>=`, `!=`) stay Int-only.
+    env.globals.insert(
+        "==".into(),
+        Type::Forall {
+            vars: vec!["a".into()],
+            body: Box::new(Type::Fn {
+                params: vec![
+                    Type::Var { name: "a".into() },
+                    Type::Var { name: "a".into() },
+                ],
+                ret: Box::new(Type::bool_()),
+                effects: vec![],
+            }),
+        },
+    );
     env.globals.insert(
         "not".into(),
         Type::Fn {
@@ -137,7 +158,7 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
         ("*", "(Int, Int) -> Int"),
         ("/", "(Int, Int) -> Int"),
         ("%", "(Int, Int) -> Int"),
-        ("==", "(Int, Int) -> Bool"),
+        ("==", "forall a. (a, a) -> Bool"),
         ("!=", "(Int, Int) -> Bool"),
         ("<", "(Int, Int) -> Bool"),
         ("<=", "(Int, Int) -> Bool"),

crates/ailang-check/src/lib.rs

@@ -3556,4 +3556,92 @@ mod tests {
             vec!["k".to_string(), "x".to_string(), "z".to_string()]
         );
     }
+
+    /// Iter 16e: helper that wraps `body` in a fn whose return type is
+    /// `Bool`, runs `check`, and returns the diagnostics. Used by the
+    /// polymorphic-`==` typecheck tests below.
+    fn check_eq_body_returns_bool(body: Term) -> Vec<Diagnostic> {
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_def(
+                "f",
+                Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::bool_()),
+                    effects: vec![],
+                },
+                vec![],
+                body,
+            )],
+        };
+        check_module(&m)
+    }
+
+    fn eq_app(a: Term, b: Term) -> Term {
+        Term::App {
+            callee: Box::new(Term::Var { name: "==".into() }),
+            args: vec![a, b],
+            tail: false,
+        }
+    }
+
+    /// Iter 16e: `==` accepts Int args (regression — the pre-16e
+    /// behaviour stays identical).
+    #[test]
+    fn eq_typechecks_at_int() {
+        let body = eq_app(
+            Term::Lit { lit: Literal::Int { value: 1 } },
+            Term::Lit { lit: Literal::Int { value: 2 } },
+        );
+        assert!(check_eq_body_returns_bool(body).is_empty());
+    }
+
+    /// Iter 16e: `==` accepts Bool args. Pre-16e this was a typecheck
+    /// error because `==` was declared `(Int, Int) -> Bool`.
+    #[test]
+    fn eq_typechecks_at_bool() {
+        let body = eq_app(
+            Term::Lit { lit: Literal::Bool { value: true } },
+            Term::Lit { lit: Literal::Bool { value: false } },
+        );
+        assert!(check_eq_body_returns_bool(body).is_empty());
+    }
+
+    /// Iter 16e: `==` accepts Str args. Same story as Bool.
+    #[test]
+    fn eq_typechecks_at_str() {
+        let body = eq_app(
+            Term::Lit { lit: Literal::Str { value: "hi".into() } },
+            Term::Lit { lit: Literal::Str { value: "ho".into() } },
+        );
+        assert!(check_eq_body_returns_bool(body).is_empty());
+    }
+
+    /// Iter 16e: `==` accepts Unit args.
+    #[test]
+    fn eq_typechecks_at_unit() {
+        let body = eq_app(
+            Term::Lit { lit: Literal::Unit },
+            Term::Lit { lit: Literal::Unit },
+        );
+        assert!(check_eq_body_returns_bool(body).is_empty());
+    }
+
+    /// Iter 16e: `==`'s type still demands the two sides to agree —
+    /// `(== 1 true)` must fail to unify the second arg's `Bool`
+    /// against the metavar already pinned to `Int` by the first.
+    #[test]
+    fn eq_rejects_mixed_int_bool() {
+        let body = eq_app(
+            Term::Lit { lit: Literal::Int { value: 1 } },
+            Term::Lit { lit: Literal::Bool { value: true } },
+        );
+        let diags = check_eq_body_returns_bool(body);
+        assert!(
+            !diags.is_empty(),
+            "(== 1 true) must fail to typecheck; got no diagnostics"
+        );
+    }
 }

crates/ailang-codegen/src/lib.rs

@@ -351,7 +351,11 @@ pub fn lower_workspace(ws: &Workspace) -> Result<String> {
 
     out.push_str("declare i32 @printf(ptr, ...)\n");
     out.push_str("declare i32 @puts(ptr)\n");
-    out.push_str("declare ptr @GC_malloc(i64)\n\n");
+    out.push_str("declare ptr @GC_malloc(i64)\n");
+    // Iter 16e: `==` on `Str` lowers to `@strcmp` followed by
+    // `icmp eq i32 0`. NUL-terminated strings make this a one-liner;
+    // libc supplies `strcmp` so no extra link flag is needed.
+    out.push_str("declare i32 @strcmp(ptr, ptr)\n\n");
     out.push_str(&header);
     out.push_str(&body);
 
@@ -1500,6 +1504,25 @@ impl<'a> Emitter<'a> {
     }
 
     fn lower_app(&mut self, name: &str, args: &[Term], tail: bool) -> Result<(String, String)> {
+        // Iter 16e: `==` is polymorphic (`forall a. (a, a) -> Bool`).
+        // Dispatch on the resolved AIL arg type — the LLVM `ptr` shape
+        // aliases multiple AIL types (Str vs ADT vs Fn), so we cannot
+        // dispatch on the LLVM type alone. ADT/Fn equality is rejected
+        // here with a clear error; `Unit` evaluates both sides for
+        // their side effects then returns constant `i1 1`.
+        if name == "==" {
+            if args.len() != 2 {
+                return Err(CodegenError::Internal(
+                    "builtin `==` expected 2 args".into(),
+                ));
+            }
+            let arg_ty = self.synth_arg_type(&args[0])?;
+            let (a, a_ll) = self.lower_term(&args[0])?;
+            let (b, _b_ll) = self.lower_term(&args[1])?;
+            let _ = tail;
+            return self.lower_eq(&arg_ty, &a, &b, &a_ll);
+        }
+
         // Built-in arithmetic / comparison.
         if let Some((instr, ret_ty)) = builtin_binop(name) {
             if args.len() != 2 {
@@ -2330,6 +2353,80 @@ impl<'a> Emitter<'a> {
         }
     }
 
+    /// Iter 16e: lower a `==` call after the two operands have been
+    /// emitted. Dispatches on the resolved AIL type of the arg side
+    /// (both sides have the same type after typecheck). The `_a_ll`
+    /// hint is the LLVM type the lowering produced for `a`; we use
+    /// it as a sanity check against `arg_ty`'s expected LLVM shape.
+    ///
+    /// Supported:
+    /// - `Int` → `icmp eq i64`
+    /// - `Bool` → `icmp eq i1`
+    /// - `Str` → `@strcmp` then `icmp eq i32 0`
+    /// - `Unit` → constant `i1 true` (both sides already evaluated
+    ///   for any side effects; Unit has a single inhabitant).
+    ///
+    /// Rejected with `CodegenError::Internal` for ADT, `Fn`, and any
+    /// other type — those would need either a structural-equality
+    /// scheme (ADT) or a fn-pointer compare (Fn) that the language
+    /// does not yet specify.
+    fn lower_eq(
+        &mut self,
+        arg_ty: &Type,
+        a: &str,
+        b: &str,
+        _a_ll: &str,
+    ) -> Result<(String, String)> {
+        match arg_ty {
+            Type::Con { name, .. } => match name.as_str() {
+                "Int" => {
+                    let dst = self.fresh_ssa();
+                    self.body.push_str(&format!(
+                        "  {dst} = icmp eq i64 {a}, {b}\n"
+                    ));
+                    Ok((dst, "i1".into()))
+                }
+                "Bool" => {
+                    let dst = self.fresh_ssa();
+                    self.body.push_str(&format!(
+                        "  {dst} = icmp eq i1 {a}, {b}\n"
+                    ));
+                    Ok((dst, "i1".into()))
+                }
+                "Str" => {
+                    let cmp = self.fresh_ssa();
+                    self.body.push_str(&format!(
+                        "  {cmp} = call i32 @strcmp(ptr {a}, ptr {b})\n"
+                    ));
+                    let dst = self.fresh_ssa();
+                    self.body.push_str(&format!(
+                        "  {dst} = icmp eq i32 {cmp}, 0\n"
+                    ));
+                    Ok((dst, "i1".into()))
+                }
+                "Unit" => {
+                    // Both sides have already been evaluated above for
+                    // any side effects; Unit has a single inhabitant,
+                    // so equality is `true` by definition.
+                    let _ = a;
+                    let _ = b;
+                    Ok(("true".into(), "i1".into()))
+                }
+                other => Err(CodegenError::Internal(format!(
+                    "`==` not supported for type `{other}` \
+                     (ADT and user-defined types lack a structural-equality scheme)"
+                ))),
+            },
+            Type::Fn { .. } => Err(CodegenError::Internal(
+                "`==` not supported for function types (no canonical fn-pointer equality)".into(),
+            )),
+            other => Err(CodegenError::Internal(format!(
+                "`==` not supported for type `{}`",
+                ailang_core::pretty::type_to_string(other)
+            ))),
+        }
+    }
+
     fn fresh_ssa(&mut self) -> String {
         self.counter += 1;
         format!("%v{}", self.counter)
@@ -2640,7 +2737,23 @@ fn builtin_ail_type(name: &str) -> Option<Type> {
     };
     Some(match name {
         "+" | "-" | "*" | "/" | "%" => int_int_int(),
-        "==" | "!=" | "<" | "<=" | ">" | ">=" => int_int_bool(),
+        "!=" | "<" | "<=" | ">" | ">=" => int_int_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
+        // right LLVM instruction (icmp eq i64 / i1, @strcmp, or
+        // constant i1 1) on those resolved types.
+        "==" => Type::Forall {
+            vars: vec!["a".into()],
+            body: Box::new(Type::Fn {
+                params: vec![
+                    Type::Var { name: "a".into() },
+                    Type::Var { name: "a".into() },
+                ],
+                ret: Box::new(Type::bool_()),
+                effects: vec![],
+            }),
+        },
         "not" => Type::Fn {
             params: vec![Type::bool_()],
             ret: Box::new(Type::bool_()),
@@ -3108,6 +3221,111 @@ mod tests {
         );
     }
 
+    /// Iter 16e: codegen rejects `==` on ADT-typed args with a clear
+    /// error. The typechecker accepts the call (the rigid var of
+    /// `forall a. (a, a) -> Bool` unifies with the ADT type), so the
+    /// rejection has to happen here. The diagnostic must mention the
+    /// `==` symbol and the ADT type name.
+    #[test]
+    fn eq_on_adt_rejected_at_codegen() {
+        // Tiny ADT `data K = Mk` (nullary).
+        let mk = Term::Ctor {
+            type_name: "K".into(),
+            ctor: "Mk".into(),
+            args: vec![],
+        };
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![
+                Def::Type(TypeDef {
+                    name: "K".into(),
+                    vars: vec![],
+                    ctors: vec![Ctor {
+                        name: "Mk".into(),
+                        fields: vec![],
+                    }],
+                    doc: None,
+                }),
+                Def::Fn(FnDef {
+                    name: "main".into(),
+                    ty: Type::Fn {
+                        params: vec![],
+                        ret: Box::new(Type::unit()),
+                        effects: vec![],
+                    },
+                    params: vec![],
+                    body: Term::Let {
+                        name: "_b".into(),
+                        value: Box::new(Term::App {
+                            callee: Box::new(Term::Var { name: "==".into() }),
+                            args: vec![mk.clone(), mk],
+                            tail: false,
+                        }),
+                        body: Box::new(Term::Lit { lit: Literal::Unit }),
+                    },
+                    doc: None,
+                }),
+            ],
+        };
+        let err = emit_ir(&m).expect_err(
+            "`==` on ADT must be rejected at codegen; emit_ir succeeded",
+        );
+        let msg = format!("{err:?}");
+        assert!(
+            msg.contains("==") && msg.contains("not supported"),
+            "expected error mentioning `==` not supported; got: {msg}"
+        );
+    }
+
+    /// Iter 16e: same negative-path guard for function-typed args.
+    /// `==` on `Fn` is rejected with a "not supported for function
+    /// types" message.
+    #[test]
+    fn eq_on_fn_rejected_at_codegen() {
+        // `let f = main in (== f f)` — `main` is in scope as a fn-value.
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![Def::Fn(FnDef {
+                name: "main".into(),
+                ty: Type::Fn {
+                    params: vec![],
+                    ret: Box::new(Type::unit()),
+                    effects: vec![],
+                },
+                params: vec![],
+                body: Term::Let {
+                    name: "f".into(),
+                    value: Box::new(Term::Var { name: "main".into() }),
+                    body: Box::new(Term::Let {
+                        name: "_b".into(),
+                        value: Box::new(Term::App {
+                            callee: Box::new(Term::Var { name: "==".into() }),
+                            args: vec![
+                                Term::Var { name: "f".into() },
+                                Term::Var { name: "f".into() },
+                            ],
+                            tail: false,
+                        }),
+                        body: Box::new(Term::Lit { lit: Literal::Unit }),
+                    }),
+                },
+                doc: None,
+            })],
+        };
+        let err = emit_ir(&m).expect_err(
+            "`==` on Fn must be rejected at codegen; emit_ir succeeded",
+        );
+        let msg = format!("{err:?}");
+        assert!(
+            msg.contains("==") && msg.contains("function"),
+            "expected error mentioning `==` and function types; got: {msg}"
+        );
+    }
+
     #[test]
     fn missing_entry_main_is_error() {
         let m = Module {

docs/DESIGN.md

@@ -773,7 +773,11 @@ collector wired up in Iter 14f, see Decision 9); nested constructor
 sub-patterns inside `match` (lifted in Iter 16a via the desugar pass);
 literal sub-patterns inside a Ctor pattern (lifted in Iter 16c — the
 desugar pass rewrites every `Pattern::Lit` to a `Term::If` on `==`,
-both at the top level of an arm and inside a Ctor sub-pattern).
+both at the top level of an arm and inside a Ctor sub-pattern);
+`==` extended from Int-only to a polymorphic
+`forall a. (a, a) -> Bool` over `Int`/`Bool`/`Str`/`Unit` (lifted
+in Iter 16e — codegen monomorphises and dispatches on the
+resolved arg type; ADT/Fn arg types are rejected at codegen).
 
 - No effect handlers — only the built-in IO and Diverge ops.
 - No refinements / SMT escalation.
@@ -798,19 +802,39 @@ What **is** supported (and used as the smoke test for the pipeline):
 - `if`, `let`, function calls, recursion.
 - Effects on function signatures, with `do op(args)` for direct effect
   ops (`io/print_int`, `io/print_bool`, `io/print_str`).
-- **Builtins.** Arithmetic and comparison operators (`+`, `-`, `*`,
-  `/`, `%`, `==`, `!=`, `<`, `<=`, `>`, `>=`) of type
-  `(Int, Int) -> Int` / `Bool`; logical `not : (Bool) -> Bool`; the
-  IO effect ops listed above; and **`__unreachable__ : forall a. a`**
-  (Iter 16d). The latter is a polymorphic bottom value: a use of
-  `__unreachable__` typechecks against any expected type at the use
-  site and codegens to the LLVM `unreachable` instruction (UB if
-  ever executed). It is the chain machinery's deepest fall-through
-  for matches that the typechecker proved exhaustive, and it is
-  available to user code as an explicit panic primitive
-  (`(if cond __unreachable__ ...)` for assertions or impossible
-  branches). Reference site is `Term::Var { name = "__unreachable__" }`
-  / form-A bare `__unreachable__`.
+- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`, `%`) of
+  type `(Int, Int) -> Int`; ordering operators and `!=` (`!=`,
+  `<`, `<=`, `>`, `>=`) of type `(Int, Int) -> Bool`; logical
+  `not : (Bool) -> Bool`; the IO effect ops listed above;
+  **`==` : forall a. (a, a) -> Bool** (Iter 16e); and
+  **`__unreachable__ : forall a. a`** (Iter 16d).
+  - **`==` is polymorphic** (Iter 16e). The typechecker accepts
+    `==` at any type whose two sides agree (the rigid `a` of the
+    `Forall` is unified by HM at the use site). Codegen
+    monomorphises and dispatches on the resolved AIL arg type:
+    `Int` → `icmp eq i64`; `Bool` → `icmp eq i1`;
+    `Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0`
+    (`@strcmp` is declared in the LLVM IR header alongside
+    `@printf` / `@GC_malloc`); `Unit` → constant `i1 true`
+    (Unit has a single inhabitant; both sides are still
+    evaluated for any side effects). ADT and `Fn` arg types are
+    rejected at codegen with a `CodegenError::Internal`
+    mentioning `==` and the offending type — neither has a
+    canonical structural-equality scheme yet, and the language
+    deliberately does not silently elide the check. The other
+    comparison ops stay Int-only; their codegen path emits
+    `icmp s{lt,le,gt,ge,ne}` over `i64`.
+  - **`__unreachable__`** is a polymorphic bottom value: a use of
+    `__unreachable__` typechecks against any expected type at
+    the use site and codegens to the LLVM `unreachable`
+    instruction (UB if ever executed). It is the chain
+    machinery's deepest fall-through for matches that the
+    typechecker proved exhaustive, and it is available to user
+    code as an explicit panic primitive
+    (`(if cond __unreachable__ ...)` for assertions or
+    impossible branches). Reference site is
+    `Term::Var { name = "__unreachable__" }` / form-A bare
+    `__unreachable__`.
 - **ADTs + pattern matching** (Iter 3, extended in Iter 16a/16c).
   Sub-patterns of a Ctor pattern may be `Var`, `Wild`, another `Ctor`
   (Iter 16a), or a literal (Iter 16c). The desugar pass flattens
@@ -820,10 +844,10 @@ What **is** supported (and used as the smoke test for the pipeline):
 - Literal patterns at top level and inside Ctor sub-patterns (Iter 16c,
   via desugar). `(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both
   parse and lower; the rewrite is to `Term::If { cond = (== sv lit) }`,
-  so any literal kind whose `==` is supported by the typechecker is
-  authorable. Today that means `Int`; `Bool`/`Str`/`Unit` lit patterns
-  are accepted by desugar but reach typecheck as a type error because
-  `==` is `(Int, Int) -> Bool` only.
+  so any literal kind whose `==` is supported is authorable. After
+  Iter 16e (`==` polymorphic over `Int`/`Bool`/`Str`/`Unit`), that
+  covers every lit kind the AST ships — including `(pat-lit "hi")`
+  over a `Str` scrutinee, exercised by `examples/eq_demo.ail.json`.
 - **Imports + qualified cross-module references** via dotted names
   (Iter 5). Extends to **types and constructors** (Iter 14h): a foreign
   module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as

docs/JOURNAL.md

@@ -4646,3 +4646,208 @@ addresses, not 16d.
 Bool/Str/Unit — surfaced by 16c, unchanged); 17a (per-fn
 arena, gated — unchanged); 16c-aux (`std_list::take`/`drop`
 refactor onto lit patterns — unchanged).
+
+## Iter 16e — `==` extends to Bool/Str/Unit (polymorphic dispatch)
+
+**Goal.** Lift the last gate the 16c entry left open: `==` was
+declared `(Int, Int) -> Bool`, so 16c's `build_eq` rewrite of a
+non-Int `Pattern::Lit` (`(pat-lit "hi")`, `(pat-lit true)`, etc.)
+desugared to a well-formed AST but failed at typecheck because
+the `==` call's arg types could not unify with `Int`. 16e
+extends `==` to a polymorphic operator usable on the four
+language-level scalar types — `Int`, `Bool`, `Str`, `Unit` —
+and cleans the gap left by 16c so every `Literal` kind that
+the AST ships is now usable in a `(pat-lit ...)` position.
+
+**Pre-16e state.** From the 16d journal: `==` lived as
+`("==", "(Int, Int) -> Bool")` in `ailang-check::builtins` (line
+~140). 16c's `build_eq` already produced `(app == lhs rhs)` for
+every non-Unit literal kind; for `Unit` it short-circuited to
+`Term::Lit { Bool { true } }` (every `()` is equal). Without
+16e, the codegen rejection of non-Int `==` was preceded by a
+typecheck rejection: `forall a. (a, a) -> Bool` was simply not
+the declared type, so unification of `Bool` against `Int` (via
+`int_int_bool`) blew up first. Iter 16d's `categorize_first`
+fixture sidestepped the issue by using only Int lit patterns;
+no shipped fixture used a `Bool`/`Str`/`Unit` lit pattern.
+
+**Architectural decision (binding, by orchestrator).**
+
+- `==`'s declared type becomes
+  `Forall(["a"], Fn([Var("a"), Var("a")], Bool, []))` —
+  `forall a. (a, a) -> Bool`. The polymorphic-builtin pattern
+  mirrors `__unreachable__` from 16d (which is a `Forall`-typed
+  value rather than a `Forall`-typed fn, but lives in the same
+  `env.globals` slot and the same `builtin_ail_type` mirror in
+  codegen). User-facing surface stays one symbol; the existing
+  `(app == ...)` shape carries every supported type.
+- Codegen monomorphises like any polymorphic builtin and
+  dispatches on the resolved AIL arg type at the call site.
+  The dispatch table (one row per supported type):
+
+  | AIL type | LLVM lowering                                  |
+  |----------|------------------------------------------------|
+  | `Int`    | `icmp eq i64`                                  |
+  | `Bool`   | `icmp eq i1`                                   |
+  | `Str`    | `call i32 @strcmp(ptr, ptr)` then `icmp eq i32 0` |
+  | `Unit`   | constant `i1 true` (single-inhabitant)         |
+  | ADT/Fn   | rejected with `CodegenError::Internal`         |
+
+- Unit's lowering still evaluates both operands above the
+  comparison (preserving any side effects), then ignores the
+  resulting SSA values and returns the constant `true`. This
+  matches the standard pattern (eval-both-then-fold) and keeps
+  `Unit` `==` semantics-preserving in the presence of an
+  effectful sub-expression (none of the shipped fixtures
+  exercise that, but the invariant is documented in
+  `lower_eq`'s rustdoc).
+- ADT and `Fn` arg types fall to a clear codegen error message
+  (`==` not supported for type X / function types`). Two design
+  reasons: (a) ADT structural equality requires either a derived
+  per-type equality fn or runtime field-by-field walk — neither
+  is in 16e's scope; (b) `Fn`-pointer equality on a closure pair
+  is meaningless without a normalisation pass (two thunks may
+  represent the same lambda). Either is its own iter, queued
+  outside this one. The negative path is gated by two new
+  codegen unit tests (`eq_on_adt_rejected_at_codegen`,
+  `eq_on_fn_rejected_at_codegen`).
+
+**Why polymorphic `==` over per-type `==int`/`==bool`/`==str`.**
+Mirrors `__unreachable__`'s precedent (one polymorphic name in
+`env.globals`, instantiated by the typechecker at every use
+site). Three concrete benefits over the alternative:
+(i) `build_eq` from 16c stays as-is — it already produces a
+single `(app == lhs rhs)` term, type-driven; (ii) authoring
+surface stays one symbol, no `==str` lookup table for the LLM
+to memorise; (iii) the existing `Forall` instantiation
+machinery (`maybe_instantiate` in `ailang-check`) does the
+work — no new typechecker code path.
+
+**The `@strcmp` extern.** `Str` `==` lowers to libc's
+`strcmp(ptr, ptr) -> i32`. Strings are NUL-terminated literals
+in the AILang ABI (see `io/print_str` lowering, which calls
+`@puts`), so `strcmp` is a one-liner. Declared in the LLVM IR
+header next to `@printf` / `@puts` / `@GC_malloc`. No extra
+clang link flag needed — `strcmp` is in libc.
+
+**What shipped.**
+
+- `crates/ailang-check/src/builtins.rs` (+22, of which ~10
+  doc): `==` is hoisted out of the `int_int_bool` shape branch
+  into a dedicated `Forall` registration; the `list()` row
+  becomes `("==", "forall a. (a, a) -> Bool")` (consumed by the
+  `ail builtins` CLI subcommand). Other comparison ops (`<`,
+  `<=`, `>`, `>=`, `!=`) keep their Int-only registration
+  unchanged — extending those is queued separately if ever
+  needed (`!=` would be a one-line change after this iter).
+- `crates/ailang-codegen/src/lib.rs` (+~110, of which ~50
+  doc): (a) IR header gains `declare i32 @strcmp(ptr, ptr)`;
+  (b) `lower_app` short-circuits `name == "=="` before the
+  `builtin_binop` block, calling a new `lower_eq` helper that
+  takes the resolved `Type` of the first arg (via
+  `synth_arg_type`) and dispatches by `Type::Con.name`;
+  (c) `builtin_ail_type` mirror gets the `Forall` form for
+  `==` so the mono pipeline's arg-type inference still
+  resolves the symbol. The old `("==", "icmp eq", "i1")` row
+  in `builtin_binop` stays — `is_static_callee` queries the
+  table to decide whether `==` is a direct callee, and the
+  early-return in `lower_app` ensures the `i64`-emission code
+  is never reached.
+- `examples/eq_demo.ailx` + `examples/eq_demo.ail.json`: new
+  fixture exercising `==` at all four supported types directly
+  via `(app == ...)` and indirectly via 16c's lit-pattern
+  desugar over a `Str` scrutinee. Drives `io/print_bool` for
+  the boolean results and `io/print_int` for the `classify_str`
+  fn (a 3-arm `(match s ... (case (pat-lit "hi") 1) ...)`).
+  Output (one per line): `true`, `false` (Int);
+  `false`, `true` (Bool); `true`, `false` (Str); `true`
+  (Unit); `1`, `2`, `0` (`classify_str` over `"hi"`/`"ho"`/
+  `"??"`). The Str lit-pattern arm is the smoking gun for
+  16c+16e working together — pre-16e, that `(pat-lit "hi")`
+  desugared to `(if (== sv "hi") 1 fall_k)` and the `==` call
+  failed to typecheck.
+- `crates/ail/tests/e2e.rs`: new `eq_demo` test (+25 incl.
+  doc), e2e count 46 → 47.
+- `crates/ailang-check/src/lib.rs` (+~85 incl. doc): five new
+  unit tests in the `tests` module — `eq_typechecks_at_int`
+  (regression), `eq_typechecks_at_bool`, `eq_typechecks_at_str`,
+  `eq_typechecks_at_unit` (positive), and
+  `eq_rejects_mixed_int_bool` (negative — confirms the rigid
+  var still demands the two sides agree).
+- `crates/ailang-codegen/src/lib.rs` tests: two new unit tests
+  (`eq_on_adt_rejected_at_codegen`,
+  `eq_on_fn_rejected_at_codegen`) that drive `emit_ir` past
+  typecheck and assert a clear error message mentions `==` and
+  the offending type kind. ADT case constructs a tiny `data K =
+  Mk` and compares two `Mk` ctors; Fn case binds `f = main` and
+  compares the fn-value with itself.
+- `crates/ail/tests/snapshots/*.ll`: the IR header in every
+  snapshot now contains `declare i32 @strcmp(ptr, ptr)`; the
+  five existing snapshots (`hello`, `list`, `max3`, `sum`,
+  `ws_main`) were refreshed via `UPDATE_SNAPSHOTS=1`. Body of
+  every `define` block is byte-identical to pre-16e — the
+  header is the only diff.
+- `docs/DESIGN.md`: Builtins bullet rewritten to call out the
+  polymorphic `==` and the dispatch table; the lit-pattern
+  bullet updated to drop the "today that means Int" caveat;
+  the "Recently lifted gates" preamble extended.
+
+**What deliberately did NOT change.**
+
+- The other comparison ops (`<`, `<=`, `>`, `>=`, `!=`) stay
+  Int-only. `!=` could be made polymorphic by the same recipe
+  (one row in `builtins.rs`, one branch in `lower_app`), but
+  staying in scope for this iter — queued.
+- Codegen `unreachable!` arms for `Term::LetRec` STAY
+  (architectural rule from the iter brief, unchanged from
+  16b.x).
+- ADT structural equality and `Fn`-pointer equality stay
+  rejected at codegen. Either could be lifted later, but
+  needs its own design.
+- `==` at the LetRec / closure-pair / lambda boundary is
+  unchanged: those still produce `Fn` arg types and now hit
+  the codegen-level rejection with a clearer error message
+  than the pre-16e "wrong LLVM type for icmp" garble.
+
+**Hash determinism.** The ten fixtures listed in the iter
+brief (`local_rec_demo`, `lit_pat`, `local_rec_capture`,
+`local_rec_let_capture`, `local_rec_match_capture`,
+`local_rec_as_value`, `local_rec_as_value_capture`,
+`poly_rec_capture`, `nested_let_rec`, `unreachable_demo`)
+all produce identical `ail manifest` output to their pre-16e
+forms — verified via direct manifest dump. No fixture's
+canonical JSON changed; no def hash changed. The new
+`eq_demo` fixture introduces two new hashes (`classify_str`,
+`main`) that obviously did not exist before.
+
+**Tests: 125 → 133 (+8).**
+
+- e2e: 46 → 47 (`eq_demo`).
+- `ailang-check::tests`: 29 → 34 (five new `eq_*` tests).
+- `ailang-codegen::tests`: 2 → 4 (two negative-path tests).
+- All other crates unchanged.
+- IR snapshot tests: 5 → 5 (unchanged count; bytes refreshed
+  for the new `@strcmp` header line).
+
+**Cumulative state, post-16e.**
+
+- Stdlib unchanged (5 modules, 29 combinators).
+- `Term`/`Pattern`/`Literal` enums unchanged. The change is
+  entirely a builtin-registration shift (`Fn` → `Forall<Fn>`
+  in `env.globals`) plus a codegen dispatch site — no AST
+  shape changed and no schema bump.
+- 16a desugar pass keeps its four-job role from 16d. 16e's
+  contribution is a pre-existing desugar output (`(app ==
+  s_var lit)` from 16c's `build_eq`) suddenly being typeable
+  for non-Int literals.
+- Compiler bugs surfaced and fixed in dogfood since 14a: 5/5
+  (unchanged).
+
+**Queue update post-16e.** 16e done. Open: `closure-of-self`
+(informally 16b.5-body — unchanged); `closure-poly`
+(informally 16b.5b — unchanged); 17a (per-fn arena, gated on
+user GC discussion — unchanged); 16c-aux (`std_list::take`/
+`drop` refactor onto lit patterns — unchanged); a low-priority
+follow-up that mirrors 16e for `!=` (one-line change in
+`builtins.rs` plus a one-line dispatch arm in `lower_app`,
+queued without a number).

examples/eq_demo.ail.json

@@ -0,0 +1 @@
+{"defs":[{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"lit":{"kind":"str","value":"hi"},"p":"lit"}},{"body":{"lit":{"kind":"int","value":2},"t":"lit"},"pat":{"lit":{"kind":"str","value":"ho"},"p":"lit"}},{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"p":"wild"}}],"scrutinee":{"name":"s","t":"var"},"t":"match"},"doc":"Lit-pattern over Str; exercises 16c's build_eq for non-Int.","kind":"fn","name":"classify_str","params":["s"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Str"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"},{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"},{"lit":{"kind":"int","value":6},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"bool","value":true},"t":"lit"},{"lit":{"kind":"bool","value":false},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"bool","value":true},"t":"lit"},{"lit":{"kind":"bool","value":true},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"hi"},"t":"lit"},{"lit":{"kind":"str","value":"hi"},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"hi"},"t":"lit"},{"lit":{"kind":"str","value":"ho"},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"unit"},"t":"lit"},{"lit":{"kind":"unit"},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"hi"},"t":"lit"}],"fn":{"name":"classify_str","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"ho"},"t":"lit"}],"fn":{"name":"classify_str","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"str","value":"??"},"t":"lit"}],"fn":{"name":"classify_str","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive == at Int/Bool/Str/Unit; then drive classify_str.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"eq_demo","schema":"ailang/v0"}

examples/eq_demo.ailx

@@ -0,0 +1,56 @@
+; Iter 16e — `==` extends from Int-only to Int/Bool/Str/Unit (polymorphic
+; dispatch). The builtin's declared type became
+;   forall a. (a, a) -> Bool
+; and codegen monomorphises on the resolved arg type:
+;   Int  → icmp eq i64
+;   Bool → icmp eq i1
+;   Str  → @strcmp + icmp eq i32 0
+;   Unit → constant i1 true (single-inhabitant type)
+;   ADT/Fn → rejected at codegen with a clear error.
+;
+; This fixture exercises all four supported types, both directly via
+; `(app == ...)` and indirectly via 16c's lit-pattern desugar (which
+; rewrites `(pat-lit "hi")` → `(if (== sv "hi") body fall_k)` and
+; therefore inherits 16e's polymorphic `==`).
+;
+; Expected stdout (one per line):
+;   true   ; (== 5 5)
+;   false  ; (== 5 6)
+;   false  ; (== true false)
+;   true   ; (== true true)
+;   true   ; (== "hi" "hi")
+;   false  ; (== "hi" "ho")
+;   true   ; (== () ())
+;   1      ; classify_str "hi"   (lit-pattern hits 1 arm)
+;   2      ; classify_str "ho"   (lit-pattern hits 2 arm)
+;   0      ; classify_str "??"   (default arm)
+;
+; Driver lowers via io/print_bool / io/print_int.
+
+(module eq_demo
+
+  (fn classify_str
+    (doc "Lit-pattern over Str; exercises 16c's build_eq for non-Int.")
+    (type (fn-type (params (con Str)) (ret (con Int))))
+    (params s)
+    (body
+      (match s
+        (case (pat-lit "hi") 1)
+        (case (pat-lit "ho") 2)
+        (case _ 0))))
+
+  (fn main
+    (doc "Drive == at Int/Bool/Str/Unit; then drive classify_str.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (seq (do io/print_bool (app == 5 5))
+      (seq (do io/print_bool (app == 5 6))
+      (seq (do io/print_bool (app == true false))
+      (seq (do io/print_bool (app == true true))
+      (seq (do io/print_bool (app == "hi" "hi"))
+      (seq (do io/print_bool (app == "hi" "ho"))
+      (seq (do io/print_bool (app == (lit-unit) (lit-unit)))
+      (seq (do io/print_int (app classify_str "hi"))
+      (seq (do io/print_int (app classify_str "ho"))
+           (do io/print_int (app classify_str "??"))))))))))))))