//! Typechecker for AILang (MVP).
//!
//! Sits between `ailang-core` (AST + canonical JSON + content hash) and
//! `ailang-codegen` (LLVM IR emit) in the pipeline `core → check →
//! codegen → ail`. Top-level entry points: [`check_module`] (one module,
//! returns [`Diagnostic`]s), [`check_workspace`] (multi-module), and
//! [`check`] (single-error legacy form returning a [`CheckedModule`]).
//!
//! HM with explicit top-level polymorphism. All top-level defs must carry
//! their full type annotation; lambda bodies inside defs are checked
//! monomorphically against their declared types. Polymorphism is opt-in
//! via `Type::Forall { vars, body }` at top-level def types and is
//! instantiated at every use site (the textbook ML rule).
//!
//! Effects are propagated as a set and reconciled against the annotation
//! on the function type.
//!
//! Built-in operations are resolved via the [`builtins`] table installed
//! into every fresh [`Env`].
//!
//! ## Internals
//!
//! Type variables come in two flavours during checking:
//! - **Rigid vars** — universally quantified vars from a `Forall` that
//!   end up in scope while checking a polymorphic def's body. They are
//!   `Type::Var { name: "<name>" }` where `<name>` is the source-level
//!   name (`a`, `b`, ...). They unify only with themselves.
//! - **Metavars** — fresh placeholders for instantiated forall vars at
//!   use sites. Encoded inside the existing `Type::Var` as
//!   `Type::Var { name: "$m<id>" }`. The naming convention keeps the AST
//!   schema untouched (no new variant, hashes stay stable). Source-level
//!   names cannot collide with the `$m` prefix because identifiers may
//!   not start with `$`.

use ailang_core::ast::*;
use ailang_core::Workspace;
use indexmap::IndexMap;
use std::collections::{BTreeMap, BTreeSet};

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

/// Metavariable substitution. Maps fresh metavar ids (from `$m<id>` in
/// `Type::Var.name`) to the type they have been unified against.
#[derive(Debug, Default, Clone)]
pub struct Subst {
    map: BTreeMap<u32, Type>,
}

impl Subst {
    /// Allocates a fresh metavar. The counter is owned by the caller so
    /// that ids stay deterministic across `synth` calls within one
    /// def-check.
    fn fresh(counter: &mut u32) -> Type {
        let id = *counter;
        *counter += 1;
        Type::Var { name: format!("$m{id}") }
    }

    /// `Some(id)` iff the var name is the metavar encoding `$m<id>`.
    fn meta_id(name: &str) -> Option<u32> {
        name.strip_prefix("$m").and_then(|s| s.parse::<u32>().ok())
    }

    fn lookup(&self, id: u32) -> Option<&Type> {
        self.map.get(&id)
    }

    fn extend(&mut self, id: u32, t: Type) {
        self.map.insert(id, t);
    }

    /// Walks `t`, replacing every metavar with its current binding (if
    /// any) — recursively so chains collapse. Rigid vars and concrete
    /// types pass through unchanged.
    pub fn apply(&self, t: &Type) -> Type {
        match t {
            Type::Var { name } => {
                if let Some(id) = Self::meta_id(name) {
                    if let Some(bound) = self.lookup(id) {
                        return self.apply(&bound.clone());
                    }
                }
                Type::Var { name: name.clone() }
            }
            Type::Con { name, args } => Type::Con {
                name: name.clone(),
                args: args.iter().map(|a| self.apply(a)).collect(),
            },
            Type::Fn { params, ret, effects, .. } => Type::Fn {
                params: params.iter().map(|p| self.apply(p)).collect(),
                ret: Box::new(self.apply(ret)),
                effects: effects.clone(),
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            Type::Forall { vars, 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(),
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        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 mod lift;

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

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

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

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

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

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

    /// Iter 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>,
    },

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

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

impl CheckError {
    /// Stable kebab-case code for machine consumption (`ail check --json`).
    /// Passed through recursively via the `Def` wrapping — the inner error
    /// carries the actual code, the wrapper only the def context.
    pub fn code(&self) -> &'static str {
        match self {
            CheckError::Def(_, inner) => inner.code(),
            CheckError::TypeMismatch { .. } => "type-mismatch",
            CheckError::UnknownIdent(_) => "unbound-var",
            CheckError::UnknownEffectOp(_) => "unknown-effect-op",
            CheckError::NotAFunction(..) => "not-a-function",
            CheckError::ArityMismatch { .. } => "arity-mismatch",
            CheckError::UndeclaredEffect(_) => "undeclared-effect",
            CheckError::FnTypeRequired(..) => "fn-type-required",
            CheckError::ParamCountMismatch { .. } => "param-count-mismatch",
            CheckError::PolymorphicNotSupported(_) => "polymorphic-not-supported",
            CheckError::ConstHasEffects(..) => "const-has-effects",
            CheckError::UnknownType(_) => "unknown-type",
            CheckError::UnknownCtor { .. } => "unknown-ctor",
            CheckError::UnknownCtorInPattern(_) => "unknown-ctor-in-pattern",
            CheckError::CtorArity { .. } => "arity-mismatch",
            CheckError::NonExhaustive { .. } => "non-exhaustive-match",
            CheckError::PrimitiveNeedsWildcard(_) => "primitive-needs-wildcard",
            CheckError::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",
            CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
        }
    }

    /// 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})
            }
            CheckError::ReuseAsNonAllocatingBody { got, .. } => {
                serde_json::json!({"got": got})
            }
            _ => serde_json::Value::Object(serde_json::Map::new()),
        }
    }

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

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

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

    /// Lowers this error into the public [`Diagnostic`] shape consumed
    /// by `ail check --json`. Pulls `code`, `message`, and `ctx` through
    /// the recursive accessors and attaches the optional def name from
    /// any wrapping [`CheckError::Def`].
    pub fn to_diagnostic(&self) -> Diagnostic {
        let mut d = Diagnostic::error(self.code(), self.message()).with_ctx(self.ctx());
        if let Some(name) = self.def() {
            d = d.with_def(name);
        }
        // Iter 18d.1: typecheck-side suggested_rewrites for the
        // reuse-as-non-allocating-body diagnostic. The replacement is
        // simply the body without the `(reuse-as ...)` wrapper — the
        // hint is meaningless here, so drop it.
        if let CheckError::ReuseAsNonAllocatingBody { body_form_a, .. } = self.inner() {
            d = d.with_suggested_rewrite(
                "drop the meaningless reuse-as wrapper around the non-allocating body",
                body_form_a.clone(),
            );
        }
        d
    }
}

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

/// Top-level API for cross-module typecheck.
///
/// Iterates over all modules of the workspace and checks each with access
/// to the top-level symbol tables of all other modules. Qualified
/// references are resolved via the import map of the respective module:
/// `Term::Var { name }` with exactly one dot in the name is interpreted
/// as `<prefix>.<def>`; `<prefix>` is an import alias (or the module name,
/// if imported without an alias).
///
/// Multi-diagnose: pass-2 collects diagnostics per def across all modules.
/// Pass-1 (symbol table) stays fail-fast — see [`check_module`].
/// Module iteration order is deterministic: entry first, then the rest in
/// BTreeMap order, so output ordering is stable.
pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
    // Iter 16a: desugar every module of the workspace before any check
    // logic runs. The rewrite is pure and per-module; we rebuild a
    // workspace shell around the desugared modules (paths and entry
    // are unchanged).
    let ws_owned = Workspace {
        entry: ws.entry.clone(),
        modules: ws
            .modules
            .iter()
            .map(|(k, m)| (k.clone(), ailang_core::desugar::desugar_module(m)))
            .collect(),
        root_dir: ws.root_dir.clone(),
        // Iter 22b.1: pass the registry through unchanged. The desugar
        // pass does not touch class/instance defs (see desugar.rs:
        // 22b.1 passthrough), so the registry built at load time
        // remains valid against the desugared modules.
        registry: ws.registry.clone(),
    };
    let ws = &ws_owned;
    // Pass 1: build per-module top-level symbol table — without checking
    // bodies. This lets module A access defs from module B even when B
    // comes later in the BTreeMap. Duplicate def names and dot-in-def
    // names are reported here immediately, because without clean symbol
    // tables all further diagnostics would be unreliable.
    let module_globals = match build_module_globals(ws) {
        Ok(g) => g,
        Err(e) => return vec![e.to_diagnostic()],
    };

    // Pass 2: body-check per module. `check_in_workspace` builds the env
    // with additional cross-module globals and an import map. Errors
    // accumulate across modules.
    let mut order: Vec<&String> = Vec::new();
    if ws.modules.contains_key(&ws.entry) {
        order.push(&ws.entry);
    }
    for name in ws.modules.keys() {
        if name != &ws.entry {
            order.push(name);
        }
    }
    let mut diagnostics: Vec<Diagnostic> = Vec::new();
    for name in order {
        let m = &ws.modules[name];
        let typecheck_errors = check_in_workspace(m, ws, &module_globals);
        let had_typecheck_errors = !typecheck_errors.is_empty();
        // Per-module diagnostic accumulator. The suppress filter
        // (Iter 19b) runs at the end of the per-module block, so
        // we keep this module's diagnostics in their own vec while
        // accumulating, then merge into the workspace-wide list.
        let mut module_diags: Vec<Diagnostic> = Vec::new();
        for e in typecheck_errors {
            module_diags.push(e.to_diagnostic());
        }
        // Iter 18c.2: linearity check runs only on modules that
        // typechecked clean. Running it on a body that already has a
        // type error would wade into a partly-defined IR (e.g.
        // unresolved Var lookups, mismatched ctor arities) and produce
        // noise. Cleanly-typechecked modules with at least one
        // all-explicit-mode fn are exactly the surface the check is
        // designed to inspect.
        if !had_typecheck_errors {
            module_diags.extend(linearity::check_module(m));
            // Iter 18d.2: reuse-as shape compatibility check. Runs on
            // the same activation gate as linearity (all-explicit-mode
            // fns only). The check resolves each `(reuse-as <var>
            // <body-ctor>)` site against the path-ctor of `<var>` and
            // rejects mismatches with `reuse-as-shape-mismatch`. Runs
            // after linearity so its output appears after linearity's
            // diagnostics for the same def — stable ordering for the
            // JSON consumer.
            module_diags.extend(reuse_shape::check_module(m));
        }
        // Iter 19b: apply per-fn `suppress` filter. Runs after every
        // diagnostic source has appended so any code the author
        // listed can actually be matched. Drops matching diagnostics
        // and pushes `empty-suppress-reason` (Error) for malformed
        // entries. See [`crate::suppress_filter`] for details.
        suppress_filter::apply(m, &mut module_diags);
        diagnostics.extend(module_diags);
    }
    diagnostics
}

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

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

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

/// Iter 15a: builds the ADT type-def table per module. Sibling of
/// [`build_module_globals`]: gives the body checker O(1) lookup of any
/// type declared anywhere in the workspace, keyed by module name.
/// Read by qualified `Type::Con.name` resolution
/// (`module.Type`), qualified `Term::Ctor.type_name`, and the
/// cross-module `Pattern::Ctor` fallback. Duplicate type / ctor errors
/// inside a single module surface during the per-module body-check
/// phase, not here.
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![],
                },
                // Iter 22b.1: class/instance defs do not contribute
                // monomorphic globals to the workspace symbol table
                // before 22b.3 monomorphisation runs. Skip them here.
                Def::Class(_) | Def::Instance(_) => continue,
            };
            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),
        // Iter 22b.1: schema-only landing for class/instance defs.
        // Class-schema validation (KindMismatch, InvalidSuperclassParam,
        // ConstraintReferencesUnboundTypeVar) and instance-body
        // typechecking (with class-method substitution) land in 22b.2.
        // Workspace-load coherence checks (Orphan / Duplicate /
        // MissingMethod) already fire from `workspace::build_registry`,
        // so a malformed instance never reaches this point.
        Def::Class(_) | Def::Instance(_) => Ok(()),
    }
}

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

fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
    match t {
        Type::Con { name, args } => {
            let is_primitive = 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)
        }
        Term::LetRec { body, in_term, .. } => {
            // Iter 16b.3: `Term::LetRec` may now survive the desugar
            // pass (when it captures `Term::Let`-bound names whose
            // types are only known after typecheck). The body is the
            // body of a fn-typed binding; the recursive name is what
            // gets tail-called, so `body` is NOT in tail position. The
            // in-clause IS in tail position iff the enclosing context
            // is — same propagation rule as `Term::Let.body`.
            verify_tail_positions(body, false)?;
            verify_tail_positions(in_term, is_tail)
        }
        Term::Clone { value } => {
            // Iter 18c.1: clone is identity. Tail-position propagates
            // through unchanged — `(clone tail-call)` is a tail call.
            verify_tail_positions(value, is_tail)
        }
        Term::ReuseAs { source, body } => {
            // Iter 18d.1: reuse-as is identity at codegen. The `source`
            // is a side-effect-free Var in shipping fixtures, so it is
            // not a tail call; the `body` is the value of the whole
            // expression and inherits the enclosing tail position.
            verify_tail_positions(source, false)?;
            verify_tail_positions(body, is_tail)
        }
    }
}

fn check_const(c: &ConstDef, env: &Env) -> Result<()> {
    // Const types are never polymorphic — a Forall here is rejected
    // outright. Any other type passes through to `synth` as before.
    if matches!(&c.ty, Type::Forall { .. }) {
        return Err(CheckError::PolymorphicNotSupported(c.name.clone()));
    }
    let mut locals = IndexMap::new();
    let mut effects = BTreeSet::new();
    let mut subst = Subst::default();
    let mut counter: u32 = 0;
    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(())
}

pub(crate) fn synth(
    t: &Term,
    env: &Env,
    locals: &mut IndexMap<String, Type>,
    effects: &mut BTreeSet<String>,
    in_def: &str,
    subst: &mut Subst,
    counter: &mut u32,
) -> 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.
            //
            // Iter 15b: when the type is cross-module, `cdef.fields` is
            // written in the owning module's local namespace. A recursive
            // self-reference like `Cons a (List a)` carries `Con
            // { name: "List" }` even though, from the consumer's view,
            // the type is `std_list.List`. Apply `qualify_local_types`
            // with the owning module so that recursive ctor field types
            // (and any other locally-named cross-module type-cons) are
            // qualified before substitution / unification.
            let owning_module: Option<String>;
            let td = if type_name.matches('.').count() == 1 {
                let (prefix, suffix) = type_name.split_once('.').expect("checked");
                let target_module = match env.imports.get(prefix) {
                    Some(m) => m.clone(),
                    None => {
                        return Err(CheckError::UnknownModule {
                            module: prefix.to_string(),
                        });
                    }
                };
                let td = env.module_types
                    .get(&target_module)
                    .and_then(|tys| tys.get(suffix))
                    .cloned()
                    .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
                owning_module = Some(target_module);
                td
            } else {
                owning_module = None;
                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 15b: qualify local type-cons in the field types when
            // the ctor's owning type is cross-module. No-op when the
            // type is local (owning_module is None).
            let qualified_fields: Vec<Type> = match &owning_module {
                Some(m) => {
                    let owner_types = env
                        .module_types
                        .get(m)
                        .cloned()
                        .unwrap_or_default();
                    cdef.fields
                        .iter()
                        .map(|f| qualify_local_types(f, m, &owner_types))
                        .collect()
                }
                None => cdef.fields.clone(),
            };
            // Iter 13a: parameterised ADT — instantiate the type's vars
            // with fresh metavars, substitute them through every ctor
            // field type, and let the field types' metavars be solved by
            // unifying against the actual arg types. The result type
            // carries the same metavars as type-args, so the surrounding
            // context can pin them down.
            let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
            let mut type_args: Vec<Type> = Vec::with_capacity(td.vars.len());
            for v in &td.vars {
                let m = Subst::fresh(counter);
                mapping.insert(v.clone(), m.clone());
                type_args.push(m);
            }
            for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                let exp_inst = substitute_rigids(exp, &mapping);
                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
                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(),
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            })
        }
        Term::LetRec { name, ty, params, body, in_term } => {
            // Iter 16b.3: a `Term::LetRec` reaches `synth` only when
            // the desugar pass deferred it (some capture is
            // `Term::Let`-bound and its type is only knowable here).
            // We synthesize it as if it were a recursive fn-typed
            // local binding:
            //   1. Peel any `Forall` defensively (16b.6 still rejects
            //      Forall-typed LetRecs at desugar — this is just for
            //      shape uniformity with `check_fn`).
            //   2. Validate that `params.len() == ty.params.len()`.
            //   3. Extend `locals` with `name: ty` for the body
            //      (recursive self-reference) and each
            //      `params[i]: ty.params[i]`.
            //   4. Synth the body, unify against `ty.ret`, check
            //      effects-subset against `ty.effects`.
            //   5. Restore locals; extend with `name: ty`; synth
            //      `in_term`. Restore. Return `in_term`'s type.
            let inner_ty = match ty {
                Type::Forall { body, .. } => (**body).clone(),
                other => other.clone(),
            };
            let (param_tys, ret_ty, declared_effs) = match &inner_ty {
                Type::Fn { params: ps, ret, effects, .. } => {
                    (ps.clone(), (**ret).clone(), effects.clone())
                }
                other => {
                    return Err(CheckError::FnTypeRequired(
                        name.clone(),
                        ailang_core::pretty::type_to_string(other),
                    ));
                }
            };
            if param_tys.len() != params.len() {
                return Err(CheckError::ParamCountMismatch {
                    name: name.clone(),
                    ty_count: param_tys.len(),
                    param_count: params.len(),
                });
            }

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

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

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

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

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

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

/// 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(),
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        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 } => {
            // Iter 16a: nested **Ctor** sub-patterns are removed by
            // `ailang_core::desugar::desugar_module` before this checker
            // runs, so we only have to defend against the still-rejected
            // **Lit** sub-pattern case. The `nested-ctor-pattern-not-allowed`
            // error code is reused for that — its meaning is now narrower
            // ("non-flat: a Lit sub-pattern was found"), and the docstring
            // on the variant reflects that.
            for sub in fields {
                match sub {
                    Pattern::Var { .. } | Pattern::Wild => {}
                    Pattern::Lit { .. } => {
                        return Err(CheckError::NestedCtorPatternNotAllowed(ctor.clone()));
                    }
                    Pattern::Ctor { .. } => {
                        unreachable!(
                            "nested Ctor sub-patterns are removed by \
                             ailang_core::desugar before check"
                        );
                    }
                }
            }
            // 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).
            //
            // Iter 15b: track whether the resolved ctor lives in an
            // imported module. If so, the cdef's recursive self-references
            // need `qualify_local_types` (symmetric to the term-ctor fix);
            // otherwise their bare names will not unify against the
            // qualified scrutinee args.
            let resolved_type_name: String;
            let resolved_td: TypeDef;
            let resolved_owning_module: Option<String>;
            if let Some(cref) = env.ctor_index.get(ctor) {
                resolved_type_name = cref.type_name.clone();
                resolved_td = env.types[&cref.type_name].clone();
                resolved_owning_module = None;
            } else {
                let mut hits: Vec<(String, 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}"),
                                    imp.clone(),
                                    td.clone(),
                                ));
                            }
                        }
                    }
                }
                match hits.len() {
                    0 => return Err(CheckError::UnknownCtorInPattern(ctor.clone())),
                    1 => {
                        let (qname, owner, td) =
                            hits.into_iter().next().expect("len == 1");
                        resolved_type_name = qname;
                        resolved_td = td;
                        resolved_owning_module = Some(owner);
                    }
                    _ => {
                        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`).
            //
            // Iter 15b: when the resolved ctor lives in an imported
            // module, qualify any bare local type-cons in the field
            // types first — symmetric to the term-ctor fix.
            let qualified_fields: Vec<Type> = match &resolved_owning_module {
                Some(m) => {
                    let owner_types = env
                        .module_types
                        .get(m)
                        .cloned()
                        .unwrap_or_default();
                    cdef.fields
                        .iter()
                        .map(|f| qualify_local_types(f, m, &owner_types))
                        .collect()
                }
                None => cdef.fields.clone(),
            };
            let mapping: BTreeMap<String, Type> = td
                .vars
                .iter()
                .cloned()
                .zip(scrutinee_args)
                .collect();
            let mut out = Vec::new();
            for (sub, sub_ty) in fields.iter().zip(qualified_fields.iter()) {
                let sub_ty_inst = substitute_rigids(sub_ty, &mapping);
                out.extend(type_check_pattern(sub, &sub_ty_inst, env)?);
            }
            Ok(out)
        }
    }
}

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

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

/// Typechecker environment for a single module-check pass.
///
/// Cloned cheaply when we need a scoped extension (e.g. installing
/// rigid vars while checking a polymorphic def's body) so that the
/// parent scope stays immutable. Construction goes through
/// [`Env::default`] / the internal `new`; population is the
/// responsibility of [`builtins::install`] and the per-module setup in
/// `check_in_workspace`.
///
/// Several of the fields are conceptually disjoint name-spaces (term
/// vars vs effect ops vs ADT names vs ctor names), kept as separate
/// maps because the AST already commits to which channel a reference
/// goes through (`Term::Var` vs `Term::Do` vs `Term::Ctor` vs
/// `Pattern::Ctor`).
#[derive(Debug, Default, Clone)]
pub struct Env {
    /// Term-level names in scope — built-in operators, user fn/const
    /// defs of the current module, and (after pass-1) an entry per
    /// local def. Looked up by `Term::Var { name }` lookup.
    pub globals: IndexMap<String, Type>,
    /// Effect-op table. Looked up by `Term::Do { op }`. See
    /// [`builtins::EffectOpSig`] for the payload shape.
    pub effect_ops: IndexMap<String, builtins::EffectOpSig>,
    /// User-declared ADTs of the current module, by name. Populated
    /// from `Def::Type` entries; consulted by `Term::Ctor`,
    /// `Pattern::Ctor`, and the well-formedness check on declared
    /// types.
    pub types: IndexMap<String, TypeDef>,
    /// Inverse index: ctor name -> reference to the owning ADT.
    pub ctor_index: IndexMap<String, CtorRef>,
    /// Import map: alias-or-module-name → actual module name.
    /// Used when `Term::Var { name }` contains a dot
    /// (qualified cross-module reference).
    pub imports: BTreeMap<String, String>,
    /// Top-level symbol table per module of the workspace.
    /// `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 {
    pub(crate) fn new() -> Self {
        Self::default()
    }
}

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

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

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

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

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

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

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

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

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

    /// Iter 12a: a top-level def annotated `forall a. (a) -> a` is
    /// admitted; its body checks against a rigid type var. The
    /// var name (`a`) is in scope as a rigid throughout the body.
    #[test]
    fn polymorphic_id_def_typechecks() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "id",
                Type::Forall {
                    vars: vec!["a".into()],
                    body: Box::new(Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        ret: Box::new(Type::Var { name: "a".into() }),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    }),
                },
                vec!["x"],
                Term::Var { name: "x".into() },
            )],
        };
        check(&m).expect("polymorphic id should typecheck");
    }

    /// Iter 12a: `id` instantiates fresh metavars at each use site.
    /// Calling `id(42)` produces an `Int`; calling `id(true)` would
    /// produce a `Bool`. Two distinct uses must not bleed into each
    /// other (each gets its own metavar).
    #[test]
    fn polymorphic_id_can_be_used_at_int_and_bool() {
        let id_def = fn_def(
            "id",
            Type::Forall {
                vars: vec!["a".into()],
                body: Box::new(Type::Fn {
                    params: vec![Type::Var { name: "a".into() }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            vec!["x"],
            Term::Var { name: "x".into() },
        );
        // `use_int` returns id(42) :: Int.
        let use_int = fn_def(
            "use_int",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
                tail: false,
            },
        );
        // `use_bool` returns id(true) :: Bool.
        let use_bool = fn_def(
            "use_bool",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::bool_()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
                tail: false,
            },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![id_def, use_int, use_bool],
        };
        check(&m).expect("two distinct id instantiations should typecheck");
    }

    /// Iter 12a: a `Forall` callee at App must instantiate consistently.
    /// `id(42) :: Bool` is rejected because the metavar gets pinned to
    /// `Int` by the arg, which conflicts with the declared `Bool` ret.
    #[test]
    fn polymorphic_id_consistency_is_enforced() {
        let id_def = fn_def(
            "id",
            Type::Forall {
                vars: vec!["a".into()],
                body: Box::new(Type::Fn {
                    params: vec![Type::Var { name: "a".into() }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            vec!["x"],
            Term::Var { name: "x".into() },
        );
        // Returns id(42) but declared Bool — must fail.
        let bad = fn_def(
            "bad",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::bool_()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "id".into() }),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
                tail: false,
            },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![id_def, bad],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("type mismatch"), "got: {msg}");
    }

    /// Iter 12a: two-var polymorphism. `apply : forall a b. ((a -> b),
    /// a) -> b`. Body applies the function. We instantiate at two
    /// different use sites with different (a, b) pairs.
    #[test]
    fn polymorphic_apply_with_two_vars() {
        let apply_def = fn_def(
            "apply",
            Type::Forall {
                vars: vec!["a".into(), "b".into()],
                body: Box::new(Type::Fn {
                    params: vec![
                        Type::Fn {
                            params: vec![Type::Var { name: "a".into() }],
                            ret: Box::new(Type::Var { name: "b".into() }),
                            effects: vec![],
                            param_modes: vec![],
                            ret_mode: ParamMode::Implicit,
                        },
                        Type::Var { name: "a".into() },
                    ],
                    ret: Box::new(Type::Var { name: "b".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            vec!["f", "x"],
            Term::App {
                callee: Box::new(Term::Var { name: "f".into() }),
                args: vec![Term::Var { name: "x".into() }],
                tail: false,
            },
        );
        // A monomorphic helper to be passed to apply.
        let succ = fn_def(
            "succ",
            Type::Fn {
                params: vec![Type::int()],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec!["n"],
            Term::App {
                callee: Box::new(Term::Var { name: "+".into() }),
                args: vec![
                    Term::Var { name: "n".into() },
                    Term::Lit { lit: Literal::Int { value: 1 } },
                ],
                tail: false,
            },
        );
        let use_apply = fn_def(
            "use_apply",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::int()),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::App {
                callee: Box::new(Term::Var { name: "apply".into() }),
                args: vec![
                    Term::Var { name: "succ".into() },
                    Term::Lit { lit: Literal::Int { value: 41 } },
                ],
                tail: false,
            },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![apply_def, succ, use_apply],
        };
        check(&m).expect("apply instantiation should typecheck");
    }

    /// Iter 13a: parameterised ADT — `type Box[a] = MkBox(a)` is well-
    /// formed and `MkBox(42)` typechecks at result type `Box<Int>`.
    #[test]
    fn parameterised_adt_ctor_at_int() {
        let box_def = Def::Type(TypeDef {
            name: "Box".into(),
            vars: vec!["a".into()],
            ctors: vec![Ctor {
                name: "MkBox".into(),
                fields: vec![Type::Var { name: "a".into() }],
            }],
            doc: None,
            drop_iterative: false,
        });
        // fn make :: () -> Box<Int> = MkBox(42)
        let make = fn_def(
            "make",
            Type::Fn {
                params: vec![],
                ret: Box::new(Type::Con {
                    name: "Box".into(),
                    args: vec![Type::int()],
                }),
                effects: vec![],
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            },
            vec![],
            Term::Ctor {
                type_name: "Box".into(),
                ctor: "MkBox".into(),
                args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
            },
        );
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![box_def, make],
        };
        check(&m).expect("Box<Int> ctor should typecheck");
    }

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

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

    /// Iter 10: `seq` requires lhs to be Unit. A non-Unit lhs is a
    /// type error — the value of lhs gets discarded so a useful (non-
    /// Unit) value would silently vanish.
    #[test]
    fn seq_lhs_must_be_unit() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                Term::Seq {
                    lhs: Box::new(Term::Lit {
                        lit: Literal::Int { value: 7 },
                    }),
                    rhs: Box::new(Term::Lit {
                        lit: Literal::Int { value: 1 },
                    }),
                },
            )],
        };
        let err = check(&m).unwrap_err();
        let msg = format!("{err}");
        assert!(msg.contains("type mismatch"), "got: {msg}");
    }

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

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

    /// Helper for the cross-module tests: build a workspace whose entry
    /// imports `lib` and exposes its types via qualified names.
    fn cross_module_ws(consumer: Module) -> Workspace {
        // `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,
                    drop_iterative: false,
                }),
                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,
                    drop_iterative: false,
                }),
            ],
        };
        let mut modules = BTreeMap::new();
        modules.insert("lib".into(), lib);
        modules.insert(consumer.name.clone(), consumer.clone());
        Workspace {
            entry: consumer.name,
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        }
    }

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

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

    /// Iter 15a, 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![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec!["b"],
                Term::Match {
                    scrutinee: Box::new(Term::Var { name: "b".into() }),
                    arms: vec![Arm {
                        pat: Pattern::Ctor {
                            ctor: "MkBox".into(),
                            fields: vec![Pattern::Var { name: "x".into() }],
                        },
                        body: Term::Var { name: "x".into() },
                    }],
                },
            )],
        };
        let ws = cross_module_ws(consumer);
        let diags = check_workspace(&ws);
        assert!(diags.is_empty(), "expected green; got {diags:?}");
    }

    /// Iter 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,
                drop_iterative: false,
            })],
        };
        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,
                drop_iterative: false,
            })],
        };
        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![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                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("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let diags = check_workspace(&ws);
        assert!(
            diags.iter().any(|d| d.code == "ambiguous-ctor"),
            "expected ambiguous-ctor diagnostic; got {diags:?}"
        );
    }

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

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

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

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

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

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

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

    /// Iter 16e: helper that wraps `body` in a fn whose return type is
    /// `Bool`, runs `check`, and returns the diagnostics. Used by the
    /// polymorphic-`==` typecheck tests below.
    fn check_eq_body_returns_bool(body: Term) -> Vec<Diagnostic> {
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_def(
                "f",
                Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::bool_()),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                vec![],
                body,
            )],
        };
        check_module(&m)
    }

    fn eq_app(a: Term, b: Term) -> Term {
        Term::App {
            callee: Box::new(Term::Var { name: "==".into() }),
            args: vec![a, b],
            tail: false,
        }
    }

    /// Iter 16e: `==` accepts Int args (regression — the pre-16e
    /// behaviour stays identical).
    #[test]
    fn eq_typechecks_at_int() {
        let body = eq_app(
            Term::Lit { lit: Literal::Int { value: 1 } },
            Term::Lit { lit: Literal::Int { value: 2 } },
        );
        assert!(check_eq_body_returns_bool(body).is_empty());
    }

    /// Iter 16e: `==` accepts Bool args. Pre-16e this was a typecheck
    /// error because `==` was declared `(Int, Int) -> Bool`.
    #[test]
    fn eq_typechecks_at_bool() {
        let body = eq_app(
            Term::Lit { lit: Literal::Bool { value: true } },
            Term::Lit { lit: Literal::Bool { value: false } },
        );
        assert!(check_eq_body_returns_bool(body).is_empty());
    }

    /// Iter 16e: `==` accepts Str args. Same story as Bool.
    #[test]
    fn eq_typechecks_at_str() {
        let body = eq_app(
            Term::Lit { lit: Literal::Str { value: "hi".into() } },
            Term::Lit { lit: Literal::Str { value: "ho".into() } },
        );
        assert!(check_eq_body_returns_bool(body).is_empty());
    }

    /// Iter 16e: `==` accepts Unit args.
    #[test]
    fn eq_typechecks_at_unit() {
        let body = eq_app(
            Term::Lit { lit: Literal::Unit },
            Term::Lit { lit: Literal::Unit },
        );
        assert!(check_eq_body_returns_bool(body).is_empty());
    }

    /// Iter 16e: `==`'s type still demands the two sides to agree —
    /// `(== 1 true)` must fail to unify the second arg's `Bool`
    /// against the metavar already pinned to `Int` by the first.
    #[test]
    fn eq_rejects_mixed_int_bool() {
        let body = eq_app(
            Term::Lit { lit: Literal::Int { value: 1 } },
            Term::Lit { lit: Literal::Bool { value: true } },
        );
        let diags = check_eq_body_returns_bool(body);
        assert!(
            !diags.is_empty(),
            "(== 1 true) must fail to typecheck; got no diagnostics"
        );
    }

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