//! LLVM IR text emitter for AILang (MVP).
//!
//! Third stage of the compiler pipeline (`core` → `check` → `codegen`
//! → `ail` CLI). Consumes a fully type-checked [`Module`] (single-file
//! mode) or [`Workspace`] (multi-module mode) and produces LLVM IR as
//! a UTF-8 string ready to be written as a `.ll` file and handed to
//! `clang`. The two entry points are [`emit_ir`] (single module) and
//! [`lower_workspace`] (multi-module); both share the same mangling
//! scheme and ABI.
//!
//! Strategy: we generate LLVM IR as a string, write it as `.ll`, and
//! link it with `clang`. No binding to a specific libllvm version.
//!
//! Type mapping:
//! - `Int` -> `i64`
//! - `Bool` -> `i1`
//! - `Unit` -> `i8` (value always 0)
//!
//! Mangling scheme (Iter 5c):
//! - **All** AILang functions become `@ail_<module>_<def>`. This holds
//!   even for single-module programs. The old form `@ail_<def>` is gone.
//! - Global string/constant symbols are mangled per module:
//!   `@.str_<module>_<idx>` and `@ail_<module>_<def>` for constant globals.
//! - The entry point remains `main` (LLVM/C ABI). [`lower_workspace`]
//!   emits `define i64 @main() { call @ail_<entry-module>_main() ... }`
//!   as a trampoline to the entry module's `main`. If missing, the
//!   build fails with [`CodegenError::MissingEntryMain`].
//! - `source_filename` appears exactly once at the top, with
//!   `<entry-module>.ail` as value (per workspace).
//!
//! **Precondition.** Neither [`emit_ir`] nor [`lower_workspace`] runs
//! the typechecker. Callers must have run `ailang_check::check_module`
//! (or `check_workspace`) first; codegen will panic or emit malformed
//! IR if invariants the checker enforces (resolved metavars, declared
//! effects, ctor arity) are violated.

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

mod escape;
use escape::NonEscapeSet;

/// Failure modes of [`emit_ir`] / [`lower_workspace`].
///
/// Most variants signal a compiler invariant violation rather than a
/// user-facing diagnostic — by the time a module reaches codegen the
/// typechecker has already accepted it. The exceptions are
/// [`CodegenError::MissingEntryMain`] (a workspace-level shape check
/// that the typechecker doesn't enforce) and the wrapping variants
/// [`CodegenError::Def`] / [`CodegenError::InModule`] which add path
/// context to an inner error.
#[derive(Debug, thiserror::Error)]
pub enum CodegenError {
    /// Wraps an inner error with the name of the def being lowered.
    /// Attached by the per-def lowering loop in [`lower_workspace`] so
    /// the failing definition is named in the message even when the
    /// underlying error is structural (e.g. an [`CodegenError::Internal`]
    /// from deep inside `lower_term`).
    #[error("def `{0}`: {1}")]
    Def(String, Box<CodegenError>),

    /// Wraps an inner error with the name of the module being lowered.
    /// Attached by [`lower_workspace`]'s per-module loop so multi-module
    /// builds report which module failed without requiring the caller
    /// to thread a module name through every call site.
    #[error("module `{0}`: {1}")]
    InModule(String, Box<CodegenError>),

    /// `llvm_type` was asked to lower an AILang [`Type`] it does not
    /// know how to represent. In the MVP this fires for an unresolved
    /// rigid `Type::Var` reaching codegen (a substitution bug; see
    /// Iter 13b notes in `DESIGN.md`) or for any non-`Con`/`Fn`/`Var`
    /// shape that has not yet been wired through.
    #[error("unsupported type: {0}")]
    UnsupportedType(String),

    /// A `Term::Var { name }` could not be resolved against the local
    /// SSA stack, the current module's top-level fns, or a qualified
    /// import. A correctly type-checked module never produces this; if
    /// it does, the typechecker and the codegen-side resolver have
    /// drifted out of sync.
    #[error("unknown variable: `{0}`")]
    UnknownVar(String),

    /// A `Def::Fn` was reached whose `ty` is not a `Type::Fn`. The
    /// typechecker ([`ailang_check::CheckError::FnTypeRequired`]) should
    /// have rejected this case before us; emit_fn re-checks defensively
    /// because a stale typechecker contract would otherwise produce
    /// malformed IR.
    #[error("expected fn type, got {0}")]
    NotFnType(String),

    /// The entry module of the workspace has no `main : () -> Unit !IO`
    /// def, so [`lower_workspace`] cannot emit the C-ABI trampoline.
    /// This is a workspace-level shape requirement that the typechecker
    /// does not enforce (a library module is well-typed without a main),
    /// so it surfaces here instead.
    #[error("entry module `{0}` has no `main` def")]
    MissingEntryMain(String),

    /// Catch-all for codegen-side invariant violations: missing
    /// ctor entry, lambda environment shape mismatch, mono-queue
    /// inconsistency, etc. The string carries the precise diagnostic;
    /// a user-facing build never produces this if the workspace
    /// type-checks cleanly.
    #[error("internal: {0}")]
    Internal(String),
}

type Result<T> = std::result::Result<T, CodegenError>;

/// Bench iter: which heap-allocation runtime the emitted IR targets.
///
/// `Gc` is the default (Boehm conservative GC, Decision 9 / Iter 14f).
/// `Bump` swaps every `@GC_malloc` for `@bump_malloc`, which is supplied
/// by `runtime/bump.c` — a no-free, statically-sized arena allocator
/// used purely to quantify the GC's overhead via an A/B comparison.
/// The IR is otherwise byte-identical between the two strategies.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AllocStrategy {
    Gc,
    Bump,
}

impl Default for AllocStrategy {
    fn default() -> Self {
        AllocStrategy::Gc
    }
}

impl AllocStrategy {
    /// LLVM IR-level name of the allocator fn (without leading `@`).
    fn fn_name(self) -> &'static str {
        match self {
            AllocStrategy::Gc => "GC_malloc",
            AllocStrategy::Bump => "bump_malloc",
        }
    }
}

/// Single-module entry point. Lowers `m` to a `.ll` string with `m`
/// itself as the entry module. Returns the full LLVM IR text, ready to
/// be written to disk and handed to `clang`.
///
/// Used by tests, by `ail emit-ir`, and by `ail build`/`run` whenever
/// the input is a single `.ail.json` file rather than a workspace.
/// Internally builds a trivial [`Workspace`] containing only `m` and
/// delegates to [`lower_workspace`] — the mangling scheme,
/// `source_filename`, and the `@main` trampoline are therefore
/// identical between the two entry points.
///
/// **Precondition.** `m` must already type-check. This function does
/// **not** call `ailang_check`; passing a module with unresolved
/// metavars, undeclared effects, or arity mismatches will produce
/// either a [`CodegenError`] or malformed IR. For any input that came
/// from disk, run `ailang_check::check_module(m)` first and only call
/// `emit_ir` when the diagnostic list is empty.
///
/// Use [`lower_workspace`] instead when the program spans multiple
/// modules (cross-module calls, transitive imports) — `emit_ir` is the
/// short-cut for the single-file demo case.
pub fn emit_ir(m: &Module) -> Result<String> {
    // Iter 16a: nested ctor patterns are desugared inside
    // `lower_workspace`, so single-module callers go through the
    // same code path with no extra work here.
    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("."),
    };
    lower_workspace(&ws)
}

/// Bench iter: variant of [`lower_workspace`] that selects the heap
/// allocator at codegen time. `AllocStrategy::Gc` produces IR
/// byte-identical to [`lower_workspace`]; `AllocStrategy::Bump` swaps
/// every `@GC_malloc` site for `@bump_malloc` (supplied by
/// `runtime/bump.c`). Used by `ail build --alloc=bump` to quantify the
/// GC's runtime overhead via an A/B comparison.
pub fn lower_workspace_with_alloc(ws: &Workspace, alloc: AllocStrategy) -> Result<String> {
    lower_workspace_inner(ws, alloc)
}

/// Multi-module entry point. Lowers an entire [`Workspace`] (entry
/// module plus its transitive imports, as produced by
/// `ailang_core::load_workspace`) to a single `.ll` string and emits
/// the C-ABI `@main` trampoline pointing at the entry module's `main`.
/// This is what `ail build` and `ail run` call for any real
/// multi-module program.
///
/// Module order is alphabetic (BTreeMap order = deterministic). Within
/// a module, def order matches the AST.
///
/// Cross-module calls: `Term::Var { name }` with exactly one dot
/// (`<prefix>.<def>`) is resolved via the calling module's import map
/// to `@ail_<actual_module>_<def>`. Local var lookups (no dot) stay
/// stack locals or local top-level defs of the current module.
///
/// **Precondition.** Every module in `ws.modules` must already
/// type-check (`ailang_check::check_workspace(ws)` returns no errors).
/// `lower_workspace` does **not** invoke the typechecker itself;
/// running it on an unchecked workspace is a caller bug. Beyond
/// type-checking, this function additionally requires that the entry
/// module declares `main : () -> Unit !IO` — otherwise it returns
/// [`CodegenError::MissingEntryMain`].
///
/// Use [`emit_ir`] for the single-file shortcut when there are no
/// imports.
pub fn lower_workspace(ws: &Workspace) -> Result<String> {
    lower_workspace_inner(ws, AllocStrategy::Gc)
}

fn lower_workspace_inner(ws: &Workspace, alloc: AllocStrategy) -> Result<String> {
    // Iter 16a: desugar every module before any lowering work runs.
    // The pass is idempotent and structurally identical to what
    // `ailang-check` runs at its public entries, so the codegen
    // sees the same flat-pattern AST as the typechecker.
    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(),
    };
    let ws = &ws_owned;
    let mut header = String::new();
    let mut body = String::new();
    let mut all_strings: BTreeMap<String, Vec<(String, String)>> = BTreeMap::new();
    // ^ per module: list of (global-name, content). Order = insertion order.

    // Pass 1: per-module top-level symbol tables.
    // - `module_user_fns`: LLVM-typed FnSig for monomorphic fns. Used by
    //   the call resolver. Polymorphic fns are deliberately excluded —
    //   they don't have a single LLVM signature; specialised entries
    //   appear here on demand during monomorphisation (Iter 12b).
    // - `module_def_ail_types`: AILang `Type` for every fn-typed def
    //   (poly or mono). Used by the codegen-side type tracker to derive
    //   substitutions at polymorphic call sites and to look up the
    //   original `Forall` body when specialising.
    let mut module_user_fns: BTreeMap<String, BTreeMap<String, FnSig>> = BTreeMap::new();
    let mut module_def_ail_types: BTreeMap<String, BTreeMap<String, Type>> = BTreeMap::new();
    let mut module_polymorphic_fns: BTreeMap<String, BTreeMap<String, FnDef>> = BTreeMap::new();
    // Iter 15a: cross-module ctor table. Maps module name → ctor name →
    // CtorRef (with `type_name` *unqualified*, since the ctor is defined
    // in that module). Cross-module ctor lookups resolve through this
    // table instead of the per-Emitter `ctor_index`.
    let mut module_ctor_index: BTreeMap<String, BTreeMap<String, CtorRef>> = BTreeMap::new();
    // Iter 15b: per-module const table. Used to resolve `Term::Var`
    // references to const defs (literal or non-literal) at lowering
    // time. Literal consts emit a global and are loaded; non-literal
    // consts (e.g. ctor expressions) are inlined at every reference
    // site since check_const guarantees their bodies are pure.
    let mut module_consts: BTreeMap<String, BTreeMap<String, ConstDef>> = BTreeMap::new();
    for (mname, m) in &ws.modules {
        let mut user_fns = BTreeMap::new();
        let mut ail_types = BTreeMap::new();
        let mut poly_fns = BTreeMap::new();
        let mut ctors = BTreeMap::new();
        for def in &m.defs {
            if let Def::Fn(f) = def {
                ail_types.insert(f.name.clone(), f.ty.clone());
                match &f.ty {
                    Type::Fn { params, ret, .. } => {
                        let psig: Result<Vec<String>> = params.iter().map(llvm_type).collect();
                        let rsig = llvm_type(ret);
                        if let (Ok(params), Ok(ret)) = (psig, rsig) {
                            user_fns.insert(f.name.clone(), FnSig { params, ret });
                        }
                    }
                    Type::Forall { .. } => {
                        // Polymorphic def — no LLVM sig now; specialised
                        // versions get queued as call sites are lowered.
                        poly_fns.insert(f.name.clone(), f.clone());
                    }
                    _ => {}
                }
            }
            if let Def::Type(td) = def {
                for (i, c) in td.ctors.iter().enumerate() {
                    let fields: Vec<String> = c
                        .fields
                        .iter()
                        .map(|t| llvm_type(t).unwrap_or_else(|_| "ptr".into()))
                        .collect();
                    ctors.insert(
                        c.name.clone(),
                        CtorRef {
                            type_name: td.name.clone(),
                            tag: i as u32,
                            fields,
                            ail_fields: c.fields.clone(),
                            type_vars: td.vars.clone(),
                        },
                    );
                }
            }
        }
        // Iter 15b: collect const defs for this module so non-literal
        // consts can be inlined at `Term::Var` reference sites.
        let mut consts: BTreeMap<String, ConstDef> = BTreeMap::new();
        for def in &m.defs {
            if let Def::Const(c) = def {
                consts.insert(c.name.clone(), c.clone());
            }
        }
        module_user_fns.insert(mname.clone(), user_fns);
        module_def_ail_types.insert(mname.clone(), ail_types);
        module_polymorphic_fns.insert(mname.clone(), poly_fns);
        module_ctor_index.insert(mname.clone(), ctors);
        module_consts.insert(mname.clone(), consts);
    }

    // Pass 2: lower per module. Globals/strings are accumulated per module,
    // because they are mangled per module.
    for (mname, m) in &ws.modules {
        // Import map for cross-module resolution. Identical to the
        // logic in the typechecker (see `check_in_workspace`): alias or
        // module name as key, actual module name as value.
        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());
        }

        let mut emitter = Emitter::new(
            m,
            mname,
            &module_user_fns,
            &module_def_ail_types,
            &module_polymorphic_fns,
            &module_ctor_index,
            &module_consts,
            import_map,
            alloc,
        );
        emitter
            .emit_module()
            .map_err(|e| CodegenError::InModule(mname.clone(), Box::new(e)))?;
        header.push_str(&emitter.header);
        body.push_str(&emitter.body);
        // Collect strings in insertion order.
        let mut entries: Vec<(String, String)> = Vec::new();
        for (content, (name, _)) in &emitter.strings {
            entries.push((name.clone(), content.clone()));
        }
        // sort by global name to stay deterministic across runs (intern_string
        // uses a monotonic counter, so alphabetic is enough).
        entries.sort_by(|a, b| a.0.cmp(&b.0));
        all_strings.insert(mname.clone(), entries);
    }

    // Trampoline: verify that the entry module has a
    // `main : () -> Unit !IO`. If not, the workspace isn't runnable.
    let entry_module = ws
        .modules
        .get(&ws.entry)
        .ok_or_else(|| CodegenError::Internal(format!("entry module `{}` not in workspace", ws.entry)))?;
    let has_main = entry_module
        .defs
        .iter()
        .any(|d| matches!(d, Def::Fn(f) if f.name == "main" && main_is_void(&f.ty)));
    if !has_main {
        return Err(CodegenError::MissingEntryMain(ws.entry.clone()));
    }

    let mut out = String::new();
    out.push_str("; AILang generated workspace; entry: ");
    out.push_str(&ws.entry);
    out.push('\n');
    out.push_str("source_filename = \"");
    out.push_str(&ws.entry);
    out.push_str(".ail\"\n");
    out.push_str("target triple = \"");
    out.push_str(default_triple());
    out.push_str("\"\n\n");

    // Globals: per module, alphabetically over module names (BTreeMap order),
    // then insertion order per module.
    let mut emitted_global = false;
    for entries in all_strings.values() {
        for (name, content) in entries {
            let escaped = ll_string_literal(content);
            let len = c_byte_len(content);
            out.push_str(&format!(
                "@{name} = private unnamed_addr constant [{len} x i8] c\"{escaped}\", align 1\n",
            ));
            emitted_global = true;
        }
    }
    if emitted_global {
        out.push('\n');
    }

    out.push_str("declare i32 @printf(ptr, ...)\n");
    out.push_str("declare i32 @puts(ptr)\n");
    // Bench iter: the allocator declaration name follows `alloc`.
    // Default `Gc` keeps the emitted IR byte-identical to the pre-bench
    // pipeline; `Bump` declares `@bump_malloc` instead, supplied by
    // `runtime/bump.c` and linked in lieu of `-lgc`.
    out.push_str(&format!("declare ptr @{}(i64)\n", alloc.fn_name()));
    // Iter 16e: `==` on `Str` lowers to `@strcmp` followed by
    // `icmp eq i32 0`. NUL-terminated strings make this a one-liner;
    // libc supplies `strcmp` so no extra link flag is needed.
    out.push_str("declare i32 @strcmp(ptr, ptr)\n\n");
    out.push_str(&header);
    out.push_str(&body);

    // Trampoline @main → @ail_<entry>_main.
    out.push_str(&format!(
        "\ndefine i32 @main() {{\n  call i8 @ail_{}_main()\n  ret i32 0\n}}\n",
        ws.entry
    ));

    Ok(out)
}

fn main_is_void(t: &Type) -> bool {
    match t {
        Type::Fn { params, ret, .. } => {
            params.is_empty()
                && matches!(ret.as_ref(), Type::Con { name, .. } if name == "Unit")
        }
        _ => false,
    }
}

struct Emitter<'a> {
    module: &'a Module,
    /// Name of the currently lowered module (for mangling).
    module_name: &'a str,
    header: String,
    body: String,
    /// String constants: content -> (global name (without `@`), llvm type length incl. \0)
    strings: BTreeMap<String, (String, usize)>,
    /// Local symbol table per function: (name, ssa, llvm_type, ail_type).
    /// The AILang type is recorded so that the codegen-side type tracker
    /// can derive substitutions at polymorphic call sites without
    /// re-running the typechecker (Iter 12b).
    locals: Vec<(String, String, String, Type)>,
    /// Monotonic counter for SSA values and labels.
    counter: u64,
    /// Monotonic counter for global string names (per module).
    str_counter: u64,
    /// Top-level functions per module of the workspace, for call resolution.
    module_user_fns: &'a BTreeMap<String, BTreeMap<String, FnSig>>,
    /// AILang types of every fn-typed top-level def, per module. Carries
    /// `Forall` for polymorphic defs (used to derive substitutions at
    /// monomorphic call sites). Populated in pass 1 of `lower_workspace`.
    module_def_ail_types: &'a BTreeMap<String, BTreeMap<String, Type>>,
    /// Polymorphic defs per module — full FnDef so we can specialise
    /// the body when monomorphising. Mono fns aren't included.
    module_polymorphic_fns: &'a BTreeMap<String, BTreeMap<String, FnDef>>,
    /// Iter 12b: queue of (module, def, substitution) tuples that need
    /// to be emitted as specialised versions of polymorphic defs.
    /// `mono_emitted` tracks the same keys to deduplicate. The descriptor
    /// string is the deterministic name suffix (`Int`, `Int_Bool`, ...).
    mono_queue: Vec<(String, String, BTreeMap<String, Type>, String)>,
    mono_emitted: BTreeSet<(String, String, String)>, // (module, def, descriptor)
    /// Import map of the current module (alias/module name → actual module name).
    import_map: BTreeMap<String, String>,
    /// ADT table: type_name -> list of ctors in definition order.
    /// Tag of a ctor = index in this list.
    /// Kept around for future tools (pretty-printer for ADT values,
    /// decision-tree optimization).
    #[allow(dead_code)]
    types: BTreeMap<String, Vec<CtorInfo>>,
    /// Iter 15a: cross-module ctor index, keyed by module name. Used by
    /// `lookup_ctor_by_type` (for `Term::Ctor.type_name`) and
    /// `lookup_ctor_in_pattern` (for `Pattern::Ctor.ctor`). Built once
    /// per workspace and shared by every Emitter. Replaces the per-
    /// emitter `ctor_index` of pre-15a — that table only knew the
    /// current module's ctors and broke on cross-module references.
    module_ctor_index: &'a BTreeMap<String, BTreeMap<String, CtorRef>>,
    /// Iter 15b: per-module const defs, used to resolve `Term::Var`
    /// references (bare or qualified) to a const's body. Literal
    /// consts emit a global and are loaded via `@ail_<m>_<name>`;
    /// non-literal consts are inlined at every reference site (sound
    /// because `check_const` rejects effects, so the body is pure).
    module_consts: &'a BTreeMap<String, BTreeMap<String, ConstDef>>,
    /// Current basic block label. Set by `start_block` and is
    /// the single source of truth for `phi` operands.
    current_block: String,
    /// Iter 14e: true while the current block already ends in a
    /// terminator (currently only `ret` after a `musttail call`).
    /// Callers in the term lowering walk consult this to skip
    /// fall-through `br` emission and to omit the value from a
    /// surrounding match-arm phi. Reset by [`Self::start_block`].
    block_terminated: bool,
    /// Iter 7: SSA value (or `@global`) -> its FnSig, for first-class
    /// function values. Populated whenever we lower a `Term::Var` to a
    /// top-level fn pointer or when a fn-typed parameter is bound at
    /// function entry. Used by `Term::App` when the callee is not a
    /// statically-known top-level name.
    ssa_fn_sigs: BTreeMap<String, FnSig>,
    /// Iter 8b: name of the currently-emitted def (for lambda thunk
    /// naming `<def>_lam<n>`).
    current_def: String,
    /// Iter 8b: per-def counter for lambda thunks. Reset in emit_fn.
    lam_counter: u32,
    /// Iter 8b: thunk fn IR text for lambdas encountered during
    /// lowering. Flushed at the end of emit_fn (LLVM IR allows fns in
    /// any order).
    deferred_thunks: Vec<String>,
    /// Iter 17a: per-fn escape-analysis result. Set of pointer-as-usize
    /// addresses of `Term::Ctor` and `Term::Lam` nodes that the
    /// analysis proved do not escape the fn frame they are allocated
    /// in. Such allocations lower to `alloca` instead of `@GC_malloc`.
    /// Populated by `analyze_fn_body` at the start of `emit_fn` and at
    /// the start of every lambda thunk emission inside `lower_lambda`.
    non_escape: NonEscapeSet,
    /// Bench iter: which allocator the heap-allocation paths target.
    /// Decided at the top-level entry point (`lower_workspace_inner`)
    /// and propagated to every site that emits a `call ptr @<alloc>(...)`.
    alloc: AllocStrategy,
}

#[derive(Debug, Clone)]
#[allow(dead_code)]
struct CtorInfo {
    name: String,
    fields: Vec<String>, // llvm types
}

#[derive(Debug, Clone)]
struct CtorRef {
    type_name: String,
    tag: u32,
    /// Precomputed LLVM field types. Valid only for monomorphic ADTs
    /// (`type_vars.is_empty()`). For parameterised ADTs the entries are
    /// meaningless (free `Type::Var` lowers via the `_ => ptr` fallback)
    /// and must be re-derived per use site after substituting through
    /// `ail_fields`.
    fields: Vec<String>,
    /// AILang-level field types (parallel to `fields`). Carries
    /// `Type::Var` references for parameterised ADTs (Iter 13b); these
    /// are substituted at every ctor / match-arm use site.
    ail_fields: Vec<Type>,
    /// Iter 13b: type parameters of the owning TypeDef, in declaration
    /// order. Empty for monomorphic ADTs (`type IntList = ...`); non-
    /// empty for parameterised ADTs (`type Box[a] = MkBox(a)` →
    /// `["a"]`). Used as the var-set for `unify_for_subst` when deriving
    /// substitutions at a use site, and to map type-args
    /// (`Type::Con.args[i]`) back to the right var when lowering match
    /// arms against a parameterised scrutinee.
    type_vars: Vec<String>,
}

#[derive(Debug, Clone)]
struct FnSig {
    params: Vec<String>, // llvm types
    ret: String,         // llvm type
}

impl<'a> Emitter<'a> {
    fn new(
        module: &'a Module,
        module_name: &'a str,
        module_user_fns: &'a BTreeMap<String, BTreeMap<String, FnSig>>,
        module_def_ail_types: &'a BTreeMap<String, BTreeMap<String, Type>>,
        module_polymorphic_fns: &'a BTreeMap<String, BTreeMap<String, FnDef>>,
        module_ctor_index: &'a BTreeMap<String, BTreeMap<String, CtorRef>>,
        module_consts: &'a BTreeMap<String, BTreeMap<String, ConstDef>>,
        import_map: BTreeMap<String, String>,
        alloc: AllocStrategy,
    ) -> Self {
        let mut types: BTreeMap<String, Vec<CtorInfo>> = BTreeMap::new();
        for def in &module.defs {
            if let Def::Type(td) = def {
                let mut infos = Vec::new();
                for c in td.ctors.iter() {
                    // Iter 13b: precomputed LLVM field types are only
                    // meaningful for monomorphic ADTs. For parameterised
                    // ADTs the field types reference free `Type::Var`s
                    // and must be derived per use site after
                    // substituting; we still populate the slot with
                    // `i64`/`ptr` placeholders so the index shape stays
                    // uniform, but neither `lower_ctor` nor
                    // `lower_match` reads from it when `type_vars` is
                    // non-empty.
                    let fields: Vec<String> = c
                        .fields
                        .iter()
                        .map(|t| llvm_type(t).unwrap_or_else(|_| "ptr".into()))
                        .collect();
                    infos.push(CtorInfo {
                        name: c.name.clone(),
                        fields,
                    });
                }
                types.insert(td.name.clone(), infos);
            }
        }

        Self {
            module,
            module_name,
            header: String::new(),
            body: String::new(),
            strings: BTreeMap::new(),
            locals: Vec::new(),
            counter: 0,
            str_counter: 0,
            module_user_fns,
            module_def_ail_types,
            module_polymorphic_fns,
            mono_queue: Vec::new(),
            mono_emitted: BTreeSet::new(),
            import_map,
            types,
            module_ctor_index,
            module_consts,
            current_block: String::new(),
            block_terminated: false,
            ssa_fn_sigs: BTreeMap::new(),
            current_def: String::new(),
            lam_counter: 0,
            deferred_thunks: Vec::new(),
            non_escape: NonEscapeSet::new(),
            alloc,
        }
    }

    fn start_block(&mut self, label: &str) {
        self.body.push_str(label);
        self.body.push_str(":\n");
        self.current_block = label.to_string();
        self.block_terminated = false;
    }

    fn emit_module(&mut self) -> Result<()> {
        let defs: Vec<&Def> = self.module.defs.iter().collect();
        for def in defs {
            match def {
                Def::Fn(f) => {
                    // Polymorphic defs aren't emitted in their original
                    // form — they are specialised on demand at call sites
                    // (Iter 12b). Skip them here; the drain pass below
                    // emits the specialised versions.
                    if matches!(&f.ty, Type::Forall { .. }) {
                        continue;
                    }
                    self.emit_fn(f)
                        .map_err(|e| CodegenError::Def(f.name.clone(), Box::new(e)))?;
                }
                Def::Const(c) => {
                    self.emit_const(c)
                        .map_err(|e| CodegenError::Def(c.name.clone(), Box::new(e)))?;
                }
                Def::Type(_) => {
                    // No LLVM definition needed: the ADT exists only as a
                    // logical type. Heap boxes are allocated ad hoc via
                    // GC_malloc (Boehm conservative collector, Iter 14f).
                }
            }
        }
        // Drain the monomorphisation queue. Specialised fns may
        // themselves invoke polymorphic defs and queue further entries,
        // so iterate until empty.
        while let Some((owner_module, def_name, subst, descriptor)) = self.mono_queue.pop() {
            self.emit_specialised_fn(&owner_module, &def_name, &subst, &descriptor)
                .map_err(|e| {
                    CodegenError::Def(
                        format!("{def_name}__{descriptor}"),
                        Box::new(e),
                    )
                })?;
        }
        Ok(())
    }

    /// Iter 12b: emit one specialised version of a polymorphic def.
    /// Substitutes rigid vars in both the type and the body, then
    /// calls `emit_fn` against a synthetic FnDef whose `name` already
    /// contains the descriptor — the existing mangling concatenates
    /// `ail_<module>_<name>` and produces the desired symbol.
    fn emit_specialised_fn(
        &mut self,
        owner_module: &str,
        def_name: &str,
        subst: &BTreeMap<String, Type>,
        descriptor: &str,
    ) -> Result<()> {
        let fdef = self
            .module_polymorphic_fns
            .get(owner_module)
            .and_then(|m| m.get(def_name))
            .cloned()
            .ok_or_else(|| {
                CodegenError::Internal(format!(
                    "emit_specialised_fn: `{owner_module}.{def_name}` not registered"
                ))
            })?;
        let inner_ty = match &fdef.ty {
            Type::Forall { body, .. } => (**body).clone(),
            other => other.clone(),
        };
        let mono_ty = apply_subst_to_type(&inner_ty, subst);
        let mono_body = apply_subst_to_term(&fdef.body, subst);
        let synthetic = FnDef {
            name: format!("{def_name}__{descriptor}"),
            ty: mono_ty,
            params: fdef.params.clone(),
            body: mono_body,
            doc: fdef.doc.clone(),
        };
        // Specialised def belongs to the polymorphic def's owner
        // module, not necessarily self.module_name. Swap module_name
        // briefly so mangling stays correct.
        let saved_module = self.module_name;
        // SAFETY: we rebind module_name through a raw pointer cast
        // because the field is `&'a str`. Equivalent: hand
        // emit_fn the mangling target via a parameter. Simpler to
        // restore.
        // Instead of unsafe, we just call emit_fn directly — the
        // mangling uses self.module_name which is &'a str but the
        // owner_module string lives inside self.module_polymorphic_fns,
        // also borrowed for 'a, so we can re-borrow it.
        let owner_ref: &'a str = self
            .module_polymorphic_fns
            .keys()
            .find(|k| k.as_str() == owner_module)
            .map(|s| s.as_str())
            .ok_or_else(|| {
                CodegenError::Internal(format!(
                    "owner module `{owner_module}` not in module_polymorphic_fns"
                ))
            })?;
        self.module_name = owner_ref;
        let r = self.emit_fn(&synthetic);
        self.module_name = saved_module;
        r
    }

    fn emit_const(&mut self, c: &ConstDef) -> Result<()> {
        // Iter 15b: non-literal const values (e.g. ctor expressions) are
        // not emitted as globals. They are inlined at every `Term::Var`
        // reference site — sound because `check_const` rejects effectful
        // bodies, so re-evaluating the body at each use is observably
        // equivalent to a single computation. Trade-off: a long
        // recursive const evaluated in many places duplicates work,
        // but the demo-scale workloads shipped in the stdlib
        // examples are small enough that this is a non-issue. A
        // future iter may layer a `@llvm.global_ctors`-style init
        // path on top to share the result across reference sites.
        let lty = llvm_type(&c.ty)?;
        let lit = match &c.value {
            Term::Lit { lit } => lit,
            _ => return Ok(()),
        };
        let (val_ty, val) = match lit {
            Literal::Int { value } => ("i64".to_string(), value.to_string()),
            Literal::Bool { value } => (
                "i1".to_string(),
                if *value { "true".into() } else { "false".into() },
            ),
            Literal::Unit => ("i8".to_string(), "0".to_string()),
            Literal::Str { value } => {
                let g = self.intern_string("str", value);
                ("ptr".to_string(), format!("@{g}"))
            }
        };
        if val_ty != lty {
            return Err(CodegenError::Internal(format!(
                "const type mismatch: {} vs {}",
                lty, val_ty
            )));
        }
        self.header.push_str(&format!(
            "@ail_{module}_{name} = constant {ty} {val}\n",
            module = self.module_name,
            name = c.name,
            ty = lty,
            val = val,
        ));
        Ok(())
    }

    fn emit_fn(&mut self, f: &FnDef) -> Result<()> {
        let (param_tys, ret_ty) = match &f.ty {
            Type::Fn { params, ret, .. } => (params.clone(), (**ret).clone()),
            other => {
                return Err(CodegenError::NotFnType(
                    ailang_core::pretty::type_to_string(other),
                ));
            }
        };

        let llvm_param_tys: Vec<String> =
            param_tys.iter().map(llvm_type).collect::<Result<_>>()?;
        let llvm_ret = llvm_type(&ret_ty)?;

        self.locals.clear();
        self.counter = 0;
        // Per-fn body: the sidetable starts empty. Top-level fn references
        // get registered on demand by `lower_term(Term::Var)`.
        self.ssa_fn_sigs.clear();
        // Iter 8b: lambda thunks live in the same module body but get
        // collected during lowering and appended after the parent fn.
        self.current_def = f.name.clone();
        self.lam_counter = 0;
        // Iter 17a: run escape analysis over the fn body. The result
        // is queried at every `Term::Ctor` / `Term::Lam` lowering site
        // to decide between `alloca` (non-escaping) and `@GC_malloc`
        // (escaping). The analysis is purely additive — a stale or
        // empty result only loses optimisation opportunities, never
        // correctness.
        self.non_escape = escape::analyze_fn_body(&f.body);

        let mut sig = format!(
            "define {ret} @ail_{module}_{name}(",
            ret = llvm_ret,
            module = self.module_name,
            name = f.name
        );
        for (i, ((pname, pty), pty_ail)) in f
            .params
            .iter()
            .zip(llvm_param_tys.iter())
            .zip(param_tys.iter())
            .enumerate()
        {
            if i > 0 {
                sig.push_str(", ");
            }
            // SSA argument name: %arg_<name>
            let pssa = format!("%arg_{}", pname);
            sig.push_str(&format!("{pty} {pssa}"));
            self.locals.push((
                pname.clone(),
                pssa.clone(),
                pty.clone(),
                pty_ail.clone(),
            ));
            // Iter 7: if this param is a function value, record its sig
            // so that `f(args)` inside the body can emit an indirect call.
            if let Some(fs) = fn_sig_from_type(pty_ail) {
                self.ssa_fn_sigs.insert(pssa, fs);
            }
        }
        sig.push_str(") {\n");
        self.body.push_str(&sig);
        self.start_block("entry");

        let (val, val_ty) = self.lower_term(&f.body)?;
        if !self.block_terminated {
            if val_ty != llvm_ret {
                return Err(CodegenError::Internal(format!(
                    "fn `{}`: body type {val_ty} != return type {llvm_ret}",
                    f.name
                )));
            }
            self.body
                .push_str(&format!("  ret {val_ty} {val}\n}}\n\n"));
        } else {
            // Iter 14e: a `tail-app`/`tail-do` at the body root already
            // emitted its own `ret` (after `musttail call`). Just close
            // the function body — no fall-through ret.
            self.body.push_str("}\n\n");
        }

        // Iter 8b: flush lambda thunks collected while lowering this fn's
        // body. They go after the closing `}` of the parent fn, before
        // the adapter, so the parent fn is contiguous.
        for t in self.deferred_thunks.drain(..) {
            self.body.push_str(&t);
        }

        // Iter 8a: emit closure-pair scaffold (adapter + static closure)
        // for this fn. The adapter takes an extra `ptr %_env` (ignored,
        // null sentinel for top-level fns) and forwards to the real fn.
        // The static closure pair `{ adapter_ptr, null }` is the value
        // produced when this fn is referenced as a `Term::Var` value
        // (closure-pair pointer ABI).
        self.emit_adapter_and_static_closure(&f.name, &llvm_param_tys, &llvm_ret);
        Ok(())
    }

    /// Iter 8a: closure-pair scaffold for a top-level fn. Always emitted
    /// (one wrapper per fn), so cross-module references just use the
    /// `<m>_<f>_clos` symbol without coordination.
    fn emit_adapter_and_static_closure(
        &mut self,
        fn_name: &str,
        param_tys: &[String],
        ret_ty: &str,
    ) {
        let m = self.module_name;
        // Adapter: `(ptr %_env, params...) -> ret` calls the real fn,
        // returning whatever it returned.
        let mut adapter = format!(
            "define {ret} @ail_{m}_{fn_name}_adapter(ptr %_env",
            ret = ret_ty,
        );
        for (i, pty) in param_tys.iter().enumerate() {
            adapter.push_str(&format!(", {pty} %a{i}"));
        }
        adapter.push_str(") {\nentry:\n");
        let mut call_args = String::new();
        for (i, pty) in param_tys.iter().enumerate() {
            if i > 0 {
                call_args.push_str(", ");
            }
            call_args.push_str(&format!("{pty} %a{i}"));
        }
        adapter.push_str(&format!(
            "  %r = call {ret} @ail_{m}_{fn_name}({call_args})\n",
            ret = ret_ty,
        ));
        adapter.push_str(&format!("  ret {ret} %r\n}}\n\n", ret = ret_ty));
        self.body.push_str(&adapter);

        // Static closure pair: `{ adapter_ptr, null }`. The address of
        // this global IS the fn-value that escapes to other code.
        self.header.push_str(&format!(
            "@ail_{m}_{fn_name}_clos = private unnamed_addr constant {{ ptr, ptr }} {{ ptr @ail_{m}_{fn_name}_adapter, ptr null }}\n"
        ));
    }

    /// Lowers a term to (SSA value string, LLVM type).
    fn lower_term(&mut self, t: &Term) -> Result<(String, String)> {
        match t {
            Term::Lit { lit } => Ok(match lit {
                Literal::Int { value } => (value.to_string(), "i64".into()),
                Literal::Bool { value } => (
                    if *value { "true".into() } else { "false".into() },
                    "i1".into(),
                ),
                Literal::Str { value } => {
                    // Create global constant; in opaque-pointer LLVM,
                    // `@name` is directly a valid `ptr`.
                    let g = self.intern_string("str", value);
                    (format!("@{g}"), "ptr".into())
                }
                Literal::Unit => ("0".into(), "i8".into()),
            }),
            Term::Var { name } => {
                // Iter 16d: `__unreachable__` is a polymorphic bottom
                // value (`forall a. a`). At codegen we emit LLVM
                // `unreachable` as the block terminator and return a
                // dummy SSA value. The surrounding `if`/`match`/`seq`
                // already inspects `block_terminated` and forwards the
                // sibling branch's type, so the type we report here is
                // not consumed by a phi node — `i8` is a sound
                // placeholder. Subsequent emissions in this block are
                // gated by `block_terminated`.
                if name == "__unreachable__" {
                    self.body.push_str("  unreachable\n");
                    self.block_terminated = true;
                    return Ok(("0".into(), "i8".into()));
                }
                if let Some((_, ssa, ty, _)) =
                    self.locals.iter().rev().find(|(n, _, _, _)| n == name)
                {
                    return Ok((ssa.clone(), ty.clone()));
                }
                // Iter 7: bare reference to a top-level fn yields a fn-pointer
                // value of type `ptr`. Cross-module via `prefix.def`, current
                // module via plain `def`. Sidetable carries the sig.
                if let Some((global, sig)) = self.resolve_top_level_fn(name) {
                    self.ssa_fn_sigs.entry(global.clone()).or_insert(sig);
                    return Ok((global, "ptr".into()));
                }
                // Iter 15b: const lookup. Both bare (`xs`) and qualified
                // (`prefix.xs`) forms resolve through `module_consts`.
                // Literal-bodied consts get a load from the global; non-
                // literal bodies (e.g. ctor expressions) are inlined.
                if let Some((owner_module, cdef)) = self.resolve_const(name) {
                    let lty = llvm_type(&cdef.ty)?;
                    if matches!(&cdef.value, Term::Lit { .. }) {
                        let v = self.fresh_ssa();
                        self.body.push_str(&format!(
                            "  {v} = load {lty}, ptr @ail_{owner_module}_{cname}, align 8\n",
                            cname = cdef.name,
                        ));
                        return Ok((v, lty));
                    } else {
                        // Inline the const body. Switch module context to
                        // the owning module while lowering so any nested
                        // bare references resolve in the const's home
                        // namespace. Simpler approach: call lower_term
                        // directly; the current emitter's module context
                        // is fine because cross-module ctors are already
                        // qualified in the AST after typecheck.
                        let value = cdef.value.clone();
                        return self.lower_term(&value);
                    }
                }
                Err(CodegenError::UnknownVar(name.clone()))
            }
            Term::Let { name, value, body } => {
                let val_ail = self.synth_arg_type(value)?;
                let (val_ssa, val_ty) = self.lower_term(value)?;
                self.locals.push((name.clone(), val_ssa, val_ty, val_ail));
                let r = self.lower_term(body);
                self.locals.pop();
                r
            }
            Term::If { cond, then, else_ } => {
                let (cond_v, cond_ty) = self.lower_term(cond)?;
                if cond_ty != "i1" {
                    return Err(CodegenError::Internal(format!(
                        "if cond not i1: {cond_ty}"
                    )));
                }
                let id = self.fresh_id();
                let then_lbl = format!("then.{id}");
                let else_lbl = format!("else.{id}");
                let join_lbl = format!("join.{id}");

                self.body.push_str(&format!(
                    "  br i1 {cond_v}, label %{then_lbl}, label %{else_lbl}\n"
                ));

                self.start_block(&then_lbl);
                let (then_v, then_ty) = self.lower_term(then)?;
                // Iter 14e: a tail-call in this branch already terminated
                // its block; skip its branch to join and exclude from phi.
                let then_terminated = self.block_terminated;
                let then_block_end = self.current_block.clone();
                if !then_terminated {
                    self.body.push_str(&format!("  br label %{join_lbl}\n"));
                }

                self.start_block(&else_lbl);
                let (else_v, else_ty) = self.lower_term(else_)?;
                let else_terminated = self.block_terminated;
                let else_block_end = self.current_block.clone();
                if !then_terminated && !else_terminated && then_ty != else_ty {
                    return Err(CodegenError::Internal(format!(
                        "if branches type mismatch: {then_ty} vs {else_ty}"
                    )));
                }
                if !else_terminated {
                    self.body.push_str(&format!("  br label %{join_lbl}\n"));
                }

                // Iter 14e: if both branches terminated, the whole `if` is
                // terminated and no join is reachable. Mark and bail.
                if then_terminated && else_terminated {
                    self.block_terminated = true;
                    return Ok(("0".into(), then_ty));
                }
                // If exactly one branch terminated, the join receives only
                // the other branch's value — no phi node is needed.
                if then_terminated {
                    self.start_block(&join_lbl);
                    return Ok((else_v, else_ty));
                }
                if else_terminated {
                    self.start_block(&join_lbl);
                    return Ok((then_v, then_ty));
                }

                self.start_block(&join_lbl);
                let phi = self.fresh_ssa();
                self.body.push_str(&format!(
                    "  {phi} = phi {ty} [ {tv}, %{tlbl} ], [ {ev}, %{elbl} ]\n",
                    ty = then_ty,
                    tv = then_v,
                    tlbl = then_block_end,
                    ev = else_v,
                    elbl = else_block_end,
                ));
                // Iter 7: if both branches yield the same fn-pointer sig,
                // forward it to the phi SSA so subsequent indirect calls
                // can resolve.
                if then_ty == "ptr" {
                    if let (Some(ts), Some(es)) =
                        (self.ssa_fn_sigs.get(&then_v), self.ssa_fn_sigs.get(&else_v))
                    {
                        if ts.params == es.params && ts.ret == es.ret {
                            let merged = ts.clone();
                            self.ssa_fn_sigs.insert(phi.clone(), merged);
                        }
                    }
                }
                Ok((phi, then_ty))
            }
            Term::App { callee, args, tail } => {
                // Direct call when the callee is a `Var` referring to a
                // statically-known target (builtin, current-module fn,
                // qualified cross-module fn) AND not shadowed by a local.
                // Otherwise we fall through to the indirect-call path,
                // which lowers the callee to a fn-pointer and looks up
                // its sig in the sidetable.
                if let Term::Var { name } = callee.as_ref() {
                    let shadowed = self.locals.iter().any(|(n, _, _, _)| n == name);
                    if !shadowed && self.is_static_callee(name) {
                        return self.lower_app(name, args, *tail);
                    }
                }
                let (callee_ssa, callee_ty) = self.lower_term(callee)?;
                if callee_ty != "ptr" {
                    return Err(CodegenError::Internal(format!(
                        "indirect call: callee type must be ptr, got {callee_ty}"
                    )));
                }
                let sig = self
                    .ssa_fn_sigs
                    .get(&callee_ssa)
                    .cloned()
                    .ok_or_else(|| {
                        CodegenError::Internal(format!(
                            "indirect call: no FnSig recorded for `{callee_ssa}`"
                        ))
                    })?;
                self.emit_indirect_call(&callee_ssa, &sig, args, *tail)
            }
            Term::Do { op, args, tail } => self.lower_effect_op(op, args, *tail),
            Term::Ctor { type_name, ctor, args } => {
                // Iter 17a: pass the term pointer so `lower_ctor` can
                // consult the escape-analysis result for this exact
                // allocation site.
                let term_ptr = (t as *const Term) as usize;
                self.lower_ctor(type_name, ctor, args, term_ptr)
            }
            Term::Match { scrutinee, arms } => self.lower_match(scrutinee, arms),
            Term::Lam { params, param_tys, ret_ty, effects: _, body } => {
                // Iter 17a: same as `Ctor` — pass the term pointer for
                // escape-analysis lookup. A non-escaping closure pair
                // (and its env) lower to `alloca`.
                let term_ptr = (t as *const Term) as usize;
                self.lower_lambda(params, param_tys, ret_ty, body, term_ptr)
            }
            Term::Seq { lhs, rhs } => {
                // Iter 10: lower lhs for its effects, discard the SSA;
                // lower rhs and return its value as the whole expression.
                // Iter 14e: lhs may not legally be a `tail` call (the
                // typechecker rejects that), so `block_terminated` is
                // false after it. rhs is in the same tail context as the
                // surrounding seq, so a `tail-app` there will set
                // `block_terminated`; the outer match-arm/fn-body
                // handler honours that.
                let _ = self.lower_term(lhs)?;
                self.lower_term(rhs)
            }
            Term::LetRec { .. } => {
                // Iter 16b.1: `Term::LetRec` is eliminated by the
                // desugar pass before codegen runs, so reaching it
                // here is a bug.
                unreachable!("Term::LetRec eliminated by desugar")
            }
        }
    }

    /// Iter 15a: resolves a ctor reference by `type_name` (which may be
    /// qualified `module.T` or bare `T`) plus a bare ctor name. Returns
    /// the same `CtorRef` shape used by the local `ctor_index`. The
    /// returned `CtorRef.type_name` is always the bare type name as
    /// declared in the owning module. The current `module_name` is the
    /// authority for "bare" — that lets a specialised fn body emitted
    /// under a swapped `module_name` (see `emit_specialised_fn`)
    /// resolve its bare ctor references against the *owner* module's
    /// ctor table, not the consumer's.
    fn lookup_ctor_by_type(
        &self,
        type_name: &str,
        ctor_name: &str,
    ) -> Result<CtorRef> {
        if type_name.matches('.').count() == 1 {
            let (prefix, suffix) = type_name.split_once('.').expect("checked");
            let target_module = self.import_map.get(prefix).cloned().ok_or_else(|| {
                CodegenError::Internal(format!(
                    "qualified ctor `{type_name}/{ctor_name}`: prefix `{prefix}` not in import map"
                ))
            })?;
            let cref = self
                .module_ctor_index
                .get(&target_module)
                .and_then(|m| m.get(ctor_name))
                .cloned()
                .ok_or_else(|| {
                    CodegenError::Internal(format!(
                        "qualified ctor `{type_name}/{ctor_name}` not in module `{target_module}`"
                    ))
                })?;
            if cref.type_name != suffix {
                return Err(CodegenError::Internal(format!(
                    "ctor `{ctor_name}` belongs to `{}`, not `{type_name}`",
                    cref.type_name
                )));
            }
            Ok(cref)
        } else {
            let cref = self
                .module_ctor_index
                .get(self.module_name)
                .and_then(|m| m.get(ctor_name))
                .cloned()
                .ok_or_else(|| {
                    CodegenError::Internal(format!(
                        "unknown ctor `{ctor_name}` in module `{}`",
                        self.module_name
                    ))
                })?;
            if cref.type_name != type_name {
                return Err(CodegenError::Internal(format!(
                    "ctor `{ctor_name}` belongs to `{}`, not `{type_name}`",
                    cref.type_name
                )));
            }
            Ok(cref)
        }
    }

    /// Iter 15a: collects the set of type names declared in `owner_module`.
    /// Used to mirror the typechecker's `qualify_local_types` rewrite
    /// when reading a polymorphic fn's signature pulled across the
    /// import boundary.
    fn collect_owner_local_types(&self, owner_module: &str) -> BTreeSet<String> {
        self.module_ctor_index
            .get(owner_module)
            .map(|m| {
                m.values()
                    .map(|c| c.type_name.clone())
                    .collect::<BTreeSet<_>>()
            })
            .unwrap_or_default()
    }

    /// Iter 15a: resolves a ctor in pattern position. The current
    /// `module_name`'s ctor table is consulted first; on miss, the
    /// imported modules are scanned (the typechecker has already
    /// vetted unambiguity, so the first hit wins — local always
    /// shadows imported on conflict). Using `module_name` rather than
    /// `self.ctor_index` matters when emitting a specialised fn body
    /// in the owner's module context (see `emit_specialised_fn`).
    fn lookup_ctor_in_pattern(&self, ctor_name: &str) -> Result<CtorRef> {
        if let Some(cref) = self
            .module_ctor_index
            .get(self.module_name)
            .and_then(|m| m.get(ctor_name))
            .cloned()
        {
            return Ok(cref);
        }
        // Walk the *current* module's imports for fallback. When
        // emitting a specialised fn body in another module, the
        // emitter's `import_map` is still the consumer's; we want the
        // owner's. Look up the owner module's import map indirectly
        // through `self.module` whenever it equals `self.module_name`,
        // and fall back to the active `import_map` only when we are
        // genuinely emitting in the consumer module. Since
        // `emit_specialised_fn` swaps only `module_name`, not
        // `import_map`, the fallback below covers both cases by
        // additionally searching every module in `module_ctor_index`
        // — that's cheap (number of modules in a workspace is small)
        // and the typechecker has already pinned uniqueness.
        for (mname, ctors) in self.module_ctor_index.iter() {
            if mname == self.module_name {
                continue;
            }
            if let Some(cref) = ctors.get(ctor_name).cloned() {
                return Ok(cref);
            }
        }
        Err(CodegenError::Internal(format!(
            "unknown ctor in pattern: `{ctor_name}`"
        )))
    }

    /// Heap box layout: 8 bytes tag (i64) followed by 8 bytes per field.
    /// i1 and i8 fields also occupy a full 8-byte slot — the typed
    /// load/store instructions write/read only the required size.
    ///
    /// Iter 17a: `term_ptr` is the pointer-as-usize of the lowered
    /// `Term::Ctor` node. If escape analysis flagged this site as
    /// non-escaping (i.e., the value cannot live past the current fn
    /// frame), allocation lowers to LLVM `alloca` instead of
    /// `@GC_malloc`. The rest of the lowering (tag store, field
    /// stores, ptr return) is identical.
    fn lower_ctor(
        &mut self,
        type_name: &str,
        ctor_name: &str,
        args: &[Term],
        term_ptr: usize,
    ) -> Result<(String, String)> {
        let cref = self.lookup_ctor_by_type(type_name, ctor_name)?;
        if args.len() != cref.ail_fields.len() {
            return Err(CodegenError::Internal(format!(
                "ctor `{type_name}/{ctor_name}` arity"
            )));
        }
        // Iter 13b: for parameterised ADTs the precomputed `cref.fields`
        // is meaningless because field types reference rigid type vars.
        // Derive a per-use-site substitution from the arg types and
        // re-lower each field type. Monomorphic ADTs hit the fast path
        // (no var-set, substitution is empty, ail_fields lower exactly
        // like cref.fields).
        // Iter 15b: for cross-module ctors, qualify any local type-cons
        // in `cref.ail_fields` (symmetric to the term-ctor synth fix).
        let qualified_ail_fields: Vec<Type> = if type_name.matches('.').count() == 1 {
            let (prefix, _) = type_name.split_once('.').expect("checked");
            if let Some(target) = self.import_map.get(prefix) {
                let owner_local_types = self.collect_owner_local_types(target);
                cref.ail_fields
                    .iter()
                    .map(|f| qualify_local_types_codegen(f, target, &owner_local_types))
                    .collect()
            } else {
                cref.ail_fields.clone()
            }
        } else {
            cref.ail_fields.clone()
        };
        let expected_llvm_tys: Vec<String> = if cref.type_vars.is_empty() {
            cref.fields.clone()
        } else {
            let arg_ail_tys: Vec<Type> = args
                .iter()
                .map(|a| self.synth_arg_type(a))
                .collect::<Result<_>>()?;
            let var_set: BTreeSet<&str> =
                cref.type_vars.iter().map(|s| s.as_str()).collect();
            let mut subst: BTreeMap<String, Type> = BTreeMap::new();
            for (exp, actual) in qualified_ail_fields.iter().zip(arg_ail_tys.iter()) {
                unify_for_subst(exp, actual, &var_set, &mut subst)?;
            }
            qualified_ail_fields
                .iter()
                .map(|f| llvm_type(&apply_subst_to_type(f, &subst)))
                .collect::<Result<_>>()?
        };
        // Evaluate arguments up front so allocation and store stay close
        // together.
        let mut compiled = Vec::new();
        for (a, exp) in args.iter().zip(expected_llvm_tys.iter()) {
            let (v, vty) = self.lower_term(a)?;
            if &vty != exp {
                return Err(CodegenError::Internal(format!(
                    "ctor `{ctor_name}` field type {vty} != expected {exp}"
                )));
            }
            compiled.push((v, vty));
        }
        let size_bytes = 8 + (compiled.len() * 8) as i64;
        let p = self.fresh_ssa();
        // Iter 17a: pick allocator based on escape analysis. `alloca`
        // for non-escaping (stack-allocated, freed on fn return);
        // `@GC_malloc` for everything else.
        if self.non_escape.contains(&term_ptr) {
            self.body.push_str(&format!(
                "  {p} = alloca i8, i64 {size_bytes}, align 8\n"
            ));
        } else {
            self.body.push_str(&format!(
                "  {p} = call ptr @{}(i64 {size_bytes})\n",
                self.alloc.fn_name()
            ));
        }
        // Write tag.
        self.body.push_str(&format!(
            "  store i64 {tag}, ptr {p}, align 8\n",
            tag = cref.tag
        ));
        // Write fields.
        for (i, (v, ty)) in compiled.iter().enumerate() {
            let off = 8 + i as i64 * 8;
            let addr = self.fresh_ssa();
            self.body.push_str(&format!(
                "  {addr} = getelementptr inbounds i8, ptr {p}, i64 {off}\n"
            ));
            self.body
                .push_str(&format!("  store {ty} {v}, ptr {addr}, align 8\n"));
        }
        Ok((p, "ptr".into()))
    }

    fn lower_match(
        &mut self,
        scrutinee: &Term,
        arms: &[Arm],
    ) -> Result<(String, String)> {
        let s_ail = self.synth_arg_type(scrutinee)?;
        let (s_val, s_ty) = self.lower_term(scrutinee)?;
        if s_ty != "ptr" {
            return Err(CodegenError::Internal(format!(
                "match on non-ADT scrutinee (got {s_ty}); MVP supports only ADTs"
            )));
        }

        // Load tag.
        let tag = self.fresh_ssa();
        self.body
            .push_str(&format!("  {tag} = load i64, ptr {s_val}, align 8\n"));

        // Separate arms.
        let mut ctor_arms: Vec<(CtorRef, &Arm, Vec<Option<String>>)> = Vec::new();
        let mut open_arm: Option<&Arm> = None;
        let mut open_var: Option<String> = None;
        for arm in arms {
            match &arm.pat {
                Pattern::Wild => {
                    open_arm = Some(arm);
                }
                Pattern::Var { name } => {
                    open_arm = Some(arm);
                    open_var = Some(name.clone());
                }
                Pattern::Ctor { ctor, fields } => {
                    // Iter 15a: lookup falls back to imported modules when
                    // a bare ctor name doesn't resolve locally.
                    let cref = self.lookup_ctor_in_pattern(ctor)?;
                    let bindings: Vec<Option<String>> = fields
                        .iter()
                        .map(|p| match p {
                            Pattern::Var { name } => Some(name.clone()),
                            Pattern::Wild => None,
                            _ => None, // MVP: nested ctor/lit patterns not supported
                        })
                        .collect();
                    ctor_arms.push((cref, arm, bindings));
                }
                Pattern::Lit { .. } => {
                    return Err(CodegenError::Internal(
                        "MVP: lit patterns in match not supported".into(),
                    ));
                }
            }
        }

        let id = self.fresh_id();
        let join_lbl = format!("mjoin.{id}");
        let default_lbl = format!("mdefault.{id}");

        // switch
        let mut sw = format!(
            "  switch i64 {tag}, label %{default_lbl} [\n",
            tag = tag
        );
        let mut arm_labels: Vec<String> = Vec::new();
        for (i, (cref, _, _)) in ctor_arms.iter().enumerate() {
            let lbl = format!("marm.{id}.{i}");
            sw.push_str(&format!("    i64 {}, label %{}\n", cref.tag, lbl));
            arm_labels.push(lbl);
        }
        sw.push_str("  ]\n");
        self.body.push_str(&sw);

        let mut phi_inputs: Vec<(String, String)> = Vec::new(); // (value, block)
        let mut result_ty: Option<String> = None;

        for (i, (cref, arm, bindings)) in ctor_arms.iter().enumerate() {
            self.start_block(&arm_labels[i]);
            // Iter 13b: derive substitution for parameterised ADTs from
            // the scrutinee's concrete type-args. Map `cref.type_vars[i]`
            // → `s_ail.args[i]`. For monomorphic ADTs the mapping is
            // empty and substitution is a no-op. The substituted AILang
            // types are used both for the LLVM `load` instruction and as
            // the AILang-type slot of the local — without the latter, a
            // downstream `unbox(b)` would see `b: a` (rigid var) instead
            // of `b: Int`.
            let arm_subst: BTreeMap<String, Type> = if cref.type_vars.is_empty() {
                BTreeMap::new()
            } else {
                match &s_ail {
                    Type::Con { args, .. } if args.len() == cref.type_vars.len() => cref
                        .type_vars
                        .iter()
                        .cloned()
                        .zip(args.iter().cloned())
                        .collect(),
                    _ => {
                        return Err(CodegenError::Internal(format!(
                            "match: scrutinee type `{}` not aligned with ctor `{}`'s {} type vars",
                            ailang_core::pretty::type_to_string(&s_ail),
                            cref.type_name,
                            cref.type_vars.len(),
                        )));
                    }
                }
            };
            // Load fields and bind as locals.
            // Iter 15b: when the scrutinee's ADT lives in another module,
            // `cref.ail_fields[idx]` carries the field type written in
            // the owner's local namespace. Qualify it before substituting
            // — symmetric to the term-ctor and pat-ctor fixes in
            // ailang-check.
            let owning_module: Option<String> = match &s_ail {
                Type::Con { name, .. } if name.matches('.').count() == 1 => name
                    .split_once('.')
                    .map(|(p, _)| p.to_string()),
                _ => None,
            };
            let mut pushed = 0usize;
            for (idx, binding) in bindings.iter().enumerate() {
                if let Some(bname) = binding {
                    let raw_ail = cref.ail_fields.get(idx).cloned().unwrap_or(Type::unit());
                    let qualified_ail = match &owning_module {
                        Some(m) => {
                            let owner_local_types = self.collect_owner_local_types(m);
                            qualify_local_types_codegen(&raw_ail, m, &owner_local_types)
                        }
                        None => raw_ail,
                    };
                    let bind_ail = if arm_subst.is_empty() {
                        qualified_ail
                    } else {
                        apply_subst_to_type(&qualified_ail, &arm_subst)
                    };
                    let fty = llvm_type(&bind_ail)?;
                    let off = 8 + idx as i64 * 8;
                    let addr = self.fresh_ssa();
                    self.body.push_str(&format!(
                        "  {addr} = getelementptr inbounds i8, ptr {s_val}, i64 {off}\n"
                    ));
                    let v = self.fresh_ssa();
                    self.body.push_str(&format!(
                        "  {v} = load {fty}, ptr {addr}, align 8\n"
                    ));
                    self.locals.push((bname.clone(), v, fty, bind_ail));
                    pushed += 1;
                }
            }
            let (val, vty) = self.lower_term(&arm.body)?;
            // pop bindings
            for _ in 0..pushed {
                self.locals.pop();
            }
            // Iter 14e: if the arm body lowered to a `musttail call` +
            // `ret`, the block is already terminated. Skip the
            // fall-through `br` and exclude this arm from the join phi.
            if !self.block_terminated {
                phi_inputs.push((val, self.current_block.clone()));
                self.body
                    .push_str(&format!("  br label %{join_lbl}\n"));
                if let Some(rt) = &result_ty {
                    if rt != &vty {
                        return Err(CodegenError::Internal(format!(
                            "match arm result type {vty} != {rt}"
                        )));
                    }
                } else {
                    result_ty = Some(vty);
                }
            }
        }

        // default block
        self.start_block(&default_lbl);
        if let Some(arm) = open_arm {
            // set up var binding if needed
            let pushed = if let Some(name) = open_var.take() {
                self.locals
                    .push((name, s_val.clone(), "ptr".into(), s_ail.clone()));
                1
            } else {
                0
            };
            let (val, vty) = self.lower_term(&arm.body)?;
            for _ in 0..pushed {
                self.locals.pop();
            }
            if !self.block_terminated {
                phi_inputs.push((val, self.current_block.clone()));
                self.body
                    .push_str(&format!("  br label %{join_lbl}\n"));
                if let Some(rt) = &result_ty {
                    if rt != &vty {
                        return Err(CodegenError::Internal(format!(
                            "match default arm result type {vty} != {rt}"
                        )));
                    }
                } else {
                    result_ty = Some(vty);
                }
            }
        } else {
            // Typechecker guarantees exhaustiveness, so unreachable.
            self.body.push_str("  unreachable\n");
        }

        // join
        // Iter 14e: if every arm tail-called and terminated its own
        // block, no predecessor branches into the join. Mark the whole
        // match as block-terminated and emit no join body — the
        // surrounding context (top-level fn body, seq rhs, etc.) checks
        // `block_terminated` before any fall-through emission.
        if phi_inputs.is_empty() {
            self.block_terminated = true;
            // Return a dummy SSA + type that won't be consumed. Use the
            // result_ty if any arm produced one, else fall back to i8.
            let rt = result_ty.unwrap_or_else(|| "i8".into());
            return Ok(("0".into(), rt));
        }
        self.start_block(&join_lbl);
        let phi = self.fresh_ssa();
        let rt = result_ty.unwrap_or_else(|| "i64".into());
        let phi_args = phi_inputs
            .iter()
            .map(|(v, b)| format!("[ {v}, %{b} ]"))
            .collect::<Vec<_>>()
            .join(", ");
        self.body.push_str(&format!(
            "  {phi} = phi {rt} {phi_args}\n"
        ));
        Ok((phi, rt))
    }

    fn lower_app(&mut self, name: &str, args: &[Term], tail: bool) -> Result<(String, String)> {
        // Iter 16e: `==` is polymorphic (`forall a. (a, a) -> Bool`).
        // Dispatch on the resolved AIL arg type — the LLVM `ptr` shape
        // aliases multiple AIL types (Str vs ADT vs Fn), so we cannot
        // dispatch on the LLVM type alone. ADT/Fn equality is rejected
        // here with a clear error; `Unit` evaluates both sides for
        // their side effects then returns constant `i1 1`.
        if name == "==" {
            if args.len() != 2 {
                return Err(CodegenError::Internal(
                    "builtin `==` expected 2 args".into(),
                ));
            }
            let arg_ty = self.synth_arg_type(&args[0])?;
            let (a, a_ll) = self.lower_term(&args[0])?;
            let (b, _b_ll) = self.lower_term(&args[1])?;
            let _ = tail;
            return self.lower_eq(&arg_ty, &a, &b, &a_ll);
        }

        // Built-in arithmetic / comparison.
        if let Some((instr, ret_ty)) = builtin_binop(name) {
            if args.len() != 2 {
                return Err(CodegenError::Internal(format!(
                    "builtin `{name}` expected 2 args"
                )));
            }
            let (a, _) = self.lower_term(&args[0])?;
            let (b, _) = self.lower_term(&args[1])?;
            let dst = self.fresh_ssa();
            self.body.push_str(&format!(
                "  {dst} = {instr} i64 {a}, {b}\n"
            ));
            // Builtins are not function calls in LLVM (they're inline
            // arithmetic); `tail` annotation has nothing to act on.
            // The typechecker accepts the marker but it is a no-op
            // here. (Iter 14e survey: no fixture marks a builtin tail.)
            let _ = tail;
            return Ok((dst, ret_ty.into()));
        }
        if name == "not" {
            if args.len() != 1 {
                return Err(CodegenError::Internal("not arity".into()));
            }
            let (a, _) = self.lower_term(&args[0])?;
            let dst = self.fresh_ssa();
            self.body
                .push_str(&format!("  {dst} = xor i1 {a}, true\n"));
            return Ok((dst, "i1".into()));
        }

        // Cross-module call: exactly one dot in the name → resolve via import map.
        // Logic identical to the typechecker (see `synth` for `Term::Var`).
        if name.matches('.').count() == 1 {
            let (prefix, suffix) = name.split_once('.').expect("checked");
            let target_module = self.import_map.get(prefix).cloned().ok_or_else(|| {
                CodegenError::Internal(format!(
                    "cross-module call `{name}`: prefix `{prefix}` not in import map"
                ))
            })?;
            // Polymorphic def in target module? Monomorphise on demand.
            if self
                .module_polymorphic_fns
                .get(&target_module)
                .is_some_and(|m| m.contains_key(suffix))
            {
                return self.lower_polymorphic_call(&target_module, suffix, args, tail);
            }
            let target_fns = self
                .module_user_fns
                .get(&target_module)
                .ok_or_else(|| {
                    CodegenError::Internal(format!(
                        "cross-module call `{name}`: target module `{target_module}` not found in workspace"
                    ))
                })?;
            let sig = target_fns
                .get(suffix)
                .cloned()
                .ok_or_else(|| {
                    CodegenError::Internal(format!(
                        "cross-module call `{name}`: def `{suffix}` not in module `{target_module}`"
                    ))
                })?;
            return self.emit_call(&target_module, suffix, &sig, args, tail);
        }

        // Polymorphic def in the current module?
        if self
            .module_polymorphic_fns
            .get(self.module_name)
            .is_some_and(|m| m.contains_key(name))
        {
            let owner = self.module_name.to_string();
            return self.lower_polymorphic_call(&owner, name, args, tail);
        }

        // User function in the current module?
        if let Some(sig) = self
            .module_user_fns
            .get(self.module_name)
            .and_then(|m| m.get(name))
            .cloned()
        {
            return self.emit_call(self.module_name, name, &sig, args, tail);
        }

        Err(CodegenError::Internal(format!(
            "unknown callee: `{name}`"
        )))
    }

    /// Iter 12b: lower a direct call to a polymorphic def. Derives the
    /// substitution from the actual arg types, queues the (def,
    /// substitution) pair for specialisation if not yet emitted, and
    /// emits a direct call to the mangled name `@ail_<m>_<def>__<descr>`.
    fn lower_polymorphic_call(
        &mut self,
        owner_module: &str,
        def_name: &str,
        args: &[Term],
        tail: bool,
    ) -> Result<(String, String)> {
        let fdef = self
            .module_polymorphic_fns
            .get(owner_module)
            .and_then(|m| m.get(def_name))
            .cloned()
            .ok_or_else(|| {
                CodegenError::Internal(format!(
                    "lower_polymorphic_call: `{owner_module}.{def_name}` not registered"
                ))
            })?;
        let (forall_vars, params, ret) = match &fdef.ty {
            Type::Forall { vars, body } => match body.as_ref() {
                Type::Fn { params, ret, .. } => {
                    (vars.clone(), params.clone(), (**ret).clone())
                }
                _ => {
                    return Err(CodegenError::Internal(format!(
                        "lower_polymorphic_call: `{def_name}` Forall body is not Fn"
                    )));
                }
            },
            _ => {
                return Err(CodegenError::Internal(format!(
                    "lower_polymorphic_call: `{def_name}` is not polymorphic"
                )));
            }
        };
        // Iter 15a: when we're calling into another module, the fn's
        // params and ret reference local type names that — from this
        // call site's perspective — are qualified `module.T`. Qualify
        // before deriving the substitution so the unification mirrors
        // what the typechecker has already validated.
        let (params, ret) = if owner_module != self.module_name {
            let owner_types = self.collect_owner_local_types(owner_module);
            (
                params
                    .iter()
                    .map(|p| qualify_local_types_codegen(p, owner_module, &owner_types))
                    .collect::<Vec<_>>(),
                qualify_local_types_codegen(&ret, owner_module, &owner_types),
            )
        } else {
            (params, ret)
        };

        // Derive the substitution by comparing the declared param
        // types against the actual arg types.
        let arg_ail_tys: Vec<Type> = args
            .iter()
            .map(|a| self.synth_arg_type(a))
            .collect::<Result<_>>()?;
        let subst = derive_substitution(&forall_vars, &params, &arg_ail_tys)?;

        // Specialised types and signature.
        let mono_params: Vec<Type> = params
            .iter()
            .map(|p| apply_subst_to_type(p, &subst))
            .collect();
        let mono_ret = apply_subst_to_type(&ret, &subst);
        let llvm_params: Vec<String> = mono_params.iter().map(llvm_type).collect::<Result<_>>()?;
        let llvm_ret = llvm_type(&mono_ret)?;
        let descriptor = descriptor_for_subst(&forall_vars, &subst);
        let mangled = format!("ail_{owner_module}_{def_name}__{descriptor}");

        // Queue specialisation (deduplicated).
        let key = (owner_module.to_string(), def_name.to_string(), descriptor.clone());
        if self.mono_emitted.insert(key) {
            self.mono_queue.push((
                owner_module.to_string(),
                def_name.to_string(),
                subst.clone(),
                descriptor,
            ));
        }

        // Lower args and emit a direct call to the mangled name.
        let mut compiled_args = Vec::new();
        for (a, exp_ty) in args.iter().zip(llvm_params.iter()) {
            let (v, vty) = self.lower_term(a)?;
            if &vty != exp_ty {
                return Err(CodegenError::Internal(format!(
                    "poly call `{owner_module}.{def_name}` arg type mismatch: expected {exp_ty}, got {vty}"
                )));
            }
            compiled_args.push((v, vty));
        }
        let arglist = compiled_args
            .iter()
            .map(|(v, t)| format!("{t} {v}"))
            .collect::<Vec<_>>()
            .join(", ");
        let dst = self.fresh_ssa();
        let call_kw = if tail { "musttail call" } else { "call" };
        self.body.push_str(&format!(
            "  {dst} = {call_kw} {ret} @{mangled}({arglist})\n",
            ret = llvm_ret,
        ));
        if tail {
            self.body
                .push_str(&format!("  ret {ret} {dst}\n", ret = llvm_ret));
            self.block_terminated = true;
        }
        Ok((dst, llvm_ret))
    }

    fn emit_call(
        &mut self,
        target_module: &str,
        target_def: &str,
        sig: &FnSig,
        args: &[Term],
        tail: bool,
    ) -> Result<(String, String)> {
        let mut compiled_args = Vec::new();
        for (a, exp_ty) in args.iter().zip(sig.params.iter()) {
            let (v, vty) = self.lower_term(a)?;
            if &vty != exp_ty {
                return Err(CodegenError::Internal(format!(
                    "call `{target_module}.{target_def}` arg type mismatch: expected {exp_ty}, got {vty}"
                )));
            }
            compiled_args.push((v, vty));
        }
        let arglist = compiled_args
            .iter()
            .map(|(v, t)| format!("{t} {v}"))
            .collect::<Vec<_>>()
            .join(", ");
        let dst = self.fresh_ssa();
        // Iter 14e: emit `musttail call ... ret` for `tail: true`. The
        // call SSA flows directly into the `ret`, satisfying LLVM's
        // "must immediately ret" rule. Same calling convention and
        // signature as the surrounding fn (the typechecker enforces
        // type compatibility).
        let call_kw = if tail { "musttail call" } else { "call" };
        self.body.push_str(&format!(
            "  {dst} = {call_kw} {ret} @ail_{module}_{name}({arglist})\n",
            ret = sig.ret,
            module = target_module,
            name = target_def,
        ));
        if tail {
            self.body
                .push_str(&format!("  ret {ret} {dst}\n", ret = sig.ret));
            self.block_terminated = true;
        }
        Ok((dst, sig.ret.clone()))
    }

    /// Iter 8a: indirect call through a closure-pair pointer. The
    /// callee SSA points at `{ ptr thunk, ptr env }`; we GEP+load both
    /// halves and call `thunk(env, args...)`. The user-visible `sig`
    /// describes only the user-level params/ret — the env_ptr is
    /// inserted by codegen, transparent to the source language.
    fn emit_indirect_call(
        &mut self,
        callee_ssa: &str,
        sig: &FnSig,
        args: &[Term],
        tail: bool,
    ) -> Result<(String, String)> {
        if args.len() != sig.params.len() {
            return Err(CodegenError::Internal(format!(
                "indirect call arity mismatch: sig expects {}, got {}",
                sig.params.len(),
                args.len()
            )));
        }
        let mut compiled = Vec::new();
        for (a, exp_ty) in args.iter().zip(sig.params.iter()) {
            let (v, vty) = self.lower_term(a)?;
            if &vty != exp_ty {
                return Err(CodegenError::Internal(format!(
                    "indirect call arg type mismatch: expected {exp_ty}, got {vty}"
                )));
            }
            compiled.push((v, vty));
        }
        // Unpack the closure pair: thunk pointer at offset 0, env pointer
        // at offset 8. Use a typed GEP through `{ ptr, ptr }` so the
        // offsets are computed correctly across targets.
        let thunk_p = self.fresh_ssa();
        let thunk = self.fresh_ssa();
        let env_p = self.fresh_ssa();
        let env = self.fresh_ssa();
        self.body.push_str(&format!(
            "  {thunk_p} = getelementptr inbounds {{ ptr, ptr }}, ptr {callee_ssa}, i64 0, i32 0\n"
        ));
        self.body
            .push_str(&format!("  {thunk} = load ptr, ptr {thunk_p}\n"));
        self.body.push_str(&format!(
            "  {env_p} = getelementptr inbounds {{ ptr, ptr }}, ptr {callee_ssa}, i64 0, i32 1\n"
        ));
        self.body
            .push_str(&format!("  {env} = load ptr, ptr {env_p}\n"));

        // Build the actual call. The thunk's signature is `(ptr, params...)`
        // — env_ptr is the implicit first arg, transparent to the user.
        let mut arglist = format!("ptr {env}");
        for (v, t) in &compiled {
            arglist.push_str(&format!(", {t} {v}"));
        }
        let mut param_tys = String::from("ptr");
        for pt in &sig.params {
            param_tys.push_str(", ");
            param_tys.push_str(pt);
        }
        let dst = self.fresh_ssa();
        // Iter 14e: indirect tail calls. Same `musttail`/`ret` shape as
        // emit_call. The thunk's signature uniformly inserts an
        // `env_ptr` first arg, but a `musttail call` to a thunk whose
        // signature exactly matches the parent fn's prototype +
        // env_ptr is malformed (parent has no env_ptr in its prototype).
        // For the MVP no fixture marks an indirect tail call; we honour
        // the flag by emitting `musttail call` (LLVM verifier will
        // catch a real signature mismatch at IR-verification time).
        let call_kw = if tail { "musttail call" } else { "call" };
        self.body.push_str(&format!(
            "  {dst} = {call_kw} {ret} ({ptys}) {thunk}({arglist})\n",
            ret = sig.ret,
            ptys = param_tys,
        ));
        if tail {
            self.body
                .push_str(&format!("  ret {ret} {dst}\n", ret = sig.ret));
            self.block_terminated = true;
        }
        Ok((dst, sig.ret.clone()))
    }

    /// Iter 8b: lower a `Term::Lam`. Walks the body to find captures
    /// (free vars relative to the enclosing scope, minus builtins and
    /// top-level fns), allocates a heap env for the captures, lifts the
    /// body to a top-level thunk fn `@ail_<m>_<def>_lam<id>`, and
    /// returns a closure-pair pointer that pairs the thunk with the env.
    fn lower_lambda(
        &mut self,
        lam_params: &[String],
        lam_param_tys: &[Type],
        lam_ret_ty: &Type,
        lam_body: &Term,
        term_ptr: usize,
    ) -> Result<(String, String)> {
        let llvm_param_tys: Vec<String> =
            lam_param_tys.iter().map(llvm_type).collect::<Result<_>>()?;
        let llvm_ret = llvm_type(lam_ret_ty)?;

        // 1. Capture analysis. The "bound" set seeds with everything
        //    that's a local in the enclosing scope OR a lambda param —
        //    but params are bound only INSIDE the body, not before. So
        //    pass them through as part of the recursion.
        let top_level: BTreeSet<String> = self
            .module_user_fns
            .get(self.module_name)
            .map(|m| m.keys().cloned().collect())
            .unwrap_or_default();
        let builtins_owned: Vec<String> = ailang_check::builtins::value_names()
            .into_iter()
            .map(|s| s.to_string())
            .collect();
        let builtins: BTreeSet<&str> =
            builtins_owned.iter().map(|s| s.as_str()).collect();

        let mut bound: BTreeSet<String> = BTreeSet::new();
        for p in lam_params {
            bound.insert(p.clone());
        }
        let mut captures: Vec<String> = Vec::new();
        let mut captures_set: BTreeSet<String> = BTreeSet::new();
        Self::collect_captures(
            lam_body,
            &mut bound,
            &mut captures,
            &mut captures_set,
            &builtins,
            &top_level,
        );

        // Outer scope provides every capture as a local — assert and
        // pull SSA + LLVM type from `self.locals`. Unknown captures
        // would mean the typechecker let through an unbound var, so a
        // hard internal error is right.
        // Tuple: (name, outer_ssa, llvm_type, ail_type, optional_fn_sig).
        let mut cap_meta: Vec<(String, String, String, Type, Option<FnSig>)> = Vec::new();
        for c in &captures {
            let (_, outer_ssa, lty, ail_ty) = self
                .locals
                .iter()
                .rev()
                .find(|(n, _, _, _)| n == c)
                .ok_or_else(|| {
                    CodegenError::Internal(format!(
                        "lambda capture `{c}` not in scope (typechecker bug?)"
                    ))
                })?
                .clone();
            let sig = self.ssa_fn_sigs.get(&outer_ssa).cloned();
            cap_meta.push((c.clone(), outer_ssa, lty, ail_ty, sig));
        }

        // 2. Pick a thunk name and switch the emitter into "thunk
        //    emission" mode by saving and resetting per-fn state.
        let lam_id = self.lam_counter;
        self.lam_counter += 1;
        let parent = self.current_def.clone();
        let thunk_name = format!("{parent}_lam{lam_id}");
        let thunk_symbol = format!("@ail_{m}_{thunk_name}", m = self.module_name);

        let saved_body = std::mem::take(&mut self.body);
        let saved_locals = std::mem::take(&mut self.locals);
        let saved_counter = self.counter;
        let saved_block = std::mem::take(&mut self.current_block);
        let saved_terminated = self.block_terminated;
        self.block_terminated = false;
        let saved_sigs = std::mem::take(&mut self.ssa_fn_sigs);
        // Iter 17a: a lambda thunk is its own fn frame for escape
        // analysis. Save the outer fn's non-escape set and recompute
        // for the lambda body. Restored at the end alongside the rest
        // of the saved emitter state.
        let saved_non_escape = std::mem::take(&mut self.non_escape);
        self.non_escape = escape::analyze_fn_body(lam_body);
        // Lambdas inside lambdas are fine: they get their own counter
        // namespace within the enclosing thunk. They share the
        // `deferred_thunks` queue (top-level body owns it).
        self.counter = 0;

        // Thunk header: `(ptr %env, params...)`.
        let mut thunk_sig = format!("define {ret} {thunk_symbol}(ptr %env", ret = llvm_ret);
        for (pname, pty) in lam_params.iter().zip(llvm_param_tys.iter()) {
            thunk_sig.push_str(&format!(", {pty} %arg_{pname}"));
        }
        thunk_sig.push_str(") {\n");
        self.body.push_str(&thunk_sig);
        self.start_block("entry");

        // Unpack captures back into named locals at the start of the
        // body. Layout: 8 bytes per slot, regardless of LLVM type
        // (typed load reads only the needed bytes; padding is wasted
        // but uniform).
        for (i, (cname, _outer, cty, c_ail, sig_opt)) in cap_meta.iter().enumerate() {
            let offset = (i * 8) as i64;
            let slot = self.fresh_ssa();
            let val = self.fresh_ssa();
            self.body.push_str(&format!(
                "  {slot} = getelementptr inbounds i8, ptr %env, i64 {offset}\n"
            ));
            self.body
                .push_str(&format!("  {val} = load {cty}, ptr {slot}\n"));
            self.locals.push((
                cname.clone(),
                val.clone(),
                cty.clone(),
                c_ail.clone(),
            ));
            if let Some(sig) = sig_opt {
                self.ssa_fn_sigs.insert(val, sig.clone());
            }
        }

        // Push lambda params as locals (after captures so shadowing
        // honors lexical order — params win).
        for ((pname, pty), pty_ail) in lam_params
            .iter()
            .zip(llvm_param_tys.iter())
            .zip(lam_param_tys.iter())
        {
            let pssa = format!("%arg_{pname}");
            self.locals.push((
                pname.clone(),
                pssa.clone(),
                pty.clone(),
                pty_ail.clone(),
            ));
            if let Some(fs) = fn_sig_from_type(pty_ail) {
                self.ssa_fn_sigs.insert(pssa, fs);
            }
        }

        let (body_v, body_ty) = self.lower_term(lam_body)?;
        if !self.block_terminated {
            if body_ty != llvm_ret {
                return Err(CodegenError::Internal(format!(
                    "lambda `{thunk_name}`: body type {body_ty} != return type {llvm_ret}"
                )));
            }
            self.body
                .push_str(&format!("  ret {body_ty} {body_v}\n}}\n\n"));
        } else {
            self.body.push_str("}\n\n");
        }

        // Park the thunk text in the deferred queue and restore outer
        // emitter state.
        let thunk_text = std::mem::take(&mut self.body);
        self.deferred_thunks.push(thunk_text);
        self.body = saved_body;
        self.locals = saved_locals;
        self.counter = saved_counter;
        self.current_block = saved_block;
        self.block_terminated = saved_terminated;
        self.ssa_fn_sigs = saved_sigs;
        self.non_escape = saved_non_escape;

        // 3. Emit allocation + capture filling + closure-pair packing
        //    in the OUTER body. Captures use 8 bytes each; closure-pair
        //    is 16 bytes.
        // Iter 17a: env and closure-pair share the Lam term's escape
        // status — they have parallel lifetimes. If the closure pair
        // does not escape (only used as a callee in the outer body),
        // both can be `alloca`'d. The escape-analysis lookup runs
        // against the outer fn's `non_escape` set (already restored
        // above).
        let lam_local = self.non_escape.contains(&term_ptr);
        let env_size = (cap_meta.len() * 8) as i64;
        let env_ssa = if env_size > 0 {
            let env = self.fresh_ssa();
            if lam_local {
                self.body.push_str(&format!(
                    "  {env} = alloca i8, i64 {env_size}, align 8\n"
                ));
            } else {
                self.body.push_str(&format!(
                    "  {env} = call ptr @{}(i64 {env_size})\n",
                    self.alloc.fn_name()
                ));
            }
            for (i, (_cname, outer_ssa, cty, _c_ail, _sig)) in cap_meta.iter().enumerate() {
                let offset = (i * 8) as i64;
                let slot = self.fresh_ssa();
                self.body.push_str(&format!(
                    "  {slot} = getelementptr inbounds i8, ptr {env}, i64 {offset}\n"
                ));
                self.body.push_str(&format!(
                    "  store {cty} {outer_ssa}, ptr {slot}\n"
                ));
            }
            env
        } else {
            "null".into()
        };

        let clos = self.fresh_ssa();
        if lam_local {
            self.body
                .push_str(&format!("  {clos} = alloca i8, i64 16, align 8\n"));
        } else {
            self.body.push_str(&format!(
                "  {clos} = call ptr @{}(i64 16)\n",
                self.alloc.fn_name()
            ));
        }
        let cs_t = self.fresh_ssa();
        self.body.push_str(&format!(
            "  {cs_t} = getelementptr inbounds {{ ptr, ptr }}, ptr {clos}, i64 0, i32 0\n"
        ));
        self.body
            .push_str(&format!("  store ptr {thunk_symbol}, ptr {cs_t}\n"));
        let cs_e = self.fresh_ssa();
        self.body.push_str(&format!(
            "  {cs_e} = getelementptr inbounds {{ ptr, ptr }}, ptr {clos}, i64 0, i32 1\n"
        ));
        self.body
            .push_str(&format!("  store ptr {env_ssa}, ptr {cs_e}\n"));

        // Register sig so subsequent indirect calls on `clos` work.
        let fs = FnSig {
            params: llvm_param_tys,
            ret: llvm_ret,
        };
        self.ssa_fn_sigs.insert(clos.clone(), fs);

        Ok((clos, "ptr".into()))
    }

    /// Iter 8b: walk a Term collecting free-variable names that should
    /// be captured by an enclosing lambda. Builtins and top-level fns
    /// are excluded — they're globally accessible. Qualified names
    /// (`prefix.def`) are excluded too.
    fn collect_captures(
        t: &Term,
        bound: &mut BTreeSet<String>,
        captures: &mut Vec<String>,
        captures_set: &mut BTreeSet<String>,
        builtins: &BTreeSet<&str>,
        top_level: &BTreeSet<String>,
    ) {
        match t {
            Term::Lit { .. } => {}
            Term::Var { name } => {
                if name.contains('.') {
                    return; // qualified ref is module-level
                }
                if bound.contains(name) {
                    return;
                }
                if builtins.contains(name.as_str()) {
                    return;
                }
                if top_level.contains(name) {
                    return;
                }
                if captures_set.insert(name.clone()) {
                    captures.push(name.clone());
                }
            }
            Term::App { callee, args, .. } => {
                Self::collect_captures(callee, bound, captures, captures_set, builtins, top_level);
                for a in args {
                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
                }
            }
            Term::Let { name, value, body } => {
                Self::collect_captures(value, bound, captures, captures_set, builtins, top_level);
                let inserted = bound.insert(name.clone());
                Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
                if inserted {
                    bound.remove(name);
                }
            }
            Term::If { cond, then, else_ } => {
                Self::collect_captures(cond, bound, captures, captures_set, builtins, top_level);
                Self::collect_captures(then, bound, captures, captures_set, builtins, top_level);
                Self::collect_captures(else_, bound, captures, captures_set, builtins, top_level);
            }
            Term::Do { args, .. } => {
                for a in args {
                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
                }
            }
            Term::Ctor { args, .. } => {
                for a in args {
                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
                }
            }
            Term::Match { scrutinee, arms } => {
                Self::collect_captures(scrutinee, bound, captures, captures_set, builtins, top_level);
                for arm in arms {
                    let mut pat_bindings = Vec::new();
                    Self::pattern_bound_names(&arm.pat, &mut pat_bindings);
                    let mut newly_bound = Vec::new();
                    for n in &pat_bindings {
                        if bound.insert(n.clone()) {
                            newly_bound.push(n.clone());
                        }
                    }
                    Self::collect_captures(&arm.body, bound, captures, captures_set, builtins, top_level);
                    for n in newly_bound {
                        bound.remove(&n);
                    }
                }
            }
            Term::Lam { params, body, .. } => {
                // Inner lambda's params don't escape; its free vars
                // (relative to the outer) DO contribute to outer captures.
                let mut newly_bound = Vec::new();
                for p in params {
                    if bound.insert(p.clone()) {
                        newly_bound.push(p.clone());
                    }
                }
                Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
                for n in newly_bound {
                    bound.remove(&n);
                }
            }
            Term::Seq { lhs, rhs } => {
                Self::collect_captures(lhs, bound, captures, captures_set, builtins, top_level);
                Self::collect_captures(rhs, bound, captures, captures_set, builtins, top_level);
            }
            Term::LetRec { .. } => {
                // Iter 16b.1: eliminated by desugar before codegen.
                unreachable!("Term::LetRec eliminated by desugar")
            }
        }
    }

    fn pattern_bound_names(p: &Pattern, out: &mut Vec<String>) {
        match p {
            Pattern::Wild | Pattern::Lit { .. } => {}
            Pattern::Var { name } => out.push(name.clone()),
            Pattern::Ctor { fields, .. } => {
                for f in fields {
                    Self::pattern_bound_names(f, out);
                }
            }
        }
    }

    /// Iter 7: is `name` a callee that can be resolved at compile time
    /// (no fn-pointer needed)? True for builtin operators, the
    /// current-module top-level fns (mono or poly), and qualified
    /// `prefix.def`. Locals shadow this — the caller checks for
    /// that first.
    fn is_static_callee(&self, name: &str) -> bool {
        if builtin_binop(name).is_some() || name == "not" {
            return true;
        }
        if name.matches('.').count() == 1 {
            return true;
        }
        if self
            .module_user_fns
            .get(self.module_name)
            .is_some_and(|m| m.contains_key(name))
        {
            return true;
        }
        self.module_polymorphic_fns
            .get(self.module_name)
            .is_some_and(|m| m.contains_key(name))
    }

    /// Iter 8a: resolve `name` to a top-level fn-value, i.e. the address
    /// of its static closure pair `@ail_<m>_<def>_clos`, plus the user-
    /// visible FnSig (params/ret WITHOUT the env_ptr — that's added at
    /// the call site by the closure ABI). Returns None if the name does
    /// not refer to a top-level fn. Operators / `not` are not first-
    /// class values; `is_static_callee` filters them earlier.
    fn resolve_top_level_fn(&self, name: &str) -> Option<(String, FnSig)> {
        if name.matches('.').count() == 1 {
            let (prefix, suffix) = name.split_once('.')?;
            let target = self.import_map.get(prefix)?;
            let sig = self.module_user_fns.get(target)?.get(suffix)?.clone();
            return Some((format!("@ail_{target}_{suffix}_clos"), sig));
        }
        let sig = self
            .module_user_fns
            .get(self.module_name)?
            .get(name)?
            .clone();
        Some((
            format!("@ail_{module}_{name}_clos", module = self.module_name),
            sig,
        ))
    }

    /// Iter 15b: resolve a `Term::Var` reference to a const def. Returns
    /// `(owning_module, ConstDef)` on hit. Both bare current-module
    /// references and qualified `prefix.name` cross-module references
    /// resolve through the same path; the prefix routes through the
    /// emitter's `import_map` to the actual module.
    fn resolve_const(&self, name: &str) -> Option<(String, ConstDef)> {
        if name.matches('.').count() == 1 {
            let (prefix, suffix) = name.split_once('.')?;
            let target = self.import_map.get(prefix)?;
            let cdef = self.module_consts.get(target)?.get(suffix)?.clone();
            return Some((target.clone(), cdef));
        }
        let cdef = self
            .module_consts
            .get(self.module_name)?
            .get(name)?
            .clone();
        Some((self.module_name.to_string(), cdef))
    }

    fn lower_effect_op(&mut self, op: &str, args: &[Term], tail: bool) -> Result<(String, String)> {
        // Iter 14e: `musttail` requires identical caller/callee
        // prototypes (same return type, same param types). The MVP's
        // runtime print helpers (`printf`, `puts`) return `i32`, but the
        // AILang fn enclosing a `tail-do io/print_*` returns `Unit`
        // (`i8`). `musttail` would be rejected by the LLVM verifier.
        // We therefore use the `tail` keyword (LLVM IR optimisation
        // hint, NOT a guarantee) for `tail: true` do-ops. The optimiser
        // is free to TCO it; if it can't, the call falls back to a
        // normal call. The body of the AILang fn afterwards is empty
        // (the op was the last thing), so we close it with `ret i8 0`.
        let _ = tail;
        let call_kw = if tail { "tail call" } else { "call" };
        match op {
            "io/print_int" => {
                if args.len() != 1 {
                    return Err(CodegenError::Internal(
                        "io/print_int arity".into(),
                    ));
                }
                let (v, vty) = self.lower_term(&args[0])?;
                if vty != "i64" {
                    return Err(CodegenError::Internal(
                        "io/print_int needs i64".into(),
                    ));
                }
                let fmt = self.intern_string("fmt_int", "%lld\n");
                self.body.push_str(&format!(
                    "  {call_kw} i32 (ptr, ...) @printf(ptr @{fmt}, i64 {v})\n"
                ));
                if tail {
                    self.body.push_str("  ret i8 0\n");
                    self.block_terminated = true;
                }
                Ok(("0".into(), "i8".into()))
            }
            "io/print_str" => {
                if args.len() != 1 {
                    return Err(CodegenError::Internal(
                        "io/print_str arity".into(),
                    ));
                }
                let (v, vty) = self.lower_term(&args[0])?;
                if vty != "ptr" {
                    return Err(CodegenError::Internal(
                        "io/print_str needs ptr".into(),
                    ));
                }
                self.body
                    .push_str(&format!("  {call_kw} i32 @puts(ptr {v})\n"));
                if tail {
                    self.body.push_str("  ret i8 0\n");
                    self.block_terminated = true;
                }
                Ok(("0".into(), "i8".into()))
            }
            "io/print_bool" => {
                if args.len() != 1 {
                    return Err(CodegenError::Internal(
                        "io/print_bool arity".into(),
                    ));
                }
                let (v, vty) = self.lower_term(&args[0])?;
                if vty != "i1" {
                    return Err(CodegenError::Internal(
                        "io/print_bool needs i1".into(),
                    ));
                }
                // Print "true\n" or "false\n".
                let fmt_t = self.intern_string("fmt_true", "true\n");
                let fmt_f = self.intern_string("fmt_false", "false\n");
                let id = self.fresh_id();
                let then_lbl = format!("ptbl_t.{id}");
                let else_lbl = format!("ptbl_f.{id}");
                let join_lbl = format!("ptbl_j.{id}");
                self.body.push_str(&format!(
                    "  br i1 {v}, label %{then_lbl}, label %{else_lbl}\n"
                ));
                self.start_block(&then_lbl);
                self.body.push_str(&format!(
                    "  call i32 (ptr, ...) @printf(ptr @{fmt_t})\n"
                ));
                self.body.push_str(&format!("  br label %{join_lbl}\n"));
                self.start_block(&else_lbl);
                self.body.push_str(&format!(
                    "  call i32 (ptr, ...) @printf(ptr @{fmt_f})\n"
                ));
                self.body.push_str(&format!("  br label %{join_lbl}\n"));
                self.start_block(&join_lbl);
                if tail {
                    self.body.push_str("  ret i8 0\n");
                    self.block_terminated = true;
                }
                Ok(("0".into(), "i8".into()))
            }
            other => Err(CodegenError::Internal(format!(
                "unknown effect op: {other}"
            ))),
        }
    }

    /// Iter 16e: lower a `==` call after the two operands have been
    /// emitted. Dispatches on the resolved AIL type of the arg side
    /// (both sides have the same type after typecheck). The `_a_ll`
    /// hint is the LLVM type the lowering produced for `a`; we use
    /// it as a sanity check against `arg_ty`'s expected LLVM shape.
    ///
    /// Supported:
    /// - `Int` → `icmp eq i64`
    /// - `Bool` → `icmp eq i1`
    /// - `Str` → `@strcmp` then `icmp eq i32 0`
    /// - `Unit` → constant `i1 true` (both sides already evaluated
    ///   for any side effects; Unit has a single inhabitant).
    ///
    /// Rejected with `CodegenError::Internal` for ADT, `Fn`, and any
    /// other type — those would need either a structural-equality
    /// scheme (ADT) or a fn-pointer compare (Fn) that the language
    /// does not yet specify.
    fn lower_eq(
        &mut self,
        arg_ty: &Type,
        a: &str,
        b: &str,
        _a_ll: &str,
    ) -> Result<(String, String)> {
        match arg_ty {
            Type::Con { name, .. } => match name.as_str() {
                "Int" => {
                    let dst = self.fresh_ssa();
                    self.body.push_str(&format!(
                        "  {dst} = icmp eq i64 {a}, {b}\n"
                    ));
                    Ok((dst, "i1".into()))
                }
                "Bool" => {
                    let dst = self.fresh_ssa();
                    self.body.push_str(&format!(
                        "  {dst} = icmp eq i1 {a}, {b}\n"
                    ));
                    Ok((dst, "i1".into()))
                }
                "Str" => {
                    let cmp = self.fresh_ssa();
                    self.body.push_str(&format!(
                        "  {cmp} = call i32 @strcmp(ptr {a}, ptr {b})\n"
                    ));
                    let dst = self.fresh_ssa();
                    self.body.push_str(&format!(
                        "  {dst} = icmp eq i32 {cmp}, 0\n"
                    ));
                    Ok((dst, "i1".into()))
                }
                "Unit" => {
                    // Both sides have already been evaluated above for
                    // any side effects; Unit has a single inhabitant,
                    // so equality is `true` by definition.
                    let _ = a;
                    let _ = b;
                    Ok(("true".into(), "i1".into()))
                }
                other => Err(CodegenError::Internal(format!(
                    "`==` not supported for type `{other}` \
                     (ADT and user-defined types lack a structural-equality scheme)"
                ))),
            },
            Type::Fn { .. } => Err(CodegenError::Internal(
                "`==` not supported for function types (no canonical fn-pointer equality)".into(),
            )),
            other => Err(CodegenError::Internal(format!(
                "`==` not supported for type `{}`",
                ailang_core::pretty::type_to_string(other)
            ))),
        }
    }

    fn fresh_ssa(&mut self) -> String {
        self.counter += 1;
        format!("%v{}", self.counter)
    }
    fn fresh_id(&mut self) -> u64 {
        self.counter += 1;
        self.counter
    }

    fn intern_string(&mut self, hint: &str, content: &str) -> String {
        if let Some((name, _)) = self.strings.get(content) {
            return name.clone();
        }
        // Mangling per module: `.str_<module>_<hint>_<idx>`.
        let name = format!(".str_{}_{}_{}", self.module_name, hint, self.str_counter);
        self.str_counter += 1;
        let len = c_byte_len(content);
        self.strings
            .insert(content.to_string(), (name.clone(), len));
        name
    }

    /// Iter 12b: lightweight AILang-type computation for an expression
    /// in the current scope. Mirrors what the typechecker already
    /// derived; we replay it here only because the typechecker doesn't
    /// hand its annotations down.
    ///
    /// Used at polymorphic call sites to derive the type substitution
    /// from the actual argument types, at let-bindings / match-arm
    /// scrutinees to populate the AILang-type slot of locals. Trusts
    /// the typechecker for well-formedness — failures here are internal
    /// errors (e.g. unbound var that the checker should have rejected).
    ///
    /// Limitations: nested polymorphic instantiations (an arg that is
    /// itself a polymorphic call) work via `synth_with_extras`'s
    /// recursion; the substitution is derived on-the-fly and applied
    /// to the return type. The body of a let is walked with the
    /// let-bound name added to a small `extras` shadow stack so we
    /// don't need `&mut self`.
    fn synth_arg_type(&self, t: &Term) -> Result<Type> {
        self.synth_with_extras(t, &[])
    }

    fn synth_with_extras(&self, t: &Term, extras: &[(String, Type)]) -> Result<Type> {
        match t {
            Term::Lit { lit } => Ok(match lit {
                Literal::Int { .. } => Type::int(),
                Literal::Bool { .. } => Type::bool_(),
                Literal::Str { .. } => Type::str_(),
                Literal::Unit => Type::unit(),
            }),
            Term::Var { name } => {
                // Lookup precedence: extras (let-bindings introduced
                // during this synth walk) → emitter locals → globals
                // → builtins. Mirrors typechecker shadowing.
                for (n, ty) in extras.iter().rev() {
                    if n == name {
                        return Ok(ty.clone());
                    }
                }
                if let Some((_, _, _, ail)) =
                    self.locals.iter().rev().find(|(n, _, _, _)| n == name)
                {
                    return Ok(ail.clone());
                }
                if name.matches('.').count() == 1 {
                    let (prefix, suffix) = name.split_once('.').expect("checked");
                    if let Some(target) = self.import_map.get(prefix) {
                        if let Some(ty) = self
                            .module_def_ail_types
                            .get(target)
                            .and_then(|m| m.get(suffix))
                        {
                            // Iter 15a: qualify any bare type-cons that
                            // refer to types declared in `target` so the
                            // returned signature lines up with the
                            // qualified ctors / type names produced
                            // elsewhere in the consumer module. Mirrors
                            // the typechecker's `qualify_local_types`.
                            let owner_local_types = self.collect_owner_local_types(target);
                            return Ok(qualify_local_types_codegen(
                                ty,
                                target,
                                &owner_local_types,
                            ));
                        }
                    }
                }
                if let Some(ty) = self
                    .module_def_ail_types
                    .get(self.module_name)
                    .and_then(|m| m.get(name))
                {
                    return Ok(ty.clone());
                }
                // Iter 15b: const refs participate in arg-type
                // synthesis. Bare or qualified, both forms route
                // through `resolve_const` and yield the const's
                // declared type. Const types are already qualified
                // (the AST writes them in the consumer's namespace
                // via `module.Type`), so no further qualification
                // is needed.
                if let Some((_, cdef)) = self.resolve_const(name) {
                    return Ok(cdef.ty);
                }
                if let Some(t) = builtin_ail_type(name) {
                    return Ok(t);
                }
                Err(CodegenError::UnknownVar(name.clone()))
            }
            Term::Lam {
                param_tys,
                ret_ty,
                effects,
                ..
            } => Ok(Type::Fn {
                params: param_tys.clone(),
                ret: ret_ty.clone(),
                effects: effects.clone(),
            }),
            Term::App { callee, args, .. } => {
                let cty = self.synth_with_extras(callee, extras)?;
                match cty {
                    Type::Fn { ret, .. } => Ok(*ret),
                    Type::Forall { vars, body } => {
                        let arg_tys: Vec<Type> = args
                            .iter()
                            .map(|a| self.synth_with_extras(a, extras))
                            .collect::<Result<_>>()?;
                        let (params, ret) = match body.as_ref() {
                            Type::Fn { params, ret, .. } => (params.clone(), (**ret).clone()),
                            _ => {
                                return Err(CodegenError::Internal(
                                    "synth_arg_type: forall body is not Fn".into(),
                                ));
                            }
                        };
                        let subst = derive_substitution(&vars, &params, &arg_tys)?;
                        Ok(apply_subst_to_type(&ret, &subst))
                    }
                    other => Err(CodegenError::Internal(format!(
                        "synth_arg_type: callee not a fn type: {}",
                        ailang_core::pretty::type_to_string(&other)
                    ))),
                }
            }
            Term::Let { name, value, body } => {
                let v_ail = self.synth_with_extras(value, extras)?;
                let mut new_extras: Vec<(String, Type)> = extras.to_vec();
                new_extras.push((name.clone(), v_ail));
                self.synth_with_extras(body, &new_extras)
            }
            Term::If { then, .. } => self.synth_with_extras(then, extras),
            Term::Do { op, .. } => builtin_effect_op_ret(op).ok_or_else(|| {
                CodegenError::Internal(format!(
                    "synth_arg_type: unknown effect op `{op}`"
                ))
            }),
            Term::Ctor { type_name, ctor, args } => {
                // Iter 13b: derive concrete type-args of a parameterised
                // ADT instance from the recursively-synthesised arg
                // types. For monomorphic ADTs (`type_vars.is_empty()`)
                // we keep the pre-13b shape `Type::Con { args: vec![] }`
                // — matching what the typechecker produces.
                // Iter 15a: a qualified `type_name` resolves through the
                // cross-module ctor index. The result `Type::Con.name`
                // stays qualified to match what the typechecker emits.
                // Iter 15b: when the ctor is cross-module, `cref.ail_fields`
                // is written in the owning module's local namespace, so a
                // recursive self-reference like `Cons a (List a)` carries
                // a bare `Con("List", _)` even though every other place
                // sees the qualified `std_list.List<...>`. Apply
                // `qualify_local_types_codegen` before `unify_for_subst`
                // so the unification doesn't fail on name mismatch.
                let cref = self.lookup_ctor_by_type(type_name, ctor)?;
                if cref.type_vars.is_empty() {
                    return Ok(Type::Con {
                        name: type_name.clone(),
                        args: vec![],
                    });
                }
                let qualified_ail_fields: Vec<Type> = if type_name.matches('.').count() == 1 {
                    let (prefix, _) = type_name.split_once('.').expect("checked");
                    if let Some(target) = self.import_map.get(prefix) {
                        let owner_local_types = self.collect_owner_local_types(target);
                        cref.ail_fields
                            .iter()
                            .map(|f| qualify_local_types_codegen(f, target, &owner_local_types))
                            .collect()
                    } else {
                        cref.ail_fields.clone()
                    }
                } else {
                    cref.ail_fields.clone()
                };
                let arg_tys: Vec<Type> = args
                    .iter()
                    .map(|a| self.synth_with_extras(a, extras))
                    .collect::<Result<_>>()?;
                let var_set: BTreeSet<&str> =
                    cref.type_vars.iter().map(|s| s.as_str()).collect();
                let mut subst: BTreeMap<String, Type> = BTreeMap::new();
                for (exp, actual) in qualified_ail_fields.iter().zip(arg_tys.iter()) {
                    unify_for_subst(exp, actual, &var_set, &mut subst)?;
                }
                // Vars not pinned by ctor args (e.g. `Nil` for `List a`,
                // `None` for `Maybe a`) are filled with a synth-only
                // wildcard `Type::Var { name: "$u" }`. The `$u`-prefix
                // is reserved here (mirrors the checker's `$m` for
                // metavars) and is treated as a match-anything wildcard
                // by `unify_for_subst` on the arg side. This matters
                // when a nullary ctor like `Nil` is nested inside a
                // parent ctor whose other args pin the same type var
                // concretely — e.g. `Cons(Int, Nil) : List<a>` must
                // pin `a = Int` from the head and let the tail's
                // unconstrained `a` defer rather than collide on
                // `Type::unit()` as it would have pre-fix.
                let resolved: Vec<Type> = cref
                    .type_vars
                    .iter()
                    .map(|v| {
                        subst
                            .get(v)
                            .cloned()
                            .unwrap_or_else(|| Type::Var { name: "$u".into() })
                    })
                    .collect();
                Ok(Type::Con {
                    name: type_name.clone(),
                    args: resolved,
                })
            }
            Term::Match { arms, .. } => {
                if let Some(first) = arms.first() {
                    self.synth_with_extras(&first.body, extras)
                } else {
                    Err(CodegenError::Internal(
                        "synth_arg_type: empty match".into(),
                    ))
                }
            }
            Term::Seq { rhs, .. } => self.synth_with_extras(rhs, extras),
            Term::LetRec { .. } => {
                // Iter 16b.1: eliminated by desugar before codegen.
                unreachable!("Term::LetRec eliminated by desugar")
            }
        }
    }
}

fn llvm_type(t: &Type) -> Result<String> {
    match t {
        Type::Con { name, .. } => match name.as_str() {
            "Int" => Ok("i64".into()),
            "Bool" => Ok("i1".into()),
            "Unit" => Ok("i8".into()),
            "Str" => Ok("ptr".into()),
            // All other type names are treated as ADT (boxed).
            // If the typechecker didn't reject this earlier, it's
            // intentional — otherwise `ptr` would mask a wrong value.
            _ => Ok("ptr".into()),
        },
        // Function values (Iter 7): all fn-pointers are opaque `ptr`
        // at the LLVM level. The actual signature travels via the
        // emitter's `ssa_fn_sigs` sidetable.
        Type::Fn { .. } => Ok("ptr".into()),
        // Iter 13b: an unresolved rigid `Type::Var` reaching codegen is
        // a substitution bug. Earlier this silently lowered as `ptr`
        // (via the ADT fallback) and produced garbage IR; failing loudly
        // here surfaces the bug in the test suite.
        Type::Var { name } => Err(CodegenError::UnsupportedType(format!(
            "unresolved type var `{name}` in codegen"
        ))),
        other => Err(CodegenError::UnsupportedType(
            ailang_core::pretty::type_to_string(other),
        )),
    }
}

/// Builds an `FnSig` (LLVM types only) from an AILang `Type::Fn`.
/// Returns `None` for non-function types or if any param/ret type fails
/// to lower (e.g. a residual `Type::Var` or `Forall` that the typechecker
/// would reject before us).
fn fn_sig_from_type(t: &Type) -> Option<FnSig> {
    if let Type::Fn { params, ret, .. } = t {
        let p: Result<Vec<String>> = params.iter().map(llvm_type).collect();
        let r = llvm_type(ret);
        if let (Ok(p), Ok(r)) = (p, r) {
            return Some(FnSig { params: p, ret: r });
        }
    }
    None
}

/// Iter 12b: AILang type of a builtin operator. Used by
/// `synth_arg_type` for arg-type inference at polymorphic call sites.
/// Mirrors what the typechecker installs in its env via `builtins`.
fn builtin_ail_type(name: &str) -> Option<Type> {
    let int_int_int = || Type::Fn {
        params: vec![Type::int(), Type::int()],
        ret: Box::new(Type::int()),
        effects: vec![],
    };
    let int_int_bool = || Type::Fn {
        params: vec![Type::int(), Type::int()],
        ret: Box::new(Type::bool_()),
        effects: vec![],
    };
    Some(match name {
        "+" | "-" | "*" | "/" | "%" => int_int_int(),
        "!=" | "<" | "<=" | ">" | ">=" => int_int_bool(),
        // Iter 16e: `==` is polymorphic — `forall a. (a, a) -> Bool`.
        // The mono pipeline asks `synth_arg_type` for the actual arg
        // types at the call site; `lower_app` then dispatches to the
        // right LLVM instruction (icmp eq i64 / i1, @strcmp, or
        // constant i1 1) on those resolved types.
        "==" => Type::Forall {
            vars: vec!["a".into()],
            body: Box::new(Type::Fn {
                params: vec![
                    Type::Var { name: "a".into() },
                    Type::Var { name: "a".into() },
                ],
                ret: Box::new(Type::bool_()),
                effects: vec![],
            }),
        },
        "not" => Type::Fn {
            params: vec![Type::bool_()],
            ret: Box::new(Type::bool_()),
            effects: vec![],
        },
        // Iter 16d: `__unreachable__` is the polymorphic bottom value
        // (`forall a. a`). Mirrors the typechecker's `builtins::install`.
        "__unreachable__" => Type::Forall {
            vars: vec!["a".into()],
            body: Box::new(Type::Var { name: "a".into() }),
        },
        _ => return None,
    })
}

/// Iter 12b: AILang return type of a built-in effect op. The op's
/// param signature is irrelevant here since we only consume the ret.
fn builtin_effect_op_ret(op: &str) -> Option<Type> {
    Some(match op {
        "io/print_int" | "io/print_bool" | "io/print_str" => Type::unit(),
        _ => return None,
    })
}

/// Iter 12b: derive a name → concrete-type substitution from the
/// declared params of a `Forall` body and the actual arg types at a
/// call site. Walks both sides in parallel; whenever a `Type::Var`
/// (rigid name) appears on the params side, binds it to the
/// corresponding concrete type. Conflicts (same var bound to two
/// different types) surface as an internal error — the typechecker
/// would already have rejected such a call.
fn derive_substitution(
    vars: &[String],
    params: &[Type],
    arg_tys: &[Type],
) -> Result<BTreeMap<String, Type>> {
    if params.len() != arg_tys.len() {
        return Err(CodegenError::Internal(format!(
            "derive_substitution: arity mismatch ({} params vs {} args)",
            params.len(),
            arg_tys.len(),
        )));
    }
    let var_set: BTreeSet<&str> = vars.iter().map(|s| s.as_str()).collect();
    let mut subst: BTreeMap<String, Type> = BTreeMap::new();
    for (p, a) in params.iter().zip(arg_tys.iter()) {
        unify_for_subst(p, a, &var_set, &mut subst)?;
    }
    // Any forall var not pinned by the args is left unbound. For the
    // MVP this is an error — we can't specialise without a concrete
    // type. The typechecker's body should have constrained it already
    // through return-type unification, but at the call site we only
    // see args; if needed, callers can extend this with expected-ret
    // info.
    // Iter 15a: a forall var that the args couldn't pin (e.g.
    // `is_none(Nothing) : forall a. (Maybe a) -> Bool` — `a` is
    // genuinely unobservable from the args alone) defaults to `Unit`.
    // The specialised body must not actually read an `a`-typed value,
    // or it would have failed type-checking; a dummy concrete type is
    // sound and lets monomorphisation proceed deterministically. The
    // descriptor uses the same default, so all such call sites
    // converge on a single specialisation.
    for v in vars {
        if !subst.contains_key(v) {
            subst.insert(v.clone(), Type::unit());
        }
    }
    Ok(subst)
}

/// Walks `param` and `arg` in parallel, treating any `Type::Var { name }`
/// on the param side whose name is in `vars` as an unknown to be bound
/// in `subst`. Identical concrete shapes pass through; structural
/// mismatches yield an internal error.
fn unify_for_subst(
    param: &Type,
    arg: &Type,
    vars: &BTreeSet<&str>,
    subst: &mut BTreeMap<String, Type>,
) -> Result<()> {
    // Iter 14a fix, extended in 15g-aux: a `$u`-prefixed var is a
    // synth-only wildcard produced by `synth_arg_type` for nullary
    // ctors of a parameterised ADT (e.g. `Nil : List<$u>`). It
    // carries no real constraint — accept without binding so a
    // sibling arg can pin the type var instead. Without this,
    // `Cons(Int, Nil)` synth would unify `a = Int` (from head) and
    // then `a = $u` (from tail's recursive `List<a>` slot) and
    // falsely error.
    //
    // 15g-aux: the early-return must accept `$u` on **either** side.
    // `$u` enters in arg position from synth, but the prev-binding
    // recursion below (`unify_for_subst(&prev, arg, ...)`) can swap
    // a `$u` onto the param side when a previously-bound type is
    // unified against a fresher arg whose roles differ. Reduced
    // repro: `length [Left 1, Right 10]` — `a` first binds to
    // `Either<Int, $u>` from `Left 1`, then a recursive unification
    // against `Either<$u, Int>` from `Right 10` lands `$u` in the
    // param-pos[1] slot. Symmetric early-return is correct because
    // `$u` is a synth-only wildcard regardless of which side carries
    // it after the prev-binding swap.
    if let Type::Var { name } = arg {
        if name.starts_with("$u") {
            return Ok(());
        }
    }
    if let Type::Var { name } = param {
        if name.starts_with("$u") {
            return Ok(());
        }
    }
    match (param, arg) {
        (Type::Var { name }, _) if vars.contains(name.as_str()) => {
            if let Some(prev) = subst.get(name).cloned() {
                // Iter 15b: the previously-bound type may be more
                // concrete than `arg` (e.g. `prev = List<Int>` from a
                // sibling binding, `arg = List<$u>` from a synth-
                // wildcard nullary ctor). Use recursive unification
                // instead of strict equality so the inner `$u`
                // wildcard matches `Int`. The previous strict-
                // equality check rejected such overlaps as bogus
                // duplicate bindings.
                return unify_for_subst(&prev, arg, vars, subst);
            }
            subst.insert(name.clone(), arg.clone());
            Ok(())
        }
        (
            Type::Con { name: pn, args: pa },
            Type::Con { name: an, args: aa },
        ) if pn == an && pa.len() == aa.len() => {
            for (p, a) in pa.iter().zip(aa.iter()) {
                unify_for_subst(p, a, vars, subst)?;
            }
            Ok(())
        }
        (
            Type::Fn { params: pp, ret: pr, .. },
            Type::Fn { params: ap, ret: ar, .. },
        ) => {
            if pp.len() != ap.len() {
                return Err(CodegenError::Internal(
                    "monomorphisation: fn arity mismatch in arg".into(),
                ));
            }
            for (p, a) in pp.iter().zip(ap.iter()) {
                unify_for_subst(p, a, vars, subst)?;
            }
            unify_for_subst(pr, ar, vars, subst)
        }
        (Type::Var { name: pn }, Type::Var { name: an }) if pn == an => Ok(()),
        _ => Err(CodegenError::Internal(format!(
            "monomorphisation: cannot match param `{}` to arg `{}`",
            ailang_core::pretty::type_to_string(param),
            ailang_core::pretty::type_to_string(arg),
        ))),
    }
}

/// Iter 15a: rewrites bare `Type::Con` references that resolve against
/// `owner_local_types` into qualified `module.Type` form. Mirrors
/// `ailang_check::qualify_local_types`. Used when the codegen pulls a
/// polymorphic fn signature across the import boundary; without this
/// the substitution derived from the call site's qualified args
/// (`std_maybe.Maybe<Int>`) would fail to unify against the bare
/// signature (`Maybe<a>`).
fn qualify_local_types_codegen(
    t: &Type,
    owner_module: &str,
    owner_local_types: &BTreeSet<String>,
) -> Type {
    match t {
        Type::Con { name, args } => {
            let qualified = if name.contains('.') {
                name.clone()
            } else if matches!(name.as_str(), "Int" | "Bool" | "Unit" | "Str") {
                name.clone()
            } else if owner_local_types.contains(name) {
                format!("{owner_module}.{name}")
            } else {
                name.clone()
            };
            Type::Con {
                name: qualified,
                args: args
                    .iter()
                    .map(|a| qualify_local_types_codegen(a, owner_module, owner_local_types))
                    .collect(),
            }
        }
        Type::Fn { params, ret, effects } => Type::Fn {
            params: params
                .iter()
                .map(|p| qualify_local_types_codegen(p, owner_module, owner_local_types))
                .collect(),
            ret: Box::new(qualify_local_types_codegen(ret, owner_module, owner_local_types)),
            effects: effects.clone(),
        },
        Type::Forall { vars, body } => Type::Forall {
            vars: vars.clone(),
            body: Box::new(qualify_local_types_codegen(body, owner_module, owner_local_types)),
        },
        Type::Var { .. } => t.clone(),
    }
}

/// Iter 12b: substitute rigid type vars in `t` according to `subst`.
/// Used to specialise the type of a polymorphic def for a given
/// instantiation.
fn apply_subst_to_type(t: &Type, subst: &BTreeMap<String, Type>) -> Type {
    match t {
        Type::Var { name } => subst.get(name).cloned().unwrap_or_else(|| t.clone()),
        Type::Con { name, args } => Type::Con {
            name: name.clone(),
            args: args.iter().map(|a| apply_subst_to_type(a, subst)).collect(),
        },
        Type::Fn { params, ret, effects } => Type::Fn {
            params: params.iter().map(|p| apply_subst_to_type(p, subst)).collect(),
            ret: Box::new(apply_subst_to_type(ret, subst)),
            effects: effects.clone(),
        },
        Type::Forall { vars, body } => {
            // Inner forall shadows: don't substitute re-bound names.
            let inner: BTreeMap<String, Type> = subst
                .iter()
                .filter(|(k, _)| !vars.contains(k))
                .map(|(k, v)| (k.clone(), v.clone()))
                .collect();
            Type::Forall {
                vars: vars.clone(),
                body: Box::new(apply_subst_to_type(body, &inner)),
            }
        }
    }
}

/// Iter 12b: substitute rigid type vars throughout a Term. Only
/// `Term::Lam` carries types in the AST (params/ret), so most arms
/// just recurse. `Term::Var` contains a name string only and is
/// left untouched.
fn apply_subst_to_term(t: &Term, subst: &BTreeMap<String, Type>) -> Term {
    match t {
        Term::Lit { .. } | Term::Var { .. } => t.clone(),
        Term::App { callee, args, tail } => Term::App {
            callee: Box::new(apply_subst_to_term(callee, subst)),
            args: args.iter().map(|a| apply_subst_to_term(a, subst)).collect(),
            tail: *tail,
        },
        Term::Let { name, value, body } => Term::Let {
            name: name.clone(),
            value: Box::new(apply_subst_to_term(value, subst)),
            body: Box::new(apply_subst_to_term(body, subst)),
        },
        Term::If { cond, then, else_ } => Term::If {
            cond: Box::new(apply_subst_to_term(cond, subst)),
            then: Box::new(apply_subst_to_term(then, subst)),
            else_: Box::new(apply_subst_to_term(else_, subst)),
        },
        Term::Do { op, args, tail } => Term::Do {
            op: op.clone(),
            args: args.iter().map(|a| apply_subst_to_term(a, subst)).collect(),
            tail: *tail,
        },
        Term::Ctor { type_name, ctor, args } => Term::Ctor {
            type_name: type_name.clone(),
            ctor: ctor.clone(),
            args: args.iter().map(|a| apply_subst_to_term(a, subst)).collect(),
        },
        Term::Match { scrutinee, arms } => Term::Match {
            scrutinee: Box::new(apply_subst_to_term(scrutinee, subst)),
            arms: arms
                .iter()
                .map(|a| Arm {
                    pat: a.pat.clone(),
                    body: apply_subst_to_term(&a.body, subst),
                })
                .collect(),
        },
        Term::Lam { params, param_tys, ret_ty, effects, body } => Term::Lam {
            params: params.clone(),
            param_tys: param_tys
                .iter()
                .map(|t| apply_subst_to_type(t, subst))
                .collect(),
            ret_ty: Box::new(apply_subst_to_type(ret_ty, subst)),
            effects: effects.clone(),
            body: Box::new(apply_subst_to_term(body, subst)),
        },
        Term::Seq { lhs, rhs } => Term::Seq {
            lhs: Box::new(apply_subst_to_term(lhs, subst)),
            rhs: Box::new(apply_subst_to_term(rhs, subst)),
        },
        Term::LetRec { .. } => {
            // Iter 16b.1: eliminated by desugar before any
            // monomorphisation pass runs.
            unreachable!("Term::LetRec eliminated by desugar")
        }
    }
}

/// Iter 12b: deterministic descriptor string for a substitution. Used
/// as the suffix in the mangled name `@ail_<m>_<def>__<descriptor>`.
/// Vars are emitted in the order given by the FnDef's forall vars
/// (so two call sites with the same instantiation map to the same
/// descriptor regardless of internal BTreeMap ordering).
fn descriptor_for_subst(vars: &[String], subst: &BTreeMap<String, Type>) -> String {
    let mut parts: Vec<String> = Vec::with_capacity(vars.len());
    for v in vars {
        let ty = subst.get(v).cloned().unwrap_or_else(|| Type::unit());
        parts.push(type_descriptor(&ty));
    }
    parts.join("_")
}

/// Iter 12b: a stable, identifier-safe descriptor for a `Type`.
/// Maps `Int → I`, `Bool → B`, `Unit → U`, `Str → S`, ADT name `Foo →
/// FFoo`, fn → `F<params...>R<ret>` (no recursion guard since types in
/// the MVP are non-recursive at the type level).
fn type_descriptor(t: &Type) -> String {
    match t {
        Type::Con { name, args } => {
            let head = match name.as_str() {
                "Int" => "I".into(),
                "Bool" => "B".into(),
                "Unit" => "U".into(),
                "Str" => "S".into(),
                other => format!("F{other}"),
            };
            if args.is_empty() {
                head
            } else {
                // Iter 13a: parameterised ADTs get their type-arg
                // descriptors appended, e.g. `FBox` of `Int` → `FBox_I`.
                let mut s = head;
                for a in args {
                    s.push('_');
                    s.push_str(&type_descriptor(a));
                }
                s
            }
        }
        Type::Fn { params, ret, .. } => {
            let mut s = String::from("Fn");
            for p in params {
                s.push('_');
                s.push_str(&type_descriptor(p));
            }
            s.push_str("__r_");
            s.push_str(&type_descriptor(ret));
            s
        }
        Type::Var { name } => format!("V{name}"),
        Type::Forall { .. } => "FORALL".into(),
    }
}

fn builtin_binop(name: &str) -> Option<(&'static str, &'static str)> {
    Some(match name {
        "+" => ("add", "i64"),
        "-" => ("sub", "i64"),
        "*" => ("mul", "i64"),
        "/" => ("sdiv", "i64"),
        "%" => ("srem", "i64"),
        "==" => ("icmp eq", "i1"),
        "!=" => ("icmp ne", "i1"),
        "<" => ("icmp slt", "i1"),
        "<=" => ("icmp sle", "i1"),
        ">" => ("icmp sgt", "i1"),
        ">=" => ("icmp sge", "i1"),
        _ => return None,
    })
}

fn c_byte_len(s: &str) -> usize {
    s.len() + 1 // + NUL terminator
}

/// Escapes a string for LLVM IR `c"..."`. All bytes outside
/// 0x20..0x7E are escaped as `\HH`; `"` and `\` likewise. Ends with `\00`.
fn default_triple() -> &'static str {
    // In the MVP we query the compile host. For cross-compilation this
    // would need to be configurable — not needed now.
    if cfg!(target_os = "linux") && cfg!(target_arch = "x86_64") {
        "x86_64-pc-linux-gnu"
    } else if cfg!(target_os = "macos") && cfg!(target_arch = "aarch64") {
        "arm64-apple-darwin"
    } else if cfg!(target_os = "macos") && cfg!(target_arch = "x86_64") {
        "x86_64-apple-darwin"
    } else if cfg!(target_arch = "aarch64") {
        "aarch64-unknown-linux-gnu"
    } else {
        "x86_64-pc-linux-gnu"
    }
}

fn ll_string_literal(s: &str) -> String {
    let mut out = String::new();
    for &b in s.as_bytes() {
        match b {
            b'"' => out.push_str("\\22"),
            b'\\' => out.push_str("\\5C"),
            0x20..=0x7E => out.push(b as char),
            _ => out.push_str(&format!("\\{:02X}", b)),
        }
    }
    out.push_str("\\00");
    out
}

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

    #[test]
    fn emits_arith_fn() {
        // Single module becomes a trivial workspace via `emit_ir`; the
        // mangling is `@ail_<module>_<def>` even in the single-file case.
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Fn(FnDef {
                    name: "add".into(),
                    ty: Type::Fn {
                        params: vec![Type::int(), Type::int()],
                        ret: Box::new(Type::int()),
                        effects: vec![],
                    },
                    params: vec!["a".into(), "b".into()],
                    body: Term::App {
                        callee: Box::new(Term::Var { name: "+".into() }),
                        args: vec![
                            Term::Var { name: "a".into() },
                            Term::Var { name: "b".into() },
                        ],
                        tail: false,
                    },
                    doc: None,
                }),
                // Entry module needs a `main`, otherwise
                // `lower_workspace` returns `MissingEntryMain`.
                Def::Fn(FnDef {
                    name: "main".into(),
                    ty: Type::Fn {
                        params: vec![],
                        ret: Box::new(Type::unit()),
                        effects: vec![],
                    },
                    params: vec![],
                    body: Term::Lit { lit: Literal::Unit },
                    doc: None,
                }),
            ],
        };
        let ir = emit_ir(&m).unwrap();
        assert!(
            ir.contains("define i64 @ail_t_add(i64 %arg_a, i64 %arg_b)"),
            "ir was: {ir}"
        );
        assert!(ir.contains("add i64 %arg_a, %arg_b"));
        assert!(
            ir.contains("call i8 @ail_t_main()"),
            "trampoline call missing: {ir}"
        );
    }

    /// Iter 16e: codegen rejects `==` on ADT-typed args with a clear
    /// error. The typechecker accepts the call (the rigid var of
    /// `forall a. (a, a) -> Bool` unifies with the ADT type), so the
    /// rejection has to happen here. The diagnostic must mention the
    /// `==` symbol and the ADT type name.
    #[test]
    fn eq_on_adt_rejected_at_codegen() {
        // Tiny ADT `data K = Mk` (nullary).
        let mk = Term::Ctor {
            type_name: "K".into(),
            ctor: "Mk".into(),
            args: vec![],
        };
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "K".into(),
                    vars: vec![],
                    ctors: vec![Ctor {
                        name: "Mk".into(),
                        fields: vec![],
                    }],
                    doc: None,
                }),
                Def::Fn(FnDef {
                    name: "main".into(),
                    ty: Type::Fn {
                        params: vec![],
                        ret: Box::new(Type::unit()),
                        effects: vec![],
                    },
                    params: vec![],
                    body: Term::Let {
                        name: "_b".into(),
                        value: Box::new(Term::App {
                            callee: Box::new(Term::Var { name: "==".into() }),
                            args: vec![mk.clone(), mk],
                            tail: false,
                        }),
                        body: Box::new(Term::Lit { lit: Literal::Unit }),
                    },
                    doc: None,
                }),
            ],
        };
        let err = emit_ir(&m).expect_err(
            "`==` on ADT must be rejected at codegen; emit_ir succeeded",
        );
        let msg = format!("{err:?}");
        assert!(
            msg.contains("==") && msg.contains("not supported"),
            "expected error mentioning `==` not supported; got: {msg}"
        );
    }

    /// Iter 16e: same negative-path guard for function-typed args.
    /// `==` on `Fn` is rejected with a "not supported for function
    /// types" message.
    #[test]
    fn eq_on_fn_rejected_at_codegen() {
        // `let f = main in (== f f)` — `main` is in scope as a fn-value.
        let m = Module {
            schema: SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![Def::Fn(FnDef {
                name: "main".into(),
                ty: Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::unit()),
                    effects: vec![],
                },
                params: vec![],
                body: Term::Let {
                    name: "f".into(),
                    value: Box::new(Term::Var { name: "main".into() }),
                    body: Box::new(Term::Let {
                        name: "_b".into(),
                        value: Box::new(Term::App {
                            callee: Box::new(Term::Var { name: "==".into() }),
                            args: vec![
                                Term::Var { name: "f".into() },
                                Term::Var { name: "f".into() },
                            ],
                            tail: false,
                        }),
                        body: Box::new(Term::Lit { lit: Literal::Unit }),
                    }),
                },
                doc: None,
            })],
        };
        let err = emit_ir(&m).expect_err(
            "`==` on Fn must be rejected at codegen; emit_ir succeeded",
        );
        let msg = format!("{err:?}");
        assert!(
            msg.contains("==") && msg.contains("function"),
            "expected error mentioning `==` and function types; got: {msg}"
        );
    }

    #[test]
    fn missing_entry_main_is_error() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "noentry".into(),
            imports: vec![],
            defs: vec![Def::Fn(FnDef {
                name: "helper".into(),
                ty: Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::int()),
                    effects: vec![],
                },
                params: vec![],
                body: Term::Lit {
                    lit: Literal::Int { value: 1 },
                },
                doc: None,
            })],
        };
        let err = emit_ir(&m).unwrap_err();
        match err {
            CodegenError::MissingEntryMain(name) => assert_eq!(name, "noentry"),
            other => panic!("expected MissingEntryMain, got {other:?}"),
        }
    }
}