diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 08e2840..7d4b48a 100644 --- a/crates/ailang-check/src/lib.rs +++ b/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: "" }` where `` 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" }`. 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` in +/// `Type::Var.name`) to the type they have been unified against. +#[derive(Debug, Default, Clone)] +pub struct Subst { + map: BTreeMap, +} + +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`. + fn meta_id(name: &str) -> Option { + name.strip_prefix("$m").and_then(|s| s.parse::().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) { + let mut mapping: BTreeMap = BTreeMap::new(); + let mut metas: Vec = 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) -> 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 = 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, 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 = 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, effects: &mut BTreeSet, in_def: &str, + subst: &mut Subst, + counter: &mut u32, ) -> Result { 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 `.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 = 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(), <y)?; - synth(rhs, env, locals, effects, in_def) + let lty = synth(lhs, env, locals, effects, in_def, subst, counter)?; + unify(&Type::unit(), <y, 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)> = 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 = 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 = 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, pub effect_ops: IndexMap, @@ -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, } #[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.