//! 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};

/// 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(),
            },
            Type::Forall { vars, body } => Type::Forall {
                vars: vars.clone(),
                body: Box::new(self.apply(body)),
            },
        }
    }
}

/// Replaces every var named in `vars` inside `body` with a fresh metavar.
/// Used at use sites to instantiate a `Forall` type. Returns the
/// instantiated body and the parallel list of fresh metavars (one per
/// forall var, same order) — useful for codegen monomorphisation.
fn instantiate(forall_vars: &[String], body: &Type, counter: &mut u32) -> (Vec<Type>, Type) {
    let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
    let mut metas: Vec<Type> = Vec::with_capacity(forall_vars.len());
    for v in forall_vars {
        let m = Subst::fresh(counter);
        mapping.insert(v.clone(), m.clone());
        metas.push(m);
    }
    (metas, substitute_rigids(body, &mapping))
}

/// Substitutes named rigid vars throughout a type (used by
/// `instantiate`). Unlike `Subst::apply`, this targets vars by name —
/// it has no notion of metavar ids.
fn substitute_rigids(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
    match t {
        Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()),
        Type::Con { 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(),
        },
        Type::Forall { vars, body } => {
            // Inner forall shadows: only substitute vars not re-bound here.
            let inner: BTreeMap<String, Type> = mapping
                .iter()
                .filter(|(k, _)| !vars.contains(k))
                .map(|(k, v)| (k.clone(), v.clone()))
                .collect();
            Type::Forall {
                vars: vars.clone(),
                body: Box::new(substitute_rigids(body, &inner)),
            }
        }
    }
}

/// Returns true if metavar `id` occurs in `t` (after applying the
/// current substitution). Used as the occurs check during unification.
fn occurs(id: u32, t: &Type, subst: &Subst) -> bool {
    let t = subst.apply(t);
    match &t {
        Type::Var { name } => Subst::meta_id(name) == Some(id),
        Type::Con { 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 use diagnostic::{Diagnostic, Severity};

/// 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 not in [`Env::ctor_index`]. 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::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 non-`Var`/non-`Wild` sub-pattern. The
    /// MVP forbids decision-tree lowering of nested patterns. 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 15a: a bare `Pattern::Ctor.ctor` did not resolve against the
    /// current module's `ctor_index` and resolved against ctors in two
    /// or more imported modules. The author must qualify the scrutinee
    /// type so that ctor lookup is unambiguous (e.g. write
    /// `(con std_maybe.Maybe (con Int))` for the scrutinee). Code:
    /// `ambiguous-ctor`. `ctx`: `{"ctor": "<n>", "candidates": ["m1.T", "m2.T"]}`.
    #[error("ambiguous constructor `{ctor}`: declared in {candidates:?}")]
    AmbiguousCtor {
        ctor: String,
        candidates: Vec<String>,
    },
}

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::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::AmbiguousCtor { .. } => "ambiguous-ctor",
        }
    }

    /// 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::AmbiguousCtor { ctor, candidates } => {
                serde_json::json!({"ctor": ctor, "candidates": candidates})
            }
            _ => 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);
        }
        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> {
    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("."),
    };
    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> {
    // 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];
        for e in check_in_workspace(m, ws, &module_globals) {
            diagnostics.push(e.to_diagnostic());
        }
    }
    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> {
    // 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("."),
    };
    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).
    let mut symbols = IndexMap::new();
    for def in &m.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![],
            },
        };
        symbols.insert(def.name().to_string(), (ty, h));
    }
    Ok(CheckedModule { symbols })
}

/// 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.
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
}

/// 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.
fn build_module_globals(
    ws: &Workspace,
) -> Result<BTreeMap<String, IndexMap<String, Type>>> {
    let mut out: BTreeMap<String, IndexMap<String, Type>> = BTreeMap::new();
    for (mname, m) in &ws.modules {
        let mut globals = IndexMap::new();
        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(),
                    }),
                ));
            }
            if globals.contains_key(def_name) {
                return Err(CheckError::Def(
                    def_name.to_string(),
                    Box::new(CheckError::DuplicateDef(def_name.to_string())),
                ));
            }
            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![],
                },
            };
            globals.insert(def_name.to_string(), ty);
        }
        out.insert(mname.clone(), globals);
    }
    Ok(out)
}

/// 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, IndexMap<String, Type>>,
) -> Vec<CheckError> {
    let mut env = Env::new();
    builtins::install(&mut env);
    let mut errors: Vec<CheckError> = Vec::new();

    // Register type defs (local per module; cross-module ADT sharing is
    // explicitly not part of 5b).
    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());
        }
    }

    // Take local globals from the previously built table.
    if let Some(g) = module_globals.get(&m.name) {
        for (n, t) in g {
            env.globals.insert(n.clone(), t.clone());
        }
    }

    // Build import map: alias (or module name, if without alias) →
    // module name. Conflicts are not allowed in the MVP: the same `as`
    // clause twice would stand out and should surface as a duplicate
    // symbol name — currently "last wins", because Iter 5b doesn't
    // introduce a dedicated diagnostic for it; if needed later →
    // `ambiguous-import` code.
    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());
    }
    env.imports = import_map;
    env.module_globals = module_globals.clone();
    env.module_types = build_module_types(ws);
    env.current_module = m.name.clone();
    // Workspace isn't directly needed in the env; cross-module lookup uses
    // only `module_globals`. But we keep the ws reference in the
    // comment as a reminder, in case cross-module ADTs are added later.
    let _ = ws;

    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),
    }
}

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 = matches!(name.as_str(), "Int" | "Bool" | "Unit" | "Str");
            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, 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;
    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter)?;
    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()));
        }
    }
    Ok(())
}

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

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;
    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter)?;
    unify(&c.ty, &v, &mut subst)?;
    if !effects.is_empty() {
        return Err(CheckError::ConstHasEffects(
            c.name.clone(),
            effects.into_iter().collect(),
        ));
    }
    Ok(())
}

fn synth(
    t: &Term,
    env: &Env,
    locals: &mut IndexMap<String, Type>,
    effects: &mut BTreeSet<String>,
    in_def: &str,
    subst: &mut Subst,
    counter: &mut u32,
) -> Result<Type> {
    match t {
        Term::Lit { lit } => Ok(match lit {
            Literal::Int { .. } => Type::int(),
            Literal::Bool { .. } => Type::bool_(),
            Literal::Str { .. } => Type::str_(),
            Literal::Unit => Type::unit(),
        }),
        Term::Var { name } => {
            // Lookup precedence: locals → local globals → qualified
            // cross-module ref. A `Forall` resolved at any of these
            // levels is instantiated with fresh metavars at the use
            // site (textbook ML rule); rigid vars and concrete types
            // pass through unchanged.
            let raw = if let Some(t) = locals.get(name) {
                t.clone()
            } else if let Some(t) = env.globals.get(name) {
                t.clone()
            } else if name.matches('.').count() == 1 {
                let (prefix, suffix) = name.split_once('.').expect("checked");
                let target_module = match env.imports.get(prefix) {
                    Some(m) => m.clone(),
                    None => {
                        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();
                qualify_local_types(&raw_ty, &target_module, &owner_types)
            } else {
                return Err(CheckError::UnknownIdent(name.clone()));
            };
            Ok(maybe_instantiate(raw, counter))
        }
        Term::App { callee, args, .. } => {
            let cty = synth(callee, env, locals, effects, in_def, subst, counter)?;
            let cty = subst.apply(&cty);
            let (params, ret, fx) = match &cty {
                Type::Fn { params, ret, effects: fx } => {
                    (params.clone(), (**ret).clone(), fx.clone())
                }
                Type::Forall { vars, body } => {
                    // Defensive — Var should already have instantiated.
                    let (_, body) = instantiate(vars, body, counter);
                    match &body {
                        Type::Fn { params, ret, effects: fx } => {
                            (params.clone(), (**ret).clone(), fx.clone())
                        }
                        other => {
                            return Err(CheckError::NotAFunction(
                                callee_name(callee),
                                ailang_core::pretty::type_to_string(other),
                            ));
                        }
                    }
                }
                other => {
                    return Err(CheckError::NotAFunction(
                        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)?;
                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)?;
            let prev = locals.insert(name.clone(), v);
            let r = synth(body, env, locals, effects, in_def, subst, counter)?;
            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)?;
            unify(&Type::bool_(), &c, subst)?;
            let t1 = synth(then, env, locals, effects, in_def, subst, counter)?;
            let t2 = synth(else_, env, locals, effects, in_def, subst, counter)?;
            unify(&t1, &t2, subst)?;
            Ok(subst.apply(&t1))
        }
        Term::Do { op, args, .. } => {
            let sig = env
                .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)?;
                unify(exp, &actual, subst)?;
            }
            effects.insert(sig.effect.clone());
            Ok(sig.ret)
        }
        Term::Ctor { type_name, ctor, args } => {
            // Iter 15a: a qualified `type_name` (`module.Type`) resolves
            // through the import map; the ctor name stays bare and is
            // looked up inside the resolved TypeDef. The bare-name path
            // is the original Iter 13 behaviour.
            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(),
                        });
                    }
                };
                env.module_types
                    .get(&target_module)
                    .and_then(|tys| tys.get(suffix))
                    .cloned()
                    .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?
            } else {
                env.types
                    .get(type_name)
                    .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?
                    .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 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(cdef.fields.iter()) {
                let exp_inst = substitute_rigids(exp, &mapping);
                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
                unify(&exp_inst, &actual, subst)?;
            }
            Ok(Type::Con {
                name: type_name.clone(),
                args: type_args,
            })
        }
        Term::Match { scrutinee, arms } => {
            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter)?;
            if arms.is_empty() {
                return Err(CheckError::NonExhaustive {
                    ty: ailang_core::pretty::type_to_string(&s_ty),
                    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)?;
                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)?;
            unify(&Type::unit(), &lty, subst)?;
            synth(rhs, env, locals, effects, in_def, subst, counter)
        }
        Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
            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);
            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(),
            })
        }
    }
}

/// If `t` is a `Forall`, instantiate it with fresh metavars; otherwise
/// pass through unchanged. Used at every var-resolution site.
fn maybe_instantiate(t: Type, counter: &mut u32) -> Type {
    if let Type::Forall { vars, body } = &t {
        let (_, inst) = instantiate(vars, body, counter);
        inst
    } else {
        t
    }
}

/// 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 matches!(name.as_str(), "Int" | "Bool" | "Unit" | "Str") {
                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(),
        },
        Type::Forall { vars, body } => Type::Forall {
            vars: vars.clone(),
            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(),
            };
            expect_eq(expected, &lt)?;
            Ok(vec![])
        }
        Pattern::Ctor { ctor, fields } => {
            // MVP: sub-patterns of ctor patterns may only be `Var` or `Wild`.
            // Nested ctor or lit patterns need decision-tree lowering,
            // which we don't have in codegen yet.
            for sub in fields {
                if !matches!(sub, Pattern::Var { .. } | Pattern::Wild) {
                    return Err(CheckError::NestedCtorPatternNotAllowed(ctor.clone()));
                }
            }
            // Iter 15a: try local ctor_index first; if the bare name
            // doesn't resolve locally, fall back to scanning imported
            // modules' type defs. The fallback lookup keys on the
            // `module.Type` form so it lines up with what the typechecker
            // produces for qualified `Term::Ctor`s. Multiple imported
            // candidates → `ambiguous-ctor` (local always wins on
            // conflict, hence the "imported only if local missing" order).
            let resolved_type_name: String;
            let resolved_td: TypeDef;
            if let Some(cref) = env.ctor_index.get(ctor) {
                resolved_type_name = cref.type_name.clone();
                resolved_td = env.types[&cref.type_name].clone();
            } else {
                let mut hits: Vec<(String, TypeDef)> = Vec::new();
                for imp in env.imports.values() {
                    if let Some(tys) = env.module_types.get(imp) {
                        for (tname, td) in tys {
                            if td.ctors.iter().any(|c| &c.name == ctor) {
                                hits.push((format!("{imp}.{tname}"), td.clone()));
                            }
                        }
                    }
                }
                match hits.len() {
                    0 => return Err(CheckError::UnknownCtorInPattern(ctor.clone())),
                    1 => {
                        let (qname, td) = hits.into_iter().next().expect("len == 1");
                        resolved_type_name = qname;
                        resolved_td = td;
                    }
                    _ => {
                        return Err(CheckError::AmbiguousCtor {
                            ctor: ctor.clone(),
                            candidates: hits.into_iter().map(|(q, _)| q).collect(),
                        });
                    }
                }
            }
            // expected must be this ADT. For parameterised ADTs, capture
            // the type-args so we can substitute them into the cdef's
            // field types when binding sub-patterns.
            let scrutinee_args: Vec<Type> = match expected {
                Type::Con { name, args } if name == &resolved_type_name => 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)
                .expect("indexed ctor exists");
            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`).
            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(cdef.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.
    /// `check_in_workspace` populates this from `build_module_globals`.
    pub module_globals: BTreeMap<String, IndexMap<String, Type>>,
    /// 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>,
}

/// 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 {
    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,
            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![],
                },
                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![],
                },
                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
                },
                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![],
                },
                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,
                }),
                fn_def(
                    "f",
                    Type::Fn {
                        params: vec![Type::Con { name: "Maybe".into(), args: vec![] }],
                        ret: Box::new(Type::int()),
                        effects: vec![],
                    },
                    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,
                }),
                fn_def(
                    "f",
                    Type::Fn {
                        params: vec![Type::Con { name: "Maybe".into(), args: vec![] }],
                        ret: Box::new(Type::int()),
                        effects: vec![],
                    },
                    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![],
                },
                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()],
                    body: Box::new(Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        ret: Box::new(Type::Var { name: "a".into() }),
                        effects: vec![],
                    }),
                },
                vec!["x"],
                Term::Var { name: "x".into() },
            )],
        };
        check(&m).expect("polymorphic id should typecheck");
    }

    /// Iter 12a: `id` instantiates fresh metavars at each use site.
    /// Calling `id(42)` produces an `Int`; calling `id(true)` would
    /// produce a `Bool`. Two distinct uses must not bleed into each
    /// other (each gets its own metavar).
    #[test]
    fn polymorphic_id_can_be_used_at_int_and_bool() {
        let id_def = fn_def(
            "id",
            Type::Forall {
                vars: vec!["a".into()],
                body: Box::new(Type::Fn {
                    params: vec![Type::Var { name: "a".into() }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                }),
            },
            vec!["x"],
            Term::Var { name: "x".into() },
        );
        // `use_int` returns id(42) :: Int.
        let use_int = fn_def(
            "use_int",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::int()),
                effects: vec![],
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
                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![],
            },
            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()],
                body: Box::new(Type::Fn {
                    params: vec![Type::Var { name: "a".into() }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                }),
            },
            vec!["x"],
            Term::Var { name: "x".into() },
        );
        // Returns id(42) but declared Bool — must fail.
        let bad = fn_def(
            "bad",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::bool_()),
                effects: vec![],
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
                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()],
                body: Box::new(Type::Fn {
                    params: vec![
                        Type::Fn {
                            params: vec![Type::Var { name: "a".into() }],
                            ret: Box::new(Type::Var { name: "b".into() }),
                            effects: vec![],
                        },
                        Type::Var { name: "a".into() },
                    ],
                    ret: Box::new(Type::Var { name: "b".into() }),
                    effects: vec![],
                }),
            },
            vec!["f", "x"],
            Term::App {
                callee: Box::new(Term::Var { name: "f".into() }),
                args: vec![Term::Var { name: "x".into() }],
                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![],
            },
            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![],
            },
            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,
        });
        // 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![],
            },
            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,
        });
        let unbox = Def::Fn(FnDef {
            name: "unbox".into(),
            ty: Type::Forall {
                vars: vec!["a".into()],
                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![],
                }),
            },
            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() },
                }],
            },
            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![],
            },
            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![],
            },
            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,
        });
        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![],
            },
            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![],
                },
                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,
                }),
                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![],
                    },
                    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 {
        // `lib` declares `data Box a = MkBox(a)` and `data Bag a = Pack(a)`.
        // The second type lets us exercise ambiguous-ctor in dedicated tests.
        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,
                }),
                Def::Type(TypeDef {
                    name: "Bag".into(),
                    vars: vec!["a".into()],
                    ctors: vec![Ctor {
                        name: "Pack".into(),
                        fields: vec![Type::Var { name: "a".into() }],
                    }],
                    doc: None,
                }),
            ],
        };
        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("."),
        }
    }

    /// 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![],
                },
                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![],
                },
                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, path 3: a bare `Pattern::Ctor.ctor` falls back through
    /// imports when the ctor isn't local. The scrutinee carries the
    /// qualified type so the pattern check finds the right ADT.
    #[test]
    fn cross_module_pat_ctor_fallback_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![],
                },
                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 15a, path 4: a bare ctor name that resolves in two
    /// imported modules surfaces as `ambiguous-ctor` with both
    /// candidates listed.
    #[test]
    fn cross_module_pat_ctor_ambiguous_errors() {
        // Two different libs, each declaring a ctor `Mk` (intentional clash).
        let lib_a = Module {
            schema: SCHEMA.into(),
            name: "lib_a".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "TA".into(),
                vars: vec![],
                ctors: vec![Ctor { name: "Mk".into(), fields: vec![] }],
                doc: None,
            })],
        };
        let lib_b = Module {
            schema: SCHEMA.into(),
            name: "lib_b".into(),
            imports: vec![],
            defs: vec![Def::Type(TypeDef {
                name: "TB".into(),
                vars: vec![],
                ctors: vec![Ctor { name: "Mk".into(), fields: vec![] }],
                doc: None,
            })],
        };
        let consumer = Module {
            schema: SCHEMA.into(),
            name: "use_both".into(),
            imports: vec![
                Import { module: "lib_a".into(), alias: None },
                Import { module: "lib_b".into(), alias: None },
            ],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![Type::Con {
                        name: "lib_a.TA".into(),
                        args: vec![],
                    }],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                },
                vec!["t"],
                Term::Match {
                    scrutinee: Box::new(Term::Var { name: "t".into() }),
                    arms: vec![Arm {
                        // Bare `Mk` is ambiguous between lib_a and lib_b.
                        pat: Pattern::Ctor {
                            ctor: "Mk".into(),
                            fields: vec![],
                        },
                        body: Term::Lit { lit: Literal::Int { value: 0 } },
                    }],
                },
            )],
        };
        let mut modules = BTreeMap::new();
        modules.insert("lib_a".into(), lib_a);
        modules.insert("lib_b".into(), lib_b);
        modules.insert("use_both".into(), consumer);
        let ws = Workspace {
            entry: "use_both".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
        };
        let diags = check_workspace(&ws);
        assert!(
            diags.iter().any(|d| d.code == "ambiguous-ctor"),
            "expected ambiguous-ctor diagnostic; got {diags:?}"
        );
    }

    /// 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,
                }),
                fn_def(
                    "drain",
                    Type::Fn {
                        params: vec![Type::Con { name: "L".into(), args: vec![] }],
                        ret: Box::new(Type::unit()),
                        effects: vec!["IO".into()],
                    },
                    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");
    }
}