//! Iter 16b.3: post-typecheck `Term::LetRec` lift.
//!
//! Background. The 16a desugar pass (`ailang-core::desugar::desugar_module`)
//! eliminates most `Term::LetRec` nodes by lifting them to synthetic
//! top-level fns. That works as long as every captured name has a
//! statically-known type at desugar time — fn-params and Lam-params
//! qualify (16b.2). When a capture is bound by a `Term::Let`, the
//! let-value's type is inferred at typecheck and the desugar pass
//! cannot resolve it. In that case the desugar pass leaves the
//! `Term::LetRec` in place; this module's [`lift_letrecs`] picks them
//! up afterwards and lifts them using the typechecker's resolved
//! types.
//!
//! Pipeline placement. After [`crate::check`] succeeds. The lifter
//! produces a new `Module` whose `defs` may have additional synthetic
//! `Def::Fn` entries appended. The module's existing top-level defs
//! are NOT renamed; only the `body` of each `Def::Fn` (and the
//! `value` of each `Def::Const`, defensively) is rewritten.
//!
//! Symbol-hashing invariant. Synthetic FnDefs added by `lift_letrecs`
//! must NOT appear in `CheckedModule.symbols` — that table is built
//! from the original on-disk module, preserving the canonical-bytes
//! identity that `ail diff` and `ail manifest` rely on. The 16b.2
//! lift in desugar already follows the same convention. Concretely:
//! `check` keeps building symbols as today (from the input module);
//! `lift_letrecs` runs separately and returns the possibly-larger
//! module that goes to codegen.

use ailang_core::ast::*;
use ailang_core::desugar::{
    find_non_callee_use, free_vars_in_term, subst_call_with_extras, subst_var,
};
use indexmap::IndexMap;
use std::collections::{BTreeMap, BTreeSet};

use crate::{builtins, synth, CheckError, Env, Result, Subst};

/// Iter 16b.3: post-typecheck pass that eliminates every surviving
/// `Term::LetRec` from `m` by lifting it to a synthetic top-level
/// `Def::Fn`. Returns a new module that goes to codegen.
///
/// Pre-condition: `m` has been typechecked (i.e. `check(m)` returned
/// `Ok`). The lifter calls `synth` to resolve capture types, but
/// only on sub-terms that were already typechecked successfully — it
/// does not perform new type checking, only type queries.
///
/// The synthetic FnDefs are appended to `Module.defs` after every
/// pre-existing def. Their names follow the `<hint>$lr_N` convention
/// from 16b.2; the lifter's counter starts past the highest `*$lr_N`
/// suffix already present in `m.defs` to avoid collisions with
/// 16b.2's lifts.
pub fn lift_letrecs(m: &Module) -> Result<Module> {
    // Fast path: if the module contains no `Term::LetRec`, the lift
    // pass has nothing to do. Returning the input module verbatim
    // also means we don't build an env or run any sub-term type
    // synthesis — important because cross-module references in
    // typical fixtures would fail to resolve under the
    // single-module env we build below (a deliberate scope choice:
    // `lift_letrecs` is per-module, but cross-module info would only
    // ever be needed if a deferred LetRec were present).
    if !contains_any_letrec(m) {
        return Ok(m.clone());
    }

    // Build the full env once (matches `check_in_workspace`'s setup),
    // so we can re-synthesize sub-terms during the walk.
    //
    // `lift_letrecs` is a single-module pass; cross-module info isn't
    // needed because the LetRec capture set comes from the *enclosing*
    // fn's locals (which are always local to this module). Capture
    // types may mention foreign type-cons (e.g. `std_list.List Int`),
    // but those flow through verbatim — the lifter never needs to
    // resolve them.
    let mut env = Env::new();
    builtins::install(&mut env);

    // Type defs of this module.
    for def in &m.defs {
        if let Def::Type(td) = def {
            for c in &td.ctors {
                env.ctor_index.insert(
                    c.name.clone(),
                    crate::CtorRef {
                        type_name: td.name.clone(),
                    },
                );
            }
            env.types.insert(td.name.clone(), td.clone());
        }
    }

    // Top-level globals (fn / const types, including any 16b.2-lifted
    // synthetic fns that already live in the desugared module).
    for def in &m.defs {
        let ty = match def {
            Def::Fn(f) => f.ty.clone(),
            Def::Const(c) => c.ty.clone(),
            Def::Type(_) => Type::Con {
                name: def.name().to_string(),
                args: vec![],
            },
            // Iter 22b.1: skip class/instance defs in the global-type
            // collection. Class methods become globally typed names
            // only after 22b.3 monomorphisation; until then there is
            // no concrete `Type` to register here.
            Def::Class(_) | Def::Instance(_) => continue,
        };
        env.globals.insert(def.name().to_string(), ty);
    }

    // Imports (used by qualified-ref synth, even though LetRec captures
    // resolve through `locals`).
    let mut import_map: BTreeMap<String, String> = BTreeMap::new();
    for imp in &m.imports {
        let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
        import_map.insert(key, imp.module.clone());
    }
    env.imports = import_map;
    env.current_module = m.name.clone();

    // Counter init: scan existing def names for the highest `*$lr_N`
    // suffix so a new lift never collides with a 16b.2 lift.
    let mut counter: u64 = highest_lr_suffix(&m.defs).map(|n| n + 1).unwrap_or(0);

    // Pre-collect every existing top-level name so freshly-generated
    // names cannot shadow them.
    let mut module_names: BTreeSet<String> = BTreeSet::new();
    for def in &m.defs {
        module_names.insert(def.name().to_string());
    }

    // The walk.
    let mut lifter = Lifter {
        env,
        counter,
        module_names: &mut module_names,
        lifted: Vec::new(),
        current_def_forall_vars: Vec::new(),
        enclosing_letrec_names: BTreeSet::new(),
    };
    let _ = &mut counter; // counter lives in lifter from here on

    let mut out = m.clone();
    for def in &mut out.defs {
        match def {
            Def::Fn(f) => {
                // Build the locals scope for this fn (params with
                // their declared types, peeling Forall like check_fn
                // does).
                let inner_ty = match &f.ty {
                    Type::Forall { body, .. } => (**body).clone(),
                    other => other.clone(),
                };
                let mut locals: IndexMap<String, Type> = IndexMap::new();
                if let Type::Fn { params: ptys, .. } = &inner_ty {
                    if ptys.len() == f.params.len() {
                        for (n, t) in f.params.iter().zip(ptys.iter()) {
                            locals.insert(n.clone(), t.clone());
                        }
                    }
                }
                // Iter 13a: install rigid vars from a Forall enclosing
                // fn so check_type_well_formed inside synth doesn't
                // reject them. Save and restore so the lifter env is
                // clean across defs.
                let mut rigids_added: Vec<String> = Vec::new();
                if let Type::Forall { vars, .. } = &f.ty {
                    for v in vars {
                        if lifter.env.rigid_vars.insert(v.clone()) {
                            rigids_added.push(v.clone());
                        }
                    }
                }
                // Iter 16b.6: stash the enclosing fn's Forall.vars (or
                // empty for a monomorphic enclosing fn) for the LetRec
                // arm. Save and restore so it never leaks across defs.
                let saved_forall_vars =
                    std::mem::take(&mut lifter.current_def_forall_vars);
                lifter.current_def_forall_vars = match &f.ty {
                    Type::Forall { vars, .. } => vars.clone(),
                    _ => Vec::new(),
                };
                f.body = lifter.lift_in_term(&f.body, &mut locals, &f.name)?;
                lifter.current_def_forall_vars = saved_forall_vars;
                for v in rigids_added {
                    lifter.env.rigid_vars.remove(&v);
                }
            }
            Def::Const(c) => {
                let mut locals: IndexMap<String, Type> = IndexMap::new();
                c.value = lifter.lift_in_term(&c.value, &mut locals, &c.name)?;
            }
            Def::Type(_) => {}
            // Iter 22b.1: class/instance defs do not enter the lift
            // pass yet. 22b.2 will lift method-body lambdas in instance
            // methods; for 22b.1 this is a passthrough.
            Def::Class(_) | Def::Instance(_) => {}
        }
    }

    out.defs.extend(lifter.lifted.into_iter());
    Ok(out)
}

/// State for a single-module lift pass. Mirrors `Desugarer` in
/// `ailang-core::desugar` but resolves capture types via `synth`
/// instead of relying on a `ScopeEntry` map.
///
/// Iter 16b.6 field:
/// - `current_def_forall_vars` carries the enclosing fn's
///   `Type::Forall.vars` while lifting its body. Empty for monomorphic
///   enclosing fns. Read by the LetRec arm to wrap the synthetic
///   lifted fn's signature in `Type::Forall` mirroring the enclosing
///   fn — the lifted fn enters codegen's monomorphisation queue at
///   every call site, specialising at the same type args as its host.
struct Lifter<'a> {
    env: Env,
    counter: u64,
    module_names: &'a mut BTreeSet<String>,
    lifted: Vec<Def>,
    /// Iter 16b.6: enclosing fn's Forall.vars (or empty if mono).
    /// Reset on entry to each `Def::Fn`.
    current_def_forall_vars: Vec<String>,
    /// Iter 16b.7: names of LetRecs whose bodies are currently being
    /// lifted (i.e. enclosing `Term::LetRec` names visible at this
    /// point in the walk). Mirrors the desugar pass's
    /// `ScopeEntry::EnclosingLetRec` marker. An inner LetRec capturing
    /// any of these names is rejected — same chicken-and-egg as
    /// 16b.5-body / closure-of-self.
    enclosing_letrec_names: BTreeSet<String>,
}

impl<'a> Lifter<'a> {
    /// Walk `t`, lifting any `Term::LetRec` that survived desugar.
    /// Maintains `locals` parallel to the term's lexical scope so we
    /// can resolve capture types via `synth`.
    fn lift_in_term(
        &mut self,
        t: &Term,
        locals: &mut IndexMap<String, Type>,
        in_def: &str,
    ) -> Result<Term> {
        match t {
            Term::Lit { .. } | Term::Var { .. } => Ok(t.clone()),
            Term::App { callee, args, tail } => {
                let new_callee = self.lift_in_term(callee, locals, in_def)?;
                let mut new_args = Vec::with_capacity(args.len());
                for a in args {
                    new_args.push(self.lift_in_term(a, locals, in_def)?);
                }
                Ok(Term::App {
                    callee: Box::new(new_callee),
                    args: new_args,
                    tail: *tail,
                })
            }
            Term::Let { name, value, body } => {
                let v = self.lift_in_term(value, locals, in_def)?;
                // Synth the value's type (after lifting any nested
                // LetRecs inside it), so the body's lift sees a
                // resolved type for `name`.
                let v_ty = self.synth_type(&v, locals, in_def)?;
                let prev = locals.insert(name.clone(), v_ty);
                let b = self.lift_in_term(body, locals, in_def)?;
                match prev {
                    Some(p) => {
                        locals.insert(name.clone(), p);
                    }
                    None => {
                        locals.shift_remove(name);
                    }
                }
                Ok(Term::Let {
                    name: name.clone(),
                    value: Box::new(v),
                    body: Box::new(b),
                })
            }
            Term::If { cond, then, else_ } => Ok(Term::If {
                cond: Box::new(self.lift_in_term(cond, locals, in_def)?),
                then: Box::new(self.lift_in_term(then, locals, in_def)?),
                else_: Box::new(self.lift_in_term(else_, locals, in_def)?),
            }),
            Term::Do { op, args, tail } => {
                let mut new_args = Vec::with_capacity(args.len());
                for a in args {
                    new_args.push(self.lift_in_term(a, locals, in_def)?);
                }
                Ok(Term::Do {
                    op: op.clone(),
                    args: new_args,
                    tail: *tail,
                })
            }
            Term::Ctor { type_name, ctor, args } => {
                let mut new_args = Vec::with_capacity(args.len());
                for a in args {
                    new_args.push(self.lift_in_term(a, locals, in_def)?);
                }
                Ok(Term::Ctor {
                    type_name: type_name.clone(),
                    ctor: ctor.clone(),
                    args: new_args,
                })
            }
            Term::Match { scrutinee, arms } => {
                let s = self.lift_in_term(scrutinee, locals, in_def)?;
                // Synthesize the scrutinee's type so we can resolve
                // pattern-arm bindings to typed locals.
                let s_ty = self.synth_type(&s, locals, in_def)?;
                let mut new_arms = Vec::with_capacity(arms.len());
                for arm in arms {
                    let bindings = type_check_pattern_for_lift(&arm.pat, &s_ty, &self.env)?;
                    let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
                    for (n, t) in &bindings {
                        let prev = locals.insert(n.clone(), t.clone());
                        pushed.push((n.clone(), prev));
                    }
                    let body = self.lift_in_term(&arm.body, locals, in_def)?;
                    for (n, prev) in pushed.into_iter().rev() {
                        match prev {
                            Some(p) => {
                                locals.insert(n, p);
                            }
                            None => {
                                locals.shift_remove(&n);
                            }
                        }
                    }
                    new_arms.push(Arm {
                        pat: arm.pat.clone(),
                        body,
                    });
                }
                Ok(Term::Match {
                    scrutinee: Box::new(s),
                    arms: new_arms,
                })
            }
            Term::Lam { params, param_tys, ret_ty, effects, body } => {
                let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
                for (n, t) in params.iter().zip(param_tys.iter()) {
                    let prev = locals.insert(n.clone(), t.clone());
                    pushed.push((n.clone(), prev));
                }
                let new_body = self.lift_in_term(body, locals, in_def)?;
                for (n, prev) in pushed.into_iter().rev() {
                    match prev {
                        Some(p) => {
                            locals.insert(n, p);
                        }
                        None => {
                            locals.shift_remove(&n);
                        }
                    }
                }
                Ok(Term::Lam {
                    params: params.clone(),
                    param_tys: param_tys.clone(),
                    ret_ty: ret_ty.clone(),
                    effects: effects.clone(),
                    body: Box::new(new_body),
                })
            }
            Term::Seq { lhs, rhs } => Ok(Term::Seq {
                lhs: Box::new(self.lift_in_term(lhs, locals, in_def)?),
                rhs: Box::new(self.lift_in_term(rhs, locals, in_def)?),
            }),
            Term::Clone { value } => Ok(Term::Clone {
                // Iter 18c.1: structural recursion through the wrapper.
                value: Box::new(self.lift_in_term(value, locals, in_def)?),
            }),
            Term::ReuseAs { source, body } => Ok(Term::ReuseAs {
                // Iter 18d.1: structural recursion through both children.
                source: Box::new(self.lift_in_term(source, locals, in_def)?),
                body: Box::new(self.lift_in_term(body, locals, in_def)?),
            }),
            Term::LetRec { name, ty, params, body, in_term } => {
                // Iter 16b.3: post-order traversal — lift any inner
                // LetRecs first. Within the body's scope, `name` and
                // `params` are visible.
                //
                // Body-scope locals: name + params with their declared
                // types (peeled from `ty` if Forall).
                let inner_ty = match ty {
                    Type::Forall { body, .. } => (**body).clone(),
                    other => other.clone(),
                };
                let param_tys: Vec<Type> = match &inner_ty {
                    Type::Fn { params: ps, .. } => ps.clone(),
                    _ => {
                        return Err(CheckError::FnTypeRequired(
                            name.clone(),
                            ailang_core::pretty::type_to_string(&inner_ty),
                        ));
                    }
                };

                let mut body_pushed: Vec<(String, Option<Type>)> = Vec::new();
                let prev_name = locals.insert(name.clone(), ty.clone());
                body_pushed.push((name.clone(), prev_name));
                for (n, t) in params.iter().zip(param_tys.iter()) {
                    let prev = locals.insert(n.clone(), t.clone());
                    body_pushed.push((n.clone(), prev));
                }
                // Iter 16b.7: mark `name` as an enclosing LetRec while
                // lifting its body, so any inner LetRec that captures
                // `name` panics with the closure-of-self message rather
                // than silently lifting with `name` as a fn-typed extra
                // param (which would mis-compile when `name` itself has
                // its own captures).
                let name_was_marked = self.enclosing_letrec_names.insert(name.clone());
                let lifted_body = self.lift_in_term(body, locals, in_def)?;
                if name_was_marked {
                    self.enclosing_letrec_names.remove(name);
                }
                for (n, prev) in body_pushed.into_iter().rev() {
                    match prev {
                        Some(p) => {
                            locals.insert(n, p);
                        }
                        None => {
                            locals.shift_remove(&n);
                        }
                    }
                }

                // In-clause scope: only `name` is visible.
                let prev_in = locals.insert(name.clone(), ty.clone());
                let lifted_in = self.lift_in_term(in_term, locals, in_def)?;
                match prev_in {
                    Some(p) => {
                        locals.insert(name.clone(), p);
                    }
                    None => {
                        locals.shift_remove(name);
                    }
                }

                // 16b.5: name-as-value INSIDE the body remains rejected
                // (would require an eta-Lam that calls the unlifted name —
                // chicken-and-egg with the call-site rewrite).
                if find_non_callee_use(&lifted_body, name).is_some() {
                    panic!(
                        "Iter 16b.5: LetRec `{name}` appears as a value INSIDE its own \
                         body; name-as-value of a LetRec inside its own body is not yet \
                         supported."
                    );
                }
                // 16b.5: name-as-value in in_term IS supported. The wrap
                // is built below after we know `lifted_name` and `extras`.
                let in_has_value_use = find_non_callee_use(&lifted_in, name).is_some();

                // Iter 16b.6: reject name-as-value in `in_term` when the
                // enclosing fn is polymorphic — the eta-Lam wrap would
                // need to be `Forall`-quantified, but `Term::Lam` has no
                // such slot. Closure conversion with polymorphism is the
                // proper fix; queued as `closure-poly` (informally
                // 16b.5b). Mono enclosing fn + name-as-value-in-in-term
                // continues to work via the eta-Lam wrap.
                if in_has_value_use && !self.current_def_forall_vars.is_empty() {
                    panic!(
                        "Iter 16b.6: name-as-value of LetRec `{name}` is not yet \
                         supported in a polymorphic enclosing fn — closure conversion \
                         with polymorphism would be required. Queued separately as \
                         `closure-poly` (informally 16b.5b)."
                    );
                }

                // Recompute captures of the lifted body against the
                // current `locals` (deterministic order via BTreeSet).
                let mut local_bound: BTreeSet<String> = BTreeSet::new();
                local_bound.insert(name.clone());
                for p in params {
                    local_bound.insert(p.clone());
                }
                let mut frees: BTreeSet<String> = BTreeSet::new();
                free_vars_in_term(&lifted_body, &local_bound, &mut frees);
                let captures: Vec<String> = frees
                    .iter()
                    .filter(|f| locals.contains_key(*f))
                    .cloned()
                    .collect();

                // Iter 16b.7: if any capture refers to an enclosing
                // LetRec's NAME (rather than its params or a regular
                // local), reject. Lifting `name$lr_N` with `outer` as a
                // fn-typed extra param would mis-compile: the outer
                // LetRec has not been lifted yet, and once it is, its
                // own captures must be threaded through every value-
                // position use — exactly the closure-of-self problem.
                // Outer-LetRec PARAMS (KnownType in the desugar marker)
                // are fine and reach here as ordinary locals.
                for c in &captures {
                    if self.enclosing_letrec_names.contains(c) {
                        panic!(
                            "Iter 16b.7: nested LetRec `{name}` captures outer LetRec name \
                             `{c}` — closure conversion of a LetRec inside its own body \
                             would be required (the capture's value is the outer LetRec's \
                             pre-lift fn-value, which has no callable form before the \
                             outer lift completes). Queued as `closure-of-self` (informally \
                             16b.5-body / closure-poly)."
                        );
                    }
                }

                // Resolve each capture's type via the locals table
                // (populated as we walked).
                let mut capture_types: Vec<(String, Type)> = Vec::new();
                for c in &captures {
                    let t = locals.get(c).cloned().unwrap_or_else(|| {
                        panic!(
                            "Iter 16b.3 invariant: LetRec `{name}` capture `{c}` not in \
                             locals at lift time — capture set inconsistent with env walk"
                        )
                    });
                    capture_types.push((c.clone(), t));
                }

                // Build the lifted FnDef.
                //
                // Iter 16b.6: when the enclosing fn is polymorphic, wrap
                // the augmented Fn in a `Type::Forall` mirroring the
                // enclosing fn's type vars (`current_def_forall_vars`).
                // The capture types may mention any of those vars; the
                // Forall binds them. Codegen's mono pipeline (Iter
                // 12b/14a) specialises `f$lr_N` at every call site with
                // the same type args as the enclosing fn's current
                // mono — see `apply_subst_to_type`, which substitutes
                // through both the original params and the appended
                // capture types uniformly because they're all `Type::Fn`
                // params at the AST level.
                let inner_augmented_ty = match ty {
                    Type::Fn { params: ps, ret, effects, .. } => {
                        let mut new_ps = ps.clone();
                        for (_, t) in &capture_types {
                            new_ps.push(t.clone());
                        }
                        Type::Fn {
                            params: new_ps,
                            ret: ret.clone(),
                            effects: effects.clone(),
                            param_modes: vec![],
                            ret_mode: ParamMode::Implicit,
                        }
                    }
                    Type::Forall { .. } => panic!(
                        "Iter 16b.6 invariant: LetRec `{name}` has its OWN Forall type at \
                         lift; LetRec doesn't quantify, only the enclosing fn does"
                    ),
                    other => panic!(
                        "Iter 16b.3 invariant: LetRec `{name}` non-Fn/Forall type {:?}",
                        other
                    ),
                };
                let augmented_ty = if self.current_def_forall_vars.is_empty() {
                    inner_augmented_ty
                } else {
                    Type::Forall {
                        vars: self.current_def_forall_vars.clone(),
                        constraints: vec![],
                        body: Box::new(inner_augmented_ty),
                    }
                };
                let mut augmented_params = params.clone();
                for (cn, _) in &capture_types {
                    augmented_params.push(cn.clone());
                }

                let lifted_name = self.fresh_lifted(name);
                let extras: Vec<String> =
                    capture_types.iter().map(|(n, _)| n.clone()).collect();

                // Body rewrite: every `(app name args)` → `(app
                // lifted_name args... cap0 cap1 ...)`. Then rename
                // any leftover `Var{name}` (none in practice — already
                // ruled out by find_non_callee_use). Symmetrical with
                // the 16b.2 desugar lift.
                let body_call_rw =
                    subst_call_with_extras(&lifted_body, name, &lifted_name, &extras);
                let body_full = subst_var(&body_call_rw, name, &lifted_name);

                // In-clause: rewrite call sites, but skip subst_var so that
                // bare `Var{name}` references (16b.5: name-as-value uses)
                // can resolve to the eta-Lam binding we wrap below.
                let in_call_rw =
                    subst_call_with_extras(&lifted_in, name, &lifted_name, &extras);

                // 16b.5: extract effects, param types, ret type from the
                // LetRec's declared type to mirror them on the eta-Lam.
                let (orig_param_tys, orig_ret_ty, lr_effects): (Vec<Type>, Type, Vec<String>) =
                    match ty {
                        Type::Fn { params: ps, ret, effects, .. } => {
                            (ps.clone(), (**ret).clone(), effects.clone())
                        }
                        Type::Forall { .. } => unreachable!("rejected above"),
                        _ => unreachable!("rejected above"),
                    };

                let in_full = if in_has_value_use {
                    let lam_args: Vec<Term> = params
                        .iter()
                        .map(|p| Term::Var { name: p.clone() })
                        .chain(extras.iter().map(|c| Term::Var { name: c.clone() }))
                        .collect();
                    let lam_body = Term::App {
                        callee: Box::new(Term::Var { name: lifted_name.clone() }),
                        args: lam_args,
                        tail: false,
                    };
                    let eta_lam = Term::Lam {
                        params: params.clone(),
                        param_tys: orig_param_tys,
                        ret_ty: Box::new(orig_ret_ty),
                        effects: lr_effects,
                        body: Box::new(lam_body),
                    };
                    Term::Let {
                        name: name.clone(),
                        value: Box::new(eta_lam),
                        body: Box::new(in_call_rw),
                    }
                } else {
                    // No name-as-value uses: defensive subst_var keeps
                    // the historical zero-capture symmetry intact.
                    subst_var(&in_call_rw, name, &lifted_name)
                };

                // Append the lifted FnDef. The doc string makes
                // post-mortem debugging easier — anything containing
                // `$lr_` plus this string is a 16b.3 lift.
                let doc = format!(
                    "Lifted by 16b.3 from let-rec '{name}' inside '{in_def}'."
                );
                self.lifted.push(Def::Fn(FnDef {
                    name: lifted_name.clone(),
                    ty: augmented_ty.clone(),
                    params: augmented_params,
                    body: body_full,
                    suppress: vec![],
                    doc: Some(doc),
                }));

                // Update env globals so any outer LetRec lifted later
                // sees the new top-level fn.
                self.env
                    .globals
                    .insert(lifted_name.clone(), augmented_ty);
                self.module_names.insert(lifted_name);

                Ok(in_full)
            }
        }
    }

    /// Iter 16b.3: produce a fresh `<hint>$lr_N` name not present in
    /// `module_names`. Bumps `counter` and `module_names` so a later
    /// lift cannot collide.
    fn fresh_lifted(&mut self, hint: &str) -> String {
        loop {
            let candidate = format!("{hint}$lr_{}", self.counter);
            self.counter += 1;
            if !self.module_names.contains(&candidate) {
                self.module_names.insert(candidate.clone());
                return candidate;
            }
        }
    }

    /// Synthesize the type of an already-lifted sub-term against the
    /// current env+locals. Used for `Term::Let.value` (so the body's
    /// `name` gets a typed local) and `Term::Match.scrutinee` (so
    /// pattern bindings get typed locals).
    ///
    /// We re-run inference on the sub-term — it has already passed
    /// the typechecker once before lift, so this is guaranteed to
    /// succeed under the same env / locals.
    fn synth_type(
        &mut self,
        t: &Term,
        locals: &mut IndexMap<String, Type>,
        in_def: &str,
    ) -> Result<Type> {
        let mut subst = Subst::default();
        let mut counter: u32 = 0;
        let mut effects: BTreeSet<String> = BTreeSet::new();
        // Iter 22b.2 (Task 9): the lift pass does its own type
        // synthesis to figure out free-var types for letrec captures.
        // Class-method residuals collected here are discarded — the
        // missing-constraint check has already run for the enclosing
        // fn during `check_fn`. Threading the accumulator only keeps
        // `synth`'s signature uniform.
        let mut residuals: Vec<crate::ResidualConstraint> = Vec::new();
        let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals)?;
        Ok(subst.apply(&ty))
    }
}

/// Iter 16b.3: returns true iff any `Def::Fn` body or `Def::Const`
/// value in `m` reaches a `Term::LetRec`. Used as a fast-path skip:
/// modules without any deferred LetRec need no traversal at all.
fn contains_any_letrec(m: &Module) -> bool {
    fn term_has_letrec(t: &Term) -> bool {
        match t {
            Term::Lit { .. } | Term::Var { .. } => false,
            Term::App { callee, args, .. } => {
                term_has_letrec(callee) || args.iter().any(term_has_letrec)
            }
            Term::Let { value, body, .. } => term_has_letrec(value) || term_has_letrec(body),
            Term::If { cond, then, else_ } => {
                term_has_letrec(cond) || term_has_letrec(then) || term_has_letrec(else_)
            }
            Term::Do { args, .. } => args.iter().any(term_has_letrec),
            Term::Ctor { args, .. } => args.iter().any(term_has_letrec),
            Term::Match { scrutinee, arms } => {
                term_has_letrec(scrutinee) || arms.iter().any(|a| term_has_letrec(&a.body))
            }
            Term::Lam { body, .. } => term_has_letrec(body),
            Term::Seq { lhs, rhs } => term_has_letrec(lhs) || term_has_letrec(rhs),
            Term::LetRec { .. } => true,
            // Iter 18c.1: identity passthrough for the letrec-detection scan.
            Term::Clone { value } => term_has_letrec(value),
            // Iter 18d.1: structural recursion through both children.
            Term::ReuseAs { source, body } => term_has_letrec(source) || term_has_letrec(body),
        }
    }
    for def in &m.defs {
        match def {
            Def::Fn(f) if term_has_letrec(&f.body) => return true,
            Def::Const(c) if term_has_letrec(&c.value) => return true,
            _ => {}
        }
    }
    false
}

/// Iter 16b.3: scan `defs` for the highest existing `*$lr_N` suffix
/// and return that N. Used to seed `Lifter.counter` past any
/// 16b.2-lifted defs that already live in the desugared module.
fn highest_lr_suffix(defs: &[Def]) -> Option<u64> {
    let mut max: Option<u64> = None;
    for def in defs {
        let name = def.name();
        if let Some(idx) = name.rfind("$lr_") {
            let suffix = &name[idx + "$lr_".len()..];
            if let Ok(n) = suffix.parse::<u64>() {
                max = Some(max.map(|m| m.max(n)).unwrap_or(n));
            }
        }
    }
    max
}

/// Iter 16b.3: minimal pattern → bindings inference for the lift
/// pass. Called only for patterns the typechecker has already
/// accepted, so we propagate just enough to resolve capture types
/// (we don't re-run unification here — the typechecker did that
/// already).
///
/// Mirrors the relevant arms of `crate::type_check_pattern` but only
/// for the side effect we need: returning a mapping
/// `binder_name -> Type`. Returns `Internal` if the pattern shape
/// cannot be handled — every shape that the typechecker accepts
/// reaches here.
fn type_check_pattern_for_lift(
    p: &Pattern,
    s_ty: &Type,
    env: &Env,
) -> Result<Vec<(String, Type)>> {
    match p {
        Pattern::Wild | Pattern::Lit { .. } => Ok(vec![]),
        Pattern::Var { name } => Ok(vec![(name.clone(), s_ty.clone())]),
        Pattern::Ctor { ctor, fields } => {
            // Resolve the ctor against the scrutinee's type.
            let (td, type_args, owner_module): (TypeDef, Vec<Type>, Option<String>) =
                match s_ty {
                    Type::Con { name, args } => {
                        if name.matches('.').count() == 1 {
                            let (prefix, suffix) = name.split_once('.').expect("checked");
                            let target_module = env
                                .imports
                                .get(prefix)
                                .cloned()
                                .or_else(|| {
                                    if env.module_types.contains_key(prefix) {
                                        Some(prefix.to_string())
                                    } else {
                                        None
                                    }
                                })
                                .ok_or_else(|| CheckError::UnknownModule {
                                    module: prefix.to_string(),
                                })?;
                            let td = env
                                .module_types
                                .get(&target_module)
                                .and_then(|tys| tys.get(suffix))
                                .cloned()
                                .ok_or_else(|| CheckError::UnknownType(name.clone()))?;
                            (td, args.clone(), Some(target_module))
                        } else {
                            let td = env
                                .types
                                .get(name)
                                .cloned()
                                .ok_or_else(|| CheckError::UnknownType(name.clone()))?;
                            (td, args.clone(), None)
                        }
                    }
                    _ => {
                        return Err(CheckError::PatternTypeMismatch {
                            ctor: ctor.clone(),
                            ty: ailang_core::pretty::type_to_string(s_ty),
                        });
                    }
                };
            let cdef = td
                .ctors
                .iter()
                .find(|c| &c.name == ctor)
                .cloned()
                .ok_or_else(|| CheckError::UnknownCtor {
                    ty: td.name.clone(),
                    ctor: ctor.clone(),
                })?;
            if fields.len() != cdef.fields.len() {
                return Err(CheckError::CtorArity {
                    ty: td.name.clone(),
                    ctor: ctor.clone(),
                    expected: cdef.fields.len(),
                    got: fields.len(),
                });
            }
            // Substitute the ADT's type vars with the actual args
            // from the scrutinee's `Type::Con.args`. Field types may
            // contain owning-module-qualified type-cons references
            // (the same qualification dance `synth` does for
            // `Term::Ctor`), but we don't need to do it here — the
            // pattern var's recorded type is consumed only by the
            // lifter to seed locals, and any capture's type that
            // includes a qualified type-cons gets passed verbatim
            // into the lifted FnDef's signature.
            let _ = owner_module; // (unused in this minimal lookup)
            let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
            for (v, a) in td.vars.iter().zip(type_args.iter()) {
                mapping.insert(v.clone(), a.clone());
            }
            let mut out: Vec<(String, Type)> = Vec::new();
            for (sub_pat, field_ty) in fields.iter().zip(cdef.fields.iter()) {
                let inst_ty = substitute_rigids_local(field_ty, &mapping);
                out.extend(type_check_pattern_for_lift(sub_pat, &inst_ty, env)?);
            }
            Ok(out)
        }
    }
}

/// Local copy of the substitution helper from `crate`. Inlined here
/// because the original is private to the parent module; the
/// lifter only needs the mono-substitution case.
fn substitute_rigids_local(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
    match t {
        Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()),
        Type::Con { name, args } => Type::Con {
            name: name.clone(),
            args: args.iter().map(|a| substitute_rigids_local(a, mapping)).collect(),
        },
        Type::Fn { params, ret, effects, .. } => Type::Fn {
            params: params
                .iter()
                .map(|p| substitute_rigids_local(p, mapping))
                .collect(),
            ret: Box::new(substitute_rigids_local(ret, mapping)),
            effects: effects.clone(),
            param_modes: vec![],
            ret_mode: ParamMode::Implicit,
        },
        Type::Forall { vars, constraints, body } => {
            let inner: BTreeMap<String, Type> = mapping
                .iter()
                .filter(|(k, _)| !vars.contains(k))
                .map(|(k, v)| (k.clone(), v.clone()))
                .collect();
            Type::Forall {
                vars: vars.clone(),
                constraints: constraints.clone(),
                body: Box::new(substitute_rigids_local(body, &inner)),
            }
        }
    }
}
