AILang/crates/ailang-check/src/lib.rs

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

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

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

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

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

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

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

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

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

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

/// Substitutes named rigid vars throughout a type (used by
/// `instantiate`). Unlike `Subst::apply`, this targets vars by name —
/// it has no notion of metavar ids.
pub(crate) fn substitute_rigids(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
    match t {
        Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()),
        Type::Con { name, args } => Type::Con {
            name: name.clone(),
            args: args.iter().map(|a| substitute_rigids(a, mapping)).collect(),
        },
        Type::Fn { params, param_modes, ret, ret_mode, effects } => Type::Fn {
            params: params.iter().map(|p| substitute_rigids(p, mapping)).collect(),
            ret: Box::new(substitute_rigids(ret, mapping)),
            effects: effects.clone(),
            // 2026-05-14 bugfix-print-leak-show-ret-mode: preserve
            // param_modes and ret_mode through rigid substitution.
            // The earlier `..` discarded both and hard-reset to
            // Implicit, which silently stripped the Show class
            // method's `ret_mode: Own` (declared in
            // `examples/prelude.ail.json`) when mono synthesised
            // `show__Int` via `synthesise_mono_fn`'s
            // `substitute_rigids(&class_method.ty, …)`. Codegen's
            // `is_rc_heap_allocated` App-arm then declined to track
            // print's `let s = show x` binder, leaking the heap-Str.
            param_modes: param_modes.clone(),
            ret_mode: *ret_mode,
        },
        Type::Forall { vars, constraints, body } => {
            // Inner forall shadows: only substitute vars not re-bound here.
            let inner: BTreeMap<String, Type> = mapping
                .iter()
                .filter(|(k, _)| !vars.contains(k))
                .map(|(k, v)| (k.clone(), v.clone()))
                .collect();
            Type::Forall {
                vars: vars.clone(),
                constraints: constraints.clone(),
                body: Box::new(substitute_rigids(body, &inner)),
            }
        }
    }
}

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

/// Returns true if metavar `id` occurs in `t` (after applying the
/// current substitution). Used as the occurs check during unification.
fn occurs(id: u32, t: &Type, subst: &Subst) -> bool {
    let t = subst.apply(t);
    match &t {
        Type::Var { name } => Subst::meta_id(name) == Some(id),
        Type::Con { args, .. } => args.iter().any(|a| occurs(id, a, subst)),
        Type::Fn { params, ret, .. } => {
            params.iter().any(|p| occurs(id, p, subst)) || occurs(id, ret, subst)
        }
        Type::Forall { body, .. } => occurs(id, body, subst),
    }
}

/// Unifies two types under the current substitution. Symmetric. Extends
/// the substitution as needed, with the standard occurs check.
fn unify(a: &Type, b: &Type, subst: &mut Subst) -> Result<()> {
    let a = subst.apply(a);
    let b = subst.apply(b);
    match (&a, &b) {
        // Metavar unification — bind the metavar to the other side.
        (Type::Var { name }, _) if Subst::meta_id(name).is_some() => {
            let id = Subst::meta_id(name).unwrap();
            if let Type::Var { name: bn } = &b {
                if Subst::meta_id(bn) == Some(id) {
                    return Ok(()); // same metavar, done
                }
            }
            if occurs(id, &b, subst) {
                return Err(CheckError::TypeMismatch {
                    expected: ailang_core::pretty::type_to_string(&a),
                    got: ailang_core::pretty::type_to_string(&b),
                });
            }
            subst.extend(id, b);
            Ok(())
        }
        (_, Type::Var { name }) if Subst::meta_id(name).is_some() => {
            let id = Subst::meta_id(name).unwrap();
            if occurs(id, &a, subst) {
                return Err(CheckError::TypeMismatch {
                    expected: ailang_core::pretty::type_to_string(&a),
                    got: ailang_core::pretty::type_to_string(&b),
                });
            }
            subst.extend(id, a);
            Ok(())
        }
        // Rigid vars: only unify with the same name.
        (Type::Var { name: an }, Type::Var { name: bn }) if an == bn => Ok(()),
        // Concrete con: same name and same arity, then unify args
        // pointwise. Iter 13a: parameterised ADTs unify arg-by-arg.
        (
            Type::Con { name: an, args: aa },
            Type::Con { name: bn, args: ba },
        ) if an == bn && aa.len() == ba.len() => {
            for (x, y) in aa.iter().zip(ba.iter()) {
                unify(x, y, subst)?;
            }
            Ok(())
        }
        // Function types: zip params, unify ret, effects must match as a set.
        (
            Type::Fn { params: ap, ret: ar, effects: ae, .. },
            Type::Fn { params: bp, ret: br, effects: be, .. },
        ) => {
            if ap.len() != bp.len() {
                return Err(CheckError::TypeMismatch {
                    expected: ailang_core::pretty::type_to_string(&a),
                    got: ailang_core::pretty::type_to_string(&b),
                });
            }
            for (x, y) in ap.iter().zip(bp.iter()) {
                unify(x, y, subst)?;
            }
            unify(ar, br, subst)?;
            let mut ae = ae.clone();
            let mut be = be.clone();
            ae.sort();
            be.sort();
            if ae != be {
                return Err(CheckError::TypeMismatch {
                    expected: ailang_core::pretty::type_to_string(&a),
                    got: ailang_core::pretty::type_to_string(&b),
                });
            }
            Ok(())
        }
        _ => Err(CheckError::TypeMismatch {
            expected: ailang_core::pretty::type_to_string(&a),
            got: ailang_core::pretty::type_to_string(&b),
        }),
    }
}

pub mod builtins;
pub mod diagnostic;
pub mod lift;
pub mod mono;

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

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

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

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

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

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

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

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

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

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

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

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

    /// An `(export …)` fn has a parameter or return type that is not
    /// a permitted embedding-ABI type. The embedding ABI is frozen as
    /// of M3 (design/contracts/embedding-abi.md):
    /// `Int`/`Float` or a single-constructor record of those; every
    /// other shape (multi-ctor sums, `Str`/`List`/nested-record
    /// fields) is rejected at typecheck (the feature-acceptance
    /// clause-3 discriminator, in code).
    /// Code: `export-non-scalar-signature`.
    #[error("export `{0}`: embedding ABI accepts `Int`/`Float` or a single-constructor record of those — {1} type `{2}` is not permitted (multi-constructor sums, and `Str`/`List`/nested-record fields, are a future M4 layer)")]
    ExportNonScalarSignature(String, &'static str, String),

    /// An `(export …)` fn has a non-empty effect set. An embedding
    /// kernel must be pure (a `(State,Chunk)->State` fold has no
    /// effects). Code: `export-has-effects`.
    #[error("export `{0}` must be pure — declared effects !{1:?} are not allowed on an embedding boundary")]
    ExportHasEffects(String, Vec<String>),

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    /// 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 `design/contracts/tail-calls.md`.
    #[error("call marked `tail` is not in tail position")]
    TailCallNotInTailPosition,

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

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

    /// a `FnDef` calls a class method at a
    /// fully-concrete type (e.g. `show 42` resolves the residual class
    /// param to `Int`), but the workspace registry has no
    /// `instance class at_type` entry. This is the dual of
    /// `MissingConstraint`: when the residual type is concrete, the fn
    /// cannot push the obligation to a caller via `Forall.constraints`
    /// — it can only be discharged by an existing instance. Without a
    /// matching registry entry, monomorphisation (22b.3) would have no
    /// dictionary to substitute. Code: `no-instance`. `ctx`:
    /// `{"class": "<C>", "method": "<m>", "at_type": "<T>"}`.
    #[error(
        "fn `{def}` calls `{method}` requiring `instance {class} {at_type}`, \
        but no such instance exists in the workspace"
    )]
    NoInstance {
        def: String,
        method: String,
        class: String,
        at_type: String,
        /// additive candidate-class list. Empty on residuals from
        /// the single-class dispatch path (pre-canonical-class-form shape preserved).
        /// Non-empty when the diagnostic originated from the
        /// multi-candidate refinement path with zero registry survivors.
        candidate_classes: Vec<String>,
    },

    /// a monomorphic call site `<method> x` with multiple
    /// candidate classes (each declaring `<method>` and each having an
    /// instance for `x`'s concrete type) cannot be resolved unambiguously.
    /// The LLM-author writes an explicit qualifier
    /// (`<class-qualifier>.<method> x`) to disambiguate.
    /// Code: `ambiguous-method-resolution`. `ctx`:
    /// `{"method": "<m>", "at_type": "<T>", "candidate_classes": ["<C1>", ...]}`.
    #[error(
        "method `{method}` at type `{at_type}` is ambiguous: classes \
        {candidate_classes:?} all declare it and provide an instance. \
        Disambiguate with `<ClassQualifier>.{method}`."
    )]
    AmbiguousMethodResolution {
        method: String,
        at_type: String,
        candidate_classes: Vec<String>,
    },

    /// an explicit class qualifier in `Term::Var.name` names a
    /// qualified class that is not in the workspace registry of
    /// candidate classes for the method. Code: `unknown-class`. `ctx`:
    /// `{"name": "<qualified-class>"}`.
    #[error("class `{name}` is not declared in any module of this workspace")]
    UnknownClass {
        name: String,
    },

    /// loop-recur iter loop-recur.tidy: `Term::Lam` reached typecheck
    /// inside a lexically-enclosing `Term::Loop`, and the lambda's body
    /// references a loop binder declared by that enclosing loop. Loop
    /// binders are alloca-resident (codegen reuses the
    /// `binder_allocas` registry, `std::mem::take`-emptied at the
    /// lambda frame boundary). Capturing one into a closure would
    /// require lifting it to the heap (deferred) or rejecting the
    /// capture; this milestone takes the latter route rather than
    /// panicking codegen on type-correct input.
    #[error("loop binder `{name}` cannot be captured by a lambda — loop binders are alloca-resident and do not escape their enclosing loop. Either move the lambda outside the loop, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")]
    LoopBinderCapturedByLambda { name: String },

    /// loop-recur iter 2: `Term::Recur` reached typecheck with no
    /// lexically-enclosing `Term::Loop` (the `loop_stack` was empty).
    #[error("`recur` is only valid inside a `loop` — there is no enclosing loop here")]
    RecurOutsideLoop,

    /// loop-recur iter 2: `Term::Recur`'s argument count differs from
    /// the enclosing loop's binder count. `recur` rebinds every loop
    /// binder positionally, so the counts must match exactly.
    #[error("`recur` passes {got} argument(s) but the enclosing loop has {expected} binder(s) — recur must rebind every binder positionally")]
    RecurArityMismatch { expected: usize, got: usize },

    /// loop-recur iter 2: a `recur` argument's type differs from the
    /// corresponding loop binder's declared type (0-based position).
    #[error("`recur` argument {position} has type `{got}` but the enclosing loop's binder at that position is `{expected}` — every recur argument must match its binder's type")]
    RecurTypeMismatch {
        position: usize,
        expected: String,
        got: String,
    },

    /// loop-recur iter 2: `Term::Recur` appears somewhere other than
    /// the tail position of its enclosing loop body. `recur` is a
    /// structural back-jump; it cannot be a sub-expression.
    #[error("`recur` must be in tail position of its enclosing `loop` body — it is a back-jump, not a value-producing sub-expression")]
    RecurNotInTailPosition,

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

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

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

    /// Structured context for a diagnostic. Lands directly in the JSON
    /// under the key `ctx`. Empty object when no context is available.
    pub fn ctx(&self) -> serde_json::Value {
        match self {
            CheckError::Def(_, inner) => inner.ctx(),
            CheckError::TypeMismatch { expected, got } => {
                serde_json::json!({"expected": expected, "actual": got})
            }
            CheckError::ArityMismatch { expected, got, .. } => {
                serde_json::json!({"expected": expected, "actual": got})
            }
            CheckError::CtorArity {
                expected, got, ..
            } => serde_json::json!({"expected": expected, "actual": got}),
            CheckError::ParamCountMismatch {
                ty_count,
                param_count,
                ..
            } => serde_json::json!({"expected": ty_count, "actual": param_count}),
            CheckError::NonExhaustive { missing, .. } => {
                serde_json::json!({"missing": missing})
            }
            CheckError::UnknownModule { module } => {
                serde_json::json!({"module": module})
            }
            CheckError::UnknownImport { module, name } => {
                serde_json::json!({"module": module, "name": name})
            }
            CheckError::InvalidDefName { name } => {
                serde_json::json!({"name": name, "reason": "contains-dot"})
            }
            CheckError::ReuseAsNonAllocatingBody { got, .. } => {
                serde_json::json!({"got": got})
            }
            CheckError::MissingConstraint { class, method, at_type, .. } => {
                serde_json::json!({"class": class, "method": method, "at_type": at_type})
            }
            CheckError::NoInstance { class, method, at_type, candidate_classes, .. } => {
                let mut obj = serde_json::json!({
                    "class": class,
                    "method": method,
                    "at_type": at_type,
                });
                if !candidate_classes.is_empty() {
                    obj["candidate_classes"] = serde_json::json!(candidate_classes);
                }
                obj
            }
            CheckError::AmbiguousMethodResolution { method, at_type, candidate_classes } => {
                serde_json::json!({
                    "method": method,
                    "at_type": at_type,
                    "candidate_classes": candidate_classes,
                })
            }
            CheckError::UnknownClass { name } => {
                serde_json::json!({ "name": name })
            }
            CheckError::LoopBinderCapturedByLambda { name } => {
                serde_json::json!({"name": name})
            }
            CheckError::RecurArityMismatch { expected, got } => {
                serde_json::json!({"expected": expected, "actual": got})
            }
            CheckError::RecurTypeMismatch { position, expected, got } => {
                serde_json::json!({"position": position, "expected": expected, "actual": 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);
        }
        // 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(),
            );
        }
        // Float-aware addendum on `NoInstance`. When the
        // unresolved class is `Eq` or `Ord` AND the type is `Float`,
        // append a cross-reference to design/contracts/float-semantics.md so
        // the LLM author learns the partial-Float story immediately
        // rather than seeing a bare "no instance" message. Float has
        // neither Eq nor Ord by design (partial orderability per
        // IEEE-754), and the polymorphic prelude helpers
        // (`ne` / `lt` / `le` / `gt` / `ge` / direct `eq` / `compare`)
        // are the natural surface where the LLM hits this.
        if let CheckError::NoInstance { class, at_type, .. } = self.inner() {
            // `class` carries the qualified workspace-key shape
            // (`prelude.Eq` / `prelude.Ord`), not the bare name.
            if (class == "prelude.Eq" || class == "prelude.Ord") && at_type == "Float" {
                d.message = format!(
                    "{} — Float has no Eq/Ord instance by design (partial \
                     orderability per IEEE-754); see design/contracts/float-semantics.md.",
                    d.message
                );
            } else if class == "prelude.Show" {
                // Show-aware addendum on `NoInstance`. Fires
                // for any type lacking a Show instance — most commonly
                // a function type (`print f` where f is bare-fn-typed)
                // or a user type the LLM-author forgot to give an
                // instance for. Cross-references
                // design/contracts/typeclasses.md so the author learns
                // which types ship with built-in Show immediately.
                d.message = format!(
                    "{} — `print` and `show` require a Show instance. \
                     Built-in Show ships for Int, Bool, Str, Float in \
                     the prelude; see design/contracts/typeclasses.md. \
                     User types declare their own \
                     `instance prelude.Show <T>` in the type's defining \
                     module per the typeclass design coherence.",
                    d.message
                );
            }
        }
        d
    }
}

/// Top-level API for structured diagnostics.
///
/// Empty Vec = green. From Iter 6 onwards the body-check phase is
/// multi-diagnose: each def in each module is checked independently and
/// failures accumulate, so a single `ail check` run reports every
/// independent body error in the workspace.
///
/// Pass-1 errors (top-level symbol-table construction:
/// `invalid-def-name`, `duplicate-def`) are still fail-fast — those
/// errors corrupt the symbol table, and any further diagnostic would be
/// unreliable. Likewise, the type-def installation is fail-fast within
/// a single module, but other modules continue being checked.
///
/// Backwards compatibility: a bare `&Module` is internally lifted into a
/// trivial workspace (`modules = {m.name: m}`, `entry = m.name`) so that
/// tooling checking individual modules avoids building a `Workspace`.
/// Modules with imports on other modules not present in the trivial
/// workspace will inevitably produce `unknown-module` errors on qualified
/// references — which is correct.
pub fn check_module(m: &Module) -> Vec<Diagnostic> {
    // 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("."),
        // single-module check_module entry point does not
        // build a registry. The registry is workspace-load-time
        // metadata; check_module is invoked from in-memory paths
        // (tests, single-file CLI) where no workspace DFS happened.
        // Once 22b.2 typecheck arms read the registry, those paths
        // will need to populate it from the in-memory module too.
        registry: ailang_core::workspace::Registry::default(),
    };
    check_workspace(&ws)
}

/// Top-level API for cross-module typecheck.
///
/// Iterates over all modules of the workspace and checks each with access
/// to the top-level symbol tables of all other modules. Qualified
/// references are resolved via the import map of the respective module:
/// `Term::Var { name }` with exactly one dot in the name is interpreted
/// as `<prefix>.<def>`; `<prefix>` is an import alias (or the module name,
/// if imported without an alias).
///
/// Multi-diagnose: pass-2 collects diagnostics per def across all modules.
/// Pass-1 (symbol table) stays fail-fast — see [`check_module`].
/// Module iteration order is deterministic: entry first, then the rest in
/// BTreeMap order, so output ordering is stable.
pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
    // Floats milestone post-fieldtest B1: hard-reject
    // `Pattern::Lit { Literal::Float }` before desugar rewrites lit
    // arms into `(== scrutinee lit)`. See `pre_desugar_validation`
    // for the full rationale. Walked per-def so the diagnostic
    // carries the offending def's name; modules are visited in
    // BTreeMap order, defs in declaration order. All hits in this
    // pass are accumulated and returned together (consistent with
    // pass-2 multi-diagnose); if any are present, later passes do
    // not run, since a violating Float-lit pattern would otherwise
    // be silently rewritten by desugar before typecheck.
    {
        let mut pre_desugar_errors: Vec<Diagnostic> = Vec::new();
        for m in ws.modules.values() {
            for def in &m.defs {
                if let Err(e) = pre_desugar_validation::reject_float_patterns_in_def(def) {
                    let wrapped = CheckError::Def(def.name().to_string(), Box::new(e));
                    pre_desugar_errors.push(wrapped.to_diagnostic());
                }
            }
        }
        if !pre_desugar_errors.is_empty() {
            return pre_desugar_errors;
        }
    }
    // 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(),
        // 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];
        // synth-time warnings collected per module then merged
        // into the per-module diagnostic stream alongside typecheck
        // errors. The synth warnings flow through `check_in_workspace`
        // even when `had_typecheck_errors` is true; surface them so a
        // shadowed-class-method warning is visible even when the
        // module also has unrelated errors.
        let mut synth_warnings: Vec<Diagnostic> = Vec::new();
        let typecheck_errors = check_in_workspace(m, ws, &module_globals, &mut synth_warnings);
        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());
        }
        module_diags.extend(synth_warnings);
        // 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 {
            // linearity check needs visibility into
            // polymorphic free fns + class methods from implicitly-
            // imported modules (currently just the auto-injected
            // prelude). Without this, a Borrow-mode user fn that
            // forwards its borrow params into a prelude poly fn
            // (e.g. `gt x y`) fires `consume-while-borrowed`
            // false positives because `callee_arg_modes` defaults
            // to Consume when it cannot see the callee's
            // `param_modes`. Symmetric to the class-method case
            // closed in iter 23.4-prep.
            let visible_extra: Vec<&Module> = ws
                .modules
                .iter()
                .filter_map(|(other_name, other_mod)| {
                    if other_name == name {
                        None
                    } else {
                        Some(other_mod)
                    }
                })
                .collect();
            module_diags.extend(linearity::check_module_with_visible(m, &visible_extra));
            // 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));
        }
        // apply per-fn `suppress` filter. Runs after every
        // diagnostic source has appended so any code the author
        // listed can actually be matched. Drops matching diagnostics
        // and pushes `empty-suppress-reason` (Error) for malformed
        // entries. See [`crate::suppress_filter`] for details.
        suppress_filter::apply(m, &mut module_diags);
        diagnostics.extend(module_diags);
    }
    diagnostics
}

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

/// Single-error entry point. Typechecks `m` standalone (trivial
/// workspace), returning a [`CheckedModule`] with the symbol-to-hash
/// table on success or the **first** [`CheckError`] on failure.
///
/// Prefer [`check_module`] for new callers — it returns
/// `Vec<Diagnostic>` (multi-diagnose, JSON-ready). This function is
/// kept for legacy callers (snapshot tests, the `manifest` codepath
/// that needs the hash-to-type mapping).
pub fn check(m: &Module) -> Result<CheckedModule> {
    // Floats milestone post-fieldtest B1: hard-reject
    // `Pattern::Lit { Literal::Float }` before desugar runs, because
    // `desugar::build_eq` rewrites lit-pattern arms (Float included)
    // into `(== scrutinee lit)` and would otherwise hide the
    // unreachable Float-pattern arm in `type_check_pattern`. See
    // `pre_desugar_validation` for the full rationale.
    pre_desugar_validation::reject_float_patterns_in_module(m)?;
    // 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("."),
        // 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`. Synth warnings are collected here but
    // discarded — `check`'s legacy contract returns only the first
    // error, and warnings on this path have no surface to flow to.
    let mut synth_warnings: Vec<Diagnostic> = Vec::new();
    if let Some(first) = check_in_workspace(m, &ws, &module_globals, &mut synth_warnings).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![],
            },
            // 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 })
}

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

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

/// per-module top-level symbol table. Holds the classic
/// fn/const/type-name-to-type mapping in [`Self::fns`] and class-method
/// names in [`Self::class_methods`]. The two channels are kept separate
/// because class-method resolution at a call site needs more context
/// than a plain `Type` lookup (the owning class, the class param name,
/// and the defining module — see [`ClassMethodEntry`]). Pre-22b.2 the
/// inner shape was `IndexMap<String, Type>`; 22b.2 wraps that in this
/// struct so call sites that only need fn lookup can keep using
/// `mod_globals.fns` while typeclass code goes through `class_methods`.
#[derive(Debug, Default, Clone)]
pub struct ModuleGlobals {
    /// Top-level fn / const / type symbols, by name. The pre-22b.2 inner
    /// shape — every call site that only needs HM lookup goes through
    /// here.
    pub fns: IndexMap<String, Type>,
    /// re-keyed by `(qualified-class-name, method-name)` tuple —
    /// post-retirement of `MethodNameCollision`, two classes can declare
    /// same-named methods within the same workspace. The tuple key
    /// disambiguates without losing the per-module ordering guarantee
    /// (`IndexMap` preserves insertion order). Lookups by method-name-
    /// only consult `method_to_candidate_classes` (Env-level) to get
    /// the candidate-class set, then index into `class_methods` with
    /// `(resolved_class, method)`.
    pub class_methods: IndexMap<(String, String), ClassMethodEntry>,
}

impl ModuleGlobals {
    /// True if class `class` declares a method named `name` in this
    /// module. Tuple-keyed lookup after `MethodNameCollision`
    /// retirement.
    pub fn has_class_method(&self, class: &str, name: &str) -> bool {
        self.class_methods.contains_key(&(class.to_string(), name.to_string()))
    }

    /// The class that declared the method `name` in class `class`, or
    /// `None` if no such entry exists. (Pre-canonical-class-form callers passed only the
    /// method name; post-canonical-class-form they must disambiguate by class.)
    pub fn class_method_class(&self, class: &str, name: &str) -> Option<&str> {
        self.class_methods
            .get(&(class.to_string(), name.to_string()))
            .map(|e| e.class_name.as_str())
    }

    /// The full [`ClassMethodEntry`] for method `name` in class `class`,
    /// or `None` if no such entry exists.
    pub fn class_method(&self, class: &str, name: &str) -> Option<&ClassMethodEntry> {
        self.class_methods.get(&(class.to_string(), name.to_string()))
    }

    /// enumerate all `(class, method) -> entry` pairs whose
    /// method name matches `name`. Returns zero-or-more entries —
    /// pre-canonical-class-form always at most one, post-canonical-class-form a workspace may have
    /// multiple classes declaring the same method.
    pub fn class_method_candidates(&self, name: &str) -> Vec<(&String, &ClassMethodEntry)> {
        self.class_methods
            .iter()
            .filter_map(|((c, m), e)| if m == name { Some((c, e)) } else { None })
            .collect()
    }
}

/// per-class-method metadata stored in
/// [`ModuleGlobals::class_methods`]. Carries everything the 22b.2
/// typecheck arms (`missing-constraint`, `no-instance`) need to resolve
/// a `Term::Var { name }` that refers to a class method into a residual
/// class constraint at the call site.
#[derive(Debug, Clone)]
pub struct ClassMethodEntry {
    /// The class that declared the method (e.g. `Show` for `show`).
    ///
    /// carries the qualified form `<defining_module>.<Class>`;
    /// flows downstream into `ResidualConstraint.class` and
    /// `MonoTarget::ClassMethod.class` unchanged. Match the registry
    /// key shape so discharge / mono lookups land on the right entry.
    pub class_name: String,
    /// The class's single type parameter name (e.g. `a` in
    /// `class Show a`). The class param appears at this name inside
    /// [`Self::method_ty`].
    pub class_param: String,
    /// The method's declared signature — a `Type::Fn` whose param /
    /// return positions may contain `Type::Var { name: class_param }`.
    /// Task 9 instantiates the class param with a fresh metavar at the
    /// call site to build the residual constraint.
    pub method_ty: Type,
    /// Module that declared the class. Tasks 9 / 10 use this to find
    /// the matching `Registry` entries when checking constraints.
    pub defining_module: String,
}

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

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

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

    // env.module_globals + env.class_methods — built from
    // `build_module_globals(ws)`. The .fns projection feeds
    // `module_globals`; the .class_methods entries are merged
    // workspace-wide into `class_methods` (uniqueness enforced
    // earlier by `workspace::build_registry`'s
    // method-name-collision check).
    let mg = build_module_globals(ws)
        .expect("build_module_globals: pre-condition (typecheck succeeded) violated");
    env.module_globals = mg
        .iter()
        .map(|(k, v)| (k.clone(), v.fns.clone()))
        .collect();
    for g in mg.values() {
        for ((qualified_class, method_name), e) in &g.class_methods {
            // env.class_methods is tuple-keyed by
            // `(qualified-class, method-name)`. Multiple classes may
            // share a method name post-`MethodNameCollision`-retirement.
            env.class_methods.insert(
                (qualified_class.clone(), method_name.clone()),
                e.clone(),
            );
            // build the inverse method → candidate-class set in
            // the same loop. `e.class_name` already carries the
            // qualified form (canonical-class-form invariant), so the set is keyed on
            // workspace-flat qualified class names directly.
            env.method_to_candidate_classes
                .entry(method_name.clone())
                .or_default()
                .insert(e.class_name.clone());
        }
    }

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

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

    // env.class_superclasses — walk every module's Def::Class.
    //
    // key + value both carry the qualified class name. The map
    // is queried by `expand_declared_constraints` with `c.class`
    // (a `Constraint.class` value, which is canonical-form on the
    // residual side post-canonical-class-form), so both halves of the map must match
    // the same workspace-key shape. A bare `SuperclassRef.class`
    // (same-module superclass) is lifted via `qualify_class_ref` —
    // mirrored inline below to avoid pulling in the workspace helper.
    for (mod_name, m) in &ws.modules {
        for d in &m.defs {
            if let Def::Class(cd) = d {
                if let Some(sc) = &cd.superclass {
                    let class_qualified = format!("{mod_name}.{}", cd.name);
                    let sc_qualified = if sc.class.contains('.') {
                        sc.class.clone()
                    } else {
                        format!("{mod_name}.{}", sc.class)
                    };
                    env.class_superclasses.insert(class_qualified, sc_qualified);
                }
            }
        }
    }

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

    env
}

/// Checks the bodies of a single module in the context of the workspace.
/// Assumption: `module_globals` already contains the top-level symbol
/// tables for **all** modules of the workspace (including `m`) — built
/// by `build_module_globals`.
///
/// Returns **all** errors found in this module, in def declaration order:
///
/// - The type-def setup phase is fail-fast within the module (duplicate
///   type or ctor names corrupt the env, so we abort *this* module after
///   the first such error and let the outer loop continue with others).
/// - The body-check phase is multi-diagnose: each def is checked
///   independently against the assembled env; a failure is recorded and
///   the next def is attempted.
fn check_in_workspace(
    m: &Module,
    ws: &Workspace,
    module_globals: &BTreeMap<String, ModuleGlobals>,
    // synth-time warnings collected here so the caller can
    // surface them into the workspace-wide diagnostic stream. Today
    // only `class-method-shadowed-by-fn` flows through this channel
    // (emitted from `synth` via `check_fn`'s warnings accumulator).
    out_warnings: &mut Vec<Diagnostic>,
) -> Vec<CheckError> {
    let mut env = build_check_env(ws);
    let mut errors: Vec<CheckError> = Vec::new();

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

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

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

    for def in &m.defs {
        match check_def(def, &env, out_warnings) {
            Ok(()) => {}
            Err(e) => {
                errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
            }
        }
    }
    // stamp the synth warnings with the module's name as `def`
    // so the JSON consumer can correlate them with the surrounding
    // module. The warning's `def` field carries the call-site def name
    // already (set inside `check_fn`); the workspace-wide caller
    // extends without further annotation.
    errors
}

fn check_def(
    def: &Def,
    env: &Env,
    out_warnings: &mut Vec<Diagnostic>,
) -> Result<()> {
    match def {
        Def::Fn(f) => check_fn(f, env, out_warnings),
        Def::Const(c) => check_const(c, env, out_warnings),
        Def::Type(td) => check_type_def(td, env),
        // bugfix-instance-body-unbound-var (2026-05-13): each instance
        // method body is walked through `check_fn` via a synthetic
        // `FnDef` lifted from the `Term::Lam` the InstanceMethod body
        // carries. This routes instance bodies through the same
        // identifier-resolution path as fn bodies, so an unbound
        // identifier inside an instance method fires `[unbound-var]`
        // at `ail check` instead of slipping past and surfacing as a
        // degraded "monomorphise_workspace: unknown identifier"
        // diagnostic at `ail build`. Class-method substitution
        // (class param → instance type) happens inside
        // `check_instance` before the body-walk. Class-schema
        // validation (InvalidSuperclassParam, etc.) and the workspace-
        // load coherence checks (Orphan / Duplicate / MissingMethod)
        // fire from `workspace::build_registry` independently, so a
        // malformed instance never reaches this body-walk. `Def::Class`
        // remains schema-only at this layer.
        Def::Class(_) => Ok(()),
        Def::Instance(inst) => check_instance(inst, env, out_warnings),
    }
}

/// Route each `InstanceMethod` body through `check_fn` by wrapping
/// it in a synthetic `FnDef`. The InstanceMethod body is by
/// convention a `Term::Lam` carrying its own `paramTypes` / `retType`
/// (the canonical class-form shape); we extract its `param_tys` /
/// `ret_ty` / `params` / `body` into an `FnDef` shape and reuse the
/// existing fn-body-check machinery.
///
/// Class-method substitution: the on-disk Lam's `param_tys` / `ret_ty`
/// reference the class's type parameter directly (e.g. the prelude
/// `instance Eq Int` body declares `(typed x a) (typed y a)` with `a`
/// being `Eq`'s class param). Before handing to `check_fn` we look up
/// the class's `param` name via `env.class_methods` and substitute it
/// to the instance's concrete `type_`, using the existing
/// `substitute_rigids` helper on type positions and
/// `substitute_rigids_in_term` on the body (which targets any embedded
/// Type annotations on nested Lams / LetRecs). Without this step
/// `check_fn` would fire `polymorphic-not-supported` on the class
/// param appearing in non-Forall position.
///
/// The synthetic fn name is `"<class>::<method>"`, used only for
/// diagnostic strings.
///
/// Non-Lam method bodies are not part of the current schema (all
/// fixtures in the corpus and the convention reaffirmed when method dispatch became type-driven
/// use `Term::Lam`); they are silently skipped here. If a future
/// schema admits non-Lam shapes, this arm must be extended to walk
/// them — silent skip is the conservative choice today because
/// the pre-fix behaviour was also silent.
fn check_instance(
    inst: &InstanceDef,
    env: &Env,
    out_warnings: &mut Vec<Diagnostic>,
) -> Result<()> {
    let qualified_class = qualify_class_ref_in_check(&inst.class, &env.current_module);
    for im in &inst.methods {
        // Look up the class's param name. Workspace-load's MissingMethod
        // gates this — if the (class, method) pair isn't in the table,
        // the instance was structurally rejected upstream and we never
        // get here in practice. Defensive fallback: skip substitution
        // (body walks without class-param resolution).
        let subst_map: BTreeMap<String, Type> = env
            .class_methods
            .get(&(qualified_class.clone(), im.name.clone()))
            .map(|entry| {
                let mut m = BTreeMap::new();
                m.insert(entry.class_param.clone(), inst.type_.clone());
                m
            })
            .unwrap_or_default();

        let Term::Lam { params, param_tys, ret_ty, effects, body } = &im.body else {
            // Non-Lam method body: skip (see fn-level doc-comment).
            continue;
        };
        let subst_param_tys: Vec<Type> = param_tys
            .iter()
            .map(|t| substitute_rigids(t, &subst_map))
            .collect();
        let subst_ret_ty = substitute_rigids(ret_ty, &subst_map);
        let subst_body = substitute_rigids_in_term(body, &subst_map);
        let fn_ty = Type::fn_implicit(
            subst_param_tys,
            subst_ret_ty,
            effects.clone(),
        );
        let synthetic = FnDef {
            name: format!("{}::{}", inst.class, im.name),
            ty: fn_ty,
            params: params.clone(),
            body: subst_body,
            doc: None,
            suppress: Vec::new(),
        export: None,
        };
        check_fn(&synthetic, env, out_warnings)?;
    }
    Ok(())
}

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

fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
    match t {
        Type::Con { name, args } => {
            let is_primitive = ailang_core::primitives::is_primitive_name(name);
            if is_primitive {
                if !args.is_empty() {
                    return Err(CheckError::UnknownType(format!(
                        "{name} (primitive does not take type args)"
                    )));
                }
                return Ok(());
            }
            // 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, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
    // Peel an outer Forall (Iter 12a). The vars become rigid in the
    // inner env so they pass `check_type_well_formed` and unify only
    // with themselves. An empty `vars` list (vacuously polymorphic)
    // gets normalised to a non-polymorphic body.
    let (rigids, inner_ty): (Vec<String>, Type) = match &f.ty {
        Type::Forall { vars, constraints: _, body } => (vars.clone(), (**body).clone()),
        other => (vec![], other.clone()),
    };

    let (param_tys, ret_ty, declared_effs) = match &inner_ty {
        Type::Fn { params, ret, effects, .. } => {
            (params.clone(), (**ret).clone(), effects.clone())
        }
        other => {
            return Err(CheckError::FnTypeRequired(
                f.name.clone(),
                ailang_core::pretty::type_to_string(other),
            ));
        }
    };

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

    // Install rigid vars. Cloning the env keeps the parent immutable
    // and the rigid set scoped to this def.
    let mut env = env.clone();
    for v in &rigids {
        env.rigid_vars.insert(v.clone());
    }

    // 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)?;

    // Embedding-ABI gate (M1 scalars / M2 ctx / M3 record): an
    // `(export …)` fn is the C call boundary. Its signature must be
    // C-ABI-permitted — `Int`/`Float`, or a single-constructor
    // record of those (M3) — and pure. Gate order: params → ret →
    // effects, first violation wins (so a combined Str+IO export
    // deterministically fails on the signature). Unconditional at
    // check-time — independent of the codegen emit mode — this IS
    // the clause-3 discriminator.
    if f.export.is_some() {
        fn is_c_scalar(t: &Type) -> bool {
            matches!(t, Type::Con { name, args, .. }
                if args.is_empty() && (name == "Int" || name == "Float"))
        }
        // M3 (spec 2026-05-18-embedding-abi-m3 §Architecture): a C
        // scalar, OR a single-constructor `data` whose every field is a
        // *bare* C scalar. Two-level by design — a record-typed field
        // stays rejected (M4 owns nested-record recursion). Uses the
        // in-scope `env.types: String -> TypeDef` (cf. lib.rs:1826).
        fn is_c_abi_type(t: &Type, env: &Env) -> bool {
            if is_c_scalar(t) {
                return true;
            }
            if let Type::Con { name, args, .. } = t {
                if args.is_empty() {
                    if let Some(td) = env.types.get(name) {
                        if td.ctors.len() == 1 {
                            return td.ctors[0]
                                .fields
                                .iter()
                                .all(is_c_scalar);
                        }
                    }
                }
            }
            false
        }
        for p in &param_tys {
            if !is_c_abi_type(p, &env) {
                return Err(CheckError::ExportNonScalarSignature(
                    f.name.clone(),
                    "parameter",
                    ailang_core::pretty::type_to_string(p),
                ));
            }
        }
        if !is_c_abi_type(&ret_ty, &env) {
            return Err(CheckError::ExportNonScalarSignature(
                f.name.clone(),
                "return",
                ailang_core::pretty::type_to_string(&ret_ty),
            ));
        }
        if !declared_effs.is_empty() {
            return Err(CheckError::ExportHasEffects(
                f.name.clone(),
                declared_effs.clone(),
            ));
        }
    }

    // build the post-superclass-expansion declared-constraint
    // set ONCE here and stash on env, so synth's Var-arm class-method
    // branch can hand it to `resolve_method_dispatch`'s constraint-
    // driven filter. The post-synth missing-constraint check below
    // re-reads the same expanded list from env to keep one source of
    // truth.
    //
    // Canonical-class-form follow-on: declared constraints carry the canonical-form
    // `class` value (bare for same-module, qualified for cross-module).
    // Lift to the workspace-key shape (always qualified) before
    // expanding — residuals always carry qualified `class` because
    // they come from `ClassMethodEntry.class_name` which is qualified
    // post-canonical-class-form
    let declared_constraints: Vec<Constraint> = match &f.ty {
        Type::Forall { constraints, .. } => constraints
            .iter()
            .map(|c| Constraint {
                class: qualify_class_ref_in_check(&c.class, &env.current_module),
                type_: c.type_.clone(),
            })
            .collect(),
        _ => Vec::new(),
    };
    env.active_declared_constraints =
        expand_declared_constraints(&declared_constraints, &env.class_superclasses);

    let mut locals = IndexMap::new();
    for (n, t) in f.params.iter().zip(param_tys.iter()) {
        locals.insert(n.clone(), t.clone());
    }
    let mut effects = BTreeSet::new();
    let mut subst = Subst::default();
    let mut counter: u32 = 0;
    // Per-fn residual class constraints. Every call to a class method
    // inside the body pushes a [`ResidualConstraint`] here; after the
    // body finishes, we compare against the expanded declared set.
    let mut residuals: Vec<ResidualConstraint> = Vec::new();
    let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
    let mut warnings: Vec<Diagnostic> = Vec::new();
    // loop-recur iter 2: fresh per-fn-body loop-binder-type stack.
    // Empty at fn entry; pushed/popped by `Term::Loop` arms during
    // the synth walk; discarded after the body type-checks.
    let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
    let body_ty = synth(&f.body, &env, &mut locals, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
    unify(&ret_ty, &body_ty, &mut subst)?;
    // surface synth-time warnings into the caller-supplied
    // accumulator. The warnings already carry `def: Some(f.name)`
    // set inside synth's emission site.
    out_warnings.extend(warnings);

    // tail-position verification (the explicit-tail-call contract). 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)?;

    // loop-recur iter 2: recur-in-tail-position verification. Runs
    // after synth (so RecurOutsideLoop/arity/type take code-
    // precedence) and alongside verify_tail_positions (sibling, not
    // a repurpose — verify_tail_positions' tail-app role is frozen).
    verify_loop_body(&f.body, false)?;

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

    // missing-constraint check. The expanded
    // declared-constraint set (declared + one-step superclass per
    // the typeclass design) was computed pre-synth and stashed on
    // `env.active_declared_constraints`. Var-shaped residuals
    // not covered by the expanded set fire `MissingConstraint`. Concrete
    // residuals are deferred to Task 10's `no-instance` arm.
    let expanded = &env.active_declared_constraints;
    for r in &residuals {
        let r_ty = subst.apply(&r.type_);

        // multi-candidate residuals refine before the existing
        // single-class discharge path. `MethodNameCollision` keeps the
        // candidate set singleton in real workspaces today; this branch
        // is exercised exclusively by unit tests until the type-driven dispatch refactor.
        if r.candidates.is_some() {
            // Normalize the type before hashing — same contract as the
            // single-class path below.
            let r_ty_norm = env
                .workspace_registry
                .normalize_type_for_lookup(env.current_module.as_str(), &r_ty);
            let normalized_residual = ResidualConstraint {
                class: r.class.clone(),
                type_: r_ty_norm,
                method: r.method.clone(),
                candidates: r.candidates.clone(),
            };
            let registry_unit: BTreeMap<(String, String), ()> = env
                .workspace_registry
                .entries
                .keys()
                .map(|k| (k.clone(), ()))
                .collect();
            match refine_multi_candidate_residual(
                &normalized_residual,
                expanded,
                &registry_unit,
            ) {
                RefineOutcome::Resolved(_) => {
                    // Discharge succeeded — the resolved class has an
                    // instance for this concrete type (or the rigid
                    // var has a matching declared constraint). Move
                    // on to the next residual; nothing to push.
                    continue;
                }
                RefineOutcome::NoInstance { method, at_type, candidate_classes } => {
                    return Err(CheckError::NoInstance {
                        def: f.name.clone(),
                        method,
                        class: r.class.clone(),
                        at_type,
                        candidate_classes,
                    });
                }
                RefineOutcome::Ambiguous { method, at_type, candidate_classes } => {
                    return Err(CheckError::AmbiguousMethodResolution {
                        method,
                        at_type,
                        candidate_classes,
                    });
                }
                RefineOutcome::MissingConstraint { method, candidate_classes } => {
                    return Err(CheckError::MissingConstraint {
                        def: f.name.clone(),
                        method,
                        class: candidate_classes.first().cloned().unwrap_or_default(),
                        at_type: ailang_core::pretty::type_to_string(&r_ty),
                    });
                }
            }
        }

        if let Type::Var { name } = &r_ty {
            // Skip residuals over metavars (`$mN`) — those mean the
            // residual is over a value the body never connected to a
            // rigid var; treat as concrete-uncovered, which Task 10
            // will handle. Only rigid (source-level) vars participate
            // in the missing-constraint check here.
            if Subst::meta_id(name).is_some() {
                continue;
            }
            let satisfied = expanded
                .iter()
                .any(|d| d.class == r.class && constraint_type_matches(&d.type_, &r_ty));
            if !satisfied {
                return Err(CheckError::MissingConstraint {
                    def: f.name.clone(),
                    method: r.method.clone(),
                    class: r.class.clone(),
                    at_type: name.clone(),
                });
            }
        } else if is_fully_concrete(&r_ty) {
            // fully-concrete residual — the class
            // method was called at a concrete type, so the obligation
            // can only be discharged by an existing workspace instance.
            // Look up `(class, type_hash(r_ty))` in the registry; absence
            // → no-instance. The hash uses `canonical::type_hash`, the
            // same key shape `workspace::build_registry` writes with, so
            // representation-equal types match deterministically.
            // normalize to match Registry::normalize_type_for_lookup contract
            let r_ty_norm = env
                .workspace_registry
                .normalize_type_for_lookup(env.current_module.as_str(), &r_ty);
            let key = (
                r.class.clone(),
                ailang_core::canonical::type_hash(&r_ty_norm),
            );
            if !env.workspace_registry.entries.contains_key(&key) {
                return Err(CheckError::NoInstance {
                    def: f.name.clone(),
                    method: r.method.clone(),
                    class: r.class.clone(),
                    at_type: ailang_core::pretty::type_to_string(&r_ty),
                    candidate_classes: vec![],
                });
            }
        }
        // Other shapes (unsolved metavars inside a `Type::Con`,
        // `Type::Fn`, `Type::Forall`) are out of scope for the 22b.2
        // diagnostics: metavars mean the body never connected the
        // class param to anything observable, and `Fn`/`Forall` cannot
        // appear as instance heads (the typeclass design).
    }
    Ok(())
}

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

/// per-call-site residual class constraint
/// recorded by `synth` when a `Term::Var` resolves to a class method.
/// Carries the method name (for diagnostic rendering), the class, and
/// the type the class is applied to at the call site. The type is
/// typically a fresh metavar (which unification then ties to the
/// argument's actual type) or, after `subst.apply`, a rigid var or a
/// concrete `Type::Con`.
#[derive(Debug, Clone)]
pub struct ResidualConstraint {
    /// Class name (e.g. `Show`).
    ///
    /// When [`Self::candidates`] is `None`, this is the resolved class
    /// (single-class dispatch path). When `Some(set)`, this is a
    /// tentative value (typically the first set element in BTreeSet
    /// order); discharge / mono refinement overwrites it with the
    /// actually-resolved class.
    pub class: String,
    /// Class param's instance at this call site. Pre-substitution: the
    /// fresh metavar inserted at the Var site. Post-substitution: the
    /// solved type — rigid var, concrete con, or unsolved metavar.
    pub type_: Type,
    /// Method name (e.g. `show`); used by the missing-constraint
    /// diagnostic to point the author at which call site triggered
    /// the residual.
    pub method: String,
    /// candidate-class set for the multi-candidate dispatch
    /// path. `None` ⇒ single-class semantics (pre-canonical-class-form behaviour);
    /// the [`Self::class`] field is the resolved class. `Some(set)`
    /// ⇒ multi-candidate residual; discharge / mono refinement filters
    /// the set at fn-body-end. With `MethodNameCollision` still active
    /// (pre-canonical-class-form), real workspaces only ever construct `None`-candidate
    /// residuals; the `Some`-path is exercised exclusively by unit
    /// tests until the type-driven dispatch refactor retires the workaround.
    pub candidates: Option<BTreeSet<String>>,
}

/// outcome of the dispatch-resolution helper
/// [`resolve_method_dispatch`]. The synth Var-arm consumer translates
/// this enum into either a singleton [`ResidualConstraint`]
/// (`Resolved`) or a multi-candidate residual (`Multi`) for discharge-
/// time refinement, or a `CheckError` (`Unknown` / `Ambiguous`).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum MethodDispatchOutcome {
    /// Single class resolved unambiguously.
    Resolved(String),
    /// Explicit qualifier names a class not in the candidate set.
    UnknownClass(String),
    /// Bare-method call site survived both type-driven and
    /// constraint-driven filters with > 1 candidate.
    Ambiguous {
        method: String,
        at_type: String,
        candidates: Vec<String>,
    },
    /// Bare-method call site with multiple candidates that need
    /// discharge-time refinement (rigid var type at synth time;
    /// concrete type only available at discharge).
    Multi {
        method: String,
        candidates: BTreeSet<String>,
    },
}

/// resolve a method-call site per the spec's 5-step rule. Pure
/// function — no Env mutation, no residual emission.
///
/// `qualifier_prefix` is the dot-stripped class prefix (e.g.
/// `"prelude.Show"` for a `Term::Var.name == "prelude.Show.show"`).
/// `None` = bare method form.
///
/// `concrete_arg_type` is `Some` when the caller has the arg type
/// available (e.g. discharge-time refinement); `None` when synth is at
/// the Var arm before App-arm unification. When `None`, the helper
/// emits `Multi` if the candidate set is non-singleton (no early
/// type-driven filter possible). When `Some(t)` with `t` a non-rigid
/// concrete type, the type-driven filter applies; when `t` is a rigid
/// `Type::Var`, the constraint-driven filter applies.
///
/// `declared_constraints` are the active forall-bound constraints in
/// scope at the call site; consulted for the rigid-var fallback.
///
/// `registry` is the workspace registry keyed by `(qualified_class,
/// type_hash)` for instance-existence checks. Values are unit; only
/// key presence matters.
pub fn resolve_method_dispatch(
    method: &str,
    qualifier_prefix: Option<&str>,
    candidates: &BTreeSet<String>,
    concrete_arg_type: Option<&Type>,
    declared_constraints: &[ailang_core::ast::Constraint],
    registry: &BTreeMap<(String, String), ()>,
) -> MethodDispatchOutcome {
    // Step 3 (5-step rule): explicit qualifier present.
    if let Some(q) = qualifier_prefix {
        if candidates.contains(q) {
            return MethodDispatchOutcome::Resolved(q.to_string());
        }
        return MethodDispatchOutcome::UnknownClass(q.to_string());
    }

    // Step 4: bare-method form, singleton candidate set — pre-canonical-class-form
    // path. Returns immediately so the post-canonical-class-form multi-candidate
    // logic below stays gated on a non-singleton candidate set.
    if candidates.len() == 1 {
        return MethodDispatchOutcome::Resolved(
            candidates.iter().next().cloned().unwrap(),
        );
    }

    // Multi-candidate path: type-driven filter first when the arg
    // type is concrete (non-Var).
    let concrete = concrete_arg_type
        .filter(|t| !matches!(t, Type::Var { .. }));
    if let Some(t) = concrete {
        let type_h = ailang_core::canonical::type_hash(t);
        let survivors: BTreeSet<String> = candidates
            .iter()
            .filter(|c| registry.contains_key(&((**c).clone(), type_h.clone())))
            .cloned()
            .collect();
        if survivors.len() == 1 {
            return MethodDispatchOutcome::Resolved(
                survivors.into_iter().next().unwrap(),
            );
        }
        if survivors.len() > 1 {
            let mut sorted: Vec<String> = survivors.into_iter().collect();
            sorted.sort();
            let at_type = ailang_core::pretty::type_to_string(t);
            return MethodDispatchOutcome::Ambiguous {
                method: method.to_string(),
                at_type,
                candidates: sorted,
            };
        }
        // Zero survivors after the type-driven filter: fall through
        // to constraint-driven filter, then `Multi` for discharge-
        // time refinement (where `NoInstance` with `candidate_classes`
        // is fired against the full candidate set).
    }

    // Constraint-driven filter (rigid-var case or no concrete arg).
    let survivors: BTreeSet<String> = candidates
        .iter()
        .filter(|c| {
            declared_constraints
                .iter()
                .any(|dc| &dc.class == *c)
        })
        .cloned()
        .collect();
    if survivors.len() == 1 {
        return MethodDispatchOutcome::Resolved(
            survivors.into_iter().next().unwrap(),
        );
    }

    // No filter narrowed; emit `Multi` for discharge-time refinement.
    MethodDispatchOutcome::Multi {
        method: method.to_string(),
        candidates: candidates.clone(),
    }
}

/// outcome of multi-candidate residual refinement at discharge
/// time. Consumed by `check_fn`'s residual loop and by mono's
/// residual-to-target mapping.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum RefineOutcome {
    /// Refinement converged on a single class.
    Resolved(String),
    /// Concrete `type_` with zero registry survivors — the call site
    /// must be discharged via an existing instance, but none of the
    /// candidate classes has one for this type. Surfaces as a
    /// `CheckError::NoInstance` with the full candidate set populated.
    NoInstance {
        method: String,
        at_type: String,
        candidate_classes: Vec<String>,
    },
    /// Concrete `type_` with multiple registry survivors — every
    /// surviving candidate has an instance for this type; the author
    /// must disambiguate explicitly. Surfaces as a
    /// `CheckError::AmbiguousMethodResolution`.
    Ambiguous {
        method: String,
        at_type: String,
        candidate_classes: Vec<String>,
    },
    /// Rigid-var residual with non-singleton constraint-set survivors.
    /// Surfaces as a `CheckError::MissingConstraint` (the body must
    /// declare a constraint to commit to one of the candidates).
    MissingConstraint {
        method: String,
        candidate_classes: Vec<String>,
    },
}

/// refine a multi-candidate residual at discharge time per the
/// spec's 5-step rule (constraint-discharge refinement subsection).
/// Caller MUST pass a residual whose `candidates` is `Some(...)`;
/// single-candidate residuals (`candidates: None`) bypass this helper
/// and discharge directly against the registry as in pre-canonical-class-form
///
/// Refinement strategy:
/// - Concrete `type_`: filter the candidate set against the registry
///   keyed on `(class, type_hash(type_))`. 0 survivors → `NoInstance`;
///   1 → `Resolved`; >1 → `Ambiguous`.
/// - Rigid-var `type_`: filter the candidate set against the active
///   declared-constraint list. 1 survivor → `Resolved`; otherwise
///   → `MissingConstraint`.
pub fn refine_multi_candidate_residual(
    residual: &ResidualConstraint,
    declared_constraints: &[ailang_core::ast::Constraint],
    registry: &BTreeMap<(String, String), ()>,
) -> RefineOutcome {
    let candidates = residual
        .candidates
        .as_ref()
        .expect("refine_multi_candidate_residual called on single-candidate residual");

    // Concrete-type path.
    if !matches!(residual.type_, Type::Var { .. }) {
        let type_h = ailang_core::canonical::type_hash(&residual.type_);
        let survivors: Vec<String> = candidates
            .iter()
            .filter(|c| registry.contains_key(&((**c).clone(), type_h.clone())))
            .cloned()
            .collect();
        let at_type = ailang_core::pretty::type_to_string(&residual.type_);
        return match survivors.len() {
            0 => RefineOutcome::NoInstance {
                method: residual.method.clone(),
                at_type,
                candidate_classes: candidates.iter().cloned().collect(),
            },
            1 => RefineOutcome::Resolved(survivors.into_iter().next().unwrap()),
            _ => {
                let mut sorted = survivors;
                sorted.sort();
                RefineOutcome::Ambiguous {
                    method: residual.method.clone(),
                    at_type,
                    candidate_classes: sorted,
                }
            }
        };
    }

    // Rigid-var path: filter against declared constraints requiring
    // BOTH class-name match AND type-unification with the residual's
    // `type_` (per spec §"Constraint-discharge refinement" 130-138).
    // `constraint_type_matches` is the post-`subst.apply` Var/Con
    // recursive matcher; the residual's `type_` has been `subst.apply`-d
    // by the discharge caller, so rigid-var identity (Var("a") vs
    // Var("b")) is a direct name comparison.
    let survivors: Vec<String> = candidates
        .iter()
        .filter(|c| {
            declared_constraints.iter().any(|dc| {
                &dc.class == *c && constraint_type_matches(&dc.type_, &residual.type_)
            })
        })
        .cloned()
        .collect();
    match survivors.len() {
        1 => RefineOutcome::Resolved(survivors.into_iter().next().unwrap()),
        _ => RefineOutcome::MissingConstraint {
            method: residual.method.clone(),
            candidate_classes: candidates.iter().cloned().collect(),
        },
    }
}

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

/// lift a canonical-form class-ref value to the qualified
/// workspace-key shape. Bare ⇒ prepend `caller_module` (the bare
/// form names the caller-module-local class under the canonical-form
/// rule); qualified ⇒ as-is. Sibling of `workspace::qualify_class_ref`
/// for the check-side; duplicated to keep `ailang-check` from
/// reaching across crates for one private helper.
pub(crate) fn qualify_class_ref_in_check(class_ref: &str, caller_module: &str) -> String {
    if class_ref.contains('.') {
        class_ref.to_string()
    } else {
        format!("{caller_module}.{class_ref}")
    }
}

/// split a `Term::Var.name` into `(method_name,
/// optional_qualifier_prefix)` at the last dot.
///
/// - `"show"` → `("show", None)`
/// - `"prelude.Show.show"` → `("show", Some("prelude.Show"))`
/// - `"Show.show"` → `("show", Some("Show"))`
/// - `"std_list.length"` → `("length", Some("std_list"))`
///
/// Callers distinguish class qualifiers from cross-module-fn
/// qualifiers via [`qualifier_is_class_shape`]: PascalCase
/// single-segment prefixes (e.g. `"Show"`) and multi-segment
/// prefixes (e.g. `"prelude.Show"`) are class qualifiers per
/// the canonical-class-form rule; lowercase single-segment prefixes
/// (e.g. `"std_list"`) are module names and the caller falls
/// through to the cross-module-fn path.
pub(crate) fn parse_method_qualifier(name: &str) -> (&str, Option<String>) {
    if let Some(dot_idx) = name.rfind('.') {
        (&name[dot_idx + 1..], Some(name[..dot_idx].to_string()))
    } else {
        (name, None)
    }
}

/// mq.tidy: predicate gating the synth Var-arm's class-method
/// dispatch entry on the qualifier shape. Accepts:
///   - bare-method form (qualifier absent), e.g. `"show"`.
///   - bare-class qualifier, e.g. `"Show.show"` — class names are
///     PascalCase per repo convention (first character uppercase).
///   - module-qualified class qualifier, e.g. `"prelude.Show.show"`.
///
/// Rejects qualifier shapes that look like cross-module-fn calls
/// (`"std_list.length"`): qualifier starts with lowercase, no
/// inner dot — falls through to the qualified-fn arm.
pub(crate) fn qualifier_is_class_shape(qualifier_opt: &Option<String>) -> bool {
    match qualifier_opt {
        None => true,
        Some(q) => {
            // Contains inner dot: module-qualified class
            // (`prelude.Show`).
            if q.contains('.') {
                return true;
            }
            // Single segment: class iff the first char is uppercase
            // (PascalCase convention).
            q.chars().next().map(|c| c.is_uppercase()).unwrap_or(false)
        }
    }
}

/// Type-driven dispatch entry predicate: the synth Var-arm runs this to
/// decide whether `name` should be routed through the class-method
/// dispatch helper. Matches a bare method name (e.g. `"show"`) or a
/// class-shaped qualifier (`"Show.show"`, `"prelude.Show.show"`).
/// A 1-dot lowercase name (`"std_list.length"`) is structurally a
/// cross-module-fn call per the canonical-class-form rule's canonical-form rule and falls
/// through to the qualified-fn arm.
fn is_class_method_dispatch(name: &str, env: &Env) -> bool {
    let (method_name, qualifier_opt) = parse_method_qualifier(name);
    qualifier_is_class_shape(&qualifier_opt)
        && env.method_to_candidate_classes.contains_key(method_name)
}

/// mq.tidy: predicate for the `class-method-shadowed-by-fn`
/// warning emission. The full spec rule (§"Class-fn collisions"
/// 161-162) requires a class candidate WITH AN INSTANCE FOR THE
/// ACTUAL ARG TYPE; the arg type is unavailable at the synth
/// Var-arm where the warning fires (App-arm unification has not
/// run yet). This conservative approximation requires only that
/// at least one candidate class has SOME instance in the
/// workspace registry — stricter than today's "any class
/// declares the method" (which fires even for class methods
/// with zero instances anywhere), looser than the full spec
/// rule. A future tighten can defer the warning emission to a
/// later pass where the arg type is known.
pub(crate) fn any_candidate_class_has_instance(
    method_to_candidate_classes: &BTreeMap<String, BTreeSet<String>>,
    workspace_registry_entries: &BTreeMap<(String, String), ()>,
    method_name: &str,
) -> bool {
    let Some(cands) = method_to_candidate_classes.get(method_name) else {
        return false;
    };
    cands.iter().any(|c| {
        // BTreeMap is ordered lexicographically on the tuple key;
        // `range((c, "")..).next()` is the first entry whose first
        // component is >= `c`. The check `k == c` rejects spillover
        // into the next class. O(log n) per candidate.
        workspace_registry_entries
            .range((c.clone(), String::new())..)
            .next()
            .map(|((k, _), _)| k == c)
            .unwrap_or(false)
    })
}

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

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

/// verifies that every `Term::App { tail: true, .. }` and
/// `Term::Do { tail: true, .. }` actually sits in tail position, per
/// the explicit-tail-call contract
/// (`design/contracts/tail-calls.md`).
///
/// `is_tail` is the tail-context flag for the term currently being
/// visited. The propagation rules (from design/contracts/tail-calls.md):
///
/// - 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, .. } => {
            // `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 } => {
            // 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 } => {
            // 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)
        }
        // loop-recur iter 1: binder inits are evaluated once on loop
        // entry, NOT in tail position. The loop body inherits the
        // enclosing tail position (the loop's value is the body's
        // value on the exiting iteration). This arm only defines
        // tail-app descent through the new node; it makes NO claim
        // about recur tail-position (that is loop-recur iter 2's
        // `verify_loop_body`). The tail-app verification role is
        // unchanged — no pre-existing fixture contains a
        // `loop`/`recur` node.
        Term::Loop { binders, body } => {
            for b in binders {
                verify_tail_positions(&b.init, false)?;
            }
            verify_tail_positions(body, is_tail)
        }
        // recur transfers control and does not fall through, so there
        // is no tail position to propagate. Its args are evaluated in
        // non-tail position (call-argument-like). Introduces no
        // tail-app violation.
        Term::Recur { args } => {
            for a in args {
                verify_tail_positions(a, false)?;
            }
            Ok(())
        }
    }
}

/// loop-recur iter 2: enforces that every `Term::Recur` occurs in
/// tail position of its lexically-innermost enclosing `Term::Loop`
/// body. A NEW private pass — a *sibling* of
/// `verify_tail_positions` (which is spec-frozen for its tail-app
/// role and unchanged). Invoked from `check_fn` *after* `synth`, so
/// `RecurOutsideLoop`/arity/type (raised in `synth`) take code-
/// precedence; by the time a `Recur` is reached here it is known to
/// be inside a loop with matching arity/types — this pass adds only
/// the tail-position rule. `in_loop_tail` is the loop analogue of
/// `verify_tail_positions`' `is_tail`, scoped to the innermost loop.
fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
    match t {
        Term::Lit { .. } | Term::Var { .. } => Ok(()),
        Term::Recur { args } => {
            if !in_loop_tail {
                return Err(CheckError::RecurNotInTailPosition);
            }
            // recur args are evaluated in non-tail position; a recur
            // nested inside a recur arg is itself non-tail.
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Loop { binders, body } => {
            // Binder inits run once on loop entry — not in the
            // loop's tail scope. The loop body opens a FRESH
            // innermost-loop tail scope (independent of where the
            // loop itself sits — the loop's tail scope is intrinsic).
            for b in binders {
                verify_loop_body(&b.init, false)?;
            }
            verify_loop_body(body, true)
        }
        Term::App { callee, args, .. } => {
            verify_loop_body(callee, false)?;
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Do { args, .. } => {
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Let { value, body, .. } => {
            verify_loop_body(value, false)?;
            verify_loop_body(body, in_loop_tail)
        }
        Term::If { cond, then, else_ } => {
            verify_loop_body(cond, false)?;
            verify_loop_body(then, in_loop_tail)?;
            verify_loop_body(else_, in_loop_tail)
        }
        Term::Seq { lhs, rhs } => {
            verify_loop_body(lhs, false)?;
            verify_loop_body(rhs, in_loop_tail)
        }
        Term::Match { scrutinee, arms } => {
            verify_loop_body(scrutinee, false)?;
            for arm in arms {
                verify_loop_body(&arm.body, in_loop_tail)?;
            }
            Ok(())
        }
        Term::Ctor { args, .. } => {
            for a in args {
                verify_loop_body(a, false)?;
            }
            Ok(())
        }
        Term::Lam { body, .. } => {
            // A `recur` cannot cross a lambda boundary (different
            // control frame). Reset: a recur inside a lam is outside
            // every enclosing loop's tail scope — and synth's
            // loop_stack likewise does not cross the lam, so such a
            // recur is already a synth `RecurOutsideLoop`.
            verify_loop_body(body, false)
        }
        Term::LetRec { body, in_term, .. } => {
            verify_loop_body(body, false)?;
            verify_loop_body(in_term, in_loop_tail)
        }
        Term::Clone { value } => verify_loop_body(value, in_loop_tail),
        Term::ReuseAs { source, body } => {
            verify_loop_body(source, false)?;
            verify_loop_body(body, in_loop_tail)
        }
    }
}

fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> 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;
    // const bodies don't carry a `Forall.constraints`
    // (rejected upstream), so any residual would have to be concrete —
    // Task 10's no-instance arm will pick those up. We thread an
    // accumulator only to keep `synth`'s signature uniform.
    let mut residuals: Vec<ResidualConstraint> = Vec::new();
    let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
    let mut warnings: Vec<Diagnostic> = Vec::new();
    // loop-recur iter 2: a const value has no enclosing loop; any
    // `recur` in a const body correctly fires `RecurOutsideLoop`.
    let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
    let v = synth(&c.value, env, &mut locals, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
    out_warnings.extend(warnings);
    unify(&c.ty, &v, &mut subst)?;
    if !effects.is_empty() {
        return Err(CheckError::ConstHasEffects(
            c.name.clone(),
            effects.into_iter().collect(),
        ));
    }
    Ok(())
}

#[allow(clippy::too_many_arguments)]
pub(crate) fn synth(
    t: &Term,
    env: &Env,
    locals: &mut IndexMap<String, Type>,
    // loop-recur iter 2: per-walk loop-binder stack. Each frame is one
    // `Term::Loop`'s binders in declaration order. `recur` rebinds
    // binders by position, not name, so the type list is positional;
    // iter loop-recur.tidy added the binder name alongside the type
    // so `Term::Lam`'s escape guard can reject a free var that is an
    // in-scope loop binder. Pushed on `Term::Loop` body entry, popped
    // on exit; consulted innermost-first by `Term::Recur` for arity +
    // per-position type, and across all frames by `Term::Lam` for the
    // escape check. Position: locals-adjacent — per-fn-body
    // lexical-control scope state.
    loop_stack: &mut Vec<Vec<(String, Type)>>,
    effects: &mut BTreeSet<String>,
    in_def: &str,
    subst: &mut Subst,
    counter: &mut u32,
    residuals: &mut Vec<ResidualConstraint>,
    free_fn_calls: &mut Vec<FreeFnCall>,
    // out-parameter for synth-time structured warnings. Symmetric
    // to `residuals` / `free_fn_calls`. Currently only the
    // `class-method-shadowed-by-fn` warning is emitted here; future
    // synth-time warnings (if any) would flow through the same channel.
    warnings: &mut Vec<crate::diagnostic::Diagnostic>,
) -> Result<Type> {
    match t {
        Term::Lit { lit } => Ok(match lit {
            Literal::Int { .. } => Type::int(),
            Literal::Bool { .. } => Type::bool_(),
            Literal::Str { .. } => Type::str_(),
            Literal::Unit => Type::unit(),
            Literal::Float { .. } => Type::float(),
        }),
        Term::Var { name } => {
            // Lookup precedence: locals → local globals → class-method
            // table → qualified cross-module ref. A `Forall` resolved at
            // any of these levels is instantiated with fresh metavars at
            // the use site (textbook ML rule); rigid vars and concrete
            // types pass through unchanged.
            //
            // the class-method channel sits between
            // local globals and qualified cross-module ref. When a name
            // resolves through `env.class_methods`, we substitute the
            // class param with a fresh metavar and record a residual
            // class constraint — `check_fn` later compares the residual
            // set against the declared `Forall.constraints`.
            // alongside the bare type, capture
            //   (owner_module, unqualified_name_in_owner_module)
            // for any non-local resolution that lands on a
            // `Type::Forall` AND is a real workspace-declared
            // `Def::Fn` (NOT a builtin operator like `==`). The
            // discriminator is whether the name appears in
            // `env.module_globals[<owner>]` — builtins are installed
            // into `env.globals` only. The unqualified-name capture
            // matters for dot-qualified call sites: the FreeFnCall
            // records the suffix (e.g. `length`), not the full
            // `std_list.length`, so `synthesise_mono_fn_for_free_fn`
            // can look up the source def by its bare name in the
            // owner module's def list.
            //
            // After the resolution ladder, if `raw` is a `Type::Forall`
            // AND a `free_fn_owner` is known, push a `FreeFnCall`
            // observation; the mono pass `subst.apply`s the metas
            // post-synth to recover concrete type-args at each
            // polymorphic free-fn call site.
            // a helper closure that emits the
            // `class-method-shadowed-by-fn` warning when a fn-precedence
            // branch resolves a name that ALSO has class-method
            // candidates in the workspace. The fn resolution proceeds;
            // the warning surfaces the shadow so the LLM-author can
            // disambiguate via explicit class-qualified call if the
            // shadow was unintentional. Locals/same-module-fn/implicit-
            // import-fn all share this rule.
            let emit_shadow_warning_if_class_method =
                |name: &str, owner_module: &str, warnings: &mut Vec<crate::diagnostic::Diagnostic>| {
                    let (method_name, _) = parse_method_qualifier(name);
                    // mq.tidy: tighten emission per spec §"Class-fn
                    // collisions" — fire only when at least one
                    // candidate class has a registry instance (any
                    // type). Without this, the warning fires on any
                    // class declaring the method, including class
                    // methods with zero instances anywhere in the
                    // workspace.
                    let registry_unit_view: BTreeMap<(String, String), ()> = env
                        .workspace_registry
                        .entries
                        .keys()
                        .map(|k| (k.clone(), ()))
                        .collect();
                    if !any_candidate_class_has_instance(
                        &env.method_to_candidate_classes,
                        &registry_unit_view,
                        method_name,
                    ) {
                        return;
                    }
                    if let Some(cands) = env.method_to_candidate_classes.get(method_name) {
                        let mut candidate_list: Vec<String> = cands.iter().cloned().collect();
                        candidate_list.sort();
                        let d = crate::diagnostic::Diagnostic::warning(
                            "class-method-shadowed-by-fn",
                            format!(
                                "free fn `{name}` in module `{owner_module}` shadows class method `{method_name}` \
                                 declared in classes {candidate_list:?}. \
                                 To call the class method instead, write `<ClassQualifier>.{method_name} ...`.",
                            ),
                        )
                        .with_def(in_def.to_string())
                        .with_ctx(serde_json::json!({
                            "name": name,
                            "method": method_name,
                            "fn_owner_module": owner_module,
                            "candidate_classes": candidate_list,
                        }));
                        warnings.push(d);
                    }
                };

            let (raw, free_fn_owner): (Type, Option<(String, String)>) = if let Some(t) = locals.get(name) {
                // Locals (lambda / let / fn-params) — fn wins per
                // lookup precedence. A class method shadowed by a
                // local binding fires the shadow warning so the
                // author can disambiguate if unintentional.
                emit_shadow_warning_if_class_method(name, env.current_module.as_str(), warnings);
                (t.clone(), None)
            } else if let Some(t) = env.globals.get(name) {
                // Same-module global. Owner is the current module IFF
                // the name is in this module's declared globals
                // (i.e. it's a `Def::Fn`, not a builtin). The bare
                // `name` works as the in-module key.
                let owner = env
                    .module_globals
                    .get(&env.current_module)
                    .filter(|m| m.contains_key(name))
                    .map(|_| (env.current_module.clone(), name.clone()));
                emit_shadow_warning_if_class_method(name, env.current_module.as_str(), warnings);
                (t.clone(), owner)
            } else if let Some((owner_module, raw_ty)) = env
                .imports
                .values()
                .find_map(|mod_name| {
                    env.module_globals
                        .get(mod_name)
                        .and_then(|mg| mg.get(name).map(|ty| (mod_name.clone(), ty.clone())))
                })
            {
                // implicit-import free-fn precedence runs BEFORE
                // the class-method branch (fn wins per spec
                // §"Class-fn collisions"). When the name has class-
                // method candidates too, emit the shadow warning.
                //
                // bare-name fall-through to free fns of
                // implicitly-imported modules. Today only the prelude is
                // implicitly imported (see `build_check_env` and
                // `check_in_workspace`'s prelude-injection), so the
                // first match is unambiguous. If a second implicit
                // import lands, the single-match-wins rule becomes a
                // real ambiguity and this branch needs a
                // duplicate-detection diagnostic.
                emit_shadow_warning_if_class_method(name, owner_module.as_str(), warnings);
                // Qualify any bare type-cons referring to a type defined in
                // the owning module — same treatment the dot-qualified arm
                // below applies — so signatures cross the module boundary
                // with fully-qualified Type::Cons.
                let owner_types = env
                    .module_types
                    .get(&owner_module)
                    .cloned()
                    .unwrap_or_default();
                let qualified = qualify_local_types(&raw_ty, &owner_module, &owner_types);
                // Bare name resolves through implicit import; the
                // unqualified name in the owner module is the same `name`.
                (qualified, Some((owner_module, name.clone())))
            } else if is_class_method_dispatch(name, env) {
                // type-driven dispatch entry. The Var arm runs
                // before App-arm unification, so the arg type is not
                // available here. The dispatch helper resolves on
                // (a) explicit class qualifier, (b) singleton candidate
                // set (today's invariant), or (c) constraint-driven
                // filter (rigid-var case); otherwise it emits `Multi`
                // for discharge-time refinement.
                //
                // With `MethodNameCollision` still active (pre-canonical-class-form),
                // real workspaces never reach the `Multi` branch — the
                // candidate set is always singleton. The branch is
                // installed here for the type-driven dispatch refactor to exercise without further
                // dispatch-side edits.
                let (method_name, qualifier_opt) = parse_method_qualifier(name);
                let candidates = env
                    .method_to_candidate_classes
                    .get(method_name)
                    .expect("contains_key invariant: gate above guarantees presence");

                // Build a unit-view of the workspace registry keyed by
                // (qualified_class, type_hash). Values are unit; only
                // key presence matters for the type-driven filter.
                let registry_unit: BTreeMap<(String, String), ()> = env
                    .workspace_registry
                    .entries
                    .keys()
                    .map(|k| (k.clone(), ()))
                    .collect();

                let outcome = resolve_method_dispatch(
                    method_name,
                    qualifier_opt.as_deref(),
                    candidates,
                    /*concrete_arg_type*/ None,
                    /*declared_constraints*/ &env.active_declared_constraints,
                    /*registry*/ &registry_unit,
                );

                let (residual_class, residual_candidates) = match outcome {
                    MethodDispatchOutcome::Resolved(class) => (class, None),
                    MethodDispatchOutcome::Multi { candidates: cs, method: _ } => {
                        // Tentative class: first BTreeSet element.
                        // Refinement at discharge / mono time overwrites it.
                        let tentative = cs.iter().next().cloned().unwrap_or_default();
                        (tentative, Some(cs))
                    }
                    MethodDispatchOutcome::UnknownClass(qname) => {
                        return Err(CheckError::UnknownClass { name: qname });
                    }
                    MethodDispatchOutcome::Ambiguous { method, at_type, candidates: cs } => {
                        return Err(CheckError::AmbiguousMethodResolution {
                            method,
                            at_type,
                            candidate_classes: cs,
                        });
                    }
                };

                // class_methods is tuple-keyed by
                // `(qualified-class, method)`. The dispatcher above
                // resolved a tentative class (single-survivor or first
                // BTreeSet element for the multi-candidate path) — use
                // it to disambiguate the lookup. The `expect` is sound
                // by construction: `method_to_candidate_classes` and
                // `class_methods` are built from the same source loop
                // (every entry in one has a matching entry in the
                // other; see `build_check_env`).
                let cm = env
                    .class_methods
                    .get(&(residual_class.clone(), method_name.to_string()))
                    .expect(
                        "method_to_candidate_classes invariant: \
                         (resolved class, method) present implies class_methods entry",
                    );
                let owner_types = env
                    .module_types
                    .get(&cm.defining_module)
                    .cloned()
                    .unwrap_or_default();
                let qualified_method_ty =
                    qualify_local_types(&cm.method_ty, &cm.defining_module, &owner_types);
                let fresh = Subst::fresh(counter);
                let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
                mapping.insert(cm.class_param.clone(), fresh.clone());
                let inst_ty = substitute_rigids(&qualified_method_ty, &mapping);
                residuals.push(ResidualConstraint {
                    class: residual_class,
                    type_: fresh,
                    method: method_name.to_string(),
                    candidates: residual_candidates,
                });
                return Ok(inst_ty);
            } 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(),
                    }
                })?;
                // qualify any bare type-cons referring to a
                // type defined in the owning module so that signatures
                // pulled across the boundary unify against
                // qualified-form ctors and types in the consumer
                // module.
                let owner_types = env
                    .module_types
                    .get(&target_module)
                    .cloned()
                    .unwrap_or_default();
                let qualified = qualify_local_types(&raw_ty, &target_module, &owner_types);
                // Dot-qualified `prefix.suffix`: the unqualified name in
                // the owner module is `suffix`.
                (qualified, Some((target_module, suffix.to_string())))
            } else {
                return Err(CheckError::UnknownIdent(name.clone()));
            };
            // if raw is `Type::Forall` AND we know the
            // owner module (i.e. the resolution went through a non-
            // local branch), record a FreeFnCall observation BEFORE
            // instantiating. The metas are the fresh metavars we
            // about to use; the mono pass `subst.apply`s them later.
            // Note: `unqualified_name` is the name as seen inside the
            // owner module (so the mono pass can find the `Def::Fn`
            // by bare name); the source-level `name` may be a
            // dot-qualified form (`prefix.suffix`) the synth started
            // with.
            if let (Type::Forall { vars, constraints, body }, Some((owner, unqualified_name))) =
                (&raw, &free_fn_owner)
            {
                let (metas, inst) = instantiate(vars, body, counter);
                // push a residual for each declared constraint
                // of the poly free fn with the rigid var substituted by
                // its fresh metavar. The discharge loop at the enclosing
                // `check_fn`'s post-synth phase resolves the residual
                // against the workspace registry (fully-concrete after
                // App-arm unification) and fires `NoInstance` if no
                // instance ships for the unified type. Without this push,
                // `print f` at a function type `f : Int -> Int` would
                // typecheck silently — the `Show f`-shaped obligation
                // would only surface at codegen as an `unknown variable`
                // error from the synthesised mono body.
                //
                // The substitution mirrors `instantiate`'s body-side
                // mapping: position-by-position pairing of `vars` with
                // the freshly-generated `metas`. The discharge path
                // post-`subst.apply` produces the same concrete type
                // that the App-arm unified into the metavars.
                let cmapping: BTreeMap<String, Type> = vars
                    .iter()
                    .cloned()
                    .zip(metas.iter().cloned())
                    .collect();
                for c in constraints {
                    let c_class = qualify_class_ref_in_check(&c.class, owner);
                    let c_ty = substitute_rigids(&c.type_, &cmapping);
                    // Look up the class's method name via the workspace
                    // class index; we need it for the `ResidualConstraint`'s
                    // `method` field (used by `NoInstance`'s rendering).
                    let method_name = env
                        .class_methods
                        .iter()
                        .find_map(|((cls, m), _)| {
                            if *cls == c_class { Some(m.clone()) } else { None }
                        })
                        .expect(
                            "class_methods registry coherence — a declared constraint's \
                             class is missing from env.class_methods. The pre-pass \
                             `MissingClass` diagnostic should have rejected this earlier; \
                             reaching here means workspace-registry / class-index drift. \
                             Surface to debug skill rather than silently render NoInstance \
                             with an empty method name.",
                        );
                    residuals.push(ResidualConstraint {
                        class: c_class,
                        type_: c_ty,
                        method: method_name,
                        candidates: None,
                    });
                }
                free_fn_calls.push(FreeFnCall {
                    name: unqualified_name.clone(),
                    owner_module: owner.clone(),
                    forall_vars: vars.clone(),
                    metas: metas.clone(),
                });
                return Ok(inst);
            }
            Ok(maybe_instantiate(raw, counter))
        }
        Term::App { callee, args, .. } => {
            let cty = synth(callee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            let cty = subst.apply(&cty);
            let (params, ret, fx) = match &cty {
                Type::Fn { params, ret, effects: fx, .. } => {
                    (params.clone(), (**ret).clone(), fx.clone())
                }
                Type::Forall { vars, constraints: _, body } => {
                    // Defensive — Var should already have instantiated.
                    let (_, body) = instantiate(vars, body, counter);
                    match &body {
                        Type::Fn { params, ret, effects: fx, .. } => {
                            (params.clone(), (**ret).clone(), fx.clone())
                        }
                        other => {
                            return Err(CheckError::NotAFunction(
                                callee_name(callee),
                                ailang_core::pretty::type_to_string(other),
                            ));
                        }
                    }
                }
                other => {
                    return Err(CheckError::NotAFunction(
                        callee_name(callee),
                        ailang_core::pretty::type_to_string(other),
                    ));
                }
            };
            if args.len() != params.len() {
                return Err(CheckError::ArityMismatch {
                    name: callee_name(callee),
                    expected: params.len(),
                    got: args.len(),
                });
            }
            for (a, exp) in args.iter().zip(params.iter()) {
                let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            let prev = locals.insert(name.clone(), v);
            let r = synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            unify(&Type::bool_(), &c, subst)?;
            let t1 = synth(then, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            let t2 = synth(else_, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                unify(exp, &actual, subst)?;
            }
            effects.insert(sig.effect.clone());
            Ok(sig.ret)
        }
        Term::Ctor { type_name, ctor, args } => {
            // Canonical-type-lookup: Term::Ctor lookup is direct post-canonical-type-form
            // Canonical type_name: bare = local TypeDef, qualified =
            // explicit cross-module. The imports-fallback (iter
            // 23.1.3) is gone — bare cross-module refs are rejected
            // upstream by the workspace validator (via the canonical-form validator).
            //
            // when the type is cross-module, `cdef.fields` is
            // written in the owning module's local namespace. A recursive
            // self-reference like `Cons a (List a)` carries `Con
            // { name: "List" }` even though, from the consumer's view,
            // the type is `std_list.List`. Apply `qualify_local_types`
            // with the owning module so that recursive ctor field types
            // (and any other locally-named cross-module type-cons) are
            // qualified before substitution / unification.
            let owning_module: Option<String>;
            let result_type_name: String = type_name.clone();
            let td = if type_name.matches('.').count() == 1 {
                let (prefix, suffix) = type_name.split_once('.').expect("checked");
                let target_module = match env.imports.get(prefix) {
                    Some(m) => m.clone(),
                    None => {
                        return Err(CheckError::UnknownModule {
                            module: prefix.to_string(),
                        });
                    }
                };
                let td = env.module_types
                    .get(&target_module)
                    .and_then(|tys| tys.get(suffix))
                    .cloned()
                    .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
                owning_module = Some(target_module);
                td
            } else if let Some(td) = env.types.get(type_name) {
                owning_module = None;
                td.clone()
            } else {
                return Err(CheckError::UnknownType(type_name.clone()));
            };
            let cdef = td
                .ctors
                .iter()
                .find(|c| &c.name == ctor)
                .ok_or_else(|| CheckError::UnknownCtor {
                    ty: type_name.clone(),
                    ctor: ctor.clone(),
                })?
                .clone();
            if args.len() != cdef.fields.len() {
                return Err(CheckError::CtorArity {
                    ty: type_name.clone(),
                    ctor: ctor.clone(),
                    expected: cdef.fields.len(),
                    got: args.len(),
                });
            }
            // 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(),
            };
            // 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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                unify(&exp_inst, &actual, subst)?;
            }
            Ok(Type::Con {
                name: result_type_name,
                args: type_args,
            })
        }
        Term::Match { scrutinee, arms } => {
            let s_ty = synth(scrutinee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                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 {
                // 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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            unify(&Type::unit(), &lty, subst)?;
            synth(rhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
        }
        Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
            // reject lambda-captures-of-loop-binder.
            // Walk the lambda body for free Vars (names not bound by
            // the lambda's own params) that match any loop binder on
            // the enclosing `loop_stack`. Loop binders are
            // alloca-resident and `std::mem::take`-emptied at the
            // lambda frame boundary in codegen — capturing one panics
            // `unreachable!()` at codegen, so the type checker rejects
            // it here instead. Reuses `desugar::free_vars_in_term`
            // (same walker `lift.rs` uses) which honours pattern
            // bindings inside `Term::Match` arms; gated on a non-empty
            // `loop_stack` so lambdas outside any loop typecheck
            // unchanged.
            if !loop_stack.is_empty() {
                let mut lam_bound: BTreeSet<String> = BTreeSet::new();
                for p in params {
                    lam_bound.insert(p.clone());
                }
                let mut frees: BTreeSet<String> = BTreeSet::new();
                ailang_core::desugar::free_vars_in_term(body, &lam_bound, &mut frees);
                for free_name in &frees {
                    for frame in loop_stack.iter() {
                        if frame.iter().any(|(n, _)| n == free_name) {
                            return Err(CheckError::LoopBinderCapturedByLambda {
                                name: free_name.clone(),
                            });
                        }
                    }
                }
            }

            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, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
            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 } => {
            // 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, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);

            // 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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
            match prev_in {
                Some(p) => {
                    locals.insert(name.clone(), p);
                }
                None => {
                    locals.shift_remove(name);
                }
            }
            in_ty
        }
        Term::Clone { value } => {
            // `(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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
        }
        Term::ReuseAs { source, body } => {
            // `(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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
            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::Loop { .. } => "loop",
                        Term::Recur { .. } => "recur",
                        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, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
        }
        // loop-recur iter 2: each binder init is synthed in the
        // outer scope plus already-declared binder names of THIS
        // loop (declaration order; later inits + body see earlier
        // binders via `locals`, exactly as `Term::Let` binds its
        // name). The loop's static type is the body's type. The
        // ordered binders (name + type) are pushed onto `loop_stack`
        // for the body walk so an inner `Term::Recur` can
        // position-check the types and `Term::Lam`'s escape guard
        // (iter loop-recur.tidy) can reject capture of a binder name;
        // popped on exit.
        Term::Loop { binders, body } => {
            let mut binder_frame: Vec<(String, Type)> = Vec::new();
            let mut restore: Vec<(String, Option<Type>)> = Vec::new();
            for b in binders {
                let init_ty = synth(
                    &b.init, env, locals, loop_stack, effects,
                    in_def, subst, counter, residuals, free_fn_calls, warnings,
                )?;
                unify(&b.ty, &init_ty, subst)?;
                binder_frame.push((b.name.clone(), b.ty.clone()));
                let prev = locals.insert(b.name.clone(), b.ty.clone());
                restore.push((b.name.clone(), prev));
            }
            loop_stack.push(binder_frame);
            let body_result = synth(
                body, env, locals, loop_stack, effects,
                in_def, subst, counter, residuals, free_fn_calls, warnings,
            );
            loop_stack.pop();
            for (name, prev) in restore.into_iter().rev() {
                match prev {
                    Some(p) => {
                        locals.insert(name, p);
                    }
                    None => {
                        locals.shift_remove(&name);
                    }
                }
            }
            body_result
        }
        // loop-recur iter 2: recur re-enters the innermost enclosing
        // loop, rebinding its binders positionally. RecurOutsideLoop
        // when `loop_stack` is empty; RecurArityMismatch on count
        // disagreement; RecurTypeMismatch via the Assign-style
        // subst-apply-then-structural-compare (Boss call 1) so the
        // dedicated code fires point-exactly. recur's OWN type is a
        // fresh metavar — it transfers control and never falls
        // through, so it unifies with whatever sibling branch the
        // enclosing if/match requires.
        Term::Recur { args } => {
            let binder_frame = match loop_stack.last() {
                None => return Err(CheckError::RecurOutsideLoop),
                Some(frame) => frame.clone(),
            };
            if args.len() != binder_frame.len() {
                return Err(CheckError::RecurArityMismatch {
                    expected: binder_frame.len(),
                    got: args.len(),
                });
            }
            for (i, a) in args.iter().enumerate() {
                let arg_ty = synth(
                    a, env, locals, loop_stack, effects,
                    in_def, subst, counter, residuals, free_fn_calls, warnings,
                )?;
                let applied_binder = subst.apply(&binder_frame[i].1);
                let applied_arg = subst.apply(&arg_ty);
                if applied_binder != applied_arg {
                    return Err(CheckError::RecurTypeMismatch {
                        position: i,
                        expected: ailang_core::pretty::type_to_string(&applied_binder),
                        got: ailang_core::pretty::type_to_string(&applied_arg),
                    });
                }
            }
            Ok(Subst::fresh(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, constraints: _, body } = &t {
        let (_, inst) = instantiate(vars, body, counter);
        inst
    } else {
        t
    }
}

/// 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 } => {
            // The first two branches share the body `name.clone()` but
            // express semantically distinct reasons (already qualified;
            // primitive needs no qualification). Combining them with
            // `||` would obscure why each disqualifies the name.
            #[allow(clippy::if_same_then_else)]
            let qualified_name = if name.contains('.') {
                name.clone()
            } else if ailang_core::primitives::is_primitive_name(name) {
                name.clone()
            } else if local_types.contains_key(name) {
                format!("{owner_module}.{name}")
            } else {
                name.clone()
            };
            Type::Con {
                name: qualified_name,
                args: args
                    .iter()
                    .map(|a| qualify_local_types(a, owner_module, local_types))
                    .collect(),
            }
        }
        Type::Fn { params, ret, effects, .. } => Type::Fn {
            params: params
                .iter()
                .map(|p| qualify_local_types(p, owner_module, local_types))
                .collect(),
            ret: Box::new(qualify_local_types(ret, owner_module, local_types)),
            effects: effects.clone(),
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        Type::Forall { vars, constraints, body } => Type::Forall {
            vars: vars.clone(),
            constraints: constraints
                .iter()
                .map(|c| Constraint {
                    class: c.class.clone(),
                    type_: qualify_local_types(&c.type_, owner_module, local_types),
                })
                .collect(),
            body: Box::new(qualify_local_types(body, owner_module, local_types)),
        },
        Type::Var { .. } => t.clone(),
    }
}

/// Checks a pattern against an expected type and returns the bindings
/// introduced by the pattern.
fn type_check_pattern(
    p: &Pattern,
    expected: &Type,
    env: &Env,
) -> Result<Vec<(String, Type)>> {
    match p {
        Pattern::Wild => Ok(vec![]),
        Pattern::Var { name } => Ok(vec![(name.clone(), expected.clone())]),
        Pattern::Lit { lit } => {
            let lt = match lit {
                Literal::Int { .. } => Type::int(),
                Literal::Bool { .. } => Type::bool_(),
                Literal::Str { .. } => Type::str_(),
                Literal::Unit => Type::unit(),
                Literal::Float { .. } => {
                    return Err(CheckError::FloatPatternNotAllowed);
                }
            };
            expect_eq(expected, &lt)?;
            Ok(vec![])
        }
        Pattern::Ctor { ctor, fields } => {
            // 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"
                        );
                    }
                }
            }
            // Canonical-type-pattern lookup: Pattern::Ctor lookup is type-driven post-canonical-type-form
            // The scrutinee's Type::Con name is canonical (bare = local
            // TypeDef, qualified = explicit cross-module). Derive the
            // TypeDef from `expected` and find the ctor by name within
            // it; no env.ctor_index consult, no imports-walk.
            let (resolved_type_name, resolved_td, resolved_owning_module, scrutinee_args) =
                match expected {
                    Type::Con { name, args } => {
                        if let Some((owner, suffix)) = name.split_once('.') {
                            let td = env
                                .module_types
                                .get(owner)
                                .and_then(|tys| tys.get(suffix))
                                .cloned()
                                .ok_or_else(|| {
                                    CheckError::PatternTypeMismatch {
                                        ctor: ctor.clone(),
                                        ty: ailang_core::pretty::type_to_string(expected),
                                    }
                                })?;
                            (name.clone(), td, Some(owner.to_string()), args.clone())
                        } else {
                            let td = env.types.get(name).cloned().ok_or_else(|| {
                                CheckError::PatternTypeMismatch {
                                    ctor: ctor.clone(),
                                    ty: ailang_core::pretty::type_to_string(expected),
                                }
                            })?;
                            (name.clone(), td, None, args.clone())
                        }
                    }
                    _ => {
                        return Err(CheckError::PatternTypeMismatch {
                            ctor: ctor.clone(),
                            ty: ailang_core::pretty::type_to_string(expected),
                        });
                    }
                };
            let td = &resolved_td;
            let cdef = td
                .ctors
                .iter()
                .find(|c| &c.name == ctor)
                .ok_or_else(|| CheckError::UnknownCtorInPattern(ctor.clone()))?;
            if fields.len() != cdef.fields.len() {
                return Err(CheckError::CtorArity {
                    ty: resolved_type_name.clone(),
                    ctor: ctor.clone(),
                    expected: cdef.fields.len(),
                    got: fields.len(),
                });
            }
            // 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`).
            //
            // when the resolved ctor lives in an imported
            // module, qualify any bare local type-cons in the field
            // types first — symmetric to the term-ctor fix.
            let qualified_fields: Vec<Type> = match &resolved_owning_module {
                Some(m) => {
                    let owner_types = env
                        .module_types
                        .get(m)
                        .cloned()
                        .unwrap_or_default();
                    cdef.fields
                        .iter()
                        .map(|f| qualify_local_types(f, m, &owner_types))
                        .collect()
                }
                None => cdef.fields.clone(),
            };
            let mapping: BTreeMap<String, Type> = td
                .vars
                .iter()
                .cloned()
                .zip(scrutinee_args)
                .collect();
            let mut out = Vec::new();
            for (sub, sub_ty) in fields.iter().zip(qualified_fields.iter()) {
                let sub_ty_inst = substitute_rigids(sub_ty, &mapping);
                out.extend(type_check_pattern(sub, &sub_ty_inst, env)?);
            }
            Ok(out)
        }
    }
}

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

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

/// Typechecker environment for a single module-check pass.
///
/// Cloned cheaply when we need a scoped extension (e.g. installing
/// rigid vars while checking a polymorphic def's body) so that the
/// parent scope stays immutable. Construction goes through
/// [`Env::default`] / the internal `new`; population is the
/// responsibility of [`builtins::install`] and the per-module setup in
/// `check_in_workspace`.
///
/// Several of the fields are conceptually disjoint name-spaces (term
/// vars vs effect ops vs ADT names vs ctor names), kept as separate
/// maps because the AST already commits to which channel a reference
/// goes through (`Term::Var` vs `Term::Do` vs `Term::Ctor` vs
/// `Pattern::Ctor`).
#[derive(Debug, Default, Clone)]
pub struct Env {
    /// Term-level names in scope — built-in operators, user fn/const
    /// defs of the current module, and (after pass-1) an entry per
    /// local def. Looked up by `Term::Var { name }` lookup.
    pub globals: IndexMap<String, Type>,
    /// Effect-op table. Looked up by `Term::Do { op }`. See
    /// [`builtins::EffectOpSig`] for the payload shape.
    pub effect_ops: IndexMap<String, builtins::EffectOpSig>,
    /// User-declared ADTs of the current module, by name. Populated
    /// from `Def::Type` entries; consulted by `Term::Ctor`,
    /// `Pattern::Ctor`, and the well-formedness check on declared
    /// types.
    pub types: IndexMap<String, TypeDef>,
    /// Inverse index: ctor name -> reference to the owning ADT.
    pub ctor_index: IndexMap<String, CtorRef>,
    /// Import map: alias-or-module-name → actual module name.
    /// Used when `Term::Var { name }` contains a dot
    /// (qualified cross-module reference).
    pub imports: BTreeMap<String, String>,
    /// Top-level symbol table per module of the workspace.
    /// Populated by [`crate::build_check_env`] from
    /// [`build_module_globals`].
    pub module_globals: BTreeMap<String, IndexMap<String, Type>>,
    /// Per-module import map: module-name → (alias-or-module-name →
    /// actual-module-name). Sibling-shape to [`Self::module_globals`];
    /// populated workspace-flat by [`crate::build_check_env`] so the
    /// mono pass's per-fn entry points can re-seed the local
    /// [`Self::imports`] before re-running `synth` on a body. Both
    /// `check_in_workspace` and `mono::build_workspace_env` consume
    /// the same env shape; `check_in_workspace` then overwrites
    /// [`Self::imports`] with the current module's map at the call
    /// site.
    pub module_imports: BTreeMap<String, BTreeMap<String, String>>,
    /// 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>,
    /// workspace-flat aggregate of every module's
    /// [`ModuleGlobals::class_methods`], re-keyed to
    /// `(qualified-class-name, method-name)` so post-retirement of
    /// `MethodNameCollision` two classes can share a method name.
    /// Consumed by `synth`'s `Term::Var` arm via the resolved class
    /// (from `method_to_candidate_classes` + dispatch) plus the method
    /// name. Mono's presence checks consult
    /// [`Self::method_to_candidate_classes`] (method-keyed natively).
    pub class_methods: BTreeMap<(String, String), ClassMethodEntry>,
    /// workspace-flat inverse of [`Self::class_methods`] — for
    /// each method name, the set of qualified class names that declare
    /// it. Pre-canonical-class-form, the `MethodNameCollision` invariant guarantees
    /// each set is singleton; the type-driven dispatch refactor lifts the invariant and any
    /// cardinality above one becomes legal. Synth's `Term::Var` arm
    /// consults this index for type-driven dispatch (spec
    /// §Architecture's 5-step rule).
    pub method_to_candidate_classes: BTreeMap<String, BTreeSet<String>>,
    /// post-superclass-expansion declared constraints of the
    /// active fn body being checked. Populated by `check_fn` before
    /// invoking `synth` on the body; empty at workspace entry.
    /// Consumed by `synth`'s Var-arm class-method branch when calling
    /// `resolve_method_dispatch` — the constraint-driven filter
    /// disambiguates multi-candidate residuals at the rigid-var
    /// fallback (e.g. inside a polymorphic fn body where the arg
    /// type is still a rigid type variable).
    pub active_declared_constraints: Vec<Constraint>,
    /// one-step superclass expansion table.
    /// Maps each class name to its superclass class name. Absence from
    /// the map means the class has no superclass — populated only for
    /// classes that declare one. Used by `check_fn` to expand
    /// `Forall.constraints` for the missing-constraint check (the
    /// typeclass design caps superclass expansion at one step). The
    /// schema permits at most one
    /// superclass per class.
    pub class_superclasses: BTreeMap<String, String>,
    /// workspace-wide instance registry, threaded
    /// through from [`Workspace::registry`]. Read by `check_fn` in the
    /// concrete-residual path: when a class-method call at a fully-
    /// concrete type produces a residual `(class, type_)` whose
    /// `(class, type_hash(type_))` key is absent from `registry.entries`,
    /// the fn fires `NoInstance`. Default-constructed (empty) for
    /// the standalone [`check_module`] entry point — pre-22b fixtures
    /// never invoke class methods, so the empty registry is harmless.
    pub workspace_registry: ailang_core::workspace::Registry,
}

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

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

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

    /// Helper that synths a single Term against a default empty env +
    /// fresh local / scope / effect state. Returns the substituted
    /// final type.
    fn synth_standalone(term: &Term) -> Type {
        let env = Env::default();
        let mut locals: IndexMap<String, Type> = IndexMap::new();
        // loop-recur iter 2: loop-free unit-test call site — fresh
        // empty loop-stack.
        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
        let mut effects: BTreeSet<String> = BTreeSet::new();
        let mut subst = Subst::default();
        let mut counter: u32 = 0;
        let mut residuals: Vec<ResidualConstraint> = Vec::new();
        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
        let mut warnings: Vec<Diagnostic> = Vec::new();
        let ty = synth(
            term,
            &env,
            &mut locals,
            &mut loop_stack,
            &mut effects,
            "<test>",
            &mut subst,
            &mut counter,
            &mut residuals,
            &mut free_fn_calls,
            &mut warnings,
        )
        .expect("synth must succeed");
        subst.apply(&ty)
    }

    /// `CheckError::LoopBinderCapturedByLambda`
    /// carries the stable kebab code `loop-binder-captured-by-lambda`
    /// and a non-panicking `ctx()` arm carrying the captured name —
    /// symmetric to `mut_var_captured_by_lambda_diagnostic_has_kebab_code`.
    #[test]
    fn loop_binder_captured_by_lambda_diagnostic_has_kebab_code() {
        let e = CheckError::LoopBinderCapturedByLambda { name: "acc".into() };
        assert_eq!(e.code(), "loop-binder-captured-by-lambda");
        let _ = e.ctx();
    }

    /// loop-recur iter 2: the four `Recur*` `CheckError` variants carry
    /// the exact stable kebab codes the spec acceptance mandates
    /// (`recur-outside-loop` / `recur-arity-mismatch` /
    /// `recur-type-mismatch` / `recur-not-in-tail-position`).
    #[test]
    fn recur_checkerror_codes_are_exact() {
        assert_eq!(CheckError::RecurOutsideLoop.code(), "recur-outside-loop");
        assert_eq!(
            CheckError::RecurArityMismatch { expected: 2, got: 1 }.code(),
            "recur-arity-mismatch"
        );
        assert_eq!(
            CheckError::RecurTypeMismatch {
                position: 0,
                expected: "Int".into(),
                got: "Bool".into(),
            }
            .code(),
            "recur-type-mismatch"
        );
        assert_eq!(
            CheckError::RecurNotInTailPosition.code(),
            "recur-not-in-tail-position"
        );
    }

    /// Regression guard — a lambda built without any enclosing loop
    /// typechecks unchanged. Property protected: the free-var scan in
    /// `Term::Lam`'s synth arm is gated on `!loop_stack.is_empty()`
    /// and must not disturb lambdas outside loops. The body refers to
    /// the lambda's own param (no builtin lookup needed) so the test
    /// stays pure in `Env::default()`.
    #[test]
    fn lambda_outside_loop_still_typechecks_clean() {
        let term = Term::Lam {
            params: vec!["x".into()],
            param_tys: vec![Type::int()],
            ret_ty: Box::new(Type::int()),
            effects: vec![],
            body: Box::new(Term::Var { name: "x".into() }),
        };
        let _ty = synth_standalone(&term);
    }

    /// a lambda nested inside a `Term::Loop`
    /// whose body references a loop binder declared by the enclosing
    /// loop is rejected with `LoopBinderCapturedByLambda`. The
    /// captured-name field reports the offending binder.
    #[test]
    fn lambda_inside_loop_capturing_binder_emits_loop_binder_captured_by_lambda() {
        // (loop (acc : Int = 0)
        //   (let f = (lam () : Int -> acc) in 0))
        let term = Term::Loop {
            binders: vec![ailang_core::ast::LoopBinder {
                name: "acc".into(),
                ty: Type::int(),
                init: Term::Lit { lit: Literal::Int { value: 0 } },
            }],
            body: Box::new(Term::Let {
                name: "f".into(),
                value: Box::new(Term::Lam {
                    params: vec![],
                    param_tys: vec![],
                    ret_ty: Box::new(Type::int()),
                    effects: vec![],
                    body: Box::new(Term::Var { name: "acc".into() }),
                }),
                body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
            }),
        };
        let env = Env::default();
        let mut locals: IndexMap<String, Type> = IndexMap::new();
        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
        let mut effects: BTreeSet<String> = BTreeSet::new();
        let mut subst = Subst::default();
        let mut counter: u32 = 0;
        let mut residuals: Vec<ResidualConstraint> = Vec::new();
        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
        let mut warnings: Vec<Diagnostic> = Vec::new();
        let err = synth(
            &term, &env, &mut locals, &mut loop_stack, &mut effects,
            "<test>", &mut subst, &mut counter, &mut residuals,
            &mut free_fn_calls, &mut warnings,
        )
        .expect_err("lambda capturing loop binder must be rejected");
        match err {
            CheckError::LoopBinderCapturedByLambda { name } => assert_eq!(name, "acc"),
            other => panic!("expected LoopBinderCapturedByLambda, got {other:?}"),
        }
    }

    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,
        export: 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_str".into(),
                    args: vec![Term::Lit {
                        lit: Literal::Str {
                            value: "hi".into(),
                        },
                    }],
                    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"));
    }

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

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

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

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

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

    /// ctor field type substitution and match-arm bindings.
    /// `unbox :: forall a. (Box<a>) -> a` extracts the wrapped value.
    #[test]
    fn parameterised_adt_polymorphic_unbox() {
        let box_def = Def::Type(TypeDef {
            name: "Box".into(),
            vars: vec!["a".into()],
            ctors: vec![Ctor {
                name: "MkBox".into(),
                fields: vec![Type::Var { name: "a".into() }],
            }],
            doc: None,
            drop_iterative: false,
        });
        let unbox = Def::Fn(FnDef {
            name: "unbox".into(),
            ty: Type::Forall {
                vars: vec!["a".into()],
                constraints: vec![],
                body: Box::new(Type::Fn {
                    params: vec![Type::Con {
                        name: "Box".into(),
                        args: vec![Type::Var { name: "a".into() }],
                    }],
                    ret: Box::new(Type::Var { name: "a".into() }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                }),
            },
            params: vec!["b".into()],
            body: Term::Match {
                scrutinee: Box::new(Term::Var { name: "b".into() }),
                arms: vec![Arm {
                    pat: Pattern::Ctor {
                        ctor: "MkBox".into(),
                        fields: vec![Pattern::Var { name: "x".into() }],
                    },
                    body: Term::Var { name: "x".into() },
                }],
            },
            suppress: vec![],
            doc: None,
        export: 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");
    }

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

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

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

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

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

    /// 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:?}");
    }

    /// 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:?}");
    }

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

    /// 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:?}");
    }

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

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

    /// 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_str".into(),
                                        args: vec![Term::Lit {
                                            lit: Literal::Str {
                                                value: "x".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");
    }

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

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

    /// `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:?}"),
        }
    }

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

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

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

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

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

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

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

    /// `==`'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"
        );
    }

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

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

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

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

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

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

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

    /// `AmbiguousMethodResolution` is the new check-time
    /// diagnostic for multi-candidate residuals that survive type-driven
    /// filtering at a monomorphic call site. Verifies the variant is
    /// constructible, its `code()` returns the structured-diagnostic key,
    /// and the Display surface names the candidate classes.
    #[test]
    fn mq2_ambiguous_method_resolution_display_and_code() {
        let err = CheckError::AmbiguousMethodResolution {
            method: "show".to_string(),
            at_type: "Int".to_string(),
            candidate_classes: vec![
                "prelude.Show".to_string(),
                "userlib.Show".to_string(),
            ],
        };
        assert_eq!(err.code(), "ambiguous-method-resolution");
        let rendered = format!("{}", err);
        assert!(rendered.contains("show"), "Display must echo method, got: {rendered}");
        assert!(rendered.contains("prelude.Show"), "Display must name candidate, got: {rendered}");
        assert!(rendered.contains("userlib.Show"), "Display must name candidate, got: {rendered}");
    }

    /// `UnknownClass` is the new check-time diagnostic for an
    /// explicit class qualifier in `Term::Var.name` that names a
    /// qualified class not in the workspace.
    #[test]
    fn mq2_unknown_class_display_and_code() {
        let err = CheckError::UnknownClass {
            name: "unknownlib.Show".to_string(),
        };
        assert_eq!(err.code(), "unknown-class");
        let rendered = format!("{}", err);
        assert!(rendered.contains("unknownlib.Show"), "Display must echo the qualified name, got: {rendered}");
    }

    /// `NoInstance` carries an additive `candidate_classes`
    /// list. When non-empty, the rendered ctx() carries the candidate
    /// list; when empty, the ctx() shape is unchanged from pre-canonical-class-form
    /// form (backwards compatible for single-class call sites).
    #[test]
    fn mq2_no_instance_with_candidate_classes_renders() {
        let err = CheckError::NoInstance {
            def: "f".to_string(),
            class: "prelude.Show".to_string(),
            method: "show".to_string(),
            at_type: "MyType".to_string(),
            candidate_classes: vec![
                "prelude.Show".to_string(),
                "userlib.Show".to_string(),
            ],
        };
        let rendered = format!("{}", err);
        assert!(rendered.contains("show"), "Display must echo method, got: {rendered}");
        assert!(rendered.contains("MyType"), "Display must echo type, got: {rendered}");
        let ctx = err.ctx();
        assert_eq!(ctx["candidate_classes"][0], "prelude.Show");
        assert_eq!(ctx["candidate_classes"][1], "userlib.Show");
    }

    /// empty `candidate_classes` keeps the existing single-class
    /// ctx() shape — no `candidate_classes` key in the JSON.
    #[test]
    fn mq2_no_instance_empty_candidates_back_compat() {
        let err = CheckError::NoInstance {
            def: "f".to_string(),
            class: "prelude.Show".to_string(),
            method: "show".to_string(),
            at_type: "MyType".to_string(),
            candidate_classes: vec![],
        };
        let rendered = format!("{}", err);
        assert!(rendered.contains("prelude.Show"), "Display must echo class, got: {rendered}");
        let ctx = err.ctx();
        assert!(ctx.get("candidate_classes").is_none(),
            "empty candidate_classes must not render in ctx; got: {ctx}");
    }

    /// `ResidualConstraint` carries an optional candidate-class
    /// set for the multi-candidate dispatch path. `None` preserves the
    /// pre-canonical-class-form single-class semantics (the `class` field is the
    /// resolved class). `Some(...)` carries the candidate set; the
    /// `class` field's content is a tentative value until discharge
    /// resolves it.
    #[test]
    fn mq2_residual_constraint_candidates_field_exists() {
        let single = ResidualConstraint {
            class: "prelude.Eq".to_string(),
            type_: Type::Con { name: "Int".to_string(), args: vec![] },
            method: "eq".to_string(),
            candidates: None,
        };
        assert!(single.candidates.is_none());

        let mut multi_set = std::collections::BTreeSet::new();
        multi_set.insert("prelude.Show".to_string());
        multi_set.insert("userlib.Show".to_string());
        let multi = ResidualConstraint {
            class: "prelude.Show".to_string(),
            type_: Type::Con { name: "Int".to_string(), args: vec![] },
            method: "show".to_string(),
            candidates: Some(multi_set.clone()),
        };
        assert_eq!(multi.candidates, Some(multi_set));
    }

    /// smoke test on `parse_method_qualifier` — the helper
    /// underpinning the rewritten synth Var-arm. Bare names pass
    /// through with `None` qualifier; dotted names split at the last
    /// dot so the prefix is the (possibly-multi-dot) class qualifier.
    #[test]
    fn mq2_parse_method_qualifier_smoke() {
        assert_eq!(parse_method_qualifier("show"), ("show", None));
        assert_eq!(
            parse_method_qualifier("prelude.Show.show"),
            ("show", Some("prelude.Show".to_string()))
        );
        assert_eq!(
            parse_method_qualifier("std_list.length"),
            ("length", Some("std_list".to_string()))
        );
    }

    /// a multi-candidate residual with a concrete `type_`
    /// resolved post-unification to `Int` is filtered against the
    /// registry. Single survivor → Resolved.
    #[test]
    fn mq2_discharge_multi_candidate_concrete_type_single_survivor() {
        let mut candidates = BTreeSet::new();
        candidates.insert("prelude.Show".to_string());
        candidates.insert("userlib.Show".to_string());
        let residual = ResidualConstraint {
            class: "prelude.Show".to_string(), // tentative
            type_: Type::Con { name: "Int".to_string(), args: vec![] },
            method: "show".to_string(),
            candidates: Some(candidates),
        };
        let mut registry: BTreeMap<(String, String), ()> = BTreeMap::new();
        let int_h = ailang_core::canonical::type_hash(
            &Type::Con { name: "Int".to_string(), args: vec![] }
        );
        registry.insert(("prelude.Show".to_string(), int_h), ());

        let outcome = refine_multi_candidate_residual(
            &residual,
            /*declared_constraints*/ &[],
            /*registry*/ &registry,
        );
        assert_eq!(outcome, RefineOutcome::Resolved("prelude.Show".to_string()));
    }

    /// zero registry survivors → NoInstance with the full
    /// candidate-class set echoed back to the author.
    #[test]
    fn mq2_discharge_multi_candidate_concrete_type_zero_survivors_no_instance() {
        let mut candidates = BTreeSet::new();
        candidates.insert("prelude.Show".to_string());
        candidates.insert("userlib.Show".to_string());
        let residual = ResidualConstraint {
            class: "prelude.Show".to_string(),
            type_: Type::Con { name: "MyType".to_string(), args: vec![] },
            method: "show".to_string(),
            candidates: Some(candidates.clone()),
        };
        let registry: BTreeMap<(String, String), ()> = BTreeMap::new();
        let outcome = refine_multi_candidate_residual(&residual, &[], &registry);
        match outcome {
            RefineOutcome::NoInstance { candidate_classes, .. } => {
                assert_eq!(candidate_classes.len(), 2);
            }
            other => panic!("expected NoInstance, got {other:?}"),
        }
    }

    /// multi survivors → AmbiguousMethodResolution.
    #[test]
    fn mq2_discharge_multi_candidate_concrete_type_multi_survivors_ambiguous() {
        let mut candidates = BTreeSet::new();
        candidates.insert("prelude.Show".to_string());
        candidates.insert("userlib.Show".to_string());
        let residual = ResidualConstraint {
            class: "prelude.Show".to_string(),
            type_: Type::Con { name: "Int".to_string(), args: vec![] },
            method: "show".to_string(),
            candidates: Some(candidates.clone()),
        };
        let mut registry: BTreeMap<(String, String), ()> = BTreeMap::new();
        let int_h = ailang_core::canonical::type_hash(
            &Type::Con { name: "Int".to_string(), args: vec![] }
        );
        registry.insert(("prelude.Show".to_string(), int_h.clone()), ());
        registry.insert(("userlib.Show".to_string(), int_h), ());
        let outcome = refine_multi_candidate_residual(&residual, &[], &registry);
        match outcome {
            RefineOutcome::Ambiguous { candidate_classes, .. } => {
                assert_eq!(candidate_classes.len(), 2);
            }
            other => panic!("expected Ambiguous, got {other:?}"),
        }
    }

    /// `Env` carries a workspace-flat
    /// `method_to_candidate_classes: BTreeMap<String, BTreeSet<String>>`
    /// inverse map of `class_methods`. Today's `MethodNameCollision`
    /// invariant guarantees each set is singleton; post-canonical-class-form the
    /// cardinality > 1 case becomes legal.
    #[test]
    fn mq2_env_method_to_candidate_classes_built() {
        use ailang_core::ast::{ClassDef, ClassMethod, Module};
        let m = Module {
            schema: SCHEMA.into(),
            name: "m".to_string(),
            imports: vec![],
            defs: vec![Def::Class(ClassDef {
                name: "MyShow".to_string(),
                param: "a".to_string(),
                superclass: None,
                methods: vec![ClassMethod {
                    name: "myshow".to_string(),
                    ty: Type::Fn {
                        params: vec![Type::Var { name: "a".to_string() }],
                        param_modes: vec![ParamMode::Borrow],
                        ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }),
                        effects: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    default: None,
                }],
                doc: None,
            })],
        };
        let mut modules = BTreeMap::new();
        modules.insert("m".into(), m);
        let ws = Workspace {
            entry: "m".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let env = build_check_env(&ws);
        let candidates = env.method_to_candidate_classes.get("myshow")
            .expect("method_to_candidate_classes must contain `myshow`");
        assert!(candidates.contains("m.MyShow"), "candidates: {candidates:?}");
        assert_eq!(candidates.len(), 1, "MethodNameCollision invariant: singleton");
    }

    /// `Env` carries an `active_declared_constraints` field
    /// holding the active fn's POST-superclass-expansion declared
    /// constraints. Empty at workspace entry; populated by `check_fn`
    /// before invoking `synth` on the fn body. Consumed by `synth`'s
    /// Var-arm class-method branch when calling `resolve_method_dispatch`
    /// (constraint-driven filter path).
    #[test]
    fn mq3_env_active_declared_constraints_field_exists() {
        let env = Env::default();
        assert_eq!(env.active_declared_constraints.len(), 0,
            "active_declared_constraints empty at default-construction");
    }

    /// when synth's Var-arm resolves a name to a free fn
    /// (locals / caller-module-fn / implicit-import fn) AND the same
    /// method name has class-method candidates in the workspace, a
    /// structured warning `class-method-shadowed-by-fn` is emitted
    /// via the warnings out-parameter. The fn resolution proceeds;
    /// the warning surfaces the shadow so the LLM-author can
    /// disambiguate via explicit class-qualified call if the shadow
    /// was unintentional.
    #[test]
    fn mq3_class_method_shadowed_by_fn_warning_fires() {
        use ailang_core::ast::{ClassDef, ClassMethod, Module};
        // Synthesise a workspace with `class Show { show: a -> Str }`
        // in module `clsmod` and `fn show : (Int) -> Str` in module
        // `fnmod`. Module `m` imports both implicitly; `synth` on
        // `Term::Var { name: "show" }` should resolve to the fn AND
        // emit the shadow warning.
        let clsmod = Module {
            schema: SCHEMA.into(),
            name: "clsmod".into(),
            imports: vec![],
            defs: vec![Def::Class(ClassDef {
                name: "Show".into(),
                param: "a".into(),
                superclass: None,
                methods: vec![ClassMethod {
                    name: "show".into(),
                    ty: Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        param_modes: vec![ParamMode::Borrow],
                        ret: Box::new(Type::str_()),
                        effects: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    default: None,
                }],
                doc: None,
            })],
        };
        let show_fn_ty = Type::Fn {
            params: vec![Type::int()],
            param_modes: vec![ParamMode::Borrow],
            ret: Box::new(Type::str_()),
            effects: vec![],
            ret_mode: ParamMode::Implicit,
        };
        let fnmod = Module {
            schema: SCHEMA.into(),
            name: "fnmod".into(),
            imports: vec![],
            defs: vec![Def::Fn(FnDef {
                name: "show".into(),
                ty: show_fn_ty.clone(),
                params: vec!["x".into()],
                body: Term::Lit { lit: Literal::Str { value: "_".into() } },
                doc: None,
                suppress: vec![],
            export: None,
            })],
        };
        let mut modules = BTreeMap::new();
        modules.insert("clsmod".into(), clsmod);
        modules.insert("fnmod".into(), fnmod);
        // mq.tidy T3: post-tightening, the warning fires only when at
        // least one candidate class has an instance in the workspace
        // registry. Ship a `clsmod.Show Int` instance so the fixture
        // continues to assert positive-fire behaviour under the
        // post-tidy spec rule.
        let mut registry = ailang_core::workspace::Registry::default();
        let int_h = ailang_core::canonical::type_hash(&Type::int());
        registry.entries.insert(
            ("clsmod.Show".into(), int_h),
            ailang_core::workspace::RegistryEntry {
                instance: ailang_core::ast::InstanceDef {
                    class: "clsmod.Show".into(),
                    type_: Type::int(),
                    methods: vec![],
                    doc: None,
                },
                defining_module: "clsmod".into(),
            },
        );
        let ws = Workspace {
            entry: "fnmod".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry,
        };
        let mut env = build_check_env(&ws);
        // Treat both modules as implicitly imported by `env.imports`
        // (the test-only equivalent of the prelude-injection convention).
        env.imports.insert("clsmod".into(), "clsmod".into());
        env.imports.insert("fnmod".into(), "fnmod".into());
        env.current_module = "fnmod".into();

        let term = Term::Var { name: "show".into() };
        let mut locals: IndexMap<String, Type> = IndexMap::new();
        // loop-recur iter 2: loop-free unit-test call site — fresh
        // empty loop-stack.
        let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
        let mut effects: BTreeSet<String> = BTreeSet::new();
        let mut subst = Subst::default();
        let mut counter: u32 = 0;
        let mut residuals: Vec<ResidualConstraint> = Vec::new();
        let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
        let mut warnings: Vec<crate::diagnostic::Diagnostic> = Vec::new();
        let _ = synth(
            &term,
            &env,
            &mut locals,
            &mut loop_stack,
            &mut effects,
            "test_call_site",
            &mut subst,
            &mut counter,
            &mut residuals,
            &mut free_fn_calls,
            &mut warnings,
        )
        .expect("synth must succeed (fn wins precedence)");
        assert!(
            warnings.iter().any(|d| d.code == "class-method-shadowed-by-fn"),
            "expected at least one class-method-shadowed-by-fn warning, got: {warnings:?}",
        );
    }

    /// `Env.class_methods` is keyed by `(QualifiedClassName,
    /// MethodName)` tuple — post-canonical-class-form the workspace can carry multiple
    /// classes sharing a method name, so the key must disambiguate.
    /// O(1) lookup post-dispatch via `(resolved_class, method)`.
    #[test]
    fn mq3_env_class_methods_tuple_keyed() {
        use ailang_core::ast::{ClassDef, ClassMethod, Module};
        let m = Module {
            schema: SCHEMA.into(),
            name: "m".to_string(),
            imports: vec![],
            defs: vec![Def::Class(ClassDef {
                name: "MyCls".to_string(),
                param: "a".to_string(),
                superclass: None,
                methods: vec![ClassMethod {
                    name: "mymethod".to_string(),
                    ty: Type::Fn {
                        params: vec![Type::Var { name: "a".to_string() }],
                        param_modes: vec![ParamMode::Borrow],
                        ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }),
                        effects: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    default: None,
                }],
                doc: None,
            })],
        };
        let mut modules = BTreeMap::new();
        modules.insert("m".into(), m);
        let ws = Workspace {
            entry: "m".into(),
            modules,
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let env = build_check_env(&ws);
        let key = ("m.MyCls".to_string(), "mymethod".to_string());
        assert!(env.class_methods.contains_key(&key),
                "env.class_methods must contain {key:?}");
    }

    /// mq.tidy T1: discharge-time rigid-var refinement must filter
    /// declared constraints by BOTH class-name match AND
    /// type-unification with the residual's `type_` (spec
    /// §"Constraint-discharge refinement" lines 130-138). Two
    /// same-class declared constraints on different typevars must
    /// be discriminated by the residual's actual typevar identity.
    #[test]
    fn mq_tidy_rigid_var_filter_uses_type_unification() {
        use ailang_core::ast::Constraint;

        // Candidate set: two distinct classes both named "Show".
        let mut candidates = BTreeSet::new();
        candidates.insert("prelude.Show".to_string());
        candidates.insert("userlib.Show".to_string());

        // Residual on Var "a".
        let residual = ResidualConstraint {
            class: "prelude.Show".to_string(),
            type_: Type::Var { name: "a".to_string() },
            method: "show".to_string(),
            candidates: Some(candidates),
        };

        // Declared: prelude.Show a (matches residual type),
        // userlib.Show b (does NOT match residual type).
        let declared = vec![
            Constraint {
                class: "prelude.Show".to_string(),
                type_: Type::Var { name: "a".to_string() },
            },
            Constraint {
                class: "userlib.Show".to_string(),
                type_: Type::Var { name: "b".to_string() },
            },
        ];

        let registry: BTreeMap<(String, String), ()> = BTreeMap::new();
        let outcome = refine_multi_candidate_residual(&residual, &declared, &registry);

        assert_eq!(
            outcome,
            RefineOutcome::Resolved("prelude.Show".to_string()),
            "type-unification leg must drop userlib.Show because its declared type (Var b) does not match the residual type (Var a)"
        );
    }

    /// mq.tidy T2: the synth Var-arm's class-method dispatch entry
    /// gates on a qualifier-shape predicate. The predicate must
    /// accept three shapes — bare-method (None), bare-class
    /// PascalCase qualifier (`"Show"`), module-qualified class
    /// qualifier (`"prelude.Show"`) — and reject bare-fn
    /// qualifiers (`"std_list"`, lowercase, no inner dot) which
    /// belong to the cross-module-fn arm.
    #[test]
    fn mq_tidy_bare_class_qualifier_shape_accepted() {
        assert!(qualifier_is_class_shape(&None));
        assert!(qualifier_is_class_shape(&Some("Show".to_string())));
        assert!(qualifier_is_class_shape(&Some("prelude.Show".to_string())));

        // Bare fn qualifier (lowercase, no inner dot) — NOT class-shape.
        assert!(!qualifier_is_class_shape(&Some("std_list".to_string())));
    }

    /// mq.tidy T3: the `class-method-shadowed-by-fn` warning fires
    /// only when at least one candidate class has a registry
    /// instance (any type) per spec §"Class-fn collisions" 161-162.
    /// Without this conservative-tightening, the warning fires
    /// unconditionally on `method_to_candidate_classes` presence,
    /// including class methods with zero instances anywhere.
    #[test]
    fn mq_tidy_shadow_warning_suppressed_when_no_instance() {
        let mut method_to_candidate_classes: BTreeMap<String, BTreeSet<String>> =
            BTreeMap::new();
        let mut foo_cands = BTreeSet::new();
        foo_cands.insert("userlib.Foo".to_string());
        method_to_candidate_classes.insert("foo".to_string(), foo_cands);

        // Empty registry → no candidate class has an instance → false.
        let empty_registry: BTreeMap<(String, String), ()> = BTreeMap::new();
        assert!(!any_candidate_class_has_instance(
            &method_to_candidate_classes,
            &empty_registry,
            "foo",
        ));

        // Add one instance for userlib.Foo → true.
        let mut registry_with_inst: BTreeMap<(String, String), ()> = BTreeMap::new();
        registry_with_inst.insert(
            ("userlib.Foo".to_string(), "Int_hash".to_string()),
            (),
        );
        assert!(any_candidate_class_has_instance(
            &method_to_candidate_classes,
            &registry_with_inst,
            "foo",
        ));
    }
}