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

use ailang_check::uniqueness::{infer_module, UniquenessTable};

mod drop;
mod escape;
mod lambda;
mod match_lower;
mod subst;
mod synth;

use escape::NonEscapeSet;
use subst::{
    apply_subst_to_term, apply_subst_to_type, derive_substitution, descriptor_for_subst,
    qualify_local_types_codegen, unify_for_subst,
};
use synth::{
    builtin_ail_type, builtin_binop, builtin_effect_op_ret, c_byte_len, default_triple,
    fn_sig_from_type, ll_string_literal, llvm_type,
};

/// 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.
/// `Rc` (Iter 18b, Decision 10) routes allocation through
/// `@ailang_rc_alloc` from `runtime/rc.c`, which prefixes every payload
/// with an 8-byte refcount header. Iter 18b stops at allocator routing —
/// codegen does not yet emit `inc`/`dec` calls, so programs leak
/// every allocation under `Rc`. The actual instrumentation arrives in
/// Iter 18c once uniqueness inference is wired up.
/// The IR is otherwise byte-identical between the three strategies
/// modulo the allocator symbol name.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AllocStrategy {
    Gc,
    Bump,
    Rc,
}

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",
            AllocStrategy::Rc => "ailang_rc_alloc",
        }
    }
}

/// 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("."),
        // Iter 22b.1: emit_ir is the single-module shortcut. The
        // empty registry is fine for 22b.1 because codegen does not
        // yet read it; once 22b.3 monomorphisation runs, the queue
        // is built from class-method-call sites in already-typechecked
        // module bodies, not from the registry.
        registry: ailang_core::workspace::Registry::default(),
    };
    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(),
        // Iter 22b.1: pass the registry through unchanged. The desugar
        // pass does not touch class/instance defs (see desugar.rs:
        // 22b.1 passthrough), so the registry built at load time
        // remains valid against the desugared modules.
        registry: ws.registry.clone(),
    };
    let ws = &ws_owned;
    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 18c.3: under `--alloc=rc`, also declare the inc/dec ABI from
    // `runtime/rc.c` so codegen can emit refcount calls at every
    // `Term::Clone` site and at end-of-scope of trackable RC binders.
    // `Gc` and `Bump` keep their pre-18c IR shape — nothing to declare.
    if matches!(alloc, AllocStrategy::Rc) {
        out.push_str("declare void @ailang_rc_inc(ptr)\n");
        out.push_str("declare void @ailang_rc_dec(ptr)\n");
        // Iter 18e: drop-worklist ABI for `(drop-iterative)` types.
        // Declared unconditionally under `--alloc=rc` (the linker
        // drops symbols if no emitted fn references them); symmetric
        // with inc/dec above. See `runtime/rc.c` for the strategy.
        out.push_str("declare ptr @ailang_drop_worklist_new()\n");
        out.push_str("declare void @ailang_drop_worklist_push(ptr, ptr)\n");
        out.push_str("declare ptr @ailang_drop_worklist_pop(ptr)\n");
        out.push_str("declare void @ailang_drop_worklist_free(ptr)\n");
    }
    // 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,
    /// Iter 18c.3: per-binder uniqueness side-table for the current
    /// module, keyed by `(def_name, binder_name)`. Built once per
    /// emitter and consulted by `Term::Let` lowering to decide whether
    /// to emit `call void @ailang_rc_dec(ptr %v)` at scope close. The
    /// table is module-scoped because the inference is whole-fn local;
    /// no cross-module entries appear.
    uniqueness: UniquenessTable,
    /// Iter 18c.4: per-closure-pair drop-function symbol. Keyed by the
    /// closure-pair SSA value (e.g. `%v17`) the most-recent
    /// `lower_lambda` call returned. Consulted by the `Term::Let`
    /// lowering to emit `call void @<drop>(ptr %v17)` instead of the
    /// raw `@ailang_rc_dec` when the binder owns a closure pair.
    /// Empty under non-`Rc` allocators — a closure under
    /// `--alloc=gc`/`--alloc=bump` has no drop fn and is freed by
    /// the collector / arena.
    closure_drops: BTreeMap<String, String>,
    /// Iter 18d.3: per-fn-body move tracking. Keyed by binder name, maps
    /// to the set of positional ctor-field indices that have been
    /// "moved out" via a pattern destructure. A field is moved when a
    /// `(case (Ctor h t) <body>)` arm binds a non-wildcard, pointer-
    /// typed slot — the load-into-binder is treated as a transfer of
    /// ownership from the source slot to the binder's SSA. The source
    /// slot is NOT mutated; codegen merely remembers, statically, that
    /// the binder's new owner now holds the only live reference along
    /// this path.
    ///
    /// Consulted at two call sites that emit dec sequences against the
    /// source binder:
    ///   1. `Term::Let` scope close (`is_rc_heap_allocated` path) —
    ///      when the entry is non-empty, codegen inlines a per-field
    ///      dec sequence that skips slots in the moved set. When the
    ///      entry is empty (the common case), the existing
    ///      `drop_<m>_<T>(ptr)` call is emitted unchanged.
    ///   2. `lower_reuse_as_rc`'s reuse arm — moved-out slots are
    ///      skipped (they no longer hold a live reference); non-moved
    ///      slots are dec'd via `field_drop_call` before the new field
    ///      values overwrite them.
    ///
    /// Reset to empty at the top of every fn body (`emit_fn` and the
    /// thunk-emission section of `lower_lambda`). Entries for a
    /// particular binder are removed when that binder leaves scope
    /// (on `Term::Let` body close, on match-arm body close).
    moved_slots: BTreeMap<String, BTreeSet<usize>>,
    /// Iter 18d.4 fix: per-fn-body parameter modes, keyed by parameter
    /// name. Set once at the top of `emit_fn` (and at lambda thunk
    /// entry) from the fn type's `param_modes`. Consulted by
    /// `lower_match`'s arm-close pattern-binder dec emission (Iter A) to
    /// decide whether the scrutinee was statically owned: if the
    /// scrutinee resolves to a fn-param whose mode is `Borrow` or
    /// `Implicit`, the pattern-binder dec must NOT fire — the caller
    /// still holds a reference and dec'ing the pattern-binder would
    /// fragment the caller's structure.
    ///
    /// Symmetric with the Iter B gate at fn return (`emit_fn`'s Own-
    /// param dec): both sites must check the param-mode signal before
    /// dec'ing, because Implicit and Borrow do not carry the "caller
    /// handed off ownership" signal that makes the dec safe.
    current_param_modes: BTreeMap<String, ParamMode>,
}

#[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);
            }
        }

        // Iter 18c.3: build the per-module uniqueness side-table once
        // per emitter. The inference is pure (no I/O, no global state),
        // so doing it here is cheap and keeps codegen's input self-
        // contained.
        let uniqueness = infer_module(module);

        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,
            uniqueness,
            closure_drops: BTreeMap::new(),
            moved_slots: BTreeMap::new(),
            current_param_modes: BTreeMap::new(),
        }
    }

    pub(crate) 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).
                }
                // Iter 22b.1: class/instance defs do not emit IR yet.
                // 22b.3 monomorphisation will rewrite class-method
                // calls into calls against synthesised monomorphic
                // FnDefs; once that pass runs, class/instance bodies
                // never reach the emit path on their own — they only
                // appear inlined into the synthesised fns.
                Def::Class(_) | Def::Instance(_) => {}
            }
        }
        // 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),
                    )
                })?;
        }
        // Iter 18c.4: per-ADT drop functions. Emitted only under
        // `--alloc=rc`. One `void @drop_<module>_<TypeName>(ptr)` per
        // `Def::Type` in the current module — the call site for
        // recursive ADTs (`drop_<m>_List` calling itself on the tail)
        // requires every ADT to have a uniformly-named drop fn, so we
        // emit even for ADTs with no boxed children (those drop fns
        // just dec the outer box). Under `Gc`/`Bump` no drop fns
        // appear — the IR shape stays byte-identical to pre-18c.4.
        if matches!(self.alloc, AllocStrategy::Rc) {
            for def in &self.module.defs {
                if let Def::Type(td) = def {
                    if td.drop_iterative {
                        // Iter 18e: opt-in iterative-drop body. The
                        // recursive cascade overflows the C stack on
                        // long chains (a million-cell list ≈ 8MB
                        // stack); the iterative variant uses an
                        // explicit heap-allocated worklist instead.
                        self.emit_iterative_drop_fn_for_type(td);
                    } else {
                        self.emit_drop_fn_for_type(td);
                    }
                    // Iter 18g.tidy.fu2: tag-conditional partial-drop
                    // helper alongside the recursive/iterative drop fn.
                    // Used at carve-out sites where a binder's runtime
                    // tag is dynamic and `moved_slots` is a strict
                    // subset of its ptr fields. Same shape regardless
                    // of `(drop-iterative)` (the helper is single-shot
                    // on the binder; field cascades go through their
                    // own drop fns which themselves choose recursive
                    // vs iterative).
                    self.emit_partial_drop_fn_for_type(td);
                }
            }
        }
        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,
            suppress: vec![],
            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<()> {
        // Iter 18d.4: also lift `param_modes` out of the fn type. The
        // fn-return Own-param dec emission below consults it to decide
        // which params get a drop call before `ret`. `Implicit`
        // entries (legacy / unannotated) and `Borrow` entries are
        // skipped — only `Own` carries the static "caller handed off
        // ownership" signal.
        let (param_tys, ret_ty, param_modes) = match &f.ty {
            Type::Fn {
                params,
                ret,
                param_modes,
                ..
            } => (params.clone(), (**ret).clone(), param_modes.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 18d.3: move tracking is per-fn-body.
        self.moved_slots.clear();
        // Iter 18d.4 fix: param-mode lookup is per-fn-body. Built from
        // the fn type's `param_modes` (already destructured above) and
        // consulted by `lower_match`'s Iter A gate to skip arm-close
        // pattern-binder dec when the scrutinee is a non-Own param.
        self.current_param_modes.clear();
        for (i, pname) in f.params.iter().enumerate() {
            let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
            self.current_param_modes.insert(pname.clone(), mode);
        }
        // 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
                )));
            }
            // Iter 18d.4: fn-return Own-param dec. Symmetric to
            // 18c.3/18c.4's `Term::Let`-scope-close drop and 18d.4's
            // arm-close pattern-binder dec, fired at the lexical
            // close of a fn body. For each parameter with
            // `ParamMode::Own`, emit a drop call iff:
            //   - alloc strategy is `Rc`,
            //   - the parameter's lowered type is `ptr`,
            //   - uniqueness inference recorded `consume_count == 0`
            //     for the param in this fn's body (no internal use
            //     consumed it; the param's slot owns the only ref the
            //     callee received from the caller's hand-off),
            //   - the param's SSA is not the body's tail value
            //     (returning the param transfers ownership back to
            //     the caller's frame; caller dec's, not us),
            //   - the current block is still open.
            //
            // `Implicit`-mode params do NOT get this dec: they have
            // no static "caller handed off ownership" signal —
            // emitting a dec here might double-dec a value the caller
            // also dec's. `Borrow`-mode params definitely don't get
            // dec'd (the caller still owns them).
            //
            // Closes the 18c.3/18c.4 carve-out: "fn parameters still
            // don't get dec'd at fn return — the caller-handed-off-
            // ownership signal is the `(own T)` mode, but wiring it
            // through codegen is part of the wider mode-aware story."
            if matches!(self.alloc, AllocStrategy::Rc) {
                for (i, ((pname, plty), pty_ail)) in f
                    .params
                    .iter()
                    .zip(llvm_param_tys.iter())
                    .zip(param_tys.iter())
                    .enumerate()
                {
                    if plty != "ptr" {
                        continue;
                    }
                    let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
                    if !matches!(mode, ParamMode::Own) {
                        continue;
                    }
                    let consume_count = self
                        .uniqueness
                        .get(&(self.current_def.clone(), pname.clone()))
                        .map(|info| info.consume_count)
                        .unwrap_or(u32::MAX);
                    if consume_count != 0 {
                        continue;
                    }
                    let p_ssa = format!("%arg_{}", pname);
                    if val == p_ssa {
                        // The param IS the fn's return value —
                        // ownership transfers back to the caller.
                        continue;
                    }
                    let moves = self
                        .moved_slots
                        .get(pname)
                        .cloned()
                        .unwrap_or_default();
                    if moves.is_empty() {
                        // Route through the per-type drop fn for the
                        // param's static type. `field_drop_call`
                        // resolves `Type::Con` to `drop_<owner>_<T>`
                        // and falls back to `ailang_rc_dec` for
                        // closure / Var fields — closure-typed Own
                        // params therefore use the same shallow free
                        // 18c.4 set up for closure-typed ADT fields,
                        // matching the iter brief's "closure-typed
                        // Own params follow whichever debt path
                        // 18c.4 set up" carve-out.
                        let drop_call = self.field_drop_call(pty_ail);
                        self.body.push_str(&format!(
                            "  call void @{drop_call}(ptr {p_ssa})\n"
                        ));
                    } else {
                        // Iter 18g.tidy.fu2: dynamic-tag partial-drop
                        // via the per-type helper. The param's runtime
                        // tag is dynamic but its static type is known
                        // (`pty_ail`), so we route through
                        // `partial_drop_<owner>_<T>(p, mask)` which
                        // dispatches on the runtime tag and dec's only
                        // the unmoved fields. The fallback to shallow
                        // `ailang_rc_dec` only fires for non-ADT param
                        // types (Str, fn-typed, vars) — none of which
                        // can populate `moved_slots` in practice, so
                        // the fallback is dead under the typechecker.
                        let sym = Self::partial_drop_symbol_for_type(
                            self, pty_ail,
                        );
                        let mask = Self::build_moved_mask(&moves);
                        if let (Some(sym), Some(mask)) = (sym, mask) {
                            self.body.push_str(&format!(
                                "  call void @{sym}(ptr {p_ssa}, i64 {mask})\n"
                            ));
                        } else {
                            self.body.push_str(&format!(
                                "  call void @ailang_rc_dec(ptr {p_ssa})\n"
                            ));
                        }
                    }
                }
            }
            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).
    pub(crate) 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 } => {
                // Iter 18c.3: decide whether this let-binder is
                // trackable for `dec` emission BEFORE lowering. The
                // value term must lower through `ailang_rc_alloc` —
                // that means `Term::Ctor` / `Term::Lam` whose escape
                // analysis says "heap" (not `alloca`) under
                // `--alloc=rc`. Other value shapes (calls, vars,
                // literals) lower to SSAs we don't statically own at
                // this scope.
                let trackable = self.is_rc_heap_allocated(value);

                let val_ail = self.synth_arg_type(value)?;
                let (val_ssa, val_ty) = self.lower_term(value)?;
                self.locals
                    .push((name.clone(), val_ssa.clone(), val_ty.clone(), val_ail));
                // Iter 18g.tidy.fu: let-alias-aware mode propagation.
                // If `value` is a `Term::Var` referencing a name in
                // `current_param_modes`, the let-binder inherits that
                // mode for the duration of the body. Without this,
                // `(let a t (match a ...))` where `t` is an Implicit
                // / Borrow-mode param defeats the
                // `scrutinee_is_owned` gate in `lower_match` (the
                // gate looks up `a` in `current_param_modes`, misses,
                // and defaults to "owned" — Iter A then dec's
                // pattern-binders whose underlying memory belongs to
                // the caller).
                //
                // Restored on let-body-close (push/pop pattern).
                let inherited_mode: Option<ParamMode> = match value.as_ref() {
                    Term::Var { name: src } => {
                        self.current_param_modes.get(src).copied()
                    }
                    _ => None,
                };
                let prior_mode = if let Some(m) = inherited_mode {
                    let prior = self.current_param_modes.insert(name.clone(), m);
                    Some(prior)
                } else {
                    None
                };
                let r = self.lower_term(body);
                if let Some(prior) = prior_mode {
                    match prior {
                        Some(m) => {
                            self.current_param_modes.insert(name.clone(), m);
                        }
                        None => {
                            self.current_param_modes.remove(name);
                        }
                    }
                }
                self.locals.pop();
                // Iter 18d.3: lift the binder's move set out of the
                // side table. The binder is leaving scope here; we
                // remove the entry whether or not we end up using it
                // for the dec emission below. `take` returns a
                // by-value `BTreeSet<usize>` (or empty) so we can
                // both consult and clear in one move.
                let moves_for_binder: BTreeSet<usize> =
                    self.moved_slots.remove(name).unwrap_or_default();

                // Iter 18c.3: emit a drop call at scope close iff:
                //  - we're tracking this binder (heap RC alloc above),
                //  - the value type is `ptr` (not a primitive),
                //  - uniqueness inference recorded `consume_count == 0`
                //    for the binder (no callee / outer term has already
                //    taken ownership; the binder owns the only ref),
                //  - the body's tail value is NOT the binder itself
                //    (a binder that flows out as the result transfers
                //    ownership to the caller — caller dec's), and
                //  - the current block is still open (a tail-call /
                //    `unreachable` already exited; nothing to emit).
                //
                // Iter 18c.4: the drop call is no longer a raw
                // `ailang_rc_dec`. For a `Term::Ctor` binder the call
                // routes through `@drop_<owner>_<TypeName>` so any
                // boxed children of the cell cascade through their
                // own drop fns; for a `Term::Lam` binder the call
                // routes through the per-pair drop fn the lambda
                // emission recorded in `closure_drops`. Both shapes
                // call `ailang_rc_dec` on the outer box internally,
                // so the refcount story is unchanged.
                if trackable && val_ty == "ptr" && !self.block_terminated {
                    let consume_count = self
                        .uniqueness
                        .get(&(self.current_def.clone(), name.clone()))
                        .map(|info| info.consume_count)
                        .unwrap_or(u32::MAX); // Defensive: skip if missing.
                    let body_returns_binder = match &r {
                        Ok((body_ssa, _)) => body_ssa == &val_ssa,
                        Err(_) => true, // Don't emit on error path either.
                    };
                    if consume_count == 0 && !body_returns_binder {
                        // Iter 18d.3: when the binder has moved-out
                        // pattern slots, the uniform `drop_<m>_<T>`
                        // would re-dec values that have already been
                        // transferred to other binders. Inline a
                        // per-field dec sequence that skips moved
                        // slots; non-moved pointer slots dec via
                        // `field_drop_call` (null-guarded drop fns
                        // matching the recursive cascade in
                        // `emit_drop_fn_for_type`). For the empty-
                        // moves common case (every fixture pre-18d.3
                        // and most fixtures post-18d.3) we emit the
                        // identical `drop_<m>_<T>(ptr)` call as
                        // 18c.4, preserving IR shape.
                        if !moves_for_binder.is_empty() {
                            self.emit_inlined_partial_drop(
                                value,
                                &val_ssa,
                                &moves_for_binder,
                            )?;
                        } else {
                            let drop_sym = self.drop_symbol_for_binder(value, &val_ssa);
                            self.body.push_str(&format!(
                                "  call void @{drop_sym}(ptr {val_ssa})\n"
                            ));
                        }
                    }
                }

                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")
            }
            Term::Clone { value } => {
                // Iter 18c.3: lower the inner value, then emit
                // `call void @ailang_rc_inc(ptr %v)` under `--alloc=rc`.
                // Inc is skipped for non-`ptr` values (primitives like
                // `i64` carry no refcount) and for `@`-prefixed SSAs
                // (top-level fn closure-pair globals live in the LLVM
                // data segment, not heap memory — `runtime/rc.c`'s
                // header layout doesn't apply to them). Codegen elision
                // here matches `runtime/rc.c`'s comment about static
                // pointers.
                let (val_ssa, val_ty) = self.lower_term(value)?;
                if matches!(self.alloc, AllocStrategy::Rc)
                    && val_ty == "ptr"
                    && !val_ssa.starts_with('@')
                    && !self.block_terminated
                {
                    self.body.push_str(&format!(
                        "  call void @ailang_rc_inc(ptr {val_ssa})\n"
                    ));
                }
                Ok((val_ssa, val_ty))
            }
            Term::ReuseAs { source, body } => {
                // Iter 18d.2: under --alloc=rc, lower as a runtime-
                // refcount-1 dispatch — if the source's box is
                // unique we overwrite it in place (skipping the
                // alloc-and-cascade-dec round-trip); otherwise we
                // allocate a fresh box and dec the source. Other
                // allocators keep the 18d.1 identity behaviour.
                if !matches!(self.alloc, AllocStrategy::Rc) {
                    return self.lower_term(body);
                }
                // The body must be a Term::Ctor for the in-place
                // rewrite to make sense. 18d.1 typecheck rejects
                // any other shape; lams are accepted by typecheck
                // but not yet supported by reuse codegen — fall
                // back to identity for those (the body still
                // allocates via ailang_rc_alloc, just without the
                // reuse fast path).
                let (body_type_name, body_ctor, body_args) = match body.as_ref() {
                    Term::Ctor { type_name, ctor, args } => (type_name, ctor, args),
                    _ => return self.lower_term(body),
                };
                self.lower_reuse_as_rc(source, body_type_name, body_ctor, body_args)
            }
        }
    }

    /// 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.
    pub(crate) 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.
    pub(crate) 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`).
    pub(crate) 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}`"
        )))
    }

    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, constraints: _, 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 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)
            ))),
        }
    }

    pub(crate) fn fresh_ssa(&mut self) -> String {
        self.counter += 1;
        format!("%v{}", self.counter)
    }
    pub(crate) 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`.
    pub(crate) 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(),
                param_modes: vec![],
                ret_mode: ParamMode::Implicit,
            }),
            Term::App { callee, args, .. } => {
                let cty = self.synth_with_extras(callee, extras)?;
                match cty {
                    Type::Fn { ret, .. } => Ok(*ret),
                    Type::Forall { vars, constraints: _, 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")
            }
            Term::Clone { value } => {
                // Iter 18c.1: clone is identity — same type as inner.
                self.synth_with_extras(value, extras)
            }
            Term::ReuseAs { body, .. } => {
                // Iter 18d.1: identity — the result type is the body's
                // type. The source is dropped at codegen.
                self.synth_with_extras(body, extras)
            }
        }
    }
}

#[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![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    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,
                    },
                    suppress: vec![],
                    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![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    params: vec![],
                    body: Term::Lit { lit: Literal::Unit },
                    suppress: vec![],
                    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,
                    drop_iterative: false,
                }),
                Def::Fn(FnDef {
                    name: "main".into(),
                    ty: Type::Fn {
                        params: vec![],
                        ret: Box::new(Type::unit()),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    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 }),
                    },
                    suppress: vec![],
                    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![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                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 }),
                    }),
                },
                suppress: vec![],
                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![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                params: vec![],
                body: Term::Lit {
                    lit: Literal::Int { value: 1 },
                },
                suppress: vec![],
                doc: None,
            })],
        };
        let err = emit_ir(&m).unwrap_err();
        match err {
            CodegenError::MissingEntryMain(name) => assert_eq!(name, "noentry"),
            other => panic!("expected MissingEntryMain, got {other:?}"),
        }
    }

    /// Iter 18c.4: under `--alloc=rc`, codegen emits one
    /// `define void @drop_<m>_<T>` per `Def::Type`. For a recursive
    /// ADT — a `IntList` with `Cons(Int, IntList)` — the `Cons` arm
    /// of the drop fn loads the tail field and calls the ADT's own
    /// drop fn on it (the recursion 18e replaces with an iterative
    /// worklist). We assert both shapes here:
    ///
    ///   1. `define void @drop_<m>_IntList(ptr %p)` is present.
    ///   2. The fn's body contains a self-recursive call
    ///      `call void @drop_<m>_IntList(ptr %v...)` — proof that
    ///      the `Cons` arm walked the tail field rather than just
    ///      decrementing the outer cell.
    ///
    /// The `Nil` arm has no boxed children and is a `br` to the
    /// shared `join` block — implicit in (1).
    ///
    /// Negative complement: under `--alloc=gc` no drop fn is
    /// emitted; the IR shape stays byte-identical to the pre-18c.4
    /// pipeline.
    #[test]
    fn rc_alloc_emits_recursive_drop_fn_for_recursive_adt() {
        let m = Module {
            schema: SCHEMA.into(),
            name: "rclist".into(),
            imports: vec![],
            defs: vec![
                Def::Type(TypeDef {
                    name: "IntList".into(),
                    vars: vec![],
                    ctors: vec![
                        Ctor {
                            name: "Nil".into(),
                            fields: vec![],
                        },
                        Ctor {
                            name: "Cons".into(),
                            fields: vec![
                                Type::int(),
                                Type::Con {
                                    name: "IntList".into(),
                                    args: vec![],
                                },
                            ],
                        },
                    ],
                    doc: None,
                    drop_iterative: false,
                }),
                Def::Fn(FnDef {
                    name: "main".into(),
                    ty: Type::Fn {
                        params: vec![],
                        ret: Box::new(Type::unit()),
                        effects: vec![],
                        param_modes: vec![],
                        ret_mode: ParamMode::Implicit,
                    },
                    params: vec![],
                    body: Term::Lit { lit: Literal::Unit },
                    suppress: vec![],
                    doc: None,
                }),
            ],
        };
        let ws = Workspace {
            entry: m.name.clone(),
            modules: {
                let mut x = BTreeMap::new();
                x.insert(m.name.clone(), m.clone());
                x
            },
            root_dir: std::path::PathBuf::from("."),
            registry: ailang_core::workspace::Registry::default(),
        };
        let ir_rc = lower_workspace_with_alloc(&ws, AllocStrategy::Rc).unwrap();
        assert!(
            ir_rc.contains("define void @drop_rclist_IntList(ptr %p)"),
            "rc IR missing per-type drop fn header. IR was:\n{ir_rc}"
        );
        // The Cons arm loads the tail field and recurses through
        // the same drop symbol — proof that the cascade is wired.
        assert!(
            ir_rc.contains("call void @drop_rclist_IntList(ptr %v"),
            "rc IR missing recursive drop call inside drop_rclist_IntList. IR was:\n{ir_rc}"
        );
        // The drop fn finishes by dec'ing the outer box.
        assert!(
            ir_rc.contains("call void @ailang_rc_dec(ptr %p)"),
            "rc IR missing outer-box dec inside drop_rclist_IntList. IR was:\n{ir_rc}"
        );

        // Negative complement: no drop fns under `--alloc=gc`.
        let ir_gc = lower_workspace_with_alloc(&ws, AllocStrategy::Gc).unwrap();
        assert!(
            !ir_gc.contains("@drop_rclist_IntList"),
            "gc IR should not declare/define any per-type drop fn. IR was:\n{ir_gc}"
        );
    }
}