Skip to main content

nova_hir/
lib.rs

1//! High-level IR for the Nova compiler.
2//!
3//! HIR is the *desugared, typed* representation produced by `nova-typeck`
4//! from the AST and consumed by `nova-mir`:
5//!
6//! - every expression carries a [`Ty`] and a `Span`
7//! - string interpolation is desugared to [`ExprKind::StrConcat`] over
8//!   [`ExprKind::ToStr`] conversions
9//! - compound assignment is desugared to a plain assign of a binary op
10//! - names are resolved: locals are [`LocalId`], callees are [`Callee`]
11//!
12//! The [`Ty`] type also serves as the type representation used *during*
13//! inference (it can contain [`Ty::Var`] inference variables); a fully
14//! checked module contains no `Var` types.
15
16use nova_diagnostics::Span;
17use nova_resolver::{Builtin, DefId};
18
19/// A type. This is the shared type representation across typeck, HIR and
20/// monomorphization (spec `12-TYPESYSTEM.md` §3, trimmed to the Phase 1
21/// feature set).
22#[derive(Debug, Clone, PartialEq)]
23pub enum Ty {
24    /// 64-bit signed integer (the default integer type).
25    Int,
26    /// 64-bit float (the default float type).
27    Float,
28    Bool,
29    Char,
30    String,
31    /// An immutable byte buffer.
32    ///
33    /// Structurally identical to [`Ty::String`] -- both are a `{len, ptr}` GC
34    /// leaf header; a runtime-made value's bytes follow it inline in the same
35    /// object, a `String` literal's are static data -- and semantically distinct:
36    /// only `String` carries a UTF-8 guarantee. Nothing converts between them
37    /// implicitly. This reaches codegen as the same opaque `MirTy::Ptr` every
38    /// other heap pointer already lowers to, so neither backend needs an arm
39    /// for it -- not because every operation on it is an intrinsic
40    /// (`index_of`/`contains` in `std/bytes/lib.nova` are pure Nova control
41    /// flow), but because codegen dispatches on MIR types, and `Ptr` is not
42    /// new.
43    Bytes,
44    /// The unit type `()`.
45    Unit,
46    /// A function type `fn(A, B) -> R`.
47    Fn {
48        params: Vec<Ty>,
49        ret: Box<Ty>,
50    },
51    /// A future produced by calling an `async fn`; the payload is the
52    /// function's declared return type (the future's *output*).
53    ///
54    /// Compiler-constructed only: there is no surface syntax that builds one,
55    /// and no impls may be written on it (`head()` returns `None`). At runtime
56    /// it is the same 2-word fat pointer as a function value —
57    /// `{ poll_code, state_ptr }` — which is why it sits beside `Ty::Fn` here
58    /// rather than being a record in `std/core`. Nova has no lang-item
59    /// mechanism: `Option` and `Result` are ordinary prelude sums the compiler
60    /// does not know by name, so a std record could not be recognized.
61    Future(Box<Ty>),
62    /// A user-defined sum type with generic arguments.
63    Sum {
64        def_id: DefId,
65        args: Vec<Ty>,
66    },
67    /// A user-defined record (struct) type with generic arguments.
68    Record {
69        def_id: DefId,
70        args: Vec<Ty>,
71    },
72    /// A heap array `[T]` with elements of a single type.
73    Array(Box<Ty>),
74    /// A generic type parameter of the enclosing item (`T`).
75    Param(u32),
76    /// A projection onto a trait's associated type: `<on>::Name`, where
77    /// `assoc` is the associated type's own `DefId` (see
78    /// `DefKind::AssocType`).
79    ///
80    /// This is the one `Ty` variant that is **not** a type by itself — it is a
81    /// *request* for one, answerable only with the impl table. It is therefore
82    /// normalized away at three seams ([`normalize_ty`] called from typeck,
83    /// `check_impl_conformance`, and `mono` after `subst`), and the unifier
84    /// never has to decide a projection against a concrete type.
85    ///
86    /// `on` is `Param(k)` inside a generic body and a concrete type at an
87    /// ordinary use site.
88    ///
89    /// **It can also be an unsolved `Var`, which the design doc §4.2 claims is
90    /// unreachable.** That claim holds for the case it argues:
91    /// `check_method_call` rejects an uninferred receiver with `E0011` before any
92    /// return type is computed, so a *receiver's* projection is never on a `Var`.
93    /// It does not hold for a generic call, where the type arguments are fresh
94    /// variables that argument unification narrows as it goes — `fn f<I: It>(y:
95    /// I::Item, x: I)` reaches the first parameter with `Assoc { on: Var(0) }`
96    /// and nothing has solved `Var(0)` yet. `Checker::instantiate` applies the
97    /// current substitution before normalizing, which covers every ordering where
98    /// the determining argument comes first; the reverse order is a genuine
99    /// (order-dependent) limitation of resolving at seams instead of deferring,
100    /// and it reports an ordinary type mismatch naming the projection rather than
101    /// anything worse.
102    Assoc {
103        on: Box<Ty>,
104        assoc: DefId,
105    },
106    /// An unsolved inference variable (only during type checking).
107    Var(u32),
108    /// The never type `!` (return, panic); coerces to anything.
109    Never,
110    /// Placeholder after a type error, suppresses cascading errors.
111    Error,
112}
113
114impl Ty {
115    /// Substitute `Param(i)` with `args[i]`. Used for generic instantiation
116    /// and monomorphization.
117    pub fn subst(&self, args: &[Ty]) -> Ty {
118        match self {
119            Ty::Param(i) => args.get(*i as usize).cloned().unwrap_or(Ty::Error),
120            Ty::Fn { params, ret } => Ty::Fn {
121                params: params.iter().map(|p| p.subst(args)).collect(),
122                ret: Box::new(ret.subst(args)),
123            },
124            Ty::Sum { def_id, args: a } => Ty::Sum {
125                def_id: *def_id,
126                args: a.iter().map(|t| t.subst(args)).collect(),
127            },
128            Ty::Record { def_id, args: a } => Ty::Record {
129                def_id: *def_id,
130                args: a.iter().map(|t| t.subst(args)).collect(),
131            },
132            Ty::Array(elem) => Ty::Array(Box::new(elem.subst(args))),
133            Ty::Future(out) => Ty::Future(Box::new(out.subst(args))),
134            Ty::Assoc { on, assoc } => Ty::Assoc {
135                on: Box::new(on.subst(args)),
136                assoc: *assoc,
137            },
138            other => other.clone(),
139        }
140    }
141
142    /// Whether this type (transitively) mentions the generic parameter `idx`.
143    pub fn mentions_param(&self, idx: u32) -> bool {
144        match self {
145            Ty::Param(k) => *k == idx,
146            Ty::Fn { params, ret } => {
147                params.iter().any(|p| p.mentions_param(idx)) || ret.mentions_param(idx)
148            }
149            Ty::Sum { args, .. } | Ty::Record { args, .. } => {
150                args.iter().any(|a| a.mentions_param(idx))
151            }
152            Ty::Array(elem) => elem.mentions_param(idx),
153            Ty::Future(out) => out.mentions_param(idx),
154            Ty::Assoc { on, .. } => on.mentions_param(idx),
155            _ => false,
156        }
157    }
158
159    /// Whether this type (transitively) contains any generic `Param`.
160    pub fn has_params(&self) -> bool {
161        match self {
162            Ty::Param(_) => true,
163            Ty::Fn { params, ret } => params.iter().any(Ty::has_params) || ret.has_params(),
164            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_params),
165            Ty::Array(elem) => elem.has_params(),
166            Ty::Future(out) => out.has_params(),
167            Ty::Assoc { on, .. } => on.has_params(),
168            _ => false,
169        }
170    }
171
172    /// Whether this type (transitively) contains any inference variable.
173    pub fn has_vars(&self) -> bool {
174        match self {
175            Ty::Var(_) => true,
176            Ty::Fn { params, ret } => params.iter().any(Ty::has_vars) || ret.has_vars(),
177            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_vars),
178            Ty::Array(elem) => elem.has_vars(),
179            Ty::Future(out) => out.has_vars(),
180            Ty::Assoc { on, .. } => on.has_vars(),
181            _ => false,
182        }
183    }
184
185    /// Whether this type (transitively) contains an associated-type projection.
186    ///
187    /// Lets a caller ask "is there anything here for [`normalize_ty`] to do?"
188    /// before paying for a normalization pass — and, more importantly, before
189    /// taking a step that is only correct *because* a projection is present. The
190    /// call seams in `nova-typeck` resolve their inference variables before
191    /// normalizing, which they must not do to an ordinary signature type.
192    pub fn has_assoc(&self) -> bool {
193        match self {
194            Ty::Assoc { .. } => true,
195            Ty::Fn { params, ret } => params.iter().any(Ty::has_assoc) || ret.has_assoc(),
196            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_assoc),
197            Ty::Array(elem) => elem.has_assoc(),
198            Ty::Future(out) => out.has_assoc(),
199            _ => false,
200        }
201    }
202
203    /// Whether this type (transitively) contains [`Ty::Error`].
204    ///
205    /// `Ty::Error` means "a diagnostic about this type has already been
206    /// reported", and it behaves **oppositely at the two consumers** that read
207    /// it. At `InferCtx::unify` it absorbs: it unifies with anything, so a
208    /// poisoned type silently stops cascading. `Ty` derives `PartialEq` with no
209    /// such absorption, so at a consumer that compares two types *directly* an
210    /// `Error` on one side instead **forces** a mismatch, and the second
211    /// diagnostic renders it as the meaningless `{error}`.
212    ///
213    /// This is for that second kind of consumer: it asks "is either side already
214    /// poisoned?" so the comparison can be skipped rather than turned into
215    /// noise. Transitive rather than a top-level `== Ty::Error` check because the
216    /// poison is usually nested — an impl binding an unresolvable type makes the
217    /// trait's `Option<Self::Item>` normalize to `Option<{error}>`, which is not
218    /// itself `Ty::Error`.
219    pub fn has_error(&self) -> bool {
220        match self {
221            Ty::Error => true,
222            Ty::Fn { params, ret } => params.iter().any(Ty::has_error) || ret.has_error(),
223            Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(Ty::has_error),
224            Ty::Array(elem) => elem.has_error(),
225            Ty::Future(out) => out.has_error(),
226            Ty::Assoc { on, .. } => on.has_error(),
227            _ => false,
228        }
229    }
230
231    /// The nominal head of this type, if it has one — used to key impl
232    /// lookups. Generic arguments do not participate (Phase 1 has no
233    /// overlapping impls per head).
234    pub fn head(&self) -> Option<TyHead> {
235        match self {
236            Ty::Int => Some(TyHead::Int),
237            Ty::Float => Some(TyHead::Float),
238            Ty::Bool => Some(TyHead::Bool),
239            Ty::Char => Some(TyHead::Char),
240            Ty::String => Some(TyHead::String),
241            Ty::Bytes => Some(TyHead::Bytes),
242            Ty::Sum { def_id, .. } => Some(TyHead::Sum(*def_id)),
243            Ty::Record { def_id, .. } => Some(TyHead::Record(*def_id)),
244            _ => None,
245        }
246    }
247
248    /// One-directional match: treat `self` as a pattern that may contain
249    /// `Param(k)` and match it against the concrete `ground` type, recording
250    /// each `Param(k)` → ground binding into `out` (grown as needed). A
251    /// parameter seen twice must bind to the same type. Returns `false` on a
252    /// structural mismatch. Used to recover a generic impl's type arguments
253    /// from a concrete receiver type (e.g. `Box<T>` vs `Box<Int>` → `T=Int`).
254    pub fn match_pattern(&self, ground: &Ty, out: &mut Vec<Option<Ty>>) -> bool {
255        match (self, ground) {
256            (Ty::Param(k), g) => {
257                let k = *k as usize;
258                if out.len() <= k {
259                    out.resize(k + 1, None);
260                }
261                match &out[k] {
262                    Some(existing) => existing == g,
263                    None => {
264                        out[k] = Some(g.clone());
265                        true
266                    }
267                }
268            }
269            (
270                Ty::Record {
271                    def_id: d1,
272                    args: a1,
273                },
274                Ty::Record {
275                    def_id: d2,
276                    args: a2,
277                },
278            )
279            | (
280                Ty::Sum {
281                    def_id: d1,
282                    args: a1,
283                },
284                Ty::Sum {
285                    def_id: d2,
286                    args: a2,
287                },
288            ) => {
289                d1 == d2
290                    && a1.len() == a2.len()
291                    && a1.iter().zip(a2).all(|(p, g)| p.match_pattern(g, out))
292            }
293            (Ty::Array(e1), Ty::Array(e2)) => e1.match_pattern(e2, out),
294            (Ty::Future(o1), Ty::Future(o2)) => o1.match_pattern(o2, out),
295            (
296                Ty::Fn {
297                    params: p1,
298                    ret: r1,
299                },
300                Ty::Fn {
301                    params: p2,
302                    ret: r2,
303                },
304            ) => {
305                p1.len() == p2.len()
306                    && p1.iter().zip(p2).all(|(a, b)| a.match_pattern(b, out))
307                    && r1.match_pattern(r2, out)
308            }
309            (Ty::Assoc { on: p, assoc: pa }, Ty::Assoc { on: g, assoc: ga }) => {
310                pa == ga && p.match_pattern(g, out)
311            }
312            // Primitives, `Unit`, etc.: match iff identical.
313            (a, b) => a == b,
314        }
315    }
316}
317
318/// The nominal head of a type, used as the key for impl lookups
319/// (spec `12-TYPESYSTEM.md` §5.2, `ImplTable` indexed by trait + type head).
320#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
321pub enum TyHead {
322    Int,
323    Float,
324    Bool,
325    Char,
326    String,
327    Bytes,
328    Sum(DefId),
329    Record(DefId),
330}
331
332/// A local variable slot within a function (parameters come first).
333#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
334pub struct LocalId(pub u32);
335
336/// Metadata for one local variable.
337#[derive(Debug, Clone)]
338pub struct Local {
339    pub name: String,
340    pub ty: Ty,
341    pub is_mut: bool,
342    pub span: Span,
343}
344
345/// An `extern` function declaration: a C-ABI import with no Nova body. Only its
346/// signature and (unmangled) C symbol name are needed to declare and call it.
347#[derive(Debug, Clone)]
348pub struct ExternFn {
349    pub def_id: DefId,
350    /// The raw C symbol to import and call (never mangled).
351    pub symbol: String,
352    pub params: Vec<Ty>,
353    pub ret: Ty,
354    /// Declaration site, for conflicting-signature diagnostics.
355    pub span: Span,
356}
357
358/// A fully checked module: type layouts plus typed functions.
359#[derive(Debug, Default)]
360pub struct Module {
361    pub sums: Vec<SumType>,
362    pub records: Vec<RecordType>,
363    pub traits: Vec<TraitDef>,
364    pub impls: Vec<ImplInfo>,
365    pub functions: Vec<Function>,
366    /// `extern` (FFI) function declarations reachable in the program.
367    pub externs: Vec<ExternFn>,
368}
369
370impl Module {
371    /// Find the extern function declared under `def_id`, if any.
372    pub fn extern_fn(&self, def_id: DefId) -> Option<&ExternFn> {
373        self.externs.iter().find(|e| e.def_id == def_id)
374    }
375
376    /// Find the sum type declared under `def_id`, if any.
377    pub fn sum(&self, def_id: DefId) -> Option<&SumType> {
378        self.sums.iter().find(|s| s.def_id == def_id)
379    }
380
381    /// Find the record type declared under `def_id`, if any.
382    pub fn record(&self, def_id: DefId) -> Option<&RecordType> {
383        self.records.iter().find(|r| r.def_id == def_id)
384    }
385
386    /// Find the trait declared under `def_id`, if any.
387    pub fn trait_def(&self, def_id: DefId) -> Option<&TraitDef> {
388        self.traits.iter().find(|t| t.def_id == def_id)
389    }
390
391    /// Find the function declared under `def_id`, if any.
392    pub fn function(&self, def_id: DefId) -> Option<&Function> {
393        self.functions.iter().find(|f| f.def_id == def_id)
394    }
395
396    /// Resolve trait method `method` (index into the trait's methods) for a
397    /// concrete self type to the compiled function it should dispatch to,
398    /// paired with the type arguments that function must be instantiated with:
399    ///
400    /// - if the matching impl provides the method, dispatch to it, instantiated
401    ///   with the impl's own type arguments recovered from `self_ty`
402    ///   (`impl<T> Show for Box<T>` called on `Box<Int>` → `[Int]`);
403    /// - otherwise dispatch to the trait's default body, which is generic over
404    ///   `Self` → `[self_ty]`.
405    ///
406    /// Returns `None` if no impl of the trait fits `self_ty`.
407    pub fn resolve_method_full(
408        &self,
409        trait_id: DefId,
410        method: u32,
411        self_ty: &Ty,
412    ) -> Option<(DefId, Vec<Ty>)> {
413        let tr = self.trait_def(trait_id)?;
414        let method_name = &tr.methods.get(method as usize)?.name;
415        let head = self_ty.head()?;
416        // Among all impls of this trait for the head, select the one whose
417        // self-type pattern actually fits — not merely the first sharing the
418        // head. Coherence (no overlapping impls) guarantees at most one fits.
419        let (imp, impl_args) = self
420            .impls
421            .iter()
422            .filter(|i| i.trait_id == Some(trait_id) && i.self_head == head)
423            .find_map(|i| i.match_args(self_ty).map(|args| (i, args)))?;
424        if let Some((_, def)) = imp.methods.iter().find(|(n, _)| n == method_name) {
425            Some((*def, impl_args))
426        } else {
427            let def = tr.methods[method as usize].default_def?;
428            Some((def, vec![self_ty.clone()]))
429        }
430    }
431}
432
433/// How many resolutions deep one projection *chain* may go before
434/// [`normalize_ty`] gives up.
435///
436/// Charged only where a projection is actually resolved, and passed *unchanged*
437/// into the compound arms: a finite type is a finite tree, so recursion into
438/// `Fn`/`Sum`/`Record`/`Array` cannot diverge, and charging it would reject a
439/// legitimately deeply-nested type.
440///
441/// Two jobs, both load-bearing:
442///
443/// - It catches a **cycle**. `type Item = Self::Item` resolves to itself forever;
444///   `type Item = [Self::Item]` grows a level each time, so a "have I seen this
445///   exact projection" set would not catch it but a counter does.
446/// - It bounds the **stack**, which is why it cannot simply be raised. Each
447///   resolution costs a constant number of `normalize_within` frames, and a
448///   growing binding nests one level deeper per step, so recursion depth tracks
449///   this number. Measured: allowing 10 000 resolutions makes
450///   `type Item = [Self::Item]` overflow a test thread's 2 MiB stack — a hard
451///   crash, strictly worse than the diagnostic it replaced. 64 keeps the deepest
452///   walk to a couple of hundred frames.
453///
454/// **64 is still the right number even though this limit is user-facing** (see
455/// `Checker::normalize` — a non-cyclic chain of 64 links reports `E0078`, so this
456/// is reachable from ordinary source and not merely a backstop for compiler
457/// defects). Nova has no macros and no code generation, so every binding chain is
458/// hand-written, and a hand-written one is one to three links; 64 is already
459/// twenty times past the plausible. Raising it trades a limit nobody can reach by
460/// accident for a stack overflow, which is the wrong trade.
461///
462/// It does **not** bound total work — see [`NORMALIZE_STEP_LIMIT`].
463pub const NORMALIZE_DEPTH_LIMIT: u32 = 64;
464
465/// How many nodes one whole [`normalize_ty`] walk may visit before giving up.
466///
467/// **The second of two allowances, because bounding chain depth does not bound
468/// work.** [`NORMALIZE_DEPTH_LIMIT`]'s justification — "a finite type is a finite
469/// tree, so compound recursion cannot diverge" — is sound and proves the wrong
470/// thing: non-divergence is not bounded work. A *branching* binding chain
471/// multiplies. With `type A(k) = Pair<Self::A(k+1), Self::A(k+1)>` terminating at
472/// `type A(n) = Int` — no cycle, chain length `n`, every link far inside the depth
473/// limit — the resolved type is itself `2^n` nodes, and each level pays for both
474/// copies of the level below. Measured through `nova check` on programs it
475/// *accepts*: n=16 → 716 ms, n=20 → 12.9 s, n=24 (a 60-line source file) → still
476/// running after two minutes. A four-field record gives `4^n` in fewer lines.
477///
478/// So this counter is a single allowance shared by the entire walk, spent one step
479/// per node, charged by **every** arm. That bounds total work by construction: at
480/// most this many calls happen, so at most this many nodes are built.
481///
482/// Memoizing the projection lookups was the other candidate and does **not** fix
483/// it: the *result* for `A(0)` is `2^n` nodes whatever the cache hit rate, so it
484/// must still be materialized, and cloned into both branches at every level. Only
485/// a cap on the result bounds the work, and a shared step counter is that cap.
486///
487/// 10 000 is three orders of magnitude past anything a person writes (std's
488/// largest signature type is a handful of nodes), exhausts in microseconds when
489/// something pathological hits it, and caps a resolved type at ~10 000 nodes. It
490/// is deliberately *not* the same number as the depth limit: the units differ
491/// (total nodes vs. resolutions along one chain), and 64 total nodes would reject
492/// an ordinary projection-free type with 64 parts.
493pub const NORMALIZE_STEP_LIMIT: u32 = 10_000;
494
495/// Which of [`normalize_ty`]'s two allowances ran out. They fail on different
496/// shapes and a user fixes them differently, so the diagnostic distinguishes
497/// them: [`Depth`](Self::Depth) means a chain that does not terminate,
498/// [`Steps`](Self::Steps) means one that terminates at an unreasonable size.
499#[derive(Debug, Clone, Copy, PartialEq, Eq)]
500pub enum NormalizeLimit {
501    /// [`NORMALIZE_DEPTH_LIMIT`] — resolutions along one projection chain.
502    Depth,
503    /// [`NORMALIZE_STEP_LIMIT`] — nodes visited by the whole walk.
504    Steps,
505}
506
507/// [`normalize_ty`] ran out of budget.
508///
509/// This is deliberately *not* folded into `Ty::Error`: `Error` unifies with
510/// anything, so returning it would silently accept whatever the caller compared
511/// the type against, turning a hang into a wrong answer. The caller must report
512/// a diagnostic.
513#[derive(Debug, Clone, PartialEq)]
514pub struct NormalizeOverflow {
515    /// The type [`normalize_ty`] was asked to resolve — the whole input, not the
516    /// intermediate the walk happened to be on when the budget ran out.
517    ///
518    /// The intermediate is the wrong thing to name. On a linear chain
519    /// `A0 → A1 → … → A64` it is `W::A64`, a rung the user never wrote, in the
520    /// middle of a ladder they would have to count to find; the input is `W::A0`,
521    /// which is the projection to go and look at. Depth-first exhaustion also
522    /// makes *which* intermediate you land on an artifact of traversal order.
523    pub at: Ty,
524    /// Which allowance ran out.
525    pub limit: NormalizeLimit,
526}
527
528/// Resolve every [`Ty::Assoc`] projection in `ty` that the impl table can
529/// answer, leaving the rest untouched.
530///
531/// This is the shared core of all three normalization seams (see the design doc
532/// §4.1): `nova-typeck` calls it where a checked type is consumed, and
533/// monomorphization calls it after `subst`. It lives here, over a plain
534/// `&[ImplInfo]` slice, because that is the one signature both callers can
535/// satisfy — the `Checker` holds `impls` mid-construction and mono holds the
536/// finished `Module::impls`.
537///
538/// **A projection is resolved when, and only when, its Self type has a
539/// nominal [`Ty::head`]:**
540///
541/// - `Assoc { on: W<Int> }` resolves through the impl of the owning trait for
542///   `W`, substituting the impl's own type arguments (recovered by
543///   [`ImplInfo::match_args`]) into the bound type.
544/// - `Assoc { on: Param(k) }` has no head and is returned unchanged. That is not
545///   a failure: inside a generic body the projection is genuinely abstract until
546///   monomorphization substitutes `Param(k)`.
547/// - A projection with a head but no impl binding it is likewise returned
548///   unchanged, so the caller's unification reports a type error that *names the
549///   projection* rather than a normalizer that invented `Ty::Error`.
550///
551/// The impl is selected by the associated type's own `DefId`, which belongs to
552/// exactly one associated type of exactly one trait. An impl binding that
553/// `DefId` is therefore an impl of the owning trait by construction, and no
554/// separate trait lookup (or `Definitions` access) is needed here.
555///
556/// The result is **re-normalized**, because a bound type may itself be a
557/// projection: `type A = Self::B` with `type B = Int` must resolve all the way
558/// to `Int`. That is what makes the step guard load-bearing rather than
559/// paranoid — see [`NORMALIZE_STEP_LIMIT`].
560pub fn normalize_ty(ty: &Ty, impls: &[ImplInfo]) -> Result<Ty, NormalizeOverflow> {
561    let mut steps = NORMALIZE_STEP_LIMIT;
562    // The inner walk reports only *which* allowance ran out; the type named in
563    // the diagnostic is this call's input, not whichever intermediate depth-first
564    // traversal happened to be on (see `NormalizeOverflow::at`).
565    normalize_within(ty, impls, NORMALIZE_DEPTH_LIMIT, &mut steps).map_err(|limit| {
566        NormalizeOverflow {
567            at: ty.clone(),
568            limit,
569        }
570    })
571}
572
573fn normalize_within(
574    ty: &Ty,
575    impls: &[ImplInfo],
576    depth: u32,
577    steps: &mut u32,
578) -> Result<Ty, NormalizeLimit> {
579    // Charged once per node by every arm, compound arms included, out of one
580    // allowance shared by the whole walk. Charging only the `Assoc` arm is what
581    // let a branching binding chain do exponential work without ever diverging —
582    // see `NORMALIZE_STEP_LIMIT`. `depth`, by contrast, stays per-branch.
583    *steps = steps.checked_sub(1).ok_or(NormalizeLimit::Steps)?;
584    match ty {
585        Ty::Assoc { on, assoc } => {
586            let Some(depth) = depth.checked_sub(1) else {
587                return Err(NormalizeLimit::Depth);
588            };
589            // The Self type may itself contain a projection, so resolve it
590            // before asking it for a head.
591            let on = normalize_within(on, impls, depth, steps)?;
592            let Some(head) = on.head() else {
593                return Ok(Ty::Assoc {
594                    on: Box::new(on),
595                    assoc: *assoc,
596                });
597            };
598            // Sharing a head is not enough: an impl with a repeated or
599            // partially-concrete self type (`impl<T> It for Pair<T, T>`) only
600            // applies to Self types that genuinely fit it, which is what
601            // `match_args` decides.
602            let bound = impls.iter().filter(|i| i.self_head == head).find_map(|i| {
603                let (_, bound) = i.assoc_bindings.iter().find(|(d, _)| d == assoc)?;
604                let args = i.match_args(&on)?;
605                Some(bound.subst(&args))
606            });
607            match bound {
608                Some(bound) => normalize_within(&bound, impls, depth, steps),
609                None => Ok(Ty::Assoc {
610                    on: Box::new(on),
611                    assoc: *assoc,
612                }),
613            }
614        }
615        Ty::Fn { params, ret } => Ok(Ty::Fn {
616            params: params
617                .iter()
618                .map(|p| normalize_within(p, impls, depth, steps))
619                .collect::<Result<_, _>>()?,
620            ret: Box::new(normalize_within(ret, impls, depth, steps)?),
621        }),
622        Ty::Sum { def_id, args } => Ok(Ty::Sum {
623            def_id: *def_id,
624            args: args
625                .iter()
626                .map(|a| normalize_within(a, impls, depth, steps))
627                .collect::<Result<_, _>>()?,
628        }),
629        Ty::Record { def_id, args } => Ok(Ty::Record {
630            def_id: *def_id,
631            args: args
632                .iter()
633                .map(|a| normalize_within(a, impls, depth, steps))
634                .collect::<Result<_, _>>()?,
635        }),
636        Ty::Array(elem) => Ok(Ty::Array(Box::new(normalize_within(
637            elem, impls, depth, steps,
638        )?))),
639        Ty::Future(out) => Ok(Ty::Future(Box::new(normalize_within(
640            out, impls, depth, steps,
641        )?))),
642        Ty::Int
643        | Ty::Float
644        | Ty::Bool
645        | Ty::Char
646        | Ty::String
647        | Ty::Bytes
648        | Ty::Unit
649        | Ty::Param(_)
650        | Ty::Var(_)
651        | Ty::Never
652        | Ty::Error => Ok(ty.clone()),
653    }
654}
655
656/// Whether two impl self-type patterns share a common ground instance — i.e.
657/// the impls overlap and one concrete type could match both. `a` uses generic
658/// parameters `0..a_generics`; `b`'s parameters are an independent namespace
659/// `0..b_generics`. Exact: first-order unification with an occurs check, so
660/// genuinely disjoint patterns (`Pair<Int, Bool>` vs `Pair<Int, String>`) are
661/// never reported as overlapping, while a generic and a specific pattern
662/// (`Box<T>` vs `Box<Int>`) are.
663pub fn self_types_overlap(a: &Ty, a_generics: u32, b: &Ty, b_generics: u32) -> bool {
664    // A projection's value is unknown until normalized, so assume it could
665    // coincide with anything unless both sides are projections that provably
666    // differ. A false E0074 is a loud error; a missed overlap is a silent
667    // miscompile, so err toward overlap.
668    match (a, b) {
669        (Ty::Assoc { on: a1, assoc: x }, Ty::Assoc { on: b1, assoc: y }) => {
670            x != y || self_types_overlap(a1, a_generics, b1, b_generics)
671        }
672        (Ty::Assoc { .. }, _) | (_, Ty::Assoc { .. }) => true,
673        _ => {
674            // Shift `b`'s parameters into a disjoint range so the two namespaces
675            // do not collide in the shared substitution.
676            let b = shift_params(b, a_generics);
677            let mut subst: Vec<Option<Ty>> = vec![None; (a_generics + b_generics) as usize];
678            unify_patterns(a, &b, &mut subst)
679        }
680    }
681}
682
683fn shift_params(t: &Ty, by: u32) -> Ty {
684    match t {
685        Ty::Param(k) => Ty::Param(k + by),
686        Ty::Fn { params, ret } => Ty::Fn {
687            params: params.iter().map(|p| shift_params(p, by)).collect(),
688            ret: Box::new(shift_params(ret, by)),
689        },
690        Ty::Sum { def_id, args } => Ty::Sum {
691            def_id: *def_id,
692            args: args.iter().map(|a| shift_params(a, by)).collect(),
693        },
694        Ty::Record { def_id, args } => Ty::Record {
695            def_id: *def_id,
696            args: args.iter().map(|a| shift_params(a, by)).collect(),
697        },
698        Ty::Array(elem) => Ty::Array(Box::new(shift_params(elem, by))),
699        Ty::Future(out) => Ty::Future(Box::new(shift_params(out, by))),
700        other => other.clone(),
701    }
702}
703
704/// Resolve `t` through the substitution one level (following a bound `Param`).
705fn walk_param(t: &Ty, subst: &[Option<Ty>]) -> Ty {
706    match t {
707        Ty::Param(k) => match subst.get(*k as usize).and_then(|o| o.as_ref()) {
708            Some(bound) => walk_param(bound, subst),
709            None => t.clone(),
710        },
711        _ => t.clone(),
712    }
713}
714
715fn occurs(k: u32, t: &Ty, subst: &[Option<Ty>]) -> bool {
716    match walk_param(t, subst) {
717        Ty::Param(j) => j == k,
718        Ty::Fn { params, ret } => {
719            params.iter().any(|p| occurs(k, p, subst)) || occurs(k, &ret, subst)
720        }
721        Ty::Sum { args, .. } | Ty::Record { args, .. } => args.iter().any(|a| occurs(k, a, subst)),
722        Ty::Array(elem) => occurs(k, &elem, subst),
723        Ty::Future(out) => occurs(k, &out, subst),
724        _ => false,
725    }
726}
727
728fn unify_patterns(a: &Ty, b: &Ty, subst: &mut Vec<Option<Ty>>) -> bool {
729    let a = walk_param(a, subst);
730    let b = walk_param(b, subst);
731    match (&a, &b) {
732        (Ty::Param(i), Ty::Param(j)) if i == j => true,
733        (Ty::Param(i), _) => {
734            if occurs(*i, &b, subst) {
735                return false;
736            }
737            subst[*i as usize] = Some(b.clone());
738            true
739        }
740        (_, Ty::Param(j)) => {
741            if occurs(*j, &a, subst) {
742                return false;
743            }
744            subst[*j as usize] = Some(a.clone());
745            true
746        }
747        (
748            Ty::Record {
749                def_id: d1,
750                args: a1,
751            },
752            Ty::Record {
753                def_id: d2,
754                args: a2,
755            },
756        )
757        | (
758            Ty::Sum {
759                def_id: d1,
760                args: a1,
761            },
762            Ty::Sum {
763                def_id: d2,
764                args: a2,
765            },
766        ) => {
767            d1 == d2
768                && a1.len() == a2.len()
769                && a1.iter().zip(a2).all(|(x, y)| unify_patterns(x, y, subst))
770        }
771        (Ty::Array(e1), Ty::Array(e2)) => unify_patterns(e1, e2, subst),
772        (Ty::Future(o1), Ty::Future(o2)) => unify_patterns(o1, o2, subst),
773        (
774            Ty::Fn {
775                params: p1,
776                ret: r1,
777            },
778            Ty::Fn {
779                params: p2,
780                ret: r2,
781            },
782        ) => {
783            p1.len() == p2.len()
784                && p1.iter().zip(p2).all(|(x, y)| unify_patterns(x, y, subst))
785                && unify_patterns(r1, r2, subst)
786        }
787        // Primitives, `Unit`, `Error`: overlap iff identical.
788        (x, y) => x == y,
789    }
790}
791
792/// A trait declaration with its method signatures.
793#[derive(Debug, Clone)]
794pub struct TraitDef {
795    pub def_id: DefId,
796    pub name: String,
797    /// Traits this one requires (`trait Ord: Eq` → `[Eq]`), resolved and
798    /// deduplicated. Direct supertraits only — the transitive closure is taken
799    /// where it is needed, so a cyclic declaration cannot make this list
800    /// infinite.
801    ///
802    /// The graph formed by these lists **can itself be cyclic**: `trait A: B`
803    /// together with `trait B: A` is accepted (`nova-typeck` only ever
804    /// requires satisfiability, not acyclicity). A transitive walk over this
805    /// field — chasing `supertraits` into each named trait's own
806    /// `supertraits`, and so on — must therefore track which traits it has
807    /// already visited, or it will loop forever on such a declaration. (The
808    /// existing transitive expansion in `nova-typeck` does this by construction:
809    /// it only ever appends an id it has not already recorded.)
810    pub supertraits: Vec<DefId>,
811    pub methods: Vec<TraitMethod>,
812    /// Associated types this trait declares, in declaration order, each with
813    /// its own `DefId` (`DefKind::AssocType`). An impl must bind every one of
814    /// them; `check_impl_conformance` enforces that.
815    pub assoc_types: Vec<(String, DefId)>,
816}
817
818/// One method of a trait. In `params`/`ret`, `Ty::Param(0)` denotes `Self` and
819/// `Ty::Param(1..=generics)` the method's own generic parameters (a generic
820/// method like `fn map<U>(self, …)`). `params` never itself contains a
821/// `self` entry: when the method declares a `self` receiver it is implicit
822/// rather than stored here, but a trait method need not declare one at all
823/// (e.g. `fn zero() -> Int`), in which case `params` is just its declared
824/// parameters.
825#[derive(Debug, Clone)]
826pub struct TraitMethod {
827    pub name: String,
828    pub params: Vec<Ty>,
829    pub ret: Ty,
830    /// Whether the method declares a `self` receiver. A method without one is
831    /// an associated function, called as `Type::name(…)` with no receiver —
832    /// never as `value.name(…)`. `params` looks the same either way (`self` is
833    /// never stored in it), so this flag is the only record of the difference,
834    /// and dispatch that ignores it lowers a receiver argument into a callee
835    /// that has no slot for it.
836    pub has_self: bool,
837    /// Whether the `self` receiver is declared `mut`, i.e. whether the method is
838    /// a mutator whose callers must supply a mutable receiver place (`E0060`,
839    /// ADR 0005 §1). Meaningless when `has_self` is false, and the conformance
840    /// check that compares this against the impl's own `mut` runs only after the
841    /// two agree about `has_self` at all.
842    ///
843    /// It has to live here rather than being read off the impl: trait dispatch
844    /// resolves to `(trait_id, method_index)`, and for a generic receiver
845    /// (`fn f<T: Tr>(mut x: T) { x.m() }`) there is no single impl whose
846    /// receiver declaration could be consulted. `params` cannot carry it either
847    /// — `method_sig_parts` strips a `self` parameter whether or not it is
848    /// `mut`, so the flag is the only record, exactly as `has_self` is the only
849    /// record of the receiver's presence.
850    pub mut_self: bool,
851    /// Number of the method's own generic parameters (not counting `Self`).
852    pub generics: u32,
853    /// Trait bounds per method generic parameter (indexed `0..generics`).
854    pub bounds: Vec<Vec<DefId>>,
855    /// The compiled default-body function, if the trait provides a default.
856    pub default_def: Option<DefId>,
857}
858
859/// One `impl` block: an inherent impl (`trait_id: None`) or a trait impl.
860#[derive(Debug, Clone)]
861pub struct ImplInfo {
862    pub trait_id: Option<DefId>,
863    /// The nominal head of the self type — the impl-table lookup key.
864    pub self_head: TyHead,
865    /// The impl's self type, with `Param(k)` standing for the impl's k-th
866    /// generic parameter (e.g. `Box<Param(0)>` for `impl<T> … for Box<T>`).
867    /// A non-generic impl's self type contains no `Param`.
868    pub self_ty: Ty,
869    /// Number of generic parameters the impl introduces.
870    pub generics: u32,
871    /// Trait bounds on each impl generic parameter (`impl<T: Bound>`), indexed
872    /// by parameter position — empty for an unconstrained or non-generic impl.
873    pub bounds: Vec<Vec<DefId>>,
874    /// `(method name, compiled method function DefId)` for methods this
875    /// impl defines directly.
876    pub methods: Vec<(String, DefId)>,
877    /// Associated types this impl binds, keyed by the associated type's own
878    /// `DefId` (`DefKind::AssocType`, the same id `TraitDef::assoc_types`
879    /// carries). The bound type may contain the impl's `Param(k)`, so
880    /// normalization must substitute the impl's arguments before using it.
881    ///
882    /// Empty for an inherent impl: only a trait declares associated types, so
883    /// only a trait impl can bind one.
884    pub assoc_bindings: Vec<(DefId, Ty)>,
885}
886
887impl ImplInfo {
888    /// Recover this impl's type arguments (in `Param` order) from a concrete
889    /// self type. Returns `None` when the self type does not actually match the
890    /// impl's self-type pattern — sharing a head is not enough, so an impl with
891    /// a repeated (`Pair<T, T>`) or partially-concrete (`Pair<Int, T>`) self
892    /// type only applies to receivers that genuinely fit it. A parameter the
893    /// pattern does not mention resolves to `Ty::Error` (an unconstrained,
894    /// unused impl generic, which never reaches code).
895    pub fn match_args(&self, concrete: &Ty) -> Option<Vec<Ty>> {
896        let mut out: Vec<Option<Ty>> = Vec::new();
897        if !self.self_ty.match_pattern(concrete, &mut out) {
898            return None;
899        }
900        Some(
901            (0..self.generics as usize)
902                .map(|i| out.get(i).cloned().flatten().unwrap_or(Ty::Error))
903                .collect(),
904        )
905    }
906}
907
908/// A record (struct) declaration with typed fields.
909#[derive(Debug, Clone)]
910pub struct RecordType {
911    pub def_id: DefId,
912    pub name: String,
913    /// Number of generic parameters.
914    pub generics: u32,
915    pub fields: Vec<RecordField>,
916}
917
918/// One field of a record; the type may reference `Ty::Param`.
919#[derive(Debug, Clone)]
920pub struct RecordField {
921    pub name: String,
922    pub ty: Ty,
923}
924
925/// A sum type declaration with typed variant payloads.
926#[derive(Debug, Clone)]
927pub struct SumType {
928    pub def_id: DefId,
929    pub name: String,
930    /// Number of generic parameters.
931    pub generics: u32,
932    pub variants: Vec<Variant>,
933}
934
935/// One variant of a sum type; field types may reference `Ty::Param`.
936#[derive(Debug, Clone)]
937pub struct Variant {
938    pub name: String,
939    pub fields: Vec<Ty>,
940}
941
942/// A typed function.
943#[derive(Debug)]
944pub struct Function {
945    pub def_id: DefId,
946    pub name: String,
947    /// Number of generic parameters; generic functions are monomorphized
948    /// before codegen.
949    pub generics: u32,
950    /// Trait bounds per generic parameter (`bounds[i]` are the trait
951    /// `DefId`s the i-th parameter must satisfy). Checked at
952    /// monomorphization once the concrete type argument is known.
953    pub bounds: Vec<Vec<DefId>>,
954    /// Whether this function is the code of a function value (a closure or
955    /// a bare-fn wrapper). Such functions take a leading environment
956    /// pointer in their ABI: `(env_ptr, params...)`. Normal, directly
957    /// called functions do not.
958    pub takes_env: bool,
959    /// For a closure, the number of leading `locals` that are captured
960    /// variables loaded from the environment at entry (0 for a bare-fn
961    /// wrapper). The captured locals precede the real parameters.
962    pub capture_count: u32,
963    /// The first `params` entries of `locals` are the real parameters
964    /// (after any captures). For a closure the captured locals occupy
965    /// indices `0..capture_count` and the parameters `capture_count..`.
966    pub params: u32,
967    pub locals: Vec<Local>,
968    pub ret_ty: Ty,
969    /// Whether this function was declared `async`. `ret_ty` is already
970    /// `Ty::Future(output)` when true; this flag is what tells `nova-mir`
971    /// which functions to treat specially, since a non-async function may
972    /// also return a `Future` (by calling an async fn and not awaiting it),
973    /// so `ret_ty` alone can't distinguish them — which is the whole reason
974    /// this flag exists rather than a test on `ret_ty`'s shape.
975    ///
976    /// What `nova-mir` does with it is that crate's contract
977    /// (`nova-mir/src/async_lower.rs`), not restated here, for the reason
978    /// [`ExprKind::Await`]'s doc gives.
979    pub is_async: bool,
980    pub body: Expr,
981    pub span: Span,
982}
983
984/// A typed expression.
985#[derive(Debug, Clone)]
986pub struct Expr {
987    pub kind: ExprKind,
988    pub ty: Ty,
989    pub span: Span,
990}
991
992/// What a call dispatches to.
993#[derive(Debug, Clone, Copy, PartialEq, Eq)]
994pub enum Callee {
995    /// A top-level function.
996    Def(DefId),
997    /// A compiler builtin.
998    Builtin(Builtin),
999    /// An indirect call through a fn-typed local.
1000    Local(LocalId),
1001}
1002
1003/// Binary operators after type checking (operand types are known).
1004#[derive(Debug, Clone, Copy, PartialEq, Eq)]
1005pub enum BinOp {
1006    Add,
1007    Sub,
1008    Mul,
1009    Div,
1010    Rem,
1011    Eq,
1012    Ne,
1013    Lt,
1014    Le,
1015    Gt,
1016    Ge,
1017    BitAnd,
1018    BitOr,
1019    BitXor,
1020    Shl,
1021    Shr,
1022}
1023
1024/// Unary operators.
1025#[derive(Debug, Clone, Copy, PartialEq, Eq)]
1026pub enum UnOp {
1027    /// Numeric negation.
1028    Neg,
1029    /// Boolean not.
1030    Not,
1031    /// Bitwise not (Int).
1032    BitNot,
1033}
1034
1035/// Expression kinds. Desugared relative to the AST: no string interpolation,
1036/// no compound assignment, no `for` (Phase 1 defers iterators).
1037#[derive(Debug, Clone)]
1038pub enum ExprKind {
1039    IntLit(i64),
1040    FloatLit(f64),
1041    BoolLit(bool),
1042    StrLit(String),
1043    CharLit(char),
1044    /// The unit value `()`.
1045    Unit,
1046    /// Read a local variable.
1047    Local(LocalId),
1048    /// Build a function value (fat pointer `{ code, env }`). `func` is the
1049    /// code function (a closure body or a bare-fn wrapper), instantiated
1050    /// with `type_args`; `captures` are the environment's values in order
1051    /// (empty for a bare-fn wrapper).
1052    MakeClosure {
1053        func: DefId,
1054        type_args: Vec<Ty>,
1055        captures: Vec<Expr>,
1056    },
1057    /// Call a function. `type_args` instantiate the callee's generics when
1058    /// `func` is `Callee::Def`.
1059    Call {
1060        func: Callee,
1061        type_args: Vec<Ty>,
1062        args: Vec<Expr>,
1063    },
1064    /// Construct a sum type variant. The expression's `ty` carries the
1065    /// concrete `Sum { args, .. }` instantiation.
1066    MakeVariant {
1067        sum: DefId,
1068        variant: u32,
1069        args: Vec<Expr>,
1070    },
1071    /// Construct a record value. `fields` are in the record's declared
1072    /// field order; the expression's `ty` is the `Record { args, .. }`
1073    /// instantiation.
1074    MakeRecord {
1075        record: DefId,
1076        fields: Vec<Expr>,
1077    },
1078    /// Read field `index` of a record value.
1079    FieldGet {
1080        target: Box<Expr>,
1081        index: u32,
1082    },
1083    /// Store `record.field = value`. `index` is the field's position, so the
1084    /// store offset is `8 * index` — the same layout `FieldGet` reads.
1085    /// Unit-typed.
1086    FieldSet {
1087        target: Box<Expr>,
1088        index: u32,
1089        value: Box<Expr>,
1090    },
1091    /// Construct a heap array `{ len, elems... }`; the expression's `ty`
1092    /// is the `Array(elem)` type.
1093    MakeArray {
1094        elems: Vec<Expr>,
1095    },
1096    /// `[init; len]` — a heap array of `len` slots, every one holding `init`,
1097    /// where `len` is a runtime `Int`. Unlike `MakeArray` the element count is
1098    /// not known statically, so MIR lowering allocates and then fills with a
1099    /// loop. The expression's `ty` is the `Array(elem)` type.
1100    ///
1101    /// `init` is evaluated **once**, and that single value is stored into every
1102    /// slot — these are not `len` copies. For a heap element type the slots are
1103    /// therefore one object rather than `len` objects: `[Vec::new(); 2]` is a
1104    /// single `Vec` in both slots, so a `push` through one is visible through
1105    /// the other. That follows from Nova's reference semantics (there is no
1106    /// `Copy` and no clone to insert per slot), and
1107    /// `tests/runtime/array_repeat.nova` executes the case so a change to
1108    /// per-slot evaluation cannot happen silently.
1109    ArrayRepeat {
1110        init: Box<Expr>,
1111        len: Box<Expr>,
1112    },
1113    /// Read `target[index]` (bounds-checked). `target` is an array.
1114    Index {
1115        target: Box<Expr>,
1116        index: Box<Expr>,
1117    },
1118    /// Assign `target[index] = value` (bounds-checked); unit-typed.
1119    IndexSet {
1120        target: Box<Expr>,
1121        index: Box<Expr>,
1122        value: Box<Expr>,
1123    },
1124    /// The length of an array (`arr.len()`).
1125    ArrayLen {
1126        target: Box<Expr>,
1127    },
1128    /// A trait method call, resolved to a concrete impl during monomorphization
1129    /// (static dispatch). `self_ty` is the `Self` type — concrete for a call on
1130    /// a known type, or `Param(k)` inside a generic function (dispatch through
1131    /// that parameter's bound) until substitution makes it concrete.
1132    TraitCall {
1133        trait_id: DefId,
1134        method: u32,
1135        self_ty: Ty,
1136        /// The method's own generic arguments (`Param(1..)`), inferred per call
1137        /// site; empty for a non-generic trait method.
1138        type_args: Vec<Ty>,
1139        /// The receiver of `receiver.method(args)`, or `None` for a trait
1140        /// associated function called as `Type::method(args)` — one that
1141        /// declares no `self` (see [`TraitMethod::has_self`]). `None` rather
1142        /// than a flag beside a placeholder expression so that lowering a
1143        /// receiver that does not exist is not representable: there is nothing
1144        /// to lower, so no consumer can accidentally pass one.
1145        receiver: Option<Box<Expr>>,
1146        args: Vec<Expr>,
1147    },
1148    /// A non-short-circuit binary operation.
1149    Binary {
1150        op: BinOp,
1151        lhs: Box<Expr>,
1152        rhs: Box<Expr>,
1153    },
1154    /// Short-circuit `&&`.
1155    LogicalAnd {
1156        lhs: Box<Expr>,
1157        rhs: Box<Expr>,
1158    },
1159    /// Short-circuit `||`.
1160    LogicalOr {
1161        lhs: Box<Expr>,
1162        rhs: Box<Expr>,
1163    },
1164    Unary {
1165        op: UnOp,
1166        expr: Box<Expr>,
1167    },
1168    /// `let` binding as a unit-typed statement expression.
1169    Let {
1170        local: LocalId,
1171        init: Box<Expr>,
1172    },
1173    /// Assignment to a mutable local; unit-typed.
1174    Assign {
1175        local: LocalId,
1176        value: Box<Expr>,
1177    },
1178    /// `{ stmts; trailing }` — value is `trailing` or unit.
1179    Block {
1180        stmts: Vec<Expr>,
1181        trailing: Option<Box<Expr>>,
1182    },
1183    If {
1184        cond: Box<Expr>,
1185        then: Box<Expr>,
1186        else_: Option<Box<Expr>>,
1187    },
1188    While {
1189        cond: Box<Expr>,
1190        body: Box<Expr>,
1191    },
1192    /// Exit the innermost enclosing loop; diverging (`Never`).
1193    Break,
1194    /// Skip to the next iteration of the innermost loop; diverging.
1195    Continue,
1196    Match {
1197        scrutinee: Box<Expr>,
1198        arms: Vec<Arm>,
1199    },
1200    Return(Option<Box<Expr>>),
1201    /// Convert a primitive to `String` (from string interpolation).
1202    ToStr(Box<Expr>),
1203    /// Concatenate `String` parts (from string interpolation).
1204    StrConcat(Vec<Expr>),
1205    /// `e.await` inside an `async fn`. `e` has type `Future<T>` and the
1206    /// `Await` expression has type `T`.
1207    ///
1208    /// Only ever appears inside an `async fn`'s body, which `nova-typeck`'s
1209    /// `fcx.in_async` is what enforces — so nothing downstream needs a guard
1210    /// against one outside a function that is [`Function::is_async`].
1211    ///
1212    /// What this node becomes is `nova-mir`'s: `lower.rs` emits a `Stmt::Await`
1213    /// marker and `async_lower.rs`'s block split turns that into suspend/resume
1214    /// control flow. **Deliberately not described further here.** A description
1215    /// of another crate's behaviour, kept in this one, goes false the moment that
1216    /// behaviour changes and has nothing to keep it honest — so this doc holds
1217    /// only the two facts above, both of which are about this node and this
1218    /// crate, and `nova-mir`'s own docs carry the contract.
1219    Await(Box<Expr>),
1220}
1221
1222/// One `match` arm.
1223#[derive(Debug, Clone)]
1224pub struct Arm {
1225    pub pattern: Pattern,
1226    pub body: Expr,
1227    pub span: Span,
1228}
1229
1230/// Patterns after checking. Phase 1 supports flat patterns: variant
1231/// destructuring binds directly to locals (or discards with `None`).
1232#[derive(Debug, Clone)]
1233pub enum Pattern {
1234    /// `_`
1235    Wildcard,
1236    /// A catch-all binding: `n => ...`
1237    Bind(LocalId),
1238    LitInt(i64),
1239    LitBool(bool),
1240    LitStr(String),
1241    /// `Variant(a, _, c)` — one binder slot per payload field.
1242    Variant {
1243        sum: DefId,
1244        variant: u32,
1245        binders: Vec<Option<LocalId>>,
1246    },
1247}
1248
1249#[cfg(test)]
1250mod tests {
1251    use super::*;
1252
1253    #[test]
1254    fn subst_recurses_into_a_projection_without_normalizing() {
1255        use nova_resolver::DefId;
1256        let proj = Ty::Assoc {
1257            on: Box::new(Ty::Param(0)),
1258            assoc: DefId(7),
1259        };
1260        // subst has no impl table, so it substitutes and stops. Normalizing is
1261        // the caller's job (typeck's `normalize`, or mono after subst).
1262        assert_eq!(
1263            proj.subst(&[Ty::Int]),
1264            Ty::Assoc {
1265                on: Box::new(Ty::Int),
1266                assoc: DefId(7)
1267            }
1268        );
1269    }
1270
1271    #[test]
1272    fn a_projection_has_no_head_and_no_param_of_its_own() {
1273        use nova_resolver::DefId;
1274        let proj = Ty::Assoc {
1275            on: Box::new(Ty::Param(2)),
1276            assoc: DefId(7),
1277        };
1278        // No head: impl lookup cannot key on an unnormalized projection.
1279        assert!(proj.head().is_none());
1280        // But it does mention the parameter in its Self type, which
1281        // `E0073`'s unused-impl-parameter check depends on.
1282        assert!(proj.mentions_param(2));
1283        assert!(!proj.mentions_param(0));
1284    }
1285
1286    #[test]
1287    fn a_projection_reports_the_params_and_vars_inside_its_self_type() {
1288        use nova_resolver::DefId;
1289        let on_param = Ty::Assoc {
1290            on: Box::new(Ty::Param(0)),
1291            assoc: DefId(7),
1292        };
1293        assert!(on_param.has_params(), "a projection on a Param is generic");
1294        assert!(!on_param.has_vars());
1295
1296        let on_var = Ty::Assoc {
1297            on: Box::new(Ty::Var(3)),
1298            assoc: DefId(7),
1299        };
1300        // Assoc-on-Var is meant to be unreachable (E0011 fires first), but
1301        // typeck's finalize checks are the net for that argument being wrong,
1302        // and they are driven by has_vars.
1303        assert!(
1304            on_var.has_vars(),
1305            "a projection on a Var still contains a var"
1306        );
1307        assert!(!on_var.has_params());
1308
1309        let concrete = Ty::Assoc {
1310            on: Box::new(Ty::Int),
1311            assoc: DefId(7),
1312        };
1313        assert!(!concrete.has_params());
1314        assert!(!concrete.has_vars());
1315    }
1316
1317    // `self_types_overlap`'s two new arms, mutation-tested: the reviewer
1318    // found that mutating this function to unconditional `false` (the
1319    // silent-miscompile direction the design doc warns about) left the full
1320    // workspace suite green before this test existed.
1321    #[test]
1322    fn self_types_overlap_treats_a_projection_conservatively() {
1323        use nova_resolver::DefId;
1324        let item = DefId(7);
1325        let other = DefId(8);
1326
1327        // Same associated type, Self types that provably differ: no overlap.
1328        let on_int = Ty::Assoc {
1329            on: Box::new(Ty::Int),
1330            assoc: item,
1331        };
1332        let on_bool = Ty::Assoc {
1333            on: Box::new(Ty::Bool),
1334            assoc: item,
1335        };
1336        assert!(
1337            !self_types_overlap(&on_int, 0, &on_bool, 0),
1338            "same associated type, but Int and Bool can never be the same Self type"
1339        );
1340
1341        // Same associated type, Self types that could unify (a generic
1342        // parameter against a concrete type): overlap.
1343        let on_param = Ty::Assoc {
1344            on: Box::new(Ty::Param(0)),
1345            assoc: item,
1346        };
1347        assert!(
1348            self_types_overlap(&on_param, 1, &on_int, 0),
1349            "Param(0) can be instantiated to Int, so these can coincide"
1350        );
1351
1352        // Different associated types: nothing is known about either, so the
1353        // conservative answer is still overlap.
1354        let other_assoc = Ty::Assoc {
1355            on: Box::new(Ty::Int),
1356            assoc: other,
1357        };
1358        assert!(
1359            self_types_overlap(&on_int, 0, &other_assoc, 0),
1360            "different associated types cannot be proven disjoint, so assume overlap"
1361        );
1362
1363        // A projection against a non-projection: always assumed to overlap,
1364        // in both argument orders.
1365        assert!(self_types_overlap(&on_int, 0, &Ty::Int, 0));
1366        assert!(self_types_overlap(&Ty::Bool, 0, &on_int, 0));
1367    }
1368
1369    // `match_pattern`'s new arm, mutation-tested: the reviewer found that
1370    // mutating it to unconditional `false` also left the full workspace
1371    // suite green before this test existed.
1372    #[test]
1373    fn match_pattern_treats_assoc_structurally() {
1374        use nova_resolver::DefId;
1375        let item = DefId(7);
1376        let other = DefId(8);
1377
1378        // Same associated type: the Self-type pattern matches structurally
1379        // and records its Param binding like any other position.
1380        let pattern = Ty::Assoc {
1381            on: Box::new(Ty::Param(0)),
1382            assoc: item,
1383        };
1384        let ground = Ty::Assoc {
1385            on: Box::new(Ty::Int),
1386            assoc: item,
1387        };
1388        let mut out = Vec::new();
1389        assert!(pattern.match_pattern(&ground, &mut out));
1390        assert_eq!(out, vec![Some(Ty::Int)]);
1391
1392        // Different associated types: never a match, even with identical
1393        // Self types.
1394        let different_assoc = Ty::Assoc {
1395            on: Box::new(Ty::Int),
1396            assoc: other,
1397        };
1398        let same_self = Ty::Assoc {
1399            on: Box::new(Ty::Int),
1400            assoc: item,
1401        };
1402        assert!(!same_self.match_pattern(&different_assoc, &mut Vec::new()));
1403
1404        // A projection on only one side is a structural mismatch, not a
1405        // partial match, in both argument orders.
1406        assert!(!pattern.match_pattern(&Ty::Int, &mut Vec::new()));
1407        assert!(!Ty::Int.match_pattern(&ground, &mut Vec::new()));
1408    }
1409
1410    #[test]
1411    fn has_assoc_finds_a_projection_at_every_nesting_depth() {
1412        use nova_resolver::DefId;
1413        let p = || Ty::Assoc {
1414            on: Box::new(Ty::Int),
1415            assoc: DefId(7),
1416        };
1417        assert!(p().has_assoc());
1418        assert!(Ty::Array(Box::new(p())).has_assoc());
1419        assert!(
1420            Ty::Future(Box::new(p())).has_assoc(),
1421            "a future's output counts too, not only an array's element"
1422        );
1423        assert!(
1424            Ty::Record {
1425                def_id: DefId(1),
1426                args: vec![Ty::Bool, p()],
1427            }
1428            .has_assoc(),
1429            "not only the first argument"
1430        );
1431        assert!(Ty::Sum {
1432            def_id: DefId(1),
1433            args: vec![p()],
1434        }
1435        .has_assoc());
1436        assert!(
1437            Ty::Fn {
1438                params: vec![Ty::Int],
1439                ret: Box::new(p()),
1440            }
1441            .has_assoc(),
1442            "the return type counts, not only the parameters"
1443        );
1444        assert!(Ty::Fn {
1445            params: vec![p()],
1446            ret: Box::new(Ty::Int),
1447        }
1448        .has_assoc());
1449        // And says no when there is genuinely nothing to normalize, including
1450        // for the compound types it recurses into.
1451        assert!(!Ty::Int.has_assoc());
1452        assert!(!Ty::Param(0).has_assoc());
1453        assert!(!Ty::Array(Box::new(Ty::Int)).has_assoc());
1454        assert!(!Ty::Future(Box::new(Ty::Int)).has_assoc());
1455        assert!(!Ty::Fn {
1456            params: vec![Ty::Int],
1457            ret: Box::new(Ty::Bool),
1458        }
1459        .has_assoc());
1460    }
1461
1462    #[test]
1463    fn future_recurses_into_its_output_type() {
1464        // Each predicate must look THROUGH the Future, not past it. A `_ => false`
1465        // catch-all would pass a test that only ever asked about Future<Int>.
1466        let p = || Ty::Param(0);
1467        assert!(Ty::Future(Box::new(p())).has_params());
1468        assert!(!Ty::Future(Box::new(Ty::Int)).has_params());
1469        assert!(Ty::Future(Box::new(Ty::Var(0))).has_vars());
1470        assert!(!Ty::Future(Box::new(Ty::Int)).has_vars());
1471        assert!(Ty::Future(Box::new(Ty::Error)).has_error());
1472        assert!(!Ty::Future(Box::new(Ty::Int)).has_error());
1473        assert!(Ty::Future(Box::new(p())).mentions_param(0));
1474        assert!(!Ty::Future(Box::new(p())).mentions_param(1));
1475    }
1476
1477    #[test]
1478    fn future_substitutes_its_output_type() {
1479        let subbed = Ty::Future(Box::new(Ty::Param(0))).subst(&[Ty::Float]);
1480        assert_eq!(subbed, Ty::Future(Box::new(Ty::Float)));
1481    }
1482
1483    #[test]
1484    fn future_match_pattern_binds_through_the_output() {
1485        // Recovers T from Future<T> against a concrete Future<Bool>.
1486        let mut out = Vec::new();
1487        assert!(Ty::Future(Box::new(Ty::Param(0)))
1488            .match_pattern(&Ty::Future(Box::new(Ty::Bool)), &mut out));
1489        assert_eq!(out, vec![Some(Ty::Bool)]);
1490        // And refuses a structural mismatch rather than binding anything.
1491        let mut out2 = Vec::new();
1492        assert!(!Ty::Future(Box::new(Ty::Param(0)))
1493            .match_pattern(&Ty::Array(Box::new(Ty::Bool)), &mut out2));
1494    }
1495
1496    // === normalize_ty ===
1497
1498    /// `impl<generics> ? for self_ty { type <assoc> = <bound> }` — the minimum
1499    /// an `ImplInfo` needs to be for `normalize_ty` to read it. `trait_id` is
1500    /// deliberately `None` on some of these: `normalize_ty` keys on the
1501    /// associated type's own `DefId`, which belongs to exactly one trait, so it
1502    /// never has to consult `trait_id` — and a test that set it would hide a
1503    /// lookup that secretly depended on it.
1504    fn imp(self_ty: Ty, generics: u32, bindings: Vec<(DefId, Ty)>) -> ImplInfo {
1505        ImplInfo {
1506            trait_id: None,
1507            self_head: self_ty.head().expect("test self types have a head"),
1508            self_ty,
1509            generics,
1510            bounds: Vec::new(),
1511            methods: Vec::new(),
1512            assoc_bindings: bindings,
1513        }
1514    }
1515
1516    fn rec(def: u32, args: Vec<Ty>) -> Ty {
1517        Ty::Record {
1518            def_id: DefId(def),
1519            args,
1520        }
1521    }
1522
1523    fn proj(on: Ty, assoc: u32) -> Ty {
1524        Ty::Assoc {
1525            on: Box::new(on),
1526            assoc: DefId(assoc),
1527        }
1528    }
1529
1530    const ITEM: u32 = 7;
1531
1532    #[test]
1533    fn normalize_resolves_a_projection_through_the_impls_own_arguments() {
1534        // `impl<T> It for W<T> { type Item = T }`, projected onto `W<Int>`.
1535        let impls = [imp(
1536            rec(1, vec![Ty::Param(0)]),
1537            1,
1538            vec![(DefId(ITEM), Ty::Param(0))],
1539        )];
1540        assert_eq!(
1541            normalize_ty(&proj(rec(1, vec![Ty::Int]), ITEM), &impls),
1542            Ok(Ty::Int)
1543        );
1544    }
1545
1546    #[test]
1547    fn normalize_picks_the_impl_whose_self_type_matches() {
1548        // Two impls binding the *same* associated type on different heads. With
1549        // only one impl in the table, "looks the impl up" and "takes the only
1550        // impl" are indistinguishable.
1551        let impls = [
1552            imp(
1553                rec(1, vec![Ty::Param(0)]),
1554                1,
1555                vec![(DefId(ITEM), Ty::Param(0))],
1556            ),
1557            imp(rec(2, vec![]), 0, vec![(DefId(ITEM), Ty::Bool)]),
1558        ];
1559        assert_eq!(
1560            normalize_ty(&proj(rec(1, vec![Ty::Char]), ITEM), &impls),
1561            Ok(Ty::Char),
1562            "W<Char>::Item comes from the W impl"
1563        );
1564        assert_eq!(
1565            normalize_ty(&proj(rec(2, vec![]), ITEM), &impls),
1566            Ok(Ty::Bool),
1567            "K::Item comes from the K impl"
1568        );
1569    }
1570
1571    #[test]
1572    fn normalize_rejects_an_impl_that_shares_the_head_but_does_not_fit() {
1573        // Two impls on the SAME head, one structurally non-matching:
1574        // `impl<T> It for Pair<T, T>` does not cover `Pair<Int, Bool>`, so the
1575        // projection must resolve through `impl It for Pair<Int, Bool>` instead.
1576        //
1577        // This is the only test of the `match_args` gate that a head-only
1578        // implementation fails. `normalize_picks_the_impl_whose_self_type_matches`
1579        // and `normalize_recurses_into_every_compound_type` both discriminate by
1580        // *head* alone, so dropping the gate (`i.match_args(&on)?` →
1581        // `.unwrap_or_default()`) survives them: the wrong impl is selected, its
1582        // `Param(0)` substitutes against an empty argument list to `Ty::Error`,
1583        // and `Ty::Error` unifies with anything downstream. Head-only impl
1584        // selection is the miscompile class this project has already shipped once
1585        // (see the comment on the gate), which is why it gets its own test.
1586        let pair = |a: Ty, b: Ty| rec(1, vec![a, b]);
1587        let impls = [
1588            imp(
1589                pair(Ty::Param(0), Ty::Param(0)),
1590                1,
1591                vec![(DefId(ITEM), Ty::Param(0))],
1592            ),
1593            imp(pair(Ty::Int, Ty::Bool), 0, vec![(DefId(ITEM), Ty::String)]),
1594        ];
1595        assert_eq!(
1596            normalize_ty(&proj(pair(Ty::Int, Ty::Bool), ITEM), &impls),
1597            Ok(Ty::String),
1598            "Pair<Int, Bool> does not fit Pair<T, T>, so the concrete impl answers"
1599        );
1600        // The control: the generic impl *is* selected when the self type fits it.
1601        // Without this, the test above would also pass if `Pair<T, T>` were never
1602        // selectable at all.
1603        assert_eq!(
1604            normalize_ty(&proj(pair(Ty::Int, Ty::Int), ITEM), &impls),
1605            Ok(Ty::Int),
1606            "Pair<Int, Int> does fit Pair<T, T>"
1607        );
1608    }
1609
1610    #[test]
1611    fn normalize_resolves_a_projection_whose_self_type_is_itself_a_projection() {
1612        // `Assoc { on: Assoc { .. } }` — the shape that makes pre-normalizing
1613        // `on` load-bearing. `W::Mid` resolves to `K`, and only then does the
1614        // outer projection have a head to look `Item` up on.
1615        //
1616        // Unwritable in Nova source (a binding cannot name another concrete
1617        // type's associated type), but `subst` builds it: monomorphization can
1618        // substitute a projection into `Assoc { on: Param(k) }`. Without the
1619        // pre-normalization the outer `on` has no `head()` and the whole thing is
1620        // returned unresolved.
1621        //
1622        // `normalize_recurses_into_every_compound_type`'s last case looks like
1623        // this but is not: there the projection is *inside* a record that already
1624        // has a head, so the outer lookup succeeds either way.
1625        let mid = 9;
1626        let w = rec(1, vec![]);
1627        let k = rec(2, vec![]);
1628        let impls = [
1629            imp(w.clone(), 0, vec![(DefId(mid), k)]),
1630            imp(rec(2, vec![]), 0, vec![(DefId(ITEM), Ty::Bool)]),
1631        ];
1632        assert_eq!(
1633            normalize_ty(&proj(proj(w, mid), ITEM), &impls),
1634            Ok(Ty::Bool)
1635        );
1636    }
1637
1638    #[test]
1639    fn normalize_only_reads_the_binding_for_the_projected_associated_type() {
1640        // One impl binding two associated types. Reading the first entry
1641        // regardless of key gives `Ty::Int` for both.
1642        let other = 8;
1643        let impls = [imp(
1644            rec(1, vec![]),
1645            0,
1646            vec![(DefId(ITEM), Ty::Int), (DefId(other), Ty::String)],
1647        )];
1648        assert_eq!(
1649            normalize_ty(&proj(rec(1, vec![]), ITEM), &impls),
1650            Ok(Ty::Int)
1651        );
1652        assert_eq!(
1653            normalize_ty(&proj(rec(1, vec![]), other), &impls),
1654            Ok(Ty::String)
1655        );
1656    }
1657
1658    #[test]
1659    fn normalize_leaves_a_projection_on_a_generic_parameter_alone() {
1660        // `Assoc { on: Param(k) }` has no head, so no impl can be selected. It
1661        // is monomorphization's job (Task 7), not an error and not `Ty::Error`.
1662        let impls = [imp(rec(1, vec![]), 0, vec![(DefId(ITEM), Ty::Int)])];
1663        let abstract_proj = proj(Ty::Param(0), ITEM);
1664        assert_eq!(normalize_ty(&abstract_proj, &impls), Ok(abstract_proj));
1665    }
1666
1667    #[test]
1668    fn normalize_leaves_a_projection_with_no_matching_impl_alone() {
1669        // No impl of the owning trait for `Int`: the projection stays, so the
1670        // caller's unification reports a type error naming the projection
1671        // rather than a normalizer that invented `Ty::Error`.
1672        let impls = [imp(rec(1, vec![]), 0, vec![(DefId(ITEM), Ty::Int)])];
1673        let unresolvable = proj(Ty::Bool, ITEM);
1674        assert_eq!(normalize_ty(&unresolvable, &impls), Ok(unresolvable));
1675    }
1676
1677    #[test]
1678    fn normalize_recurses_into_every_compound_type() {
1679        // A projection nested inside a compound type must be reached. An
1680        // implementation that only handles a top-level `Assoc` passes every
1681        // test whose projection is the whole type.
1682        let impls = [
1683            imp(rec(1, vec![]), 0, vec![(DefId(ITEM), Ty::Int)]),
1684            imp(rec(2, vec![Ty::Param(0)]), 1, vec![(DefId(ITEM), Ty::Char)]),
1685        ];
1686        let p = || proj(rec(1, vec![]), ITEM);
1687        assert_eq!(
1688            normalize_ty(&Ty::Array(Box::new(p())), &impls),
1689            Ok(Ty::Array(Box::new(Ty::Int)))
1690        );
1691        // A `clone`-without-recursing arm would return this unchanged
1692        // (`Ok(Ty::Future(Box::new(p())))`), leaving the projection intact.
1693        assert_eq!(
1694            normalize_ty(&Ty::Future(Box::new(p())), &impls),
1695            Ok(Ty::Future(Box::new(Ty::Int)))
1696        );
1697        assert_eq!(
1698            normalize_ty(&rec(3, vec![p(), Ty::Bool]), &impls),
1699            Ok(rec(3, vec![Ty::Int, Ty::Bool]))
1700        );
1701        assert_eq!(
1702            normalize_ty(
1703                &Ty::Sum {
1704                    def_id: DefId(4),
1705                    args: vec![p()]
1706                },
1707                &impls
1708            ),
1709            Ok(Ty::Sum {
1710                def_id: DefId(4),
1711                args: vec![Ty::Int]
1712            })
1713        );
1714        assert_eq!(
1715            normalize_ty(
1716                &Ty::Fn {
1717                    params: vec![p(), Ty::Bool],
1718                    ret: Box::new(p())
1719                },
1720                &impls
1721            ),
1722            Ok(Ty::Fn {
1723                params: vec![Ty::Int, Ty::Bool],
1724                ret: Box::new(Ty::Int)
1725            })
1726        );
1727        // And inside the Self type of another projection.
1728        assert_eq!(
1729            normalize_ty(&proj(rec(2, vec![p()]), ITEM), &impls),
1730            Ok(Ty::Char),
1731            "the inner W::Item resolves to Int, making the outer K<Int>::Item"
1732        );
1733    }
1734
1735    #[test]
1736    fn normalize_follows_a_chain_of_bindings_to_the_end() {
1737        // `type A = Self::B` with `type B = Int`: one resolution step is not
1738        // enough, so the result has to be re-normalized. This is the behaviour
1739        // that forces the step guard to exist.
1740        let a = 7;
1741        let b = 8;
1742        let self_ty = rec(1, vec![]);
1743        let impls = [imp(
1744            self_ty.clone(),
1745            0,
1746            vec![(DefId(a), proj(self_ty.clone(), b)), (DefId(b), Ty::Int)],
1747        )];
1748        assert_eq!(normalize_ty(&proj(self_ty, a), &impls), Ok(Ty::Int));
1749    }
1750
1751    #[test]
1752    fn normalize_gives_up_on_a_cyclic_binding_instead_of_diverging() {
1753        // typeck rejects this at collection (E0077) and poisons the binding, so
1754        // this shape is unreachable from source today. The guard exists because
1755        // that argument covers *bindings*, not every path that can build a
1756        // projection — and a compiler that hangs is worse than one that reports
1757        // a limit. This test's other value is that it completes.
1758        let self_ty = rec(1, vec![]);
1759        let cycle = proj(self_ty.clone(), ITEM);
1760        let impls = [imp(self_ty, 0, vec![(DefId(ITEM), cycle.clone())])];
1761        assert_eq!(
1762            normalize_ty(&cycle, &impls),
1763            Err(NormalizeOverflow {
1764                at: cycle,
1765                // The chain, not the total: a cycle resolves one link at a time
1766                // and never widens, so it is the depth allowance that stops it.
1767                limit: NormalizeLimit::Depth
1768            })
1769        );
1770    }
1771
1772    #[test]
1773    fn normalize_gives_up_on_a_binding_that_grows_without_bound() {
1774        // `type Item = [Self::Item]`, the nested cycle: each step is a strictly
1775        // larger type rather than the same one, so a guard implemented as a
1776        // "have I seen this exact projection before" set would loop forever
1777        // where a step counter does not.
1778        let self_ty = rec(1, vec![]);
1779        let grows = Ty::Array(Box::new(proj(self_ty.clone(), ITEM)));
1780        let impls = [imp(self_ty.clone(), 0, vec![(DefId(ITEM), grows)])];
1781        assert_eq!(
1782            normalize_ty(&proj(self_ty.clone(), ITEM), &impls),
1783            Err(NormalizeOverflow {
1784                at: proj(self_ty, ITEM),
1785                // Depth, and this case is why the depth allowance cannot simply be
1786                // raised to match the step allowance: each resolution nests one
1787                // `Array` deeper, so recursion depth tracks it. At 10 000 this
1788                // overflows a test thread's 2 MiB stack instead of reporting.
1789                limit: NormalizeLimit::Depth
1790            }),
1791            "reports overflow rather than diverging"
1792        );
1793    }
1794
1795    #[test]
1796    fn normalize_admits_a_chain_longer_than_a_couple_of_links() {
1797        // The limit must be generous enough that a legitimate chain never trips
1798        // it. Sixteen links is far past anything a person writes and well inside
1799        // the limit.
1800        let self_ty = rec(1, vec![]);
1801        let n = 16u32;
1802        let mut bindings: Vec<(DefId, Ty)> = (0..n)
1803            .map(|i| (DefId(100 + i), proj(self_ty.clone(), 101 + i)))
1804            .collect();
1805        bindings.push((DefId(100 + n), Ty::Int));
1806        let impls = [imp(self_ty.clone(), 0, bindings)];
1807        assert_eq!(normalize_ty(&proj(self_ty, 100), &impls), Ok(Ty::Int));
1808    }
1809
1810    #[test]
1811    fn normalize_bounds_total_work_not_only_chain_depth() {
1812        // `type A(k) = Pair<Self::A(k+1), Self::A(k+1)>` down to `type A(n) = Int`.
1813        // No cycle, and the chain is `n` links — half the depth limit — but the
1814        // resolved type is `2^n` nodes, so a budget charged only when a projection
1815        // is resolved and passed *unchanged* into each compound arm does
1816        // exponential work while remaining, technically, convergent. At n=32 that
1817        // is four billion nodes.
1818        //
1819        // This is the test that separates "cannot diverge" from "does bounded
1820        // work", and the only overflow test here that is not a cycle — a cycle is
1821        // caught by the depth allowance alone, which is why the review found this
1822        // class unguarded. Measured through `nova check` before the step
1823        // allowance existed: n=20 took 12.9 s and n=24 (a 60-line source file,
1824        // accepted) had not finished after two minutes.
1825        let n = 32u32;
1826        let self_ty = rec(1, vec![]);
1827        let pair = |a: Ty, b: Ty| rec(2, vec![a, b]);
1828        let mut bindings: Vec<(DefId, Ty)> = (0..n)
1829            .map(|i| {
1830                let next = proj(self_ty.clone(), 101 + i);
1831                (DefId(100 + i), pair(next.clone(), next))
1832            })
1833            .collect();
1834        bindings.push((DefId(100 + n), Ty::Int));
1835        let impls = [imp(self_ty.clone(), 0, bindings)];
1836        let input = proj(self_ty, 100);
1837        assert_eq!(
1838            normalize_ty(&input, &impls),
1839            Err(NormalizeOverflow {
1840                at: input,
1841                // Steps, not depth: n=32 is inside the depth limit of 64, so
1842                // asserting the limit is what proves the *new* allowance is doing
1843                // the work rather than the old one catching it by luck.
1844                limit: NormalizeLimit::Steps
1845            }),
1846            "a diagnostic, not a hang — and not `Ty::Error`, which unifies with \
1847             anything and would make this a wrong answer instead"
1848        );
1849    }
1850
1851    #[test]
1852    fn normalize_admits_a_branching_chain_that_stays_within_the_allowance() {
1853        // The control for the test above: branching is not itself the problem, so
1854        // a modest branching chain must still resolve. Ten levels is 1 024 leaves
1855        // and ~2 047 nodes, comfortably inside 10 000, and the result is checked
1856        // in full — a guard that rejected all branching would pass an assertion
1857        // that only looked at `is_ok`.
1858        let n = 10u32;
1859        let self_ty = rec(1, vec![]);
1860        let pair = |a: Ty, b: Ty| rec(2, vec![a, b]);
1861        let mut bindings: Vec<(DefId, Ty)> = (0..n)
1862            .map(|i| {
1863                let next = proj(self_ty.clone(), 101 + i);
1864                (DefId(100 + i), pair(next.clone(), next))
1865            })
1866            .collect();
1867        bindings.push((DefId(100 + n), Ty::Int));
1868        let impls = [imp(self_ty.clone(), 0, bindings)];
1869        let mut expected = Ty::Int;
1870        for _ in 0..n {
1871            expected = pair(expected.clone(), expected);
1872        }
1873        assert_eq!(normalize_ty(&proj(self_ty, 100), &impls), Ok(expected));
1874    }
1875}