//! Iter 18c.2: linearity check for fns whose every parameter mode is
//! explicit (`Borrow` or `Own`).
//!
//! ## Scope
//!
//! - **Active only** on `Def::Fn` whose `Type::Fn.param_modes` is
//!   non-empty AND contains no [`ParamMode::Implicit`]. Any
//!   `Implicit`-mode param skips the entire fn — that is the back-compat
//!   lane that keeps every existing fixture green (only
//!   `borrow_own_demo` ships an all-explicit signature today).
//! - **Pure diagnostic.** Emits [`Diagnostic`]s with codes
//!   `use-after-consume` / `consume-while-borrowed`. No IR change, no
//!   codegen change, no runtime change. The check runs after
//!   [`crate::check_fn`] type-checking succeeded for the def.
//! - **No uniqueness inference.** That is Iter 18c.3. The check only
//!   tracks what is *spelled* in the source: a binder is consumed when
//!   it appears in a non-borrow position; cloned via [`Term::Clone`];
//!   borrowed via fn-call into a `Borrow` parameter.
//!
//! ## Position model
//!
//! Each [`Term::Var`] occurrence is in some "position", determined by
//! its parent term:
//!
//! - **Consume** — default. The use takes ownership.
//! - **Borrow** — the use lends a reference; ownership stays with the
//!   binder.
//!
//! Position propagation:
//! - `Term::App.callee` — Consume (the value is called once).
//! - `Term::App.args[i]` — Borrow if the callee is a `Var` whose
//!   resolved type is a `Type::Fn` with `param_modes[i] == Borrow`;
//!   otherwise Consume (Own / Implicit / unknown all default to
//!   Consume).
//! - `Term::Clone.value` — Borrow (clone reads + bumps RC, doesn't
//!   move).
//! - `Term::Match.scrutinee` — Borrow (matching is a read; for an
//!   `Own` param this leaves the binder uneconsumed, which is a known
//!   false-negative for "param declared own but never moved" — out of
//!   scope for 18c.2 per the assignment).
//! - `Term::Let.value`, `Term::Seq.lhs`, `Term::If.cond` — Consume.
//! - `Term::Ctor.args[*]`, `Term::Do.args[*]` — Consume.
//! - `Term::Lam` — captures are conservatively Consume.
//!
//! ## Within-call borrow lifetime (consume-while-borrowed)
//!
//! For `App { callee, args, .. }` whose callee is a `Var` resolving to
//! a fn-typed binding with explicit `param_modes`: when the i-th arg is
//! a bare `Term::Var { name }` consumed in Borrow position, we
//! **increment** `borrow_count[name]` *before* evaluating
//! `args[i+1..]`. After all args are evaluated and the call has run,
//! we **decrement** them again. So a sibling subterm that consumes the
//! same binder while it is still borrowed by an earlier sibling
//! triggers the `consume-while-borrowed` diagnostic.
//!
//! For a `Borrow` *parameter* of the enclosing fn, the binder starts
//! the body with `borrow_count = 1` (the caller's outer borrow). Any
//! attempt to consume it inside the body therefore also triggers
//! `consume-while-borrowed`.
//!
//! ## Suggested rewrites
//!
//! Each diagnostic carries a non-empty
//! [`crate::diagnostic::Diagnostic::suggested_rewrites`]. The form-A
//! replacement is parseable by [`ailang_surface::parse_term`] — that's
//! the contract guarded by the round-trip test in `tests/`.
//!
//! - `use-after-consume` on `Var x`: replacement `(clone <name>)` —
//!   the author should clone an *earlier* use so this later use stays
//!   the unique consume.
//! - `consume-while-borrowed` on `Var x`: replacement `(clone <name>)`
//!   — the author should clone here so the original keeps the borrow.
//!
//! ## Iter 19a: `over-strict-mode` lint
//!
//! After the linearity walk has finished for a fn whose every param
//! mode is explicit, we re-inspect each param annotated `(own T)`:
//!
//! - The uniqueness pass ([`crate::uniqueness::infer_module`]) gives
//!   us the param's `consume_count` and, importantly, the
//!   `consume_count` of every pattern-binder introduced when the
//!   param is matched on.
//! - If `consume_count(p) == 0` AND, for every `match p ...` in the
//!   body, every pattern-binder bound by an arm of that match has
//!   `consume_count == 0`, then the fn could have been written with
//!   `(borrow T)` instead and would be cheaper to call (no inc/dec
//!   pair, no rec-cascade at fn return). Emit `over-strict-mode` as
//!   a `Severity::Warning` with a suggested fn-type rewrite.
//!
//! ### Iter 19a.1: precise sub-binder analysis
//!
//! 19a originally shipped a conservative cut ("any `match` whose
//! scrutinee is `p` silences the lint") because the precise check
//! seemed to require a new side-table. In practice the side-table
//! is already there: the uniqueness pass populates `consume_count`
//! for every binder including pattern-binders. 19a.1 replaces the
//! cut with a precise per-arm walk: for each `(match p ...)`, we
//! ask whether any **heap-typed** pattern-binder of any arm has
//! `consume_count > 0`. If yes, `(own T)` is genuinely needed and
//! the lint stays silent. If no, the param is purely read by the
//! match and the lint fires — exactly the shape of fixtures like
//! `rc_own_param_drop.head_or_zero` (which only returns the head
//! and never moves the tail).
//!
//! ### Why "heap-typed" matters
//!
//! A pattern-binder of primitive type (`Int` / `Bool` / `Str` /
//! `Unit`) being consumed does not force the scrutinee to be `Own`
//! — primitives are copied out by value, no RC operation is
//! involved. The uniqueness pass bumps `consume_count` for every
//! Consume-position read regardless of type, so the lint must
//! filter primitive-typed binders out via the pattern's parent
//! ctor field types. `head_or_zero`'s body
//! `match xs { Cons(h, t) => h }` returns `h: Int`; without the
//! filter, `h.consume_count == 1` would silence the lint.
//!
//! **Known debt: deeply-nested-match-on-sub-binder.** A pattern like
//! `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }`
//! has the inner match's scrutinee `t` (not `p`), so the inner-arm
//! binder `t2`'s consume is not seen when we ask "did any arm-binder
//! of `match p` get consumed?". The outer-arm binder `t` has
//! `consume_count == 0` (matching is Borrow), so the lint will fire
//! even though `(own T)` is genuinely needed because `t2` is
//! consumed. This is recorded in the JOURNAL as a follow-up; for the
//! current corpus it would cost a spurious warning rather than miss
//! a real one.

use crate::diagnostic::Diagnostic;
use crate::uniqueness::{infer_module as infer_uniqueness, UniquenessTable};
use ailang_core::ast::{Arm, Ctor, Def, FnDef, Module, ParamMode, Pattern, Term, Type};
use ailang_surface::{term_to_form_a, type_to_form_a};
use std::collections::HashMap;

/// Iter 19a.1: a `Type::Con` whose name is `Int`/`Bool`/`Str`/`Unit`
/// is a primitive value type — no RC, no heap. Reading a primitive
/// pattern-binder bumps `consume_count` in the uniqueness table but
/// does not force the scrutinee param to be `Own`. The lint filters
/// those out so a fn like `match xs { Cons(h, t) => h }` (where `h`
/// is `Int`) can still fire `over-strict-mode` when `t.consume_count
/// == 0`.
fn is_heap_type(t: &Type) -> bool {
    match t {
        Type::Con { name, .. } => !matches!(name.as_str(), "Int" | "Bool" | "Str" | "Unit"),
        // Type::Var (a polymorphic param) is conservatively heap —
        // it could instantiate to a heap type at the call site.
        Type::Var { .. } => true,
        Type::Fn { .. } => true,
        Type::Forall { .. } => true,
    }
}

/// Position in which a [`Term::Var`] is being used. See module-level
/// docs for the propagation rules.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
enum Position {
    /// The use takes ownership (default position).
    Consume,
    /// The use lends a non-owning reference for the duration of the
    /// enclosing call (or, for `Term::Clone` / `Term::Match`, for the
    /// duration of the read).
    Borrow,
}

/// Mutable per-binder linearity state, keyed by binder name. Names
/// shadow lexically — see [`Checker::with_binder`] for the
/// save/restore pattern.
#[derive(Debug, Default, Clone)]
struct BinderState {
    /// `true` once the binder has been used in a Consume position.
    /// Subsequent uses (in any position) trigger `use-after-consume`.
    consumed: bool,
    /// Number of currently-live borrows of this binder. Incremented
    /// when a Borrow-position use starts (in a fn-call arg slot or as
    /// the initial state of a `Borrow` parameter); decremented when
    /// the borrow ends. Consume while `> 0` triggers
    /// `consume-while-borrowed`.
    borrow_count: u32,
}

/// Iter 18c.2: top-level entry. Walks every fn in `m` and emits
/// linearity diagnostics for the all-explicit-mode fns. Other fns are
/// skipped without traversal.
///
/// Output ordering: defs in declaration order; within a def, diagnostics
/// in source-order discovery (depth-first left-to-right walk).
pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
    let mut globals: HashMap<String, Type> = HashMap::new();
    // Iter 19a.1: ctor name → field types, used by the
    // `over-strict-mode` lint to filter out primitive-typed
    // pattern-binders (Int / Bool / Str / Unit) — their consume
    // does not force ownership of the scrutinee.
    let mut ctors: HashMap<String, Vec<Type>> = HashMap::new();
    for def in &m.defs {
        match def {
            Def::Fn(f) => {
                let ty = strip_forall(&f.ty);
                globals.insert(f.name.clone(), ty.clone());
            }
            Def::Const(c) => {
                globals.insert(c.name.clone(), strip_forall(&c.ty).clone());
            }
            Def::Type(td) => {
                for c in &td.ctors {
                    let Ctor { name, fields } = c;
                    ctors.insert(name.clone(), fields.clone());
                }
            }
            // Iter 22b.1: class/instance defs are skipped here. Once
            // 22b.3 monomorphisation materialises class methods as
            // ordinary `FnDef`s, the lift's globals map will pick
            // them up automatically.
            Def::Class(_) | Def::Instance(_) => {}
        }
    }

    // Iter 19a: the over-strict-mode lint reads `consume_count` from
    // the uniqueness side table. Build it once for the whole module;
    // reusing the existing pass keeps the "what counts as a consume"
    // definition in a single place.
    let uniq = infer_uniqueness(m);

    let mut diags = Vec::new();
    for def in &m.defs {
        if let Def::Fn(f) = def {
            check_fn(f, &globals, &ctors, &uniq, &mut diags);
        }
    }
    diags
}

/// Returns the inner type of a top-level `Forall<Fn ...>` (or `t`
/// unchanged if not a `Forall`). The linearity check only inspects
/// `param_modes`, which sit on the inner `Type::Fn`.
fn strip_forall(t: &Type) -> &Type {
    match t {
        Type::Forall { body, .. } => body,
        other => other,
    }
}

/// Per-fn check. Skips fns whose signature has any `Implicit` param —
/// see module-level scope rules.
fn check_fn(
    f: &FnDef,
    globals: &HashMap<String, Type>,
    ctors: &HashMap<String, Vec<Type>>,
    uniq: &UniquenessTable,
    diags: &mut Vec<Diagnostic>,
) {
    let inner = strip_forall(&f.ty);
    let (param_tys, param_modes) = match inner {
        Type::Fn { params, param_modes, .. } => (params.as_slice(), param_modes.as_slice()),
        _ => return,
    };

    // Activation gate: every param mode must be explicit (Borrow / Own).
    // No params at all also disables the check — there are no binders
    // to track in the param-list, so the check has nothing to enforce.
    if param_modes.is_empty() || param_modes.iter().any(|m| matches!(m, ParamMode::Implicit)) {
        return;
    }

    // Sanity: param-count has been verified by `check_fn` upstream, but
    // double-defend in case the type vec is shorter than the binder list
    // — the linearity walk treats over-long binder lists as `Implicit`
    // and would silently mis-skip the check otherwise.
    if param_modes.len() != f.params.len() || param_tys.len() != f.params.len() {
        return;
    }

    let mut checker = Checker {
        globals,
        diags,
        def_name: &f.name,
        binders: HashMap::new(),
    };

    // Install fn parameters as binders, with initial `borrow_count = 1`
    // for `Borrow` params (the caller's outer borrow stays live for the
    // body's whole duration) and `0` for `Own` params.
    for (name, mode) in f.params.iter().zip(param_modes.iter()) {
        let initial = BinderState {
            consumed: false,
            borrow_count: match mode {
                ParamMode::Borrow => 1,
                ParamMode::Own | ParamMode::Implicit => 0,
            },
        };
        checker.binders.insert(name.clone(), initial);
    }

    checker.walk(&f.body, Position::Consume);

    // Iter 19a / 19a.1: `over-strict-mode` lint. After the linearity
    // walk has completed (and any errors have been recorded), inspect
    // each `Own`-annotated param: if `consume_count(p) == 0` AND no
    // pattern-binder of any `(match p ...)` arm in the body has
    // `consume_count > 0`, the param could be re-annotated `Borrow`.
    // Emit a Warning with a form-A rewrite.
    //
    // The precise sub-binder check (19a.1) replaces 19a's
    // conservative "any match on `p` silences" cut: matching on `p`
    // is fine as long as none of the arms moves a sub-binder out.
    // The uniqueness pass already populates `consume_count` for
    // pattern-binders, so the check is a deterministic walk.
    for (i, mode) in param_modes.iter().enumerate() {
        if !matches!(mode, ParamMode::Own) {
            continue;
        }
        let pname = &f.params[i];
        let consume_count = uniq
            .get(&(f.name.clone(), pname.clone()))
            .map(|info| info.consume_count)
            .unwrap_or(0);
        if consume_count != 0 {
            continue;
        }
        if any_sub_binder_consumed_for(&f.body, pname, uniq, &f.name, ctors) {
            // A pattern-binder of some `(match p ...)` arm is
            // consumed → `(own T)` is genuinely needed. Stay silent.
            continue;
        }
        diags.push(make_over_strict_mode(&f.name, pname, inner, i));
    }
}

/// Per-fn linearity walker.
struct Checker<'a> {
    /// Top-level symbol → type. Used to look up the param_modes of an
    /// `App` callee that resolves to a global fn def.
    globals: &'a HashMap<String, Type>,
    /// Diagnostic accumulator (shared with the module-level walk).
    diags: &'a mut Vec<Diagnostic>,
    /// Name of the fn currently being checked (becomes
    /// [`Diagnostic::def`]).
    def_name: &'a str,
    /// Live binder state, keyed by name. Modified in place; lexical
    /// scoping is restored by [`Checker::with_binder`].
    binders: HashMap<String, BinderState>,
}

impl<'a> Checker<'a> {
    /// The core position-aware walk. Recurses through `t` and updates
    /// per-binder state according to the rules in the module-level
    /// docs.
    fn walk(&mut self, t: &Term, pos: Position) {
        match t {
            Term::Lit { .. } => {}
            Term::Var { name } => self.use_var(name, pos),
            Term::App { callee, args, .. } => {
                // The callee itself is consumed (it's "the function value");
                // for var-callees this is typically a global fn ref.
                self.walk(callee, Position::Consume);

                // Determine arg modes from the callee's resolved type.
                let arg_modes = self.callee_arg_modes(callee, args.len());

                // Track which binders we lent so we can release them
                // after the call.
                let mut lent: Vec<String> = Vec::new();

                for (i, arg) in args.iter().enumerate() {
                    let arg_pos = match arg_modes.get(i) {
                        Some(ParamMode::Borrow) => Position::Borrow,
                        // Own / Implicit / unknown → Consume.
                        _ => Position::Consume,
                    };
                    self.walk(arg, arg_pos);

                    // If we lent a *bare* binder reference at this arg
                    // slot, the borrow stays live for the rest of the
                    // call (i.e. while subsequent args evaluate, and
                    // until the callee returns). Bump `borrow_count`
                    // now so a sibling Consume of the same binder
                    // triggers `consume-while-borrowed`.
                    if matches!(arg_pos, Position::Borrow) {
                        if let Term::Var { name } = arg {
                            if let Some(s) = self.binders.get_mut(name) {
                                s.borrow_count = s.borrow_count.saturating_add(1);
                                lent.push(name.clone());
                            }
                        }
                    }
                }

                // Call returns: all lent borrows end.
                for name in lent {
                    if let Some(s) = self.binders.get_mut(&name) {
                        s.borrow_count = s.borrow_count.saturating_sub(1);
                    }
                }
            }
            Term::Let { name, value, body } => {
                self.walk(value, Position::Consume);
                self.with_binder(name, BinderState::default(), |this| {
                    this.walk(body, pos);
                });
            }
            Term::LetRec { name, body, in_term, .. } => {
                // The body is the recursive fn's own body; treating it as
                // an opaque closure is sufficient for 18c.2 — its
                // captures are conservatively traversed in `Consume`
                // mode but with the recursive `name` masked (so the
                // recursive self-reference does not flag as a
                // use-after-consume of the in_term's view).
                self.with_binder(name, BinderState::default(), |this| {
                    this.walk(body, Position::Consume);
                    this.walk(in_term, pos);
                });
            }
            Term::If { cond, then, else_ } => {
                self.walk(cond, Position::Consume);
                // Branch independence: each arm starts from the pre-branch
                // state. If any arm consumes/borrows a binder, that
                // outcome is visible to the post-`If` continuation
                // (conservative merge: union of consumed flags, max of
                // borrow_count).
                let saved = self.binders.clone();
                self.walk(then, pos);
                let after_then = std::mem::replace(&mut self.binders, saved);
                self.walk(else_, pos);
                merge_states(&mut self.binders, &after_then);
            }
            Term::Match { scrutinee, arms } => {
                // Scrutinee is read (Borrow), not moved.
                self.walk(scrutinee, Position::Borrow);
                let saved = self.binders.clone();
                let mut acc: Option<HashMap<String, BinderState>> = None;
                for arm in arms {
                    self.binders = saved.clone();
                    self.walk_arm(arm, pos);
                    match acc.as_mut() {
                        None => acc = Some(self.binders.clone()),
                        Some(m) => merge_states(m, &self.binders),
                    }
                }
                if let Some(merged) = acc {
                    self.binders = merged;
                } else {
                    self.binders = saved;
                }
            }
            Term::Seq { lhs, rhs } => {
                self.walk(lhs, Position::Consume);
                self.walk(rhs, pos);
            }
            Term::Ctor { args, .. } => {
                // Ctor args are consumed (the new value owns them).
                for a in args {
                    self.walk(a, Position::Consume);
                }
            }
            Term::Do { args, .. } => {
                for a in args {
                    self.walk(a, Position::Consume);
                }
            }
            Term::Lam { params, body, .. } => {
                // Lam captures cross the linearity boundary: any free
                // var of the body is implicitly consumed by closure
                // construction (we don't yet model captured-borrow
                // discipline; that is 18c.3 territory). For 18c.2 we
                // walk the body with the lam's own params as fresh
                // binders.
                let mut saved_for_params: HashMap<String, Option<BinderState>> = HashMap::new();
                for p in params {
                    saved_for_params.insert(p.clone(), self.binders.remove(p));
                    self.binders.insert(p.clone(), BinderState::default());
                }
                self.walk(body, Position::Consume);
                for p in params {
                    self.binders.remove(p);
                    if let Some(prev) = saved_for_params.remove(p).flatten() {
                        self.binders.insert(p.clone(), prev);
                    }
                }
            }
            Term::Clone { value } => {
                // (clone X) reads X (Borrow) regardless of outer pos:
                // the resulting *value* is owned, but the inner term is
                // only borrowed. So `(clone xs)` does NOT consume `xs`.
                self.walk(value, Position::Borrow);
            }
            Term::ReuseAs { source, body } => {
                // Iter 18d.1: linearity for `(reuse-as SRC BODY)`:
                //   - `SRC` must be a bare `Var { name }` of an
                //     in-scope binder (else `reuse-as-source-not-bare-var`).
                //   - The binder must currently have `consumed == false`
                //     (else `use-after-consume` at this site).
                //   - Visiting reuse-as marks the binder consumed (the
                //     reuse semantics is "this is where the source is
                //     freed/overwritten").
                //   - `BODY` walks normally — its sub-uses are subject
                //     to the usual position rules; e.g. a Consume of
                //     the same binder inside `BODY` will fire
                //     use-after-consume because reuse-as already ate it.
                match source.as_ref() {
                    Term::Var { name } if self.binders.contains_key(name) => {
                        let already_consumed = self
                            .binders
                            .get(name)
                            .map(|s| s.consumed)
                            .unwrap_or(false);
                        if already_consumed {
                            self.diags
                                .push(make_use_after_consume_at_reuse_as(self.def_name, name, body));
                        } else if let Some(s) = self.binders.get_mut(name) {
                            // Mark the source consumed at the reuse-as site.
                            s.consumed = true;
                        }
                    }
                    other => {
                        self.diags.push(make_reuse_as_source_not_bare_var(
                            self.def_name,
                            other,
                            body,
                        ));
                    }
                }
                // Walk the body normally; its sub-uses go through the
                // standard position rules.
                self.walk(body, pos);
            }
        }
    }

    /// Walk one match arm: introduce the pattern's bindings as fresh
    /// `Live` binders, walk the body, then drop them. Pattern bindings
    /// are linearity-fresh in 18c.2; we do not yet track ownership
    /// transfer from the scrutinee (that requires modelling pattern
    /// borrow vs. consume, which is 18c.3 work).
    fn walk_arm(&mut self, arm: &Arm, pos: Position) {
        let names = collect_pattern_binders(&arm.pat);
        let mut saved: HashMap<String, Option<BinderState>> = HashMap::new();
        for n in &names {
            saved.insert(n.clone(), self.binders.remove(n));
            self.binders.insert(n.clone(), BinderState::default());
        }
        self.walk(&arm.body, pos);
        for n in &names {
            self.binders.remove(n);
            if let Some(prev) = saved.remove(n).flatten() {
                self.binders.insert(n.clone(), prev);
            }
        }
    }

    /// Record a use of `name` in `pos`. If `name` is not a tracked
    /// binder (i.e. it's a global / built-in), we ignore the use.
    ///
    /// Note: Borrow-position uses do **not** increment `borrow_count`
    /// here. The counter tracks borrows whose lifetime extends across
    /// sibling subterms — only the [`Term::App`] walker manages those
    /// (incrementing before the next sibling, decrementing when the
    /// call returns). A scrutinee or `Term::Clone` borrow does not
    /// span siblings, so it just checks `consumed` and returns.
    fn use_var(&mut self, name: &str, pos: Position) {
        let state = match self.binders.get_mut(name) {
            Some(s) => s,
            None => return,
        };

        // Already-consumed: any further use is a use-after-consume,
        // regardless of position.
        if state.consumed {
            self.diags
                .push(make_use_after_consume(self.def_name, name));
            return;
        }

        match pos {
            Position::Borrow => {
                // No state change; the App walker is responsible for
                // bumping `borrow_count` when a Borrow arg lives across
                // sibling args, and for the per-fn-param initial value.
            }
            Position::Consume => {
                if state.borrow_count > 0 {
                    self.diags
                        .push(make_consume_while_borrowed(self.def_name, name));
                    return;
                }
                state.consumed = true;
            }
        }
    }

    /// Resolve the param-mode vector of a fn-call's callee.
    ///
    /// Currently only handles `callee = Term::Var { name }` resolving
    /// to a global fn type (with explicit `param_modes`). All other
    /// callee shapes return an empty vec → all args default to
    /// Consume. This is the conservative, "no false negatives on the
    /// borrow-arg case" behaviour: if we can't see the modes, we
    /// assume Consume and may miss a borrow.
    fn callee_arg_modes(&self, callee: &Term, n_args: usize) -> Vec<ParamMode> {
        let name = match callee {
            Term::Var { name } => name,
            _ => return vec![],
        };
        // Locals never carry fn-types in 18c.2 (no first-class fn vars
        // with mode info). Look up the global symbol table.
        let ty = match self.globals.get(name) {
            Some(t) => t,
            None => return vec![],
        };
        let inner = strip_forall(ty);
        match inner {
            Type::Fn { param_modes, .. } => {
                if param_modes.is_empty() {
                    // All-implicit case (legacy): no mode info → all
                    // Consume, by the rule above.
                    vec![ParamMode::Implicit; n_args]
                } else {
                    param_modes.clone()
                }
            }
            _ => vec![],
        }
    }

    /// Save the current state of `name`, install `fresh` for the
    /// duration of `body`, then restore. Used by `Let` / `LetRec` /
    /// `Lam` / pattern-arm to introduce a fresh binder while
    /// preserving lexical scope.
    fn with_binder<F: FnOnce(&mut Self)>(&mut self, name: &str, fresh: BinderState, body: F) {
        let prev = self.binders.remove(name);
        self.binders.insert(name.to_string(), fresh);
        body(self);
        self.binders.remove(name);
        if let Some(p) = prev {
            self.binders.insert(name.to_string(), p);
        }
    }
}

/// Recursively collect every binder name introduced by a pattern.
/// Wildcards and literals contribute nothing; `Var` adds itself; `Ctor`
/// recurses into fields.
fn collect_pattern_binders(p: &Pattern) -> Vec<String> {
    match p {
        Pattern::Wild | Pattern::Lit { .. } => vec![],
        Pattern::Var { name } => vec![name.clone()],
        Pattern::Ctor { fields, .. } => fields
            .iter()
            .flat_map(|f| collect_pattern_binders(f))
            .collect(),
    }
}

/// Conservative merge of two branch states: a binder is consumed in
/// the merged state iff it was consumed in either branch; borrow_count
/// becomes the max of the two. Names present only in one map are
/// carried through.
fn merge_states(into: &mut HashMap<String, BinderState>, other: &HashMap<String, BinderState>) {
    for (name, s) in other {
        let entry = into.entry(name.clone()).or_default();
        entry.consumed = entry.consumed || s.consumed;
        entry.borrow_count = entry.borrow_count.max(s.borrow_count);
    }
}

/// Build a `use-after-consume` diagnostic for `binder` in `def`.
/// Suggested rewrite: clone the offending use (the LATER use is the
/// flagged one; turning IT into `(clone <binder>)` doesn't help, but
/// the suggested rewrite is the intent — "this use should have been
/// `(clone X)`, or an earlier use should have been"). The form-A
/// snippet is `(clone <binder>)`, parseable by
/// [`ailang_surface::parse_term`].
fn make_use_after_consume(def: &str, binder: &str) -> Diagnostic {
    let replacement = term_to_form_a(&Term::Clone {
        value: Box::new(Term::Var { name: binder.to_string() }),
    });
    Diagnostic::error(
        "use-after-consume",
        format!("`{binder}` is used after it was already consumed"),
    )
    .with_def(def)
    .with_ctx(serde_json::json!({"binder": binder}))
    .with_suggested_rewrite(
        format!(
            "wrap an earlier use of `{binder}` in `(clone)` so this later use stays the unique consume"
        ),
        replacement,
    )
}

/// Iter 18d.1: build a `reuse-as-source-not-bare-var` diagnostic.
/// Fires when a `Term::ReuseAs.source` is anything other than a bare
/// `Term::Var { name }` referring to an in-scope binder. The
/// suggested rewrite drops the meaningless wrapper and keeps the
/// `body` alone.
fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> Diagnostic {
    let got = match source {
        Term::Lit { .. } => "lit",
        Term::Var { .. } => "var",
        Term::App { .. } => "app",
        Term::Let { .. } => "let",
        Term::LetRec { .. } => "let-rec",
        Term::If { .. } => "if",
        Term::Do { .. } => "do",
        Term::Ctor { .. } => "ctor",
        Term::Match { .. } => "match",
        Term::Lam { .. } => "lam",
        Term::Seq { .. } => "seq",
        Term::Clone { .. } => "clone",
        Term::ReuseAs { .. } => "reuse-as",
    };
    let replacement = term_to_form_a(body);
    Diagnostic::error(
        "reuse-as-source-not-bare-var",
        format!(
            "reuse-as source must be a bare variable referring to an in-scope binder, got {got}"
        ),
    )
    .with_def(def)
    .with_ctx(serde_json::json!({"got": got}))
    .with_suggested_rewrite(
        "drop the malformed reuse-as wrapper; keep the body alone",
        replacement,
    )
}

/// Iter 18d.1: `use-after-consume` raised at a `(reuse-as <var> <body>)`
/// site whose `<var>` binder has already been consumed elsewhere. Same
/// code as the regular use-after-consume; the suggested rewrite is to
/// drop the (now unsatisfiable) reuse hint and keep the body — the
/// allocation will happen via the normal allocator.
fn make_use_after_consume_at_reuse_as(def: &str, binder: &str, body: &Term) -> Diagnostic {
    let replacement = term_to_form_a(body);
    Diagnostic::error(
        "use-after-consume",
        format!("`{binder}` is used after it was already consumed"),
    )
    .with_def(def)
    .with_ctx(serde_json::json!({"binder": binder}))
    .with_suggested_rewrite(
        format!(
            "drop the reuse-as hint on `{binder}`; the binder is already consumed so reuse cannot fire"
        ),
        replacement,
    )
}

/// Iter 19a.1: precise sub-binder check for the over-strict-mode
/// lint. Returns `true` iff some `(match p ...)` somewhere in `t`,
/// where `p` is the param `pname`, has an arm whose pattern-binders
/// include at least one binder with `consume_count > 0` in the
/// uniqueness side table.
///
/// "Match on `p`" includes `(match p ...)` and
/// `(match (clone p) ...)` — both expose `p`'s sub-binders to the
/// arms.
///
/// Walks every other Term variant looking for further matches; a
/// `match p ...` may sit arbitrarily deep inside `If` / `Let` /
/// `App` / etc.
///
/// **Known limit (recorded as debt in JOURNAL.md):** if an arm's
/// body contains a *nested* match on a sub-binder of `p` (e.g.
/// `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }`),
/// we only check `t.consume_count`, not `t2.consume_count`. The
/// inner match's scrutinee is `t`, not `p`, and our recursion looks
/// for `match-on-pname`, so we miss `t2`. For the current corpus
/// this would mean a *spurious* warning (the lint fires but `(own)`
/// is genuinely needed), not a missed one. The fix is to either
/// chase pattern-binder lineage or to check inner matches whose
/// scrutinee transitively traces back to `p`.
fn any_sub_binder_consumed_for(
    t: &Term,
    pname: &str,
    uniq: &UniquenessTable,
    def_name: &str,
    ctors: &HashMap<String, Vec<Type>>,
) -> bool {
    match t {
        Term::Lit { .. } | Term::Var { .. } => false,
        Term::Match { scrutinee, arms } => {
            if scrutinee_matches_param(scrutinee, pname) {
                for arm in arms {
                    if pattern_has_consumed_heap_binder(&arm.pat, uniq, def_name, ctors) {
                        return true;
                    }
                    // Recurse into the arm body: a deeper
                    // `match p ...` could also count.
                    if any_sub_binder_consumed_for(&arm.body, pname, uniq, def_name, ctors) {
                        return true;
                    }
                }
                false
            } else {
                // The scrutinee isn't `p`, but `p` could still be
                // matched-on inside the scrutinee or inside any arm.
                if any_sub_binder_consumed_for(scrutinee, pname, uniq, def_name, ctors) {
                    return true;
                }
                arms.iter()
                    .any(|a| any_sub_binder_consumed_for(&a.body, pname, uniq, def_name, ctors))
            }
        }
        Term::App { callee, args, .. } => {
            any_sub_binder_consumed_for(callee, pname, uniq, def_name, ctors)
                || args
                    .iter()
                    .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors))
        }
        Term::Let { value, body, .. } => {
            any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors)
                || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
        }
        Term::LetRec { body, in_term, .. } => {
            any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
                || any_sub_binder_consumed_for(in_term, pname, uniq, def_name, ctors)
        }
        Term::If { cond, then, else_ } => {
            any_sub_binder_consumed_for(cond, pname, uniq, def_name, ctors)
                || any_sub_binder_consumed_for(then, pname, uniq, def_name, ctors)
                || any_sub_binder_consumed_for(else_, pname, uniq, def_name, ctors)
        }
        Term::Seq { lhs, rhs } => {
            any_sub_binder_consumed_for(lhs, pname, uniq, def_name, ctors)
                || any_sub_binder_consumed_for(rhs, pname, uniq, def_name, ctors)
        }
        Term::Ctor { args, .. } | Term::Do { args, .. } => args
            .iter()
            .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)),
        Term::Lam { body, .. } => any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors),
        Term::Clone { value } => any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors),
        Term::ReuseAs { source, body } => {
            any_sub_binder_consumed_for(source, pname, uniq, def_name, ctors)
                || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
        }
    }
}

/// Iter 19a.1: returns `true` if `pat` introduces any **heap-typed**
/// binder whose recorded `consume_count` is `> 0`. Primitive-typed
/// pattern-binders (`Int` / `Bool` / `Str` / `Unit`) never count
/// because reading a primitive does not force the scrutinee to be
/// `Own` — the value is copied, not moved out of the scrutinee's
/// allocation. This is the key reason `match xs { Cons(h, t) => h }`
/// (head_or_zero) fires the lint: `h: Int` is filtered out, `t:
/// IntList` has `consume_count == 0`.
///
/// Walks `Pattern::Ctor` recursively. After 16a's desugar pass,
/// top-level patterns under a Ctor field are flattened into separate
/// matches — but the recursion is defensive (cheap and correct under
/// any pattern shape; nested binders are looked up by their own name
/// in `uniq`, regardless of their pattern depth).
fn pattern_has_consumed_heap_binder(
    pat: &Pattern,
    uniq: &UniquenessTable,
    def_name: &str,
    ctors: &HashMap<String, Vec<Type>>,
) -> bool {
    pattern_has_consumed_heap_binder_at(pat, None, uniq, def_name, ctors)
}

/// Iter 19a.1: helper carrying the optional declared type of `pat`.
/// At the top of an arm pattern, `declared_ty` is `None` (we don't
/// track the scrutinee's type in the lint); the type becomes known
/// when we descend into a `Pattern::Ctor`'s fields, where the
/// ctor's `Ctor::fields[i]` gives `fields[i]`'s type.
///
/// For a `Pattern::Var { name }` with `declared_ty == None`, we
/// conservatively treat the binder as heap (we don't know its
/// type from the pattern alone). For `declared_ty == Some(t)`, we
/// only count the binder if `is_heap_type(t)`.
fn pattern_has_consumed_heap_binder_at(
    pat: &Pattern,
    declared_ty: Option<&Type>,
    uniq: &UniquenessTable,
    def_name: &str,
    ctors: &HashMap<String, Vec<Type>>,
) -> bool {
    match pat {
        Pattern::Wild | Pattern::Lit { .. } => false,
        Pattern::Var { name } => {
            // Conservative when type unknown: assume heap.
            let counts = match declared_ty {
                Some(t) => is_heap_type(t),
                None => true,
            };
            if !counts {
                return false;
            }
            uniq.get(&(def_name.to_string(), name.clone()))
                .map(|info| info.consume_count > 0)
                .unwrap_or(false)
        }
        Pattern::Ctor { ctor, fields } => {
            let field_tys: &[Type] = ctors.get(ctor).map(|v| v.as_slice()).unwrap_or(&[]);
            fields.iter().enumerate().any(|(i, f)| {
                let ty = field_tys.get(i);
                pattern_has_consumed_heap_binder_at(f, ty, uniq, def_name, ctors)
            })
        }
    }
}

/// Iter 19a: a scrutinee "is" `pname` if it's a bare `Var { pname }`
/// or `Clone(Var { pname })`. Anything else (a fresh App result, a
/// let-binder, …) does not put `pname` directly in scrutinee
/// position.
fn scrutinee_matches_param(scrutinee: &Term, pname: &str) -> bool {
    match scrutinee {
        Term::Var { name } => name == pname,
        Term::Clone { value } => scrutinee_matches_param(value, pname),
        _ => false,
    }
}

/// Iter 19a: build the `over-strict-mode` warning. `inner` is the
/// fn-type with the original mode; we synthesise a relaxed copy with
/// `param_modes[i] = Borrow` and render it through
/// [`type_to_form_a`] to produce the suggested rewrite.
fn make_over_strict_mode(def: &str, binder: &str, inner: &Type, i: usize) -> Diagnostic {
    let relaxed = relax_param_to_borrow(inner, i);
    let replacement = type_to_form_a(&relaxed);
    Diagnostic::warning(
        "over-strict-mode",
        format!(
            "param `{binder}` is annotated `(own ...)` but the body does not consume it; `(borrow ...)` would suffice"
        ),
    )
    .with_def(def)
    .with_ctx(serde_json::json!({
        "binder": binder,
        "current_mode": "own",
        "suggested_mode": "borrow",
    }))
    .with_suggested_rewrite(
        format!("relax param `{binder}` mode from `(own ...)` to `(borrow ...)`"),
        replacement,
    )
}

/// Iter 19a: clone of `inner` (assumed `Type::Fn`) with
/// `param_modes[i]` rewritten to `ParamMode::Borrow`. Other slots
/// are preserved bit-for-bit. Falls back to returning `inner`
/// unchanged if `inner` is not a `Type::Fn` (defensive — caller
/// should have screened this).
fn relax_param_to_borrow(inner: &Type, i: usize) -> Type {
    match inner {
        Type::Fn {
            params,
            param_modes,
            ret,
            ret_mode,
            effects,
        } => {
            // Materialise param_modes to full length so the relaxed
            // mode is positioned correctly even when the original
            // vec was elided to "all-implicit empty" (not the case
            // here — we only reach this for an `Own` slot — but
            // defensive).
            let mut new_modes: Vec<ParamMode> = (0..params.len())
                .map(|j| param_modes.get(j).copied().unwrap_or(ParamMode::Implicit))
                .collect();
            if i < new_modes.len() {
                new_modes[i] = ParamMode::Borrow;
            }
            Type::Fn {
                params: params.clone(),
                param_modes: new_modes,
                ret: ret.clone(),
                ret_mode: *ret_mode,
                effects: effects.clone(),
            }
        }
        other => other.clone(),
    }
}

/// Build a `consume-while-borrowed` diagnostic for `binder` in `def`.
/// Suggested rewrite: clone here so the original retains the borrow.
fn make_consume_while_borrowed(def: &str, binder: &str) -> Diagnostic {
    let replacement = term_to_form_a(&Term::Clone {
        value: Box::new(Term::Var { name: binder.to_string() }),
    });
    Diagnostic::error(
        "consume-while-borrowed",
        format!("`{binder}` is consumed while a borrow of it is still live"),
    )
    .with_def(def)
    .with_ctx(serde_json::json!({"binder": binder}))
    .with_suggested_rewrite(
        format!(
            "consume `(clone {binder})` here so the original keeps its outstanding borrow"
        ),
        replacement,
    )
}

#[cfg(test)]
mod tests {
    use super::*;
    use ailang_core::ast::{FnDef, Literal};

    fn fn_with_modes(name: &str, modes: Vec<ParamMode>, body: Term) -> Def {
        Def::Fn(FnDef {
            name: name.into(),
            ty: Type::Fn {
                params: modes
                    .iter()
                    .map(|_| Type::Con { name: "List".into(), args: vec![] })
                    .collect(),
                param_modes: modes.clone(),
                ret: Box::new(Type::int()),
                ret_mode: ParamMode::Implicit,
                effects: vec![],
            },
            params: (0..modes.len()).map(|i| format!("p{i}")).collect(),
            body,
            suppress: vec![],
            doc: None,
        })
    }

    /// All-Implicit fn → check is skipped, no diagnostics, even if the
    /// body would trigger a use-after-consume under explicit modes.
    #[test]
    fn implicit_fn_is_exempt() {
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes(
                "f",
                vec![ParamMode::Implicit],
                Term::Var { name: "p0".into() },
            )],
        };
        assert!(check_module(&m).is_empty());
    }

    /// Mixed Implicit + Borrow → still skipped (any Implicit disables
    /// the check entirely, per the activation gate).
    #[test]
    fn mixed_implicit_explicit_is_exempt() {
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes(
                "f",
                vec![ParamMode::Borrow, ParamMode::Implicit],
                Term::Lit { lit: Literal::Int { value: 0 } },
            )],
        };
        assert!(check_module(&m).is_empty());
    }

    /// All-explicit fn that NEVER uses its params, annotated `Borrow`:
    /// clean. (Pre-19a this test exercised the same shape with `Own`
    /// and asserted clean; 19a's `over-strict-mode` lint now fires on
    /// `Own` + zero-consume — moved into a dedicated positive test
    /// below. With `Borrow`, the lint does not apply.)
    #[test]
    fn explicit_fn_with_no_uses_is_clean() {
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes(
                "f",
                vec![ParamMode::Borrow],
                Term::Lit { lit: Literal::Int { value: 0 } },
            )],
        };
        assert!(check_module(&m).is_empty());
    }

    /// Iter 18d.1: a `(reuse-as 42 (Cons ...))` whose source is a literal
    /// (not a bare `Var`) is flagged with `reuse-as-source-not-bare-var`.
    /// The suggested rewrite drops the wrapper and keeps the body.
    #[test]
    fn reuse_as_with_non_var_source_is_reported() {
        // Body shape: (reuse-as 42 (term-ctor Wrap Wrap p0))
        // The source `42` is a literal — invalid for reuse-as.
        let body = Term::ReuseAs {
            source: Box::new(Term::Lit { lit: Literal::Int { value: 42 } }),
            body: Box::new(Term::Ctor {
                type_name: "Wrap".into(),
                ctor: "Wrap".into(),
                args: vec![Term::Var { name: "p0".into() }],
            }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
        };
        let diags = check_module(&m);
        assert_eq!(diags.len(), 1, "expected exactly one diagnostic, got {diags:?}");
        let d = &diags[0];
        assert_eq!(d.code, "reuse-as-source-not-bare-var");
        assert_eq!(d.def.as_deref(), Some("f"));
        assert_eq!(d.ctx, serde_json::json!({"got": "lit"}));
        assert!(
            !d.suggested_rewrites.is_empty(),
            "diagnostic should carry a suggested rewrite"
        );
        // The replacement must round-trip through parse_term.
        let rep = &d.suggested_rewrites[0].replacement;
        ailang_surface::parse_term(rep)
            .unwrap_or_else(|e| panic!("suggested rewrite must parse: {rep} ({e})"));
    }

    /// Iter 18d.1: a `(reuse-as p0 ...)` where `p0` was already
    /// consumed by an earlier sibling fires `use-after-consume` at the
    /// reuse-as site (not `reuse-as-source-not-bare-var`).
    #[test]
    fn reuse_as_after_consume_is_use_after_consume() {
        // Body shape: (seq p0 (reuse-as p0 (term-ctor Wrap Wrap p0)))
        // The first `p0` (in `seq.lhs`) consumes the binder; the
        // reuse-as in the rhs then sees an already-consumed binder.
        let body = Term::Seq {
            lhs: Box::new(Term::Var { name: "p0".into() }),
            rhs: Box::new(Term::ReuseAs {
                source: Box::new(Term::Var { name: "p0".into() }),
                body: Box::new(Term::Ctor {
                    type_name: "Wrap".into(),
                    ctor: "Wrap".into(),
                    args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
                }),
            }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
        };
        let diags = check_module(&m);
        assert_eq!(diags.len(), 1, "expected exactly one diagnostic, got {diags:?}");
        let d = &diags[0];
        assert_eq!(d.code, "use-after-consume");
        assert_eq!(d.ctx, serde_json::json!({"binder": "p0"}));
    }

    // ---- Iter 19a: over-strict-mode -----------------------------------

    use crate::diagnostic::Severity;

    /// Iter 19a, positive: a fn with `(own T)` whose body merely
    /// borrows the param via a `Borrow`-mode call → fires
    /// `over-strict-mode` (Warning) with binder=p0, current=own,
    /// suggested=borrow, and a non-empty rewrite.
    #[test]
    fn over_strict_mode_fires_when_param_only_borrowed() {
        // Module shape:
        //   (fn read (params (borrow (con List))) ... ) ; helper, body irrelevant
        //   (fn f    (params (own    (con List)))     ; over-strict
        //     body = (app read p0))
        let read_def = Def::Fn(FnDef {
            name: "read".into(),
            ty: Type::Fn {
                params: vec![Type::Con { name: "List".into(), args: vec![] }],
                param_modes: vec![ParamMode::Borrow],
                ret: Box::new(Type::int()),
                ret_mode: ParamMode::Implicit,
                effects: vec![],
            },
            params: vec!["xs".into()],
            body: Term::Lit { lit: Literal::Int { value: 0 } },
            suppress: vec![],
            doc: None,
        });
        let f_body = Term::App {
            callee: Box::new(Term::Var { name: "read".into() }),
            args: vec![Term::Var { name: "p0".into() }],
            tail: false,
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![read_def, fn_with_modes("f", vec![ParamMode::Own], f_body)],
        };
        let diags = check_module(&m);
        // Filter to over-strict-mode in case the helper triggers anything
        // (it shouldn't — `read` is `Borrow` and param is unused).
        let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect();
        assert_eq!(osm.len(), 1, "expected one over-strict-mode, got {diags:?}");
        let d = osm[0];
        assert_eq!(d.severity, Severity::Warning);
        assert_eq!(d.def.as_deref(), Some("f"));
        assert_eq!(
            d.ctx,
            serde_json::json!({
                "binder": "p0",
                "current_mode": "own",
                "suggested_mode": "borrow",
            })
        );
        assert!(
            !d.suggested_rewrites.is_empty(),
            "diagnostic should carry a suggested rewrite"
        );
        // The replacement is a fn-type, so it does not have to round-trip
        // through `parse_term` (which parses terms). We only assert it's
        // a non-empty string that mentions the relaxed `(borrow ...)`.
        let rep = &d.suggested_rewrites[0].replacement;
        assert!(
            rep.contains("(borrow"),
            "rewrite should mention `(borrow`; got {rep}"
        );
        assert!(
            !rep.contains("(own"),
            "rewrite should NOT contain the original `(own`; got {rep}"
        );
    }

    /// Iter 19a, negative: a fn with `(own T)` whose body consumes
    /// the param directly does not fire `over-strict-mode`.
    #[test]
    fn over_strict_mode_silent_when_body_consumes_param() {
        // Body: (seq p0 0) — `p0` is consumed in seq.lhs.
        let body = Term::Seq {
            lhs: Box::new(Term::Var { name: "p0".into() }),
            rhs: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
        };
        let diags = check_module(&m);
        assert!(
            !diags.iter().any(|d| d.code == "over-strict-mode"),
            "no over-strict-mode expected; got {diags:?}"
        );
    }

    /// Iter 19a, negative: a fn with `(borrow T)` and a borrowing
    /// body never fires `over-strict-mode` (the lint is gated on
    /// `Own`).
    #[test]
    fn over_strict_mode_silent_when_param_is_borrow() {
        // Body shape: literal — no use of the param at all.
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes(
                "f",
                vec![ParamMode::Borrow],
                Term::Lit { lit: Literal::Int { value: 0 } },
            )],
        };
        let diags = check_module(&m);
        assert!(
            !diags.iter().any(|d| d.code == "over-strict-mode"),
            "no over-strict-mode expected for borrow-mode param; got {diags:?}"
        );
    }

    /// Iter 19a.1, positive: a fn with `(own T)` whose body is
    /// `(match p0 ...)` and never consumes `p0` directly nor any of
    /// `p0`'s sub-binders DOES fire `over-strict-mode` under the
    /// precise sub-binder analysis. This is the test that 19a left
    /// pinned as a TODO marker; 19a.1 flipped it from a negative to
    /// a positive assertion.
    #[test]
    fn over_strict_mode_fires_when_match_arm_uses_no_sub_binder() {
        // Body: (match p0 ((pat-wild) 0))
        // — no sub-binders are bound; the param is only read.
        let body = Term::Match {
            scrutinee: Box::new(Term::Var { name: "p0".into() }),
            arms: vec![Arm {
                pat: Pattern::Wild,
                body: Term::Lit { lit: Literal::Int { value: 0 } },
            }],
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
        };
        let diags = check_module(&m);
        let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect();
        assert_eq!(
            osm.len(),
            1,
            "precise rule: expected one over-strict-mode warning when the body matches on `p0` and binds no sub-consume; got {diags:?}"
        );
        assert_eq!(osm[0].severity, Severity::Warning);
        assert_eq!(osm[0].def.as_deref(), Some("f"));
    }

    /// Iter 19a.1: helper to build an `IntList = Nil | Cons(Int,
    /// IntList)` ADT def. Used by the head_or_zero-shape tests
    /// (positive + negative variants below) so the lint can look up
    /// each ctor field's type and filter out primitives.
    fn intlist_typedef() -> Def {
        Def::Type(ailang_core::ast::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,
        })
    }

    /// Iter 19a.1: helper to build a fn whose single param is
    /// `(own IntList)` and whose body is `body`. Distinct from
    /// `fn_with_modes` (which uses a generic `List` type for params)
    /// so the test exercises a real ctor-field-types lookup.
    fn fn_own_intlist(name: &str, body: Term) -> Def {
        Def::Fn(FnDef {
            name: name.into(),
            ty: Type::Fn {
                params: vec![Type::Con { name: "IntList".into(), args: vec![] }],
                param_modes: vec![ParamMode::Own],
                ret: Box::new(Type::int()),
                ret_mode: ParamMode::Implicit,
                effects: vec![],
            },
            params: vec!["xs".into()],
            body,
            suppress: vec![],
            doc: None,
        })
    }

    /// Iter 19a.1, negative: a fn with `(own IntList)` whose body
    /// is `match xs { Cons(h, t) => t }` consumes the *heap-typed*
    /// pattern-binder `t`. The lint must NOT fire — the
    /// sub-consume forces ownership.
    #[test]
    fn over_strict_mode_silent_when_match_arm_consumes_sub_binder() {
        // Body: (match xs ((pat-ctor Cons (pat-var h) (pat-var t)) t))
        let body = Term::Match {
            scrutinee: Box::new(Term::Var { name: "xs".into() }),
            arms: vec![Arm {
                pat: Pattern::Ctor {
                    ctor: "Cons".into(),
                    fields: vec![
                        Pattern::Var { name: "h".into() },
                        Pattern::Var { name: "t".into() },
                    ],
                },
                body: Term::Var { name: "t".into() },
            }],
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![intlist_typedef(), fn_own_intlist("f", body)],
        };
        let diags = check_module(&m);
        assert!(
            !diags.iter().any(|d| d.code == "over-strict-mode"),
            "no over-strict-mode expected when a heap-typed arm-binder is consumed; got {diags:?}"
        );
    }

    /// Iter 19a.1, positive: a fn with `(own IntList)` whose body
    /// is `match xs { Nil => 0, Cons(h, t) => h }` returns the
    /// **primitive-typed** `h` (`Int`) and never moves the
    /// heap-typed `t`. The lint MUST fire — `(borrow IntList)`
    /// would have sufficed. This is exactly
    /// `rc_own_param_drop.head_or_zero`'s shape.
    #[test]
    fn over_strict_mode_fires_when_match_arm_binders_unused() {
        // Body: (match xs
        //         ((pat-ctor Nil) 0)
        //         ((pat-ctor Cons (pat-var h) (pat-var t)) h))
        let body = Term::Match {
            scrutinee: Box::new(Term::Var { name: "xs".into() }),
            arms: vec![
                Arm {
                    pat: Pattern::Ctor {
                        ctor: "Nil".into(),
                        fields: vec![],
                    },
                    body: Term::Lit { lit: Literal::Int { value: 0 } },
                },
                Arm {
                    pat: Pattern::Ctor {
                        ctor: "Cons".into(),
                        fields: vec![
                            Pattern::Var { name: "h".into() },
                            Pattern::Var { name: "t".into() },
                        ],
                    },
                    body: Term::Var { name: "h".into() },
                },
            ],
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![intlist_typedef(), fn_own_intlist("f", body)],
        };
        let diags = check_module(&m);
        let osm: Vec<_> = diags.iter().filter(|d| d.code == "over-strict-mode").collect();
        assert_eq!(
            osm.len(),
            1,
            "expected one over-strict-mode warning (head_or_zero shape); got {diags:?}"
        );
        assert_eq!(osm[0].severity, Severity::Warning);
        assert_eq!(osm[0].def.as_deref(), Some("f"));
        assert_eq!(
            osm[0].ctx,
            serde_json::json!({
                "binder": "xs",
                "current_mode": "own",
                "suggested_mode": "borrow",
            })
        );
    }
}