Iter 12a: typechecker polymorphism via Forall instantiation

Polymorphism is now opt-in via Type::Forall at top-level def types.
Implementation is the textbook ML rule: peel the Forall when checking
the def body, instantiate fresh metavars at every use site, unify.

Mechanics:
- New Subst struct + unify(): standard occurs-check unification, with
  effects compared as a set.
- Metavars encoded inside the existing Type::Var as Type::Var{name:
  "$m<id>"}. The "$" prefix can't collide with source-level identifiers,
  so the AST schema stays untouched and existing module hashes don't
  shift (verified: sum.ail.json keeps db33f57cb329935e / d9a916a0ed10a3d3).
- check_fn peels an outer Forall and installs the rigid vars in
  Env.rigid_vars, where check_type_well_formed accepts them. Inner
  forall vars unify only with themselves.
- Term::Var lookup runs maybe_instantiate on the resolved type, so
  polymorphic globals get fresh metavars at each occurrence. Two
  use sites of the same `id` get independent ($m0)→$m0 and ($m1)→$m1
  shapes — no bleed.
- All expect_eq calls inside synth replaced with unify; expect_eq is
  still used for the App-arity / etc. structural checks where no
  metavars can appear.

Constraints kept tight on purpose:
- Const types may not be Forall (rejected outright).
- Forall in ADT field positions still rejected.
- No higher-rank polymorphism: App's callee can be Forall (defensive
  instantiate) but the body doesn't introduce new quantifiers.
- No let-generalisation of lambdas — all polymorphism is at top-level
  defs only.

Codegen still rejects Forall types, so polymorphic programs typecheck
but don't yet compile. Iter 12b adds monomorphisation.

Tests: 14/14 (was 10/10) — added polymorphic_id_def_typechecks,
polymorphic_id_can_be_used_at_int_and_bool,
polymorphic_id_consistency_is_enforced, polymorphic_apply_with_two_vars.

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

crates/ailang-check/src/lib.rs

@@ -1,16 +1,220 @@
 //! Typechecker for AILang (MVP).
 //!
-//! Monomorphic HM subset: no type variables in the body; all top-level defs
-//! must be fully annotated. Effects are propagated as a set and reconciled
-//! against the annotation on the function type.
+//! HM with explicit top-level polymorphism. All top-level defs must carry
+//! their full type annotation; lambda bodies inside defs are checked
+//! monomorphically against their declared types. Polymorphism is opt-in
+//! via `Type::Forall { vars, body }` at top-level def types and is
+//! instantiated at every use site (the textbook ML rule).
+//!
+//! Effects are propagated as a set and reconciled against the annotation
+//! on the function type.
 //!
 //! Built-in operations are resolved via [`Builtins`].
+//!
+//! ## Internals
+//!
+//! Type variables come in two flavours during checking:
+//! - **Rigid vars** — universally quantified vars from a `Forall` that
+//!   end up in scope while checking a polymorphic def's body. They are
+//!   `Type::Var { name: "<name>" }` where `<name>` is the source-level
+//!   name (`a`, `b`, ...). They unify only with themselves.
+//! - **Metavars** — fresh placeholders for instantiated forall vars at
+//!   use sites. Encoded inside the existing `Type::Var` as
+//!   `Type::Var { name: "$m<id>" }`. The naming convention keeps the AST
+//!   schema untouched (no new variant, hashes stay stable). Source-level
+//!   names cannot collide with the `$m` prefix because identifiers may
+//!   not start with `$`.
 
 use ailang_core::ast::*;
 use ailang_core::Workspace;
 use indexmap::IndexMap;
 use std::collections::{BTreeMap, BTreeSet};
 
+/// Metavariable substitution. Maps fresh metavar ids (from `$m<id>` in
+/// `Type::Var.name`) to the type they have been unified against.
+#[derive(Debug, Default, Clone)]
+pub struct Subst {
+    map: BTreeMap<u32, Type>,
+}
+
+impl Subst {
+    /// Allocates a fresh metavar. The counter is owned by the caller so
+    /// that ids stay deterministic across `synth` calls within one
+    /// def-check.
+    fn fresh(counter: &mut u32) -> Type {
+        let id = *counter;
+        *counter += 1;
+        Type::Var { name: format!("$m{id}") }
+    }
+
+    /// `Some(id)` iff the var name is the metavar encoding `$m<id>`.
+    fn meta_id(name: &str) -> Option<u32> {
+        name.strip_prefix("$m").and_then(|s| s.parse::<u32>().ok())
+    }
+
+    fn lookup(&self, id: u32) -> Option<&Type> {
+        self.map.get(&id)
+    }
+
+    fn extend(&mut self, id: u32, t: Type) {
+        self.map.insert(id, t);
+    }
+
+    /// Walks `t`, replacing every metavar with its current binding (if
+    /// any) — recursively so chains collapse. Rigid vars and concrete
+    /// types pass through unchanged.
+    pub fn apply(&self, t: &Type) -> Type {
+        match t {
+            Type::Var { name } => {
+                if let Some(id) = Self::meta_id(name) {
+                    if let Some(bound) = self.lookup(id) {
+                        return self.apply(&bound.clone());
+                    }
+                }
+                Type::Var { name: name.clone() }
+            }
+            Type::Con { .. } => t.clone(),
+            Type::Fn { params, ret, effects } => Type::Fn {
+                params: params.iter().map(|p| self.apply(p)).collect(),
+                ret: Box::new(self.apply(ret)),
+                effects: effects.clone(),
+            },
+            Type::Forall { vars, body } => Type::Forall {
+                vars: vars.clone(),
+                body: Box::new(self.apply(body)),
+            },
+        }
+    }
+}
+
+/// Replaces every var named in `vars` inside `body` with a fresh metavar.
+/// Used at use sites to instantiate a `Forall` type. Returns the
+/// instantiated body and the parallel list of fresh metavars (one per
+/// forall var, same order) — useful for codegen monomorphisation.
+fn instantiate(forall_vars: &[String], body: &Type, counter: &mut u32) -> (Vec<Type>, Type) {
+    let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
+    let mut metas: Vec<Type> = Vec::with_capacity(forall_vars.len());
+    for v in forall_vars {
+        let m = Subst::fresh(counter);
+        mapping.insert(v.clone(), m.clone());
+        metas.push(m);
+    }
+    (metas, substitute_rigids(body, &mapping))
+}
+
+/// Substitutes named rigid vars throughout a type (used by
+/// `instantiate`). Unlike `Subst::apply`, this targets vars by name —
+/// it has no notion of metavar ids.
+fn substitute_rigids(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
+    match t {
+        Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()),
+        Type::Con { .. } => t.clone(),
+        Type::Fn { params, ret, effects } => Type::Fn {
+            params: params.iter().map(|p| substitute_rigids(p, mapping)).collect(),
+            ret: Box::new(substitute_rigids(ret, mapping)),
+            effects: effects.clone(),
+        },
+        Type::Forall { vars, body } => {
+            // Inner forall shadows: only substitute vars not re-bound here.
+            let inner: BTreeMap<String, Type> = mapping
+                .iter()
+                .filter(|(k, _)| !vars.contains(k))
+                .map(|(k, v)| (k.clone(), v.clone()))
+                .collect();
+            Type::Forall {
+                vars: vars.clone(),
+                body: Box::new(substitute_rigids(body, &inner)),
+            }
+        }
+    }
+}
+
+/// Returns true if metavar `id` occurs in `t` (after applying the
+/// current substitution). Used as the occurs check during unification.
+fn occurs(id: u32, t: &Type, subst: &Subst) -> bool {
+    let t = subst.apply(t);
+    match &t {
+        Type::Var { name } => Subst::meta_id(name) == Some(id),
+        Type::Con { .. } => false,
+        Type::Fn { params, ret, .. } => {
+            params.iter().any(|p| occurs(id, p, subst)) || occurs(id, ret, subst)
+        }
+        Type::Forall { body, .. } => occurs(id, body, subst),
+    }
+}
+
+/// Unifies two types under the current substitution. Symmetric. Extends
+/// the substitution as needed, with the standard occurs check.
+fn unify(a: &Type, b: &Type, subst: &mut Subst) -> Result<()> {
+    let a = subst.apply(a);
+    let b = subst.apply(b);
+    match (&a, &b) {
+        // Metavar unification — bind the metavar to the other side.
+        (Type::Var { name }, _) if Subst::meta_id(name).is_some() => {
+            let id = Subst::meta_id(name).unwrap();
+            if let Type::Var { name: bn } = &b {
+                if Subst::meta_id(bn) == Some(id) {
+                    return Ok(()); // same metavar, done
+                }
+            }
+            if occurs(id, &b, subst) {
+                return Err(CheckError::TypeMismatch {
+                    expected: ailang_core::pretty::type_to_string(&a),
+                    got: ailang_core::pretty::type_to_string(&b),
+                });
+            }
+            subst.extend(id, b);
+            Ok(())
+        }
+        (_, Type::Var { name }) if Subst::meta_id(name).is_some() => {
+            let id = Subst::meta_id(name).unwrap();
+            if occurs(id, &a, subst) {
+                return Err(CheckError::TypeMismatch {
+                    expected: ailang_core::pretty::type_to_string(&a),
+                    got: ailang_core::pretty::type_to_string(&b),
+                });
+            }
+            subst.extend(id, a);
+            Ok(())
+        }
+        // Rigid vars: only unify with the same name.
+        (Type::Var { name: an }, Type::Var { name: bn }) if an == bn => Ok(()),
+        // Concrete con: same name.
+        (Type::Con { name: an }, Type::Con { name: bn }) if an == bn => Ok(()),
+        // Function types: zip params, unify ret, effects must match as a set.
+        (
+            Type::Fn { params: ap, ret: ar, effects: ae },
+            Type::Fn { params: bp, ret: br, effects: be },
+        ) => {
+            if ap.len() != bp.len() {
+                return Err(CheckError::TypeMismatch {
+                    expected: ailang_core::pretty::type_to_string(&a),
+                    got: ailang_core::pretty::type_to_string(&b),
+                });
+            }
+            for (x, y) in ap.iter().zip(bp.iter()) {
+                unify(x, y, subst)?;
+            }
+            unify(ar, br, subst)?;
+            let mut ae = ae.clone();
+            let mut be = be.clone();
+            ae.sort();
+            be.sort();
+            if ae != be {
+                return Err(CheckError::TypeMismatch {
+                    expected: ailang_core::pretty::type_to_string(&a),
+                    got: ailang_core::pretty::type_to_string(&b),
+                });
+            }
+            Ok(())
+        }
+        _ => Err(CheckError::TypeMismatch {
+            expected: ailang_core::pretty::type_to_string(&a),
+            got: ailang_core::pretty::type_to_string(&b),
+        }),
+    }
+}
+
 pub mod builtins;
 pub mod diagnostic;
 
@@ -488,17 +692,34 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
             }
             check_type_well_formed(ret, env)
         }
-        Type::Var { .. } | Type::Forall { .. } => {
-            // No type-level polymorphism inside ADT fields in the MVP.
-            Err(CheckError::PolymorphicNotSupported(
-                "type def".into(),
-            ))
+        Type::Var { name } => {
+            // Rigid var: legal iff it is in scope. Used inside a forall
+            // body when checking a polymorphic def.
+            if env.rigid_vars.contains(name) {
+                Ok(())
+            } else {
+                Err(CheckError::PolymorphicNotSupported("type def".into()))
+            }
+        }
+        Type::Forall { .. } => {
+            // ADT fields and lambda annotations cannot themselves be
+            // polymorphic — only top-level def types may carry a Forall.
+            Err(CheckError::PolymorphicNotSupported("type def".into()))
         }
     }
 }
 
 fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
-    let (param_tys, ret_ty, declared_effs) = match &f.ty {
+    // Peel an outer Forall (Iter 12a). The vars become rigid in the
+    // inner env so they pass `check_type_well_formed` and unify only
+    // with themselves. An empty `vars` list (vacuously polymorphic)
+    // gets normalised to a non-polymorphic body.
+    let (rigids, inner_ty): (Vec<String>, Type) = match &f.ty {
+        Type::Forall { vars, body } => (vars.clone(), (**body).clone()),
+        other => (vec![], other.clone()),
+    };
+
+    let (param_tys, ret_ty, declared_effs) = match &inner_ty {
         Type::Fn { params, ret, effects } => {
             (params.clone(), (**ret).clone(), effects.clone())
         }
@@ -518,13 +739,22 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
         });
     }
 
+    // Install rigid vars. Cloning the env keeps the parent immutable
+    // and the rigid set scoped to this def.
+    let mut env = env.clone();
+    for v in &rigids {
+        env.rigid_vars.insert(v.clone());
+    }
+
     let mut locals = IndexMap::new();
     for (n, t) in f.params.iter().zip(param_tys.iter()) {
         locals.insert(n.clone(), t.clone());
     }
     let mut effects = BTreeSet::new();
-    let body_ty = synth(&f.body, env, &mut locals, &mut effects, &f.name)?;
-    expect_eq(&ret_ty, &body_ty)?;
+    let mut subst = Subst::default();
+    let mut counter: u32 = 0;
+    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter)?;
+    unify(&ret_ty, &body_ty, &mut subst)?;
 
     let declared: BTreeSet<String> = declared_effs.into_iter().collect();
     for e in &effects {
@@ -536,10 +766,17 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
 }
 
 fn check_const(c: &ConstDef, env: &Env) -> Result<()> {
+    // Const types are never polymorphic — a Forall here is rejected
+    // outright. Any other type passes through to `synth` as before.
+    if matches!(&c.ty, Type::Forall { .. }) {
+        return Err(CheckError::PolymorphicNotSupported(c.name.clone()));
+    }
     let mut locals = IndexMap::new();
     let mut effects = BTreeSet::new();
-    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name)?;
-    expect_eq(&c.ty, &v)?;
+    let mut subst = Subst::default();
+    let mut counter: u32 = 0;
+    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter)?;
+    unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
         return Err(CheckError::ConstHasEffects(
             c.name.clone(),
@@ -555,6 +792,8 @@ fn synth(
     locals: &mut IndexMap<String, Type>,
     effects: &mut BTreeSet<String>,
     in_def: &str,
+    subst: &mut Subst,
+    counter: &mut u32,
 ) -> Result<Type> {
     match t {
         Term::Lit { lit } => Ok(match lit {
@@ -564,59 +803,62 @@ fn synth(
             Literal::Unit => Type::unit(),
         }),
         Term::Var { name } => {
-            // 1) Locals have highest priority — they can even shadow a
-            //    qualified dotted name, if someone builds a
-            //    letter-with-dot param. Not really reachable in the MVP,
-            //    but harmless.
-            if let Some(t) = locals.get(name) {
-                return Ok(t.clone());
-            }
-            // 2) Local globals.
-            if let Some(t) = env.globals.get(name) {
-                return Ok(t.clone());
-            }
-            // 3) Exactly one dot → qualified cross-module reference.
-            //    More than one dot is undefined in the current MVP
-            //    and falls through below as `unbound-var`.
-            if name.matches('.').count() == 1 {
+            // Lookup precedence: locals → local globals → qualified
+            // cross-module ref. A `Forall` resolved at any of these
+            // levels is instantiated with fresh metavars at the use
+            // site (textbook ML rule); rigid vars and concrete types
+            // pass through unchanged.
+            let raw = if let Some(t) = locals.get(name) {
+                t.clone()
+            } else if let Some(t) = env.globals.get(name) {
+                t.clone()
+            } else if name.matches('.').count() == 1 {
                 let (prefix, suffix) = name.split_once('.').expect("checked");
                 let target_module = match env.imports.get(prefix) {
                     Some(m) => m.clone(),
                     None => {
-                        // Self-reference `<self>.def` without an import entry:
-                        // we deliberately disallow this — by convention,
-                        // qualified references only go through imports.
-                        // That way the meaning of `name` stays locally stable.
                         return Err(CheckError::UnknownModule {
                             module: prefix.to_string(),
                         });
                     }
                 };
                 let g = env.module_globals.get(&target_module).ok_or_else(|| {
-                    // Import map points at a module not loaded in the
-                    // workspace. The workspace loader should have caught
-                    // this already; defensive unknown-module here.
                     CheckError::UnknownModule {
                         module: target_module.clone(),
                     }
                 })?;
-                return g.get(suffix).cloned().ok_or_else(|| {
+                g.get(suffix).cloned().ok_or_else(|| {
                     CheckError::UnknownImport {
                         module: target_module,
                         name: suffix.to_string(),
                     }
-                });
-            }
-            Err(CheckError::UnknownIdent(name.clone()))
+                })?
+            } else {
+                return Err(CheckError::UnknownIdent(name.clone()));
+            };
+            Ok(maybe_instantiate(raw, counter))
         }
         Term::App { callee, args } => {
-            let cty = synth(callee, env, locals, effects, in_def)?;
+            let cty = synth(callee, env, locals, effects, in_def, subst, counter)?;
+            let cty = subst.apply(&cty);
             let (params, ret, fx) = match &cty {
                 Type::Fn { params, ret, effects: fx } => {
                     (params.clone(), (**ret).clone(), fx.clone())
                 }
-                Type::Forall { .. } => {
-                    return Err(CheckError::PolymorphicNotSupported(in_def.to_string()));
+                Type::Forall { vars, body } => {
+                    // Defensive — Var should already have instantiated.
+                    let (_, body) = instantiate(vars, body, counter);
+                    match &body {
+                        Type::Fn { params, ret, effects: fx } => {
+                            (params.clone(), (**ret).clone(), fx.clone())
+                        }
+                        other => {
+                            return Err(CheckError::NotAFunction(
+                                callee_name(callee),
+                                ailang_core::pretty::type_to_string(other),
+                            ));
+                        }
+                    }
                 }
                 other => {
                     return Err(CheckError::NotAFunction(
@@ -633,18 +875,18 @@ fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def)?;
-                expect_eq(exp, &actual)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
+                unify(exp, &actual, subst)?;
             }
             for e in fx {
                 effects.insert(e);
             }
-            Ok(ret)
+            Ok(subst.apply(&ret))
         }
         Term::Let { name, value, body } => {
-            let v = synth(value, env, locals, effects, in_def)?;
+            let v = synth(value, env, locals, effects, in_def, subst, counter)?;
             let prev = locals.insert(name.clone(), v);
-            let r = synth(body, env, locals, effects, in_def)?;
+            let r = synth(body, env, locals, effects, in_def, subst, counter)?;
             match prev {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -656,12 +898,12 @@ fn synth(
             Ok(r)
         }
         Term::If { cond, then, else_ } => {
-            let c = synth(cond, env, locals, effects, in_def)?;
-            expect_eq(&Type::bool_(), &c)?;
-            let t1 = synth(then, env, locals, effects, in_def)?;
-            let t2 = synth(else_, env, locals, effects, in_def)?;
-            expect_eq(&t1, &t2)?;
-            Ok(t1)
+            let c = synth(cond, env, locals, effects, in_def, subst, counter)?;
+            unify(&Type::bool_(), &c, subst)?;
+            let t1 = synth(then, env, locals, effects, in_def, subst, counter)?;
+            let t2 = synth(else_, env, locals, effects, in_def, subst, counter)?;
+            unify(&t1, &t2, subst)?;
+            Ok(subst.apply(&t1))
         }
         Term::Do { op, args } => {
             let sig = env
@@ -677,8 +919,8 @@ fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(sig.params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def)?;
-                expect_eq(exp, &actual)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
+                unify(exp, &actual, subst)?;
             }
             effects.insert(sig.effect.clone());
             Ok(sig.ret)
@@ -707,15 +949,15 @@ fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(cdef.fields.iter()) {
-                let actual = synth(a, env, locals, effects, in_def)?;
-                expect_eq(exp, &actual)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
+                unify(exp, &actual, subst)?;
             }
             Ok(Type::Con {
                 name: type_name.clone(),
             })
         }
         Term::Match { scrutinee, arms } => {
-            let s_ty = synth(scrutinee, env, locals, effects, in_def)?;
+            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter)?;
             if arms.is_empty() {
                 return Err(CheckError::NonExhaustive {
                     ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -727,17 +969,13 @@ fn synth(
             let mut result_ty: Option<Type> = None;
 
             for arm in arms {
-                // Collect local bindings and push into the env, check the
-                // body, pop again — done manually because patterns can
-                // produce multiple bindings.
                 let bindings = type_check_pattern(&arm.pat, &s_ty, env)?;
                 let mut pushed = Vec::new();
                 for (n, t) in &bindings {
                     let prev = locals.insert(n.clone(), t.clone());
                     pushed.push((n.clone(), prev));
                 }
-                let body_ty = synth(&arm.body, env, locals, effects, in_def)?;
-                // Undo bindings.
+                let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter)?;
                 for (n, prev) in pushed.into_iter().rev() {
                     match prev {
                         Some(p) => {
@@ -750,7 +988,7 @@ fn synth(
                 }
 
                 if let Some(rt) = &result_ty {
-                    expect_eq(rt, &body_ty)?;
+                    unify(rt, &body_ty, subst)?;
                 } else {
                     result_ty = Some(body_ty);
                 }
@@ -768,7 +1006,6 @@ fn synth(
                 }
             }
 
-            // Exhaustiveness.
             if !has_open_arm {
                 match &s_ty {
                     Type::Con { name } if env.types.contains_key(name) => {
@@ -794,29 +1031,21 @@ fn synth(
                 }
             }
 
-            Ok(result_ty.expect("checked arms is non-empty"))
+            Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
         }
         Term::Seq { lhs, rhs } => {
-            // Iter 10: `lhs ; rhs`. lhs must be Unit (its value is
-            // discarded). Effects from both sides accumulate. The
-            // expression's type is rhs's type.
-            let lty = synth(lhs, env, locals, effects, in_def)?;
-            expect_eq(&Type::unit(), &lty)?;
-            synth(rhs, env, locals, effects, in_def)
+            let lty = synth(lhs, env, locals, effects, in_def, subst, counter)?;
+            unify(&Type::unit(), &lty, subst)?;
+            synth(rhs, env, locals, effects, in_def, subst, counter)
         }
         Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
-            // Iter 8b: a lambda's type is the declared `Type::Fn`. Push
-            // params as locals, check the body's type matches `ret_ty`,
-            // and ensure body effects are a subset of the declared set.
-            // (We trust the JSON schema for params.len() == param_tys.len();
-            // serde would have rejected a malformed AST.)
             let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
             for (n, t) in params.iter().zip(param_tys.iter()) {
                 let prev = locals.insert(n.clone(), t.clone());
                 pushed.push((n.clone(), prev));
             }
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def);
+            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter);
             for (n, prev) in pushed.into_iter().rev() {
                 match prev {
                     Some(p) => {
@@ -828,12 +1057,7 @@ fn synth(
                 }
             }
             let body_ty = body_ty?;
-            expect_eq(ret_ty, &body_ty)?;
-            // Constructing a lambda is pure — the body's effects are
-            // sealed into the lambda's type, not propagated to the
-            // outer effect set. Calling the lambda (Term::App) will
-            // pick those effects up via Type::Fn.effects.
-            // Body effects must be a subset of the declared lam_effects.
+            unify(ret_ty, &body_ty, subst)?;
             let declared: BTreeSet<String> = lam_effects.iter().cloned().collect();
             for e in &body_effects {
                 if !declared.contains(e) {
@@ -849,6 +1073,17 @@ fn synth(
     }
 }
 
+/// If `t` is a `Forall`, instantiate it with fresh metavars; otherwise
+/// pass through unchanged. Used at every var-resolution site.
+fn maybe_instantiate(t: Type, counter: &mut u32) -> Type {
+    if let Type::Forall { vars, body } = &t {
+        let (_, inst) = instantiate(vars, body, counter);
+        inst
+    } else {
+        t
+    }
+}
+
 /// Checks a pattern against an expected type and returns the bindings
 /// introduced by the pattern.
 fn type_check_pattern(
@@ -933,7 +1168,7 @@ fn expect_eq(expected: &Type, got: &Type) -> Result<()> {
     }
 }
 
-#[derive(Debug, Default)]
+#[derive(Debug, Default, Clone)]
 pub struct Env {
     pub globals: IndexMap<String, Type>,
     pub effect_ops: IndexMap<String, builtins::EffectOpSig>,
@@ -951,6 +1186,11 @@ pub struct Env {
     /// treat self-references (module name == own name) as local globals,
     /// without touching the `imports` channel.
     pub current_module: String,
+    /// Rigid type vars in scope (Iter 12a). Populated by `check_fn` when
+    /// it peels an outer `Forall` from the def's type. Inside the body,
+    /// these names are legal as `Type::Var { name }` and unify only
+    /// with themselves.
+    pub rigid_vars: BTreeSet<String>,
 }
 
 #[derive(Debug, Clone)]
@@ -1211,6 +1451,201 @@ mod tests {
         assert!(format!("{err}").contains("type mismatch"));
     }
 
+    /// Iter 12a: a top-level def annotated `forall a. (a) -> a` is
+    /// admitted; its body checks against a rigid type var. The
+    /// var name (`a`) is in scope as a rigid throughout the body.
+    #[test]
+    fn polymorphic_id_def_typechecks() {
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![fn_def(
+                "id",
+                Type::Forall {
+                    vars: vec!["a".into()],
+                    body: Box::new(Type::Fn {
+                        params: vec![Type::Var { name: "a".into() }],
+                        ret: Box::new(Type::Var { name: "a".into() }),
+                        effects: vec![],
+                    }),
+                },
+                vec!["x"],
+                Term::Var { name: "x".into() },
+            )],
+        };
+        check(&m).expect("polymorphic id should typecheck");
+    }
+
+    /// Iter 12a: `id` instantiates fresh metavars at each use site.
+    /// Calling `id(42)` produces an `Int`; calling `id(true)` would
+    /// produce a `Bool`. Two distinct uses must not bleed into each
+    /// other (each gets its own metavar).
+    #[test]
+    fn polymorphic_id_can_be_used_at_int_and_bool() {
+        let id_def = fn_def(
+            "id",
+            Type::Forall {
+                vars: vec!["a".into()],
+                body: Box::new(Type::Fn {
+                    params: vec![Type::Var { name: "a".into() }],
+                    ret: Box::new(Type::Var { name: "a".into() }),
+                    effects: vec![],
+                }),
+            },
+            vec!["x"],
+            Term::Var { name: "x".into() },
+        );
+        // `use_int` returns id(42) :: Int.
+        let use_int = fn_def(
+            "use_int",
+            Type::Fn {
+                params: vec![],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            vec![],
+            Term::App {
+                callee: Box::new(Term::Var { name: "id".into() }),
+                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
+            },
+        );
+        // `use_bool` returns id(true) :: Bool.
+        let use_bool = fn_def(
+            "use_bool",
+            Type::Fn {
+                params: vec![],
+                ret: Box::new(Type::bool_()),
+                effects: vec![],
+            },
+            vec![],
+            Term::App {
+                callee: Box::new(Term::Var { name: "id".into() }),
+                args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
+            },
+        );
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![id_def, use_int, use_bool],
+        };
+        check(&m).expect("two distinct id instantiations should typecheck");
+    }
+
+    /// Iter 12a: a `Forall` callee at App must instantiate consistently.
+    /// `id(42) :: Bool` is rejected because the metavar gets pinned to
+    /// `Int` by the arg, which conflicts with the declared `Bool` ret.
+    #[test]
+    fn polymorphic_id_consistency_is_enforced() {
+        let id_def = fn_def(
+            "id",
+            Type::Forall {
+                vars: vec!["a".into()],
+                body: Box::new(Type::Fn {
+                    params: vec![Type::Var { name: "a".into() }],
+                    ret: Box::new(Type::Var { name: "a".into() }),
+                    effects: vec![],
+                }),
+            },
+            vec!["x"],
+            Term::Var { name: "x".into() },
+        );
+        // Returns id(42) but declared Bool — must fail.
+        let bad = fn_def(
+            "bad",
+            Type::Fn {
+                params: vec![],
+                ret: Box::new(Type::bool_()),
+                effects: vec![],
+            },
+            vec![],
+            Term::App {
+                callee: Box::new(Term::Var { name: "id".into() }),
+                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
+            },
+        );
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![id_def, bad],
+        };
+        let err = check(&m).unwrap_err();
+        let msg = format!("{err}");
+        assert!(msg.contains("type mismatch"), "got: {msg}");
+    }
+
+    /// Iter 12a: two-var polymorphism. `apply : forall a b. ((a -> b),
+    /// a) -> b`. Body applies the function. We instantiate at two
+    /// different use sites with different (a, b) pairs.
+    #[test]
+    fn polymorphic_apply_with_two_vars() {
+        let apply_def = fn_def(
+            "apply",
+            Type::Forall {
+                vars: vec!["a".into(), "b".into()],
+                body: Box::new(Type::Fn {
+                    params: vec![
+                        Type::Fn {
+                            params: vec![Type::Var { name: "a".into() }],
+                            ret: Box::new(Type::Var { name: "b".into() }),
+                            effects: vec![],
+                        },
+                        Type::Var { name: "a".into() },
+                    ],
+                    ret: Box::new(Type::Var { name: "b".into() }),
+                    effects: vec![],
+                }),
+            },
+            vec!["f", "x"],
+            Term::App {
+                callee: Box::new(Term::Var { name: "f".into() }),
+                args: vec![Term::Var { name: "x".into() }],
+            },
+        );
+        // A monomorphic helper to be passed to apply.
+        let succ = fn_def(
+            "succ",
+            Type::Fn {
+                params: vec![Type::int()],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            vec!["n"],
+            Term::App {
+                callee: Box::new(Term::Var { name: "+".into() }),
+                args: vec![
+                    Term::Var { name: "n".into() },
+                    Term::Lit { lit: Literal::Int { value: 1 } },
+                ],
+            },
+        );
+        let use_apply = fn_def(
+            "use_apply",
+            Type::Fn {
+                params: vec![],
+                ret: Box::new(Type::int()),
+                effects: vec![],
+            },
+            vec![],
+            Term::App {
+                callee: Box::new(Term::Var { name: "apply".into() }),
+                args: vec![
+                    Term::Var { name: "succ".into() },
+                    Term::Lit { lit: Literal::Int { value: 41 } },
+                ],
+            },
+        );
+        let m = Module {
+            schema: SCHEMA.into(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![apply_def, succ, use_apply],
+        };
+        check(&m).expect("apply instantiation should typecheck");
+    }
+
     /// Iter 10: `seq` requires lhs to be Unit. A non-Unit lhs is a
     /// type error — the value of lhs gets discarded so a useful (non-
     /// Unit) value would silently vanish.