brink-analyzer 0.0.17

//! `signature`/`infer_body`/`type_diagnostics` — the checker substrate
//! (typed-mode-spec §2, TM-1). **Advisory-only**: this module produces
//! inference *results* for later consumers (hover, TM-3 strict mode); it
//! changes no compiler behavior and the LIR/codegen/runtime never read it.
//!
//! ## The firewall
//!
//! `infer_body(A)` (here, [`body::infer_def_body`] driven by
//! [`infer_project`]) reads only `signature(B)` for every def `B` it calls —
//! never `B`'s body. Two kinds of "signature" satisfy that rule:
//!
//! - A **global** (`VAR`/`CONST`) reads its declaration-derived
//!   [`crate::Sig::value_type`] — the existing phase-0 stub, untouched by
//!   this module (see `crate::signature`'s `signature_is_declaration_derived_only`
//!   test, which this module must never make fail).
//! - A **callable** (knot/stitch) reads its entry in `known_sigs`: either
//!   another SCC's already-finalized [`InferredSig`], or — for a call
//!   *within* the SCC currently being solved — that SCC's current fixpoint
//!   estimate. Call-site-driven inference (letting a caller's argument
//!   types flow backward into a callee's params) is never done; only a
//!   callee's own already-computed signature flows forward into how the
//!   caller's argument expressions are typed.
//! - An **`EXTERNAL` binding** (issue #786) reads its own entry in
//!   `known_sigs` too, seeded once up front by [`collect_external_sigs`]
//!   from the registered `HostManifest` rather than solved by the fixpoint
//!   (an external has no body to infer) — a call to it types its arguments
//!   exactly like a callable's, through the same `known_sigs` lookup.
//!
//! ## SCC fixpoint
//!
//! [`graph::topo_order`] batches every inferable def into strongly-connected
//! components, ordered so a component is solved only after every *other*
//! component it calls is finalized. A component may contain more than one
//! def (mutual recursion) — those solve together: seed every member with an
//! `Unknown` working signature, re-run [`body::infer_def_body`] across the
//! whole component, and repeat until no member's signature changes (or
//! [`MAX_SCC_ITERATIONS`] is hit — guard against unbounded growth, house
//! rule). This is the monomorphic Haskell-style binding-group solve spec §2
//! asks for.
//!
//! ## Laziness (perf)
//!
//! [`infer_project`] is not wired into `analysis_query`, `lir_query`,
//! `diagnostics_query`, or `story_data_query` — nothing in the existing
//! compile/IDE path calls it. The brink-db salsa wrapper
//! (`type_inference_query`) is therefore only ever computed when a consumer
//! explicitly asks for `infer_body`/`type_diagnostics`, which today is
//! nobody: this slice is pure substrate. See the PR's benchmark report for
//! the before/after warm/cold numbers this predicts (no measurable delta on
//! the existing paths).

mod body;
mod effects;
mod graph;
mod intrinsics;
mod ty;

pub(crate) use body::{is_string_numeric_concat, lambda_own_bindings};
pub(crate) use intrinsics::{intrinsic_effects, intrinsic_returns_option};

use std::collections::{BTreeMap, BTreeSet};

use brink_format::{DefinitionId, DefinitionTag};
use brink_ir::{
    AssignOp, BaseType, Block, DocBlock, FileId, HirFile, HostManifest, Name, Param, ResolutionMap,
    SymbolIndex, SymbolKind, TypeExpr, TypeRef,
};
use rowan::TextRange;

pub use effects::{EffectAtoms, EffectRow, solve_scc_effects};
pub use graph::{CallGraph, SccGraph, scc_graph};
pub use ty::{
    CoalesceError, FnRow, TowerTy, Ty, assignable, coalesce, erase_fn_rows, ref_assignable, unify,
    unify_all,
};

use body::{BodyCtx, infer_def_body};
use graph::topo_order;

/// `TextRange` has no `Ord` impl (ranges have no single natural total
/// order), so every `BTreeMap` keyed by a reference's source range in this
/// module uses this `(start, end)` `u32` pair instead.
fn range_key(range: TextRange) -> (u32, u32) {
    (range.start().into(), range.end().into())
}

/// Caps the number of re-solve rounds for one SCC batch (guard against
/// unbounded growth, house rule). Convergence is expected within a handful
/// of rounds for this finite, monomorphic, no-overloading type universe —
/// a genuinely pathological program that never stabilizes still terminates
/// with whatever partial signature this cap leaves it at, which is legal
/// (unresolved slots read as `Unknown`), not a hang.
const MAX_SCC_ITERATIONS: usize = 8;

/// A def's inferred signature: positional param types (declaration order)
/// plus a return type. The generalized, per-def result of a body's fixpoint
/// solve — what a *caller* reads (never the caller reading the callee's
/// body directly; that's the firewall).
#[derive(Debug, Clone, PartialEq, Eq, Default)]
pub struct InferredSig {
    pub params: Vec<Ty>,
    pub return_ty: Ty,
}

/// The full inferred picture of one def's body: params, every local
/// (params ∪ temps) by name, and the return type. A superset of
/// [`InferredSig`] — `signatures` is the firewall-facing projection,
/// `bodies` is what a hover/diagnostic consumer (TM-5) wants.
#[derive(Debug, Clone, PartialEq, Eq, Default)]
pub struct BodyTypes {
    pub params: Vec<(String, Ty)>,
    pub locals: BTreeMap<String, Ty>,
    pub return_ty: Ty,
    /// Issue #1028: whether the body contains at least one value-carrying
    /// `return <expr>` anywhere — see [`body::BodyResult::has_value_return`]
    /// (the field this one is copied from) for why `return_ty.is_unknown()`
    /// alone can't distinguish "never returns a value" (should infer void)
    /// from "returns a value inference couldn't pin down" (a real
    /// Unknown-escape).
    pub has_value_return: bool,
    /// T1c (docs/t1c-spec.md §4): statically-checkable facts about calls
    /// *through a value* (a callee resolving to a param/temp/VAR/CONST
    /// rather than a callable def) observed in this body, in source-walk
    /// order. Recorded unconditionally during inference (the walk is the
    /// only place argument expressions have types); **reported only by
    /// strict mode** (`strict::check` — gradual stays advisory, the runtime
    /// fault is its backstop, spec §3/§4).
    pub value_calls: Vec<ValueCallFact>,
    /// Issue #1532: every `remove(a, i)` call site in this body whose first
    /// argument is statically known to be `Ty::Array` — see
    /// `body::BodyResult::array_remove_calls`'s doc for why this is
    /// captured (the pre-#1484 array leg `remove` no longer serves).
    /// Reported only by strict mode (`strict::check_array_remove_calls`,
    /// `E149`), the same split as `value_calls`.
    pub array_remove_calls: Vec<TextRange>,
    /// Issue #1864: statically-checkable argument-type mismatches at
    /// **direct** call sites (`h("hi")`, resolving straight to a known
    /// knot/stitch via `known_sigs` — never a call through a value, which
    /// [`ValueCallFact`]/[`ValueCallKind::ArgMismatch`] already covers).
    /// Recorded unconditionally during inference, like `value_calls`;
    /// reported only by strict mode — gradual mode keeps deferring to the
    /// existing runtime type-mismatch fault as its backstop.
    ///
    /// Deliberately **excludes** an argument that is a bare `Path`
    /// resolving to a `Param`/`Temp` in the caller's own body — the exact
    /// set `InferPass::observe` unconditionally joins the callee's declared
    /// param type into, right after this check runs (see
    /// `body::InferPass::infer_call`'s doc for why). A genuine disagreement
    /// there drives that local to `Ty::Conflicted` on its own, which
    /// `strict::check_escapes` already reports as `E066` — recording a
    /// second fact here for the identical disagreement would double-report
    /// it. A `Path` argument resolving to anything else (a literal, a
    /// nested call's return value, a global `VAR`/`CONST`, an index
    /// expression, …) is unaffected by `observe` and stays fully checked.
    pub direct_call_arg_mismatches: Vec<DirectCallArgMismatch>,
    /// Issue #1877 (the remainder of #1864 left after PR #1875's direct-
    /// call-argument half): statically-checkable type mismatches at a `~
    /// temp name: T = expr` declaration initializer (against its own
    /// ascription) or a plain `~ name = expr` assignment (against the
    /// target's already-known declared type — a VAR/CONST's declaration-
    /// derived type, or an annotated `~ temp`'s ascription). A `Param`
    /// assignment target never reaches this fact at all: a param
    /// annotation is a signature-firewall slot `annotations::mismatches`
    /// (E063) already owns (compared against the body's *final* inferred
    /// param type), so checking it again here would double-report the
    /// identical disagreement. Recorded unconditionally during inference,
    /// like `direct_call_arg_mismatches`; reported only by strict mode.
    ///
    /// A `Temp` assignment target is excluded from this fact whenever
    /// `InferPass::observe`'s own join (which runs right after, on every
    /// assignment) is *already* about to drive that local to
    /// `Ty::Conflicted` on its own — that disagreement is independently
    /// reported as `E066` by `strict::check_escapes`, so recording a second
    /// fact here for it would double-report (mirrors
    /// `DirectCallArgMismatch`'s own `arg_is_observed_local` exclusion, but
    /// computed per-write rather than a blanket kind exclusion, since an
    /// assignment to an as-yet-`Unknown` local never goes `Conflicted` and
    /// would otherwise go unchecked entirely). That per-write guard is
    /// order-sensitive — a *later* read of the same temp can independently
    /// conflict it after a fact was already recorded — so
    /// `body::infer_def_body` also drops, post-walk, any fact whose
    /// target's *final* type is `Conflicted`. See
    /// `body::InferPass::check_declared_assign_target`'s doc.
    pub typed_assign_mismatches: Vec<TypedAssignMismatch>,
    /// Issue #1900 (split from #1864/#1877): a dotted struct-field
    /// assignment target (`~ p.x = expr`), with the root's declared type
    /// resolved but the field chain past it left unresolved (no shape table
    /// in this module — see [`FieldAssignMismatch`]'s own doc). Recorded
    /// unconditionally during inference, like `typed_assign_mismatches`;
    /// resolved and reported only by strict mode
    /// (`structs::check_assignments`, `E063`).
    pub field_assign_mismatches: Vec<FieldAssignMismatch>,
    /// Issue #1994 (RULED 2026-08-01, closing #1932): a lambda's own
    /// written param/return annotation disagreeing with its body-derived
    /// type — see [`LambdaAnnotationMismatch`]'s own doc for why this is a
    /// materially different severity posture from `typed_assign_mismatches`/
    /// `field_assign_mismatches` above (an eager `Error`, not a gradual
    /// `E063` advisory). Recorded unconditionally during inference, folded
    /// in from every lambda anywhere in this body (including nested ones);
    /// reported only by strict mode (`strict::check_lambda_annotation_
    /// mismatches`, `E174`).
    pub lambda_annotation_mismatches: Vec<LambdaAnnotationMismatch>,
    /// Issue #1881: per-call-site *written*-argument types for every
    /// UFCS-shaped (multi-segment, receiver-resolving) callee found in this
    /// body — see [`UfcsCallArgs`]'s own doc for why this pass records raw
    /// argument types here rather than checking them itself (the receiver
    /// resolves to a value, so this pass's own callee resolution can never
    /// see the desugared free function's declared param types the way
    /// `brink_analyzer::ufcs`'s resolution pass can). Recorded
    /// unconditionally, like `direct_call_arg_mismatches`; consumed by
    /// `ufcs::UfcsVisitor`, reported only by strict mode
    /// (`ufcs::check_strict`, `E063`).
    pub ufcs_call_args: Vec<UfcsCallArgs>,
    /// Issue #1770: see [`LambdaEscapeSlot`]. Recorded unconditionally,
    /// folded in from every lambda anywhere in this body (including nested
    /// ones) exactly like `lambda_annotation_mismatches`; reported only by
    /// strict mode (`strict::check_def`, the same `E065`/`E066` codes a
    /// top-level def's own params/temps already use).
    pub lambda_escapes: Vec<LambdaEscapeSlot>,
}

/// One UFCS-desugared call site's (`recv.name(args)` → `name(recv, args)`)
/// *written*-argument types (issue #1881) — the receiver itself is not
/// included here (its type is already known directly to
/// `ufcs::UfcsVisitor`, this fact's sole consumer, from receiver-type
/// resolution). Recorded unconditionally at every multi-segment,
/// value-resolving call this pass walks (see
/// `body::InferPass::infer_call`'s own doc for why it cannot check anything
/// against a UFCS receiver directly) — this is the raw per-argument type
/// data `brink_analyzer::ufcs`'s own resolution pass needs to complete its
/// own argument-type check against the desugared free function's
/// already-known declared param types (`InferenceResult::signatures`, keyed
/// by the *target*), without a second expression-type inference pass over
/// the same body.
///
/// Issue #1909 gave `body::InferPass` a *narrow* target lookup of its own
/// (`infer_ufcs_free_fn_result`, enough to type the call's **result**), but
/// it deliberately declines the ambiguous, struct-receiver, projected-
/// receiver and prelude cases this fact's consumer resolves properly — so
/// the split stays: the result type is inference's, the argument-type
/// *check* remains `ufcs`'s, fed by this fact.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct UfcsCallArgs {
    /// The callee `Path`'s own source range (`recv.name`'s whole span) —
    /// same convention as [`DirectCallArgMismatch::range`]; `ufcs::resolve`
    /// keys its own verdict table on this identical range (the
    /// `ResolvedRef::range` contract, issue #1561).
    pub range: TextRange,
    /// Each written argument's statically inferred type, in source order.
    pub args: Vec<Ty>,
}

/// One statically-checkable type mismatch at a **declaration-initializer or
/// assignment** site against an already-known declared type (issue #1877) —
/// the `~ temp`/plain-assignment sibling of [`DirectCallArgMismatch`], which
/// covers only direct-call arguments.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TypedAssignMismatch {
    /// The diagnostic site: the temp's own name range for a `~ temp`
    /// initializer (matching `strict::collect_temps`'s escape-check anchor),
    /// or the assignment target `Path`'s own range for a plain assignment
    /// (matching [`DirectCallArgMismatch::range`]'s callee-range
    /// convention).
    pub range: TextRange,
    /// The declared local/global's bare name.
    pub target: String,
    /// The target's already-known declared type.
    pub expected: Ty,
    /// The initializer/RHS expression's statically classified type.
    pub found: Ty,
}

/// One incompatibility between a lambda's own **written annotation** (a
/// param's `: T` or the lambda's `: R` return annotation) and its
/// body-derived type (issue #1994, RULED 2026-08-01, closing #1932: "the
/// written annotation takes priority... an incompatible body is an eager
/// error at the lambda, not a deferred surprise at the call site").
///
/// Unlike [`TypedAssignMismatch`]/[`DirectCallArgMismatch`] (both `E063`,
/// gradual/advisory — the body-derived type wins regardless, the
/// annotation-vs-body comparison is only ever a warning), a mismatch
/// recorded here is reported unconditionally as an `Error`-severity `E174`
/// by `strict::check_lambda_annotation_mismatches` — the written annotation
/// *replaces* the body-derived type at this slot (see
/// `body::InferPass::infer_lambda`'s own doc for the precedence change),
/// so a disagreement is never merely advisory.
///
/// Recorded only when a written annotation exists for this slot *and* the
/// body-derived type is not itself unresolved (`Ty::is_unresolved`) — an
/// unannotated slot has nothing to compare against and keeps #1910's
/// unchanged body-derived-wins behavior, and an `Unknown`/`Conflicted`
/// body-derived type never disagrees with anything (mirrors
/// `annotations::report_if_mismatched`'s identical guard for the `fn`/`flow`
/// case).
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LambdaAnnotationMismatch {
    /// The diagnostic site: the mismatched param's own `: T` annotation
    /// range, or the lambda's own `: R` return-annotation range.
    pub range: TextRange,
    /// `Some(param name)` for a mismatched parameter annotation, `None` for
    /// the lambda's own return annotation.
    pub param_name: Option<String>,
    /// The written annotation's resolved type — what now governs this
    /// slot's type.
    pub expected: Ty,
    /// The body's own independent derivation, which disagreed.
    pub found: Ty,
}

/// One lambda-body param or body-declared temp, ready for the same
/// Unknown-escape (`E065`) / Conflicted-escape (`E066`) treatment
/// `strict::check_def` already gives a top-level def's own `params`/
/// `locals` (issue #1770: "lambda bodies are invisible to strict-mode
/// escape checking... give lambda bodies a per-lambda frame").
///
/// A lambda literal still has no `DefinitionId`-keyed `BodyTypes` entry of
/// its own to run `check_def` against — #1727 minted a lifted lambda a
/// stable *identity*, not a `SymbolIndex` entry / `DefKey` (see that
/// issue's ruling), and `infer_project`/`InferPass` run over HIR straight
/// from `hir::lower`, strictly *before* `hir::stamp_container_ids` (which
/// only runs as part of LIR lowering / the `normalized_stamped_query`
/// salsa memo) — so even the identity #1727 does mint is not populated yet
/// at the point this fact is recorded. Building a per-lambda strict-frame
/// does not need it: each slot below is already a fully self-contained
/// `emit_escape` input (final type, declaration range, annotation-exemption
/// bit, and a ready-made slot label), so `strict::check_def` re-emits it
/// with no per-lambda grouping or lookup required.
///
/// Recorded unconditionally by [`body::InferPass::infer_lambda`] for
/// **every** lambda anywhere in the enclosing def's body, including one
/// nested inside another lambda's own body — each nested lambda gets its
/// own `infer_lambda` call and so contributes its own slots to this same
/// flat, cumulative vector (mirrors [`LambdaAnnotationMismatch`]'s
/// identical "folded in from every lambda anywhere in this body"
/// precedent). Reported only by strict mode.
///
/// Deliberately **excludes** a lambda's own return-type slot: unlike a
/// top-level `fn`'s return-type escape check, "does this lambda's body
/// ever return a value" has no `E150`-style fall-through analysis defined
/// for it, and #1994's `LambdaAnnotationMismatch` (`E174`) already owns a
/// materially different, eager check for a lambda's return-type
/// *annotation* disagreeing with its body — adding a second, gradual
/// escape check for the identical slot would double-report the same fact
/// under a different code. Out of scope for #1770; see that issue's own
/// "Ask" (params + temps only, matching `BodyTypes::locals`'s own
/// params-∪-temps membership, not `BodyTypes::return_ty`).
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct LambdaEscapeSlot {
    /// The slot's own declaration range — a param's name range, or a
    /// body-declared temp's/`if`-`as`-binding's/`for`-var's own name range.
    /// The diagnostic anchor, same convention as `check_def`'s own
    /// per-slot ranges.
    pub range: TextRange,
    /// The slot's final, escape-checked type.
    pub ty: Ty,
    /// Whether a resolvable annotation/ascription exempts an `Unknown`
    /// classification (never a `Conflicted` one) — mirrors `check_def`'s
    /// own `annotated` argument to `emit_escape`. Always `false` for a
    /// param slot: `infer_lambda`'s own annotation-governs-when-present
    /// overlay (#1994) already replaces an annotated param's `ty` with the
    /// resolved annotation itself before this slot is built, so there is
    /// nothing left for a separate exemption to do there — this field only
    /// ever does real work for a body-declared temp, which carries no such
    /// overlay.
    ///
    /// That holds only for a param whose name the lambda's own body never
    /// re-binds. A name the body *does* re-bind (`|t: int| { let t = 1;
    /// t = "oops"; t }`) never reaches a param slot at all — review finding
    /// on #1770: the governance overlay's rebound-name branch reads `ty`
    /// straight from `self.locals[name]`, i.e. the shadowing local's own
    /// accumulated type, not the annotated param's, so `infer_lambda`
    /// excludes that name from this loop entirely and reports it only as a
    /// `` "lambda temp" `` slot instead (built from the same body-declared-
    /// temps loop every ordinary temp goes through) — the escape belongs to
    /// the fresh local, not the parameter of the same spelling.
    pub annotated: bool,
    /// The slot's own label, ready to hand straight to `emit_escape` — e.g.
    /// `` "lambda parameter `x`" `` / `` "lambda temp `t`" `` — prefixed so
    /// the reported message reads distinctly from the enclosing def's own
    /// same-named slot (`check_def`'s `param_name` and `slot_label`
    /// convention, one level in).
    pub slot_label: String,
}

/// One statically-checkable type mismatch at a **dotted struct-field**
/// assignment target (issue #1900, split from #1864/#1877 — PR #1899's own
/// `check_declared_assign_target` explicitly excludes a multi-segment
/// target, since a dotted target's declared type is its *root's* shape, not
/// the field's).
///
/// Body inference resolves only the ROOT's declared type here (`ctx.globals`
/// for a `VAR`/`CONST`, or an annotated Param/Temp's ascription — see
/// `body::InferPass::check_declared_field_assign_target`'s doc) — it has no
/// struct-shape table of its own (the firewall: a body never reads
/// project-wide `STRUCT` declarations), so `path` is recorded unresolved.
/// `structs::check_assignments` (strict-mode-only) walks `path` against
/// `structs::declared_shapes`/`ShapeInfo` to resolve the specific field's
/// declared type and reports `E063`.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct FieldAssignMismatch {
    /// The root local/global's bare display name (`p` in `p.x = expr`).
    pub root: String,
    /// The root's resolved declared type — `Ty::Struct(name)` in the
    /// classifiable case; anything else (`Unknown`, a scalar/collection) is
    /// never recorded as a fact at all (see the recording site's own
    /// "Unknown never disagrees" guard).
    pub root_ty: Ty,
    /// The field-access chain past the root, in source order (`p.x` →
    /// `[x]`, `p.inner.x` → `[inner, x]`) — each segment's own `Name`
    /// carries the range a per-field diagnostic should point at.
    pub path: Vec<Name>,
    /// The assignment's operator (`=`, `+=`, …). Carried alongside `found`
    /// (issue #1900 review finding) so `structs::check_field_assign_mismatch`
    /// — the only place the field's *declared* type is ever resolved — can
    /// apply the same `+=` string-numeric display-concat carve-out
    /// `Stmt::Assignment`'s own arm applies for a bare target: this body-
    /// inference pass only knows the ROOT's type when the fact is recorded,
    /// not the field's, so the carve-out can't be decided here.
    pub op: AssignOp,
    /// The RHS's statically inferred type.
    pub found: Ty,
}

/// One statically-checkable argument-type mismatch recorded at any of
/// three producer sites whose callee resolves straight to a known def via
/// `known_sigs` — so its declared parameter types are already fully known
/// at the site — unlike the T1c call-through-a-value case
/// [`ValueCallFact`] exists for:
///
/// - a **direct call** (issue #1864) — `f(a, b)` where `f` names a known
///   knot/stitch/function directly;
/// - a `#fn(target, args…)` **creation site** (issue #2001) — not a call
///   at all, but the by-ref *binding* site for a partial application;
///   `target`'s remaining (unbound) params still go through the ordinary
///   call-through-a-value check when the resulting `Ty::Fn` value is
///   later invoked, but the *bound* prefix checked here is only ever
///   checkable at creation.
/// - a **divert with arguments** (issue #2127) — `-> knot(a, b)` — also not
///   a call expression, but a `ref` position it binds is checked exactly
///   like a direct call's `ref` argument (invariant, via `ref_assignable`).
///   By-value positions at this site are **not** checked yet (#2127 scoped
///   that out as its own design call, same posture #2001 took for
///   `infer_fn_literal`'s by-value params).
///
/// `strict::check_direct_call_args`'s rendered message reads "argument N
/// of call to `name`" for all three producers — accepted as-is for a `#fn`
/// literal and a divert target too (both still name the target function's
/// own parameter being populated), rather than adding a site-discriminant
/// field to distinguish "creation of" / "divert to" from "call to";
/// revisit if that reads as confusing in practice (#2001 review finding).
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct DirectCallArgMismatch {
    /// The diagnostic site's source range: the callee `Path`'s own range
    /// for a direct call (same convention as [`ValueCallFact::range`]), the
    /// `#fn` literal's `target` path range for a creation site, or the
    /// divert's own target path range (issue #2127).
    pub range: TextRange,
    /// The callee's display name (`h` in `h("hi")`; dotted if the resolved
    /// path had multiple segments, e.g. `Knot.stitch`).
    pub callee: String,
    /// The mismatched argument's 0-based position.
    pub index: usize,
    /// The callee's declared parameter type at `index`.
    pub expected: Ty,
    /// The argument expression's statically classified type.
    pub found: Ty,
}

/// One statically-checkable fact about a call through a function value
/// (T1c, docs/t1c-spec.md §4 — "under `types = strict`, calls through
/// function values are statically checked").
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct ValueCallFact {
    /// The callee reference's source range (the diagnostic site).
    pub range: TextRange,
    /// The callee's display name (`f` in `f(5)`).
    pub callee: String,
    pub kind: ValueCallKind,
}

/// What a [`ValueCallFact`] observed. Strict mode maps these onto the
/// existing TM-3 machinery — escape codes for unresolved callees, the
/// typed-mismatch code for known-type disagreements — rather than minting
/// parallel codes (docs/t1c-spec.md §8).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ValueCallKind {
    /// The callee's type is `Unknown` in call position — a strict-mode
    /// escape (`E065` class): the call can't be checked, so a strict author
    /// must annotate or restructure.
    UnknownCallee,
    /// The callee's type is `Conflicted` (#627) in call position (`E066`
    /// class).
    ConflictedCallee,
    /// The callee has a known concrete type that isn't `fn(T…): R` (and
    /// isn't `divert` — calling through a divert-ref variable is a
    /// pre-existing ink pattern this slice deliberately leaves unchecked).
    NotCallable(Ty),
    /// Known `fn(T…): R` callee, wrong argument count.
    ArityMismatch { expected: usize, got: usize },
    /// Known `fn(T…): R` callee; argument `index` (0-based) has a concrete
    /// type that neither matches the row's param type nor coerces to it
    /// (`int -> float` is the one legal directional coercion, spec §4).
    ArgMismatch {
        index: usize,
        expected: Ty,
        found: Ty,
    },
    /// `bind(f, args…)` (T1c-3, issue #733) supplied more args than remain
    /// in the known `fn(T…): R` callee's param row — over-binding, distinct
    /// from [`Self::ArityMismatch`] because `bind` has no fixed target arity
    /// to match (binding fewer than the remaining params is legal; only
    /// binding *more* is an error, mirroring the runtime's
    /// `FunctionValueArity` fault and `#fn`'s own `E081` over-binding check).
    OverBind { available: usize, got: usize },
}

/// The whole-project inference result (mirrors `AnalysisResult`'s shape:
/// one pure function over already-computed inputs, callable directly or
/// wrapped as a salsa query).
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct InferenceResult {
    /// Every inferable (knot/stitch) def's finalized signature.
    pub signatures: BTreeMap<DefinitionId, InferredSig>,
    /// Every inferable def's full body type picture.
    pub bodies: BTreeMap<DefinitionId, BodyTypes>,
}

impl From<crate::InferredType> for Ty {
    fn from(t: crate::InferredType) -> Self {
        match t {
            crate::InferredType::Int => Ty::Int,
            crate::InferredType::Float => Ty::Float,
            crate::InferredType::Bool => Ty::Bool,
            crate::InferredType::String => Ty::String,
            crate::InferredType::Divert => Ty::Divert,
            // Issue #628: the initializer-derived stub now carries the
            // declaring LIST's name, so this round-trips to the same
            // nominal `Ty::List` the annotation/body-inference paths use —
            // no more conservative collapse to `Unknown`.
            crate::InferredType::List(name) => Ty::List(name),
        }
    }
}

/// One inferable definition: its own id, declaring file, declared params,
/// and body.
///
/// `pub` (FG-2.1, issue #638): `brink-db`'s `solve_scc_query` builds these
/// itself from per-def `def_body_query` results (Ruling 2b's narrowed HIR
/// projection) and passes them into [`solve_scc`] directly, instead of
/// [`solve_scc`] rebuilding them via [`collect_defs`] over a whole-project
/// (or even whole-file) HIR slice.
#[derive(Debug, Clone, Copy)]
pub struct Def<'a> {
    pub id: DefinitionId,
    pub file: FileId,
    pub params: &'a [Param],
    pub body: &'a Block,
    /// The function-header return annotation (`): type ===`), when the def
    /// is a knot that carries one (T1c — the boundary-annotation firewall
    /// applied to the return slot: an `Unknown` inferred return overlays to
    /// the annotated type, so `#fn` rows built from this signature are
    /// concrete). `None` for stitches and unannotated knots.
    pub return_annotation: Option<&'a TypeExpr>,
    /// Which frontend produced [`Self::file`] — [`HirFile::native`] (issue
    /// #1862), carried per def because that is the granularity every
    /// consumer of this struct has: `brink-db`'s narrowed per-def HIR
    /// projection never holds a whole [`HirFile`]. Reaches inference as
    /// [`body::BodyCtx::native`], where the native bare-name fn-value rule
    /// (issue #1876) keys off it.
    pub native: bool,
}

/// Per-file resolution lookup: a `Path`'s range is only unique within its
/// own file, so resolutions must never be merged across files.
pub(crate) fn index_resolutions_by_file(
    resolutions: &ResolutionMap,
) -> BTreeMap<FileId, BTreeMap<(u32, u32), DefinitionId>> {
    let mut by_file: BTreeMap<FileId, BTreeMap<(u32, u32), DefinitionId>> = BTreeMap::new();
    for r in resolutions {
        by_file
            .entry(r.file)
            .or_default()
            .insert(range_key(r.range), r.target);
    }
    by_file
}

/// Every file's own declared module, read off any one symbol the index
/// already has for it (module is uniform per file — every symbol
/// `insert_file_symbols` inserts for a given file carries the identical
/// `SymbolInfo::module`, since it is computed once per file from that
/// file's own resolved `ModuleMap` entry, not re-derived per symbol). Feeds
/// [`ProjectCtx::file_modules`] — see that field's own doc for why keying by
/// [`FileId`] (rather than the def's own [`DefinitionId`], which the
/// synthetic root-content def never has an index entry for) is required.
///
/// A file with zero indexed *global* symbols at all (pure top-level content
/// with no named declaration) has no entry here and reads as `None` — the
/// same conservative "absent data reads as empty" default every other
/// module-blind path in this module already uses; nothing regresses
/// relative to the pre-#2233 `None`-everywhere behavior for that case.
///
/// Skips every **local** (`info.scope.is_some()` — a param/temp) entirely:
/// `insert_local` always stamps a local's own `SymbolInfo::module` `None`
/// regardless of its file's real declared status ("locals are never
/// module-qualified and always module-internal" — `manifest::insert_local`'s
/// own doc), so folding one in would non-deterministically shadow a file's
/// real module with `None` depending on `index.symbols`'s (`HashMap`-backed)
/// iteration order — the exact per-run-flaky bug a first version of this
/// function had.
fn index_module_by_file(index: &SymbolIndex) -> BTreeMap<FileId, Option<String>> {
    let mut by_file: BTreeMap<FileId, Option<String>> = BTreeMap::new();
    for info in index.symbols.values() {
        if info.scope.is_some() {
            continue;
        }
        by_file
            .entry(info.file)
            .or_insert_with(|| info.module.clone());
    }
    by_file
}

/// Declaration-derived global (VAR/CONST) types — read via `signature()`,
/// the firewall boundary for every non-callable reference in a body.
///
/// Reads [`Sig::value_ty`](crate::Sig::value_ty) — the declaration's type at
/// full [`Ty`] fidelity. Before issue #1540 this read the narrow
/// `Sig::value_type` (with a `Sig::fn_type` fallback), which had no
/// representation for `Array`/`Map`/`Struct`/`Fn`/`Handle`, so a
/// collection-typed global was invisible to every typed check keyed on this
/// map — E149 and the TM-3/T1e family all missed `VAR arr = #[…]` entirely.
/// One field now carries that whole domain, so nothing in it can fall out
/// again. `range` is not part of that domain yet: it has no annotation
/// grammar at all (`crate::annotations::resolve` has no arm for it), so a
/// `VAR`/`CONST` can't be declared with one in the first place. (Stale
/// pre-#1552 note, corrected for issue #2782: `Option<T>` **is** part of
/// this domain — `annotations::resolve`'s `Generic` arm has handled it
/// since #1552/PR #1804, so a `VAR`/`CONST` declared `Option<T>` reads
/// through `Sig::value_ty` here exactly like `Array<T>`/`Map<K, V>` do.)
///
/// `pub(crate)` (issue #670) so `structs::check`'s non-literal struct-field
/// classification can resolve a variable-valued initializer that names a
/// global `VAR`/`CONST` against this exact same declaration-derived type,
/// rather than re-deriving it.
pub(crate) fn collect_globals(
    files: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    manifest: Option<&HostManifest>,
) -> BTreeMap<DefinitionId, Ty> {
    let mut globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
    for (&id, info) in &index.symbols {
        if matches!(info.kind, SymbolKind::Variable | SymbolKind::Constant)
            && let Some(sig) = crate::signature::signature(id, index, files, manifest)
            && let Some(ty) = sig.value_ty.clone()
        {
            globals.insert(id, ty);
        }
    }
    globals
}

/// Declaration-derived `EXTERNAL` signatures (issue #786, docs/t1d-spec.md
/// §3: "a binding declared to take `Handle<AudioInstance>` rejects a
/// `Handle<Timer>` argument at compile time" under `types = strict`; issue
/// #805 widens this to the manifest's full scalar-semantic-type vocabulary
/// and to inline-doc-only bindings).
///
/// **Two consumers share this one resolution (issue #1004).** Both the
/// call-site seeding — this map is folded into `solve_scc`/`infer_project`'s
/// `known_sigs` so a call to a registered `EXTERNAL` checks its *arguments*
/// against the declared param types — and [`crate::strict::check_external_escapes`]
/// (the escape check over the *declarations themselves*, so a registered
/// binding whose `ManifestParam.ty` fails to resolve is reported rather than
/// silently treated as an untyped call) read the identical `(params, return)`
/// signatures from here. The strict-escape reader lives on the shared
/// [`crate::strict_diagnostics`] seam, so the analysis path
/// (`analyze_with_options`) and the compile path (`brink-db`'s
/// `whole_project_diagnostics_query`) get byte-identical external escapes
/// from one helper — never a second, drift-prone re-resolution.
///
/// `EXTERNAL name(params)` has no ink-side type-annotation grammar (unlike a
/// knot/stitch's `(x: T)`/`): T ===`), so a binding's *declared*
/// parameter/return types can only come from two sources — exactly the two
/// [`crate::external_check::analyze_externals`] already merges for its
/// `SymbolMeta`/`E039`-`E042` enrichment: a matching entry in the registered
/// [`HostManifest`]'s [`brink_ir::ManifestExternal`] list, and/or an inline
/// `///` `@param`/`@returns` [`DocBlock`] parsed off the declaration itself.
/// #805 reuses that same merge order here (inline wins by param name, else
/// the registered entry wins by position) rather than re-deriving a second,
/// narrower rule — an `EXTERNAL` documented purely via `///` tags, with no
/// corresponding `ManifestExternal` entry at all, now seeds a signature too.
///
/// Every resolved [`TypeRef`] — handle-kinded or scalar — goes through
/// [`type_ref_to_ty`], which looks the name up in the registered
/// [`SemanticTypeDef`](brink_ir::SemanticTypeDef) table regardless of which
/// source (manifest or inline doc) supplied the ref; a scalar semantic type
/// (e.g. `switch_id`, `base: Int`) now types as its own `base` (`Ty::Int`)
/// exactly like a `Handle<K>`-based one types as `Ty::Handle(K)` — the same
/// `known_sigs`/`observe`/`unify` call-checking path applies to both, so a
/// literal-typed argument that disagrees with a declared scalar semantic
/// type folds to `Ty::Conflicted` and reports through the pre-existing
/// `E066` classification, no new diagnostic code. This also covers
/// return-position kind checking uniformly: `reg`/`inline`'s `returns` ref
/// resolves through the identical `type_ref_to_ty` call as every param, so a
/// binding's declared return kind (handle or scalar) becomes the call
/// expression's own `Ty` wherever it's assigned or compared, through
/// `infer_call`'s existing `sig.return_ty.clone()` — no separate return-only
/// code path exists to fall out of sync with the param path.
///
/// No HIR read: entirely index + manifest + [`DocBlock`] derived (mirrors
/// [`collect_globals`]'s shape) — `inline_docs` is itself HIR-free
/// ([`DocBlock`] carries parsed doc content only, no source ranges), so this
/// still has no per-file dependency edge to narrow.
///
/// An `EXTERNAL` with neither a registered manifest entry nor an inline doc
/// contributes no signature at all — call sites stay exactly as unchecked as
/// before this issue. A param/return whose resolved [`TypeRef`] names
/// neither a base keyword nor a registered [`SemanticTypeDef`] types
/// `Ty::Unknown` — the same conservative fallback every other unresolved
/// slot in this module gets. `Ty::Unknown` params are inert at the
/// call-checking site (`BodyCtx::observe` is a documented no-op against
/// `Ty::Unknown`), so this never fabricates a false mismatch.
pub fn collect_external_sigs(
    index: &SymbolIndex,
    manifest: Option<&HostManifest>,
    inline_docs: &BTreeMap<(SymbolKind, String), DocBlock>,
) -> BTreeMap<DefinitionId, InferredSig> {
    let mut sigs = BTreeMap::new();
    let (types, registered) = crate::manifest_maps(manifest);
    for (&id, info) in &index.symbols {
        if info.kind != SymbolKind::External {
            continue;
        }
        let inline = inline_docs.get(&(SymbolKind::External, info.name.clone()));
        let reg = registered.get(info.name.as_str()).copied();
        if inline.is_none() && reg.is_none() {
            continue; // no declared signature at all — stays unchecked
        }

        // Param types: inline `@param` (by name) wins, else registered (by
        // position) — the exact merge order `external_check::analyze_externals`
        // uses for the same two sources.
        let params: Vec<Ty> = info
            .params
            .iter()
            .enumerate()
            .map(|(i, p)| {
                let tref: Option<&TypeRef> = inline
                    .and_then(|d| d.params.iter().find(|(n, _)| n == &p.name).map(|(_, t)| t))
                    .or_else(|| reg.and_then(|r| r.params.get(i).map(|mp| &mp.ty)));
                tref.map_or(Ty::Unknown, |t| type_ref_to_ty(t, &types))
            })
            .collect();
        let return_ty = inline
            .and_then(|d| d.returns.as_ref())
            .or_else(|| reg.map(|r| &r.returns))
            .map_or(Ty::Unknown, |t| type_ref_to_ty(t, &types));
        sigs.insert(id, InferredSig { params, return_ty });
    }
    sigs
}

/// Resolve a [`TypeRef`] (manifest- or inline-doc-sourced — both are the
/// bare name form, resolution is identical either way) to a checker [`Ty`]
/// (issue #805 — the full scalar-plus-handle slice of
/// `external_check::resolve_type`'s domain, closed-domain constraints
/// excluded: the checker substrate only needs a `Ty`, never a
/// [`Constraint`](brink_ir::Constraint)). A base scalar keyword
/// (`string`/`int`/`float`/`bool`) resolves directly; a name registered in
/// `types` resolves through its own [`SemanticTypeDef::base`] — `Ty::String`/
/// `Ty::Int`/`Ty::Float`/`Ty::Bool` for a scalar specialization (e.g.
/// `switch_id`, `base: Int`), `Ty::Handle(name)` for a `base: Handle` kind
/// definition (T1d-2, docs/t1d-spec.md §3 — the def's own `name` *is* the
/// declared handle-kind name `Handle<K>` annotations resolve `K` against).
/// `void` (either the bare keyword or a registered `base: Void` def) has no
/// `Ty` (return-only, same as an annotation's `void`); an unresolved name —
/// no manifest at all, or a name neither a base keyword nor a registered
/// semantic type — types `Ty::Unknown` (unresolved — never a hard failure).
///
/// Classification goes through [`crate::type_resolution::classify`] — the
/// same function `external_check::resolve_type` (hover/pickers) uses — so an
/// **unregistered** name (`TypeShape::Unregistered`) types `Ty::Unknown`
/// here exactly as consistently as it renders `base: None` there (#1027;
/// closes the #1004 divergence where hover showed a confident `id: var_id`
/// for a name inference correctly called `Unknown`).
fn type_ref_to_ty(t: &TypeRef, types: &BTreeMap<String, brink_ir::SemanticTypeDef>) -> Ty {
    use crate::type_resolution::{TypeShape, classify};

    match classify(t, types) {
        // Unspecified/unregistered are conservatively `Unknown` (#1027 —
        // `TypeShape::Unregistered` is exactly the class
        // `external_check::resolve_type` renders `base: None` for). The
        // bare `void`/`handle` keyword literals join them here too: `void`
        // is return-only (no represented `Ty`), and a bare `handle` (no
        // kind name) isn't a `Ty::Handle` either — that needs the kind name
        // itself, which only ever arrives as a *registered* name (i.e.
        // `TypeShape::Registered` below), never as the literal keyword
        // `handle`.
        TypeShape::Unspecified
        | TypeShape::Unregistered
        | TypeShape::Base(BaseType::Void | BaseType::Handle) => Ty::Unknown,
        TypeShape::Base(BaseType::String) => Ty::String,
        TypeShape::Base(BaseType::Int) => Ty::Int,
        TypeShape::Base(BaseType::Float) => Ty::Float,
        TypeShape::Base(BaseType::Bool) => Ty::Bool,
        TypeShape::Registered(def) => match def.base {
            BaseType::String => Ty::String,
            BaseType::Int => Ty::Int,
            BaseType::Float => Ty::Float,
            BaseType::Bool => Ty::Bool,
            BaseType::Void => Ty::Unknown,
            BaseType::Handle => Ty::Handle(t.0.trim().to_string()),
        },
    }
}

/// The synthetic `DefinitionId` `hir.root_content`'s own inference results
/// are keyed under (issue #1903). Root content has no parameters, no
/// return type, and no `DefinitionId` in the symbol table, so this mixes a
/// tag bit into the `FileId` to avoid colliding with a real definition id;
/// the id is never looked up in the symbol table, only used to key
/// `inference.bodies` so a later check can read the results back out.
///
/// This is the scheme's origin — [`collect_defs`] below synthesizes it to
/// drive inference over `root_content` in the first place. Issue #2772
/// review finding: every other site that needs to key into
/// `inference.bodies` for root content's own def
/// (`strict::check_direct_call_args`, `strict::body_def_ids`,
/// `option_conditions::check`) must call this rather than re-deriving the
/// formula inline, so a future move to module-qualified ids only has to
/// change once.
pub(crate) fn root_content_def_id(file: FileId) -> DefinitionId {
    DefinitionId::new(DefinitionTag::LocalVar, u64::from(file.0))
}

/// Every inferable (knot/stitch) def in the project, resolved back to its
/// own `DefinitionId` via `(file, kind, qualified name)` — HIR `Knot`/
/// `Stitch` nodes carry only a bare `Name`, not their own id.
///
/// A *floating* stitch (`= stitch`, declared before any `== knot ==`
/// header) lowers into `hir.knots` as a `Knot` node (`NodeClass::Stitch` provenance)
/// but was declared `SymbolKind::Stitch` with a bare name by
/// `lower_top_level_stitch` — never `SymbolKind::Knot`, and never qualified
/// with a knot prefix (there is no enclosing knot). So the symbol-kind used
/// for the `def_of` lookup must track `knot.ptr`, not assume every
/// `hir.knots` entry is a real `SymbolKind::Knot` (#626).
pub(crate) fn collect_defs<'a>(
    files: &[(FileId, &'a HirFile)],
    index: &SymbolIndex,
) -> Vec<Def<'a>> {
    let mut def_of: BTreeMap<(FileId, SymbolKind, String), DefinitionId> = BTreeMap::new();
    for (&id, info) in &index.symbols {
        def_of.insert((info.file, info.kind, info.name.clone()), id);
    }

    let mut defs: Vec<Def<'a>> = Vec::new();
    for &(file_id, hir) in files {
        // Issue #1903: walk `root_content` statements through inference,
        // creating a synthetic def so `check_declared_assign_target` and
        // `check_declared_temp_init` (called from `infer_def_body`) reach them.
        // Root content has no parameters, no return type, and no DefinitionId
        // in the symbol table. A synthetic ID is derived from the FileId
        // (mixing in a tag bit to avoid collision with real definition IDs);
        // the ID is never looked up in the symbol table, only used to key
        // `inference.bodies` so that strict checks later read the results.
        if !hir.root_content.stmts.is_empty() {
            let synthetic_id = root_content_def_id(file_id);
            defs.push(Def {
                id: synthetic_id,
                file: file_id,
                params: &[],
                body: &hir.root_content,
                return_annotation: None,
                native: hir.native,
            });
        }

        for knot in &hir.knots {
            let knot_symbol_kind = knot.symbol_kind();
            if let Some(&id) = def_of.get(&(file_id, knot_symbol_kind, knot.name.text.clone())) {
                defs.push(Def {
                    id,
                    file: file_id,
                    params: &knot.params,
                    body: &knot.body,
                    return_annotation: knot.return_type.as_ref(),
                    native: hir.native,
                });
            }
            for stitch in &knot.stitches {
                let qualified = format!("{}.{}", knot.name.text, stitch.name.text);
                if let Some(&id) = def_of.get(&(file_id, SymbolKind::Stitch, qualified)) {
                    defs.push(Def {
                        id,
                        file: file_id,
                        params: &stitch.params,
                        body: &stitch.body,
                        // #1509 widened `Stitch` with the same `return_type`
                        // grammar position `Knot` carries.
                        return_annotation: stitch.return_type.as_ref(),
                        native: hir.native,
                    });
                }
            }
        }
    }
    defs.sort_by_key(|d| d.id);
    defs
}

/// Shared read-only context every pass over `defs` needs.
struct ProjectCtx<'a> {
    index: &'a SymbolIndex,
    globals: &'a BTreeMap<DefinitionId, Ty>,
    by_file: &'a BTreeMap<FileId, BTreeMap<(u32, u32), DefinitionId>>,
    inferable: &'a BTreeSet<DefinitionId>,
    /// Declared `LIST`/`STRUCT` names, computed once per context — needed
    /// by the T1c annotation-firewall overlay (`annotations::resolve` of
    /// param/return/temp annotations inside [`body::infer_def_body`]).
    list_names: BTreeSet<String>,
    struct_names: BTreeSet<String>,
    /// Declared handle-kind names from the registered `HostManifest`
    /// (T1d-2b, issue #774, docs/t1d-spec.md §3) — computed once per
    /// context, same shape as `list_names`/`struct_names`, so `Handle<K>`
    /// param/return/temp annotations resolve during body inference too, not
    /// just at the `signature()`/annotation-firewall seam.
    handle_names: BTreeSet<String>,
    /// Every file's own declared module (`None` for an undeclared
    /// stem-module or a file with no indexed symbols at all), keyed by
    /// [`FileId`] rather than [`DefinitionId`] — module is a per-*file*
    /// fact, not a per-symbol one: every symbol `insert_file_symbols`
    /// (`brink-analyzer::manifest`) inserts for one file carries the
    /// identical [`brink_ir::SymbolInfo::module`], derived once from that
    /// file's own resolved [`crate::ModuleMap`] entry.
    ///
    /// Issue #2233 review finding: `body_ctx` used to read this straight off
    /// `index.symbols.get(&def.id).module`, keyed on the def's own id — which
    /// always misses for the synthetic root-content def [`collect_defs`]
    /// mints for `hir.root_content` (issue #1903; that id is "never looked
    /// up in the symbol table" by its own doc), silently leaving
    /// `referrer_module: None` for *every* file with non-empty top-level ink
    /// content, including one declared inside `std…` — exactly the #2233
    /// disagreement this ctx exists to close. Keying by [`FileId`] instead
    /// covers both the real and the synthetic def uniformly, since both
    /// carry [`Def::file`].
    file_modules: BTreeMap<FileId, Option<String>>,
}

impl<'a> ProjectCtx<'a> {
    fn new(
        index: &'a SymbolIndex,
        globals: &'a BTreeMap<DefinitionId, Ty>,
        by_file: &'a BTreeMap<FileId, BTreeMap<(u32, u32), DefinitionId>>,
        inferable: &'a BTreeSet<DefinitionId>,
        manifest: Option<&HostManifest>,
    ) -> Self {
        Self {
            index,
            globals,
            by_file,
            inferable,
            list_names: crate::annotations::declared_list_names(index),
            struct_names: crate::annotations::declared_struct_names(index),
            handle_names: crate::annotations::declared_handle_kinds(manifest),
            file_modules: index_module_by_file(index),
        }
    }

    fn body_ctx(
        &'a self,
        def: &Def<'_>,
        known_sigs: &'a BTreeMap<DefinitionId, InferredSig>,
    ) -> BodyCtx<'a> {
        static EMPTY: BTreeMap<(u32, u32), DefinitionId> = BTreeMap::new();
        BodyCtx {
            resolution_by_range: self.by_file.get(&def.file).unwrap_or(&EMPTY),
            index: self.index,
            globals: self.globals,
            known_sigs,
            inferable: self.inferable,
            list_names: &self.list_names,
            struct_names: &self.struct_names,
            handle_names: &self.handle_names,
            // Per *def*, not per project: `ProjectCtx` is shared across
            // every batch, and a project can mix `.ink` and `.brink` files
            // (INCLUDE/IMPORT across surfaces), so the frontend flag must
            // follow the body being walked — issue #1876.
            native: def.native,
            // Issue #2233 (review finding: keyed by file, not by the def's
            // own id — see `ProjectCtx::file_modules`'s doc for why the
            // synthetic root-content def needs this). `None` for a file with
            // no `file_modules` entry (no indexed symbols at all) or whose
            // own module is the legacy undeclared-stem-module `None`.
            referrer_module: self
                .file_modules
                .get(&def.file)
                .and_then(|module| module.as_deref()),
        }
    }
}

/// Pass 1: call-graph edges only. `known_sigs` is empty here — every call
/// resolves to `Unknown` and the resulting types are discarded — this pass
/// exists solely to discover which defs call which, which the SCC batching
/// (pass 2) needs before any real solving can start.
fn build_call_graph(defs: &[Def<'_>], ctx: &ProjectCtx<'_>) -> CallGraph {
    let no_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
    let mut graph = CallGraph::new();
    for d in defs {
        graph.add_node(d.id);
        let body_ctx = ctx.body_ctx(d, &no_sigs);
        let result = infer_def_body(d, &body_ctx);
        for callee in result.calls {
            graph.add_edge(d.id, callee);
        }
    }
    graph
}

/// Solve one SCC batch's fixpoint in place (the per-batch body of pass 2):
/// extends `known_sigs` with `batch`'s own members' finalized signatures —
/// seeded `Unknown`, re-run until stable or [`MAX_SCC_ITERATIONS`] — and
/// returns `batch`'s finalized [`BodyTypes`]. `known_sigs` must already carry
/// the finalized signature of every def *outside* `batch` that a member of
/// `batch` calls (every earlier batch's signature, for [`solve_batches`]'s
/// whole-project loop; every condensation-predecessor SCC's signature, for
/// the public [`solve_scc`] — FG-2, issue #631).
///
/// Shared by [`solve_batches`] (`ctx`/`by_id` built once, looped over every
/// batch — unchanged cost from before this function was extracted) and
/// [`solve_scc`] (`ctx`/`by_id` rebuilt per call, one batch at a time — the
/// new per-SCC query boundary).
fn solve_one_batch(
    batch: &BTreeSet<DefinitionId>,
    by_id: &BTreeMap<DefinitionId, &Def<'_>>,
    ctx: &ProjectCtx<'_>,
    known_sigs: &mut BTreeMap<DefinitionId, InferredSig>,
) -> BTreeMap<DefinitionId, BodyTypes> {
    for &id in batch {
        known_sigs.entry(id).or_insert_with(|| {
            let param_count = by_id.get(&id).map_or(0, |d| d.params.len());
            InferredSig {
                params: vec![Ty::Unknown; param_count],
                return_ty: Ty::Unknown,
            }
        });
    }

    let mut last_round: BTreeMap<DefinitionId, body::BodyResult> = BTreeMap::new();
    for _round in 0..MAX_SCC_ITERATIONS {
        let mut round: BTreeMap<DefinitionId, body::BodyResult> = BTreeMap::new();
        let mut changed = false;
        for &id in batch {
            let Some(&d) = by_id.get(&id) else { continue };
            let body_ctx = ctx.body_ctx(d, known_sigs);
            let result = infer_def_body(d, &body_ctx);
            let new_sig = InferredSig {
                params: result.params.iter().map(|(_, t)| t.clone()).collect(),
                return_ty: result.return_ty.clone(),
            };
            if known_sigs.get(&id) != Some(&new_sig) {
                changed = true;
            }
            known_sigs.insert(id, new_sig);
            round.insert(id, result);
        }
        last_round = round;
        if !changed {
            break;
        }
    }

    last_round
        .into_iter()
        .map(|(id, result)| {
            (
                id,
                BodyTypes {
                    params: result.params,
                    locals: result.locals,
                    return_ty: result.return_ty,
                    has_value_return: result.has_value_return,
                    value_calls: result.value_calls,
                    array_remove_calls: result.array_remove_calls,
                    direct_call_arg_mismatches: result.direct_call_arg_mismatches,
                    typed_assign_mismatches: result.typed_assign_mismatches,
                    field_assign_mismatches: result.field_assign_mismatches,
                    lambda_annotation_mismatches: result.lambda_annotation_mismatches,
                    ufcs_call_args: result.ufcs_call_args,
                    lambda_escapes: result.lambda_escapes,
                },
            )
        })
        .collect()
}

/// Pass 2: solve every SCC batch in dependency order, mutually-recursive
/// batches by fixpoint (spec §2's SCC rule — see the module doc).
///
/// `external_sigs` (issue #786): every `EXTERNAL`'s declaration-derived
/// signature ([`collect_external_sigs`]), seeded into `known_sigs` before any
/// batch solves — a call to an external now resolves through the exact same
/// `known_sigs` lookup + [`body::BodyCtx::observe`] unify path an ordinary
/// knot/stitch call already uses, so a `Handle<K>`-mismatched argument folds
/// its local to `Ty::Conflicted` and reports through the pre-existing `E066`
/// classification, no parallel checking surface. Externals are never SCC
/// members (never in any `batch`), so this seed is never touched again by
/// the per-batch fixpoint loop below.
fn solve_batches(
    batches: &[BTreeSet<DefinitionId>],
    by_id: &BTreeMap<DefinitionId, &Def<'_>>,
    ctx: &ProjectCtx<'_>,
    external_sigs: &BTreeMap<DefinitionId, InferredSig>,
) -> (
    BTreeMap<DefinitionId, InferredSig>,
    BTreeMap<DefinitionId, BodyTypes>,
) {
    let mut known_sigs: BTreeMap<DefinitionId, InferredSig> = external_sigs.clone();
    let mut bodies: BTreeMap<DefinitionId, BodyTypes> = BTreeMap::new();

    for batch in batches {
        let batch_bodies = solve_one_batch(batch, by_id, ctx, &mut known_sigs);
        bodies.extend(batch_bodies);
    }

    (known_sigs, bodies)
}

/// Infer types for every knot/stitch body across the whole project.
///
/// Pure function of already-computed inputs (`index`/`resolutions`, the
/// same shape `finish_analysis`/`signature` take) — safe to call directly in
/// tests, and the exact function `type_inference_query` wraps for salsa
/// memoization. `manifest` (T1d-2b, issue #774): the registered host
/// manifest, threaded through to `signature()`/annotation resolution so
/// `Handle<K>` param/return/temp annotations resolve to `Ty::Handle(K)`
/// during body inference — `None` degrades to an empty handle-kind set,
/// same posture as every other manifest-driven check. Also threaded to
/// [`collect_external_sigs`] (issue #786) so a call to a manifest-registered
/// `EXTERNAL` checks its arguments against the binding's declared param
/// types the same way a knot/stitch call already does. `inline_docs` (issue
/// #805): the project-wide merged `///` doc-comment map
/// ([`crate::project_inline_docs`]'s output), the second of
/// [`collect_external_sigs`]'s two signature sources — an empty map degrades
/// to manifest-only seeding, byte-identical to pre-#805 behavior.
#[must_use]
pub fn infer_project(
    files: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    resolutions: &ResolutionMap,
    manifest: Option<&HostManifest>,
    inline_docs: &BTreeMap<(SymbolKind, String), DocBlock>,
) -> InferenceResult {
    let by_file = index_resolutions_by_file(resolutions);
    let globals = collect_globals(files, index, manifest);
    let defs = collect_defs(files, index);
    let inferable: BTreeSet<DefinitionId> = defs.iter().map(|d| d.id).collect();
    let by_id: BTreeMap<DefinitionId, &Def<'_>> = defs.iter().map(|d| (d.id, d)).collect();

    let ctx = ProjectCtx::new(index, &globals, &by_file, &inferable, manifest);
    let external_sigs = collect_external_sigs(index, manifest, inline_docs);

    let graph = build_call_graph(&defs, &ctx);
    let batches = topo_order(&graph);
    let (signatures, bodies) = solve_batches(&batches, &by_id, &ctx, &external_sigs);

    InferenceResult { signatures, bodies }
}

// ─── Per-def/per-SCC query boundary (FG-2, issue #631) ────────────────
//
// `docs/fine-grained-salsa-proposal.md` §2 decomposes `infer_project` into
// `call_edges(def) -> scc_membership() -> solve_scc(SccId) ->
// inferred_signature(def)`. This module keeps every algorithm exactly as
// `infer_project` already used it (SCC/condensation in `graph.rs`, the
// single-batch fixpoint above); `brink-db` owns the query *keys*, *edges*,
// and `SccId` interning (a plain `DefinitionId` — the component's minimum
// member, already `graph.rs`'s own sort key) that turn these pure functions
// into salsa-memoized, per-def/per-SCC-cacheable ones.

/// Every inferable (knot/stitch) definition's id in the project (FG-2, issue
/// #631). A cheap structural scan — needs the whole project's HIR to
/// enumerate every def's body. Superseded, for `brink-db`'s per-def/per-SCC
/// query wiring, by [`inferable_defs_from_index`] (FG-2.1, issue #638,
/// Ruling 2b — the same id set, sourced from the index alone, no HIR read);
/// kept for direct pure-function callers (e.g. [`infer_project`]) and as the
/// equivalence anchor `inferable_defs_from_index_matches_hir_derived_set`
/// pins.
#[must_use]
pub fn inferable_defs(files: &[(FileId, &HirFile)], index: &SymbolIndex) -> BTreeSet<DefinitionId> {
    collect_defs(files, index).iter().map(|d| d.id).collect()
}

/// The same inferable (knot/stitch) def id set as [`inferable_defs`], read
/// directly off the index's `SymbolKind` — no HIR (FG-2.1, issue #638,
/// Ruling 2b: "`inferable` comes from an index-sourced `inferable_defs_query`
/// (dep = `inference_index_query`, not HIR)"). A knot/stitch symbol is
/// always indexed at exactly the same moment its `hir.knots` entry is
/// lowered (`lower_single_knot`/`lower_top_level`), so filtering
/// `index.symbols` by kind here is output-identical to walking every file's
/// HIR the way [`inferable_defs`] does — pinned by
/// `inferable_defs_from_index_matches_hir_derived_set`.
#[must_use]
pub fn inferable_defs_from_index(index: &SymbolIndex) -> BTreeSet<DefinitionId> {
    index
        .symbols
        .iter()
        .filter(|(_, info)| matches!(info.kind, SymbolKind::Knot | SymbolKind::Stitch))
        .map(|(&id, _)| id)
        .collect()
}

/// Find one inferable def's own params + body from a declaring-file-scoped
/// HIR slice alone (FG-2.1, issue #638, Ruling 2b — backs `brink-db`'s
/// per-def `def_body_query(def)` projection, the `inference_index_query`
/// precedent applied to bodies). A thin filter over the same
/// [`collect_defs`] walk [`call_edges`]/[`solve_scc`] already used
/// project-wide, scoped here to exactly `def`'s declaring file so the salsa
/// wrapper records a read-edge on only that file's `lowered_query` — not
/// every project file's. Returns owned data (`Vec<Param>`/`Block` both
/// `Clone`) since the salsa caller stores the result in a long-lived memo,
/// past the borrow of any one `lowered_query` call.
#[must_use]
pub fn def_body(
    def: DefinitionId,
    declaring_file_hir: &[(FileId, &HirFile)],
    index: &SymbolIndex,
) -> Option<(Vec<Param>, Option<TypeExpr>, Block)> {
    collect_defs(declaring_file_hir, index)
        .into_iter()
        .find(|d| d.id == def)
        .map(|d| {
            (
                d.params.to_vec(),
                d.return_annotation.cloned(),
                d.body.clone(),
            )
        })
}

/// Pass 1, exposed per one definition (FG-2, issue #631 — `call_edges(def)`).
/// Computes exactly what [`build_call_graph`]'s loop body computes for one
/// def: infer this def's body with `known_sigs` empty (every call resolves
/// `Unknown`; only the *set* of resolved call targets is kept, matching the
/// design doc's explicit "keep reusing `infer_def_body` and discard types,
/// as today" allowance for this query). Returns an empty set for an
/// unknown/non-inferable def id — same "absent data reads as empty, never
/// panics" contract as the rest of this module.
///
/// **Narrowed inputs (FG-2.1, issue #638, Ruling 2a).** `declaring_file_hir`
/// need only cover `def`'s own declaring file (pass 1 never needs any other
/// file's HIR to find one def's own body); `inferable` is caller-supplied
/// (index-sourced — see [`inferable_defs_from_index`]) rather than
/// recomputed via [`collect_defs`] over the narrowed slice, because a
/// resolved call target can land in a *different* file than `def`'s own.
/// `collect_globals` is dropped entirely — pass 1 discards every computed
/// type (spec §5), so a permanently-empty globals map is behavior-identical
/// and strictly cheaper.
///
/// `manifest` (T1d-2b, issue #774): threaded through to `ProjectCtx` for the
/// same reason every other per-def FG-2 seam now carries it — `call_edges`
/// discards every computed type (only the *set* of call targets survives),
/// so which handle kinds are registered can never change this function's
/// output; the parameter exists so `brink-db`'s `call_edges_query` doesn't
/// need a second, differently-shaped code path just to reach the manifest
/// `referenced_globals`/`solve_scc` also need.
#[must_use]
pub fn call_edges(
    def: DefinitionId,
    declaring_file_hir: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    resolutions: &ResolutionMap,
    inferable: &BTreeSet<DefinitionId>,
    manifest: Option<&HostManifest>,
) -> BTreeSet<DefinitionId> {
    let by_file = index_resolutions_by_file(resolutions);
    let defs = collect_defs(declaring_file_hir, index);
    let Some(d) = defs.iter().find(|d| d.id == def) else {
        return BTreeSet::new();
    };
    let empty_globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
    let ctx = ProjectCtx::new(index, &empty_globals, &by_file, inferable, manifest);
    let no_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
    let body_ctx = ctx.body_ctx(d, &no_sigs);
    infer_def_body(d, &body_ctx).calls
}

/// Pass 1b, exposed per one definition (FG-2.1, issue #638, Ruling 1 —
/// `referenced_globals(def)`, the same per-def body-facts family as
/// [`call_edges`]). The VAR/CONST global ids `def`'s body references,
/// recorded by [`body::BodyResult::referenced_globals`] regardless of
/// whether a real globals map was supplied — this call passes an empty one,
/// exactly [`call_edges`]'s "discard the computed types, keep the
/// structural fact" shape. `brink-db` resolves each returned id via
/// `signature_query` and hands the walk a small narrow `BTreeMap` before the
/// *real* solve runs (two walks: this scan, then [`solve_scc`] — see the
/// spec's Ruling 1 tradeoff note). Also the per-def global *read set* a
/// future T2 effect row needs — named and shaped for that reuse now, no
/// speculative machinery added.
///
/// `manifest` (T1d-2b, issue #774): same rationale as [`call_edges`]'s own
/// parameter — this pass discards every computed type too (only the
/// *referenced-def-id set* survives), so it can never change this
/// function's output; threaded so `brink-db`'s `referenced_globals_query`
/// shares one uniform per-def-seam shape with `call_edges_query`/
/// `solve_scc_query`.
#[must_use]
pub fn referenced_globals(
    def: DefinitionId,
    declaring_file_hir: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    resolutions: &ResolutionMap,
    manifest: Option<&HostManifest>,
) -> BTreeSet<DefinitionId> {
    let by_file = index_resolutions_by_file(resolutions);
    let defs = collect_defs(declaring_file_hir, index);
    let Some(d) = defs.iter().find(|d| d.id == def) else {
        return BTreeSet::new();
    };
    let empty_globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
    let empty_inferable: BTreeSet<DefinitionId> = BTreeSet::new();
    let ctx = ProjectCtx::new(index, &empty_globals, &by_file, &empty_inferable, manifest);
    let no_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
    let body_ctx = ctx.body_ctx(d, &no_sigs);
    infer_def_body(d, &body_ctx).referenced_globals
}

/// T2-1 (docs/effects-spec.md §2/§4, issue #860 — `def_effect_atoms(def)`).
/// One def's raw effect atoms: the read set (VAR/CONST globals read), the
/// write set (assignment targets resolving to a VAR/CONST), the call-kind set
/// (`EXTERNAL` names directly called), the inferable direct-call edges the
/// effect fixpoint follows, the fn-value creation targets (Fork A, issue
/// #1726 — `EffectAtoms::creates_fn_values`), and whether the body calls
/// through a function value it cannot trace (→ pessimal). Harvested by the
/// exact same body walk
/// [`referenced_globals`]/[`call_edges`] drive — the read set here *is*
/// FG-2.1's `referenced_globals`, and the direct-call edges are `call_edges`'s
/// set — so no new walk shape is introduced, only the per-def atom bundle T2
/// needs assembled from one pass.
///
/// **Narrowed inputs** mirror [`call_edges`] exactly: `declaring_file_hir`
/// need only cover `def`'s own file; `inferable` is caller-supplied
/// (index-sourced) so a resolved call target in a *different* file is still
/// classified as an edge, not a stray external. `manifest` is threaded for the
/// same uniform-seam reason — it can never change the *structural* atom sets
/// this discards every computed type to keep.
#[must_use]
pub fn def_effect_atoms(
    def: DefinitionId,
    declaring_file_hir: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    resolutions: &ResolutionMap,
    inferable: &BTreeSet<DefinitionId>,
    manifest: Option<&HostManifest>,
) -> EffectAtoms {
    let by_file = index_resolutions_by_file(resolutions);
    let defs = collect_defs(declaring_file_hir, index);
    let Some(d) = defs.iter().find(|d| d.id == def) else {
        return EffectAtoms::default();
    };
    let empty_globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
    let ctx = ProjectCtx::new(index, &empty_globals, &by_file, inferable, manifest);
    let no_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
    let body_ctx = ctx.body_ctx(d, &no_sigs);
    let result = infer_def_body(d, &body_ctx);
    EffectAtoms {
        reads: result.referenced_globals,
        writes: result.effect_writes,
        calls: result.external_calls,
        direct_calls: result.calls,
        creates_fn_values: result.created_fn_values,
        opaque: result.effect_opaque,
        emits: result.effect_emits,
        tags: result.effect_tags,
        faults: result.effect_faults,
        faults_refined: result.effect_faults_refined,
        param_holes: result.param_holes,
        call_fn_args: result.call_fn_args,
    }
}

/// T2-1 (docs/effects-spec.md §4, issue #860 — the whole-project effect row
/// table). Mirrors [`infer_project`]'s shape for effects: harvest every
/// inferable def's atoms, build the same call graph off the direct-call edges,
/// solve every SCC batch in condensation order with [`solve_scc_effects`]
/// (accumulating each finalized batch's rows as `known_rows` for its
/// successors). A pure function of already-computed inputs — the direct-call
/// pure-function callers and the property tests use it; `brink-db`'s per-SCC
/// `effects_scc_query` reproduces the same fold incrementally.
#[must_use]
pub fn effects_project(
    files: &[(FileId, &HirFile)],
    index: &SymbolIndex,
    resolutions: &ResolutionMap,
    manifest: Option<&HostManifest>,
) -> BTreeMap<DefinitionId, EffectRow> {
    let defs = collect_defs(files, index);
    let inferable: BTreeSet<DefinitionId> = defs.iter().map(|d| d.id).collect();

    // Harvest each def's atoms once; the direct-call edges double as the call
    // graph the SCC batching needs.
    let atoms: BTreeMap<DefinitionId, EffectAtoms> = defs
        .iter()
        .map(|d| {
            (
                d.id,
                def_effect_atoms(d.id, files, index, resolutions, &inferable, manifest),
            )
        })
        .collect();

    let mut graph = CallGraph::new();
    for (&id, a) in &atoms {
        graph.add_node(id);
        // Fork A (issue #1726): fn-value creation sites are call-graph edges
        // alongside the direct calls — structurally harvested, so no row is
        // ever consulted to build this graph. `creates_fn_values` is a subset
        // of `direct_calls` today (the same walk records both at a `#fn`
        // literal), but *this monolithic path* (`effects_project`, not the
        // salsa `call_graph_query` the IDE/`brink check`/@brink-lang/web
        // actually run — that graph is built from `call_edges_query`/
        // `direct_calls` alone and never reads `creates_fn_values`) names it
        // explicitly so batching here does not silently depend on that
        // coincidence. The salsa path deliberately still relies on the
        // subset property; `every_fn_value_creation_target_is_also_a_call_graph_edge`
        // (below) is its guard.
        for &callee in a.direct_calls.iter().chain(&a.creates_fn_values) {
            graph.add_edge(id, callee);
        }
    }
    let batches = topo_order(&graph);

    let mut rows: BTreeMap<DefinitionId, EffectRow> = BTreeMap::new();
    for batch in &batches {
        // `solve_scc_effects` reads finalized predecessor rows out of
        // `known_rows`; every earlier batch is already folded in, so passing
        // the whole accumulated `rows` is exactly the condensation-predecessor
        // set (plus already-solved siblings, harmless — a batch never edges
        // back into a later one).
        let solved = solve_scc_effects(batch, &atoms, &rows);
        rows.extend(solved);
    }
    rows
}

/// Solve exactly one SCC batch (FG-2, issue #631 — `solve_scc(SccId)`).
///
/// `known_sigs` must already carry the finalized signature of every def
/// *outside* `batch` that a member of `batch` calls — in practice, every def
/// in every condensation-predecessor SCC. `brink-db`'s `solve_scc_query`
/// gets these by recursively reading its own dependency SCCs'
/// `solve_scc_query` results first; the condensation is a DAG (SCCs are
/// maximal by construction), so that recursion is always acyclic — no salsa
/// cycles anywhere (Fork 1 ruling, design doc §8).
///
/// **Narrowed inputs (FG-2.1, issue #638, Ruling 2b/Ruling 1).** `defs` is
/// caller-supplied (built from per-def `def_body_query` results — only
/// `batch`'s own members' declaring files are ever read); `globals` is the
/// small narrow map `brink-db` built from every member's
/// [`referenced_globals`] pre-scan, resolved through `signature_query`
/// (never [`collect_globals`]'s whole-project scan); `inferable` is
/// index-sourced ([`inferable_defs_from_index`]). None of this changes the
/// fixpoint mechanics below — only how the read-only context feeding it is
/// assembled, and how narrow the salsa dependency edges recording that
/// assembly turn out to be.
///
/// `manifest` (T1d-2b, issue #774): the registered host manifest, threaded
/// through to `ProjectCtx` so a `Handle<K>` param/return/temp annotation
/// resolves to `Ty::Handle(K)` here too — this is the seam that makes
/// strict-mode handle-kind rejection reachable end-to-end (docs/t1d-spec.md
/// §3, the #767 acceptance criterion): once two locals of different
/// declared handle kinds are unified together (e.g. compared or
/// reassigned), the #627 lattice already folds them to `Ty::Conflicted`,
/// which `strict::check`'s existing `E066` classification reports — this
/// function is what was missing to let a genuine `Ty::Handle` ever reach
/// that lattice from body-usage inference at all. `brink-db`'s
/// `solve_scc_query` reads it off `project.analysis_options(db)`, the same
/// coarse project-wide dependency shape `per_file_diagnostics_query`
/// already reads `host_manifest` at.
///
/// **`EXTERNAL` call-site checking (issue #786; widened by issue #805 to
/// scalar semantic types and inline-doc-only bindings).** `known_sigs` is
/// also seeded (idempotently, every call — cheap index+manifest+doc scan, no
/// HIR) with [`collect_external_sigs`]'s declaration-derived signatures
/// before this batch solves, so a call to a manifest-registered or
/// inline-doc-only `EXTERNAL` types its arguments (and its return value,
/// wherever the call expression is used) against the binding's declared
/// types through the exact same [`body::BodyCtx::observe`] path a
/// knot/stitch call already uses — same #627 `Ty::Conflicted` lattice, same
/// `E066` report, no parallel checking surface. `index`/`manifest` are both
/// already read by this function for every other reason above; `inline_docs`
/// (issue #805) is the project-wide merged `///` doc-comment map
/// (`brink-db`'s `inline_docs_query`, the same memo `external_meta_query`
/// already reads it from), so this adds exactly one new salsa dependency
/// edge on `brink-db`'s `solve_scc_query` side — the same coarse,
/// range-free, `Eq`-cutoff shape `inline_docs_query` already gives every
/// other reader.
///
/// **Does not itself return an `EXTERNAL`'s signature (issue #1921).**
/// `batch` never contains an `EXTERNAL` — [`inferable_defs_from_index`]
/// filters the index to `SymbolKind::Knot | SymbolKind::Stitch` only — so
/// the returned `signatures` map (filtered to `batch`'s own members, see
/// below) never carries one, even though `known_sigs` is seeded with every
/// external's signature above. `brink-db`'s `type_inference_query`
/// re-merges [`collect_external_sigs`]'s seed into its own aggregated
/// `InferenceResult::signatures` once, after collecting every SCC's own
/// members' signatures from this function — not per-SCC here — so an
/// external's signature is exposed exactly once regardless of how many
/// SCCs a project has, instead of every `solve_scc_query` memo duplicating
/// the whole external-signature map.
#[must_use]
#[expect(
    clippy::too_many_arguments,
    reason = "the FG-2 per-SCC solve boundary (issue #631) — each parameter is an \
              independently-narrowed input `brink-db`'s solve_scc_query assembles from its \
              own per-def salsa queries; bundling them into a struct would just move the same \
              shape one level down for no clarity gain, and this is the one call site (the \
              salsa wrapper) plus tests, not a widely-called API"
)]
pub fn solve_scc(
    batch: &BTreeSet<DefinitionId>,
    defs: &[Def<'_>],
    index: &SymbolIndex,
    resolutions: &ResolutionMap,
    globals: &BTreeMap<DefinitionId, Ty>,
    inferable: &BTreeSet<DefinitionId>,
    mut known_sigs: BTreeMap<DefinitionId, InferredSig>,
    manifest: Option<&HostManifest>,
    inline_docs: &BTreeMap<(SymbolKind, String), DocBlock>,
) -> (
    BTreeMap<DefinitionId, InferredSig>,
    BTreeMap<DefinitionId, BodyTypes>,
) {
    known_sigs.extend(collect_external_sigs(index, manifest, inline_docs));
    let by_file = index_resolutions_by_file(resolutions);
    let by_id: BTreeMap<DefinitionId, &Def<'_>> = defs.iter().map(|d| (d.id, d)).collect();
    let ctx = ProjectCtx::new(index, globals, &by_file, inferable, manifest);

    let bodies = solve_one_batch(batch, &by_id, &ctx, &mut known_sigs);
    let signatures: BTreeMap<DefinitionId, InferredSig> = batch
        .iter()
        .filter_map(|id| known_sigs.get(id).map(|sig| (*id, sig.clone())))
        .collect();
    (signatures, bodies)
}

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

    fn build(src: &str) -> (HirFile, SymbolIndex, ResolutionMap) {
        let parsed = brink_syntax::parse(src);
        let (hir, manifest, _diag) = lower(FileId(0), &parsed.tree());
        let (index, _diag) = crate::symbol_index(&[(FileId(0), &manifest)]);
        let (resolutions, _diag) =
            crate::resolve(FileId(0), &manifest, &index, &crate::ImportScope::default());
        (hir, (*index).clone(), (*resolutions).clone())
    }

    /// [`build`], but with `FileId(0)` given an explicit **declared** module
    /// (issue #2233 review finding: `body_ctx`'s `referrer_module` threading
    /// was never exercised by any test — every `BodyCtx` literal below and
    /// every `resolve.rs` test passes the module as a hardcoded literal
    /// rather than reading it off a real `ProjectCtx::body_ctx` call). Mirrors
    /// `brink-analyzer::manifest`'s own declared-module test shape
    /// (`ResolvedModule { declared: true, .. }` inserted into a `ModuleMap`).
    fn build_with_module(src: &str, module_name: &str) -> (HirFile, SymbolIndex, ResolutionMap) {
        let parsed = brink_syntax::parse(src);
        let (hir, manifest, _diag) = lower(FileId(0), &parsed.tree());
        let mut modules = crate::ModuleMap::new();
        modules.insert(
            FileId(0),
            crate::ResolvedModule {
                name: module_name.to_string(),
                declared: true,
                was: None,
            },
        );
        let (index, _diag) = crate::symbol_index_with_modules(
            &[(FileId(0), &manifest)],
            &modules,
            crate::Dialect::Brink,
            false,
        );
        let scope = crate::ImportScope::new(Some(module_name.to_string()), &hir.imports);
        let (resolutions, _diag) = crate::resolve(FileId(0), &manifest, &index, &scope);
        (hir, (*index).clone(), (*resolutions).clone())
    }

    /// [`build`], plus the project-wide merged `///` doc map (issue #805 —
    /// the inline-doc-only `collect_external_sigs` source, mirroring
    /// `whole_project_diagnostics`'s own `collect_inline_docs` call).
    fn build_with_docs(
        src: &str,
    ) -> (
        HirFile,
        SymbolIndex,
        ResolutionMap,
        BTreeMap<(SymbolKind, String), DocBlock>,
    ) {
        let parsed = brink_syntax::parse(src);
        let (hir, manifest, _diag) = lower(FileId(0), &parsed.tree());
        let (index, _diag) = crate::symbol_index(&[(FileId(0), &manifest)]);
        let (resolutions, _diag) =
            crate::resolve(FileId(0), &manifest, &index, &crate::ImportScope::default());
        let inline_docs = crate::project_inline_docs(&[(FileId(0), &manifest)]);
        (hir, (*index).clone(), (*resolutions).clone(), inline_docs)
    }

    fn sig_of<'a>(result: &'a InferenceResult, index: &SymbolIndex, name: &str) -> &'a InferredSig {
        let id = index
            .by_name
            .get(name)
            .and_then(|ids| ids.first())
            .copied()
            .expect("no def with this name");
        result
            .signatures
            .get(&id)
            .expect("no inferred signature for this def")
    }

    #[test]
    fn param_type_inferred_from_arithmetic_use() {
        // A knot whose param is used arithmetically against an int literal.
        let (hir, index, res) = build("=== heal(hp) ===\n~ temp x = hp + 1\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "heal");
        assert_eq!(sig.params, vec![Ty::Int]);
    }

    #[test]
    fn param_type_inferred_from_comparison_with_float_literal() {
        let (hir, index, res) = build("=== spend(gold) ===\n{gold > 1.5:\n  ok\n}\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "spend");
        assert_eq!(sig.params, vec![Ty::Float]);
    }

    #[test]
    fn floating_stitch_body_is_inferred() {
        // A *floating* stitch — `= name`, declared before any `== knot ==`
        // header — lowers into `hir.knots` (with `NodeClass::Stitch` provenance) but
        // is declared `SymbolKind::Stitch` with a bare name, not
        // `SymbolKind::Knot`. Before #626, `collect_defs` always looked the
        // entry up as `SymbolKind::Knot`, the lookup silently failed, and
        // this def never made it into `defs` — no signature, no body types,
        // total silent skip.
        let (hir, index, res) = build("= heal(hp)\n~ temp x = hp + 1\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "heal");
        assert_eq!(sig.params, vec![Ty::Int]);
    }

    #[test]
    fn floating_stitch_coexists_with_real_knot_and_its_nested_stitch() {
        // Regression guard for the fix itself: distinguishing floating
        // stitches (`NodeClass::Stitch` provenance) from real knots
        // (`NodeClass::Knot` provenance) in `collect_defs` must not disturb the
        // existing, already-working real-knot / nested-stitch lookup path.
        let (hir, index, res) = build(
            "= intro(hp)\n~ temp x = hp + 1\n-> DONE\n\
             === knot_a(gold) ===\n{gold > 1.5:\n  ok\n}\n-> stitch_a ->\n\
             = stitch_a(silver)\n~ temp y = silver + 1\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        assert_eq!(sig_of(&result, &index, "intro").params, vec![Ty::Int]);
        assert_eq!(sig_of(&result, &index, "knot_a").params, vec![Ty::Float]);
        let stitch_a_id = index
            .by_name
            .get("knot_a.stitch_a")
            .and_then(|ids| ids.first())
            .copied()
            .expect("no def for knot_a.stitch_a");
        let stitch_a_sig = result
            .signatures
            .get(&stitch_a_id)
            .expect("no inferred signature for knot_a.stitch_a");
        assert_eq!(stitch_a_sig.params, vec![Ty::Int]);
    }

    /// Issue #2233 review finding (rule 19q/20a): `ProjectCtx::body_ctx`'s
    /// `referrer_module` threading was untested — every `BodyCtx` literal in
    /// `body.rs`'s own test module and every `resolve.rs` test passes the
    /// module as a hardcoded literal/argument, so replacing `body_ctx`'s
    /// computed expression with a hardcoded `None` left the whole suite
    /// green. This exercises the real `ProjectCtx::new`/`body_ctx` call path
    /// for an ordinary, indexed def declared inside `std…`.
    #[test]
    fn body_ctx_threads_referrer_module_for_a_real_def() {
        let (hir, index, _res) = build_with_module(
            "=== heal(hp) ===\n~ temp x = hp + 1\n-> DONE\n",
            "std::conventions::screenplay",
        );
        let id = index
            .by_name
            .get("heal")
            .and_then(|ids| ids.first())
            .copied()
            .expect("heal def indexed");
        let empty_globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
        let by_file: BTreeMap<FileId, BTreeMap<(u32, u32), DefinitionId>> = BTreeMap::new();
        let inferable: BTreeSet<DefinitionId> = [id].into_iter().collect();
        let ctx = ProjectCtx::new(&index, &empty_globals, &by_file, &inferable, None);
        let defs = collect_defs(&[(FileId(0), &hir)], &index);
        let def = defs.iter().find(|d| d.id == id).expect("def found");
        let no_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
        let body_ctx = ctx.body_ctx(def, &no_sigs);
        assert_eq!(
            body_ctx.referrer_module,
            Some("std::conventions::screenplay"),
            "a real def's referrer_module must come from its own declared module"
        );
    }

    /// Issue #2233 review finding: the synthetic root-content def
    /// (`collect_defs`, issue #1903 — minted for `hir.root_content`'s own
    /// walk) has no `SymbolIndex` entry of its own. Before this fix,
    /// `body_ctx`'s `index.symbols.get(&def.id)` lookup always missed for
    /// it, silently leaving `referrer_module: None` even for a file declared
    /// inside `std…` — exactly the #2233 disagreement this PR closes.
    /// `ProjectCtx::file_modules` keys by `def.file` instead, which this def
    /// carries just like a real one, so it must resolve too.
    #[test]
    fn body_ctx_threads_referrer_module_for_the_synthetic_root_content_def() {
        // The file also needs at least one *named* declaration (`knot_a`
        // here) — `ProjectCtx::file_modules` derives a file's module from
        // any symbol the index already has for it, so a file with zero
        // indexed symbols at all has no entry to derive from at all (the
        // same "absent data reads as empty" default every other
        // module-blind path in this module uses, not a regression this fix
        // introduces). The overwhelmingly common real-world shape this
        // fixes — a std file's own top-level weave calling a UFCS free
        // function — always has at least one such declaration.
        let (hir, index, _res) = build_with_module(
            "Hello.\n-> DONE\n=== knot_a ===\nworld\n-> DONE\n",
            "std::conventions::screenplay",
        );
        assert!(
            !hir.root_content.stmts.is_empty(),
            "fixture must have non-empty root content to mint the synthetic def"
        );
        let empty_globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
        let by_file: BTreeMap<FileId, BTreeMap<(u32, u32), DefinitionId>> = BTreeMap::new();
        let inferable: BTreeSet<DefinitionId> = BTreeSet::new();
        let ctx = ProjectCtx::new(&index, &empty_globals, &by_file, &inferable, None);
        let defs = collect_defs(&[(FileId(0), &hir)], &index);
        let synthetic = defs
            .iter()
            .find(|d| !index.symbols.contains_key(&d.id))
            .expect("synthetic root-content def present");
        let no_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
        let body_ctx = ctx.body_ctx(synthetic, &no_sigs);
        assert_eq!(
            body_ctx.referrer_module,
            Some("std::conventions::screenplay"),
            "the synthetic root-content def's referrer_module must still resolve, keyed by \
             file rather than the def's own (absent) index entry"
        );
    }

    #[test]
    fn unused_param_is_unknown_and_legal() {
        let (hir, index, res) = build("=== noop(x) ===\nHello.\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "noop");
        assert_eq!(sig.params, vec![Ty::Unknown]);
    }

    /// Issue #1532 (#1501 review finding 3): the #1484 `remove`/`remove_at`
    /// split's advertised latent fix — the array leg no longer narrows its
    /// *index* argument against the array's *element* type (wrong for an
    /// index; the pre-split shared `remove` code did this) — shipped with
    /// no regression test. `arr` is a `temp` — a `VAR` would work equally
    /// well since issue #1540 gave globals a full-fidelity `Sig::value_ty`,
    /// but the `temp` spelling is what this test was written against — so
    /// its `Ty::Array(String)`
    /// element type is genuinely in hand at the call site. If `remove_at`'s
    /// index arm regressed to narrowing against it, `i` would come out
    /// `Ty::String` here instead of staying `Unknown` (`i` is otherwise
    /// unused — `unused_param_is_unknown_and_legal`'s baseline). Mirrors
    /// `insert`'s array leg, which is also index-typed and was never
    /// narrowed (`infer::body`'s `"insert"` arm only narrows the map k/v
    /// pair).
    #[test]
    fn remove_at_index_arg_does_not_narrow_against_the_array_element_type() {
        let (hir, index, res) = build(
            "=== function drop_at(i) ===\n~ {\n    temp arr = #[\"a\", \"b\", \"c\"]\n    remove_at(arr, i)\n}\n~ return 0\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let drop_at_id = index
            .by_name
            .get("drop_at")
            .and_then(|ids| ids.first())
            .copied()
            .expect("drop_at");
        let body = result.bodies.get(&drop_at_id).expect("drop_at body");
        assert_eq!(
            body.locals.get("arr"),
            Some(&Ty::Array(Box::new(Ty::String))),
            "fixture sanity: arr must actually be known as an array of strings, or this test \
             can't distinguish the fix from the bug it guards"
        );
        let sig = sig_of(&result, &index, "drop_at");
        assert_eq!(
            sig.params,
            vec![Ty::Unknown],
            "remove_at's index argument must not narrow against the array's element type"
        );
    }

    #[test]
    fn return_type_inferred_from_return_statement() {
        let (hir, index, res) = build("=== function double(x) ===\n~ return x + x\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "double");
        // `x` only ever appears added to itself — Unknown stays Unknown
        // under `unify(Unknown, Unknown) == Unknown`; the *return type*
        // still comes out Unknown too (nothing ever pins `x` concrete).
        assert_eq!(sig.return_ty, Ty::Unknown);
    }

    /// [`build`]'s native-frontend twin — `InfixOp::Coalesce` (B1, issue
    /// #1460) is produced only by `hir::lower_native`, so the coalescing
    /// feedback test below (unlike every other test in this module) must
    /// parse through the native frontend rather than `brink_syntax`.
    fn build_native(src: &str) -> (HirFile, SymbolIndex, ResolutionMap) {
        let parse = brink_syntax_native::parse(src);
        assert!(
            parse.errors().is_empty(),
            "fixture must parse cleanly: {:?}",
            parse.errors()
        );
        let tree = parse.tree();
        let (hir, manifest, _diag) = brink_ir::hir::lower_native::lower(FileId(0), &tree);
        let (index, _diag) = crate::symbol_index(&[(FileId(0), &manifest)]);
        let (resolutions, _diag) =
            crate::resolve(FileId(0), &manifest, &index, &crate::ImportScope::default());
        (hir, (*index).clone(), (*resolutions).clone())
    }

    /// Review finding on PR #1469/#1460: the `InfixOp::Coalesce` arm's
    /// one-directional `observe()` feedback (`infer::body::InferPass::
    /// infer_infix`'s doc: "so if `lhs` is a bare param/temp path, `rhs`'s
    /// already-inferred type tells us the shape to expect") was asserted in
    /// the PR body but never pinned by a test. `x` is only ever used as
    /// `x or 0` — `rhs` is `int`, not itself `Option`, so the collapse-form
    /// branch feeds `Option[int]` back onto `x`, rather than `x` leaking
    /// `Unknown` (T1c's un-narrowed-Unknown posture every other bare-unused
    /// param hits — see `unused_param_is_unknown_and_legal` above).
    #[test]
    fn coalesce_lhs_param_narrows_to_option_of_the_rhs_type() {
        let (hir, index, res) = build_native("fn f(x) {\n  return x or 0;\n}\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "f");
        assert_eq!(sig.params, vec![Ty::Option(Box::new(Ty::Int))]);
    }

    #[test]
    fn call_site_propagates_callee_param_type_to_caller_local() {
        let (hir, index, res) = build(
            "=== main ===\n~ temp v = 1\n~ use_it(v)\n-> DONE\n=== use_it(n) ===\n{n > 2.5:\n  big\n}\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let use_it = sig_of(&result, &index, "use_it");
        assert_eq!(use_it.params, vec![Ty::Float]);
        // `main`'s own local `v` isn't a param, so we check it via `bodies`.
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(main_body.locals.get("v"), Some(&Ty::Float));
    }

    // ─── `EXTERNAL` call-site checking (issue #786) ─────────────────────

    fn audio_manifest_with_external(param_kind: &str) -> brink_ir::HostManifest {
        brink_ir::HostManifest {
            markup: Vec::new(),
            types: vec![
                brink_ir::SemanticTypeDef {
                    name: "AudioInstance".to_string(),
                    base: brink_ir::BaseType::Handle,
                    constraint: None,
                    values: None,
                    widget: None,
                },
                brink_ir::SemanticTypeDef {
                    name: "Timer".to_string(),
                    base: brink_ir::BaseType::Handle,
                    constraint: None,
                    values: None,
                    widget: None,
                },
            ],
            externals: vec![brink_ir::ManifestExternal {
                name: "play_sound".to_string(),
                params: vec![brink_ir::ManifestParam {
                    name: "inst".to_string(),
                    ty: brink_ir::TypeRef(param_kind.to_string()),
                }],
                returns: brink_ir::TypeRef::default(),
                kind: brink_ir::ExternalKind::default(),
                doc: None,
                widgets: Vec::new(),
                path: Vec::new(),
            }],
        }
    }

    /// The #786 mechanism, isolated: a manifest-registered `EXTERNAL`'s
    /// declared `Handle<K>` param type propagates into `known_sigs` exactly
    /// like a knot/stitch callee's declared param type does
    /// ([`call_site_propagates_callee_param_type_to_caller_local`]'s own
    /// pattern) — a caller's local passed as the argument picks up the
    /// binding's declared kind.
    #[test]
    fn external_call_propagates_declared_handle_kind_to_caller_local() {
        let (hir, index, res) = build(
            "EXTERNAL play_sound(inst)\n=== main ===\n~ temp s = get_sound(1)\n\
             ~ play_sound(s)\n-> DONE\n=== function get_sound(id): Handle<AudioInstance> ===\n~ return id\n",
        );
        let manifest = audio_manifest_with_external("AudioInstance");
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("s"),
            Some(&Ty::Handle("AudioInstance".to_string())),
            "s picks up its own declared return kind cleanly: {main_body:?}"
        );
    }

    /// Positive case: a local declared with one handle kind, passed as the
    /// argument to a binding declared for a *different* kind, folds to
    /// `Ty::Conflicted` at the call site through `observe`/`unify` — the
    /// same #627 lattice a mismatched knot/stitch call argument already
    /// used, no parallel checking surface (`strict.rs`'s
    /// `external_call_cross_kind_argument_is_conflicted_under_strict` pins
    /// the resulting `E066` diagnostic end to end).
    #[test]
    fn external_call_with_cross_kind_argument_conflicts_the_caller_local() {
        let (hir, index, res) = build(
            "EXTERNAL play_sound(inst)\n=== main ===\n~ temp t = get_timer(1)\n\
             ~ play_sound(t)\n-> DONE\n=== function get_timer(id): Handle<Timer> ===\n~ return id\n",
        );
        let manifest = audio_manifest_with_external("AudioInstance");
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("t"),
            Some(&Ty::Conflicted),
            "t is Timer-kinded but play_sound declares AudioInstance: {main_body:?}"
        );
    }

    /// No manifest registered at all: an `EXTERNAL` call contributes no
    /// signature (`collect_external_sigs` degrades to empty, same posture as
    /// every other manifest-driven check) — the call types `Ty::Unknown`,
    /// exactly today's byte-identical behavior. Pins the "gradual mode is
    /// unaffected" half of the #786 acceptance criterion at the inference
    /// level (strict mode itself never even runs without `types = strict`).
    #[test]
    fn external_call_with_no_manifest_stays_unknown() {
        let (hir, index, res) = build(
            "EXTERNAL play_sound(inst)\n=== main ===\n~ temp t = 1\n~ play_sound(t)\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        // `t` is pinned Int by its own `= 1` initializer, unaffected by the
        // unchecked external call.
        assert_eq!(main_body.locals.get("t"), Some(&Ty::Int));
    }

    /// An `EXTERNAL` with no matching registered manifest entry AND no
    /// inline `///` doc — truly undeclared — contributes no signature
    /// either, same conservative "absent data reads as no signature"
    /// contract as every other lookup miss in this module. (Issue #805
    /// widens the *inline-doc-only* case — a registered `///` doc with no
    /// matching `ManifestExternal` — to contribute a real signature; see
    /// `inline_only_external_*` below for that case specifically.)
    #[test]
    fn external_call_with_unregistered_name_stays_unknown() {
        let (hir, index, res) = build(
            "EXTERNAL other_call(inst)\n=== main ===\n~ temp t = 1\n~ other_call(t)\n-> DONE\n",
        );
        let manifest = audio_manifest_with_external("AudioInstance");
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(main_body.locals.get("t"), Some(&Ty::Int));
    }

    // ─── Issue #805: scalar semantic types, inline-only externals, and
    // return-position kind checking ─────────────────────────────────────

    /// A manifest declaring a *scalar* semantic type (`switch_id`, `base:
    /// Int`) alongside the two handle kinds — the vocabulary
    /// `collect_external_sigs` now resolves param/return `TypeRef`s against
    /// uniformly, handle or scalar.
    fn manifest_with_scalar_and_handle_types() -> brink_ir::HostManifest {
        let mut manifest = audio_manifest_with_external("AudioInstance");
        manifest.types.push(brink_ir::SemanticTypeDef {
            name: "switch_id".to_string(),
            base: brink_ir::BaseType::Int,
            constraint: None,
            values: None,
            widget: None,
        });
        manifest
    }

    /// Point (1): a manifest-registered `EXTERNAL`'s param declared with a
    /// *scalar* semantic type (not a `Handle<K>` kind) now resolves to its
    /// own `base` (`switch_id` -> `Ty::Int`) and propagates into the
    /// caller's local exactly like a `Handle<K>`-declared param already did
    /// (mirrors `external_call_propagates_declared_handle_kind_to_caller_local`).
    #[test]
    fn external_call_scalar_semantic_type_param_propagates_to_caller_local() {
        let mut manifest = manifest_with_scalar_and_handle_types();
        manifest.externals.push(brink_ir::ManifestExternal {
            name: "toggle".to_string(),
            params: vec![brink_ir::ManifestParam {
                name: "id".to_string(),
                ty: brink_ir::TypeRef("switch_id".to_string()),
            }],
            returns: brink_ir::TypeRef::default(),
            kind: brink_ir::ExternalKind::default(),
            doc: None,
            widgets: Vec::new(),
            path: Vec::new(),
        });
        let (hir, index, res) =
            build("EXTERNAL toggle(id)\n=== main ===\n~ temp s = 1\n~ toggle(s)\n-> DONE\n");
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("s"),
            Some(&Ty::Int),
            "s unifies cleanly against toggle's declared switch_id (base int): {main_body:?}"
        );
    }

    /// Point (1), negative: a caller's local pinned to a *different*
    /// concrete type (string) than the binding's declared scalar semantic
    /// type (`switch_id`, base int) folds to `Ty::Conflicted` at the call
    /// site — the same #627 lattice a `Handle<K>` mismatch already used, no
    /// new diagnostic code.
    #[test]
    fn external_call_scalar_semantic_type_mismatch_conflicts_the_caller_local() {
        let mut manifest = manifest_with_scalar_and_handle_types();
        manifest.externals.push(brink_ir::ManifestExternal {
            name: "toggle".to_string(),
            params: vec![brink_ir::ManifestParam {
                name: "id".to_string(),
                ty: brink_ir::TypeRef("switch_id".to_string()),
            }],
            returns: brink_ir::TypeRef::default(),
            kind: brink_ir::ExternalKind::default(),
            doc: None,
            widgets: Vec::new(),
            path: Vec::new(),
        });
        let (hir, index, res) = build(
            "EXTERNAL toggle(id)\n=== main ===\n~ temp s = \"harbor\"\n~ toggle(s)\n-> DONE\n",
        );
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("s"),
            Some(&Ty::Conflicted),
            "s is a string but toggle declares switch_id (base int): {main_body:?}"
        );
    }

    /// Point (2): an `EXTERNAL` documented *purely* via an inline `///
    /// @param` doc comment — no corresponding `ManifestExternal` entry at
    /// all in the registered manifest — now seeds a signature too
    /// (`collect_external_sigs`'s inline-doc merge). The manifest here only
    /// registers the `AudioInstance`/`Timer` handle-kind *vocabulary*
    /// (`types`), never a `play_sound` entry under `externals`.
    #[test]
    fn inline_only_external_param_type_propagates_to_caller_local() {
        let (hir, index, res, inline_docs) = build_with_docs(
            "/// @param inst {AudioInstance}\n\
             EXTERNAL play_sound(inst)\n\
             === main ===\n~ temp s = get_sound(1)\n~ play_sound(s)\n-> DONE\n\
             === function get_sound(id): Handle<AudioInstance> ===\n~ return id\n",
        );
        let manifest = brink_ir::HostManifest {
            markup: Vec::new(),
            types: vec![
                brink_ir::SemanticTypeDef {
                    name: "AudioInstance".to_string(),
                    base: brink_ir::BaseType::Handle,
                    constraint: None,
                    values: None,
                    widget: None,
                },
                brink_ir::SemanticTypeDef {
                    name: "Timer".to_string(),
                    base: brink_ir::BaseType::Handle,
                    constraint: None,
                    values: None,
                    widget: None,
                },
            ],
            externals: Vec::new(), // deliberately no `play_sound` entry
        };
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &inline_docs,
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("s"),
            Some(&Ty::Handle("AudioInstance".to_string())),
            "s unifies cleanly against play_sound's inline-doc-declared AudioInstance: {main_body:?}"
        );
    }

    /// Point (2), negative: same inline-doc-only `play_sound`, but the
    /// caller's local is declared a *different* handle kind (`Timer`) —
    /// folds to `Ty::Conflicted`, proving the inline-only signature is
    /// actually checked, not just recorded.
    #[test]
    fn inline_only_external_cross_kind_argument_conflicts_the_caller_local() {
        let (hir, index, res, inline_docs) = build_with_docs(
            "/// @param inst {AudioInstance}\n\
             EXTERNAL play_sound(inst)\n\
             === main ===\n~ temp t = get_timer(1)\n~ play_sound(t)\n-> DONE\n\
             === function get_timer(id): Handle<Timer> ===\n~ return id\n",
        );
        let manifest = brink_ir::HostManifest {
            markup: Vec::new(),
            types: vec![
                brink_ir::SemanticTypeDef {
                    name: "AudioInstance".to_string(),
                    base: brink_ir::BaseType::Handle,
                    constraint: None,
                    values: None,
                    widget: None,
                },
                brink_ir::SemanticTypeDef {
                    name: "Timer".to_string(),
                    base: brink_ir::BaseType::Handle,
                    constraint: None,
                    values: None,
                    widget: None,
                },
            ],
            externals: Vec::new(),
        };
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &inline_docs,
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("t"),
            Some(&Ty::Conflicted),
            "t is Timer-kinded but play_sound's inline doc declares AudioInstance: {main_body:?}"
        );
    }

    /// Point (3): return-position kind checking. `spawn_timer`'s
    /// *registered* return type is `Timer` (a handle kind) — assigning its
    /// result directly to a local already pinned `AudioInstance` (by a
    /// second call) must fold that local to `Ty::Conflicted`, proving the
    /// binding's declared *return* kind is checked, not just its params.
    /// (`external_call_propagates_declared_handle_kind_to_caller_local`
    /// already pins the positive return-position case implicitly, via
    /// `play_sound`'s *param* absorbing `get_sound`'s knot-return-annotated
    /// kind; this test isolates an `EXTERNAL`'s own declared return kind
    /// instead of a knot's.)
    #[test]
    fn external_call_return_position_kind_mismatch_conflicts_the_caller_local() {
        let mut manifest = audio_manifest_with_external("AudioInstance");
        manifest.externals.push(brink_ir::ManifestExternal {
            name: "spawn_timer".to_string(),
            params: Vec::new(),
            returns: brink_ir::TypeRef("Timer".to_string()),
            kind: brink_ir::ExternalKind::default(),
            doc: None,
            widgets: Vec::new(),
            path: Vec::new(),
        });
        let (hir, index, res) = build(
            "EXTERNAL play_sound(inst)\nEXTERNAL spawn_timer()\n\
             === main ===\n~ temp x = spawn_timer()\n~ play_sound(x)\n-> DONE\n",
        );
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("x"),
            Some(&Ty::Conflicted),
            "x is spawn_timer's declared Timer return, passed where play_sound declares \
             AudioInstance: {main_body:?}"
        );
    }

    /// Point (3), positive: `spawn_timer`'s declared return kind matches the
    /// declared param kind it's immediately passed to — unifies cleanly, no
    /// escape.
    #[test]
    fn external_call_return_position_kind_match_unifies_cleanly() {
        let mut manifest = audio_manifest_with_external("AudioInstance");
        manifest.externals.push(brink_ir::ManifestExternal {
            name: "spawn_audio".to_string(),
            params: Vec::new(),
            returns: brink_ir::TypeRef("AudioInstance".to_string()),
            kind: brink_ir::ExternalKind::default(),
            doc: None,
            widgets: Vec::new(),
            path: Vec::new(),
        });
        let (hir, index, res) = build(
            "EXTERNAL play_sound(inst)\nEXTERNAL spawn_audio()\n\
             === main ===\n~ temp x = spawn_audio()\n~ play_sound(x)\n-> DONE\n",
        );
        let result = infer_project(
            &[(FileId(0), &hir)],
            &index,
            &res,
            Some(&manifest),
            &BTreeMap::new(),
        );
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let main_body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(
            main_body.locals.get("x"),
            Some(&Ty::Handle("AudioInstance".to_string())),
            "x is spawn_audio's declared AudioInstance return, matching play_sound's own \
             declared param kind: {main_body:?}"
        );
    }

    #[test]
    #[expect(
        clippy::similar_names,
        reason = "ping/pong are the clearest names for this pair"
    )]
    fn mutual_recursion_params_stay_firewalled_to_each_defs_own_body() {
        // `ping` and `pong` call each other with an arithmetic expression
        // (`n - 1`), not a bare local — so nothing about the *callee's*
        // declared param type can flow backward onto the *caller's* own `n`
        // (call-site-driven inference is forbidden by the firewall). Each
        // def's own param type is pinned only by its own body's comparison:
        // `ping` compares `n` to an int literal, `pong` to a float literal.
        let (hir, index, res) = build(
            "=== function ping(n) ===\n{n > 0:\n  ~ return pong(n - 1)\n}\n~ return n\n\
             === function pong(n) ===\n{n > 0.5:\n  ~ return ping(n - 1)\n}\n~ return n\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let ping_sig = sig_of(&result, &index, "ping");
        let pong_sig = sig_of(&result, &index, "pong");
        assert_eq!(
            ping_sig.params,
            vec![Ty::Int],
            "ping's own body only compares n to an int"
        );
        assert_eq!(
            pong_sig.params,
            vec![Ty::Float],
            "pong's own body only compares n to a float"
        );
    }

    #[test]
    #[expect(
        clippy::similar_names,
        reason = "ping/pong are the clearest names for this pair"
    )]
    fn mutual_recursion_return_type_converges_by_fixpoint() {
        // `ping`'s return type is `unify(Float, pong's return type)`; `pong`'s
        // return type is exactly `ping`'s return type. Neither def has a
        // concrete return type on its own — round 0 sees the other's
        // `Unknown` placeholder — so this only converges to `Float` because
        // the batch is re-solved until stable (the SCC fixpoint), not in a
        // single pass.
        let (hir, index, res) = build(
            "=== function ping(n) ===\n{n == 0:\n  ~ return 0.0\n}\n~ return pong(n - 1)\n\
             === function pong(n) ===\n~ return ping(n)\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let ping_sig = sig_of(&result, &index, "ping");
        let pong_sig = sig_of(&result, &index, "pong");
        assert_eq!(ping_sig.return_ty, Ty::Float);
        assert_eq!(pong_sig.return_ty, Ty::Float);
    }

    #[test]
    fn intrinsic_len_types_int() {
        let (hir, index, res) =
            build("=== main ===\n~ temp arr = #[1, 2, 3]\n~ temp n = len(arr)\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(body.locals.get("arr"), Some(&Ty::Array(Box::new(Ty::Int))));
        assert_eq!(body.locals.get("n"), Some(&Ty::Int));
    }

    #[test]
    fn determinism_same_input_same_output() {
        let src = "=== function fib(n) ===\n{n < 2.0:\n  ~ return n\n}\n~ return fib(n - 1) + fib(n - 2)\n";
        let (hir_a, index_a, res_a) = build(src);
        let (hir_b, index_b, res_b) = build(src);
        let a = infer_project(
            &[(FileId(0), &hir_a)],
            &index_a,
            &res_a,
            None,
            &BTreeMap::new(),
        );
        let b = infer_project(
            &[(FileId(0), &hir_b)],
            &index_b,
            &res_b,
            None,
            &BTreeMap::new(),
        );
        assert_eq!(a, b, "same input must infer identical types every run");
    }

    // ─── Conflicted lattice point (#627) ───────────────────────────────

    #[test]
    fn genuinely_disjoint_uses_infer_param_as_conflicted() {
        // `hp` is compared against an int literal and a string literal —
        // a genuine, irreconcilable conflict. Pre-#627 this degraded to
        // `Unknown`, indistinguishable from "never observed".
        let (hir, index, res) = build(
            "=== conflict_case(hp) ===\n{hp > 5:\n  ok\n}\n{hp == \"no\":\n  no\n}\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "conflict_case");
        assert_eq!(sig.params, vec![Ty::Conflicted]);
    }

    #[test]
    fn conflict_detection_is_order_independent_across_real_source() {
        // The exact bug #627 exists to close: `unify(Int, String)` used to
        // degrade to `Unknown`, and `observe` short-circuits on an
        // `Unknown` candidate (a legitimate optimization for the true
        // identity element) — so which concrete type "won" depended on
        // which comparison the walk reached *last*, silently masking the
        // conflict as a normal concrete type instead of surfacing it. Both
        // source orderings below must now infer the same `Conflicted`
        // param, proving detection no longer depends on declaration order.
        let forward =
            "=== conflict_fwd(hp) ===\n{hp > 5:\n  ok\n}\n{hp == \"no\":\n  no\n}\n-> DONE\n";
        let reversed =
            "=== conflict_rev(hp) ===\n{hp == \"no\":\n  no\n}\n{hp > 5:\n  ok\n}\n-> DONE\n";

        let (hir_f, index_f, res_f) = build(forward);
        let result_f = infer_project(
            &[(FileId(0), &hir_f)],
            &index_f,
            &res_f,
            None,
            &BTreeMap::new(),
        );
        let sig_f = sig_of(&result_f, &index_f, "conflict_fwd");

        let (hir_r, index_r, res_r) = build(reversed);
        let result_r = infer_project(
            &[(FileId(0), &hir_r)],
            &index_r,
            &res_r,
            None,
            &BTreeMap::new(),
        );
        let sig_r = sig_of(&result_r, &index_r, "conflict_rev");

        assert_eq!(sig_f.params, vec![Ty::Conflicted], "int-then-string order");
        assert_eq!(sig_r.params, vec![Ty::Conflicted], "string-then-int order");
        assert_eq!(
            sig_f.params, sig_r.params,
            "conflict detection must not depend on observation order"
        );
    }

    #[test]
    #[expect(
        clippy::similar_names,
        reason = "ping/pong are the clearest names for this pair"
    )]
    fn conflicted_absorbs_through_the_scc_fixpoint() {
        // `ping`'s own base case returns a string; `pong`'s own base case
        // returns an int; each recursive case returns whatever the other
        // member currently resolves to. Neither member's own body is
        // internally conflicted (each sees only one concrete literal type
        // directly), but the two base cases can never agree once threaded
        // through the SCC's shared fixpoint — join stays monotone, so once
        // either member's estimate becomes `Conflicted` mid-fixpoint it
        // must propagate to the other and never get diluted back to
        // `Unknown` in a later round (the #627 ruling's "SCC fixpoint
        // convergence is unaffected" clause, proven end to end here rather
        // than just at the `unify` unit level).
        let (hir, index, res) = build(
            "=== function ping(n) ===\n{n == 0:\n  ~ return \"done\"\n}\n~ return pong(n - 1)\n\
             === function pong(n) ===\n{n == 0:\n  ~ return 1\n}\n~ return ping(n - 1)\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let ping_sig = sig_of(&result, &index, "ping");
        let pong_sig = sig_of(&result, &index, "pong");
        assert_eq!(ping_sig.return_ty, Ty::Conflicted);
        assert_eq!(pong_sig.return_ty, Ty::Conflicted);
    }

    // ─── Issue #1680 step 3: the effect row riding `Ty::Fn` ────────────
    //     (`docs/effects-spec.md` §5/§6.1c)

    /// §5: "a cell accumulates the join of every fn value assigned into it".
    /// Two `#fn` literals written to one slot leave **both** targets on the
    /// slot's type — the join is set union, not last-write-wins.
    #[test]
    fn a_slot_written_from_two_creation_sites_carries_both_targets() {
        let (hir, index, res) = build(
            "=== function bump(n: int): int ===\n~ return n + 1\n\
             === function twice(n: int): int ===\n~ return n * 2\n\
             === main ===\n~ temp f = #fn(bump)\n~ f = #fn(twice)\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let id_of = |name: &str| {
            index
                .by_name
                .get(name)
                .and_then(|ids| ids.first())
                .copied()
                .unwrap_or_else(|| unreachable!("no symbol named {name}"))
        };
        let body = result.bodies.get(&id_of("main")).expect("main body");
        let f = body.locals.get("f").expect("f");
        let Ty::Fn(_, _, row) = f else {
            unreachable!("expected a fn type, got {f:?}")
        };
        assert_eq!(
            row.targets(),
            Some(&BTreeSet::from([id_of("bump"), id_of("twice")]))
        );
    }

    /// The top element absorbs (§3): one write whose source the type layer
    /// cannot name — here a call's return, whose declared `fn(int): int`
    /// names no creation target — poisons the slot's row for good, in
    /// either write order. This is the type-layer twin of §6.1a's "a single
    /// untraced write poisons the name".
    #[test]
    fn one_unnameable_creation_site_poisons_the_row() {
        for order in [
            "~ temp f = #fn(bump)\n~ f = pick(#fn(bump))\n",
            "~ temp f = pick(#fn(bump))\n~ f = #fn(bump)\n",
        ] {
            let (hir, index, res) = build(&format!(
                "=== function bump(n: int): int ===\n~ return n + 1\n\
                 === function pick(cb: fn(int): int): fn(int): int ===\n~ return cb\n\
                 === main ===\n{order}-> DONE\n"
            ));
            let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
            let main_id = index
                .by_name
                .get("main")
                .and_then(|ids| ids.first())
                .copied()
                .expect("main");
            let body = result.bodies.get(&main_id).expect("main body");
            let f = body.locals.get("f").expect("f");
            let Ty::Fn(_, _, row) = f else {
                unreachable!("expected a fn type for {order:?}, got {f:?}")
            };
            assert!(row.is_unknown(), "order {order:?} must poison the row");
        }
    }

    /// The second minter: a global cell whose initializer is a `#fn`
    /// literal gets its `Ty::Fn` from `signature::declared_fn_type`, so its
    /// row must name the target too — declaration-derived, resolved by name
    /// lookup, never from an inferred row (§6.1a). This is the shape §6
    /// mechanism 3 (the heap) will read once effects-spec §6.1c's stratum
    /// question is answered.
    #[test]
    fn a_global_fn_cell_carries_its_declared_creation_target() {
        let (hir, index, res) = build(
            "=== function heal(ref hp: int, amount: int): int ===\n~ hp = hp + amount\n~ return hp\n\
             VAR player_hp = 10\n\
             VAR healer = #fn(heal, player_hp)\n\
             === main ===\n-> DONE\n",
        );
        let _ = &res;
        let files = [(FileId(0), &hir)];
        let id_of = |name: &str| {
            index
                .by_name
                .get(name)
                .and_then(|ids| ids.first())
                .copied()
                .unwrap_or_else(|| unreachable!("no symbol named {name}"))
        };
        let sig = crate::signature::signature(id_of("healer"), &index, &files, None)
            .expect("healer signature");
        let ty = sig.value_ty.clone().expect("healer value_ty");
        let Ty::Fn(params, _, row) = &ty else {
            unreachable!("expected a fn type, got {ty:?}")
        };
        assert_eq!(params.len(), 1, "the `ref hp` prefix is bound away");
        assert_eq!(row.targets(), Some(&BTreeSet::from([id_of("heal")])));
    }

    /// `bind` carries the row through unchanged: partial application never
    /// changes *which* def eventually runs (§6.1a).
    #[test]
    fn bind_preserves_the_creation_target_row() {
        let (hir, index, res) = build(
            "=== function add(a: int, b: int): int ===\n~ return a + b\n\
             === main ===\n~ temp f = #fn(add)\n~ temp g = bind(f, 1)\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let id_of = |name: &str| {
            index
                .by_name
                .get(name)
                .and_then(|ids| ids.first())
                .copied()
                .unwrap_or_else(|| unreachable!("no symbol named {name}"))
        };
        let body = result.bodies.get(&id_of("main")).expect("main body");
        let g = body.locals.get("g").expect("g");
        let Ty::Fn(params, _, row) = g else {
            unreachable!("expected a fn type, got {g:?}")
        };
        assert_eq!(params.len(), 1, "one param remains after binding one");
        assert_eq!(row.targets(), Some(&BTreeSet::from([id_of("add")])));
    }

    // ─── T1c: #fn typing + the annotation-firewall overlay ─────────────

    /// The spec's own worked example (docs/t1c-spec.md §2/§4): with the
    /// target fully annotated, `#fn(heal, player_hp)` consumes the bound
    /// prefix and types as `fn(int): int`.
    #[test]
    fn fn_literal_consumes_the_bound_prefix_of_the_targets_signature() {
        let (hir, index, res) = build(
            "=== function heal(ref hp: int, amount: int): int ===\n~ hp = hp + amount\n~ return hp\n\
             VAR player_hp = 10\n\
             === main ===\n~ temp heal_player = #fn(heal, player_hp)\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let body = result.bodies.get(&main_id).expect("main body");
        let heal_id = index
            .by_name
            .get("heal")
            .and_then(|ids| ids.first())
            .copied()
            .expect("heal");
        let cb = body.locals.get("heal_player").expect("heal_player");
        assert_eq!(
            crate::infer::erase_fn_rows(cb),
            Ty::Fn(vec![Ty::Int], Box::new(Ty::Int), FnRow::unknown())
        );
        // Issue #1680 step 3: the `#fn` literal is the creation site, so
        // the slot's type carries `heal` as its effect row.
        let Ty::Fn(_, _, row) = cb else {
            unreachable!("expected a fn type, got {cb:?}")
        };
        assert_eq!(row.targets(), Some(&BTreeSet::from([heal_id])));
    }

    #[test]
    fn fn_literal_over_an_inferred_signature_needs_no_annotations() {
        // The target's row can come from body inference alone.
        let (hir, index, res) = build(
            "=== function double(x) ===\n~ return x * 2\n\
             === main ===\n~ temp f = #fn(double)\n-> DONE\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let body = result.bodies.get(&main_id).expect("main body");
        let f = body.locals.get("f").expect("f");
        assert_eq!(
            crate::infer::erase_fn_rows(f),
            Ty::Fn(vec![Ty::Int], Box::new(Ty::Int), FnRow::unknown())
        );
    }

    #[test]
    fn fn_literal_with_unresolvable_target_stays_unknown() {
        let (hir, index, res) = build("=== main ===\n~ temp f = #fn(nowhere)\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let body = result.bodies.get(&main_id).expect("main body");
        assert_eq!(body.locals.get("f"), Some(&Ty::Unknown));
    }

    /// T1c overlay: an annotated param the body never constrains surfaces
    /// its annotation type in the inferred signature (the firewall applied
    /// to the signature — a `#fn` row built from it must be concrete).
    #[test]
    fn annotated_but_unconstrained_param_overlays_to_the_annotation_type() {
        let (hir, index, res) = build("=== noop(x: int) ===\nHello.\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "noop");
        assert_eq!(sig.params, vec![Ty::Int]);
    }

    /// Overlay is Unknown-only: a body use that disagrees with the
    /// annotation keeps its own derivation (E063's two-independent-
    /// derivations comparison, and the #627 Conflicted lattice, untouched).
    #[test]
    fn overlay_never_replaces_a_concrete_body_derivation() {
        let (hir, index, res) = build("=== heal(hp: string) ===\n{hp > 1:\n  ok\n}\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "heal");
        assert_eq!(sig.params, vec![Ty::Int], "body derivation wins");
    }

    // ─── Issue #1168: Option-returning functions escape as `Option[Unknown]` ─

    /// The issue's tightest repro: `some(x)` where `x` is an annotated
    /// param used *only* as `some`'s argument — no comparison/arithmetic
    /// anywhere else in the body ever gives `x` evidence the old code path
    /// could pick up. `some`'s arg type is a pure read (never joined
    /// against a second operand), so it should still see `x`'s own
    /// declared type, settling the return as `Option[int]`, not
    /// `Option[Unknown]`.
    #[test]
    fn some_of_an_unevidenced_annotated_param_infers_option_of_its_annotation() {
        let (hir, index, res) = build("=== function f(x: int) ===\n~ return some(x)\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "f");
        assert_eq!(sig.return_ty, Ty::Option(Box::new(Ty::Int)));
    }

    /// `get(m, k)` where `m` is an annotated `Map<...>` param, likewise
    /// never evidenced elsewhere — the confirmation comment's second
    /// repro ("`get(<any map>)` … infer `Option[Unknown]`").
    #[test]
    fn get_of_an_unevidenced_annotated_map_param_infers_option_of_the_value_type() {
        let (hir, index, res) =
            build("=== function f(m: Map<string, int>, k: string) ===\n~ return get(m, k)\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "f");
        assert_eq!(sig.return_ty, Ty::Option(Box::new(Ty::Int)));
    }

    /// `iteration.md`'s `first_over` fence: a `for` loop over an annotated
    /// `Array<int>` param used nowhere else, `return some(<the loop var>)`
    /// on one path and `return none` on the other. Regression for the
    /// iterable-position half of #1168 (the loop var itself escaped too,
    /// since its type comes from the iterable's element type).
    #[test]
    fn some_of_a_for_loop_var_over_an_unevidenced_annotated_array_param() {
        let (hir, index, res) = build(
            "=== function first_over(tab: Array<int>, floor: int) ===\n\
             ~ {\n    for coins in tab {\n        if coins > floor {\n            return some(coins)\n        }\n    }\n}\n\
             ~ return none\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "first_over");
        assert_eq!(sig.return_ty, Ty::Option(Box::new(Ty::Int)));
    }

    /// `infer_infix`'s comparison/arithmetic arms must NOT get the new
    /// read-site annotation fallback — this is the same fixture as
    /// `overlay_never_replaces_a_concrete_body_derivation` above, repeated
    /// here to pin it as the #1168 fix's own regression guard: `hp` is
    /// annotated `string` but the body's only use compares it against an
    /// int literal, so body evidence (`int`) must still win outright, not
    /// `unify(string, int) = Conflicted`.
    #[test]
    fn comparison_evidence_still_overrides_the_annotation_after_the_1168_fix() {
        let (hir, index, res) = build("=== heal(hp: string) ===\n{hp > 1:\n  ok\n}\n-> DONE\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "heal");
        assert_eq!(sig.params, vec![Ty::Int]);
    }

    /// Review correction (w65, changeset wording): only an ANNOTATED param
    /// or an ASCRIBED temp reaches `self.annotated` (`infer_def_body`'s
    /// `annotated` map + `register_ascription`) — an unascribed temp
    /// merely *copying* an annotated param's value does not inherit that
    /// annotation transitively. `v` here has no `: T` ascription of its
    /// own, so `some(v)` still infers `Option[Unknown]`, pinning the
    /// boundary the `.changeset/issue-1168-option-return-inference.md`
    /// wording now names explicitly ("annotated param / ascribed temp",
    /// not any "param/temp passed straight through").
    #[test]
    fn unascribed_temp_copy_of_an_annotated_param_does_not_inherit_the_annotation() {
        let (hir, index, res) =
            build("=== function f(x: int) ===\n~ temp v = x\n~ return some(v)\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "f");
        assert_eq!(sig.return_ty, Ty::Option(Box::new(Ty::Unknown)));
    }

    /// Review correction (w65): `contains`'s `self.observe(needle, elem)`
    /// call derives `elem` from `arg_tys[0]` (the container's shape) — if
    /// that shape were read from `tab`'s own annotation-fallback type
    /// (`read_tys`) instead of its evidence-only type (`arg_tys`), `tab`'s
    /// `Array<int>` annotation would become body *evidence* for `needle`
    /// (the sibling arg), silently discarding `needle`'s own `string`
    /// annotation. `tab` has no other evidence anywhere in the body, so
    /// this pins that `contains`'s observe call never reads the
    /// annotation-shadowed slice: `needle` must still export its own
    /// declared `string`, not `tab`'s element type `int`.
    #[test]
    fn intrinsic_sibling_arg_never_seeds_from_a_containers_own_annotation() {
        let (hir, index, res) = build(
            "=== function f(tab: Array<int>, needle: string) ===\n\
             ~ return contains(tab, needle)\n",
        );
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "f");
        assert_eq!(sig.params, vec![Ty::Array(Box::new(Ty::Int)), Ty::String]);
    }

    #[test]
    fn return_annotation_overlays_an_unconstrained_return() {
        // `return hp` types Unknown from the body alone (nothing pins hp
        // before the return); the `): int` annotation overlays it.
        let (hir, index, res) = build("=== function passthru(hp): int ===\n~ return hp\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "passthru");
        assert_eq!(sig.return_ty, Ty::Int);
    }

    /// Issue #1912: the *param*-annotation counterpart of the test above —
    /// `~ return hp` with `hp: int` annotated and no return annotation at
    /// all now exports `int` rather than `Unknown`, because
    /// `infer_return` runs the returned value through `or_own_annotation`
    /// (a pure read, no counter-evidence). The ink spelling is checked here
    /// alongside the native one in `strict::tests` because the gap was in
    /// `infer::body`, shared by both frontends.
    #[test]
    fn returning_an_annotated_param_exports_the_params_type() {
        let (hir, index, res) = build("=== function passthru(hp: int) ===\n~ return hp\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "passthru");
        assert_eq!(sig.return_ty, Ty::Int);
    }

    /// The boundary that stays put (issue #1912 must not widen into #1168's
    /// w65 correction): `or_own_annotation` overlays an `Unknown` only, so
    /// a *concrete* body derivation still wins outright and
    /// `annotations::mismatches` keeps two independent derivations to
    /// compare. `hp` is used as a `string` here, so the return type is
    /// `string` — the annotation does not launder it back to `int`.
    #[test]
    fn a_concrete_body_derivation_still_beats_the_returned_params_annotation() {
        let (hir, index, res) = build("=== function passthru(hp: int) ===\n~ return hp + \"x\"\n");
        let result = infer_project(&[(FileId(0), &hir)], &index, &res, None, &BTreeMap::new());
        let sig = sig_of(&result, &index, "passthru");
        assert_eq!(sig.params, vec![Ty::String]);
        assert_eq!(sig.return_ty, Ty::String);
    }

    // ─── Per-def/per-SCC decomposition (FG-2, issue #631) ─────────────

    #[test]
    fn call_edges_matches_the_calls_infer_project_discovers() {
        let (hir, index, res) = build(
            "=== main ===\n~ temp v = 1\n~ use_it(v)\n-> DONE\n=== use_it(n) ===\n{n > 2.5:\n  big\n}\n-> DONE\n",
        );
        let files = [(FileId(0), &hir)];
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let use_it_id = index
            .by_name
            .get("use_it")
            .and_then(|ids| ids.first())
            .copied()
            .expect("use_it");

        let inferable = inferable_defs_from_index(&index);
        let edges = call_edges(main_id, &files, &index, &res, &inferable, None);
        assert_eq!(
            edges,
            BTreeSet::from([use_it_id]),
            "main's only call edge is to use_it"
        );
        let leaf_edges = call_edges(use_it_id, &files, &index, &res, &inferable, None);
        assert!(leaf_edges.is_empty(), "use_it calls nothing");
    }

    #[test]
    fn call_edges_is_empty_for_an_unknown_def() {
        let (hir, index, res) = build("=== main ===\nHello.\n-> DONE\n");
        let files = [(FileId(0), &hir)];
        let bogus = DefinitionId::new(brink_format::DefinitionTag::Address, 0xDEAD_BEEF);
        let inferable = inferable_defs_from_index(&index);
        assert!(call_edges(bogus, &files, &index, &res, &inferable, None).is_empty());
    }

    // ─── Lazy per-reference globals (FG-2.1, issue #638) ───────────────

    #[test]
    fn inferable_defs_from_index_matches_hir_derived_set() {
        // Same three fixtures the FG-2/#626 tests already carry (plain
        // mutual call, floating stitch, nested stitch) — the index-only
        // projection must agree with the HIR-walking one on every shape
        // `collect_defs` handles, not just the easy case.
        let fixtures = [
            "=== main ===\n~ temp v = 1\n~ use_it(v)\n-> DONE\n=== use_it(n) ===\n{n > 2.5:\n  big\n}\n-> DONE\n",
            "= heal(hp)\n~ temp x = hp + 1\n-> DONE\n",
            "= intro(hp)\n~ temp x = hp + 1\n-> DONE\n\
             === knot_a(gold) ===\n{gold > 1.5:\n  ok\n}\n-> stitch_a ->\n\
             = stitch_a(silver)\n~ temp y = silver + 1\n-> DONE\n",
        ];
        for src in fixtures {
            let (hir, index, _res) = build(src);
            let files = [(FileId(0), &hir)];
            assert_eq!(
                inferable_defs_from_index(&index),
                inferable_defs(&files, &index),
                "index-sourced and HIR-walking inferable sets diverged for: {src}"
            );
        }
    }

    #[test]
    fn referenced_globals_finds_every_var_and_const_read_in_a_body() {
        let (hir, index, res) = build(
            "VAR gold = 10\nCONST max_gold = 100\n\
             === spend(cost) ===\n~ gold = gold - cost\n{gold > max_gold:\n  rich\n}\n-> DONE\n",
        );
        let files = [(FileId(0), &hir)];
        let spend_id = index
            .by_name
            .get("spend")
            .and_then(|ids| ids.first())
            .copied()
            .expect("spend");
        let gold_id = index
            .by_name
            .get("gold")
            .and_then(|ids| ids.first())
            .copied()
            .expect("gold");
        let max_gold_id = index
            .by_name
            .get("max_gold")
            .and_then(|ids| ids.first())
            .copied()
            .expect("max_gold");

        let global_refs = referenced_globals(spend_id, &files, &index, &res, None);
        assert_eq!(
            global_refs,
            BTreeSet::from([gold_id, max_gold_id]),
            "spend's body reads both gold and max_gold"
        );
    }

    #[test]
    fn referenced_globals_is_empty_when_a_body_reads_no_globals() {
        let (hir, index, res) = build("=== main ===\n~ temp v = 1\n-> DONE\n");
        let files = [(FileId(0), &hir)];
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        assert!(referenced_globals(main_id, &files, &index, &res, None).is_empty());
    }

    #[test]
    fn inferable_defs_matches_every_knot_and_stitch() {
        let (hir, index, res) = build(
            "=== main ===\n~ temp v = 1\n~ use_it(v)\n-> DONE\n=== use_it(n) ===\n{n > 2.5:\n  big\n}\n-> DONE\n",
        );
        let files = [(FileId(0), &hir)];
        let _ = &res;
        let defs = inferable_defs(&files, &index);
        let main_id = index
            .by_name
            .get("main")
            .and_then(|ids| ids.first())
            .copied()
            .expect("main");
        let use_it_id = index
            .by_name
            .get("use_it")
            .and_then(|ids| ids.first())
            .copied()
            .expect("use_it");
        assert_eq!(defs, BTreeSet::from([main_id, use_it_id]));
    }

    /// The decomposition equivalence gate the design doc's §9 FG-2 bullet
    /// asks for: composing `call_edges` -> `scc_graph` -> `solve_scc` per
    /// component, in dependency order, must equal a single `infer_project`
    /// call over the exact same inputs. Uses the mutual-recursion fixture
    /// (a real multi-round SCC fixpoint, not just a linear chain) so the
    /// composed path actually exercises cross-SCC signature threading.
    #[test]
    fn composed_per_scc_solve_equals_monolithic_infer_project() {
        let src = "=== function ping(n) ===\n{n == 0:\n  ~ return 0.0\n}\n~ return pong(n - 1)\n\
                   === function pong(n) ===\n~ return ping(n)\n\
                   === caller ===\n~ temp x = ping(3)\n-> DONE\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];

        let monolithic = infer_project(&files, &index, &res, None, &BTreeMap::new());

        // Compose: call_edges per def -> merged CallGraph -> scc_graph ->
        // solve_scc per component, threading known_sigs in dependency order
        // exactly like `solve_batches` does internally. Every per-def input
        // (defs, globals, inferable) is built the same narrowed way
        // `brink-db`'s query wiring builds it (FG-2.1, issue #638), not by
        // handing the whole-project HIR straight to `collect_defs`/
        // `collect_globals` the way the pre-#638 version of this test did.
        let defs = inferable_defs_from_index(&index);
        let mut graph = CallGraph::new();
        for &def in &defs {
            graph.add_node(def);
            for callee in call_edges(def, &files, &index, &res, &defs, None) {
                graph.add_edge(def, callee);
            }
        }
        let sg = scc_graph(&graph);

        let mut known_sigs: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
        let mut signatures: BTreeMap<DefinitionId, InferredSig> = BTreeMap::new();
        let mut bodies: BTreeMap<DefinitionId, BodyTypes> = BTreeMap::new();
        for batch in &sg.order {
            // Per-def HIR projection (Ruling 2b): only this batch's own
            // members' bodies, never the whole project's.
            let owned: Vec<(DefinitionId, Vec<Param>, Option<TypeExpr>, Block)> = batch
                .iter()
                .filter_map(|&id| def_body(id, &files, &index).map(|(p, ra, b)| (id, p, ra, b)))
                .collect();
            let batch_defs: Vec<Def<'_>> = owned
                .iter()
                .map(|(id, params, return_annotation, body)| Def {
                    id: *id,
                    file: FileId(0),
                    params,
                    body,
                    return_annotation: return_annotation.as_ref(),
                    native: false,
                })
                .collect();

            // Pre-scan + narrow map (Ruling 1): union of every member's
            // referenced_globals, resolved through signature() — never
            // collect_globals's whole-project scan.
            let mut global_ids: BTreeSet<DefinitionId> = BTreeSet::new();
            for &id in batch {
                global_ids.extend(referenced_globals(id, &files, &index, &res, None));
            }
            let mut globals: BTreeMap<DefinitionId, Ty> = BTreeMap::new();
            for gid in global_ids {
                if let Some(sig) = crate::signature::signature(gid, &index, &files, None)
                    && let Some(vt) = sig.value_type.clone()
                {
                    globals.insert(gid, Ty::from(vt));
                }
            }

            let (sigs, bods) = solve_scc(
                batch,
                &batch_defs,
                &index,
                &res,
                &globals,
                &defs,
                known_sigs.clone(),
                None,
                &BTreeMap::new(),
            );
            known_sigs.extend(sigs.iter().map(|(k, v)| (*k, v.clone())));
            signatures.extend(sigs);
            bodies.extend(bods);
        }
        let composed = InferenceResult { signatures, bodies };

        assert_eq!(
            composed, monolithic,
            "per-SCC composed inference must equal a single infer_project call"
        );
    }

    // ─── T2-1 effect rows (docs/effects-spec.md §2/§4, issue #860) ───────

    fn id_of(index: &SymbolIndex, name: &str) -> DefinitionId {
        index
            .by_name
            .get(name)
            .and_then(|ids| ids.first())
            .copied()
            .expect("no def with this name")
    }

    /// THE conservative-total soundness gate (docs/effects-spec.md §3, issue
    /// #860): for every def, the inferred row must **cover** (⊒) its own body
    /// atoms *and* every direct callee's finalized row — the no-under-report
    /// invariant. Exercised over a mutually-recursive fixture (`ping <-> pong`)
    /// so the check runs against a real multi-round SCC fixpoint, plus a
    /// higher-order value-call (`apply`) so the pessimal floor is in the mix,
    /// plus a caller (`hocaller`) that **instantiates** `apply`'s §6.1 row
    /// variable (issue #1680, Fork C) so check (2) below has to reason about a
    /// holed callee, not only ground ones.
    #[test]
    fn conservative_total_no_under_report_over_mutual_recursion() {
        let src = "VAR gold = 0\nVAR hp = 10\nEXTERNAL play_sfx(x)\n\
                   === function ping(n) ===\n~ gold = gold + 1\n\
                   {n == 0:\n  ~ return 0\n}\n~ play_sfx(n)\n~ return pong(n - 1)\n\
                   === function pong(n) ===\n~ hp = hp - 1\n~ return ping(n)\n\
                   === function apply(cb) ===\n~ return cb(1)\n\
                   === caller ===\n~ temp x = ping(3)\n-> DONE\n\
                   === hocaller ===\n~ temp y = apply(#fn(pong))\n-> DONE\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let inferable = inferable_defs(&files, &index);

        let rows = effects_project(&files, &index, &res, None);

        for &def in &inferable {
            let row = rows.get(&def).cloned().unwrap_or_default();
            let atoms = def_effect_atoms(def, &files, &index, &res, &inferable, None);

            // (1) covers its own body atoms.
            assert!(
                row.covers(&atoms.base_row()),
                "def {def:?} row must cover its own body atoms"
            );

            // (2) covers every direct callee's finalized row —
            // instantiation-aware for a holed callee (issue #1680 review
            // finding). A callee row still carrying a §6.1 hole is itself
            // pessimal by construction (`is_pessimal`), so it is never a
            // meaningful target for `covers`: no non-opaque caller could ever
            // cover it, which would make this gate reject exactly the rows
            // #1680 ships as sound. What the caller actually owes is the
            // callee's *instantiated* row — its ground atoms joined with
            // whatever this call site traced into each hole — the same
            // computation `solve_scc_effects` folds into `row` itself via
            // `instantiate_hole`.
            for callee in &atoms.direct_calls {
                let callee_row = rows.get(callee).cloned().unwrap_or_default();
                let mut effective = EffectRow {
                    holes: BTreeSet::new(),
                    ..callee_row.clone()
                };
                for &hole in &callee_row.holes {
                    effects::instantiate_hole(
                        &mut effective,
                        atoms.call_fn_args.get(&(*callee, hole)),
                        &rows,
                        &BTreeMap::new(),
                    );
                }
                assert!(
                    row.covers(&effective),
                    "def {def:?} row must cover callee {callee:?}'s instantiated row"
                );
            }
        }
    }

    #[test]
    fn effect_row_collects_read_write_and_external_call_atoms() {
        let src = "VAR gold = 0\nVAR hp = 10\nEXTERNAL play_sfx(x)\n\
                   === function spend(cost) ===\n~ gold = gold - cost\n\
                   ~ temp before = hp\n~ play_sfx(cost)\n~ return gold\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);

        let spend = id_of(&index, "spend");
        let gold = id_of(&index, "gold");
        let hp = id_of(&index, "hp");
        let row = &rows[&spend];

        assert!(row.reads.contains(&gold), "reads gold ({gold:?})");
        assert!(row.reads.contains(&hp), "reads hp ({hp:?})");
        assert!(row.writes.contains(&gold), "writes gold ({gold:?})");
        assert!(!row.writes.contains(&hp), "never writes hp");
        assert!(row.calls.contains("play_sfx"), "calls the external kind");
        assert!(!row.opaque, "a fully-visible body is not pessimal");
    }

    // ─── NS-A6 (issue #1112, docs/stdlib-spec.md §7): every draw is an
    // ordinary write to the RNG cell in the row ─────────────────────────

    /// Every brink draw-verb spelling harvests a write to
    /// `DefinitionId::RNG_CELL` — the "draws = writes" half of the
    /// rng-as-cell ruling.
    #[test]
    fn rand_draw_verbs_write_the_rng_cell() {
        use brink_format::DefinitionId;
        let cases: &[(&str, &str)] = &[
            (
                "float_draw",
                "=== function float_draw() ===\n~ return float()\n",
            ),
            (
                "chance_draw",
                "=== function chance_draw() ===\n~ return chance(0.5)\n",
            ),
            (
                "pick_draw",
                "=== function pick_draw() ===\n~ temp a = #[1, 2, 3]\n~ return pick(a)\n",
            ),
            (
                "shuffled_draw",
                "=== function shuffled_draw() ===\n~ temp a = #[1, 2, 3]\n~ return shuffled(a)\n",
            ),
            (
                "shuffle_stmt",
                "VAR deck = 0\n=== function shuffle_stmt() ===\n~ shuffle(deck)\n~ return 0\n",
            ),
            (
                "seed_stmt",
                "=== function seed_stmt() ===\n~ seed(42)\n~ return 0\n",
            ),
        ];
        for (name, src) in cases {
            let (hir, index, res) = build(src);
            let files = [(FileId(0), &hir)];
            let rows = effects_project(&files, &index, &res, None);
            let def = id_of(&index, name);
            assert!(
                rows[&def].writes.contains(&DefinitionId::RNG_CELL),
                "`{name}`'s row must contain the RNG-cell write; got {:?}",
                rows[&def].writes
            );
        }
    }

    /// The frozen ink spellings write the SAME cell — one RNG, two
    /// surfaces, one row entry (no drift).
    #[test]
    fn frozen_ink_random_spellings_write_the_same_rng_cell() {
        use brink_format::DefinitionId;
        let cases: &[(&str, &str)] = &[
            (
                "roll_ink",
                "=== function roll_ink() ===\n~ return RANDOM(1, 6)\n",
            ),
            (
                "seed_ink",
                "=== function seed_ink() ===\n~ SEED_RANDOM(9)\n~ return 0\n",
            ),
            (
                "pick_ink",
                "LIST moods = happy, sad\n=== function pick_ink() ===\n~ return LIST_RANDOM(moods)\n",
            ),
        ];
        for (name, src) in cases {
            let (hir, index, res) = build(src);
            let files = [(FileId(0), &hir)];
            let rows = effects_project(&files, &index, &res, None);
            let def = id_of(&index, name);
            assert!(
                rows[&def].writes.contains(&DefinitionId::RNG_CELL),
                "ink `{name}`'s row must contain the RNG-cell write; got {:?}",
                rows[&def].writes
            );
        }
    }

    /// The unary `float(x)` conversion intrinsic stays pure — only the
    /// nullary draw spelling touches the cell (the F4 arity split).
    #[test]
    fn unary_float_conversion_does_not_write_the_rng_cell() {
        use brink_format::DefinitionId;
        let src = "=== function conv(x) ===\n~ return float(x)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let def = id_of(&index, "conv");
        assert!(
            !rows[&def].writes.contains(&DefinitionId::RNG_CELL),
            "unary float(x) is the conversion — no draw, no cell write"
        );
        // And the nullary draw is total: no fault path.
        let src = "=== function draw() ===\n~ return float()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let draw = id_of(&index, "draw");
        assert!(
            !rows[&draw].faults,
            "nullary float() has no argument and no fault path"
        );
    }

    /// `shuffle(ref a)` records BOTH writes: the receiver cell (the #880
    /// mutator-call lesson) and the RNG cell.
    #[test]
    fn shuffle_writes_both_the_receiver_and_the_rng_cell() {
        use brink_format::DefinitionId;
        let src = "VAR deck = 0\n=== function riffle() ===\n~ shuffle(deck)\n~ return 0\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let def = id_of(&index, "riffle");
        let deck = id_of(&index, "deck");
        assert!(rows[&def].writes.contains(&deck), "writes the receiver");
        assert!(
            rows[&def].writes.contains(&DefinitionId::RNG_CELL),
            "writes the RNG cell"
        );
    }

    /// The rng write propagates transitively like any other write atom —
    /// a caller of a draw-bearing def carries the cell in its own row
    /// (this is what makes the pure-gated machinery exclude draws for
    /// free).
    #[test]
    fn rng_write_propagates_to_callers_through_the_fixpoint() {
        use brink_format::DefinitionId;
        let src = "=== function outer() ===\n~ return inner()\n\
                   === function inner() ===\n~ return chance(0.25)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        for name in ["outer", "inner"] {
            let def = id_of(&index, name);
            assert!(
                rows[&def].writes.contains(&DefinitionId::RNG_CELL),
                "`{name}` must carry the transitive RNG-cell write"
            );
        }
    }

    #[test]
    fn mutually_recursive_defs_share_the_unioned_row() {
        let src = "VAR gold = 0\nVAR hp = 10\n\
                   === function ping(n) ===\n~ gold = gold + 1\n\
                   {n == 0:\n  ~ return 0\n}\n~ return pong(n - 1)\n\
                   === function pong(n) ===\n~ hp = hp - 1\n~ return ping(n)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);

        let left = id_of(&index, "ping");
        let right = id_of(&index, "pong");
        let gold = id_of(&index, "gold");
        let hp = id_of(&index, "hp");

        // Both SCC members converge on the union of both writes.
        for def in [left, right] {
            let row = &rows[&def];
            assert!(row.writes.contains(&gold), "{def:?} writes gold");
            assert!(row.writes.contains(&hp), "{def:?} writes hp");
        }
    }

    #[test]
    fn a_call_through_a_function_value_is_pessimal() {
        // docs/effects-spec.md §4 gradual corollary: an `Unknown`-typed callee
        // slot (here a `cb` param called as `cb(1)`) has no row to read → the
        // enclosing def's row is pessimal.
        //
        // §6.1 (issue #1680) changed *how* it is pessimal, not *that* it is:
        // the param is now a row variable rather than the intrinsic opaque
        // floor, so the assertion reads `is_pessimal()` — which is what every
        // consumer of a row reads.
        let src = "=== function apply(cb) ===\n~ return cb(1)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let apply = id_of(&index, "apply");
        assert!(
            rows[&apply].is_pessimal(),
            "a call through a function value must be pessimal"
        );
    }

    /// §6.1 mechanism 1 (issue #1680): a call through an unwritten, non-`ref`
    /// fn-typed param mints a **row variable** at that param's declaration
    /// index instead of the intrinsic opaque floor. Read on its own the row
    /// is still pessimal — that is `is_pessimal`'s whole job — but the hole
    /// is what lets a caller do better (see the instantiation tests below).
    #[test]
    fn a_call_through_a_fn_typed_param_mints_a_row_variable() {
        let src = "=== function apply(a, cb) ===\n~ return cb(a)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let apply = id_of(&index, "apply");
        assert_eq!(
            rows[&apply].holes,
            [1].into_iter().collect::<BTreeSet<u32>>(),
            "the hole is keyed by the called param's declaration index"
        );
        assert!(
            !rows[&apply].opaque,
            "the floor is the hole, not intrinsic opacity"
        );
        assert!(
            rows[&apply].is_pessimal(),
            "an uninstantiated row variable still tops the lattice"
        );
    }

    /// §6.1's payoff: the caller passes a traceable `#fn` value, so the
    /// higher-order callee's row variable is **instantiated** with that
    /// target's real row and the caller escapes the pessimal floor entirely.
    #[test]
    fn a_caller_instantiates_the_callees_row_variable() {
        let src = "VAR gold = 0\n\
                   === function writer(n) ===\n~ gold = gold + n\n~ return gold\n\
                   === function apply(cb) ===\n~ return cb(1)\n\
                   === function main() ===\n~ return apply(#fn(writer))\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let main = id_of(&index, "main");
        let gold = id_of(&index, "gold");
        assert!(
            !rows[&main].is_pessimal(),
            "a fully-traced higher-order call is not pessimal"
        );
        assert!(
            rows[&main].holes.is_empty(),
            "a discharged hole belongs to the callee's param space, never the caller's"
        );
        assert!(
            rows[&main].writes.contains(&gold),
            "the instantiated row must carry the callback's own write"
        );
    }

    /// Two call sites, two different callbacks in the same position: the fill
    /// is the **join** over both (Fork A's join-over-writes rule applied to
    /// arguments), never a pick.
    #[test]
    fn two_call_sites_join_both_callbacks_into_the_hole() {
        let src = "VAR gold = 0\nVAR hp = 10\n\
                   === function pays(n) ===\n~ gold = gold + n\n~ return gold\n\
                   === function hurts(n) ===\n~ hp = hp - n\n~ return hp\n\
                   === function apply(cb) ===\n~ return cb(1)\n\
                   === function main() ===\n\
                   ~ temp a = apply(#fn(pays))\n~ temp b = apply(#fn(hurts))\n~ return a + b\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let main = id_of(&index, "main");
        assert!(!rows[&main].is_pessimal());
        assert!(rows[&main].writes.contains(&id_of(&index, "gold")));
        assert!(rows[&main].writes.contains(&id_of(&index, "hp")));
    }

    /// The soundness guard on the join above: the summary is keyed by
    /// `(callee, position)` and folded over *every* call site, so one site
    /// passing something untraceable poisons the position for all of them.
    /// Were it not, this caller's row would claim to be bounded by `pays`
    /// while `outside` could hold any fn value the caller was handed.
    #[test]
    fn one_untraced_call_site_poisons_the_whole_position() {
        let src = "VAR gold = 0\n\
                   === function pays(n) ===\n~ gold = gold + n\n~ return gold\n\
                   === function apply(cb) ===\n~ return cb(1)\n\
                   === function main(outside) ===\n\
                   ~ temp a = apply(#fn(pays))\n~ temp b = apply(outside)\n~ return a + b\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let main = id_of(&index, "main");
        assert!(
            rows[&main].is_pessimal(),
            "an untraced argument in a holed position must keep the floor"
        );
    }

    /// A param the body **reassigns** no longer holds what the caller passed,
    /// so it must not carry a row variable — the same soundness argument that
    /// keeps a Param out of `ValueCallOrigin::Local`.
    #[test]
    fn a_reassigned_param_carries_no_row_variable() {
        let src = "VAR gold = 0\n\
                   === function pays(n) ===\n~ gold = gold + n\n~ return gold\n\
                   === function apply(cb) ===\n~ cb = #fn(pays)\n~ return cb(1)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let apply = id_of(&index, "apply");
        assert!(
            rows[&apply].holes.is_empty(),
            "a written param is not a row variable"
        );
        assert!(
            rows[&apply].opaque,
            "it keeps the intrinsic pessimal floor instead"
        );
    }

    /// A `ref` param aliases the caller's own storage, so what it holds at
    /// the call-through site is not pinned by the argument expression — it is
    /// excluded from row variables at construction.
    #[test]
    fn a_ref_param_carries_no_row_variable() {
        let src = "=== function apply(ref cb) ===\n~ return cb(1)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let apply = id_of(&index, "apply");
        assert!(rows[&apply].holes.is_empty(), "`ref` params are excluded");
        assert!(rows[&apply].opaque, "so the call keeps the intrinsic floor");
    }

    /// §6.1 is shallow by ruling ("every value's row is fixed at its creation
    /// site"): passing one's *own* fn-typed param straight through to another
    /// higher-order callee would chain a hole into a hole, which is not
    /// attempted — the forwarding definition takes the floor.
    #[test]
    fn forwarding_a_param_into_another_hole_does_not_chain() {
        let src = "=== function apply(cb) ===\n~ return cb(1)\n\
                   === function forward(cb) ===\n~ return apply(cb)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let forward = id_of(&index, "forward");
        assert!(
            rows[&forward].is_pessimal(),
            "a forwarded row variable is not chained — the floor stands"
        );
    }

    #[test]
    fn a_pure_body_has_an_empty_row() {
        let src = "=== function double(n) ===\n~ return n * 2\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let double = id_of(&index, "double");
        assert!(
            rows[&double].is_empty(),
            "a pure arithmetic body reads/writes/calls nothing"
        );
    }

    /// Review-finding regression (issue #860's PR): a direct call passing a
    /// VAR/CONST global into a `ref` parameter slot writes through that
    /// parameter (docs/effects-spec.md §5 "through parameters") — the callee
    /// mutates the *caller's* cell. The exact fixture the reviewer supplied
    /// (`tests/tier1/variables/variable-pointer-ref-from-knot/story.ink`):
    /// `inc`'s own body atoms are empty (its assignment target `x` is a
    /// `Param`, never a `Variable`/`Constant`), so ground truth only shows up
    /// at `knot`'s own call site — the `conservative_total_no_under_report`
    /// property test above can never catch this since it only checks
    /// inter-row consistency, never this kind of ground-truth completeness.
    #[test]
    fn a_direct_call_writes_through_a_ref_param_at_the_call_site() {
        let src = "VAR val = 5\n\
                   === knot ===\n~ inc(val)\n{val}\n->->\n\
                   === function inc(ref x) ===\n~ x = x + 1\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);

        let knot = id_of(&index, "knot");
        let inc = id_of(&index, "inc");
        let val = id_of(&index, "val");

        assert!(
            rows[&knot].writes.contains(&val),
            "knot's call `inc(val)` writes through inc's `ref x` param — the \
             write atom must not be dropped"
        );
        assert!(
            !rows[&inc].writes.contains(&val),
            "inc's own body never names `val` — the write is only visible at \
             the call site, not inc's own atoms"
        );
    }

    // ─── T2 §8 precision rung (docs/effects-spec.md §6 item 3/§8, issue #872):
    // reading a concrete `EffectRow` off a stored `Ty::Fn` at an indirect/
    // value call site, instead of the pessimal placeholder, when the origin
    // is statically known ──────────────────────────────────────────────

    /// The core narrowing case: a write-once local holding a `#fn(target)`
    /// literal, called with the direct `f(args)` syntax. `user`'s row must
    /// stop being pessimal and instead cover `bar`'s real row (the write to
    /// `total`) — the exact improvement over the old unconditional-opaque
    /// floor `a_call_through_a_function_value_is_pessimal` still pins for
    /// the genuinely-unknown (param) case.
    #[test]
    fn known_fn_value_call_narrows_the_row_instead_of_pessimal() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function user() ===\n~ temp f = #fn(bar)\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "a call through a write-once local with a known #fn origin must narrow, not stay pessimal"
        );
        assert!(
            rows[&user].writes.contains(&total),
            "the narrowed row must cover bar's real write to total"
        );
    }

    /// Same shape, through the explicit `call(f, …)` intrinsic form —
    /// `check_value_call`'s other caller.
    #[test]
    fn known_fn_value_call_intrinsic_form_narrows_the_row() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function user() ===\n~ temp f = #fn(bar)\n~ return call(f)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "call(f) through a known origin must narrow"
        );
        assert!(rows[&user].writes.contains(&total));
    }

    /// A `bind(…)`-wrapped fn-value ("bound fn-values", the issue's own
    /// phrasing) stored in a write-once local — `bind` never changes which
    /// def eventually runs, so the origin still traces through.
    #[test]
    fn bound_fn_value_through_a_write_once_local_narrows() {
        let src = "VAR total = 0\n\
                   === function bar(n) ===\n~ total = total + n\n~ return total\n\
                   === function user() ===\n~ temp f = bind(#fn(bar), 5)\n~ return call(f)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "a bind()-wrapped known origin stored write-once must still narrow"
        );
        assert!(rows[&user].writes.contains(&total));
    }

    /// A fully inline `#fn(target)` literal passed straight into `call(…)`
    /// with no intermediate local at all — no stored-value/write-count
    /// question applies, so this narrows unconditionally.
    #[test]
    fn inline_fn_literal_at_the_call_site_narrows_without_a_stored_local() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function user() ===\n~ return call(#fn(bar))\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "an inline #fn literal callee must narrow"
        );
        assert!(rows[&user].writes.contains(&total));
    }

    /// Fork A (`docs/decision-log.md` 2026-07-28, issue #1726) supersedes the
    /// pre-#1726 write-once guard here. The old rule narrowed to a *single*
    /// def, so a local reassigned to a second known origin had to stay
    /// pessimal — picking either origin would under-report whichever branch
    /// didn't run. Joining **both** creation targets removes the choice: the
    /// row covers every value the local can hold, which over-reports at worst
    /// and so keeps the conservative-total direction (spec §3). The two
    /// origins write two *different* globals here so the join is visible —
    /// a single shared global would pass even if only one edge were taken.
    #[test]
    fn a_local_reassigned_to_a_second_known_origin_joins_both_rows() {
        let src = "VAR total = 0\nVAR extra = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function baz() ===\n~ extra = extra + 100\n~ return extra\n\
                   === function user(cond) ===\n~ temp f = #fn(bar)\n\
                   {cond:\n  ~ f = #fn(baz)\n}\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        let extra = id_of(&index, "extra");
        assert!(
            !rows[&user].opaque,
            "every write to f traced to an in-project creation site, so the \
             row must collapse to a real row instead of the pessimal floor"
        );
        assert!(
            rows[&user].writes.contains(&total),
            "the join must cover bar's write to total"
        );
        assert!(
            rows[&user].writes.contains(&extra),
            "the join must cover baz's write to extra — narrowing to a single \
             origin would under-report the other branch"
        );
    }

    /// The guard Fork A keeps: one write whose value did **not** trace to an
    /// in-project creation site poisons the whole name. Here `f` is
    /// reassigned from a param, so the reaching value could have been created
    /// anywhere — including a host callback (spec §6.2) — and the row must
    /// stay pessimal even though the *other* write is a perfectly good
    /// `#fn(bar)`.
    #[test]
    fn a_local_with_one_untraced_write_stays_pessimal() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function user(cond, cb) ===\n~ temp f = #fn(bar)\n\
                   {cond:\n  ~ f = cb\n}\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        assert!(
            rows[&user].opaque,
            "a write from an untraceable source must keep the pessimal floor"
        );
    }

    /// Review-finding regression (Fork A, issue #1726): a Temp local passed
    /// into a `ref` parameter slot is rebound by the *callee* to whatever the
    /// caller passed for that other position — `poke(f, cb)` below can leave
    /// `f` holding `cb`, an arbitrary caller-supplied value, exactly like the
    /// param-assignment case `a_local_with_one_untraced_write_stays_pessimal`
    /// covers. Before `record_ref_param_writes` folded this into
    /// `local_fn_origins` too, `f`'s summary saw only its one traced
    /// `#fn(bar)` write and Fork A's join-over-writes rule narrowed `user`'s
    /// row to `bar`'s alone — silently dropping the fact that `f` could also
    /// be `cb` after the `poke` call. The row must stay pessimal instead.
    #[test]
    fn a_ref_param_rebind_through_a_call_site_stays_pessimal() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function poke(ref g, h) ===\n~ g = h\n\
                   === function user(cond, cb) ===\n~ temp f = #fn(bar)\n\
                   {cond:\n  ~ poke(f, cb)\n}\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        assert!(
            rows[&user].opaque,
            "a ref-param rebind at a call site is an untraced write to the \
             local — narrowing through it under-reports whatever the caller \
             actually passed"
        );
    }

    // ─── Issue #1735: the fn-value aliasing channel enumeration ──────────
    //
    // Filed from the #1726/PR #1731 retro to check whether `ref` projections
    // and the heap are a genuine gap in `local_fn_origins` or a case
    // docs/effects-spec.md §5/§6.1a/§6.3 already rules coarse-but-sound. They
    // are the latter: §5 rules that a cell/collection's element *type*
    // accumulates the join of every fn value assigned into it — a
    // completely separate mechanism from this per-local write-set rung, and
    // "no separate points-to machinery exists or is planned". These two
    // tests pin that: a heap-sourced call never narrows, and a `ref`-param
    // write through a *global* root never leaks into (or out of) a Temp's
    // own write summary. No production change accompanies these — see
    // docs/effects-spec.md §6.1a's "Aliasing channel enumeration" addendum
    // for the ruling this pins.

    /// The heap channel (§5/§6.3): a fn value read out of a `VAR`/`CONST`
    /// cell is never classified as [`ValueCallOrigin::Local`] —
    /// [`InferPass::local_call_origin`] only recognizes `Temp`/`Param`
    /// symbol kinds, so a `Variable` falls straight to `Unknown`. Calling
    /// through it must stay pessimal unconditionally; narrowing it would
    /// require the points-to machinery §5 rules out, and reading it through
    /// the type-row join instead is a completely different (type-level, not
    /// call-graph-level) mechanism from what this test checks.
    #[test]
    fn a_call_through_a_heap_stored_fn_value_stays_pessimal() {
        let src = "VAR cb = #fn(bar)\n\
                   === function bar() ===\n~ return 1\n\
                   === function user() ===\n~ return cb()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        assert!(
            rows[&user].opaque,
            "a call through a VAR-held fn value is the heap channel — \
             local_fn_origins never sees VAR/CONST writes at all, so it \
             must stay pessimal rather than attempt to narrow"
        );
    }

    /// A `ref`-param write whose root is a *global* (not a Temp) — the same
    /// call-site mechanism `a_ref_param_rebind_through_a_call_site_stays_pessimal`
    /// exercises, but aimed at a differently-named `VAR` root (`npc`)
    /// instead of the Temp being narrowed (`f`). [`InferPass::record_fn_write`]
    /// only folds a write into `local_fn_origins` for a `Temp`/`Param`
    /// target — a `Variable` target is a documented no-op there (the heap
    /// case is §5's job, not this rung's). This pins the common case: `f`'s
    /// own single, fully traced `#fn(bar)` write is untouched by a sibling
    /// ref-write to `npc`, so `user`'s row narrows instead of spuriously
    /// falling to the pessimal floor.
    ///
    /// This does **not** pin the no-op's load-bearing case. `local_fn_origins`
    /// is keyed by `String` name, and `npc`/`f` are different names, so they
    /// can never collide in that map regardless of whether `record_fn_write`'s
    /// `Variable` arm is a no-op or is folded into `bump_local_write` —
    /// deleting the guard leaves this exact test green. A genuine collision
    /// needs a global root that resolves under the *same* name key as the
    /// traced local (the hazard `record_fn_write`'s own doc comment calls
    /// out for its `Param` arm, by the same reasoning). No such fixture is
    /// pinned here; this is a known gap in this pinning pass, not a claim
    /// that the guard is unnecessary.
    #[test]
    fn a_ref_param_write_to_an_unrelated_global_root_does_not_poison_a_traced_local() {
        let src = "VAR total = 0\nVAR npc = 5\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function poke(ref g, h) ===\n~ g = h\n\
                   === function user(cond, new_cb) ===\n~ temp f = #fn(bar)\n\
                   {cond:\n  ~ poke(npc, new_cb)\n}\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "a ref-param write to an unrelated global root must not poison \
             `f`'s own fully traced write set: {:?}",
            rows[&user]
        );
        assert!(
            rows[&user].writes.contains(&total),
            "the narrowed call through f must still join bar's own write to \
             total: {:?}",
            rows[&user]
        );
    }

    // ─── Issue #1755: channel 5's VAR case — the `#fn`-creation-site
    // `ref` binding ──────────────────────────────────────────────────────
    //
    // docs/effects-spec.md §6.1a enumerated this as the one aliasing channel
    // that was a genuine conservative-total (§3) *under*-report rather than a
    // deliberate pessimal fallback: `#fn(heal, player_hp)` binds `heal`'s
    // `ref hp` param to the cell `player_hp` at the **creation** site, a
    // grammar position distinct from a call site's `ref` argument, and
    // `infer_fn_literal` never called `record_ref_param_writes`. The write
    // was therefore recorded nowhere — not at the creation site, not in
    // `heal`'s own body (where `hp` resolves as a `Param`, never a
    // `Variable`), and not at the eventual `f(5)` call site (which carries no
    // record of which cell `heal` was created against).

    /// The under-report itself: creating a fn value that binds a `ref` param
    /// to a `VAR` must fold that cell into the *creating* body's own write
    /// set. Option (a) of #1755's ask — sound (the write genuinely happens
    /// when the value is called) though coarse (it is charged at the creation
    /// site whether or not the value is ever called). Over-reporting is the
    /// permitted direction (§3).
    #[test]
    fn a_fn_creation_site_ref_binding_records_the_bound_cell_as_a_write() {
        let src = "VAR player_hp = 10\n\
                   === function heal(ref hp, amount) ===\n~ hp = hp + amount\n\
                   === function user() ===\n~ temp f = #fn(heal, player_hp)\n\
                   ~ return f(5)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let player_hp = id_of(&index, "player_hp");
        assert!(
            rows[&user].writes.contains(&player_hp),
            "the cell bound into `heal`'s ref param at the `#fn` creation site \
             is genuinely written when the created value runs — omitting it \
             from `user`'s row is the under-report §3 forbids: {:?}",
            rows[&user]
        );
    }

    /// The same recording must happen even when the created value is never
    /// called from the creating body at all — the bound cell escapes with the
    /// value (returned here), so the creating body is the only place that can
    /// still see which cell was bound. Charging the write at the creation
    /// site is exactly what makes that possible.
    #[test]
    fn a_fn_creation_site_ref_binding_records_the_write_even_when_never_called() {
        let src = "VAR player_hp = 10\n\
                   === function heal(ref hp, amount) ===\n~ hp = hp + amount\n\
                   === function user() ===\n~ return #fn(heal, player_hp)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let player_hp = id_of(&index, "player_hp");
        assert!(
            rows[&user].writes.contains(&player_hp),
            "a created-but-uncalled `#fn` still binds the cell — the creation \
             site is the only place the binding is visible: {:?}",
            rows[&user]
        );
    }

    /// Channel 4's root-unwrapping applies at this grammar position too: an
    /// explicit `ref` projection (`ref npc.hp`, T1e) bound at a creation site
    /// writes through the **root** global's own cell, exactly as
    /// `record_ref_param_writes` already unwraps it at a call site.
    #[test]
    fn a_fn_creation_site_ref_projection_records_its_root_cell() {
        let src = "VAR npc = 0\n\
                   === function heal(ref hp, amount) ===\n~ hp = hp + amount\n\
                   === function user() ===\n~ temp f = #fn(heal, ref npc.hp)\n\
                   ~ return f(5)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let npc = id_of(&index, "npc");
        assert!(
            rows[&user].writes.contains(&npc),
            "mutating a projection writes through the root global's own cell: \
             {:?}",
            rows[&user]
        );
    }

    /// The pessimal floor must not *widen* on the way through (the PR #1731
    /// review lesson): a `#fn` creation site whose bound prefix contains no
    /// `ref` param at all is untouched by this fix — the local still narrows
    /// to its traced target rather than falling to `opaque`.
    #[test]
    fn a_fn_creation_site_without_a_ref_param_still_narrows() {
        let src = "VAR total = 0\n\
                   === function bar(n) ===\n~ total = total + n\n~ return total\n\
                   === function user() ===\n~ temp f = #fn(bar, 1)\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "a non-`ref` bound prefix must not be charged as an untraced \
             write — the local still narrows to `bar`: {:?}",
            rows[&user]
        );
        assert!(
            rows[&user].writes.contains(&total),
            "the narrowed call through f still joins bar's own write: {:?}",
            rows[&user]
        );
    }

    // ─── Fork A (docs/decision-log.md 2026-07-28, issue #1726): the
    // structural fn-value creation atom ─────────────────────────────────

    /// The atom itself: `#fn(target, …)` — bare, `bind`-wrapped, or never
    /// called at all — records `target` in `EffectAtoms::creates_fn_values`,
    /// and a body with no `#fn` literal records nothing. Harvested by the
    /// same empty-globals/empty-sigs walk every other structural atom uses,
    /// so no inferred row or signature is ever consulted to decide an edge.
    #[test]
    fn fn_value_creation_sites_are_harvested_as_a_structural_atom() {
        let src = "VAR total = 0\n\
                   === function bar(n) ===\n~ total = total + n\n~ return total\n\
                   === function baz() ===\n~ return 0\n\
                   === function creates() ===\n~ temp f = #fn(bar, 1)\n~ return call(f)\n\
                   === function binds() ===\n~ return call(bind(#fn(bar), 5))\n\
                   === function hands_out() ===\n~ return #fn(baz)\n\
                   === function plain() ===\n~ return bar(1)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let inferable = inferable_defs(&files, &index);
        let bar = id_of(&index, "bar");
        let baz = id_of(&index, "baz");

        let atoms = |name: &str| {
            def_effect_atoms(id_of(&index, name), &files, &index, &res, &inferable, None)
        };

        assert!(
            atoms("creates").creates_fn_values.contains(&bar),
            "a bare #fn literal is a creation site"
        );
        assert!(
            atoms("binds").creates_fn_values.contains(&bar),
            "bind() copies a value rather than naming a target — the nested \
             #fn literal is what gets recorded"
        );
        assert!(
            atoms("hands_out").creates_fn_values.contains(&baz),
            "a fn value that is created and returned, never called here, is \
             still a creation site"
        );
        assert!(
            atoms("plain").creates_fn_values.is_empty(),
            "a direct call creates no fn value"
        );
    }

    /// `creates_fn_values` is a subset of `direct_calls` by construction —
    /// the same walk records a `#fn` target as a call-graph edge, which is
    /// exactly how these edges reach the SCC batching and `solve_scc_effects`
    /// with no change to either. Pinned so a future edit cannot quietly break
    /// the batching invariant `effects_project`'s graph relies on.
    #[test]
    fn every_fn_value_creation_target_is_also_a_call_graph_edge() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function hands_out() ===\n~ return #fn(bar)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let inferable = inferable_defs(&files, &index);
        let atoms = def_effect_atoms(
            id_of(&index, "hands_out"),
            &files,
            &index,
            &res,
            &inferable,
            None,
        );
        assert!(
            atoms.creates_fn_values.is_subset(&atoms.direct_calls),
            "creation targets must also be call-graph edges: {:?} ⊄ {:?}",
            atoms.creates_fn_values,
            atoms.direct_calls
        );
    }

    /// An `EXTERNAL` `#fn` target is deliberately not a creation-atom member:
    /// it has no inferable body, so it is not a legal call-graph edge. The
    /// call-kind atom is still recorded (`record_call_edge`'s external arm),
    /// so nothing is silently dropped — see `record_fn_value_creation`'s doc.
    #[test]
    fn an_external_fn_value_target_is_a_call_kind_atom_not_a_creation_edge() {
        let src = "EXTERNAL play_sfx(x)\n\
                   === function hands_out() ===\n~ return #fn(play_sfx)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let inferable = inferable_defs(&files, &index);
        let atoms = def_effect_atoms(
            id_of(&index, "hands_out"),
            &files,
            &index,
            &res,
            &inferable,
            None,
        );
        assert!(
            atoms.creates_fn_values.is_empty(),
            "an EXTERNAL target has no row to follow, so it is not an edge"
        );
        assert!(
            atoms.calls.contains("play_sfx"),
            "the call-kind atom is still harvested — no silent drop"
        );
    }

    /// A def that creates a fn value and hands it out without ever calling it
    /// still carries the target's row, because §6.1 fixes the value's row at
    /// its creation site. This is what makes a downstream `opaque` collapse
    /// worth having — the effects are already attributed where the value was
    /// born.
    ///
    /// **This behavior predates #1726** and is pinned here, not introduced:
    /// `infer_fn_literal` already routed every `#fn` target through
    /// [`InferPass::record_call_edge`], so the graph edge existed before the
    /// creation atom did. `creates_fn_values` is therefore a strict subset of
    /// `direct_calls` and adds no new edge today — its value is making the
    /// creation fact *addressable* (spec §7's token table, §8 rung 1's
    /// reachability slicing) and guaranteeing the property stays true. The
    /// guard is `every_fn_value_creation_target_is_also_a_call_graph_edge`;
    /// this test pins that the atom did not disturb the row it rides on.
    #[test]
    fn creating_a_fn_value_joins_the_targets_row_even_without_a_call() {
        let src = "VAR total = 0\n\
                   === function bar() ===\n~ total = total + 1\n~ return total\n\
                   === function hands_out() ===\n~ return #fn(bar)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let hands_out = id_of(&index, "hands_out");
        let total = id_of(&index, "total");
        assert!(
            rows[&hands_out].writes.contains(&total),
            "the creation edge must pull bar's row into hands_out"
        );
        assert!(
            !rows[&hands_out].opaque,
            "creating a fn value is not itself an opaque construct"
        );
    }

    /// Transitive composition: narrowing must feed the *same* SCC effect
    /// fixpoint a direct call edge does, so a callee-of-the-callee's atoms
    /// still propagate all the way up through the narrowed edge — not just
    /// the immediately-dispatched def's own atoms.
    #[test]
    fn narrowed_call_composes_transitively_through_the_callees_own_callee() {
        let src = "VAR total = 0\n\
                   === function baz() ===\n~ total = total + 1\n~ return total\n\
                   === function bar() ===\n~ return baz()\n\
                   === function user() ===\n~ temp f = #fn(bar)\n~ return f()\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let user = id_of(&index, "user");
        let total = id_of(&index, "total");
        assert!(
            !rows[&user].opaque,
            "narrowing to bar must not itself force pessimal"
        );
        assert!(
            rows[&user].writes.contains(&total),
            "bar's own row already transitively covers baz's write to total \
             (ordinary direct-call SCC propagation) — user's narrowed edge to \
             bar must inherit that whole row, not just bar's own direct atoms"
        );
    }

    /// The pre-existing pessimal-floor regression must hold unchanged: an
    /// `Unknown`-typed callee (a param with no traceable origin at all) still
    /// gets no narrowing — `local_call_origin` never classifies a param as
    /// `Local`, so #872's write-summary rung does not apply to it and the
    /// floor holds regardless of write count.
    ///
    /// §6.1 (issue #1680) added the *other* way out — a row variable the
    /// caller instantiates — which is why the assertion is `is_pessimal()`:
    /// the definition read on its own is exactly as unbounded as it was.
    #[test]
    fn a_call_through_an_unresolvable_param_stays_pessimal() {
        let src = "=== function apply(cb) ===\n~ return cb(1)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let apply = id_of(&index, "apply");
        assert!(
            rows[&apply].is_pessimal(),
            "a call through a function value with no known origin must stay pessimal"
        );
    }

    /// Soundness regression (review finding on #872's initial landing): a
    /// `Param` carries an implicit caller-provided initial value that
    /// `local_write_counts` never sees. If a param is reassigned exactly
    /// once inside the body, its whole-body write count reaches 1 — but any
    /// call site *reachable before* that reassignment still runs against
    /// the caller's arbitrary (unknown) fn value, not the known origin the
    /// single write traces to. `local_call_origin` narrowing a `Param` the
    /// same way it narrows a write-once `Temp` would incorrectly narrow
    /// that earlier call site too, under-reporting whatever effects the
    /// caller's actual callee has that `bar` doesn't. `apply`'s row must
    /// stay opaque: `cb` is a `Param`, never eligible for `Local` narrowing
    /// regardless of how many times it's written.
    #[test]
    fn a_param_reassigned_once_called_before_the_write_stays_pessimal() {
        let src = "VAR total = 0\n\
                   === function bar(n) ===\n~ total = total + n\n~ return total\n\
                   === function apply(cb, guard) ===\n\
                   {guard:\n  ~ return cb(1)\n}\n~ cb = #fn(bar)\n~ return cb(1)\n";
        let (hir, index, res) = build(src);
        let files = [(FileId(0), &hir)];
        let rows = effects_project(&files, &index, &res, None);
        let apply = id_of(&index, "apply");
        assert!(
            rows[&apply].opaque,
            "a param reassigned exactly once inside the body must not narrow \
             calls reachable before that reassignment — the param still holds \
             the caller's arbitrary fn value there"
        );
    }

    // ─── Issue #1027: `type_ref_to_ty` and `external_check::resolve_type`
    // agree on unregistered semantic-type names ──────────────────────────

    /// The #1004/#1027 case, exercised through both real call sites for the
    /// exact same input: an `EXTERNAL` param typed via inline `@param` doc
    /// with a semantic-type name (`var_id`) the registered manifest does
    /// *not* define (the manifest defines `actor_id`, a sibling type, so
    /// the vocabulary genuinely reached the analyzer — this isn't the
    /// "no manifest at all" tolerant case). `collect_external_sigs`
    /// (consumed by strict inference) and `external_check::analyze_externals`
    /// (consumed by hover/signature help) must both call `var_id`
    /// unresolved: `Ty::Unknown` on one side, `ResolvedType { base: None,
    /// .. }` on the other — never a confidently-resolved type on either
    /// side. Both now delegate the base/registered/unregistered decision to
    /// the same `type_resolution::classify` helper, so this is a genuine
    /// agreement check, not a coincidence of two independently-written
    /// `match`es.
    #[test]
    fn collect_external_sigs_and_resolve_type_agree_on_an_unregistered_semantic_type() {
        let (_hir, index, _res, inline_docs) =
            build_with_docs("/// @param id {var_id}\nEXTERNAL get_variable(id)\n-> DONE\n");
        let manifest = brink_ir::HostManifest {
            markup: Vec::new(),
            types: vec![brink_ir::SemanticTypeDef {
                name: "actor_id".to_string(),
                base: brink_ir::BaseType::String,
                constraint: None,
                values: None,
                widget: None,
            }],
            externals: Vec::new(),
        };

        // Strict-inference side.
        let sigs = collect_external_sigs(&index, Some(&manifest), &inline_docs);
        let ext_id = index
            .by_name
            .get("get_variable")
            .and_then(|ids| ids.first())
            .copied()
            .expect("get_variable in index");
        let sig = sigs.get(&ext_id).expect("seeded signature");
        assert_eq!(
            sig.params,
            vec![Ty::Unknown],
            "var_id is not registered — strict inference must not fabricate a type"
        );

        // Hover/signature-help side — same index, same inline_docs, same
        // registered `types` vocabulary (`actor_id` only).
        let (types, registered) = crate::manifest_maps(Some(&manifest));
        let (metas, diags) = crate::external_check::analyze_externals(
            &index,
            &inline_docs,
            &types,
            &registered,
            crate::ExternalCheckSeverity::Error,
            true, // manifest registered → unknown types are checked (E040)
        );
        let meta = metas.get(&ext_id).expect("meta for get_variable");
        assert!(
            meta.params[0]
                .ty
                .as_ref()
                .is_some_and(|t| !t.is_registered()),
            "var_id must render as unregistered (base: None), not a confident type: {:?}",
            meta.params[0].ty
        );
        assert_eq!(
            diags.len(),
            1,
            "the same unregistered name also raises E040 on this path: {diags:?}"
        );
        assert_eq!(diags[0].code, brink_ir::DiagnosticCode::E040);
    }
}