nova-hir 0.3.2

//! High-level IR for the Nova compiler.
//!
//! HIR is the *desugared, typed* representation produced by `nova-typeck`
//! from the AST and consumed by `nova-mir`:
//!
//! - every expression carries a [`Ty`] and a `Span`
//! - string interpolation is desugared to [`ExprKind::StrConcat`] over
//!   [`ExprKind::ToStr`] conversions
//! - compound assignment is desugared to a plain assign of a binary op
//! - names are resolved: locals are [`LocalId`], callees are [`Callee`]
//!
//! The [`Ty`] type also serves as the type representation used *during*
//! inference (it can contain [`Ty::Var`] inference variables); a fully
//! checked module contains no `Var` types.

use nova_diagnostics::Span;
use nova_resolver::{Builtin, DefId};

/// A type. This is the shared type representation across typeck, HIR and
/// monomorphization (spec `12-TYPESYSTEM.md` §3, trimmed to the Phase 1
/// feature set).
#[derive(Debug, Clone, PartialEq)]
pub enum Ty {
    /// 64-bit signed integer (the default integer type).
    Int,
    /// 64-bit float (the default float type).
    Float,
    Bool,
    Char,
    String,
    /// An immutable byte buffer.
    ///
    /// Structurally identical to [`Ty::String`] -- both are a `{len, ptr}` GC
    /// leaf header; a runtime-made value's bytes follow it inline in the same
    /// object, a `String` literal's are static data -- and semantically distinct:
    /// only `String` carries a UTF-8 guarantee. Nothing converts between them
    /// implicitly. This reaches codegen as the same opaque `MirTy::Ptr` every
    /// other heap pointer already lowers to, so neither backend needs an arm
    /// for it -- not because every operation on it is an intrinsic
    /// (`index_of`/`contains` in `std/bytes/lib.nova` are pure Nova control
    /// flow), but because codegen dispatches on MIR types, and `Ptr` is not
    /// new.
    Bytes,
    /// The unit type `()`.
    Unit,
    /// A function type `fn(A, B) -> R`.
    Fn {
        params: Vec<Ty>,
        ret: Box<Ty>,
    },
    /// A future produced by calling an `async fn`; the payload is the
    /// function's declared return type (the future's *output*).
    ///
    /// Compiler-constructed only: there is no surface syntax that builds one,
    /// and no impls may be written on it (`head()` returns `None`). At runtime
    /// it is the same 2-word fat pointer as a function value —
    /// `{ poll_code, state_ptr }` — which is why it sits beside `Ty::Fn` here
    /// rather than being a record in `std/core`. Nova has no lang-item
    /// mechanism: `Option` and `Result` are ordinary prelude sums the compiler
    /// does not know by name, so a std record could not be recognized.
    Future(Box<Ty>),
    /// A user-defined sum type with generic arguments.
    Sum {
        def_id: DefId,
        args: Vec<Ty>,
    },
    /// A user-defined record (struct) type with generic arguments.
    Record {
        def_id: DefId,
        args: Vec<Ty>,
    },
    /// A heap array `[T]` with elements of a single type.
    Array(Box<Ty>),
    /// A generic type parameter of the enclosing item (`T`).
    Param(u32),
    /// A projection onto a trait's associated type: `<on>::Name`, where
    /// `assoc` is the associated type's own `DefId` (see
    /// `DefKind::AssocType`).
    ///
    /// This is the one `Ty` variant that is **not** a type by itself — it is a
    /// *request* for one, answerable only with the impl table. It is therefore
    /// normalized away at three seams ([`normalize_ty`] called from typeck,
    /// `check_impl_conformance`, and `mono` after `subst`), and the unifier
    /// never has to decide a projection against a concrete type.
    ///
    /// `on` is `Param(k)` inside a generic body and a concrete type at an
    /// ordinary use site.
    ///
    /// **It can also be an unsolved `Var`, which the design doc §4.2 claims is
    /// unreachable.** That claim holds for the case it argues:
    /// `check_method_call` rejects an uninferred receiver with `E0011` before any
    /// return type is computed, so a *receiver's* projection is never on a `Var`.
    /// It does not hold for a generic call, where the type arguments are fresh
    /// variables that argument unification narrows as it goes — `fn f<I: It>(y:
    /// I::Item, x: I)` reaches the first parameter with `Assoc { on: Var(0) }`
    /// and nothing has solved `Var(0)` yet. `Checker::instantiate` applies the
    /// current substitution before normalizing, which covers every ordering where
    /// the determining argument comes first; the reverse order is a genuine
    /// (order-dependent) limitation of resolving at seams instead of deferring,
    /// and it reports an ordinary type mismatch naming the projection rather than
    /// anything worse.
    Assoc {
        on: Box<Ty>,
        assoc: DefId,
    },
    /// An unsolved inference variable (only during type checking).
    Var(u32),
    /// The never type `!` (return, panic); coerces to anything.
    Never,
    /// Placeholder after a type error, suppresses cascading errors.
    Error,
}

impl Ty {
    /// Substitute `Param(i)` with `args[i]`. Used for generic instantiation
    /// and monomorphization.
    pub fn subst(&self, args: &[Ty]) -> Ty {
        match self {
            Ty::Param(i) => args.get(*i as usize).cloned().unwrap_or(Ty::Error),
            Ty::Fn { params, ret } => Ty::Fn {
                params: params.iter().map(|p| p.subst(args)).collect(),
                ret: Box::new(ret.subst(args)),
            },
            Ty::Sum { def_id, args: a } => Ty::Sum {
                def_id: *def_id,
                args: a.iter().map(|t| t.subst(args)).collect(),
            },
            Ty::Record { def_id, args: a } => Ty::Record {
                def_id: *def_id,
                args: a.iter().map(|t| t.subst(args)).collect(),
            },
            Ty::Array(elem) => Ty::Array(Box::new(elem.subst(args))),
            Ty::Future(out) => Ty::Future(Box::new(out.subst(args))),
            Ty::Assoc { on, assoc } => Ty::Assoc {
                on: Box::new(on.subst(args)),
                assoc: *assoc,
            },
            other => other.clone(),
        }
    }

    /// Whether this type (transitively) mentions the generic parameter `idx`.
    pub fn mentions_param(&self, idx: u32) -> bool {
        match self {
            Ty::Param(k) => *k == idx,
            Ty::Fn { params, ret } => {
                params.iter().any(|p| p.mentions_param(idx)) || ret.mentions_param(idx)
            }
            Ty::Sum { args, .. } | Ty::Record { args, .. } => {
                args.iter().any(|a| a.mentions_param(idx))
            }
            Ty::Array(elem) => elem.mentions_param(idx),
            Ty::Future(out) => out.mentions_param(idx),
            Ty::Assoc { on, .. } => on.mentions_param(idx),
            _ => false,
        }
    }

    /// Whether this type (transitively) contains any generic `Param`.
    pub fn has_params(&self) -> bool {
        match self {
            Ty::Param(_) => true,
            Ty::Fn { params, ret } => params.iter().any(Ty::has_params) || ret.has_params(),
            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_params),
            Ty::Array(elem) => elem.has_params(),
            Ty::Future(out) => out.has_params(),
            Ty::Assoc { on, .. } => on.has_params(),
            _ => false,
        }
    }

    /// Whether this type (transitively) contains any inference variable.
    pub fn has_vars(&self) -> bool {
        match self {
            Ty::Var(_) => true,
            Ty::Fn { params, ret } => params.iter().any(Ty::has_vars) || ret.has_vars(),
            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_vars),
            Ty::Array(elem) => elem.has_vars(),
            Ty::Future(out) => out.has_vars(),
            Ty::Assoc { on, .. } => on.has_vars(),
            _ => false,
        }
    }

    /// Whether this type (transitively) contains an associated-type projection.
    ///
    /// Lets a caller ask "is there anything here for [`normalize_ty`] to do?"
    /// before paying for a normalization pass — and, more importantly, before
    /// taking a step that is only correct *because* a projection is present. The
    /// call seams in `nova-typeck` resolve their inference variables before
    /// normalizing, which they must not do to an ordinary signature type.
    pub fn has_assoc(&self) -> bool {
        match self {
            Ty::Assoc { .. } => true,
            Ty::Fn { params, ret } => params.iter().any(Ty::has_assoc) || ret.has_assoc(),
            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_assoc),
            Ty::Array(elem) => elem.has_assoc(),
            Ty::Future(out) => out.has_assoc(),
            _ => false,
        }
    }

    /// Whether this type (transitively) contains [`Ty::Error`].
    ///
    /// `Ty::Error` means "a diagnostic about this type has already been
    /// reported", and it behaves **oppositely at the two consumers** that read
    /// it. At `InferCtx::unify` it absorbs: it unifies with anything, so a
    /// poisoned type silently stops cascading. `Ty` derives `PartialEq` with no
    /// such absorption, so at a consumer that compares two types *directly* an
    /// `Error` on one side instead **forces** a mismatch, and the second
    /// diagnostic renders it as the meaningless `{error}`.
    ///
    /// This is for that second kind of consumer: it asks "is either side already
    /// poisoned?" so the comparison can be skipped rather than turned into
    /// noise. Transitive rather than a top-level `== Ty::Error` check because the
    /// poison is usually nested — an impl binding an unresolvable type makes the
    /// trait's `Option<Self::Item>` normalize to `Option<{error}>`, which is not
    /// itself `Ty::Error`.
    pub fn has_error(&self) -> bool {
        match self {
            Ty::Error => true,
            Ty::Fn { params, ret } => params.iter().any(Ty::has_error) || ret.has_error(),
            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_error),
            Ty::Array(elem) => elem.has_error(),
            Ty::Future(out) => out.has_error(),
            Ty::Assoc { on, .. } => on.has_error(),
            _ => false,
        }
    }

    /// The nominal head of this type, if it has one — used to key impl
    /// lookups. Generic arguments do not participate (Phase 1 has no
    /// overlapping impls per head).
    pub fn head(&self) -> Option<TyHead> {
        match self {
            Ty::Int => Some(TyHead::Int),
            Ty::Float => Some(TyHead::Float),
            Ty::Bool => Some(TyHead::Bool),
            Ty::Char => Some(TyHead::Char),
            Ty::String => Some(TyHead::String),
            Ty::Bytes => Some(TyHead::Bytes),
            Ty::Sum { def_id, .. } => Some(TyHead::Sum(*def_id)),
            Ty::Record { def_id, .. } => Some(TyHead::Record(*def_id)),
            _ => None,
        }
    }

    /// One-directional match: treat `self` as a pattern that may contain
    /// `Param(k)` and match it against the concrete `ground` type, recording
    /// each `Param(k)` → ground binding into `out` (grown as needed). A
    /// parameter seen twice must bind to the same type. Returns `false` on a
    /// structural mismatch. Used to recover a generic impl's type arguments
    /// from a concrete receiver type (e.g. `Box<T>` vs `Box<Int>` → `T=Int`).
    pub fn match_pattern(&self, ground: &Ty, out: &mut Vec<Option<Ty>>) -> bool {
        match (self, ground) {
            (Ty::Param(k), g) => {
                let k = *k as usize;
                if out.len() <= k {
                    out.resize(k + 1, None);
                }
                match &out[k] {
                    Some(existing) => existing == g,
                    None => {
                        out[k] = Some(g.clone());
                        true
                    }
                }
            }
            (
                Ty::Record {
                    def_id: d1,
                    args: a1,
                },
                Ty::Record {
                    def_id: d2,
                    args: a2,
                },
            )
            | (
                Ty::Sum {
                    def_id: d1,
                    args: a1,
                },
                Ty::Sum {
                    def_id: d2,
                    args: a2,
                },
            ) => {
                d1 == d2
                    && a1.len() == a2.len()
                    && a1.iter().zip(a2).all(|(p, g)| p.match_pattern(g, out))
            }
            (Ty::Array(e1), Ty::Array(e2)) => e1.match_pattern(e2, out),
            (Ty::Future(o1), Ty::Future(o2)) => o1.match_pattern(o2, out),
            (
                Ty::Fn {
                    params: p1,
                    ret: r1,
                },
                Ty::Fn {
                    params: p2,
                    ret: r2,
                },
            ) => {
                p1.len() == p2.len()
                    && p1.iter().zip(p2).all(|(a, b)| a.match_pattern(b, out))
                    && r1.match_pattern(r2, out)
            }
            (Ty::Assoc { on: p, assoc: pa }, Ty::Assoc { on: g, assoc: ga }) => {
                pa == ga && p.match_pattern(g, out)
            }
            // Primitives, `Unit`, etc.: match iff identical.
            (a, b) => a == b,
        }
    }
}

/// The nominal head of a type, used as the key for impl lookups
/// (spec `12-TYPESYSTEM.md` §5.2, `ImplTable` indexed by trait + type head).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum TyHead {
    Int,
    Float,
    Bool,
    Char,
    String,
    Bytes,
    Sum(DefId),
    Record(DefId),
}

/// A local variable slot within a function (parameters come first).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct LocalId(pub u32);

/// Metadata for one local variable.
#[derive(Debug, Clone)]
pub struct Local {
    pub name: String,
    pub ty: Ty,
    pub is_mut: bool,
    pub span: Span,
}

/// An `extern` function declaration: a C-ABI import with no Nova body. Only its
/// signature and (unmangled) C symbol name are needed to declare and call it.
#[derive(Debug, Clone)]
pub struct ExternFn {
    pub def_id: DefId,
    /// The raw C symbol to import and call (never mangled).
    pub symbol: String,
    pub params: Vec<Ty>,
    pub ret: Ty,
    /// Declaration site, for conflicting-signature diagnostics.
    pub span: Span,
}

/// A fully checked module: type layouts plus typed functions.
#[derive(Debug, Default)]
pub struct Module {
    pub sums: Vec<SumType>,
    pub records: Vec<RecordType>,
    pub traits: Vec<TraitDef>,
    pub impls: Vec<ImplInfo>,
    pub functions: Vec<Function>,
    /// `extern` (FFI) function declarations reachable in the program.
    pub externs: Vec<ExternFn>,
}

impl Module {
    /// Find the extern function declared under `def_id`, if any.
    pub fn extern_fn(&self, def_id: DefId) -> Option<&ExternFn> {
        self.externs.iter().find(|e| e.def_id == def_id)
    }

    /// Find the sum type declared under `def_id`, if any.
    pub fn sum(&self, def_id: DefId) -> Option<&SumType> {
        self.sums.iter().find(|s| s.def_id == def_id)
    }

    /// Find the record type declared under `def_id`, if any.
    pub fn record(&self, def_id: DefId) -> Option<&RecordType> {
        self.records.iter().find(|r| r.def_id == def_id)
    }

    /// Find the trait declared under `def_id`, if any.
    pub fn trait_def(&self, def_id: DefId) -> Option<&TraitDef> {
        self.traits.iter().find(|t| t.def_id == def_id)
    }

    /// Find the function declared under `def_id`, if any.
    pub fn function(&self, def_id: DefId) -> Option<&Function> {
        self.functions.iter().find(|f| f.def_id == def_id)
    }

    /// Resolve trait method `method` (index into the trait's methods) for a
    /// concrete self type to the compiled function it should dispatch to,
    /// paired with the type arguments that function must be instantiated with:
    ///
    /// - if the matching impl provides the method, dispatch to it, instantiated
    ///   with the impl's own type arguments recovered from `self_ty`
    ///   (`impl<T> Show for Box<T>` called on `Box<Int>` → `[Int]`);
    /// - otherwise dispatch to the trait's default body, which is generic over
    ///   `Self` → `[self_ty]`.
    ///
    /// Returns `None` if no impl of the trait fits `self_ty`.
    pub fn resolve_method_full(
        &self,
        trait_id: DefId,
        method: u32,
        self_ty: &Ty,
    ) -> Option<(DefId, Vec<Ty>)> {
        let tr = self.trait_def(trait_id)?;
        let method_name = &tr.methods.get(method as usize)?.name;
        let head = self_ty.head()?;
        // Among all impls of this trait for the head, select the one whose
        // self-type pattern actually fits — not merely the first sharing the
        // head. Coherence (no overlapping impls) guarantees at most one fits.
        let (imp, impl_args) = self
            .impls
            .iter()
            .filter(|i| i.trait_id == Some(trait_id) && i.self_head == head)
            .find_map(|i| i.match_args(self_ty).map(|args| (i, args)))?;
        if let Some((_, def)) = imp.methods.iter().find(|(n, _)| n == method_name) {
            Some((*def, impl_args))
        } else {
            let def = tr.methods[method as usize].default_def?;
            Some((def, vec![self_ty.clone()]))
        }
    }
}

/// How many resolutions deep one projection *chain* may go before
/// [`normalize_ty`] gives up.
///
/// Charged only where a projection is actually resolved, and passed *unchanged*
/// into the compound arms: a finite type is a finite tree, so recursion into
/// `Fn`/`Sum`/`Record`/`Array` cannot diverge, and charging it would reject a
/// legitimately deeply-nested type.
///
/// Two jobs, both load-bearing:
///
/// - It catches a **cycle**. `type Item = Self::Item` resolves to itself forever;
///   `type Item = [Self::Item]` grows a level each time, so a "have I seen this
///   exact projection" set would not catch it but a counter does.
/// - It bounds the **stack**, which is why it cannot simply be raised. Each
///   resolution costs a constant number of `normalize_within` frames, and a
///   growing binding nests one level deeper per step, so recursion depth tracks
///   this number. Measured: allowing 10 000 resolutions makes
///   `type Item = [Self::Item]` overflow a test thread's 2 MiB stack — a hard
///   crash, strictly worse than the diagnostic it replaced. 64 keeps the deepest
///   walk to a couple of hundred frames.
///
/// **64 is still the right number even though this limit is user-facing** (see
/// `Checker::normalize` — a non-cyclic chain of 64 links reports `E0078`, so this
/// is reachable from ordinary source and not merely a backstop for compiler
/// defects). Nova has no macros and no code generation, so every binding chain is
/// hand-written, and a hand-written one is one to three links; 64 is already
/// twenty times past the plausible. Raising it trades a limit nobody can reach by
/// accident for a stack overflow, which is the wrong trade.
///
/// It does **not** bound total work — see [`NORMALIZE_STEP_LIMIT`].
pub const NORMALIZE_DEPTH_LIMIT: u32 = 64;

/// How many nodes one whole [`normalize_ty`] walk may visit before giving up.
///
/// **The second of two allowances, because bounding chain depth does not bound
/// work.** [`NORMALIZE_DEPTH_LIMIT`]'s justification — "a finite type is a finite
/// tree, so compound recursion cannot diverge" — is sound and proves the wrong
/// thing: non-divergence is not bounded work. A *branching* binding chain
/// multiplies. With `type A(k) = Pair<Self::A(k+1), Self::A(k+1)>` terminating at
/// `type A(n) = Int` — no cycle, chain length `n`, every link far inside the depth
/// limit — the resolved type is itself `2^n` nodes, and each level pays for both
/// copies of the level below. Measured through `nova check` on programs it
/// *accepts*: n=16 → 716 ms, n=20 → 12.9 s, n=24 (a 60-line source file) → still
/// running after two minutes. A four-field record gives `4^n` in fewer lines.
///
/// So this counter is a single allowance shared by the entire walk, spent one step
/// per node, charged by **every** arm. That bounds total work by construction: at
/// most this many calls happen, so at most this many nodes are built.
///
/// Memoizing the projection lookups was the other candidate and does **not** fix
/// it: the *result* for `A(0)` is `2^n` nodes whatever the cache hit rate, so it
/// must still be materialized, and cloned into both branches at every level. Only
/// a cap on the result bounds the work, and a shared step counter is that cap.
///
/// 10 000 is three orders of magnitude past anything a person writes (std's
/// largest signature type is a handful of nodes), exhausts in microseconds when
/// something pathological hits it, and caps a resolved type at ~10 000 nodes. It
/// is deliberately *not* the same number as the depth limit: the units differ
/// (total nodes vs. resolutions along one chain), and 64 total nodes would reject
/// an ordinary projection-free type with 64 parts.
pub const NORMALIZE_STEP_LIMIT: u32 = 10_000;

/// Which of [`normalize_ty`]'s two allowances ran out. They fail on different
/// shapes and a user fixes them differently, so the diagnostic distinguishes
/// them: [`Depth`](Self::Depth) means a chain that does not terminate,
/// [`Steps`](Self::Steps) means one that terminates at an unreasonable size.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum NormalizeLimit {
    /// [`NORMALIZE_DEPTH_LIMIT`] — resolutions along one projection chain.
    Depth,
    /// [`NORMALIZE_STEP_LIMIT`] — nodes visited by the whole walk.
    Steps,
}

/// [`normalize_ty`] ran out of budget.
///
/// This is deliberately *not* folded into `Ty::Error`: `Error` unifies with
/// anything, so returning it would silently accept whatever the caller compared
/// the type against, turning a hang into a wrong answer. The caller must report
/// a diagnostic.
#[derive(Debug, Clone, PartialEq)]
pub struct NormalizeOverflow {
    /// The type [`normalize_ty`] was asked to resolve — the whole input, not the
    /// intermediate the walk happened to be on when the budget ran out.
    ///
    /// The intermediate is the wrong thing to name. On a linear chain
    /// `A0 → A1 → … → A64` it is `W::A64`, a rung the user never wrote, in the
    /// middle of a ladder they would have to count to find; the input is `W::A0`,
    /// which is the projection to go and look at. Depth-first exhaustion also
    /// makes *which* intermediate you land on an artifact of traversal order.
    pub at: Ty,
    /// Which allowance ran out.
    pub limit: NormalizeLimit,
}

/// Resolve every [`Ty::Assoc`] projection in `ty` that the impl table can
/// answer, leaving the rest untouched.
///
/// This is the shared core of all three normalization seams (see the design doc
/// §4.1): `nova-typeck` calls it where a checked type is consumed, and
/// monomorphization calls it after `subst`. It lives here, over a plain
/// `&[ImplInfo]` slice, because that is the one signature both callers can
/// satisfy — the `Checker` holds `impls` mid-construction and mono holds the
/// finished `Module::impls`.
///
/// **A projection is resolved when, and only when, its Self type has a
/// nominal [`Ty::head`]:**
///
/// - `Assoc { on: W<Int> }` resolves through the impl of the owning trait for
///   `W`, substituting the impl's own type arguments (recovered by
///   [`ImplInfo::match_args`]) into the bound type.
/// - `Assoc { on: Param(k) }` has no head and is returned unchanged. That is not
///   a failure: inside a generic body the projection is genuinely abstract until
///   monomorphization substitutes `Param(k)`.
/// - A projection with a head but no impl binding it is likewise returned
///   unchanged, so the caller's unification reports a type error that *names the
///   projection* rather than a normalizer that invented `Ty::Error`.
///
/// The impl is selected by the associated type's own `DefId`, which belongs to
/// exactly one associated type of exactly one trait. An impl binding that
/// `DefId` is therefore an impl of the owning trait by construction, and no
/// separate trait lookup (or `Definitions` access) is needed here.
///
/// The result is **re-normalized**, because a bound type may itself be a
/// projection: `type A = Self::B` with `type B = Int` must resolve all the way
/// to `Int`. That is what makes the step guard load-bearing rather than
/// paranoid — see [`NORMALIZE_STEP_LIMIT`].
pub fn normalize_ty(ty: &Ty, impls: &[ImplInfo]) -> Result<Ty, NormalizeOverflow> {
    let mut steps = NORMALIZE_STEP_LIMIT;
    // The inner walk reports only *which* allowance ran out; the type named in
    // the diagnostic is this call's input, not whichever intermediate depth-first
    // traversal happened to be on (see `NormalizeOverflow::at`).
    normalize_within(ty, impls, NORMALIZE_DEPTH_LIMIT, &mut steps).map_err(|limit| {
        NormalizeOverflow {
            at: ty.clone(),
            limit,
        }
    })
}

fn normalize_within(
    ty: &Ty,
    impls: &[ImplInfo],
    depth: u32,
    steps: &mut u32,
) -> Result<Ty, NormalizeLimit> {
    // Charged once per node by every arm, compound arms included, out of one
    // allowance shared by the whole walk. Charging only the `Assoc` arm is what
    // let a branching binding chain do exponential work without ever diverging —
    // see `NORMALIZE_STEP_LIMIT`. `depth`, by contrast, stays per-branch.
    *steps = steps.checked_sub(1).ok_or(NormalizeLimit::Steps)?;
    match ty {
        Ty::Assoc { on, assoc } => {
            let Some(depth) = depth.checked_sub(1) else {
                return Err(NormalizeLimit::Depth);
            };
            // The Self type may itself contain a projection, so resolve it
            // before asking it for a head.
            let on = normalize_within(on, impls, depth, steps)?;
            let Some(head) = on.head() else {
                return Ok(Ty::Assoc {
                    on: Box::new(on),
                    assoc: *assoc,
                });
            };
            // Sharing a head is not enough: an impl with a repeated or
            // partially-concrete self type (`impl<T> It for Pair<T, T>`) only
            // applies to Self types that genuinely fit it, which is what
            // `match_args` decides.
            let bound = impls.iter().filter(|i| i.self_head == head).find_map(|i| {
                let (_, bound) = i.assoc_bindings.iter().find(|(d, _)| d == assoc)?;
                let args = i.match_args(&on)?;
                Some(bound.subst(&args))
            });
            match bound {
                Some(bound) => normalize_within(&bound, impls, depth, steps),
                None => Ok(Ty::Assoc {
                    on: Box::new(on),
                    assoc: *assoc,
                }),
            }
        }
        Ty::Fn { params, ret } => Ok(Ty::Fn {
            params: params
                .iter()
                .map(|p| normalize_within(p, impls, depth, steps))
                .collect::<Result<_, _>>()?,
            ret: Box::new(normalize_within(ret, impls, depth, steps)?),
        }),
        Ty::Sum { def_id, args } => Ok(Ty::Sum {
            def_id: *def_id,
            args: args
                .iter()
                .map(|a| normalize_within(a, impls, depth, steps))
                .collect::<Result<_, _>>()?,
        }),
        Ty::Record { def_id, args } => Ok(Ty::Record {
            def_id: *def_id,
            args: args
                .iter()
                .map(|a| normalize_within(a, impls, depth, steps))
                .collect::<Result<_, _>>()?,
        }),
        Ty::Array(elem) => Ok(Ty::Array(Box::new(normalize_within(
            elem, impls, depth, steps,
        )?))),
        Ty::Future(out) => Ok(Ty::Future(Box::new(normalize_within(
            out, impls, depth, steps,
        )?))),
        Ty::Int
        | Ty::Float
        | Ty::Bool
        | Ty::Char
        | Ty::String
        | Ty::Bytes
        | Ty::Unit
        | Ty::Param(_)
        | Ty::Var(_)
        | Ty::Never
        | Ty::Error => Ok(ty.clone()),
    }
}

/// Whether two impl self-type patterns share a common ground instance — i.e.
/// the impls overlap and one concrete type could match both. `a` uses generic
/// parameters `0..a_generics`; `b`'s parameters are an independent namespace
/// `0..b_generics`. Exact: first-order unification with an occurs check, so
/// genuinely disjoint patterns (`Pair<Int, Bool>` vs `Pair<Int, String>`) are
/// never reported as overlapping, while a generic and a specific pattern
/// (`Box<T>` vs `Box<Int>`) are.
pub fn self_types_overlap(a: &Ty, a_generics: u32, b: &Ty, b_generics: u32) -> bool {
    // A projection's value is unknown until normalized, so assume it could
    // coincide with anything unless both sides are projections that provably
    // differ. A false E0074 is a loud error; a missed overlap is a silent
    // miscompile, so err toward overlap.
    match (a, b) {
        (Ty::Assoc { on: a1, assoc: x }, Ty::Assoc { on: b1, assoc: y }) => {
            x != y || self_types_overlap(a1, a_generics, b1, b_generics)
        }
        (Ty::Assoc { .. }, _) | (_, Ty::Assoc { .. }) => true,
        _ => {
            // Shift `b`'s parameters into a disjoint range so the two namespaces
            // do not collide in the shared substitution.
            let b = shift_params(b, a_generics);
            let mut subst: Vec<Option<Ty>> = vec![None; (a_generics + b_generics) as usize];
            unify_patterns(a, &b, &mut subst)
        }
    }
}

fn shift_params(t: &Ty, by: u32) -> Ty {
    match t {
        Ty::Param(k) => Ty::Param(k + by),
        Ty::Fn { params, ret } => Ty::Fn {
            params: params.iter().map(|p| shift_params(p, by)).collect(),
            ret: Box::new(shift_params(ret, by)),
        },
        Ty::Sum { def_id, args } => Ty::Sum {
            def_id: *def_id,
            args: args.iter().map(|a| shift_params(a, by)).collect(),
        },
        Ty::Record { def_id, args } => Ty::Record {
            def_id: *def_id,
            args: args.iter().map(|a| shift_params(a, by)).collect(),
        },
        Ty::Array(elem) => Ty::Array(Box::new(shift_params(elem, by))),
        Ty::Future(out) => Ty::Future(Box::new(shift_params(out, by))),
        other => other.clone(),
    }
}

/// Resolve `t` through the substitution one level (following a bound `Param`).
fn walk_param(t: &Ty, subst: &[Option<Ty>]) -> Ty {
    match t {
        Ty::Param(k) => match subst.get(*k as usize).and_then(|o| o.as_ref()) {
            Some(bound) => walk_param(bound, subst),
            None => t.clone(),
        },
        _ => t.clone(),
    }
}

fn occurs(k: u32, t: &Ty, subst: &[Option<Ty>]) -> bool {
    match walk_param(t, subst) {
        Ty::Param(j) => j == k,
        Ty::Fn { params, ret } => {
            params.iter().any(|p| occurs(k, p, subst)) || occurs(k, &ret, subst)
        }
        Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(|a| occurs(k, a, subst)),
        Ty::Array(elem) => occurs(k, &elem, subst),
        Ty::Future(out) => occurs(k, &out, subst),
        _ => false,
    }
}

fn unify_patterns(a: &Ty, b: &Ty, subst: &mut Vec<Option<Ty>>) -> bool {
    let a = walk_param(a, subst);
    let b = walk_param(b, subst);
    match (&a, &b) {
        (Ty::Param(i), Ty::Param(j)) if i == j => true,
        (Ty::Param(i), _) => {
            if occurs(*i, &b, subst) {
                return false;
            }
            subst[*i as usize] = Some(b.clone());
            true
        }
        (_, Ty::Param(j)) => {
            if occurs(*j, &a, subst) {
                return false;
            }
            subst[*j as usize] = Some(a.clone());
            true
        }
        (
            Ty::Record {
                def_id: d1,
                args: a1,
            },
            Ty::Record {
                def_id: d2,
                args: a2,
            },
        )
        | (
            Ty::Sum {
                def_id: d1,
                args: a1,
            },
            Ty::Sum {
                def_id: d2,
                args: a2,
            },
        ) => {
            d1 == d2
                && a1.len() == a2.len()
                && a1.iter().zip(a2).all(|(x, y)| unify_patterns(x, y, subst))
        }
        (Ty::Array(e1), Ty::Array(e2)) => unify_patterns(e1, e2, subst),
        (Ty::Future(o1), Ty::Future(o2)) => unify_patterns(o1, o2, subst),
        (
            Ty::Fn {
                params: p1,
                ret: r1,
            },
            Ty::Fn {
                params: p2,
                ret: r2,
            },
        ) => {
            p1.len() == p2.len()
                && p1.iter().zip(p2).all(|(x, y)| unify_patterns(x, y, subst))
                && unify_patterns(r1, r2, subst)
        }
        // Primitives, `Unit`, `Error`: overlap iff identical.
        (x, y) => x == y,
    }
}

/// A trait declaration with its method signatures.
#[derive(Debug, Clone)]
pub struct TraitDef {
    pub def_id: DefId,
    pub name: String,
    /// Traits this one requires (`trait Ord: Eq` → `[Eq]`), resolved and
    /// deduplicated. Direct supertraits only — the transitive closure is taken
    /// where it is needed, so a cyclic declaration cannot make this list
    /// infinite.
    ///
    /// The graph formed by these lists **can itself be cyclic**: `trait A: B`
    /// together with `trait B: A` is accepted (`nova-typeck` only ever
    /// requires satisfiability, not acyclicity). A transitive walk over this
    /// field — chasing `supertraits` into each named trait's own
    /// `supertraits`, and so on — must therefore track which traits it has
    /// already visited, or it will loop forever on such a declaration. (The
    /// existing transitive expansion in `nova-typeck` does this by construction:
    /// it only ever appends an id it has not already recorded.)
    pub supertraits: Vec<DefId>,
    pub methods: Vec<TraitMethod>,
    /// Associated types this trait declares, in declaration order, each with
    /// its own `DefId` (`DefKind::AssocType`). An impl must bind every one of
    /// them; `check_impl_conformance` enforces that.
    pub assoc_types: Vec<(String, DefId)>,
}

/// One method of a trait. In `params`/`ret`, `Ty::Param(0)` denotes `Self` and
/// `Ty::Param(1..=generics)` the method's own generic parameters (a generic
/// method like `fn map<U>(self, …)`). `params` never itself contains a
/// `self` entry: when the method declares a `self` receiver it is implicit
/// rather than stored here, but a trait method need not declare one at all
/// (e.g. `fn zero() -> Int`), in which case `params` is just its declared
/// parameters.
#[derive(Debug, Clone)]
pub struct TraitMethod {
    pub name: String,
    pub params: Vec<Ty>,
    pub ret: Ty,
    /// Whether the method declares a `self` receiver. A method without one is
    /// an associated function, called as `Type::name(…)` with no receiver —
    /// never as `value.name(…)`. `params` looks the same either way (`self` is
    /// never stored in it), so this flag is the only record of the difference,
    /// and dispatch that ignores it lowers a receiver argument into a callee
    /// that has no slot for it.
    pub has_self: bool,
    /// Whether the `self` receiver is declared `mut`, i.e. whether the method is
    /// a mutator whose callers must supply a mutable receiver place (`E0060`,
    /// ADR 0005 §1). Meaningless when `has_self` is false, and the conformance
    /// check that compares this against the impl's own `mut` runs only after the
    /// two agree about `has_self` at all.
    ///
    /// It has to live here rather than being read off the impl: trait dispatch
    /// resolves to `(trait_id, method_index)`, and for a generic receiver
    /// (`fn f<T: Tr>(mut x: T) { x.m() }`) there is no single impl whose
    /// receiver declaration could be consulted. `params` cannot carry it either
    /// — `method_sig_parts` strips a `self` parameter whether or not it is
    /// `mut`, so the flag is the only record, exactly as `has_self` is the only
    /// record of the receiver's presence.
    pub mut_self: bool,
    /// Number of the method's own generic parameters (not counting `Self`).
    pub generics: u32,
    /// Trait bounds per method generic parameter (indexed `0..generics`).
    pub bounds: Vec<Vec<DefId>>,
    /// The compiled default-body function, if the trait provides a default.
    pub default_def: Option<DefId>,
}

/// One `impl` block: an inherent impl (`trait_id: None`) or a trait impl.
#[derive(Debug, Clone)]
pub struct ImplInfo {
    pub trait_id: Option<DefId>,
    /// The nominal head of the self type — the impl-table lookup key.
    pub self_head: TyHead,
    /// The impl's self type, with `Param(k)` standing for the impl's k-th
    /// generic parameter (e.g. `Box<Param(0)>` for `impl<T> … for Box<T>`).
    /// A non-generic impl's self type contains no `Param`.
    pub self_ty: Ty,
    /// Number of generic parameters the impl introduces.
    pub generics: u32,
    /// Trait bounds on each impl generic parameter (`impl<T: Bound>`), indexed
    /// by parameter position — empty for an unconstrained or non-generic impl.
    pub bounds: Vec<Vec<DefId>>,
    /// `(method name, compiled method function DefId)` for methods this
    /// impl defines directly.
    pub methods: Vec<(String, DefId)>,
    /// Associated types this impl binds, keyed by the associated type's own
    /// `DefId` (`DefKind::AssocType`, the same id `TraitDef::assoc_types`
    /// carries). The bound type may contain the impl's `Param(k)`, so
    /// normalization must substitute the impl's arguments before using it.
    ///
    /// Empty for an inherent impl: only a trait declares associated types, so
    /// only a trait impl can bind one.
    pub assoc_bindings: Vec<(DefId, Ty)>,
}

impl ImplInfo {
    /// Recover this impl's type arguments (in `Param` order) from a concrete
    /// self type. Returns `None` when the self type does not actually match the
    /// impl's self-type pattern — sharing a head is not enough, so an impl with
    /// a repeated (`Pair<T, T>`) or partially-concrete (`Pair<Int, T>`) self
    /// type only applies to receivers that genuinely fit it. A parameter the
    /// pattern does not mention resolves to `Ty::Error` (an unconstrained,
    /// unused impl generic, which never reaches code).
    pub fn match_args(&self, concrete: &Ty) -> Option<Vec<Ty>> {
        let mut out: Vec<Option<Ty>> = Vec::new();
        if !self.self_ty.match_pattern(concrete, &mut out) {
            return None;
        }
        Some(
            (0..self.generics as usize)
                .map(|i| out.get(i).cloned().flatten().unwrap_or(Ty::Error))
                .collect(),
        )
    }
}

/// A record (struct) declaration with typed fields.
#[derive(Debug, Clone)]
pub struct RecordType {
    pub def_id: DefId,
    pub name: String,
    /// Number of generic parameters.
    pub generics: u32,
    pub fields: Vec<RecordField>,
}

/// One field of a record; the type may reference `Ty::Param`.
#[derive(Debug, Clone)]
pub struct RecordField {
    pub name: String,
    pub ty: Ty,
}

/// A sum type declaration with typed variant payloads.
#[derive(Debug, Clone)]
pub struct SumType {
    pub def_id: DefId,
    pub name: String,
    /// Number of generic parameters.
    pub generics: u32,
    pub variants: Vec<Variant>,
}

/// One variant of a sum type; field types may reference `Ty::Param`.
#[derive(Debug, Clone)]
pub struct Variant {
    pub name: String,
    pub fields: Vec<Ty>,
}

/// A typed function.
#[derive(Debug)]
pub struct Function {
    pub def_id: DefId,
    pub name: String,
    /// Number of generic parameters; generic functions are monomorphized
    /// before codegen.
    pub generics: u32,
    /// Trait bounds per generic parameter (`bounds[i]` are the trait
    /// `DefId`s the i-th parameter must satisfy). Checked at
    /// monomorphization once the concrete type argument is known.
    pub bounds: Vec<Vec<DefId>>,
    /// Whether this function is the code of a function value (a closure or
    /// a bare-fn wrapper). Such functions take a leading environment
    /// pointer in their ABI: `(env_ptr, params...)`. Normal, directly
    /// called functions do not.
    pub takes_env: bool,
    /// For a closure, the number of leading `locals` that are captured
    /// variables loaded from the environment at entry (0 for a bare-fn
    /// wrapper). The captured locals precede the real parameters.
    pub capture_count: u32,
    /// The first `params` entries of `locals` are the real parameters
    /// (after any captures). For a closure the captured locals occupy
    /// indices `0..capture_count` and the parameters `capture_count..`.
    pub params: u32,
    pub locals: Vec<Local>,
    pub ret_ty: Ty,
    /// Whether this function was declared `async`. `ret_ty` is already
    /// `Ty::Future(output)` when true; this flag is what tells `nova-mir`
    /// which functions to treat specially, since a non-async function may
    /// also return a `Future` (by calling an async fn and not awaiting it),
    /// so `ret_ty` alone can't distinguish them — which is the whole reason
    /// this flag exists rather than a test on `ret_ty`'s shape.
    ///
    /// What `nova-mir` does with it is that crate's contract
    /// (`nova-mir/src/async_lower.rs`), not restated here, for the reason
    /// [`ExprKind::Await`]'s doc gives.
    pub is_async: bool,
    pub body: Expr,
    pub span: Span,
}

/// A typed expression.
#[derive(Debug, Clone)]
pub struct Expr {
    pub kind: ExprKind,
    pub ty: Ty,
    pub span: Span,
}

/// What a call dispatches to.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Callee {
    /// A top-level function.
    Def(DefId),
    /// A compiler builtin.
    Builtin(Builtin),
    /// An indirect call through a fn-typed local.
    Local(LocalId),
}

/// Binary operators after type checking (operand types are known).
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum BinOp {
    Add,
    Sub,
    Mul,
    Div,
    Rem,
    Eq,
    Ne,
    Lt,
    Le,
    Gt,
    Ge,
    BitAnd,
    BitOr,
    BitXor,
    Shl,
    Shr,
}

/// Unary operators.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum UnOp {
    /// Numeric negation.
    Neg,
    /// Boolean not.
    Not,
    /// Bitwise not (Int).
    BitNot,
}

/// Expression kinds. Desugared relative to the AST: no string interpolation,
/// no compound assignment, no `for` (Phase 1 defers iterators).
#[derive(Debug, Clone)]
pub enum ExprKind {
    IntLit(i64),
    FloatLit(f64),
    BoolLit(bool),
    StrLit(String),
    CharLit(char),
    /// The unit value `()`.
    Unit,
    /// Read a local variable.
    Local(LocalId),
    /// Build a function value (fat pointer `{ code, env }`). `func` is the
    /// code function (a closure body or a bare-fn wrapper), instantiated
    /// with `type_args`; `captures` are the environment's values in order
    /// (empty for a bare-fn wrapper).
    MakeClosure {
        func: DefId,
        type_args: Vec<Ty>,
        captures: Vec<Expr>,
    },
    /// Call a function. `type_args` instantiate the callee's generics when
    /// `func` is `Callee::Def`.
    Call {
        func: Callee,
        type_args: Vec<Ty>,
        args: Vec<Expr>,
    },
    /// Construct a sum type variant. The expression's `ty` carries the
    /// concrete `Sum { args, .. }` instantiation.
    MakeVariant {
        sum: DefId,
        variant: u32,
        args: Vec<Expr>,
    },
    /// Construct a record value. `fields` are in the record's declared
    /// field order; the expression's `ty` is the `Record { args, .. }`
    /// instantiation.
    MakeRecord {
        record: DefId,
        fields: Vec<Expr>,
    },
    /// Read field `index` of a record value.
    FieldGet {
        target: Box<Expr>,
        index: u32,
    },
    /// Store `record.field = value`. `index` is the field's position, so the
    /// store offset is `8 * index` — the same layout `FieldGet` reads.
    /// Unit-typed.
    FieldSet {
        target: Box<Expr>,
        index: u32,
        value: Box<Expr>,
    },
    /// Construct a heap array `{ len, elems... }`; the expression's `ty`
    /// is the `Array(elem)` type.
    MakeArray {
        elems: Vec<Expr>,
    },
    /// `[init; len]` — a heap array of `len` slots, every one holding `init`,
    /// where `len` is a runtime `Int`. Unlike `MakeArray` the element count is
    /// not known statically, so MIR lowering allocates and then fills with a
    /// loop. The expression's `ty` is the `Array(elem)` type.
    ///
    /// `init` is evaluated **once**, and that single value is stored into every
    /// slot — these are not `len` copies. For a heap element type the slots are
    /// therefore one object rather than `len` objects: `[Vec::new(); 2]` is a
    /// single `Vec` in both slots, so a `push` through one is visible through
    /// the other. That follows from Nova's reference semantics (there is no
    /// `Copy` and no clone to insert per slot), and
    /// `tests/runtime/array_repeat.nova` executes the case so a change to
    /// per-slot evaluation cannot happen silently.
    ArrayRepeat {
        init: Box<Expr>,
        len: Box<Expr>,
    },
    /// Read `target[index]` (bounds-checked). `target` is an array.
    Index {
        target: Box<Expr>,
        index: Box<Expr>,
    },
    /// Assign `target[index] = value` (bounds-checked); unit-typed.
    IndexSet {
        target: Box<Expr>,
        index: Box<Expr>,
        value: Box<Expr>,
    },
    /// The length of an array (`arr.len()`).
    ArrayLen {
        target: Box<Expr>,
    },
    /// A trait method call, resolved to a concrete impl during monomorphization
    /// (static dispatch). `self_ty` is the `Self` type — concrete for a call on
    /// a known type, or `Param(k)` inside a generic function (dispatch through
    /// that parameter's bound) until substitution makes it concrete.
    TraitCall {
        trait_id: DefId,
        method: u32,
        self_ty: Ty,
        /// The method's own generic arguments (`Param(1..)`), inferred per call
        /// site; empty for a non-generic trait method.
        type_args: Vec<Ty>,
        /// The receiver of `receiver.method(args)`, or `None` for a trait
        /// associated function called as `Type::method(args)` — one that
        /// declares no `self` (see [`TraitMethod::has_self`]). `None` rather
        /// than a flag beside a placeholder expression so that lowering a
        /// receiver that does not exist is not representable: there is nothing
        /// to lower, so no consumer can accidentally pass one.
        receiver: Option<Box<Expr>>,
        args: Vec<Expr>,
    },
    /// A non-short-circuit binary operation.
    Binary {
        op: BinOp,
        lhs: Box<Expr>,
        rhs: Box<Expr>,
    },
    /// Short-circuit `&&`.
    LogicalAnd {
        lhs: Box<Expr>,
        rhs: Box<Expr>,
    },
    /// Short-circuit `||`.
    LogicalOr {
        lhs: Box<Expr>,
        rhs: Box<Expr>,
    },
    Unary {
        op: UnOp,
        expr: Box<Expr>,
    },
    /// `let` binding as a unit-typed statement expression.
    Let {
        local: LocalId,
        init: Box<Expr>,
    },
    /// Assignment to a mutable local; unit-typed.
    Assign {
        local: LocalId,
        value: Box<Expr>,
    },
    /// `{ stmts; trailing }` — value is `trailing` or unit.
    Block {
        stmts: Vec<Expr>,
        trailing: Option<Box<Expr>>,
    },
    If {
        cond: Box<Expr>,
        then: Box<Expr>,
        else_: Option<Box<Expr>>,
    },
    While {
        cond: Box<Expr>,
        body: Box<Expr>,
    },
    /// Exit the innermost enclosing loop; diverging (`Never`).
    Break,
    /// Skip to the next iteration of the innermost loop; diverging.
    Continue,
    Match {
        scrutinee: Box<Expr>,
        arms: Vec<Arm>,
    },
    Return(Option<Box<Expr>>),
    /// Convert a primitive to `String` (from string interpolation).
    ToStr(Box<Expr>),
    /// Concatenate `String` parts (from string interpolation).
    StrConcat(Vec<Expr>),
    /// `e.await` inside an `async fn`. `e` has type `Future<T>` and the
    /// `Await` expression has type `T`.
    ///
    /// Only ever appears inside an `async fn`'s body, which `nova-typeck`'s
    /// `fcx.in_async` is what enforces — so nothing downstream needs a guard
    /// against one outside a function that is [`Function::is_async`].
    ///
    /// What this node becomes is `nova-mir`'s: `lower.rs` emits a `Stmt::Await`
    /// marker and `async_lower.rs`'s block split turns that into suspend/resume
    /// control flow. **Deliberately not described further here.** A description
    /// of another crate's behaviour, kept in this one, goes false the moment that
    /// behaviour changes and has nothing to keep it honest — so this doc holds
    /// only the two facts above, both of which are about this node and this
    /// crate, and `nova-mir`'s own docs carry the contract.
    Await(Box<Expr>),
}

/// One `match` arm.
#[derive(Debug, Clone)]
pub struct Arm {
    pub pattern: Pattern,
    pub body: Expr,
    pub span: Span,
}

/// Patterns after checking. Phase 1 supports flat patterns: variant
/// destructuring binds directly to locals (or discards with `None`).
#[derive(Debug, Clone)]
pub enum Pattern {
    /// `_`
    Wildcard,
    /// A catch-all binding: `n => ...`
    Bind(LocalId),
    LitInt(i64),
    LitBool(bool),
    LitStr(String),
    /// `Variant(a, _, c)` — one binder slot per payload field.
    Variant {
        sum: DefId,
        variant: u32,
        binders: Vec<Option<LocalId>>,
    },
}

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

    #[test]
    fn subst_recurses_into_a_projection_without_normalizing() {
        use nova_resolver::DefId;
        let proj = Ty::Assoc {
            on: Box::new(Ty::Param(0)),
            assoc: DefId(7),
        };
        // subst has no impl table, so it substitutes and stops. Normalizing is
        // the caller's job (typeck's `normalize`, or mono after subst).
        assert_eq!(
            proj.subst(&[Ty::Int]),
            Ty::Assoc {
                on: Box::new(Ty::Int),
                assoc: DefId(7)
            }
        );
    }

    #[test]
    fn a_projection_has_no_head_and_no_param_of_its_own() {
        use nova_resolver::DefId;
        let proj = Ty::Assoc {
            on: Box::new(Ty::Param(2)),
            assoc: DefId(7),
        };
        // No head: impl lookup cannot key on an unnormalized projection.
        assert!(proj.head().is_none());
        // But it does mention the parameter in its Self type, which
        // `E0073`'s unused-impl-parameter check depends on.
        assert!(proj.mentions_param(2));
        assert!(!proj.mentions_param(0));
    }

    #[test]
    fn a_projection_reports_the_params_and_vars_inside_its_self_type() {
        use nova_resolver::DefId;
        let on_param = Ty::Assoc {
            on: Box::new(Ty::Param(0)),
            assoc: DefId(7),
        };
        assert!(on_param.has_params(), "a projection on a Param is generic");
        assert!(!on_param.has_vars());

        let on_var = Ty::Assoc {
            on: Box::new(Ty::Var(3)),
            assoc: DefId(7),
        };
        // Assoc-on-Var is meant to be unreachable (E0011 fires first), but
        // typeck's finalize checks are the net for that argument being wrong,
        // and they are driven by has_vars.
        assert!(
            on_var.has_vars(),
            "a projection on a Var still contains a var"
        );
        assert!(!on_var.has_params());

        let concrete = Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: DefId(7),
        };
        assert!(!concrete.has_params());
        assert!(!concrete.has_vars());
    }

    // `self_types_overlap`'s two new arms, mutation-tested: the reviewer
    // found that mutating this function to unconditional `false` (the
    // silent-miscompile direction the design doc warns about) left the full
    // workspace suite green before this test existed.
    #[test]
    fn self_types_overlap_treats_a_projection_conservatively() {
        use nova_resolver::DefId;
        let item = DefId(7);
        let other = DefId(8);

        // Same associated type, Self types that provably differ: no overlap.
        let on_int = Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: item,
        };
        let on_bool = Ty::Assoc {
            on: Box::new(Ty::Bool),
            assoc: item,
        };
        assert!(
            !self_types_overlap(&on_int, 0, &on_bool, 0),
            "same associated type, but Int and Bool can never be the same Self type"
        );

        // Same associated type, Self types that could unify (a generic
        // parameter against a concrete type): overlap.
        let on_param = Ty::Assoc {
            on: Box::new(Ty::Param(0)),
            assoc: item,
        };
        assert!(
            self_types_overlap(&on_param, 1, &on_int, 0),
            "Param(0) can be instantiated to Int, so these can coincide"
        );

        // Different associated types: nothing is known about either, so the
        // conservative answer is still overlap.
        let other_assoc = Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: other,
        };
        assert!(
            self_types_overlap(&on_int, 0, &other_assoc, 0),
            "different associated types cannot be proven disjoint, so assume overlap"
        );

        // A projection against a non-projection: always assumed to overlap,
        // in both argument orders.
        assert!(self_types_overlap(&on_int, 0, &Ty::Int, 0));
        assert!(self_types_overlap(&Ty::Bool, 0, &on_int, 0));
    }

    // `match_pattern`'s new arm, mutation-tested: the reviewer found that
    // mutating it to unconditional `false` also left the full workspace
    // suite green before this test existed.
    #[test]
    fn match_pattern_treats_assoc_structurally() {
        use nova_resolver::DefId;
        let item = DefId(7);
        let other = DefId(8);

        // Same associated type: the Self-type pattern matches structurally
        // and records its Param binding like any other position.
        let pattern = Ty::Assoc {
            on: Box::new(Ty::Param(0)),
            assoc: item,
        };
        let ground = Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: item,
        };
        let mut out = Vec::new();
        assert!(pattern.match_pattern(&ground, &mut out));
        assert_eq!(out, vec![Some(Ty::Int)]);

        // Different associated types: never a match, even with identical
        // Self types.
        let different_assoc = Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: other,
        };
        let same_self = Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: item,
        };
        assert!(!same_self.match_pattern(&different_assoc, &mut Vec::new()));

        // A projection on only one side is a structural mismatch, not a
        // partial match, in both argument orders.
        assert!(!pattern.match_pattern(&Ty::Int, &mut Vec::new()));
        assert!(!Ty::Int.match_pattern(&ground, &mut Vec::new()));
    }

    #[test]
    fn has_assoc_finds_a_projection_at_every_nesting_depth() {
        use nova_resolver::DefId;
        let p = || Ty::Assoc {
            on: Box::new(Ty::Int),
            assoc: DefId(7),
        };
        assert!(p().has_assoc());
        assert!(Ty::Array(Box::new(p())).has_assoc());
        assert!(
            Ty::Future(Box::new(p())).has_assoc(),
            "a future's output counts too, not only an array's element"
        );
        assert!(
            Ty::Record {
                def_id: DefId(1),
                args: vec![Ty::Bool, p()],
            }
            .has_assoc(),
            "not only the first argument"
        );
        assert!(Ty::Sum {
            def_id: DefId(1),
            args: vec![p()],
        }
        .has_assoc());
        assert!(
            Ty::Fn {
                params: vec![Ty::Int],
                ret: Box::new(p()),
            }
            .has_assoc(),
            "the return type counts, not only the parameters"
        );
        assert!(Ty::Fn {
            params: vec![p()],
            ret: Box::new(Ty::Int),
        }
        .has_assoc());
        // And says no when there is genuinely nothing to normalize, including
        // for the compound types it recurses into.
        assert!(!Ty::Int.has_assoc());
        assert!(!Ty::Param(0).has_assoc());
        assert!(!Ty::Array(Box::new(Ty::Int)).has_assoc());
        assert!(!Ty::Future(Box::new(Ty::Int)).has_assoc());
        assert!(!Ty::Fn {
            params: vec![Ty::Int],
            ret: Box::new(Ty::Bool),
        }
        .has_assoc());
    }

    #[test]
    fn future_recurses_into_its_output_type() {
        // Each predicate must look THROUGH the Future, not past it. A `_ => false`
        // catch-all would pass a test that only ever asked about Future<Int>.
        let p = || Ty::Param(0);
        assert!(Ty::Future(Box::new(p())).has_params());
        assert!(!Ty::Future(Box::new(Ty::Int)).has_params());
        assert!(Ty::Future(Box::new(Ty::Var(0))).has_vars());
        assert!(!Ty::Future(Box::new(Ty::Int)).has_vars());
        assert!(Ty::Future(Box::new(Ty::Error)).has_error());
        assert!(!Ty::Future(Box::new(Ty::Int)).has_error());
        assert!(Ty::Future(Box::new(p())).mentions_param(0));
        assert!(!Ty::Future(Box::new(p())).mentions_param(1));
    }

    #[test]
    fn future_substitutes_its_output_type() {
        let subbed = Ty::Future(Box::new(Ty::Param(0))).subst(&[Ty::Float]);
        assert_eq!(subbed, Ty::Future(Box::new(Ty::Float)));
    }

    #[test]
    fn future_match_pattern_binds_through_the_output() {
        // Recovers T from Future<T> against a concrete Future<Bool>.
        let mut out = Vec::new();
        assert!(Ty::Future(Box::new(Ty::Param(0)))
            .match_pattern(&Ty::Future(Box::new(Ty::Bool)), &mut out));
        assert_eq!(out, vec![Some(Ty::Bool)]);
        // And refuses a structural mismatch rather than binding anything.
        let mut out2 = Vec::new();
        assert!(!Ty::Future(Box::new(Ty::Param(0)))
            .match_pattern(&Ty::Array(Box::new(Ty::Bool)), &mut out2));
    }

    // === normalize_ty ===

    /// `impl<generics> ? for self_ty { type <assoc> = <bound> }` — the minimum
    /// an `ImplInfo` needs to be for `normalize_ty` to read it. `trait_id` is
    /// deliberately `None` on some of these: `normalize_ty` keys on the
    /// associated type's own `DefId`, which belongs to exactly one trait, so it
    /// never has to consult `trait_id` — and a test that set it would hide a
    /// lookup that secretly depended on it.
    fn imp(self_ty: Ty, generics: u32, bindings: Vec<(DefId, Ty)>) -> ImplInfo {
        ImplInfo {
            trait_id: None,
            self_head: self_ty.head().expect("test self types have a head"),
            self_ty,
            generics,
            bounds: Vec::new(),
            methods: Vec::new(),
            assoc_bindings: bindings,
        }
    }

    fn rec(def: u32, args: Vec<Ty>) -> Ty {
        Ty::Record {
            def_id: DefId(def),
            args,
        }
    }

    fn proj(on: Ty, assoc: u32) -> Ty {
        Ty::Assoc {
            on: Box::new(on),
            assoc: DefId(assoc),
        }
    }

    const ITEM: u32 = 7;

    #[test]
    fn normalize_resolves_a_projection_through_the_impls_own_arguments() {
        // `impl<T> It for W<T> { type Item = T }`, projected onto `W<Int>`.
        let impls = [imp(
            rec(1, vec![Ty::Param(0)]),
            1,
            vec![(DefId(ITEM), Ty::Param(0))],
        )];
        assert_eq!(
            normalize_ty(&proj(rec(1, vec![Ty::Int]), ITEM), &impls),
            Ok(Ty::Int)
        );
    }

    #[test]
    fn normalize_picks_the_impl_whose_self_type_matches() {
        // Two impls binding the *same* associated type on different heads. With
        // only one impl in the table, "looks the impl up" and "takes the only
        // impl" are indistinguishable.
        let impls = [
            imp(
                rec(1, vec![Ty::Param(0)]),
                1,
                vec![(DefId(ITEM), Ty::Param(0))],
            ),
            imp(rec(2, vec![]), 0, vec![(DefId(ITEM), Ty::Bool)]),
        ];
        assert_eq!(
            normalize_ty(&proj(rec(1, vec![Ty::Char]), ITEM), &impls),
            Ok(Ty::Char),
            "W<Char>::Item comes from the W impl"
        );
        assert_eq!(
            normalize_ty(&proj(rec(2, vec![]), ITEM), &impls),
            Ok(Ty::Bool),
            "K::Item comes from the K impl"
        );
    }

    #[test]
    fn normalize_rejects_an_impl_that_shares_the_head_but_does_not_fit() {
        // Two impls on the SAME head, one structurally non-matching:
        // `impl<T> It for Pair<T, T>` does not cover `Pair<Int, Bool>`, so the
        // projection must resolve through `impl It for Pair<Int, Bool>` instead.
        //
        // This is the only test of the `match_args` gate that a head-only
        // implementation fails. `normalize_picks_the_impl_whose_self_type_matches`
        // and `normalize_recurses_into_every_compound_type` both discriminate by
        // *head* alone, so dropping the gate (`i.match_args(&on)?` →
        // `.unwrap_or_default()`) survives them: the wrong impl is selected, its
        // `Param(0)` substitutes against an empty argument list to `Ty::Error`,
        // and `Ty::Error` unifies with anything downstream. Head-only impl
        // selection is the miscompile class this project has already shipped once
        // (see the comment on the gate), which is why it gets its own test.
        let pair = |a: Ty, b: Ty| rec(1, vec![a, b]);
        let impls = [
            imp(
                pair(Ty::Param(0), Ty::Param(0)),
                1,
                vec![(DefId(ITEM), Ty::Param(0))],
            ),
            imp(pair(Ty::Int, Ty::Bool), 0, vec![(DefId(ITEM), Ty::String)]),
        ];
        assert_eq!(
            normalize_ty(&proj(pair(Ty::Int, Ty::Bool), ITEM), &impls),
            Ok(Ty::String),
            "Pair<Int, Bool> does not fit Pair<T, T>, so the concrete impl answers"
        );
        // The control: the generic impl *is* selected when the self type fits it.
        // Without this, the test above would also pass if `Pair<T, T>` were never
        // selectable at all.
        assert_eq!(
            normalize_ty(&proj(pair(Ty::Int, Ty::Int), ITEM), &impls),
            Ok(Ty::Int),
            "Pair<Int, Int> does fit Pair<T, T>"
        );
    }

    #[test]
    fn normalize_resolves_a_projection_whose_self_type_is_itself_a_projection() {
        // `Assoc { on: Assoc { .. } }` — the shape that makes pre-normalizing
        // `on` load-bearing. `W::Mid` resolves to `K`, and only then does the
        // outer projection have a head to look `Item` up on.
        //
        // Unwritable in Nova source (a binding cannot name another concrete
        // type's associated type), but `subst` builds it: monomorphization can
        // substitute a projection into `Assoc { on: Param(k) }`. Without the
        // pre-normalization the outer `on` has no `head()` and the whole thing is
        // returned unresolved.
        //
        // `normalize_recurses_into_every_compound_type`'s last case looks like
        // this but is not: there the projection is *inside* a record that already
        // has a head, so the outer lookup succeeds either way.
        let mid = 9;
        let w = rec(1, vec![]);
        let k = rec(2, vec![]);
        let impls = [
            imp(w.clone(), 0, vec![(DefId(mid), k)]),
            imp(rec(2, vec![]), 0, vec![(DefId(ITEM), Ty::Bool)]),
        ];
        assert_eq!(
            normalize_ty(&proj(proj(w, mid), ITEM), &impls),
            Ok(Ty::Bool)
        );
    }

    #[test]
    fn normalize_only_reads_the_binding_for_the_projected_associated_type() {
        // One impl binding two associated types. Reading the first entry
        // regardless of key gives `Ty::Int` for both.
        let other = 8;
        let impls = [imp(
            rec(1, vec![]),
            0,
            vec![(DefId(ITEM), Ty::Int), (DefId(other), Ty::String)],
        )];
        assert_eq!(
            normalize_ty(&proj(rec(1, vec![]), ITEM), &impls),
            Ok(Ty::Int)
        );
        assert_eq!(
            normalize_ty(&proj(rec(1, vec![]), other), &impls),
            Ok(Ty::String)
        );
    }

    #[test]
    fn normalize_leaves_a_projection_on_a_generic_parameter_alone() {
        // `Assoc { on: Param(k) }` has no head, so no impl can be selected. It
        // is monomorphization's job (Task 7), not an error and not `Ty::Error`.
        let impls = [imp(rec(1, vec![]), 0, vec![(DefId(ITEM), Ty::Int)])];
        let abstract_proj = proj(Ty::Param(0), ITEM);
        assert_eq!(normalize_ty(&abstract_proj, &impls), Ok(abstract_proj));
    }

    #[test]
    fn normalize_leaves_a_projection_with_no_matching_impl_alone() {
        // No impl of the owning trait for `Int`: the projection stays, so the
        // caller's unification reports a type error naming the projection
        // rather than a normalizer that invented `Ty::Error`.
        let impls = [imp(rec(1, vec![]), 0, vec![(DefId(ITEM), Ty::Int)])];
        let unresolvable = proj(Ty::Bool, ITEM);
        assert_eq!(normalize_ty(&unresolvable, &impls), Ok(unresolvable));
    }

    #[test]
    fn normalize_recurses_into_every_compound_type() {
        // A projection nested inside a compound type must be reached. An
        // implementation that only handles a top-level `Assoc` passes every
        // test whose projection is the whole type.
        let impls = [
            imp(rec(1, vec![]), 0, vec![(DefId(ITEM), Ty::Int)]),
            imp(rec(2, vec![Ty::Param(0)]), 1, vec![(DefId(ITEM), Ty::Char)]),
        ];
        let p = || proj(rec(1, vec![]), ITEM);
        assert_eq!(
            normalize_ty(&Ty::Array(Box::new(p())), &impls),
            Ok(Ty::Array(Box::new(Ty::Int)))
        );
        // A `clone`-without-recursing arm would return this unchanged
        // (`Ok(Ty::Future(Box::new(p())))`), leaving the projection intact.
        assert_eq!(
            normalize_ty(&Ty::Future(Box::new(p())), &impls),
            Ok(Ty::Future(Box::new(Ty::Int)))
        );
        assert_eq!(
            normalize_ty(&rec(3, vec![p(), Ty::Bool]), &impls),
            Ok(rec(3, vec![Ty::Int, Ty::Bool]))
        );
        assert_eq!(
            normalize_ty(
                &Ty::Sum {
                    def_id: DefId(4),
                    args: vec![p()]
                },
                &impls
            ),
            Ok(Ty::Sum {
                def_id: DefId(4),
                args: vec![Ty::Int]
            })
        );
        assert_eq!(
            normalize_ty(
                &Ty::Fn {
                    params: vec![p(), Ty::Bool],
                    ret: Box::new(p())
                },
                &impls
            ),
            Ok(Ty::Fn {
                params: vec![Ty::Int, Ty::Bool],
                ret: Box::new(Ty::Int)
            })
        );
        // And inside the Self type of another projection.
        assert_eq!(
            normalize_ty(&proj(rec(2, vec![p()]), ITEM), &impls),
            Ok(Ty::Char),
            "the inner W::Item resolves to Int, making the outer K<Int>::Item"
        );
    }

    #[test]
    fn normalize_follows_a_chain_of_bindings_to_the_end() {
        // `type A = Self::B` with `type B = Int`: one resolution step is not
        // enough, so the result has to be re-normalized. This is the behaviour
        // that forces the step guard to exist.
        let a = 7;
        let b = 8;
        let self_ty = rec(1, vec![]);
        let impls = [imp(
            self_ty.clone(),
            0,
            vec![(DefId(a), proj(self_ty.clone(), b)), (DefId(b), Ty::Int)],
        )];
        assert_eq!(normalize_ty(&proj(self_ty, a), &impls), Ok(Ty::Int));
    }

    #[test]
    fn normalize_gives_up_on_a_cyclic_binding_instead_of_diverging() {
        // typeck rejects this at collection (E0077) and poisons the binding, so
        // this shape is unreachable from source today. The guard exists because
        // that argument covers *bindings*, not every path that can build a
        // projection — and a compiler that hangs is worse than one that reports
        // a limit. This test's other value is that it completes.
        let self_ty = rec(1, vec![]);
        let cycle = proj(self_ty.clone(), ITEM);
        let impls = [imp(self_ty, 0, vec![(DefId(ITEM), cycle.clone())])];
        assert_eq!(
            normalize_ty(&cycle, &impls),
            Err(NormalizeOverflow {
                at: cycle,
                // The chain, not the total: a cycle resolves one link at a time
                // and never widens, so it is the depth allowance that stops it.
                limit: NormalizeLimit::Depth
            })
        );
    }

    #[test]
    fn normalize_gives_up_on_a_binding_that_grows_without_bound() {
        // `type Item = [Self::Item]`, the nested cycle: each step is a strictly
        // larger type rather than the same one, so a guard implemented as a
        // "have I seen this exact projection before" set would loop forever
        // where a step counter does not.
        let self_ty = rec(1, vec![]);
        let grows = Ty::Array(Box::new(proj(self_ty.clone(), ITEM)));
        let impls = [imp(self_ty.clone(), 0, vec![(DefId(ITEM), grows)])];
        assert_eq!(
            normalize_ty(&proj(self_ty.clone(), ITEM), &impls),
            Err(NormalizeOverflow {
                at: proj(self_ty, ITEM),
                // Depth, and this case is why the depth allowance cannot simply be
                // raised to match the step allowance: each resolution nests one
                // `Array` deeper, so recursion depth tracks it. At 10 000 this
                // overflows a test thread's 2 MiB stack instead of reporting.
                limit: NormalizeLimit::Depth
            }),
            "reports overflow rather than diverging"
        );
    }

    #[test]
    fn normalize_admits_a_chain_longer_than_a_couple_of_links() {
        // The limit must be generous enough that a legitimate chain never trips
        // it. Sixteen links is far past anything a person writes and well inside
        // the limit.
        let self_ty = rec(1, vec![]);
        let n = 16u32;
        let mut bindings: Vec<(DefId, Ty)> = (0..n)
            .map(|i| (DefId(100 + i), proj(self_ty.clone(), 101 + i)))
            .collect();
        bindings.push((DefId(100 + n), Ty::Int));
        let impls = [imp(self_ty.clone(), 0, bindings)];
        assert_eq!(normalize_ty(&proj(self_ty, 100), &impls), Ok(Ty::Int));
    }

    #[test]
    fn normalize_bounds_total_work_not_only_chain_depth() {
        // `type A(k) = Pair<Self::A(k+1), Self::A(k+1)>` down to `type A(n) = Int`.
        // No cycle, and the chain is `n` links — half the depth limit — but the
        // resolved type is `2^n` nodes, so a budget charged only when a projection
        // is resolved and passed *unchanged* into each compound arm does
        // exponential work while remaining, technically, convergent. At n=32 that
        // is four billion nodes.
        //
        // This is the test that separates "cannot diverge" from "does bounded
        // work", and the only overflow test here that is not a cycle — a cycle is
        // caught by the depth allowance alone, which is why the review found this
        // class unguarded. Measured through `nova check` before the step
        // allowance existed: n=20 took 12.9 s and n=24 (a 60-line source file,
        // accepted) had not finished after two minutes.
        let n = 32u32;
        let self_ty = rec(1, vec![]);
        let pair = |a: Ty, b: Ty| rec(2, vec![a, b]);
        let mut bindings: Vec<(DefId, Ty)> = (0..n)
            .map(|i| {
                let next = proj(self_ty.clone(), 101 + i);
                (DefId(100 + i), pair(next.clone(), next))
            })
            .collect();
        bindings.push((DefId(100 + n), Ty::Int));
        let impls = [imp(self_ty.clone(), 0, bindings)];
        let input = proj(self_ty, 100);
        assert_eq!(
            normalize_ty(&input, &impls),
            Err(NormalizeOverflow {
                at: input,
                // Steps, not depth: n=32 is inside the depth limit of 64, so
                // asserting the limit is what proves the *new* allowance is doing
                // the work rather than the old one catching it by luck.
                limit: NormalizeLimit::Steps
            }),
            "a diagnostic, not a hang — and not `Ty::Error`, which unifies with \
             anything and would make this a wrong answer instead"
        );
    }

    #[test]
    fn normalize_admits_a_branching_chain_that_stays_within_the_allowance() {
        // The control for the test above: branching is not itself the problem, so
        // a modest branching chain must still resolve. Ten levels is 1 024 leaves
        // and ~2 047 nodes, comfortably inside 10 000, and the result is checked
        // in full — a guard that rejected all branching would pass an assertion
        // that only looked at `is_ok`.
        let n = 10u32;
        let self_ty = rec(1, vec![]);
        let pair = |a: Ty, b: Ty| rec(2, vec![a, b]);
        let mut bindings: Vec<(DefId, Ty)> = (0..n)
            .map(|i| {
                let next = proj(self_ty.clone(), 101 + i);
                (DefId(100 + i), pair(next.clone(), next))
            })
            .collect();
        bindings.push((DefId(100 + n), Ty::Int));
        let impls = [imp(self_ty.clone(), 0, bindings)];
        let mut expected = Ty::Int;
        for _ in 0..n {
            expected = pair(expected.clone(), expected);
        }
        assert_eq!(normalize_ty(&proj(self_ty, 100), &impls), Ok(expected));
    }
}