//! Typechecker for AILang (MVP).
//!
//! Sits between `ailang-core` (AST + canonical JSON + content hash) and
//! `ailang-codegen` (LLVM IR emit) in the pipeline `core → check →
//! codegen → ail`. Top-level entry points: [`check_module`] (one module,
//! returns [`Diagnostic`]s), [`check_workspace`] (multi-module), and
//! [`check`] (single-error legacy form returning a [`CheckedModule`]).
//!
//! 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 the [`builtins`] table installed
//! into every fresh [`Env`].
//!
//! ## 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};

mod linearity;
mod pre_desugar_validation;
mod reuse_shape;
mod suppress_filter;
pub mod uniqueness;

/// 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 { name, args } => Type::Con {
                name: name.clone(),
                args: args.iter().map(|a| self.apply(a)).collect(),
            },
            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(),
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            Type::Forall { vars, constraints, body } => Type::Forall {
                vars: vars.clone(),
                constraints: constraints.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.
pub(crate) 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 { name, args } => Type::Con {
            name: name.clone(),
            args: args.iter().map(|a| substitute_rigids(a, mapping)).collect(),
        },
        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(),
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        Type::Forall { vars, constraints, 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(),
                constraints: constraints.clone(),
                body: Box::new(substitute_rigids(body, &inner)),
            }
        }
    }
}

/// Iter 23.4: substitute named rigid vars throughout a `Term`,
/// recursing into every sub-Term and applying [`substitute_rigids`]
/// to every embedded `Type` (in `Term::Lam.param_tys`,
/// `Term::Lam.ret_ty`). All other Term variants carry no inline
/// types and recurse structurally.
///
/// Used by `mono::synthesise_mono_fn_for_free_fn` to specialise a
/// polymorphic free-fn body for a specific instantiation. The
/// class-method arm doesn't need this — instance bodies are
/// Lam-unwrapped during synthesis, dropping their `param_tys` —
/// but a free-fn body may carry arbitrary nested Lams whose
/// `param_tys` reference the outer Forall vars.
pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Type>) -> Term {
    use ailang_core::ast::Arm;
    match t {
        Term::Lit { .. } | Term::Var { .. } => t.clone(),
        Term::App { callee, args, tail } => Term::App {
            callee: Box::new(substitute_rigids_in_term(callee, mapping)),
            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
            tail: *tail,
        },
        Term::Let { name, value, body } => Term::Let {
            name: name.clone(),
            value: Box::new(substitute_rigids_in_term(value, mapping)),
            body: Box::new(substitute_rigids_in_term(body, mapping)),
        },
        Term::LetRec { name, ty, params, body, in_term } => Term::LetRec {
            name: name.clone(),
            ty: substitute_rigids(ty, mapping),
            params: params.clone(),
            body: Box::new(substitute_rigids_in_term(body, mapping)),
            in_term: Box::new(substitute_rigids_in_term(in_term, mapping)),
        },
        Term::If { cond, then, else_ } => Term::If {
            cond: Box::new(substitute_rigids_in_term(cond, mapping)),
            then: Box::new(substitute_rigids_in_term(then, mapping)),
            else_: Box::new(substitute_rigids_in_term(else_, mapping)),
        },
        Term::Do { op, args, tail } => Term::Do {
            op: op.clone(),
            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
            tail: *tail,
        },
        Term::Ctor { type_name, ctor, args } => Term::Ctor {
            type_name: type_name.clone(),
            ctor: ctor.clone(),
            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
        },
        Term::Match { scrutinee, arms } => Term::Match {
            scrutinee: Box::new(substitute_rigids_in_term(scrutinee, mapping)),
            arms: arms
                .iter()
                .map(|a| Arm {
                    pat: a.pat.clone(),
                    body: substitute_rigids_in_term(&a.body, mapping),
                })
                .collect(),
        },
        Term::Lam { params, param_tys, ret_ty, effects, body } => Term::Lam {
            params: params.clone(),
            param_tys: param_tys
                .iter()
                .map(|t| substitute_rigids(t, mapping))
                .collect(),
            ret_ty: Box::new(substitute_rigids(ret_ty, mapping)),
            effects: effects.clone(),
            body: Box::new(substitute_rigids_in_term(body, mapping)),
        },
        Term::Seq { lhs, rhs } => Term::Seq {
            lhs: Box::new(substitute_rigids_in_term(lhs, mapping)),
            rhs: Box::new(substitute_rigids_in_term(rhs, mapping)),
        },
        Term::Clone { value } => Term::Clone {
            value: Box::new(substitute_rigids_in_term(value, mapping)),
        },
        Term::ReuseAs { source, body } => Term::ReuseAs {
            source: Box::new(substitute_rigids_in_term(source, mapping)),
            body: Box::new(substitute_rigids_in_term(body, mapping)),
        },
    }
}

/// 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 { args, .. } => args.iter().any(|a| occurs(id, a, subst)),
        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 and same arity, then unify args
        // pointwise. Iter 13a: parameterised ADTs unify arg-by-arg.
        (
            Type::Con { name: an, args: aa },
            Type::Con { name: bn, args: ba },
        ) if an == bn && aa.len() == ba.len() => {
            for (x, y) in aa.iter().zip(ba.iter()) {
                unify(x, y, subst)?;
            }
            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;
pub mod lift;
pub mod mono;

pub use diagnostic::{Diagnostic, Severity};
pub use lift::lift_letrecs;
pub use mono::monomorphise_workspace;

/// Internal error type produced by the typechecker.
///
/// One variant per stable diagnostic code (see [`CheckError::code`]). The
/// [`CheckError::Def`] wrapper attaches the name of the def in which the
/// inner error was raised — recursive accessors ([`CheckError::code`],
/// [`CheckError::ctx`], [`CheckError::message`]) transparently see
/// through the wrapping.
///
/// Typically this enum is converted to [`Diagnostic`] via
/// [`CheckError::to_diagnostic`] before crossing the crate boundary;
/// public API functions [`check_module`] and [`check_workspace`] already
/// return `Vec<Diagnostic>`.
#[derive(Debug, thiserror::Error)]
pub enum CheckError {
    /// Wraps an inner error with the name of the def it occurred in. The
    /// inner error carries the actual code and ctx; the wrapper only the
    /// def context that is later projected onto [`Diagnostic::def`].
    #[error("def `{0}`: {1}")]
    Def(String, Box<CheckError>),

    /// Two types failed to unify. Code: `type-mismatch`.
    #[error("type mismatch: expected {expected}, got {got}")]
    TypeMismatch { expected: String, got: String },

    /// A `Term::Var { name }` could not be resolved against locals,
    /// globals, or the qualified-import path. Code: `unbound-var`.
    #[error("unknown identifier: `{0}`")]
    UnknownIdent(String),

    /// `Term::Do { op }` referenced an op not in
    /// [`Env::effect_ops`]. Code: `unknown-effect-op`.
    #[error("unknown effect operation: `{0}`")]
    UnknownEffectOp(String),

    /// A non-function value was applied with `Term::App`. Code:
    /// `not-a-function`.
    #[error("`{0}` is not a function (got {1})")]
    NotAFunction(String, String),

    /// Wrong number of args at a call site. Code: `arity-mismatch`.
    #[error("arity mismatch for `{name}`: expected {expected} args, got {got}")]
    ArityMismatch {
        name: String,
        expected: usize,
        got: usize,
    },

    /// An effect was raised in a body but not listed on the enclosing
    /// fn's effect row. Code: `undeclared-effect`.
    #[error("undeclared effect `{0}` used in body")]
    UndeclaredEffect(String),

    /// A `Def::Fn` was declared with a non-`Type::Fn` (and non-`Forall<Fn>`)
    /// type. Code: `fn-type-required`.
    #[error("function type required for fn `{0}`, got {1}")]
    FnTypeRequired(String, String),

    /// `FnDef.params.len()` does not match the parameter list of
    /// `FnDef.ty`. Code: `param-count-mismatch`.
    #[error("param count mismatch in `{name}`: type has {ty_count}, params has {param_count}")]
    ParamCountMismatch {
        name: String,
        ty_count: usize,
        param_count: usize,
    },

    /// A `Type::Forall` showed up where the MVP doesn't support
    /// generalisation (e.g. inside `Def::Const`). Code:
    /// `polymorphic-not-supported`.
    #[error("polymorphic types not supported in MVP body of `{0}`")]
    PolymorphicNotSupported(String),

    /// A `Def::Const` body raised an effect — illegal because consts are
    /// pure by construction. Code: `const-has-effects`.
    #[error("const `{0}` may not have effects (got !{1:?})")]
    ConstHasEffects(String, Vec<String>),

    /// A `Type::Con` named a type not in [`Env::types`] or with a wrong
    /// arity for a parameterised ADT. Code: `unknown-type`.
    #[error("unknown type: `{0}`")]
    UnknownType(String),

    /// A `Term::Ctor` referenced a ctor that doesn't belong to the
    /// declared ADT. Code: `unknown-ctor`.
    #[error("type `{ty}` has no constructor `{ctor}`")]
    UnknownCtor { ty: String, ctor: String },

    /// A pattern referenced a ctor that does not exist in the
    /// scrutinee's resolved [`TypeDef`]. The Pattern::Ctor lookup
    /// is type-driven (post-ct.2): it walks `td.ctors` for the
    /// `expected` Type::Con's TypeDef and reports this code when
    /// no ctor of that name is present. Code: `unknown-ctor-in-pattern`.
    #[error("unknown constructor `{0}` in pattern")]
    UnknownCtorInPattern(String),

    /// Wrong number of fields in a ctor application or pattern. Code:
    /// `arity-mismatch` (shared with `ArityMismatch`).
    #[error("constructor `{ty}/{ctor}` arity: expected {expected} fields, got {got}")]
    CtorArity {
        ty: String,
        ctor: String,
        expected: usize,
        got: usize,
    },

    /// A `Term::Match` does not cover every ctor of an ADT (and has no
    /// open arm). Code: `non-exhaustive-match`. `ctx` carries the
    /// `missing` ctor names.
    #[error("non-exhaustive match on `{ty}`: missing cases {missing:?}")]
    NonExhaustive { ty: String, missing: Vec<String> },

    /// A `Term::Match` on a primitive type lacks a wildcard or var arm.
    /// Code: `primitive-needs-wildcard`.
    #[error("primitive type `{0}` requires a wildcard or variable arm in match")]
    PrimitiveNeedsWildcard(String),

    /// A `Pattern::Lit` matched against a `Literal::Float`. Float
    /// patterns are semantically dubious (NaN never matches via
    /// IEEE-`==`; equality is bit-exact not approximate), so the
    /// typechecker hard-rejects them. The surface lex / parser
    /// accept the syntax (iter 2); this diagnostic surfaces at
    /// typecheck time. Code: `float-pattern-not-allowed`.
    #[error("float-literal patterns are not allowed: use ordering operators (`<`, `>`, ...) and `is_nan` to discriminate floats")]
    FloatPatternNotAllowed,

    /// A `Pattern::Ctor` was matched against a value of a different ADT.
    /// Code: `pattern-type-mismatch`.
    #[error("cannot match constructor pattern `{ctor}` against type `{ty}`")]
    PatternTypeMismatch { ctor: String, ty: String },

    /// Two `Def::Type` defs share a name. Code: `duplicate-type`.
    #[error("duplicate type definition: `{0}`")]
    DuplicateType(String),

    /// Same ctor name registered in two different ADTs. Code:
    /// `duplicate-ctor`.
    #[error("duplicate constructor: `{ctor}` (in types `{a}` and `{b}`)")]
    DuplicateCtor { ctor: String, a: String, b: String },

    /// Two top-level defs in the same module share a name. Code:
    /// `duplicate-def`.
    #[error("duplicate definition: `{0}`")]
    DuplicateDef(String),

    /// A `Pattern::Ctor` has a [`Pattern::Lit`] sub-pattern. Iter 16a
    /// added an AST-level desugar that flattens nested **Ctor**
    /// sub-patterns before the checker sees the module, so this
    /// diagnostic now fires only for literal sub-patterns inside a
    /// Ctor (still out of scope; a future iter would lower them as a
    /// nested Match on the field). Code:
    /// `nested-ctor-pattern-not-allowed`.
    #[error("nested constructor pattern not allowed in MVP: `{0}`")]
    NestedCtorPatternNotAllowed(String),

    /// A qualified `Term::Var { name: "<m>.<n>" }` references a module
    /// alias not declared in the current module's imports. Code:
    /// `unknown-module`.
    #[error("unknown module prefix `{module}` in qualified reference")]
    UnknownModule { module: String },

    /// The aliased module exists but does not export the named def.
    /// Code: `unknown-import`.
    #[error("module `{module}` has no top-level def `{name}`")]
    UnknownImport { module: String, name: String },

    /// A def was declared with a name containing `.`, which is reserved
    /// for qualified cross-module references. Code: `invalid-def-name`.
    #[error("invalid def name `{name}`: contains `.` (reserved for qualified refs)")]
    InvalidDefName { name: String },

    /// Iter 14e: a `Term::App { tail: true, .. }` or
    /// `Term::Do { tail: true, .. }` was found in a non-tail position.
    /// Code: `tail-call-not-in-tail-position`. See Decision 8.
    #[error("call marked `tail` is not in tail position")]
    TailCallNotInTailPosition,

    /// Iter 18d.1: a `Term::ReuseAs { body, .. }` was found whose `body`
    /// is not an allocating Term variant (i.e. not `Term::Ctor` and not
    /// `Term::Lam`). `(reuse-as ...)` only makes sense when the body
    /// produces a fresh allocation that can take over the source's
    /// memory slot; otherwise the wrapper is meaningless and is
    /// rejected at typecheck. Code: `reuse-as-non-allocating-body`.
    /// `ctx`: `{"got": "<term-tag>"}`. The `body_form_a` field carries
    /// the form-A spelling of the inner body so [`Self::to_diagnostic`]
    /// can attach a `SuggestedRewrite` that drops the wrapper.
    #[error("reuse-as body must be an allocating term (Term::Ctor or Term::Lam), got {got}")]
    ReuseAsNonAllocatingBody { got: String, body_form_a: String },

    /// Iter 22b.2 (Task 9): a polymorphic `FnDef` calls a class method
    /// (e.g. `show x` where `x: a`), producing a residual class
    /// constraint `(class, a)` at the call site, but the fn's declared
    /// `Forall.constraints` does not list that constraint (and the
    /// one-step superclass-expansion of the declared set still does
    /// not cover it). Without an in-scope constraint, monomorphisation
    /// (22b.3) would have no dictionary to thread, so this is a hard
    /// soundness error. Code: `missing-constraint`. `ctx`:
    /// `{"class": "<C>", "method": "<m>", "at_type": "<a>"}`.
    /// Concrete-type residuals (`Type::Con`) are deferred to Task 10's
    /// `no-instance` diagnostic.
    #[error(
        "fn `{def}` calls class method `{method}` (class `{class}`) at type `{at_type}`, \
        but its declared constraints do not include `{class} {at_type}`"
    )]
    MissingConstraint {
        def: String,
        method: String,
        class: String,
        at_type: String,
    },

    /// Iter 22b.2 (Task 10): a `FnDef` calls a class method at a
    /// fully-concrete type (e.g. `show 42` resolves the residual class
    /// param to `Int`), but the workspace registry has no
    /// `instance class at_type` entry. This is the dual of
    /// `MissingConstraint`: when the residual type is concrete, the fn
    /// cannot push the obligation to a caller via `Forall.constraints`
    /// — it can only be discharged by an existing instance. Without a
    /// matching registry entry, monomorphisation (22b.3) would have no
    /// dictionary to substitute. Code: `no-instance`. `ctx`:
    /// `{"class": "<C>", "method": "<m>", "at_type": "<T>"}`.
    #[error(
        "fn `{def}` calls `{method}` requiring `instance {class} {at_type}`, \
        but no such instance exists in the workspace"
    )]
    NoInstance {
        def: String,
        method: String,
        class: String,
        at_type: String,
    },

    /// Iter 22b.3: an internal invariant in the typechecker / mono pass
    /// was violated — surfaced as an error so callers can propagate
    /// rather than abort, but in well-formed inputs (typecheck has
    /// succeeded) it must never fire. Code: `internal`.
    #[error("internal: {0}")]
    Internal(String),
}

pub(crate) type Result<T> = std::result::Result<T, CheckError>;

impl CheckError {
    /// Stable kebab-case code for machine consumption (`ail check --json`).
    /// Passed through recursively via the `Def` wrapping — the inner error
    /// carries the actual code, the wrapper only the def context.
    pub fn code(&self) -> &'static str {
        match self {
            CheckError::Def(_, inner) => inner.code(),
            CheckError::TypeMismatch { .. } => "type-mismatch",
            CheckError::UnknownIdent(_) => "unbound-var",
            CheckError::UnknownEffectOp(_) => "unknown-effect-op",
            CheckError::NotAFunction(..) => "not-a-function",
            CheckError::ArityMismatch { .. } => "arity-mismatch",
            CheckError::UndeclaredEffect(_) => "undeclared-effect",
            CheckError::FnTypeRequired(..) => "fn-type-required",
            CheckError::ParamCountMismatch { .. } => "param-count-mismatch",
            CheckError::PolymorphicNotSupported(_) => "polymorphic-not-supported",
            CheckError::ConstHasEffects(..) => "const-has-effects",
            CheckError::UnknownType(_) => "unknown-type",
            CheckError::UnknownCtor { .. } => "unknown-ctor",
            CheckError::UnknownCtorInPattern(_) => "unknown-ctor-in-pattern",
            CheckError::CtorArity { .. } => "arity-mismatch",
            CheckError::NonExhaustive { .. } => "non-exhaustive-match",
            CheckError::PrimitiveNeedsWildcard(_) => "primitive-needs-wildcard",
            CheckError::FloatPatternNotAllowed => "float-pattern-not-allowed",
            CheckError::PatternTypeMismatch { .. } => "pattern-type-mismatch",
            CheckError::DuplicateType(_) => "duplicate-type",
            CheckError::DuplicateCtor { .. } => "duplicate-ctor",
            CheckError::DuplicateDef(_) => "duplicate-def",
            CheckError::NestedCtorPatternNotAllowed(_) => "nested-ctor-pattern-not-allowed",
            CheckError::UnknownModule { .. } => "unknown-module",
            CheckError::UnknownImport { .. } => "unknown-import",
            CheckError::InvalidDefName { .. } => "invalid-def-name",
            CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position",
            CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
            CheckError::MissingConstraint { .. } => "missing-constraint",
            CheckError::NoInstance { .. } => "no-instance",
            CheckError::Internal(_) => "internal",
        }
    }

    /// Structured context for a diagnostic. Lands directly in the JSON
    /// under the key `ctx`. Empty object when no context is available.
    pub fn ctx(&self) -> serde_json::Value {
        match self {
            CheckError::Def(_, inner) => inner.ctx(),
            CheckError::TypeMismatch { expected, got } => {
                serde_json::json!({"expected": expected, "actual": got})
            }
            CheckError::ArityMismatch { expected, got, .. } => {
                serde_json::json!({"expected": expected, "actual": got})
            }
            CheckError::CtorArity {
                expected, got, ..
            } => serde_json::json!({"expected": expected, "actual": got}),
            CheckError::ParamCountMismatch {
                ty_count,
                param_count,
                ..
            } => serde_json::json!({"expected": ty_count, "actual": param_count}),
            CheckError::NonExhaustive { missing, .. } => {
                serde_json::json!({"missing": missing})
            }
            CheckError::UnknownModule { module } => {
                serde_json::json!({"module": module})
            }
            CheckError::UnknownImport { module, name } => {
                serde_json::json!({"module": module, "name": name})
            }
            CheckError::InvalidDefName { name } => {
                serde_json::json!({"name": name, "reason": "contains-dot"})
            }
            CheckError::ReuseAsNonAllocatingBody { got, .. } => {
                serde_json::json!({"got": got})
            }
            CheckError::MissingConstraint { class, method, at_type, .. } => {
                serde_json::json!({"class": class, "method": method, "at_type": at_type})
            }
            CheckError::NoInstance { class, method, at_type, .. } => {
                serde_json::json!({"class": class, "method": method, "at_type": at_type})
            }
            _ => serde_json::Value::Object(serde_json::Map::new()),
        }
    }

    /// If this error is wrapped by [`CheckError::Def`], returns the name
    /// of the affected def. Otherwise `None`.
    pub fn def(&self) -> Option<&str> {
        match self {
            CheckError::Def(n, _) => Some(n.as_str()),
            _ => None,
        }
    }

    /// Unwraps the error potentially wrapped by [`CheckError::Def`].
    pub fn inner(&self) -> &CheckError {
        match self {
            CheckError::Def(_, inner) => inner.inner(),
            other => other,
        }
    }

    /// Non-`Def`-wrapped message. Without the `def: ...` prefix.
    pub fn message(&self) -> String {
        format!("{}", self.inner())
    }

    /// Lowers this error into the public [`Diagnostic`] shape consumed
    /// by `ail check --json`. Pulls `code`, `message`, and `ctx` through
    /// the recursive accessors and attaches the optional def name from
    /// any wrapping [`CheckError::Def`].
    pub fn to_diagnostic(&self) -> Diagnostic {
        let mut d = Diagnostic::error(self.code(), self.message()).with_ctx(self.ctx());
        if let Some(name) = self.def() {
            d = d.with_def(name);
        }
        // Iter 18d.1: typecheck-side suggested_rewrites for the
        // reuse-as-non-allocating-body diagnostic. The replacement is
        // simply the body without the `(reuse-as ...)` wrapper — the
        // hint is meaningless here, so drop it.
        if let CheckError::ReuseAsNonAllocatingBody { body_form_a, .. } = self.inner() {
            d = d.with_suggested_rewrite(
                "drop the meaningless reuse-as wrapper around the non-allocating body",
                body_form_a.clone(),
            );
        }
        // Iter 23.5: Float-aware addendum on `NoInstance`. When the
        // unresolved class is `Eq` or `Ord` AND the type is `Float`,
        // append a cross-reference to DESIGN.md §"Float semantics" so
        // the LLM author learns the partial-Float story immediately
        // rather than seeing a bare "no instance" message. Float has
        // neither Eq nor Ord by design (partial orderability per
        // IEEE-754), and the polymorphic prelude helpers
        // (`ne` / `lt` / `le` / `gt` / `ge` / direct `eq` / `compare`)
        // are the natural surface where the LLM hits this.
        if let CheckError::NoInstance { class, at_type, .. } = self.inner() {
            if (class == "Eq" || class == "Ord") && at_type == "Float" {
                d.message = format!(
                    "{} — Float has no Eq/Ord instance by design (partial \
                     orderability per IEEE-754); see DESIGN.md §\"Float semantics\".",
                    d.message
                );
            }
        }
        d
    }
}

/// Top-level API for structured diagnostics.
///
/// Empty Vec = green. From Iter 6 onwards the body-check phase is
/// multi-diagnose: each def in each module is checked independently and
/// failures accumulate, so a single `ail check` run reports every
/// independent body error in the workspace.
///
/// Pass-1 errors (top-level symbol-table construction:
/// `invalid-def-name`, `duplicate-def`) are still fail-fast — those
/// errors corrupt the symbol table, and any further diagnostic would be
/// unreliable. Likewise, the type-def installation is fail-fast within
/// a single module, but other modules continue being checked.
///
/// Backwards compatibility: a bare `&Module` is internally lifted into a
/// trivial workspace (`modules = {m.name: m}`, `entry = m.name`) so that
/// tooling checking individual modules avoids building a `Workspace`.
/// Modules with imports on other modules not present in the trivial
/// workspace will inevitably produce `unknown-module` errors on qualified
/// references — which is correct.
pub fn check_module(m: &Module) -> Vec<Diagnostic> {
    // Iter 16a: flatten nested constructor patterns before any check
    // logic touches the AST. The rewrite is pure and runs in memory;
    // canonical-JSON hashes (computed by `ailang_core::load_module` /
    // `def_hash`) are unaffected because they use the on-disk form.
    let m = ailang_core::desugar::desugar_module(m);
    let mut modules = BTreeMap::new();
    modules.insert(m.name.clone(), m.clone());
    let ws = Workspace {
        entry: m.name.clone(),
        modules,
        root_dir: std::path::PathBuf::from("."),
        // Iter 22b.1: single-module check_module entry point does not
        // build a registry. The registry is workspace-load-time
        // metadata; check_module is invoked from in-memory paths
        // (tests, single-file CLI) where no workspace DFS happened.
        // Once 22b.2 typecheck arms read the registry, those paths
        // will need to populate it from the in-memory module too.
        registry: ailang_core::workspace::Registry::default(),
    };
    check_workspace(&ws)
}

/// Top-level API for cross-module typecheck.
///
/// Iterates over all modules of the workspace and checks each with access
/// to the top-level symbol tables of all other modules. Qualified
/// references are resolved via the import map of the respective module:
/// `Term::Var { name }` with exactly one dot in the name is interpreted
/// as `<prefix>.<def>`; `<prefix>` is an import alias (or the module name,
/// if imported without an alias).
///
/// Multi-diagnose: pass-2 collects diagnostics per def across all modules.
/// Pass-1 (symbol table) stays fail-fast — see [`check_module`].
/// Module iteration order is deterministic: entry first, then the rest in
/// BTreeMap order, so output ordering is stable.
pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
    // Floats milestone post-fieldtest B1: hard-reject
    // `Pattern::Lit { Literal::Float }` before desugar rewrites lit
    // arms into `(== scrutinee lit)`. See `pre_desugar_validation`
    // for the full rationale. Walked per-def so the diagnostic
    // carries the offending def's name; modules are visited in
    // BTreeMap order, defs in declaration order. All hits in this
    // pass are accumulated and returned together (consistent with
    // pass-2 multi-diagnose); if any are present, later passes do
    // not run, since a violating Float-lit pattern would otherwise
    // be silently rewritten by desugar before typecheck.
    {
        let mut pre_desugar_errors: Vec<Diagnostic> = Vec::new();
        for m in ws.modules.values() {
            for def in &m.defs {
                if let Err(e) = pre_desugar_validation::reject_float_patterns_in_def(def) {
                    let wrapped = CheckError::Def(def.name().to_string(), Box::new(e));
                    pre_desugar_errors.push(wrapped.to_diagnostic());
                }
            }
        }
        if !pre_desugar_errors.is_empty() {
            return pre_desugar_errors;
        }
    }
    // Iter 16a: desugar every module of the workspace before any check
    // logic runs. The rewrite is pure and per-module; we rebuild a
    // workspace shell around the desugared modules (paths and entry
    // are unchanged).
    let ws_owned = Workspace {
        entry: ws.entry.clone(),
        modules: ws
            .modules
            .iter()
            .map(|(k, m)| (k.clone(), ailang_core::desugar::desugar_module(m)))
            .collect(),
        root_dir: ws.root_dir.clone(),
        // Iter 22b.1: pass the registry through unchanged. The desugar
        // pass does not touch class/instance defs (see desugar.rs:
        // 22b.1 passthrough), so the registry built at load time
        // remains valid against the desugared modules.
        registry: ws.registry.clone(),
    };
    let ws = &ws_owned;
    // Pass 1: build per-module top-level symbol table — without checking
    // bodies. This lets module A access defs from module B even when B
    // comes later in the BTreeMap. Duplicate def names and dot-in-def
    // names are reported here immediately, because without clean symbol
    // tables all further diagnostics would be unreliable.
    let module_globals = match build_module_globals(ws) {
        Ok(g) => g,
        Err(e) => return vec![e.to_diagnostic()],
    };

    // Pass 2: body-check per module. `check_in_workspace` builds the env
    // with additional cross-module globals and an import map. Errors
    // accumulate across modules.
    let mut order: Vec<&String> = Vec::new();
    if ws.modules.contains_key(&ws.entry) {
        order.push(&ws.entry);
    }
    for name in ws.modules.keys() {
        if name != &ws.entry {
            order.push(name);
        }
    }
    let mut diagnostics: Vec<Diagnostic> = Vec::new();
    for name in order {
        let m = &ws.modules[name];
        let typecheck_errors = check_in_workspace(m, ws, &module_globals);
        let had_typecheck_errors = !typecheck_errors.is_empty();
        // Per-module diagnostic accumulator. The suppress filter
        // (Iter 19b) runs at the end of the per-module block, so
        // we keep this module's diagnostics in their own vec while
        // accumulating, then merge into the workspace-wide list.
        let mut module_diags: Vec<Diagnostic> = Vec::new();
        for e in typecheck_errors {
            module_diags.push(e.to_diagnostic());
        }
        // Iter 18c.2: linearity check runs only on modules that
        // typechecked clean. Running it on a body that already has a
        // type error would wade into a partly-defined IR (e.g.
        // unresolved Var lookups, mismatched ctor arities) and produce
        // noise. Cleanly-typechecked modules with at least one
        // all-explicit-mode fn are exactly the surface the check is
        // designed to inspect.
        if !had_typecheck_errors {
            // Iter 23.5: linearity check needs visibility into
            // polymorphic free fns + class methods from implicitly-
            // imported modules (currently just the auto-injected
            // prelude). Without this, a Borrow-mode user fn that
            // forwards its borrow params into a prelude poly fn
            // (e.g. `gt x y`) fires `consume-while-borrowed`
            // false positives because `callee_arg_modes` defaults
            // to Consume when it cannot see the callee's
            // `param_modes`. Symmetric to the class-method case
            // closed in iter 23.4-prep.
            let visible_extra: Vec<&Module> = ws
                .modules
                .iter()
                .filter_map(|(other_name, other_mod)| {
                    if other_name == name {
                        None
                    } else {
                        Some(other_mod)
                    }
                })
                .collect();
            module_diags.extend(linearity::check_module_with_visible(m, &visible_extra));
            // Iter 18d.2: reuse-as shape compatibility check. Runs on
            // the same activation gate as linearity (all-explicit-mode
            // fns only). The check resolves each `(reuse-as <var>
            // <body-ctor>)` site against the path-ctor of `<var>` and
            // rejects mismatches with `reuse-as-shape-mismatch`. Runs
            // after linearity so its output appears after linearity's
            // diagnostics for the same def — stable ordering for the
            // JSON consumer.
            module_diags.extend(reuse_shape::check_module(m));
        }
        // Iter 19b: apply per-fn `suppress` filter. Runs after every
        // diagnostic source has appended so any code the author
        // listed can actually be matched. Drops matching diagnostics
        // and pushes `empty-suppress-reason` (Error) for malformed
        // entries. See [`crate::suppress_filter`] for details.
        suppress_filter::apply(m, &mut module_diags);
        diagnostics.extend(module_diags);
    }
    diagnostics
}

/// Result of typechecking a module: mapping from symbol name to
/// (type, hash) — ready for `manifest` output.
#[derive(Debug, Clone)]
pub struct CheckedModule {
    /// Top-level symbols of the module in declaration order. The value
    /// is `(declared_type, content_hash)` — the hash is the BLAKE3 def
    /// hash from `ailang_core::hash::def_hash`, used by `ail diff` and
    /// the cross-module manifest.
    pub symbols: IndexMap<String, (Type, String)>,
}

/// Single-error entry point. Typechecks `m` standalone (trivial
/// workspace), returning a [`CheckedModule`] with the symbol-to-hash
/// table on success or the **first** [`CheckError`] on failure.
///
/// Prefer [`check_module`] for new callers — it returns
/// `Vec<Diagnostic>` (multi-diagnose, JSON-ready). This function is
/// kept for legacy callers (snapshot tests, the `manifest` codepath
/// that needs the hash-to-type mapping).
pub fn check(m: &Module) -> Result<CheckedModule> {
    // Floats milestone post-fieldtest B1: hard-reject
    // `Pattern::Lit { Literal::Float }` before desugar runs, because
    // `desugar::build_eq` rewrites lit-pattern arms (Float included)
    // into `(== scrutinee lit)` and would otherwise hide the
    // unreachable Float-pattern arm in `type_check_pattern`. See
    // `pre_desugar_validation` for the full rationale.
    pre_desugar_validation::reject_float_patterns_in_module(m)?;
    // Iter 16a: desugar nested ctor patterns before constructing the
    // trivial workspace. See `check_module` for the rationale. The
    // returned `CheckedModule.symbols` content hashes are derived from
    // the *original* on-disk module so they keep the canonical-bytes
    // identity that `ail diff` / `ail manifest` rely on.
    let original = m;
    let desugared = ailang_core::desugar::desugar_module(m);
    let m = &desugared;
    // Trivial workspace: the module alone, without cross-module resolution.
    let mut modules = BTreeMap::new();
    modules.insert(m.name.clone(), m.clone());
    let ws = Workspace {
        entry: m.name.clone(),
        modules,
        root_dir: std::path::PathBuf::from("."),
        // Iter 22b.1: the legacy single-module `check` entry point
        // builds an empty registry. See `check_module` for the same
        // pattern; once 22b.2 typecheck arms read the registry, both
        // paths must populate it from the in-memory module.
        registry: ailang_core::workspace::Registry::default(),
    };
    let module_globals = build_module_globals(&ws)?;
    // `check` keeps single-error semantics for callers (snapshot tests,
    // legacy code). Multi-diagnose is exposed via `check_module` /
    // `check_workspace`.
    if let Some(first) = check_in_workspace(m, &ws, &module_globals).into_iter().next() {
        return Err(first);
    }
    // Collect symbols for the return value (existing semantics).
    // Hashes are computed over the *original* defs, so callers like
    // `ail diff` see the on-disk identity, not a post-desugar one.
    let mut symbols = IndexMap::new();
    for def in &original.defs {
        let h = ailang_core::hash::def_hash(def);
        let ty = match def {
            Def::Fn(f) => f.ty.clone(),
            Def::Const(c) => c.ty.clone(),
            Def::Type(_) => Type::Con {
                name: def.name().to_string(),
                args: vec![],
            },
            // Iter 22b.1: class/instance defs are not yet checked.
            // The symbols map is keyed by definition name; class/
            // instance contribute their class name, but with no
            // concrete pre-monomorphisation type we represent them
            // as a placeholder Con. Tools that consume this map
            // (`ail diff`, `ail manifest`) read kind separately
            // via `def_kind`, so the placeholder type does not
            // mislead them.
            Def::Class(_) | Def::Instance(_) => Type::Con {
                name: def.name().to_string(),
                args: vec![],
            },
        };
        symbols.insert(def.name().to_string(), (ty, h));
    }
    Ok(CheckedModule { symbols })
}

/// Iter 16b.3: typecheck `m` and return both the [`CheckedModule`]
/// (for tooling that wants the original on-disk symbol identities)
/// AND the lifted module ready for codegen — i.e. the desugared
/// module with every surviving `Term::LetRec` replaced by a
/// synthetic top-level `Def::Fn`.
///
/// The check phase runs unchanged: same desugar, same typecheck,
/// same `CheckedModule.symbols` (built from the original `m`'s
/// defs). On success, the desugared module is fed through
/// [`lift_letrecs`] and the result is returned alongside.
///
/// `build` / `run` go through this entry; the `check` subcommand
/// stays on the legacy [`check`] entry (no lift needed for
/// type-checking only).
pub fn check_and_lift(m: &Module) -> Result<(CheckedModule, Module)> {
    let cm = check(m)?;
    // Run desugar exactly as `check` does. The `check` call already
    // ran desugar internally, but its result is discarded (only the
    // CheckedModule survives), so we have to re-run it here to get
    // the post-desugar form for the lift.
    let desugared = ailang_core::desugar::desugar_module(m);
    let lifted = lift_letrecs(&desugared)?;
    Ok((cm, lifted))
}

/// Iter 15a: builds the ADT type-def table per module. Sibling of
/// [`build_module_globals`]: gives the body checker O(1) lookup of any
/// type declared anywhere in the workspace, keyed by module name.
/// Read by qualified `Type::Con.name` resolution
/// (`module.Type`), qualified `Term::Ctor.type_name`, and the
/// cross-module `Pattern::Ctor` fallback. Duplicate type / ctor errors
/// inside a single module surface during the per-module body-check
/// phase, not here.
pub(crate) fn build_module_types(
    ws: &Workspace,
) -> BTreeMap<String, IndexMap<String, TypeDef>> {
    let mut out: BTreeMap<String, IndexMap<String, TypeDef>> = BTreeMap::new();
    for (mname, m) in &ws.modules {
        let mut tys = IndexMap::new();
        for def in &m.defs {
            if let Def::Type(td) = def {
                // Last definition wins on duplicate; the per-module
                // body-check phase reports `duplicate-type` separately.
                tys.insert(td.name.clone(), td.clone());
            }
        }
        out.insert(mname.clone(), tys);
    }
    out
}

/// Iter 22b.2: per-module top-level symbol table. Holds the classic
/// fn/const/type-name-to-type mapping in [`Self::fns`] and class-method
/// names in [`Self::class_methods`]. The two channels are kept separate
/// because class-method resolution at a call site needs more context
/// than a plain `Type` lookup (the owning class, the class param name,
/// and the defining module — see [`ClassMethodEntry`]). Pre-22b.2 the
/// inner shape was `IndexMap<String, Type>`; 22b.2 wraps that in this
/// struct so call sites that only need fn lookup can keep using
/// `mod_globals.fns` while typeclass code goes through `class_methods`.
#[derive(Debug, Default, Clone)]
pub struct ModuleGlobals {
    /// Top-level fn / const / type symbols, by name. The pre-22b.2 inner
    /// shape — every call site that only needs HM lookup goes through
    /// here.
    pub fns: IndexMap<String, Type>,
    /// Class-method names, by method name. Populated in
    /// [`build_module_globals`] from `Def::Class` entries; consulted by
    /// the 22b.2 `missing-constraint` / `no-instance` arms (Tasks 9 / 10).
    /// `IndexMap` matches the sibling [`Self::fns`] channel and preserves
    /// definition order — Tasks 9 / 10 may surface diagnostics in source
    /// order, and downstream consumers should not depend on a sorted
    /// iteration order they did not ask for.
    pub class_methods: IndexMap<String, ClassMethodEntry>,
}

impl ModuleGlobals {
    /// True if `name` is a class method declared in this module.
    pub fn has_class_method(&self, name: &str) -> bool {
        self.class_methods.contains_key(name)
    }

    /// The class that declared the method `name`, or `None` if `name`
    /// is not a class method in this module.
    pub fn class_method_class(&self, name: &str) -> Option<&str> {
        self.class_methods
            .get(name)
            .map(|e| e.class_name.as_str())
    }

    /// The full [`ClassMethodEntry`] for method `name`, or `None` if
    /// `name` is not a class method in this module. Tasks 9 / 10 use
    /// this to read `method_ty` and `defining_module` together; the
    /// narrower `has_class_method` / `class_method_class` accessors
    /// stay for callers that only need a yes/no or the class name.
    pub fn class_method(&self, name: &str) -> Option<&ClassMethodEntry> {
        self.class_methods.get(name)
    }
}

/// Iter 22b.2: per-class-method metadata stored in
/// [`ModuleGlobals::class_methods`]. Carries everything the 22b.2
/// typecheck arms (`missing-constraint`, `no-instance`) need to resolve
/// a `Term::Var { name }` that refers to a class method into a residual
/// class constraint at the call site.
#[derive(Debug, Clone)]
pub struct ClassMethodEntry {
    /// The class that declared the method (e.g. `Show` for `show`).
    pub class_name: String,
    /// The class's single type parameter name (e.g. `a` in
    /// `class Show a`). The class param appears at this name inside
    /// [`Self::method_ty`].
    pub class_param: String,
    /// The method's declared signature — a `Type::Fn` whose param /
    /// return positions may contain `Type::Var { name: class_param }`.
    /// Task 9 instantiates the class param with a fresh metavar at the
    /// call site to build the residual constraint.
    pub method_ty: Type,
    /// Module that declared the class. Tasks 9 / 10 use this to find
    /// the matching `Registry` entries when checking constraints.
    pub defining_module: String,
}

/// Builds the top-level symbol table per module (for cross-module lookup),
/// without checking bodies. Duplicates and dot-in-def names are reported
/// here as errors immediately — they would taint all further diagnostics.
///
/// Iter 22b.2 (Task 8): also collects class-method names from `Def::Class`
/// into [`ModuleGlobals::class_methods`], so that pass-2 lookup of a
/// class method via `Term::Var { name }` resolves to a known global
/// rather than firing `unbound-var`. The class-method channel is kept
/// separate from the fn / const / type channel because resolution
/// downstream needs the owning class and class-param name to build a
/// residual constraint at the call site.
pub fn build_module_globals(
    ws: &Workspace,
) -> Result<BTreeMap<String, ModuleGlobals>> {
    let mut out: BTreeMap<String, ModuleGlobals> = BTreeMap::new();
    for (mname, m) in &ws.modules {
        let mut globals = ModuleGlobals::default();
        for def in &m.defs {
            let def_name = def.name();
            if def_name.contains('.') {
                return Err(CheckError::Def(
                    def_name.to_string(),
                    Box::new(CheckError::InvalidDefName {
                        name: def_name.to_string(),
                    }),
                ));
            }
            // Iter 22b.2: pre-22b.2 the dup check ran across the single
            // `IndexMap<String, Type>`, but class / instance defs early-
            // `continue`d before the insert, so they never participated
            // in dup detection (and `instance Foo` re-using the class
            // name is legal). Preserving that, dup detection here is
            // scoped to the `fns` channel exactly as before. Class /
            // instance coherence (orphan / duplicate-instance /
            // missing-method / method-name-collision) is enforced
            // earlier at `workspace::build_registry`.
            match def {
                Def::Fn(f) => {
                    if globals.fns.contains_key(def_name) {
                        return Err(CheckError::Def(
                            def_name.to_string(),
                            Box::new(CheckError::DuplicateDef(def_name.to_string())),
                        ));
                    }
                    globals.fns.insert(def_name.to_string(), f.ty.clone());
                }
                Def::Const(c) => {
                    if globals.fns.contains_key(def_name) {
                        return Err(CheckError::Def(
                            def_name.to_string(),
                            Box::new(CheckError::DuplicateDef(def_name.to_string())),
                        ));
                    }
                    globals.fns.insert(def_name.to_string(), c.ty.clone());
                }
                Def::Type(_) => {
                    if globals.fns.contains_key(def_name) {
                        return Err(CheckError::Def(
                            def_name.to_string(),
                            Box::new(CheckError::DuplicateDef(def_name.to_string())),
                        ));
                    }
                    globals.fns.insert(
                        def_name.to_string(),
                        Type::Con {
                            name: def_name.to_string(),
                            args: vec![],
                        },
                    );
                }
                Def::Class(cd) => {
                    // Iter 22b.2 (Task 8): register every method
                    // declared by the class as a class-method global,
                    // with enough metadata for the typecheck arms in
                    // Tasks 9 / 10 to build a residual constraint at
                    // the call site.
                    for meth in &cd.methods {
                        globals.class_methods.insert(
                            meth.name.clone(),
                            ClassMethodEntry {
                                class_name: cd.name.clone(),
                                class_param: cd.param.clone(),
                                method_ty: meth.ty.clone(),
                                defining_module: mname.clone(),
                            },
                        );
                    }
                }
                Def::Instance(_) => {
                    // Instances do not contribute globals; coherence
                    // is enforced earlier at
                    // `workspace::build_registry`.
                }
            }
        }
        out.insert(mname.clone(), globals);
    }
    Ok(out)
}

/// Build the workspace-flat `Env` shared by `check_in_workspace`
/// and `mono::build_workspace_env`. Populates every field whose
/// contents are derivable from `Workspace` alone — no
/// `current_module` overlay applied. Both call sites are thin
/// consumers: each clones this env and applies the per-call
/// overlay (`current_module`, `globals` augmented with module fns,
/// `imports`, `rigid_vars`) at the call site.
///
/// Pre-condition: typecheck has succeeded for the workspace
/// (otherwise `build_module_globals` panics — same caller-contract
/// as the pre-refactor `mono::build_workspace_env`).
pub fn build_check_env(ws: &Workspace) -> Env {
    let mut env = Env::default();
    builtins::install(&mut env);

    // env.types + env.ctor_index — workspace-flat from every
    // module's Def::Type. Safe to flatten because `check_workspace`
    // has already accepted the workspace, so duplicate names cannot
    // occur. Mirrors the per-module loop in the pre-refactor
    // `check_in_workspace` (which fail-fast aborted on duplicates,
    // unreachable here).
    for m in ws.modules.values() {
        for d in &m.defs {
            if let Def::Type(td) = d {
                for c in &td.ctors {
                    env.ctor_index.insert(
                        c.name.clone(),
                        CtorRef { type_name: td.name.clone() },
                    );
                }
                env.types.insert(td.name.clone(), td.clone());
            }
        }
    }

    // env.module_globals + env.class_methods — built from
    // `build_module_globals(ws)`. The .fns projection feeds
    // `module_globals`; the .class_methods entries are merged
    // workspace-wide into `class_methods` (uniqueness enforced
    // earlier by `workspace::build_registry`'s
    // method-name-collision check).
    let mg = build_module_globals(ws)
        .expect("build_module_globals: pre-condition (typecheck succeeded) violated");
    env.module_globals = mg
        .iter()
        .map(|(k, v)| (k.clone(), v.fns.clone()))
        .collect();
    for g in mg.values() {
        for (n, e) in &g.class_methods {
            env.class_methods.insert(n.clone(), e.clone());
        }
    }

    // env.module_types — per-module ADT index.
    env.module_types = build_module_types(ws);

    // env.module_imports — per-module alias-or-name -> module-name.
    // Per-module because aliases collide across modules; sibling
    // shape to `module_globals`.
    for m in ws.modules.values() {
        let mut import_map: BTreeMap<String, String> = BTreeMap::new();
        for imp in &m.imports {
            let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
            import_map.insert(key, imp.module.clone());
        }
        // Iter 23.1: the prelude module is implicitly imported into
        // every non-prelude module. A user-declared explicit
        // `import { module: "prelude" }` would already place
        // "prelude" in the map above (idempotent insert via entry).
        // The prelude module itself does not import itself.
        if m.name != "prelude" {
            import_map
                .entry("prelude".to_string())
                .or_insert_with(|| "prelude".to_string());
        }
        env.module_imports.insert(m.name.clone(), import_map);
    }

    // env.class_superclasses — walk every module's Def::Class.
    for m in ws.modules.values() {
        for d in &m.defs {
            if let Def::Class(cd) = d {
                if let Some(sc) = &cd.superclass {
                    env.class_superclasses.insert(cd.name.clone(), sc.class.clone());
                }
            }
        }
    }

    // env.workspace_registry — clone of ws.registry. Used by
    // `check_fn`'s concrete-residual no-instance check.
    env.workspace_registry = ws.registry.clone();

    env
}

/// Checks the bodies of a single module in the context of the workspace.
/// Assumption: `module_globals` already contains the top-level symbol
/// tables for **all** modules of the workspace (including `m`) — built
/// by `build_module_globals`.
///
/// Returns **all** errors found in this module, in def declaration order:
///
/// - The type-def setup phase is fail-fast within the module (duplicate
///   type or ctor names corrupt the env, so we abort *this* module after
///   the first such error and let the outer loop continue with others).
/// - The body-check phase is multi-diagnose: each def is checked
///   independently against the assembled env; a failure is recorded and
///   the next def is attempted.
fn check_in_workspace(
    m: &Module,
    ws: &Workspace,
    module_globals: &BTreeMap<String, ModuleGlobals>,
) -> Vec<CheckError> {
    let mut env = build_check_env(ws);
    let mut errors: Vec<CheckError> = Vec::new();

    // Per-module overlay for `env.types` / `env.ctor_index`:
    // `build_check_env` populates these workspace-flat, but the
    // per-module pass needs only THIS module's local entries.
    // Clear and rebuild so that:
    //   - duplicate-type / duplicate-ctor detection (the in-band
    //     errors below) sees only this module's defs;
    //   - bare-name lookups (e.g. local `Term::Ctor` synth)
    //     resolve against this module's types, not against the
    //     workspace-flat union.
    // Cross-module `Pattern::Ctor` resolution no longer touches
    // this overlay — that path is type-driven via `expected` and
    // consults `env.module_types` directly (ct.2.2).
    env.types.clear();
    env.ctor_index.clear();
    for def in &m.defs {
        if let Def::Type(td) = def {
            if env.types.contains_key(&td.name) {
                errors.push(CheckError::Def(
                    td.name.clone(),
                    Box::new(CheckError::DuplicateType(td.name.clone())),
                ));
                return errors;
            }
            for c in &td.ctors {
                if let Some(prev) = env.ctor_index.get(&c.name) {
                    errors.push(CheckError::Def(
                        td.name.clone(),
                        Box::new(CheckError::DuplicateCtor {
                            ctor: c.name.clone(),
                            a: prev.type_name.clone(),
                            b: td.name.clone(),
                        }),
                    ));
                    return errors;
                }
                env.ctor_index.insert(
                    c.name.clone(),
                    CtorRef { type_name: td.name.clone() },
                );
            }
            env.types.insert(td.name.clone(), td.clone());
        }
    }

    if let Some(g) = module_globals.get(&m.name) {
        for (n, t) in &g.fns {
            env.globals.insert(n.clone(), t.clone());
        }
    }

    let mut import_map: BTreeMap<String, String> = BTreeMap::new();
    for imp in &m.imports {
        let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
        import_map.insert(key, imp.module.clone());
    }
    // Iter 23.1: the prelude module is implicitly imported into
    // every non-prelude module's body-check env. The wiring here
    // populates `env.imports` (the active per-module table the
    // body-check pass reads); the sibling block in `build_check_env`
    // populates `env.module_imports` (the workspace-wide table
    // referenced when resolving qualified names across modules).
    // Both fields need the prelude-injection rule applied, and they
    // are populated from different code paths — hence the apparent
    // duplication. The prelude itself does not import itself.
    if m.name != "prelude" {
        import_map
            .entry("prelude".to_string())
            .or_insert_with(|| "prelude".to_string());
    }
    env.imports = import_map;
    env.current_module = m.name.clone();

    for def in &m.defs {
        if let Err(e) = check_def(def, &env) {
            errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
        }
    }
    errors
}

fn check_def(def: &Def, env: &Env) -> Result<()> {
    match def {
        Def::Fn(f) => check_fn(f, env),
        Def::Const(c) => check_const(c, env),
        Def::Type(td) => check_type_def(td, env),
        // Iter 22b.1: schema-only landing for class/instance defs.
        // Class-schema validation (KindMismatch, InvalidSuperclassParam,
        // ConstraintReferencesUnboundTypeVar) and instance-body
        // typechecking (with class-method substitution) land in 22b.2.
        // Workspace-load coherence checks (Orphan / Duplicate /
        // MissingMethod) already fire from `workspace::build_registry`,
        // so a malformed instance never reaches this point.
        Def::Class(_) | Def::Instance(_) => Ok(()),
    }
}

fn check_type_def(td: &TypeDef, env: &Env) -> Result<()> {
    // Iter 13a: a parameterised ADT (`vars` non-empty) installs its
    // type parameters as rigid vars while checking the ctor field
    // types, so `List a = ... | Cons(a, List a)` resolves both
    // occurrences of `a` and the recursive use of `List a` correctly.
    let mut env = env.clone();
    for v in &td.vars {
        env.rigid_vars.insert(v.clone());
    }
    for c in &td.ctors {
        for f in &c.fields {
            check_type_well_formed(f, &env)?;
        }
    }
    Ok(())
}

fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
    match t {
        Type::Con { name, args } => {
            let is_primitive = ailang_core::primitives::is_primitive_name(name);
            if is_primitive {
                if !args.is_empty() {
                    return Err(CheckError::UnknownType(format!(
                        "{name} (primitive does not take type args)"
                    )));
                }
                return Ok(());
            }
            // Iter 15a: a qualified type name `module.Type` resolves
            // through the import map and the per-module type table. The
            // bare-name path is unchanged.
            let td_opt: Option<&TypeDef> = if name.matches('.').count() == 1 {
                let (prefix, suffix) = name.split_once('.').expect("checked");
                let target_module = match env.imports.get(prefix) {
                    Some(m) => m.as_str(),
                    None => {
                        return Err(CheckError::UnknownModule {
                            module: prefix.to_string(),
                        });
                    }
                };
                env.module_types
                    .get(target_module)
                    .and_then(|tys| tys.get(suffix))
            } else {
                env.types.get(name)
            };
            if let Some(td) = td_opt {
                if td.vars.len() != args.len() {
                    return Err(CheckError::UnknownType(format!(
                        "{name} expects {} type arg(s), got {}",
                        td.vars.len(),
                        args.len()
                    )));
                }
                for a in args {
                    check_type_well_formed(a, env)?;
                }
                Ok(())
            } else {
                Err(CheckError::UnknownType(name.clone()))
            }
        }
        Type::Fn { params, ret, .. } => {
            for p in params {
                check_type_well_formed(p, env)?;
            }
            check_type_well_formed(ret, env)
        }
        Type::Var { name } => {
            // Rigid var: legal iff it is in scope. Used inside a forall
            // body when checking a polymorphic def, or inside a
            // parameterised ADT's ctor fields.
            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<()> {
    // 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, constraints: _, 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())
        }
        other => {
            return Err(CheckError::FnTypeRequired(
                f.name.clone(),
                ailang_core::pretty::type_to_string(other),
            ));
        }
    };

    if f.params.len() != param_tys.len() {
        return Err(CheckError::ParamCountMismatch {
            name: f.name.clone(),
            ty_count: param_tys.len(),
            param_count: f.params.len(),
        });
    }

    // 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());
    }

    // Iter 13a: validate the declared parameter and return types
    // against the type environment. Catches misuses like
    // `Box<Int, Bool>` (arity mismatch on a parameterised ADT) before
    // they leak into the body and produce confusing downstream errors.
    for p in &param_tys {
        check_type_well_formed(p, &env)?;
    }
    check_type_well_formed(&ret_ty, &env)?;

    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 mut subst = Subst::default();
    let mut counter: u32 = 0;
    // Per-fn residual class constraints. Every call to a class method
    // inside the body pushes a [`ResidualConstraint`] here; after the
    // body finishes, we compare against the expanded declared set.
    let mut residuals: Vec<ResidualConstraint> = Vec::new();
    let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
    unify(&ret_ty, &body_ty, &mut subst)?;

    // Iter 14e: tail-position verification (Decision 8). Runs after
    // the main type-check so that a tail-call marker on a malformed
    // call doesn't drown out the underlying type error.
    verify_tail_positions(&f.body, true)?;

    let declared: BTreeSet<String> = declared_effs.into_iter().collect();
    for e in &effects {
        if !declared.contains(e) {
            return Err(CheckError::UndeclaredEffect(e.clone()));
        }
    }

    // Iter 22b.2 (Task 9): missing-constraint check. Build the expanded
    // declared-constraint set (declared + one-step superclass per
    // Decision 11) and compare against residuals. Var-shaped residuals
    // not covered by the expanded set fire `MissingConstraint`. Concrete
    // residuals are deferred to Task 10's `no-instance` arm.
    let declared_constraints: Vec<Constraint> = match &f.ty {
        Type::Forall { constraints, .. } => constraints.clone(),
        _ => Vec::new(),
    };
    let expanded = expand_declared_constraints(&declared_constraints, &env.class_superclasses);
    for r in &residuals {
        let r_ty = subst.apply(&r.type_);
        if let Type::Var { name } = &r_ty {
            // Skip residuals over metavars (`$mN`) — those mean the
            // residual is over a value the body never connected to a
            // rigid var; treat as concrete-uncovered, which Task 10
            // will handle. Only rigid (source-level) vars participate
            // in the missing-constraint check here.
            if Subst::meta_id(name).is_some() {
                continue;
            }
            let satisfied = expanded
                .iter()
                .any(|d| d.class == r.class && constraint_type_matches(&d.type_, &r_ty));
            if !satisfied {
                return Err(CheckError::MissingConstraint {
                    def: f.name.clone(),
                    method: r.method.clone(),
                    class: r.class.clone(),
                    at_type: name.clone(),
                });
            }
        } else if is_fully_concrete(&r_ty) {
            // Iter 22b.2 (Task 10): fully-concrete residual — the class
            // method was called at a concrete type, so the obligation
            // can only be discharged by an existing workspace instance.
            // Look up `(class, type_hash(r_ty))` in the registry; absence
            // → no-instance. The hash uses `canonical::type_hash`, the
            // same key shape `workspace::build_registry` writes with, so
            // representation-equal types match deterministically.
            // normalize to match Registry::normalize_type_for_lookup contract
            let r_ty_norm = env.workspace_registry.normalize_type_for_lookup(&r_ty);
            let key = (
                r.class.clone(),
                ailang_core::canonical::type_hash(&r_ty_norm),
            );
            if !env.workspace_registry.entries.contains_key(&key) {
                return Err(CheckError::NoInstance {
                    def: f.name.clone(),
                    method: r.method.clone(),
                    class: r.class.clone(),
                    at_type: ailang_core::pretty::type_to_string(&r_ty),
                });
            }
        }
        // Other shapes (unsolved metavars inside a `Type::Con`,
        // `Type::Fn`, `Type::Forall`) are out of scope for the 22b.2
        // diagnostics: metavars mean the body never connected the
        // class param to anything observable, and `Fn`/`Forall` cannot
        // appear as instance heads (Decision 11).
    }
    Ok(())
}

/// Iter 22b.2 (Task 10): true iff the type tree contains no `Type::Var`
/// at any depth. A fully-concrete type is the only shape eligible for
/// the no-instance lookup — anything carrying a metavar / rigid-var
/// component is either covered by the missing-constraint check or
/// genuinely under-specified at the call site.
pub(crate) fn is_fully_concrete(t: &Type) -> bool {
    match t {
        Type::Con { args, .. } => args.iter().all(is_fully_concrete),
        Type::Var { .. } => false,
        Type::Fn { params, ret, .. } => {
            params.iter().all(is_fully_concrete) && is_fully_concrete(ret)
        }
        Type::Forall { body, .. } => is_fully_concrete(body),
    }
}

/// Iter 22b.2 (Task 9): per-call-site residual class constraint
/// recorded by [`synth`] when a `Term::Var` resolves to a class method.
/// Carries the method name (for diagnostic rendering), the class, and
/// the type the class is applied to at the call site. The type is
/// typically a fresh metavar (which unification then ties to the
/// argument's actual type) or, after `subst.apply`, a rigid var or a
/// concrete `Type::Con`.
#[derive(Debug, Clone)]
pub(crate) struct ResidualConstraint {
    /// Class name (e.g. `Show`).
    pub class: String,
    /// Class param's instance at this call site. Pre-substitution: the
    /// fresh metavar inserted at the Var site. Post-substitution: the
    /// solved type — rigid var, concrete con, or unsolved metavar.
    pub type_: Type,
    /// Method name (e.g. `show`); used by the missing-constraint
    /// diagnostic to point the author at which call site triggered
    /// the residual.
    pub method: String,
}

/// Iter 23.4: per-call-site polymorphic-free-fn observation recorded by
/// [`synth`] when a `Term::Var` resolves to a `Type::Forall`-quantified
/// top-level def (NOT a class method — those are pushed to
/// [`ResidualConstraint`] instead). Carries the bare name, the owning
/// module (resolved through the same lookup ladder as `synth`'s Var arm),
/// the polymorphic source's `Forall.vars` (declaration order), and the
/// fresh metavars instantiated for those vars at the call site.
///
/// Consumed by the mono pass: after `synth` completes a body, each
/// `metas[i]` is `subst.apply`'d to recover the concrete type at vars[i].
/// Fully-concrete observations become [`crate::mono::MonoTarget::FreeFn`]
/// targets; non-concrete observations are silently dropped (covered by
/// the missing-constraint check on residuals if relevant).
#[derive(Debug, Clone)]
pub struct FreeFnCall {
    /// Bare name of the polymorphic def at the call site.
    pub name: String,
    /// Module in which the polymorphic `Def::Fn` is declared, resolved
    /// through `synth`'s lookup ladder (current module's globals,
    /// implicitly-imported module's globals, or the dot-qualified
    /// `prefix.name` path's target module).
    pub owner_module: String,
    /// The `Forall.vars` of the source def (declaration order).
    pub forall_vars: Vec<String>,
    /// Fresh metavars instantiated at this call site — same length as
    /// `forall_vars`, same order. Post-`synth`, `subst.apply(&metas[i])`
    /// yields the concrete type for `forall_vars[i]` iff the call site's
    /// substitution was fully pinned.
    pub metas: Vec<Type>,
}

/// Iter 22b.2 (Task 9): expand a list of declared class constraints
/// with their one-step superclass closure (Decision 11). For every
/// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
/// `S`. Only one step — Decision 11 forbids deeper chains. The
/// expanded list is what [`check_fn`] uses to decide whether a
/// residual is satisfied.
fn expand_declared_constraints(
    declared: &[Constraint],
    class_superclasses: &BTreeMap<String, String>,
) -> Vec<Constraint> {
    let mut out: Vec<Constraint> = declared.to_vec();
    for c in declared {
        if let Some(sc) = class_superclasses.get(&c.class) {
            out.push(Constraint {
                class: sc.clone(),
                type_: c.type_.clone(),
            });
        }
    }
    out
}

/// Iter 22b.2 (Task 9): equality of constraint types for the
/// missing-constraint match. The residual type has been
/// `subst.apply`-d, so two rigid vars match iff their names are equal;
/// a `Type::Con` matches another `Type::Con` iff their head names and
/// args agree. Conservative: anything outside `Var` / `Con` is rejected
/// (the schema bounds Constraint.type_ to plain types, and Task 9 only
/// fires on Var residuals anyway).
fn constraint_type_matches(declared: &Type, residual: &Type) -> bool {
    match (declared, residual) {
        (Type::Var { name: a }, Type::Var { name: b }) => a == b,
        (Type::Con { name: a, args: aa }, Type::Con { name: b, args: ba }) => {
            a == b
                && aa.len() == ba.len()
                && aa.iter().zip(ba.iter()).all(|(x, y)| constraint_type_matches(x, y))
        }
        _ => false,
    }
}

/// Iter 14e: verifies that every `Term::App { tail: true, .. }` and
/// `Term::Do { tail: true, .. }` actually sits in tail position, per
/// Decision 8.
///
/// `is_tail` is the tail-context flag for the term currently being
/// visited. The propagation rules (from DESIGN.md Decision 8):
///
/// - The body of a fn / Lam is visited with `is_tail = true`.
/// - `Match { scrutinee, arms }`: the scrutinee is **not** in tail
///   position; each arm body inherits the same `is_tail` as the match.
/// - `Seq { lhs, rhs }`: lhs is non-tail; rhs inherits.
/// - `Let { value, body, .. }`: value is non-tail; body inherits.
/// - `App { callee, args, tail }`: the callee and all args are
///   non-tail. If `tail == true`, the App itself must have arrived
///   with `is_tail == true`; otherwise diagnostic.
/// - `Do { args, tail }`: same rule as App; all args are non-tail.
/// - `Ctor { args }`: all args are non-tail.
/// - `Lam { body }`: the Lam value is at whatever `is_tail` was; the
///   recursion **into** the body opens a fresh tail scope (the body
///   is visited with `is_tail = true`).
/// - `Lit`, `Var`: leaves; no further descent.
pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
    match t {
        Term::Lit { .. } | Term::Var { .. } => Ok(()),
        Term::App { callee, args, tail } => {
            if *tail && !is_tail {
                return Err(CheckError::TailCallNotInTailPosition);
            }
            verify_tail_positions(callee, false)?;
            for a in args {
                verify_tail_positions(a, false)?;
            }
            Ok(())
        }
        Term::Do { args, tail, .. } => {
            if *tail && !is_tail {
                return Err(CheckError::TailCallNotInTailPosition);
            }
            for a in args {
                verify_tail_positions(a, false)?;
            }
            Ok(())
        }
        Term::Let { value, body, .. } => {
            verify_tail_positions(value, false)?;
            verify_tail_positions(body, is_tail)
        }
        Term::If { cond, then, else_ } => {
            verify_tail_positions(cond, false)?;
            verify_tail_positions(then, is_tail)?;
            verify_tail_positions(else_, is_tail)
        }
        Term::Seq { lhs, rhs } => {
            verify_tail_positions(lhs, false)?;
            verify_tail_positions(rhs, is_tail)
        }
        Term::Match { scrutinee, arms } => {
            verify_tail_positions(scrutinee, false)?;
            for arm in arms {
                verify_tail_positions(&arm.body, is_tail)?;
            }
            Ok(())
        }
        Term::Ctor { args, .. } => {
            for a in args {
                verify_tail_positions(a, false)?;
            }
            Ok(())
        }
        Term::Lam { body, .. } => {
            // Entering a Lam body opens a fresh tail scope.
            verify_tail_positions(body, true)
        }
        Term::LetRec { body, in_term, .. } => {
            // Iter 16b.3: `Term::LetRec` may now survive the desugar
            // pass (when it captures `Term::Let`-bound names whose
            // types are only known after typecheck). The body is the
            // body of a fn-typed binding; the recursive name is what
            // gets tail-called, so `body` is NOT in tail position. The
            // in-clause IS in tail position iff the enclosing context
            // is — same propagation rule as `Term::Let.body`.
            verify_tail_positions(body, false)?;
            verify_tail_positions(in_term, is_tail)
        }
        Term::Clone { value } => {
            // Iter 18c.1: clone is identity. Tail-position propagates
            // through unchanged — `(clone tail-call)` is a tail call.
            verify_tail_positions(value, is_tail)
        }
        Term::ReuseAs { source, body } => {
            // Iter 18d.1: reuse-as is identity at codegen. The `source`
            // is a side-effect-free Var in shipping fixtures, so it is
            // not a tail call; the `body` is the value of the whole
            // expression and inherits the enclosing tail position.
            verify_tail_positions(source, false)?;
            verify_tail_positions(body, is_tail)
        }
    }
}

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 mut subst = Subst::default();
    let mut counter: u32 = 0;
    // Iter 22b.2 (Task 9): const bodies don't carry a `Forall.constraints`
    // (rejected upstream), so any residual would have to be concrete —
    // Task 10's no-instance arm will pick those up. We thread an
    // accumulator only to keep `synth`'s signature uniform.
    let mut residuals: Vec<ResidualConstraint> = Vec::new();
    let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
    unify(&c.ty, &v, &mut subst)?;
    if !effects.is_empty() {
        return Err(CheckError::ConstHasEffects(
            c.name.clone(),
            effects.into_iter().collect(),
        ));
    }
    Ok(())
}

pub(crate) fn synth(
    t: &Term,
    env: &Env,
    locals: &mut IndexMap<String, Type>,
    effects: &mut BTreeSet<String>,
    in_def: &str,
    subst: &mut Subst,
    counter: &mut u32,
    residuals: &mut Vec<ResidualConstraint>,
    free_fn_calls: &mut Vec<FreeFnCall>,
) -> Result<Type> {
    match t {
        Term::Lit { lit } => Ok(match lit {
            Literal::Int { .. } => Type::int(),
            Literal::Bool { .. } => Type::bool_(),
            Literal::Str { .. } => Type::str_(),
            Literal::Unit => Type::unit(),
            Literal::Float { .. } => Type::float(),
        }),
        Term::Var { name } => {
            // Lookup precedence: locals → local globals → class-method
            // table → 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.
            //
            // Iter 22b.2 (Task 9): the class-method channel sits between
            // local globals and qualified cross-module ref. When a name
            // resolves through `env.class_methods`, we substitute the
            // class param with a fresh metavar and record a residual
            // class constraint — `check_fn` later compares the residual
            // set against the declared `Forall.constraints`.
            // Iter 23.4: alongside the bare type, capture
            //   (owner_module, unqualified_name_in_owner_module)
            // for any non-local resolution that lands on a
            // `Type::Forall` AND is a real workspace-declared
            // `Def::Fn` (NOT a builtin operator like `==`). The
            // discriminator is whether the name appears in
            // `env.module_globals[<owner>]` — builtins are installed
            // into `env.globals` only. The unqualified-name capture
            // matters for dot-qualified call sites: the FreeFnCall
            // records the suffix (e.g. `length`), not the full
            // `std_list.length`, so `synthesise_mono_fn_for_free_fn`
            // can look up the source def by its bare name in the
            // owner module's def list.
            //
            // After the resolution ladder, if `raw` is a `Type::Forall`
            // AND a `free_fn_owner` is known, push a `FreeFnCall`
            // observation; the mono pass `subst.apply`s the metas
            // post-synth to recover concrete type-args at each
            // polymorphic free-fn call site.
            let (raw, free_fn_owner): (Type, Option<(String, String)>) = if let Some(t) = locals.get(name) {
                (t.clone(), None)
            } else if let Some(t) = env.globals.get(name) {
                // Same-module global. Owner is the current module IFF
                // the name is in this module's declared globals
                // (i.e. it's a `Def::Fn`, not a builtin). The bare
                // `name` works as the in-module key.
                let owner = env
                    .module_globals
                    .get(&env.current_module)
                    .filter(|m| m.contains_key(name))
                    .map(|_| (env.current_module.clone(), name.clone()));
                (t.clone(), owner)
            } else if let Some(cm) = env.class_methods.get(name) {
                // Iter 22b.2 (Task 9): instantiate the class param with
                // a fresh metavar; the body's unification at the call
                // site fills it in, and the residual is the class
                // constraint we owe at this use site.
                //
                // ct.2 Task 1: a class method's declared type lives in
                // its defining module's bare-local namespace.
                // qualify_local_types runs symmetrically with the
                // Term::Var qualified path below so the consumer's
                // typecheck context sees the method's return /
                // parameter Type::Cons fully qualified.
                let owner_types = env
                    .module_types
                    .get(&cm.defining_module)
                    .cloned()
                    .unwrap_or_default();
                let qualified_method_ty =
                    qualify_local_types(&cm.method_ty, &cm.defining_module, &owner_types);
                let fresh = Subst::fresh(counter);
                let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
                mapping.insert(cm.class_param.clone(), fresh.clone());
                let inst_ty = substitute_rigids(&qualified_method_ty, &mapping);
                residuals.push(ResidualConstraint {
                    class: cm.class_name.clone(),
                    type_: fresh,
                    method: name.clone(),
                });
                return Ok(inst_ty);
            } else if let Some((owner_module, raw_ty)) = env
                .imports
                .values()
                .find_map(|mod_name| {
                    env.module_globals
                        .get(mod_name)
                        .and_then(|mg| mg.get(name).map(|ty| (mod_name.clone(), ty.clone())))
                })
            {
                // Iter 23.4-prep: bare-name fall-through to free fns of
                // implicitly-imported modules. Today only the prelude is
                // implicitly imported (see `build_check_env` and
                // `check_in_workspace`'s prelude-injection at this file's
                // ~1170 / ~1285), so the first match is unambiguous. If a
                // second implicit import lands, the single-match-wins rule
                // becomes a real ambiguity and this branch needs a
                // duplicate-detection diagnostic.
                //
                // Qualify any bare type-cons referring to a type defined in
                // the owning module — same treatment the dot-qualified arm
                // below applies — so signatures cross the module boundary
                // with fully-qualified Type::Cons.
                let owner_types = env
                    .module_types
                    .get(&owner_module)
                    .cloned()
                    .unwrap_or_default();
                let qualified = qualify_local_types(&raw_ty, &owner_module, &owner_types);
                // Bare name resolves through implicit import; the
                // unqualified name in the owner module is the same `name`.
                (qualified, Some((owner_module, name.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 => {
                        return Err(CheckError::UnknownModule {
                            module: prefix.to_string(),
                        });
                    }
                };
                let g = env.module_globals.get(&target_module).ok_or_else(|| {
                    CheckError::UnknownModule {
                        module: target_module.clone(),
                    }
                })?;
                let raw_ty = g.get(suffix).cloned().ok_or_else(|| {
                    CheckError::UnknownImport {
                        module: target_module.clone(),
                        name: suffix.to_string(),
                    }
                })?;
                // Iter 15a: qualify any bare type-cons referring to a
                // type defined in the owning module so that signatures
                // pulled across the boundary unify against
                // qualified-form ctors and types in the consumer
                // module.
                let owner_types = env
                    .module_types
                    .get(&target_module)
                    .cloned()
                    .unwrap_or_default();
                let qualified = qualify_local_types(&raw_ty, &target_module, &owner_types);
                // Dot-qualified `prefix.suffix`: the unqualified name in
                // the owner module is `suffix`.
                (qualified, Some((target_module, suffix.to_string())))
            } else {
                return Err(CheckError::UnknownIdent(name.clone()));
            };
            // Iter 23.4: if raw is `Type::Forall` AND we know the
            // owner module (i.e. the resolution went through a non-
            // local branch), record a FreeFnCall observation BEFORE
            // instantiating. The metas are the fresh metavars we
            // about to use; the mono pass `subst.apply`s them later.
            // Note: `unqualified_name` is the name as seen inside the
            // owner module (so the mono pass can find the `Def::Fn`
            // by bare name); the source-level `name` may be a
            // dot-qualified form (`prefix.suffix`) the synth started
            // with.
            if let (Type::Forall { vars, constraints: _, body }, Some((owner, unqualified_name))) =
                (&raw, &free_fn_owner)
            {
                let (metas, inst) = instantiate(vars, body, counter);
                free_fn_calls.push(FreeFnCall {
                    name: unqualified_name.clone(),
                    owner_module: owner.clone(),
                    forall_vars: vars.clone(),
                    metas: metas.clone(),
                });
                return Ok(inst);
            }
            Ok(maybe_instantiate(raw, counter))
        }
        Term::App { callee, args, .. } => {
            let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            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 { vars, constraints: _, 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(
                        callee_name(callee),
                        ailang_core::pretty::type_to_string(other),
                    ));
                }
            };
            if args.len() != params.len() {
                return Err(CheckError::ArityMismatch {
                    name: callee_name(callee),
                    expected: params.len(),
                    got: args.len(),
                });
            }
            for (a, exp) in args.iter().zip(params.iter()) {
                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                unify(exp, &actual, subst)?;
            }
            for e in fx {
                effects.insert(e);
            }
            Ok(subst.apply(&ret))
        }
        Term::Let { name, value, body } => {
            let v = synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            let prev = locals.insert(name.clone(), v);
            let r = synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            match prev {
                Some(p) => {
                    locals.insert(name.clone(), p);
                }
                None => {
                    locals.shift_remove(name);
                }
            }
            Ok(r)
        }
        Term::If { cond, then, else_ } => {
            let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            unify(&Type::bool_(), &c, subst)?;
            let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            unify(&t1, &t2, subst)?;
            Ok(subst.apply(&t1))
        }
        Term::Do { op, args, .. } => {
            let sig = env
                .effect_ops
                .get(op)
                .ok_or_else(|| CheckError::UnknownEffectOp(op.clone()))?
                .clone();
            if args.len() != sig.params.len() {
                return Err(CheckError::ArityMismatch {
                    name: op.clone(),
                    expected: sig.params.len(),
                    got: args.len(),
                });
            }
            for (a, exp) in args.iter().zip(sig.params.iter()) {
                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                unify(exp, &actual, subst)?;
            }
            effects.insert(sig.effect.clone());
            Ok(sig.ret)
        }
        Term::Ctor { type_name, ctor, args } => {
            // ct.2 Task 3: Term::Ctor lookup is direct post-ct.1.
            // Canonical type_name: bare = local TypeDef, qualified =
            // explicit cross-module. The imports-fallback (iter
            // 23.1.3) is gone — bare cross-module refs are rejected
            // upstream by the workspace validator (ct.1).
            //
            // Iter 15b: when the type is cross-module, `cdef.fields` is
            // written in the owning module's local namespace. A recursive
            // self-reference like `Cons a (List a)` carries `Con
            // { name: "List" }` even though, from the consumer's view,
            // the type is `std_list.List`. Apply `qualify_local_types`
            // with the owning module so that recursive ctor field types
            // (and any other locally-named cross-module type-cons) are
            // qualified before substitution / unification.
            let owning_module: Option<String>;
            let result_type_name: String = type_name.clone();
            let td = if type_name.matches('.').count() == 1 {
                let (prefix, suffix) = type_name.split_once('.').expect("checked");
                let target_module = match env.imports.get(prefix) {
                    Some(m) => m.clone(),
                    None => {
                        return Err(CheckError::UnknownModule {
                            module: prefix.to_string(),
                        });
                    }
                };
                let td = env.module_types
                    .get(&target_module)
                    .and_then(|tys| tys.get(suffix))
                    .cloned()
                    .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
                owning_module = Some(target_module);
                td
            } else if let Some(td) = env.types.get(type_name) {
                owning_module = None;
                td.clone()
            } else {
                return Err(CheckError::UnknownType(type_name.clone()));
            };
            let cdef = td
                .ctors
                .iter()
                .find(|c| &c.name == ctor)
                .ok_or_else(|| CheckError::UnknownCtor {
                    ty: type_name.clone(),
                    ctor: ctor.clone(),
                })?
                .clone();
            if args.len() != cdef.fields.len() {
                return Err(CheckError::CtorArity {
                    ty: type_name.clone(),
                    ctor: ctor.clone(),
                    expected: cdef.fields.len(),
                    got: args.len(),
                });
            }
            // Iter 15b: qualify local type-cons in the field types when
            // the ctor's owning type is cross-module. No-op when the
            // type is local (owning_module is None).
            let qualified_fields: Vec<Type> = match &owning_module {
                Some(m) => {
                    let owner_types = env
                        .module_types
                        .get(m)
                        .cloned()
                        .unwrap_or_default();
                    cdef.fields
                        .iter()
                        .map(|f| qualify_local_types(f, m, &owner_types))
                        .collect()
                }
                None => cdef.fields.clone(),
            };
            // Iter 13a: parameterised ADT — instantiate the type's vars
            // with fresh metavars, substitute them through every ctor
            // field type, and let the field types' metavars be solved by
            // unifying against the actual arg types. The result type
            // carries the same metavars as type-args, so the surrounding
            // context can pin them down.
            let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
            let mut type_args: Vec<Type> = Vec::with_capacity(td.vars.len());
            for v in &td.vars {
                let m = Subst::fresh(counter);
                mapping.insert(v.clone(), m.clone());
                type_args.push(m);
            }
            for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                let exp_inst = substitute_rigids(exp, &mapping);
                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
                unify(&exp_inst, &actual, subst)?;
            }
            Ok(Type::Con {
                name: result_type_name,
                args: type_args,
            })
        }
        Term::Match { scrutinee, arms } => {
            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            if arms.is_empty() {
                return Err(CheckError::NonExhaustive {
                    ty: ailang_core::pretty::type_to_string(&s_ty),
                    missing: vec!["(no arms)".into()],
                });
            }
            let mut covered_ctors: BTreeSet<String> = BTreeSet::new();
            let mut has_open_arm = false;
            let mut result_ty: Option<Type> = None;

            for arm in arms {
                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, subst, counter, residuals, free_fn_calls)?;
                for (n, prev) in pushed.into_iter().rev() {
                    match prev {
                        Some(p) => {
                            locals.insert(n, p);
                        }
                        None => {
                            locals.shift_remove(&n);
                        }
                    }
                }

                if let Some(rt) = &result_ty {
                    unify(rt, &body_ty, subst)?;
                } else {
                    result_ty = Some(body_ty);
                }

                match &arm.pat {
                    Pattern::Wild | Pattern::Var { .. } => {
                        has_open_arm = true;
                    }
                    Pattern::Ctor { ctor, .. } => {
                        covered_ctors.insert(ctor.clone());
                    }
                    Pattern::Lit { .. } => {
                        // Lit patterns don't structurally cover anything.
                    }
                }
            }

            if !has_open_arm {
                // Iter 15a: a qualified scrutinee type (`module.Type`,
                // produced by a cross-module ctor) resolves through
                // `env.module_types`; bare names use `env.types` as
                // before.
                let td_opt: Option<&TypeDef> = match &s_ty {
                    Type::Con { name, .. } => {
                        if name.matches('.').count() == 1 {
                            let (prefix, suffix) = name.split_once('.').expect("checked");
                            env.module_types
                                .get(prefix)
                                .and_then(|tys| tys.get(suffix))
                        } else {
                            env.types.get(name)
                        }
                    }
                    _ => None,
                };
                match (td_opt, &s_ty) {
                    (Some(td), Type::Con { name, .. }) => {
                        let missing: Vec<String> = td
                            .ctors
                            .iter()
                            .filter(|c| !covered_ctors.contains(&c.name))
                            .map(|c| c.name.clone())
                            .collect();
                        if !missing.is_empty() {
                            return Err(CheckError::NonExhaustive {
                                ty: name.clone(),
                                missing,
                            });
                        }
                    }
                    _ => {
                        return Err(CheckError::PrimitiveNeedsWildcard(
                            ailang_core::pretty::type_to_string(&s_ty),
                        ));
                    }
                }
            }

            Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
        }
        Term::Seq { lhs, rhs } => {
            let lty = synth(lhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            unify(&Type::unit(), &lty, subst)?;
            synth(rhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
        }
        Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
            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, subst, counter, residuals, free_fn_calls);
            for (n, prev) in pushed.into_iter().rev() {
                match prev {
                    Some(p) => {
                        locals.insert(n, p);
                    }
                    None => {
                        locals.shift_remove(&n);
                    }
                }
            }
            let body_ty = body_ty?;
            unify(ret_ty, &body_ty, subst)?;
            let declared: BTreeSet<String> = lam_effects.iter().cloned().collect();
            for e in &body_effects {
                if !declared.contains(e) {
                    return Err(CheckError::UndeclaredEffect(e.clone()));
                }
            }
            Ok(Type::Fn {
                params: param_tys.clone(),
                ret: Box::new((**ret_ty).clone()),
                effects: lam_effects.clone(),
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            })
        }
        Term::LetRec { name, ty, params, body, in_term } => {
            // Iter 16b.3: a `Term::LetRec` reaches `synth` only when
            // the desugar pass deferred it (some capture is
            // `Term::Let`-bound and its type is only knowable here).
            // We synthesize it as if it were a recursive fn-typed
            // local binding:
            //   1. Peel any `Forall` defensively (16b.6 still rejects
            //      Forall-typed LetRecs at desugar — this is just for
            //      shape uniformity with `check_fn`).
            //   2. Validate that `params.len() == ty.params.len()`.
            //   3. Extend `locals` with `name: ty` for the body
            //      (recursive self-reference) and each
            //      `params[i]: ty.params[i]`.
            //   4. Synth the body, unify against `ty.ret`, check
            //      effects-subset against `ty.effects`.
            //   5. Restore locals; extend with `name: ty`; synth
            //      `in_term`. Restore. Return `in_term`'s type.
            let inner_ty = match ty {
                Type::Forall { body, .. } => (**body).clone(),
                other => other.clone(),
            };
            let (param_tys, ret_ty, declared_effs) = match &inner_ty {
                Type::Fn { params: ps, ret, effects, .. } => {
                    (ps.clone(), (**ret).clone(), effects.clone())
                }
                other => {
                    return Err(CheckError::FnTypeRequired(
                        name.clone(),
                        ailang_core::pretty::type_to_string(other),
                    ));
                }
            };
            if param_tys.len() != params.len() {
                return Err(CheckError::ParamCountMismatch {
                    name: name.clone(),
                    ty_count: param_tys.len(),
                    param_count: params.len(),
                });
            }

            // Validate the LetRec's declared param/ret types against
            // the type env (catches malformed types like ADT arity
            // mismatches before they leak into the body).
            for p in &param_tys {
                check_type_well_formed(p, env)?;
            }
            check_type_well_formed(&ret_ty, env)?;

            // Save and extend locals: name + params for the body's scope.
            let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
            let prev_name = locals.insert(name.clone(), ty.clone());
            pushed.push((name.clone(), prev_name));
            for (n, t) in params.iter().zip(param_tys.iter()) {
                let prev = locals.insert(n.clone(), t.clone());
                pushed.push((n.clone(), prev));
            }

            // Body effects are tracked separately so we can check the
            // subset rule against `declared_effs` — exactly like
            // `Term::Lam`.
            let mut body_effects: BTreeSet<String> = BTreeSet::new();
            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls);

            // Restore body-scope locals (params + name).
            for (n, prev) in pushed.into_iter().rev() {
                match prev {
                    Some(p) => {
                        locals.insert(n, p);
                    }
                    None => {
                        locals.shift_remove(&n);
                    }
                }
            }
            let body_ty = body_ty?;
            unify(&ret_ty, &body_ty, subst)?;

            let declared: BTreeSet<String> = declared_effs.into_iter().collect();
            for e in &body_effects {
                if !declared.contains(e) {
                    return Err(CheckError::UndeclaredEffect(e.clone()));
                }
            }

            // Now extend locals with `name: ty` for the in-clause's
            // scope (params are not visible here; only the recursive
            // binding is).
            let prev_in = locals.insert(name.clone(), ty.clone());
            let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls);
            match prev_in {
                Some(p) => {
                    locals.insert(name.clone(), p);
                }
                None => {
                    locals.shift_remove(name);
                }
            }
            in_ty
        }
        Term::Clone { value } => {
            // Iter 18c.1: `(clone X)` typechecks identically to `X`.
            // No constraint generated, no environment change. The
            // wrapper records author intent for the future RC inc/dec
            // emission pass (18c.3); typing is pure passthrough.
            synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
        }
        Term::ReuseAs { source, body } => {
            // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to
            // be an allocating term — `Term::Ctor` or `Term::Lam`. Any
            // other shape is a structural error: the wrapper has
            // nothing to rewrite. The `source` term has no body-shape
            // constraint here — linearity (which runs only on
            // all-explicit-mode fns) enforces "source must be a bare
            // Var referring to an in-scope owned binder". Source-type
            // and body-type need not match — that's a future
            // shape-compatibility check (18d.2 will add a
            // `reuse-as-shape-mismatch` diagnostic when codegen has
            // the actual size info).
            let _ = synth(source, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
            match body.as_ref() {
                Term::Ctor { .. } | Term::Lam { .. } => {}
                other => {
                    let tag = match other {
                        Term::Lit { .. } => "lit",
                        Term::Var { .. } => "var",
                        Term::App { .. } => "app",
                        Term::Let { .. } => "let",
                        Term::LetRec { .. } => "let-rec",
                        Term::If { .. } => "if",
                        Term::Do { .. } => "do",
                        Term::Match { .. } => "match",
                        Term::Seq { .. } => "seq",
                        Term::Clone { .. } => "clone",
                        Term::ReuseAs { .. } => "reuse-as",
                        Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                    };
                    return Err(CheckError::ReuseAsNonAllocatingBody {
                        got: tag.to_string(),
                        body_form_a: ailang_surface::print::term_to_form_a(other),
                    });
                }
            }
            // Body's type is the result type of the whole reuse-as
            // expression.
            synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
        }
    }
}

/// 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, constraints: _, body } = &t {
        let (_, inst) = instantiate(vars, body, counter);
        inst
    } else {
        t
    }
}

/// Iter 15a: rewrites bare `Type::Con` references that resolve against
/// `local_types` into qualified `module.Type` form. Used when pulling a
/// fn type across module boundaries: a `Maybe a` declared inside
/// `std_maybe` becomes `std_maybe.Maybe a` when seen from a consumer
/// module — otherwise it would fail to unify with terms whose types
/// the consumer module already qualifies.
///
/// Already-qualified names, primitives (`Int`, `Bool`, `Unit`, `Str`),
/// rigid type vars, and type names that are not in `local_types` pass
/// through unchanged.
fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap<String, TypeDef>) -> Type {
    match t {
        Type::Con { name, args } => {
            let qualified_name = if name.contains('.') {
                name.clone()
            } else if ailang_core::primitives::is_primitive_name(name) {
                name.clone()
            } else if local_types.contains_key(name) {
                format!("{owner_module}.{name}")
            } else {
                name.clone()
            };
            Type::Con {
                name: qualified_name,
                args: args
                    .iter()
                    .map(|a| qualify_local_types(a, owner_module, local_types))
                    .collect(),
            }
        }
        Type::Fn { params, ret, effects, .. } => Type::Fn {
            params: params
                .iter()
                .map(|p| qualify_local_types(p, owner_module, local_types))
                .collect(),
            ret: Box::new(qualify_local_types(ret, owner_module, local_types)),
            effects: effects.clone(),
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        Type::Forall { vars, constraints, body } => Type::Forall {
            vars: vars.clone(),
            constraints: constraints
                .iter()
                .map(|c| Constraint {
                    class: c.class.clone(),
                    type_: qualify_local_types(&c.type_, owner_module, local_types),
                })
                .collect(),
            body: Box::new(qualify_local_types(body, owner_module, local_types)),
        },
        Type::Var { .. } => t.clone(),
    }
}

/// Checks a pattern against an expected type and returns the bindings
/// introduced by the pattern.
fn type_check_pattern(
    p: &Pattern,
    expected: &Type,
    env: &Env,
) -> Result<Vec<(String, Type)>> {
    match p {
        Pattern::Wild => Ok(vec![]),
        Pattern::Var { name } => Ok(vec![(name.clone(), expected.clone())]),
        Pattern::Lit { lit } => {
            let lt = match lit {
                Literal::Int { .. } => Type::int(),
                Literal::Bool { .. } => Type::bool_(),
                Literal::Str { .. } => Type::str_(),
                Literal::Unit => Type::unit(),
                Literal::Float { .. } => {
                    return Err(CheckError::FloatPatternNotAllowed);
                }
            };
            expect_eq(expected, &lt)?;
            Ok(vec![])
        }
        Pattern::Ctor { ctor, fields } => {
            // Iter 16a: nested **Ctor** sub-patterns are removed by
            // `ailang_core::desugar::desugar_module` before this checker
            // runs, so we only have to defend against the still-rejected
            // **Lit** sub-pattern case. The `nested-ctor-pattern-not-allowed`
            // error code is reused for that — its meaning is now narrower
            // ("non-flat: a Lit sub-pattern was found"), and the docstring
            // on the variant reflects that.
            for sub in fields {
                match sub {
                    Pattern::Var { .. } | Pattern::Wild => {}
                    Pattern::Lit { .. } => {
                        return Err(CheckError::NestedCtorPatternNotAllowed(ctor.clone()));
                    }
                    Pattern::Ctor { .. } => {
                        unreachable!(
                            "nested Ctor sub-patterns are removed by \
                             ailang_core::desugar before check"
                        );
                    }
                }
            }
            // ct.2 Task 2: Pattern::Ctor lookup is type-driven post-ct.1.
            // The scrutinee's Type::Con name is canonical (bare = local
            // TypeDef, qualified = explicit cross-module). Derive the
            // TypeDef from `expected` and find the ctor by name within
            // it; no env.ctor_index consult, no imports-walk.
            let (resolved_type_name, resolved_td, resolved_owning_module, scrutinee_args) =
                match expected {
                    Type::Con { name, args } => {
                        if let Some((owner, suffix)) = name.split_once('.') {
                            let td = env
                                .module_types
                                .get(owner)
                                .and_then(|tys| tys.get(suffix))
                                .cloned()
                                .ok_or_else(|| {
                                    CheckError::PatternTypeMismatch {
                                        ctor: ctor.clone(),
                                        ty: ailang_core::pretty::type_to_string(expected),
                                    }
                                })?;
                            (name.clone(), td, Some(owner.to_string()), args.clone())
                        } else {
                            let td = env.types.get(name).cloned().ok_or_else(|| {
                                CheckError::PatternTypeMismatch {
                                    ctor: ctor.clone(),
                                    ty: ailang_core::pretty::type_to_string(expected),
                                }
                            })?;
                            (name.clone(), td, None, args.clone())
                        }
                    }
                    _ => {
                        return Err(CheckError::PatternTypeMismatch {
                            ctor: ctor.clone(),
                            ty: ailang_core::pretty::type_to_string(expected),
                        });
                    }
                };
            let td = &resolved_td;
            let cdef = td
                .ctors
                .iter()
                .find(|c| &c.name == ctor)
                .ok_or_else(|| CheckError::UnknownCtorInPattern(ctor.clone()))?;
            if fields.len() != cdef.fields.len() {
                return Err(CheckError::CtorArity {
                    ty: resolved_type_name.clone(),
                    ctor: ctor.clone(),
                    expected: cdef.fields.len(),
                    got: fields.len(),
                });
            }
            // Iter 13a: substitute the scrutinee's concrete type-args
            // into each cdef field type (e.g. `Cons(a, List a)` checked
            // against a `List Int` scrutinee yields field types
            // `Int, List Int`).
            //
            // Iter 15b: when the resolved ctor lives in an imported
            // module, qualify any bare local type-cons in the field
            // types first — symmetric to the term-ctor fix.
            let qualified_fields: Vec<Type> = match &resolved_owning_module {
                Some(m) => {
                    let owner_types = env
                        .module_types
                        .get(m)
                        .cloned()
                        .unwrap_or_default();
                    cdef.fields
                        .iter()
                        .map(|f| qualify_local_types(f, m, &owner_types))
                        .collect()
                }
                None => cdef.fields.clone(),
            };
            let mapping: BTreeMap<String, Type> = td
                .vars
                .iter()
                .cloned()
                .zip(scrutinee_args)
                .collect();
            let mut out = Vec::new();
            for (sub, sub_ty) in fields.iter().zip(qualified_fields.iter()) {
                let sub_ty_inst = substitute_rigids(sub_ty, &mapping);
                out.extend(type_check_pattern(sub, &sub_ty_inst, env)?);
            }
            Ok(out)
        }
    }
}

fn callee_name(t: &Term) -> String {
    match t {
        Term::Var { name } => name.clone(),
        _ => "<expr>".into(),
    }
}

fn expect_eq(expected: &Type, got: &Type) -> Result<()> {
    if expected == got {
        Ok(())
    } else {
        Err(CheckError::TypeMismatch {
            expected: ailang_core::pretty::type_to_string(expected),
            got: ailang_core::pretty::type_to_string(got),
        })
    }
}

/// Typechecker environment for a single module-check pass.
///
/// Cloned cheaply when we need a scoped extension (e.g. installing
/// rigid vars while checking a polymorphic def's body) so that the
/// parent scope stays immutable. Construction goes through
/// [`Env::default`] / the internal `new`; population is the
/// responsibility of [`builtins::install`] and the per-module setup in
/// `check_in_workspace`.
///
/// Several of the fields are conceptually disjoint name-spaces (term
/// vars vs effect ops vs ADT names vs ctor names), kept as separate
/// maps because the AST already commits to which channel a reference
/// goes through (`Term::Var` vs `Term::Do` vs `Term::Ctor` vs
/// `Pattern::Ctor`).
#[derive(Debug, Default, Clone)]
pub struct Env {
    /// Term-level names in scope — built-in operators, user fn/const
    /// defs of the current module, and (after pass-1) an entry per
    /// local def. Looked up by `Term::Var { name }` lookup.
    pub globals: IndexMap<String, Type>,
    /// Effect-op table. Looked up by `Term::Do { op }`. See
    /// [`builtins::EffectOpSig`] for the payload shape.
    pub effect_ops: IndexMap<String, builtins::EffectOpSig>,
    /// User-declared ADTs of the current module, by name. Populated
    /// from `Def::Type` entries; consulted by `Term::Ctor`,
    /// `Pattern::Ctor`, and the well-formedness check on declared
    /// types.
    pub types: IndexMap<String, TypeDef>,
    /// Inverse index: ctor name -> reference to the owning ADT.
    pub ctor_index: IndexMap<String, CtorRef>,
    /// Import map: alias-or-module-name → actual module name.
    /// Used when `Term::Var { name }` contains a dot
    /// (qualified cross-module reference).
    pub imports: BTreeMap<String, String>,
    /// Top-level symbol table per module of the workspace.
    /// Populated by [`crate::build_check_env`] from
    /// [`build_module_globals`].
    pub module_globals: BTreeMap<String, IndexMap<String, Type>>,
    /// Per-module import map: module-name → (alias-or-module-name →
    /// actual-module-name). Sibling-shape to [`Self::module_globals`];
    /// populated workspace-flat by [`crate::build_check_env`] so the
    /// mono pass's per-fn entry points can re-seed the local
    /// [`Self::imports`] before re-running [`synth`] on a body. Both
    /// `check_in_workspace` and `mono::build_workspace_env` consume
    /// the same env shape; `check_in_workspace` then overwrites
    /// [`Self::imports`] with the current module's map at the call
    /// site.
    pub module_imports: BTreeMap<String, BTreeMap<String, String>>,
    /// Iter 15a: ADT type definitions per module of the workspace. Used
    /// to resolve qualified type references (`module.Type` in
    /// `Type::Con.name`) and qualified `Term::Ctor.type_name`, and to
    /// fall back when a bare `Pattern::Ctor.ctor` cannot be resolved
    /// against the local module. Populated by `check_in_workspace`.
    pub module_types: BTreeMap<String, IndexMap<String, TypeDef>>,
    /// Name of the currently checked module. Used during var lookup to
    /// 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>,
    /// Iter 22b.2 (Task 9): workspace-wide class-method table. Merged
    /// from every module's [`ModuleGlobals::class_methods`] so that a
    /// `Term::Var { name: "show" }` in any module resolves to the
    /// declaring class's [`ClassMethodEntry`]. Method-name uniqueness
    /// is enforced earlier by `workspace::build_registry`'s
    /// method-name-collision check (Iter 22b.2.6), so the merge is
    /// safe (no overwrites). Read in [`synth`]'s `Term::Var` arm.
    pub class_methods: BTreeMap<String, ClassMethodEntry>,
    /// Iter 22b.2 (Task 9): one-step superclass expansion table.
    /// Maps each class name to its superclass class name. Absence from
    /// the map means the class has no superclass — populated only for
    /// classes that declare one. Used by [`check_fn`] to expand
    /// `Forall.constraints` for the missing-constraint check
    /// (Decision 11: max one step). The schema permits at most one
    /// superclass per class.
    pub class_superclasses: BTreeMap<String, String>,
    /// Iter 22b.2 (Task 10): workspace-wide instance registry, threaded
    /// through from [`Workspace::registry`]. Read by [`check_fn`] in the
    /// concrete-residual path: when a class-method call at a fully-
    /// concrete type produces a residual `(class, type_)` whose
    /// `(class, type_hash(type_))` key is absent from `registry.entries`,
    /// the fn fires `NoInstance`. Default-constructed (empty) for
    /// the standalone [`check_module`] entry point — pre-22b fixtures
    /// never invoke class methods, so the empty registry is harmless.
    pub workspace_registry: ailang_core::workspace::Registry,
}

/// Back-pointer from a ctor name to the ADT that declared it. Stored
/// in [`Env::ctor_index`] so a `Pattern::Ctor` or `Term::Ctor` can
/// resolve the owning ADT in O(1).
#[derive(Debug, Clone)]
pub struct CtorRef {
    /// Name of the ADT (i.e. the `Def::Type` name) that declared the
    /// ctor.
    pub type_name: String,
}

impl Env {
    pub(crate) fn new() -> Self {
        Self::default()
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use ailang_core::SCHEMA;

    fn fn_def(name: &str, ty: Type, params: Vec<&str>, body: Term) -> Def {
        Def::Fn(FnDef {
            name: name.into(),
            ty,
            params: params.into_iter().map(|s| s.into()).collect(),
            body,
            suppress: vec![],
            doc: None,
        })
    }

    #[test]
    fn checks_simple_arithmetic_fn() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "add",
                Type::Fn {
                    params: vec![Type::int(), Type::int()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["a", "b"],
                Term::App {
                    callee: Box::new(Term::Var { name: "+".into() }),
                    args: vec![
                        Term::Var { name: "a".into() },
                        Term::Var { name: "b".into() },
                    ],
                    tail: false,
                },
            )],
        };
        check(&m).expect("should typecheck");
    }

    #[test]
    fn rejects_type_mismatch() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "bad",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Lit {
                    lit: Literal::Bool { value: true },
                },
            )],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("type mismatch"), "got: {msg}");
    }

    #[test]
    fn requires_effect_to_be_declared() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "leaks",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::unit()),
                    effects: vec![], // !IO missing,
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Do {
                    op: "io/print_int".into(),
                    args: vec![Term::Lit {
                        lit: Literal::Int { value: 1 },
                    }],
                    tail: false,
                },
            )],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("undeclared effect"), "got: {msg}");
    }

    #[test]
    fn lets_local_shadow_global() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Let {
                    name: "x".into(),
                    value: Box::new(Term::Lit {
                        lit: Literal::Int { value: 7 },
                    }),
                    body: Box::new(Term::Var { name: "x".into() }),
                },
            )],
        };
        check(&m).expect("should typecheck");
    }

    #[test]
    fn match_must_be_exhaustive() {
        // Type Maybe = None | Some(Int); fn f only matches None -> error.
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "Maybe".into(),
                    vars: vec![],
                    ctors: vec![
                        Ctor { name: "None".into(), fields: vec![] },
                        Ctor {
                            name: "Some".into(),
                            fields: vec![Type::int()],
                        },
                    ],
                    doc: None,
                    drop_iterative: false,
                }),
                fn_def(
                    "f",
                    Type::Fn {
                        params: vec![Type::Con { name: "Maybe".into(), args: vec![] }],
                        ret: Box::new(Type::int()),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    vec!["m"],
                    Term::Match {
                        scrutinee: Box::new(Term::Var { name: "m".into() }),
                        arms: vec![Arm {
                            pat: Pattern::Ctor {
                                ctor: "None".into(),
                                fields: vec![],
                            },
                            body: Term::Lit {
                                lit: Literal::Int { value: 0 },
                            },
                        }],
                    },
                ),
            ],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("non-exhaustive"), "got: {msg}");
        assert!(msg.contains("Some"), "got: {msg}");
    }

    #[test]
    fn match_with_wildcard_is_exhaustive() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "Maybe".into(),
                    vars: vec![],
                    ctors: vec![
                        Ctor { name: "None".into(), fields: vec![] },
                        Ctor {
                            name: "Some".into(),
                            fields: vec![Type::int()],
                        },
                    ],
                    doc: None,
                    drop_iterative: false,
                }),
                fn_def(
                    "f",
                    Type::Fn {
                        params: vec![Type::Con { name: "Maybe".into(), args: vec![] }],
                        ret: Box::new(Type::int()),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    vec!["m"],
                    Term::Match {
                        scrutinee: Box::new(Term::Var { name: "m".into() }),
                        arms: vec![
                            Arm {
                                pat: Pattern::Ctor {
                                    ctor: "None".into(),
                                    fields: vec![],
                                },
                                body: Term::Lit {
                                    lit: Literal::Int { value: 0 },
                                },
                            },
                            Arm {
                                pat: Pattern::Wild,
                                body: Term::Lit {
                                    lit: Literal::Int { value: 1 },
                                },
                            },
                        ],
                    },
                ),
            ],
        };
        check(&m).expect("wildcard must satisfy exhaustiveness");
    }

    #[test]
    fn if_branches_must_match() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::If {
                    cond: Box::new(Term::Lit {
                        lit: Literal::Bool { value: true },
                    }),
                    then: Box::new(Term::Lit {
                        lit: Literal::Int { value: 1 },
                    }),
                    else_: Box::new(Term::Lit { lit: Literal::Unit }),
                },
            )],
        };
        let err = check(&m).unwrap_err();
        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()],
                    constraints: vec![],
                    body: Box::new(Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        ret: Box::new(Type::Var { name: "a".into() }),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    }),
                },
                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()],
                constraints: vec![],
                body: Box::new(Type::Fn {
                    params: vec![Type::Var { name: "a".into() }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            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![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
                tail: false,
            },
        );
        // `use_bool` returns id(true) :: Bool.
        let use_bool = fn_def(
            "use_bool",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::bool_()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
                tail: false,
            },
        );
        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()],
                constraints: vec![],
                body: Box::new(Type::Fn {
                    params: vec![Type::Var { name: "a".into() }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            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![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
                tail: false,
            },
        );
        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()],
                constraints: vec![],
                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![],
                            param_modes: vec![],
                            ret_mode: ParamMode::Implicit,
                        },
                        Type::Var { name: "a".into() },
                    ],
                    ret: Box::new(Type::Var { name: "b".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            vec!["f", "x"],
            Term::App {
                callee: Box::new(Term::Var { name: "f".into() }),
                args: vec![Term::Var { name: "x".into() }],
                tail: false,
            },
        );
        // 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![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            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 } },
                ],
                tail: false,
            },
        );
        let use_apply = fn_def(
            "use_apply",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            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 } },
                ],
                tail: false,
            },
        );
        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 13a: parameterised ADT — `type Box[a] = MkBox(a)` is well-
    /// formed and `MkBox(42)` typechecks at result type `Box<Int>`.
    #[test]
    fn parameterised_adt_ctor_at_int() {
        let box_def = Def::Type(TypeDef {
            name: "Box".into(),
            vars: vec!["a".into()],
            ctors: vec![Ctor {
                name: "MkBox".into(),
                fields: vec![Type::Var { name: "a".into() }],
            }],
            doc: None,
            drop_iterative: false,
        });
        // fn make :: () -> Box<Int> = MkBox(42)
        let make = fn_def(
            "make",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::Con {
                    name: "Box".into(),
                    args: vec![Type::int()],
                }),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::Ctor {
                type_name: "Box".into(),
                ctor: "MkBox".into(),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
            },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![box_def, make],
        };
        check(&m).expect("Box<Int> ctor should typecheck");
    }

    /// Iter 13a: ctor field type substitution and match-arm bindings.
    /// `unbox :: forall a. (Box<a>) -> a` extracts the wrapped value.
    #[test]
    fn parameterised_adt_polymorphic_unbox() {
        let box_def = Def::Type(TypeDef {
            name: "Box".into(),
            vars: vec!["a".into()],
            ctors: vec![Ctor {
                name: "MkBox".into(),
                fields: vec![Type::Var { name: "a".into() }],
            }],
            doc: None,
            drop_iterative: false,
        });
        let unbox = Def::Fn(FnDef {
            name: "unbox".into(),
            ty: Type::Forall {
                vars: vec!["a".into()],
                constraints: vec![],
                body: Box::new(Type::Fn {
                    params: vec![Type::Con {
                        name: "Box".into(),
                        args: vec![Type::Var { name: "a".into() }],
                    }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            params: vec!["b".into()],
            body: Term::Match {
                scrutinee: Box::new(Term::Var { name: "b".into() }),
                arms: vec![Arm {
                    pat: Pattern::Ctor {
                        ctor: "MkBox".into(),
                        fields: vec![Pattern::Var { name: "x".into() }],
                    },
                    body: Term::Var { name: "x".into() },
                }],
            },
            suppress: vec![],
            doc: None,
        });
        // Use unbox at Int and at Bool — both must succeed and not
        // cross-contaminate the polymorphic variable.
        let use_int = fn_def(
            "ui",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "unbox".into() }),
                args: vec![Term::Ctor {
                    type_name: "Box".into(),
                    ctor: "MkBox".into(),
                    args: vec![Term::Lit { lit: Literal::Int { value: 7 } }],
                }],
                tail: false,
            },
        );
        let use_bool = fn_def(
            "ub",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::bool_()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "unbox".into() }),
                args: vec![Term::Ctor {
                    type_name: "Box".into(),
                    ctor: "MkBox".into(),
                    args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
                }],
                tail: false,
            },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![box_def, unbox, use_int, use_bool],
        };
        check(&m).expect("polymorphic Box should typecheck at both instantiations");
    }

    /// Iter 13a: parameterised-ADT arity is enforced. `Box` (1 var)
    /// used as `Box<Int, Bool>` must error.
    #[test]
    fn parameterised_adt_arity_is_enforced() {
        let box_def = Def::Type(TypeDef {
            name: "Box".into(),
            vars: vec!["a".into()],
            ctors: vec![Ctor {
                name: "MkBox".into(),
                fields: vec![Type::Var { name: "a".into() }],
            }],
            doc: None,
            drop_iterative: false,
        });
        let bad = fn_def(
            "bad",
            Type::Fn {
                params: vec![Type::Con {
                    name: "Box".into(),
                    args: vec![Type::int(), Type::bool_()],
                }],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec!["b"],
            Term::Lit { lit: Literal::Int { value: 0 } },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![box_def, bad],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("expects 1 type arg"), "got: {msg}");
    }

    /// 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.
    #[test]
    fn seq_lhs_must_be_unit() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Seq {
                    lhs: Box::new(Term::Lit {
                        lit: Literal::Int { value: 7 },
                    }),
                    rhs: Box::new(Term::Lit {
                        lit: Literal::Int { value: 1 },
                    }),
                },
            )],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("type mismatch"), "got: {msg}");
    }

    /// Iter 14e: a `Term::App { tail: true, .. }` in non-tail position
    /// must surface as `tail-call-not-in-tail-position`. Construction:
    /// the recursive call sits as an argument to a Cons ctor (the
    /// classic constructor-blocked recursion from the 14d survey).
    #[test]
    fn tail_call_in_non_tail_position_is_rejected() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "L".into(),
                    vars: vec![],
                    ctors: vec![
                        Ctor { name: "N".into(), fields: vec![] },
                        Ctor {
                            name: "C".into(),
                            fields: vec![
                                Type::int(),
                                Type::Con { name: "L".into(), args: vec![] },
                            ],
                        },
                    ],
                    doc: None,
                    drop_iterative: false,
                }),
                fn_def(
                    "loop",
                    Type::Fn {
                        params: vec![Type::Con { name: "L".into(), args: vec![] }],
                        ret: Box::new(Type::Con { name: "L".into(), args: vec![] }),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    vec!["xs"],
                    // Body: C(0, tail-app loop xs) — the recursion is
                    // an arg to C, which is NOT a tail position.
                    Term::Ctor {
                        type_name: "L".into(),
                        ctor: "C".into(),
                        args: vec![
                            Term::Lit { lit: Literal::Int { value: 0 } },
                            Term::App {
                                callee: Box::new(Term::Var { name: "loop".into() }),
                                args: vec![Term::Var { name: "xs".into() }],
                                tail: true,
                            },
                        ],
                    },
                ),
            ],
        };
        let err = check(&m).unwrap_err();
        assert_eq!(err.code(), "tail-call-not-in-tail-position", "{err}");
    }

    // ----- Iter 15a: cross-module type / ctor resolution ------------------

    /// Helper for the cross-module tests: build a workspace whose entry
    /// imports `lib` and exposes its types via qualified names.
    fn cross_module_ws(consumer: Module) -> Workspace {
        let lib = Module {
            schema: SCHEMA.into(),
            name: "lib".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "Box".into(),
                vars: vec!["a".into()],
                ctors: vec![Ctor {
                    name: "MkBox".into(),
                    fields: vec![Type::Var { name: "a".into() }],
                }],
                doc: None,
                drop_iterative: false,
            })],
        };
        let mut modules = BTreeMap::new();
        modules.insert("lib".into(), lib);
        modules.insert(consumer.name.clone(), consumer.clone());
        Workspace {
            entry: consumer.name,
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        }
    }

    /// Iter 15a, path 1: a qualified `Type::Con` (`lib.Box`) resolves
    /// through `module_types` rather than the local-module `types`.
    #[test]
    fn cross_module_qualified_type_in_param_resolves() {
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "use_lib".into(),
            imports: vec![Import { module: "lib".into(), alias: None }],
            defs: vec![fn_def(
                "noop",
                Type::Fn {
                    params: vec![Type::Con {
                        name: "lib.Box".into(),
                        args: vec![Type::int()],
                    }],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["b"],
                Term::Lit { lit: Literal::Int { value: 0 } },
            )],
        };
        let ws = cross_module_ws(consumer);
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// Iter 15a, path 2: a qualified `Term::Ctor.type_name`
    /// (`lib.Box`) resolves and constructs `lib.Box<Int>`.
    #[test]
    fn cross_module_qualified_term_ctor_resolves() {
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "use_lib".into(),
            imports: vec![Import { module: "lib".into(), alias: None }],
            defs: vec![fn_def(
                "make",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::Con {
                        name: "lib.Box".into(),
                        args: vec![Type::int()],
                    }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Ctor {
                    type_name: "lib.Box".into(),
                    ctor: "MkBox".into(),
                    args: vec![Term::Lit { lit: Literal::Int { value: 7 } }],
                },
            )],
        };
        let ws = cross_module_ws(consumer);
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// Iter 15a (post-ct.2): a bare `Pattern::Ctor` (e.g. `MkBox x`)
    /// against a scrutinee of type `lib.Box<Int>` resolves through
    /// the type-driven lookup keyed on `expected.name`. Previously
    /// this exercised an imports-fallback; post-ct.2 the lookup is
    /// anchored to the scrutinee's qualified TypeDef directly.
    #[test]
    fn cross_module_pat_ctor_typedriven_resolves() {
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "use_lib".into(),
            imports: vec![Import { module: "lib".into(), alias: None }],
            defs: vec![fn_def(
                "open",
                Type::Fn {
                    params: vec![Type::Con {
                        name: "lib.Box".into(),
                        args: vec![Type::int()],
                    }],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["b"],
                Term::Match {
                    scrutinee: Box::new(Term::Var { name: "b".into() }),
                    arms: vec![Arm {
                        pat: Pattern::Ctor {
                            ctor: "MkBox".into(),
                            fields: vec![Pattern::Var { name: "x".into() }],
                        },
                        body: Term::Var { name: "x".into() },
                    }],
                },
            )],
        };
        let ws = cross_module_ws(consumer);
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// Iter 15b: a recursive cross-module ADT (`std_list.List a` with a
    /// `Cons a (List a)` ctor) round-trips through both `Term::Ctor` synth
    /// and pattern-ctor binding without unqualified-field-name unification
    /// failures. The bug fixed in 15b: `cdef.fields` on the imported side
    /// carries `Con("List", _)` (unqualified, owner's local namespace),
    /// while the consumer-visible scrutinee/result type is
    /// `Con("std_list.List", _)`. Without `qualify_local_types` applied
    /// to the fields at use sites, `unify` rejected the mismatch.
    #[test]
    fn cross_module_recursive_adt_term_and_pat_ctor() {
        // Library: `data List a = Nil | Cons a (List a)`. The `Cons`
        // field types reference the local-namespace `List`, exactly
        // mirroring the std_list shape that tripped the gap.
        let lib = Module {
            schema: SCHEMA.into(),
            name: "lst".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "List".into(),
                vars: vec!["a".into()],
                ctors: vec![
                    Ctor { name: "Nil".into(), fields: vec![] },
                    Ctor {
                        name: "Cons".into(),
                        fields: vec![
                            Type::Var { name: "a".into() },
                            Type::Con {
                                name: "List".into(),
                                args: vec![Type::Var { name: "a".into() }],
                            },
                        ],
                    },
                ],
                doc: None,
                drop_iterative: false,
            })],
        };
        // Consumer: builds `Cons 1 (Cons 2 (Nil))` via qualified
        // `lst.List/Cons` and pattern-matches it back out. The match
        // arm exercises the symmetric pat-ctor fix.
        let cons = |head: i64, tail: Term| Term::Ctor {
            type_name: "lst.List".into(),
            ctor: "Cons".into(),
            args: vec![
                Term::Lit { lit: Literal::Int { value: head } },
                tail,
            ],
        };
        let nil = Term::Ctor {
            type_name: "lst.List".into(),
            ctor: "Nil".into(),
            args: vec![],
        };
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "uses_lst".into(),
            imports: vec![Import { module: "lst".into(), alias: None }],
            defs: vec![fn_def(
                "head_or_zero",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Match {
                    scrutinee: Box::new(cons(1, cons(2, nil.clone()))),
                    arms: vec![
                        Arm {
                            pat: Pattern::Ctor {
                                ctor: "Cons".into(),
                                fields: vec![
                                    Pattern::Var { name: "h".into() },
                                    Pattern::Wild,
                                ],
                            },
                            body: Term::Var { name: "h".into() },
                        },
                        Arm {
                            pat: Pattern::Ctor {
                                ctor: "Nil".into(),
                                fields: vec![],
                            },
                            body: Term::Lit { lit: Literal::Int { value: 0 } },
                        },
                    ],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("lst".into(), lib);
        modules.insert("uses_lst".into(), consumer);
        let ws = Workspace {
            entry: "uses_lst".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// ct.2 Task 1: a class method whose declared return type is a
    /// bare local Type::Con in the defining module (e.g.
    /// `compare : a -> a -> Ordering` declared inside `prelude`) must
    /// be presented to a consumer module's typecheck context with the
    /// return type qualified (`prelude.Ordering`). Without this, the
    /// consumer's `Pattern::Ctor LT` against the scrutinee no longer
    /// resolves once the post-ct.1 canonical form removes the
    /// imports-fallback that previously papered over the mismatch.
    #[test]
    fn ct2_class_method_cross_module_qualifies_return_type() {
        // Defining module declares `Ordering` locally and a class
        // `Ord` with a method `compare : a -> a -> Ordering`. The
        // `Ordering` Type::Con is bare-local in the class method's ty,
        // which is canonical post-ct.1 (bare = local to defining module).
        let prelude = Module {
            schema: SCHEMA.into(),
            name: "p".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "Ordering".into(),
                    vars: vec![],
                    ctors: vec![
                        Ctor { name: "LT".into(), fields: vec![] },
                        Ctor { name: "EQ".into(), fields: vec![] },
                        Ctor { name: "GT".into(), fields: vec![] },
                    ],
                    doc: None,
                    drop_iterative: false,
                }),
                Def::Class(ClassDef {
                    name: "Ord".into(),
                    param: "a".into(),
                    superclass: None,
                    methods: vec![ClassMethod {
                        name: "compare".into(),
                        ty: Type::Forall {
                            vars: vec!["a".into()],
                            constraints: vec![],
                            body: Box::new(Type::Fn {
                                params: vec![
                                    Type::Var { name: "a".into() },
                                    Type::Var { name: "a".into() },
                                ],
                                ret: Box::new(Type::Con {
                                    name: "Ordering".into(),
                                    args: vec![],
                                }),
                                effects: vec![],
                                param_modes: vec![],
                                ret_mode: ParamMode::Implicit,
                            }),
                        },
                        default: None,
                    }],
                    doc: None,
                }),
                Def::Instance(InstanceDef {
                    class: "Ord".into(),
                    type_: Type::int(),
                    methods: vec![InstanceMethod {
                        name: "compare".into(),
                        body: Term::Lam {
                            params: vec!["x".into(), "y".into()],
                            param_tys: vec![Type::int(), Type::int()],
                            ret_ty: Box::new(Type::Con {
                                name: "Ordering".into(),
                                args: vec![],
                            }),
                            effects: vec![],
                            body: Box::new(Term::Ctor {
                                type_name: "Ordering".into(),
                                ctor: "EQ".into(),
                                args: vec![],
                            }),
                        },
                    }],
                    doc: None,
                }),
            ],
        };
        // Consumer module imports prelude and calls `compare` (bare).
        // The return type seen by the consumer must be `p.Ordering`,
        // not bare `Ordering` — otherwise the match arm below fails to
        // typecheck because the Pattern::Ctor lookup is type-driven and
        // would not find `LT` in any TypeDef named bare `Ordering` in
        // the consumer's local types.
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "u".into(),
            imports: vec![Import { module: "p".into(), alias: None }],
            defs: vec![fn_def(
                "use_compare",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Match {
                    scrutinee: Box::new(Term::App {
                        callee: Box::new(Term::Var { name: "compare".into() }),
                        args: vec![
                            Term::Lit { lit: Literal::Int { value: 1 } },
                            Term::Lit { lit: Literal::Int { value: 2 } },
                        ],
                        tail: false,
                    }),
                    arms: vec![
                        Arm {
                            pat: Pattern::Ctor {
                                ctor: "LT".into(),
                                fields: vec![],
                            },
                            body: Term::Lit { lit: Literal::Int { value: 1 } },
                        },
                        Arm {
                            pat: Pattern::Ctor {
                                ctor: "EQ".into(),
                                fields: vec![],
                            },
                            body: Term::Lit { lit: Literal::Int { value: 2 } },
                        },
                        Arm {
                            pat: Pattern::Ctor {
                                ctor: "GT".into(),
                                fields: vec![],
                            },
                            body: Term::Lit { lit: Literal::Int { value: 3 } },
                        },
                    ],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("p".into(), prelude);
        modules.insert("u".into(), consumer);
        let ws = Workspace {
            entry: "u".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(
            diags.is_empty(),
            "consumer module must typecheck cleanly when calling a class \
             method whose return type is bare-local in its defining \
             module; the class-method channel must apply \
             qualify_local_types just like the qualified Term::Var path \
             does. Got diagnostics: {:?}",
            diags
        );
    }

    /// ct.2 Task 1: `qualify_local_types`'s `Type::Forall` arm must
    /// recurse into `constraints[].type_`. A class method whose
    /// declared type is `Forall<a>{Ord a}. Fn[..]` carries the
    /// constraint type `Type::Var { name: "a" }` — fine — but a
    /// hypothetical `Forall<a>{Show p.Foo}. Fn[..]` would carry a
    /// bare-local `Foo` if the defining module is `p`, and the
    /// consumer must see `p.Foo` after the cross-module qualifier
    /// runs. Symmetric to the ct.1.5a-followup fix on
    /// `normalize_type_for_registry`.
    #[test]
    fn ct2_qualify_local_types_recurses_into_forall_constraints() {
        use crate::qualify_local_types;
        let mut local_types: IndexMap<String, TypeDef> = IndexMap::new();
        local_types.insert("Foo".into(), TypeDef {
            name: "Foo".into(),
            vars: vec![],
            ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
            doc: None,
            drop_iterative: false,
        });
        let input = Type::Forall {
            vars: vec!["a".into()],
            constraints: vec![Constraint {
                class: "Show".into(),
                type_: Type::Con { name: "Foo".into(), args: vec![] },
            }],
            body: Box::new(Type::Fn {
                params: vec![Type::Var { name: "a".into() }],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            }),
        };
        let out = qualify_local_types(&input, "p", &local_types);
        match out {
            Type::Forall { constraints, .. } => {
                assert_eq!(constraints.len(), 1, "constraint count preserved");
                match &constraints[0].type_ {
                    Type::Con { name, .. } => assert_eq!(
                        name, "p.Foo",
                        "constraint Type::Con must be qualified by qualify_local_types"
                    ),
                    other => panic!("expected Type::Con, got {:?}", other),
                }
            }
            other => panic!("expected Type::Forall, got {:?}", other),
        }
    }

    /// Iter 14e: a `Term::App { tail: true, .. }` that genuinely sits
    /// in tail position (as the rhs of a `Seq` that is the body of a
    /// `Match` arm that is the body of the fn) must pass.
    #[test]
    fn tail_call_in_tail_position_is_accepted() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "L".into(),
                    vars: vec![],
                    ctors: vec![
                        Ctor { name: "N".into(), fields: vec![] },
                        Ctor {
                            name: "C".into(),
                            fields: vec![
                                Type::int(),
                                Type::Con { name: "L".into(), args: vec![] },
                            ],
                        },
                    ],
                    doc: None,
                    drop_iterative: false,
                }),
                fn_def(
                    "drain",
                    Type::Fn {
                        params: vec![Type::Con { name: "L".into(), args: vec![] }],
                        ret: Box::new(Type::unit()),
                        effects: vec!["IO".into()],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    vec!["xs"],
                    Term::Match {
                        scrutinee: Box::new(Term::Var { name: "xs".into() }),
                        arms: vec![
                            Arm {
                                pat: Pattern::Ctor {
                                    ctor: "N".into(),
                                    fields: vec![],
                                },
                                body: Term::Lit { lit: Literal::Unit },
                            },
                            Arm {
                                pat: Pattern::Ctor {
                                    ctor: "C".into(),
                                    fields: vec![
                                        Pattern::Var { name: "h".into() },
                                        Pattern::Var { name: "t".into() },
                                    ],
                                },
                                body: Term::Seq {
                                    lhs: Box::new(Term::Do {
                                        op: "io/print_int".into(),
                                        args: vec![Term::Var { name: "h".into() }],
                                        tail: false,
                                    }),
                                    rhs: Box::new(Term::App {
                                        callee: Box::new(Term::Var { name: "drain".into() }),
                                        args: vec![Term::Var { name: "t".into() }],
                                        tail: true,
                                    }),
                                },
                            },
                        ],
                    },
                ),
            ],
        };
        check(&m).expect("tail-call in tail position should typecheck");
    }

    /// Iter 16b.3: a `Term::LetRec` that captures a `Term::Let`-bound
    /// name (whose type is known only after typecheck) reaches `synth`
    /// because the desugar pass leaves it in place. The new typing
    /// rule for `Term::LetRec` accepts it: extends locals with `name`
    /// and the params, synths the body, unifies against the declared
    /// return type, then synths the in-clause.
    #[test]
    fn letrec_with_let_binding_capture_typechecks() {
        // fn outer : (Int) -> Int = \n.
        //   let threshold = + 5 5
        //   in let-rec loop : (Int) -> Int = \i.
        //        if (>= i threshold) then 0 else loop (+ i 1)
        //      in loop 0
        let body = Term::Let {
            name: "threshold".into(),
            value: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "+".into() }),
                args: vec![
                    Term::Lit { lit: Literal::Int { value: 5 } },
                    Term::Lit { lit: Literal::Int { value: 5 } },
                ],
                tail: false,
            }),
            body: Box::new(Term::LetRec {
                name: "loop".into(),
                ty: Type::Fn {
                    params: vec![Type::int()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                params: vec!["i".into()],
                body: Box::new(Term::If {
                    cond: Box::new(Term::App {
                        callee: Box::new(Term::Var { name: ">=".into() }),
                        args: vec![
                            Term::Var { name: "i".into() },
                            Term::Var { name: "threshold".into() },
                        ],
                        tail: false,
                    }),
                    then: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
                    else_: Box::new(Term::App {
                        callee: Box::new(Term::Var { name: "loop".into() }),
                        args: vec![Term::App {
                            callee: Box::new(Term::Var { name: "+".into() }),
                            args: vec![
                                Term::Var { name: "i".into() },
                                Term::Lit { lit: Literal::Int { value: 1 } },
                            ],
                            tail: false,
                        }],
                        tail: false,
                    }),
                }),
                in_term: Box::new(Term::App {
                    callee: Box::new(Term::Var { name: "loop".into() }),
                    args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
                    tail: false,
                }),
            }),
        };
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "outer",
                Type::Fn {
                    params: vec![Type::int()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["n"],
                body,
            )],
        };
        check(&m).expect("LetRec with Let-binding capture should typecheck");
    }

    /// Iter 16b.3: a LetRec whose body returns the wrong type (Bool
    /// instead of the declared Int) is caught by the new typing rule.
    /// Property protected: the new arm in `synth` for `Term::LetRec`
    /// runs `unify(&ret_ty, &body_ty, subst)` just like `Term::Lam`
    /// and `check_fn`.
    #[test]
    fn letrec_body_wrong_return_type_is_rejected() {
        // (let-rec wrong (params x) (type (Int) -> Int) (body true)
        //                                            (in  (app wrong 0)))
        let letrec = Term::LetRec {
            name: "wrong".into(),
            ty: Type::Fn {
                params: vec![Type::int()],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            params: vec!["x".into()],
            body: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
            in_term: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "wrong".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
                tail: false,
            }),
        };
        // Wrap in a Let so the desugar pass defers the LetRec (its
        // body would otherwise lift cleanly with no captures, since
        // `true` doesn't reference `x`).
        let body = Term::Let {
            name: "y".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
            // Reference `y` inside the LetRec body so it captures.
            body: Box::new(Term::LetRec {
                name: "wrong".into(),
                ty: Type::Fn {
                    params: vec![Type::int()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                params: vec!["x".into()],
                body: Box::new(Term::Seq {
                    // Use `y` so the LetRec captures it (forces deferral).
                    lhs: Box::new(Term::Lit { lit: Literal::Unit }),
                    rhs: Box::new(Term::App {
                        callee: Box::new(Term::Var { name: "+".into() }),
                        args: vec![
                            Term::Var { name: "y".into() },
                            Term::Lit { lit: Literal::Bool { value: true } },
                        ],
                        tail: false,
                    }),
                }),
                in_term: Box::new(Term::App {
                    callee: Box::new(Term::Var { name: "wrong".into() }),
                    args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
                    tail: false,
                }),
            }),
        };
        // (Suppress dead-code warning on the unused unwrapped letrec.)
        let _ = letrec;
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "outer",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                body,
            )],
        };
        let err = check(&m).expect_err("LetRec body returning Bool but declared Int must error");
        let msg = format!("{err}");
        assert!(
            msg.contains("type mismatch"),
            "expected a type-mismatch diagnostic, got: {msg}"
        );
    }

    /// Iter 16b.3: `lift_letrecs` on a module containing a deferred
    /// LetRec produces a module whose defs include a synthetic
    /// `<hint>$lr_N` FnDef and whose original fn body has rewritten
    /// call sites.
    #[test]
    fn lift_letrecs_on_let_capture_produces_synthetic_fn() {
        // fn outer : () -> Int = \.
        //   let y = 7
        //   in let-rec helper : (Int) -> Int = \x. + x y
        //      in helper 1
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "outer",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Let {
                    name: "y".into(),
                    value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
                    body: Box::new(Term::LetRec {
                        name: "helper".into(),
                        ty: Type::Fn {
                            params: vec![Type::int()],
                            ret: Box::new(Type::int()),
                            effects: vec![],
                            param_modes: vec![],
                            ret_mode: ParamMode::Implicit,
                        },
                        params: vec!["x".into()],
                        body: Box::new(Term::App {
                            callee: Box::new(Term::Var { name: "+".into() }),
                            args: vec![
                                Term::Var { name: "x".into() },
                                Term::Var { name: "y".into() },
                            ],
                            tail: false,
                        }),
                        in_term: Box::new(Term::App {
                            callee: Box::new(Term::Var { name: "helper".into() }),
                            args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
                            tail: false,
                        }),
                    }),
                },
            )],
        };
        // Typecheck must succeed (the new LetRec rule accepts this).
        check(&m).expect("typecheck before lift");
        let desugared = ailang_core::desugar::desugar_module(&m);
        // After desugar the LetRec is still present (Let-binding capture).
        // After lift_letrecs it must be gone, replaced by a synthetic
        // top-level fn with the capture appended to its signature.
        let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
        assert_eq!(lifted.defs.len(), 2, "expected one synthetic fn appended");
        let synth = match &lifted.defs[1] {
            Def::Fn(f) => f,
            _ => panic!("expected synthetic FnDef"),
        };
        assert!(
            synth.name.starts_with("helper$lr_"),
            "lifted name `{}` should start with `helper$lr_`",
            synth.name
        );
        assert_eq!(
            synth.ty,
            Type::Fn {
                params: vec![Type::int(), Type::int()],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            "lifted ty should have capture appended; got {:?}",
            synth.ty
        );
        assert_eq!(synth.params, vec!["x".to_string(), "y".to_string()]);
        // `outer`'s body must have the `(app helper 1)` rewritten to
        // `(app helper$lr_0 1 y)`. The body is now
        // `let y = 7 in (app helper$lr_0 1 y)`.
        let outer_body = match &lifted.defs[0] {
            Def::Fn(f) => &f.body,
            _ => unreachable!(),
        };
        let inner = match outer_body {
            Term::Let { body, .. } => body.as_ref(),
            other => panic!("expected outer Let, got {other:?}"),
        };
        match inner {
            Term::App { callee, args, .. } => {
                match callee.as_ref() {
                    Term::Var { name } => assert_eq!(name, &synth.name),
                    other => panic!("expected lifted callee, got {other:?}"),
                }
                assert_eq!(args.len(), 2, "expected 2 args (1 original + 1 capture)");
                match &args[1] {
                    Term::Var { name } => assert_eq!(name, "y"),
                    other => panic!("expected y as second arg, got {other:?}"),
                }
            }
            other => panic!("expected App after Let, got {other:?}"),
        }
    }

    /// Iter 16b.4: a LetRec whose body captures a `Pattern::Ctor`-Var
    /// match-arm binding is lifted by `lift_letrecs` to a synthetic
    /// top-level fn whose signature has the binding's type appended.
    /// Property protected: `type_check_pattern_for_lift` substitutes
    /// the matched ADT's type args (`[Int, Int]`) into the ctor's
    /// declared field types (`[a, b]`) and returns `[(x, Int),
    /// (y, Int)]`; the lifted fn picks up `x: Int` as the capture
    /// type. Without 16b.4, the desugar pass would have panicked
    /// before reaching `lift_letrecs`.
    #[test]
    fn lift_letrecs_on_match_arm_capture_produces_synthetic_fn() {
        // (data Pair (vars a b) (ctor MkPair a b))
        // (fn outer : (Pair Int Int) -> Int = \p.
        //   match p
        //     case (pat-ctor MkPair x y) ->
        //       let-rec helper : (Int) -> Int = \z. + z x
        //       in (app helper 0))
        let pair_td = TypeDef {
            name: "Pair".into(),
            vars: vec!["a".into(), "b".into()],
            ctors: vec![Ctor {
                name: "MkPair".into(),
                fields: vec![
                    Type::Var { name: "a".into() },
                    Type::Var { name: "b".into() },
                ],
            }],
            doc: None,
            drop_iterative: false,
        };
        let letrec = Term::LetRec {
            name: "helper".into(),
            ty: Type::Fn {
                params: vec![Type::int()],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            params: vec!["z".into()],
            body: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "+".into() }),
                args: vec![
                    Term::Var { name: "z".into() },
                    Term::Var { name: "x".into() },
                ],
                tail: false,
            }),
            in_term: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "helper".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
                tail: false,
            }),
        };
        let outer_body = Term::Match {
            scrutinee: Box::new(Term::Var { name: "p".into() }),
            arms: vec![Arm {
                pat: Pattern::Ctor {
                    ctor: "MkPair".into(),
                    fields: vec![
                        Pattern::Var { name: "x".into() },
                        Pattern::Var { name: "y".into() },
                    ],
                },
                body: letrec,
            }],
        };
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(pair_td),
                fn_def(
                    "outer",
                    Type::Fn {
                        params: vec![Type::Con {
                            name: "Pair".into(),
                            args: vec![Type::int(), Type::int()],
                        }],
                        ret: Box::new(Type::int()),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    vec!["p"],
                    outer_body,
                ),
            ],
        };
        // Typecheck must succeed.
        check(&m).expect("typecheck before lift");
        let desugared = ailang_core::desugar::desugar_module(&m);
        // Match-arm capture: desugar leaves the LetRec in place.
        let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
        // Pair (Type) + outer (Fn) + helper$lr_0 (Fn) = 3.
        assert_eq!(lifted.defs.len(), 3, "expected one synthetic fn appended");
        let synth = match &lifted.defs[2] {
            Def::Fn(f) => f,
            _ => panic!("expected synthetic FnDef at index 2"),
        };
        assert!(
            synth.name.starts_with("helper$lr_"),
            "lifted name `{}` should start with `helper$lr_`",
            synth.name
        );
        // Lifted ty: original (Int) -> Int with capture type Int
        // appended → (Int, Int) -> Int.
        assert_eq!(
            synth.ty,
            Type::Fn {
                params: vec![Type::int(), Type::int()],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            "lifted ty should have the match-arm-capture type Int appended; got {:?}",
            synth.ty
        );
        assert_eq!(synth.params, vec!["z".to_string(), "x".to_string()]);
    }

    /// Iter 16b.6: post-typecheck `lift_letrecs` lifts a deferred
    /// LetRec inside a polymorphic enclosing fn into a `Forall`-typed
    /// synthetic top-level fn, mirroring the enclosing fn's type
    /// vars. Property protected:
    ///
    /// 1. The fast-path desugar lift handles the `KnownType`-only
    ///    case end-to-end (see desugar's
    ///    `let_rec_capture_under_polymorphic_enclosing_fn_lifts_to_forall_fn`).
    /// 2. The defer path (some capture is `Term::Let`-bound) goes
    ///    through `lift_letrecs`. This test forces that path by
    ///    introducing a `Term::Let { z = 7 }` inside the body and
    ///    capturing `z`. The lifted fn must still be `Forall(a). Fn(...)`,
    ///    even though the lift happens post-typecheck rather than
    ///    in desugar.
    ///
    /// Without 16b.6, lift_letrecs would have panicked on the
    /// `Type::Forall` match arm at lift-construction time.
    #[test]
    fn lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn() {
        // fn outer : Forall(a). (a) -> a = \x.
        //   let z = 7
        //   in let-rec helper : (Int) -> a = \k. if k == 0 then x else helper(k-1) + z (impossible — types don't match)
        //
        // Simpler shape: capture z (Let-bound, Int) in a polymorphic
        // enclosing fn, with a body that returns x (the polymorphic
        // capture).
        //
        // fn outer : Forall(a). (a) -> a = \x.
        //   let z = 7
        //   in let-rec helper : (Int) -> a = \k.
        //     if k == 0 then x else helper(k - z)
        //   in helper 1
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "outer",
                Type::Forall {
                    vars: vec!["a".into()],
                    constraints: vec![],
                    body: Box::new(Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        ret: Box::new(Type::Var { name: "a".into() }),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    }),
                },
                vec!["x".into()],
                Term::Let {
                    name: "z".into(),
                    value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
                    body: Box::new(Term::LetRec {
                        name: "helper".into(),
                        ty: Type::Fn {
                            params: vec![Type::int()],
                            ret: Box::new(Type::Var { name: "a".into() }),
                            effects: vec![],
                            param_modes: vec![],
                            ret_mode: ParamMode::Implicit,
                        },
                        params: vec!["k".into()],
                        body: Box::new(Term::If {
                            cond: Box::new(Term::App {
                                callee: Box::new(Term::Var { name: "==".into() }),
                                args: vec![
                                    Term::Var { name: "k".into() },
                                    Term::Lit { lit: Literal::Int { value: 0 } },
                                ],
                                tail: false,
                            }),
                            then: Box::new(Term::Var { name: "x".into() }),
                            else_: Box::new(Term::App {
                                callee: Box::new(Term::Var { name: "helper".into() }),
                                args: vec![Term::App {
                                    callee: Box::new(Term::Var { name: "-".into() }),
                                    args: vec![
                                        Term::Var { name: "k".into() },
                                        Term::Var { name: "z".into() },
                                    ],
                                    tail: false,
                                }],
                                tail: false,
                            }),
                        }),
                        in_term: Box::new(Term::App {
                            callee: Box::new(Term::Var { name: "helper".into() }),
                            args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
                            tail: false,
                        }),
                    }),
                },
            )],
        };
        // Typecheck succeeds.
        check(&m).expect("typecheck before lift");
        let desugared = ailang_core::desugar::desugar_module(&m);
        // After desugar the LetRec should still be present (the
        // capture set is `{x: KnownType, z: LetBound}` and any
        // LetBound forces deferral).
        let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
        assert_eq!(
            lifted.defs.len(),
            2,
            "expected one synthetic fn appended; got {:?}",
            lifted.defs.iter().map(|d| d.name()).collect::<Vec<_>>()
        );
        let synth = match &lifted.defs[1] {
            Def::Fn(f) => f,
            _ => panic!("expected synthetic FnDef"),
        };
        assert!(
            synth.name.starts_with("helper$lr_"),
            "lifted name `{}` should start with `helper$lr_`",
            synth.name
        );
        // Lifted ty must be Forall(a). Fn(Int, a, Int) -> a.
        // Original LetRec params: [Int]; captures (BTreeSet order):
        // x: a then z: Int (alphabetical). Ret: a.
        match &synth.ty {
            Type::Forall { vars, constraints: _, body } => {
                assert_eq!(
                    vars,
                    &vec!["a".to_string()],
                    "Forall vars must mirror enclosing fn's vars; got {:?}",
                    vars
                );
                match body.as_ref() {
                    Type::Fn { params, ret, .. } => {
                        assert_eq!(params.len(), 3, "expected k + x + z params");
                        assert!(
                            matches!(&params[0], Type::Con { name, .. } if name == "Int"),
                            "first param: original k:Int; got {:?}",
                            params[0]
                        );
                        // Captures are in BTreeSet order, so x (a-typed) comes before z (Int).
                        assert!(
                            matches!(&params[1], Type::Var { name } if name == "a"),
                            "second param: x: a; got {:?}",
                            params[1]
                        );
                        assert!(
                            matches!(&params[2], Type::Con { name, .. } if name == "Int"),
                            "third param: z: Int; got {:?}",
                            params[2]
                        );
                        assert!(
                            matches!(ret.as_ref(), Type::Var { name } if name == "a"),
                            "ret: a; got {:?}",
                            ret
                        );
                    }
                    other => panic!("Forall body must be Fn; got {:?}", other),
                }
            }
            other => panic!(
                "lifted type must be Forall (mirroring enclosing); got {:?}",
                other
            ),
        }
        assert_eq!(
            synth.params,
            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![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                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"
        );
    }

    /// Iter 18d.1: a `(reuse-as xs 42)` where the body is a literal
    /// (not a `Term::Ctor` and not `Term::Lam`) must emit
    /// `reuse-as-non-allocating-body` with `ctx.got = "lit"`. The
    /// suggested rewrite drops the wrapper; the replacement parses
    /// via `parse_term`.
    #[test]
    fn reuse_as_with_non_allocating_body_is_reported() {
        // Body: (reuse-as x 42) — `x` is the param, body is a lit.
        let body = Term::ReuseAs {
            source: Box::new(Term::Var { name: "x".into() }),
            body: Box::new(Term::Lit { lit: Literal::Int { value: 42 } }),
        };
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![Type::int()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["x"],
                body,
            )],
        };
        let diags = check_module(&m);
        let bad: Vec<&Diagnostic> = diags
            .iter()
            .filter(|d| d.code == "reuse-as-non-allocating-body")
            .collect();
        assert_eq!(
            bad.len(),
            1,
            "want exactly one reuse-as-non-allocating-body; got: {diags:#?}"
        );
        let d = bad[0];
        assert_eq!(d.severity, Severity::Error);
        assert_eq!(d.def.as_deref(), Some("f"));
        assert_eq!(d.ctx.get("got").and_then(|v| v.as_str()), Some("lit"));
        assert_eq!(d.suggested_rewrites.len(), 1);
        // Replacement is the body without the wrapper — must parse.
        let rep = &d.suggested_rewrites[0].replacement;
        ailang_surface::parse_term(rep)
            .unwrap_or_else(|e| panic!("suggested rewrite must parse: {rep} ({e})"));
    }

    /// Floats milestone post-fieldtest B1 (RED): pattern-matching on a
    /// `Literal::Float` literal must be hard-rejected at typecheck via
    /// `CheckError::FloatPatternNotAllowed` per DESIGN.md §"Float
    /// semantics" — even when the match arm reaches `check` through
    /// the *full* check pipeline (which runs `desugar_module` first).
    ///
    /// The existing `reject_float_pattern_in_match` test in
    /// `crates/ailang-check/src/builtins.rs` calls `synth(...)`
    /// directly on a hand-built `Term::Match`, bypassing desugar; it
    /// passes today but does not protect the property the spec
    /// promises. The desugar pass `build_eq` rewrites
    /// `Pattern::Lit { lit }` arms (including `Literal::Float`) into
    /// `Term::If { cond: (== scrutinee lit), .. }` *before* typecheck
    /// runs (see `crates/ailang-core/src/desugar.rs:1056`), so the
    /// `Pattern::Lit { lit: Literal::Float { .. } }` arm at
    /// `lib.rs:2316` is unreachable on input that flows through
    /// `check`/`check_module`/`check_workspace`. This test exercises
    /// the full pipeline and pins the Float-pattern hard-reject as
    /// a property of the public check API.
    #[test]
    fn check_rejects_float_pattern_through_full_pipeline() {
        // fn classify : (Float) -> Int = \x. match x { 0.0 -> 1; _ -> 0 }
        let bits = 0.0_f64.to_bits();
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "classify",
                Type::Fn {
                    params: vec![Type::float()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["x"],
                Term::Match {
                    scrutinee: Box::new(Term::Var { name: "x".into() }),
                    arms: vec![
                        Arm {
                            pat: Pattern::Lit {
                                lit: Literal::Float { bits },
                            },
                            body: Term::Lit { lit: Literal::Int { value: 1 } },
                        },
                        Arm {
                            pat: Pattern::Wild,
                            body: Term::Lit { lit: Literal::Int { value: 0 } },
                        },
                    ],
                },
            )],
        };
        let err = check(&m).expect_err(
            "Pattern::Lit { Literal::Float } must be rejected at typecheck",
        );
        assert!(
            matches!(err, CheckError::FloatPatternNotAllowed),
            "expected CheckError::FloatPatternNotAllowed, got {err:?}"
        );
    }

    /// ct.2 Task 2: a `Pattern::Ctor` against a scrutinee of type
    /// `Type::Con { name: "p.T", .. }` looks up the TypeDef in
    /// `env.module_types["p"]["T"]` and finds the ctor by name within
    /// it — no `env.ctor_index` consult, no imports-walk. This pins the
    /// new lookup strategy.
    #[test]
    fn ct2_pattern_ctor_type_driven_lookup_cross_module() {
        let lib = Module {
            schema: SCHEMA.into(),
            name: "lib".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "Box".into(),
                vars: vec!["a".into()],
                ctors: vec![Ctor {
                    name: "MkBox".into(),
                    fields: vec![Type::Var { name: "a".into() }],
                }],
                doc: None,
                drop_iterative: false,
            })],
        };
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "use_lib".into(),
            imports: vec![Import { module: "lib".into(), alias: None }],
            defs: vec![fn_def(
                "open",
                Type::Fn {
                    params: vec![Type::Con {
                        name: "lib.Box".into(),
                        args: vec![Type::int()],
                    }],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["b"],
                Term::Match {
                    scrutinee: Box::new(Term::Var { name: "b".into() }),
                    arms: vec![Arm {
                        pat: Pattern::Ctor {
                            ctor: "MkBox".into(),
                            fields: vec![Pattern::Var { name: "x".into() }],
                        },
                        body: Term::Var { name: "x".into() },
                    }],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("lib".into(), lib);
        modules.insert("use_lib".into(), consumer);
        let ws = Workspace {
            entry: "use_lib".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// ct.2 Task 2: when the scrutinee carries a Type::Con name that
    /// doesn't resolve to any TypeDef (workspace-wide), the pattern
    /// lookup must fail closed. The post-ct.1 validator catches this
    /// shape earlier for canonical inputs; this test pins the residual
    /// runtime guard against constructed (non-loaded) AST.
    #[test]
    fn ct2_pattern_ctor_fails_closed_when_scrutinee_type_unknown() {
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "u".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![Type::Con {
                        name: "Nonexistent".into(),
                        args: vec![],
                    }],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["x"],
                Term::Match {
                    scrutinee: Box::new(Term::Var { name: "x".into() }),
                    arms: vec![Arm {
                        pat: Pattern::Ctor {
                            ctor: "Whatever".into(),
                            fields: vec![],
                        },
                        body: Term::Lit { lit: Literal::Int { value: 0 } },
                    }],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("u".into(), consumer);
        let ws = Workspace {
            entry: "u".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(
            !diags.is_empty(),
            "expected at least one diagnostic for unknown scrutinee \
             type, got none"
        );
    }

    /// ct.2 Task 3: a bare `Term::Ctor.type_name` that does not resolve
    /// to a local TypeDef must error with `UnknownType` (or
    /// `UnknownCtor`, depending on which check fires first). The
    /// imports-fallback that previously synthesised a qualified result
    /// from an arbitrary imported module is gone. The
    /// post-ct.1 validator catches this shape at load time for
    /// canonical inputs; this test pins the residual runtime guard
    /// against constructed (non-loaded) AST.
    #[test]
    fn ct2_term_ctor_bare_cross_module_fails_closed() {
        let prelude = Module {
            schema: SCHEMA.into(),
            name: "p".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "Ordering".into(),
                vars: vec![],
                ctors: vec![
                    Ctor { name: "LT".into(), fields: vec![] },
                    Ctor { name: "EQ".into(), fields: vec![] },
                    Ctor { name: "GT".into(), fields: vec![] },
                ],
                doc: None,
                drop_iterative: false,
            })],
        };
        // Consumer imports prelude but writes BARE `Ordering` in
        // Term::Ctor — this is a stale-canonical-form construction.
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "u".into(),
            imports: vec![Import { module: "p".into(), alias: None }],
            defs: vec![fn_def(
                "stale",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::Con {
                        name: "p.Ordering".into(),
                        args: vec![],
                    }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Ctor {
                    type_name: "Ordering".into(),
                    ctor: "LT".into(),
                    args: vec![],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("p".into(), prelude);
        modules.insert("u".into(), consumer);
        let ws = Workspace {
            entry: "u".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(
            diags.iter().any(|d| d.code == "unknown-type"),
            "expected unknown-type diagnostic for bare cross-module \
             Term::Ctor; got {diags:?}"
        );
    }

    /// ct.2 Task 3: a qualified `Term::Ctor.type_name`
    /// (`p.Ordering` / `LT`) continues to resolve cleanly through the
    /// qualified branch. This is the canonical form post-ct.1 and the
    /// hot path for every Term::Ctor in a migrated fixture.
    #[test]
    fn ct2_term_ctor_qualified_cross_module_resolves() {
        let prelude = Module {
            schema: SCHEMA.into(),
            name: "p".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "Ordering".into(),
                vars: vec![],
                ctors: vec![
                    Ctor { name: "LT".into(), fields: vec![] },
                    Ctor { name: "EQ".into(), fields: vec![] },
                    Ctor { name: "GT".into(), fields: vec![] },
                ],
                doc: None,
                drop_iterative: false,
            })],
        };
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "u".into(),
            imports: vec![Import { module: "p".into(), alias: None }],
            defs: vec![fn_def(
                "lt",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::Con {
                        name: "p.Ordering".into(),
                        args: vec![],
                    }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Ctor {
                    type_name: "p.Ordering".into(),
                    ctor: "LT".into(),
                    args: vec![],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("p".into(), prelude);
        modules.insert("u".into(), consumer);
        let ws = Workspace {
            entry: "u".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// Iter 23.4-prep Task 2: bare-name resolution falls through to free
    /// fns of implicitly-imported modules. The consumer calls bare `dbl`,
    /// declared in `prelude` (the singleton implicit import today). The
    /// pre-fix behaviour is `unbound-var` because the `Term::Var` lookup
    /// ladder consults locals → local globals → class_methods →
    /// dot-qualified, but never the flat free-fn tables of implicit
    /// imports.
    #[test]
    fn bare_name_resolves_through_implicit_import_to_free_fn() {
        let prelude = Module {
            schema: SCHEMA.into(),
            name: "prelude".into(),
            imports: vec![],
            defs: vec![fn_def(
                "dbl",
                Type::Fn {
                    params: vec![Type::int()],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["n"],
                Term::Var { name: "n".into() },
            )],
        };
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "m".into(),
            imports: vec![],
            defs: vec![fn_def(
                "main",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::App {
                    callee: Box::new(Term::Var { name: "dbl".into() }),
                    args: vec![Term::Lit { lit: Literal::Int { value: 5 } }],
                    tail: false,
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("prelude".into(), prelude);
        modules.insert("m".into(), consumer);
        let ws = Workspace {
            entry: "m".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(
            diags.is_empty(),
            "expected bare `dbl` to resolve through implicit prelude import; got {diags:?}"
        );
    }
}