cairnlang-core 0.5.0

//! The single Core checker.
//!
//! There is exactly one checker, here, and every front end goes through it
//! (`docs/design.md` Section 7). Every mutating operation gets back a
//! [`Report`] — the verification verdict (Section 6). An incomplete program
//! (one with holes) is not an error; it is a normal state.
//!
//! What is checked, and which Section 2 principle a failure maps to:
//!
//! - structural integrity — every referenced child hash is present (P4)
//! - locality — every name (binding or callee) resolves (P1)
//! - types — argument and result types honor declared signatures (P2)
//! - confidence — arguments meet each param's `min_confidence`, and a
//!   function's result is no weaker than its declared `produces` (P7)
//! - effects — a function's `requires` covers every effect it performs,
//!   effects propagating by union (P5)
//! - failures — every failure a callee declares is covered by the caller's
//!   `on_failure` (P6)
//!
//! ## Why this is incremental
//!
//! The store is content-addressed, so a [`NodeHash`] denotes one immutable
//! subtree forever. Facts that depend only on a subtree's content
//! ([`SubtreeFacts`]: holes and structural integrity) are a pure function of
//! its hash and are memoized by hash; re-checking after an edit recomputes
//! only changed hashes. That is the Section 7 incrementality claim, falling
//! out of content-addressing rather than being engineered. The typed walk
//! (name/type/confidence/effect/failure) is context-dependent and is
//! recomputed; memoizing it on `(hash, scope)` is a later refinement.

use crate::node::{MatchArm, Node, NodeHash, Produces};
use crate::store::{Result, Store};
use crate::ty::{Confidence, Effect, Type};
use serde::Serialize;
use std::cell::Cell;
use std::collections::{BTreeSet, HashMap};

/// Whether a subtree has unfilled holes.
#[derive(Clone, Copy, PartialEq, Eq, Debug, Serialize)]
pub enum Status {
    /// No holes anywhere in the subtree.
    Complete,
    /// At least one hole remains. A normal state, not an error.
    Incomplete,
}

/// Whether every callee-declared failure is covered by the caller.
#[derive(Clone, PartialEq, Eq, Debug, Serialize)]
pub enum Failures {
    Exhaustive,
    Uncovered(Vec<String>),
}

/// A broken design principle, with the offending node and a reason. The
/// `principle` is the Section 2 principle number.
#[derive(Clone, PartialEq, Eq, Debug, Serialize)]
pub struct Violation {
    pub principle: u8,
    pub node: NodeHash,
    pub detail: String,
}

/// The verification verdict for a checked root (`docs/design.md` Section 6).
#[derive(Clone, PartialEq, Eq, Debug, Serialize)]
pub struct Report {
    pub node: NodeHash,
    pub status: Status,
    pub holes: Vec<NodeHash>,
    /// Effects actually performed (union of callee `requires`).
    pub effects: BTreeSet<Effect>,
    /// Confidence at the produces site, when inferable.
    pub confidence: Option<Confidence>,
    pub failures: Failures,
    pub violations: Vec<Violation>,
}

impl Report {
    /// True when nothing invalid was found. Holes are not violations, so an
    /// `Incomplete` report can still be `ok`.
    pub fn ok(&self) -> bool {
        self.violations.is_empty()
    }
}

/// A function's checkable contract, extracted from its node.
#[derive(Clone)]
struct Signature {
    type_params: Vec<String>,
    params: Vec<crate::node::Param>,
    produces: Produces,
    requires: BTreeSet<Effect>,
    on_failure: Vec<String>,
}

/// Content-only facts about a subtree: holes it contains and referenced child
/// hashes absent from the store. A pure function of the subtree's hash.
#[derive(Clone, Default)]
struct SubtreeFacts {
    holes: Vec<NodeHash>,
    missing: Vec<NodeHash>,
}

/// What checking one function produced.
struct FnResult {
    result_confidence: Option<Confidence>,
    effects: BTreeSet<Effect>,
    uncovered_failures: Vec<String>,
}

/// An ordered name → (type, confidence) scope. Later entries shadow earlier
/// ones; an entry is `None` when its value's type could not be inferred (so
/// dependent checks are skipped rather than cascading).
type Scope = Vec<(String, Option<(Type, Confidence)>)>;

/// Record type name → its fields.
type RecordTable = HashMap<String, Vec<(String, Type)>>;
/// Variant type name → its cases (case name → payload fields).
type VariantTable = HashMap<String, Vec<(String, Vec<(String, Type)>)>>;

/// The checker. Borrows a [`Store`]; owns a per-instance memo of
/// [`SubtreeFacts`] keyed by content hash.
pub struct Checker<'a> {
    store: &'a Store,
    facts: HashMap<NodeHash, SubtreeFacts>,
    /// Populated from the root module at the start of `check`, read while
    /// walking.
    records: RecordTable,
    variants: VariantTable,
    computed: Cell<u64>,
}

impl<'a> Checker<'a> {
    pub fn new(store: &'a Store) -> Self {
        Self {
            store,
            facts: HashMap::new(),
            records: HashMap::new(),
            variants: HashMap::new(),
            computed: Cell::new(0),
        }
    }

    /// Nodes whose content-facts were computed rather than memoized. Used by
    /// tests to demonstrate incrementality.
    pub fn computed_count(&self) -> u64 {
        self.computed.get()
    }

    /// Check the subtree rooted at `root` and produce its [`Report`].
    pub fn check(&mut self, root: &NodeHash) -> Result<Report> {
        let Some(root_node) = self.store.get(root)? else {
            return Ok(Report {
                node: root.clone(),
                status: Status::Complete,
                holes: Vec::new(),
                effects: BTreeSet::new(),
                confidence: None,
                failures: Failures::Exhaustive,
                violations: vec![Violation {
                    principle: 4,
                    node: root.clone(),
                    detail: "root node is not present in the store".into(),
                }],
            });
        };

        let facts = self.subtree_facts(root)?;
        let mut violations: Vec<Violation> = facts
            .missing
            .iter()
            .map(|h| Violation {
                principle: 4,
                node: h.clone(),
                detail: "referenced child node is not present in the store".into(),
            })
            .collect();

        let sigs = self.signatures(root, &root_node)?;
        self.records = self.record_defs(&root_node)?;
        self.variants = self.variant_defs(&root_node)?;
        let mut effects = BTreeSet::new();
        let mut confidence = None;
        let mut uncovered: Vec<String> = Vec::new();

        match &root_node {
            Node::Function { .. } => {
                let fr = self.check_function(root, &root_node, &sigs, &mut violations)?;
                effects = fr.effects;
                confidence = fr.result_confidence;
                uncovered = fr.uncovered_failures;
            }
            Node::Module { functions, .. } => {
                for fh in functions {
                    if let Some(fnode) = self.store.get(fh)? {
                        let fr = self.check_function(fh, &fnode, &sigs, &mut violations)?;
                        effects.extend(fr.effects);
                        for u in fr.uncovered_failures {
                            if !uncovered.contains(&u) {
                                uncovered.push(u);
                            }
                        }
                    }
                }
            }
            _ => {
                // A bare expression root: still report unresolved names.
                let mut fl = BTreeSet::new();
                confidence = self
                    .walk_expr(root, &[], &sigs, &mut violations, &mut effects, &mut fl)?
                    .map(|(_, c)| c);
            }
        }

        Ok(Report {
            node: root.clone(),
            status: if facts.holes.is_empty() {
                Status::Complete
            } else {
                Status::Incomplete
            },
            holes: facts.holes,
            effects,
            confidence,
            failures: if uncovered.is_empty() {
                Failures::Exhaustive
            } else {
                Failures::Uncovered(uncovered)
            },
            violations,
        })
    }

    /// Content-only facts for a subtree, memoized by hash. The caller
    /// guarantees `hash` is present in the store.
    fn subtree_facts(&mut self, hash: &NodeHash) -> Result<SubtreeFacts> {
        if let Some(cached) = self.facts.get(hash) {
            return Ok(cached.clone());
        }
        self.computed.set(self.computed.get() + 1);

        let node = self
            .store
            .get(hash)?
            .expect("subtree_facts caller guarantees presence");

        let mut facts = SubtreeFacts::default();
        if let Node::Hole { .. } = node {
            facts.holes.push(hash.clone());
        }
        for child in child_hashes(&node) {
            match self.store.get(child)? {
                None => facts.missing.push(child.clone()),
                Some(_) => {
                    let sub = self.subtree_facts(child)?;
                    facts.holes.extend(sub.holes);
                    facts.missing.extend(sub.missing);
                }
            }
        }

        self.facts.insert(hash.clone(), facts.clone());
        Ok(facts)
    }

    /// Build the name → [`Signature`] table the root resolves calls against:
    /// every function in a module, or a lone function (so self-calls resolve).
    fn signatures(&self, _root: &NodeHash, root_node: &Node) -> Result<HashMap<String, Signature>> {
        let mut sigs = HashMap::new();
        let mut add = |node: &Node| {
            if let Node::Function {
                name,
                type_params,
                params,
                produces,
                requires,
                on_failure,
                ..
            } = node
            {
                sigs.insert(
                    name.clone(),
                    Signature {
                        type_params: type_params.clone(),
                        params: params.clone(),
                        produces: produces.clone(),
                        requires: requires.clone(),
                        on_failure: on_failure.clone(),
                    },
                );
            }
        };
        match root_node {
            Node::Function { .. } => add(root_node),
            Node::Module { functions, .. } => {
                for fh in functions {
                    if let Some(fnode) = self.store.get(fh)? {
                        add(&fnode);
                    }
                }
            }
            _ => {}
        }
        Ok(sigs)
    }

    /// Build the record-type table the root resolves type names against:
    /// every `RecordDef` in a module, or a lone `RecordDef`.
    fn record_defs(&self, root_node: &Node) -> Result<RecordTable> {
        let mut recs = HashMap::new();
        let mut add = |node: &Node| {
            if let Node::RecordDef { name, fields } = node {
                recs.insert(name.clone(), fields.clone());
            }
        };
        match root_node {
            Node::RecordDef { .. } => add(root_node),
            Node::Module { types, .. } => {
                for th in types {
                    if let Some(tnode) = self.store.get(th)? {
                        add(&tnode);
                    }
                }
            }
            _ => {}
        }
        Ok(recs)
    }

    /// Build the variant-type table: every `VariantDef` in a module, or a
    /// lone `VariantDef`.
    fn variant_defs(&self, root_node: &Node) -> Result<VariantTable> {
        let mut vars = HashMap::new();
        let mut add = |node: &Node| {
            if let Node::VariantDef { name, cases } = node {
                vars.insert(name.clone(), cases.clone());
            }
        };
        match root_node {
            Node::VariantDef { .. } => add(root_node),
            Node::Module { types, .. } => {
                for th in types {
                    if let Some(tnode) = self.store.get(th)? {
                        add(&tnode);
                    }
                }
            }
            _ => {}
        }
        Ok(vars)
    }

    /// Check one function: scope, types, confidence, effects, failures.
    fn check_function(
        &self,
        fn_hash: &NodeHash,
        fn_node: &Node,
        sigs: &HashMap<String, Signature>,
        out: &mut Vec<Violation>,
    ) -> Result<FnResult> {
        let Node::Function {
            params,
            produces,
            requires,
            on_failure,
            body,
            result,
            ..
        } = fn_node
        else {
            return Ok(FnResult {
                result_confidence: None,
                effects: BTreeSet::new(),
                uncovered_failures: Vec::new(),
            });
        };

        let mut scope: Scope = params
            .iter()
            .map(|p| (p.name.clone(), Some((p.ty.clone(), p.min_confidence))))
            .collect();
        let mut effects = BTreeSet::new();
        let mut failures = BTreeSet::new();

        for step_hash in body {
            let Some(step) = self.store.get(step_hash)? else {
                continue;
            };
            if let Node::Step { binding, value } = &step {
                let v = self
                    .walk_expr(value, &scope, sigs, out, &mut effects, &mut failures)?;
                scope.push((binding.clone(), v));
            }
        }

        let result_confidence = match self
            .walk_expr(result, &scope, sigs, out, &mut effects, &mut failures)?
        {
            Some((rt, rc)) => {
                if !compatible(&rt, &produces.ty) {
                    out.push(Violation {
                        principle: 2,
                        node: result.clone(),
                        detail: format!(
                            "result is {:?} but `produces` declares {:?}",
                            rt, produces.ty
                        ),
                    });
                }
                if rc < produces.confidence {
                    out.push(Violation {
                        principle: 7,
                        node: result.clone(),
                        detail: format!(
                            "result confidence {:?} is weaker than declared {:?}",
                            rc, produces.confidence
                        ),
                    });
                }
                Some(rc)
            }
            None => None,
        };

        // Effects propagate by union; `requires` must cover them (P5).
        for e in &effects {
            if !requires.contains(e) {
                out.push(Violation {
                    principle: 5,
                    node: fn_hash.clone(),
                    detail: format!("performs effect {e:?} not declared in `requires`"),
                });
            }
        }

        // Every callee-declared failure must be in this function's
        // `on_failure` (P6).
        let mut uncovered_failures = Vec::new();
        for f in &failures {
            if !on_failure.contains(f) {
                uncovered_failures.push(f.clone());
                out.push(Violation {
                    principle: 6,
                    node: fn_hash.clone(),
                    detail: format!("failure `{f}` is not covered by `on_failure`"),
                });
            }
        }

        Ok(FnResult {
            result_confidence,
            effects,
            uncovered_failures,
        })
    }

    /// Infer an expression's `(type, confidence)`, reporting name, type, and
    /// confidence violations and accumulating effects and failures. `None`
    /// means "not inferable" (an unresolved name or a hole) — dependent checks
    /// are then skipped rather than cascading.
    #[allow(clippy::only_used_in_recursion)]
    fn walk_expr(
        &self,
        hash: &NodeHash,
        scope: &[(String, Option<(Type, Confidence)>)],
        sigs: &HashMap<String, Signature>,
        out: &mut Vec<Violation>,
        effects: &mut BTreeSet<Effect>,
        failures: &mut BTreeSet<String>,
    ) -> Result<Option<(Type, Confidence)>> {
        let Some(node) = self.store.get(hash)? else {
            // Absence is a structural violation, already reported via facts.
            return Ok(None);
        };
        Ok(match node {
            Node::Lit(_) => Some((Type::Number, Confidence::Structural)),
            Node::FloatLit(_) => Some((Type::Float, Confidence::Structural)),
            Node::FloatOp { op, lhs, rhs } => {
                let l = self.walk_expr(&lhs, scope, sigs, out, effects, failures)?;
                let r = self.walk_expr(&rhs, scope, sigs, out, effects, failures)?;
                for (h, t) in [(&lhs, &l), (&rhs, &r)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::Float && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: h.clone(),
                                detail: format!(
                                    "float operand is {ty:?}, expected Float"
                                ),
                            });
                        }
                    }
                }
                let conf = match (&l, &r) {
                    (Some((_, a)), Some((_, b))) => (*a).min(*b),
                    _ => Confidence::Structural,
                };
                use crate::node::BinOp as B;
                if op.is_logical() || op == B::Mod || op == B::Neq {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: format!(
                            "operator `{}` is not defined on Float",
                            op.symbol()
                        ),
                    });
                    None
                } else if op.is_comparison() {
                    Some((Type::Bool, conf))
                } else {
                    Some((Type::Float, conf))
                }
            }
            Node::IntToFloat(a) => {
                let t = self.walk_expr(&a, scope, sigs, out, effects, failures)?;
                if let Some((ty, c)) = t {
                    if ty != Type::Number && ty != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: a.clone(),
                            detail: format!("to_float expects Number, got {ty:?}"),
                        });
                    }
                    Some((Type::Float, c))
                } else {
                    None
                }
            }
            Node::FloatToInt(a) => {
                let t = self.walk_expr(&a, scope, sigs, out, effects, failures)?;
                if let Some((ty, c)) = t {
                    if ty != Type::Float && ty != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: a.clone(),
                            detail: format!("to_int expects Float, got {ty:?}"),
                        });
                    }
                    Some((Type::Number, c))
                } else {
                    None
                }
            }
            Node::DecimalLit(_) => {
                Some((Type::Decimal, Confidence::Structural))
            }
            Node::DecimalOp { op, lhs, rhs } => {
                let l = self.walk_expr(&lhs, scope, sigs, out, effects, failures)?;
                let r = self.walk_expr(&rhs, scope, sigs, out, effects, failures)?;
                for (h, t) in [(&lhs, &l), (&rhs, &r)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::Decimal && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: h.clone(),
                                detail: format!(
                                    "decimal operand is {ty:?}, expected Decimal"
                                ),
                            });
                        }
                    }
                }
                let conf = match (&l, &r) {
                    (Some((_, a)), Some((_, b))) => (*a).min(*b),
                    _ => Confidence::Structural,
                };
                use crate::node::BinOp as B;
                if op.is_logical() || op == B::Mod {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: format!(
                            "operator `{}` is not defined on Decimal",
                            op.symbol()
                        ),
                    });
                    None
                } else if op.is_comparison() {
                    Some((Type::Bool, conf))
                } else {
                    Some((Type::Decimal, conf))
                }
            }
            Node::IntToDecimal(a) => {
                let t = self.walk_expr(&a, scope, sigs, out, effects, failures)?;
                if let Some((ty, c)) = t {
                    if ty != Type::Number && ty != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: a.clone(),
                            detail: format!(
                                "to_decimal expects Number, got {ty:?}"
                            ),
                        });
                    }
                    Some((Type::Decimal, c))
                } else {
                    None
                }
            }
            Node::DecimalToInt(a) | Node::DecimalRaw(a) => {
                let t = self.walk_expr(&a, scope, sigs, out, effects, failures)?;
                if let Some((ty, c)) = t {
                    if ty != Type::Decimal && ty != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: a.clone(),
                            detail: format!(
                                "expects Decimal, got {ty:?}"
                            ),
                        });
                    }
                    Some((Type::Number, c))
                } else {
                    None
                }
            }
            Node::Bool(_) => Some((Type::Bool, Confidence::Structural)),
            Node::Not(arg) => {
                let a = self.walk_expr(&arg, scope, sigs, out, effects, failures)?;
                if let Some((at, ac)) = a {
                    if at != Type::Bool && at != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: arg.clone(),
                            detail: format!("`!` operand is {at:?}, expected Bool"),
                        });
                    }
                    Some((Type::Bool, ac))
                } else {
                    None
                }
            }
            Node::Str(_) => Some((Type::String, Confidence::Structural)),
            Node::Now => {
                // Performs the Time effect (the existing P5 coverage check
                // then requires the enclosing function to declare it) and
                // yields an external-confidence Number.
                effects.insert(Effect::Time);
                Some((Type::Number, Confidence::External))
            }
            Node::List(elems) => {
                if elems.is_empty() {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: "empty list literal needs a type annotation (v0.3)"
                            .into(),
                    });
                    return Ok(None);
                }
                let mut elem_ty: Option<Type> = None;
                let mut conf = Confidence::Persisted;
                for e in &elems {
                    if let Some((t, c)) =
                        self.walk_expr(e, scope, sigs, out, effects, failures)?
                    {
                        match &elem_ty {
                            None => elem_ty = Some(t),
                            Some(et) => {
                                if !compatible(et, &t) {
                                    out.push(Violation {
                                        principle: 2,
                                        node: e.clone(),
                                        detail: format!(
                                            "list element is {t:?}, expected {et:?}"
                                        ),
                                    });
                                }
                            }
                        }
                        conf = conf.min(c);
                    }
                }
                elem_ty.map(|t| (Type::List(Box::new(t)), conf))
            }
            Node::ListEmpty { elem } => {
                Some((Type::List(Box::new(elem)), Confidence::Structural))
            }
            Node::ListCons { head, tail } => {
                let ht = self.walk_expr(&head, scope, sigs, out, effects, failures)?;
                let tt = self.walk_expr(&tail, scope, sigs, out, effects, failures)?;
                match tt {
                    Some((Type::List(et), tc)) => {
                        if let Some((h, _)) = &ht {
                            if !compatible(&et, h) {
                                out.push(Violation {
                                    principle: 2,
                                    node: head.clone(),
                                    detail: format!(
                                        "cons head is {h:?} but the list is List<{et:?}>"
                                    ),
                                });
                            }
                        }
                        let hc =
                            ht.map(|(_, c)| c).unwrap_or(Confidence::Persisted);
                        Some((Type::List(et), hc.min(tc)))
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: tail.clone(),
                            detail: format!(
                                "cons tail must be a List, got {other:?}"
                            ),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::OptionSome(v) => self
                .walk_expr(&v, scope, sigs, out, effects, failures)?
                .map(|(t, c)| (Type::Option(Box::new(t)), c)),
            Node::OptionNone { elem } => {
                Some((Type::Option(Box::new(elem)), Confidence::Structural))
            }
            Node::OptionElse { opt, default } => {
                let ot = self.walk_expr(&opt, scope, sigs, out, effects, failures)?;
                let dt =
                    self.walk_expr(&default, scope, sigs, out, effects, failures)?;
                match ot {
                    Some((Type::Option(inner), oc)) => {
                        if let Some((d, _)) = &dt {
                            if !compatible(&inner, d) {
                                out.push(Violation {
                                    principle: 2,
                                    node: default.clone(),
                                    detail: format!(
                                        "option default is {d:?} but the Option holds {inner:?}"
                                    ),
                                });
                            }
                        }
                        let dc =
                            dt.map(|(_, c)| c).unwrap_or(Confidence::Persisted);
                        Some((*inner, oc.min(dc)))
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: opt.clone(),
                            detail: format!(
                                "option_else expects an Option, got {other:?}"
                            ),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::OptionMatch {
                opt,
                some_bind,
                some_body,
                none_body,
            } => {
                let ot = self.walk_expr(&opt, scope, sigs, out, effects, failures)?;
                let (inner, oc) = match ot {
                    Some((Type::Option(inner), oc)) => (*inner, oc),
                    Some((Type::Never, oc)) => (Type::Never, oc),
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: opt.clone(),
                            detail: format!(
                                "OptionMatch scrutinee is {other:?}, expected Option"
                            ),
                        });
                        return Ok(None);
                    }
                    None => return Ok(None),
                };
                let mut s2 = scope.to_vec();
                s2.push((some_bind.clone(), Some((inner, oc))));
                let st = self.walk_expr(
                    &some_body, &s2, sigs, out, effects, failures,
                )?;
                let nt = self.walk_expr(
                    &none_body, scope, sigs, out, effects, failures,
                )?;
                match (st, nt) {
                    (Some((s, sc)), Some((n, nc))) => {
                        if !compatible(&s, &n) {
                            out.push(Violation {
                                principle: 2,
                                node: hash.clone(),
                                detail: format!(
                                    "OptionMatch arms differ: {s:?} vs {n:?}"
                                ),
                            });
                        }
                        let ty = if s == Type::Never { n } else { s };
                        Some((ty, oc.min(sc).min(nc)))
                    }
                    (Some(v), None) | (None, Some(v)) => Some(v),
                    (None, None) => None,
                }
            }
            Node::ListTryGet { list, index } => {
                let lt = self.walk_expr(&list, scope, sigs, out, effects, failures)?;
                let it = self.walk_expr(&index, scope, sigs, out, effects, failures)?;
                if let Some((t, _)) = &it {
                    if *t != Type::Number && *t != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: index.clone(),
                            detail: format!("list index is {t:?}, expected Number"),
                        });
                    }
                }
                match lt {
                    Some((Type::List(elem), lc)) => {
                        let ic =
                            it.map(|(_, c)| c).unwrap_or(Confidence::Persisted);
                        Some((Type::Option(elem), lc.min(ic)))
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: list.clone(),
                            detail: format!(
                                "list_try_get on a non-List type {other:?}"
                            ),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::ListLen(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((Type::List(_), c)) => Some((Type::Number, c)),
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: arg.clone(),
                            detail: format!("list_len expects a List, got {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::ListGet { list, index } => {
                let lt = self.walk_expr(&list, scope, sigs, out, effects, failures)?;
                let it = self.walk_expr(&index, scope, sigs, out, effects, failures)?;
                if let Some((t, _)) = &it {
                    if *t != Type::Number && *t != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: index.clone(),
                            detail: format!("list index is {t:?}, expected Number"),
                        });
                    }
                }
                match lt {
                    Some((Type::List(elem), lc)) => {
                        let ic = it.map(|(_, c)| c).unwrap_or(Confidence::Persisted);
                        Some((*elem, lc.min(ic)))
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: list.clone(),
                            detail: format!("list_get on a non-List type {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::Map(pairs) => {
                if pairs.is_empty() {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: "empty map literal needs a type annotation (v0.3)"
                            .into(),
                    });
                    return Ok(None);
                }
                let mut kt: Option<Type> = None;
                let mut vt: Option<Type> = None;
                let mut conf = Confidence::Persisted;
                for (k, v) in &pairs {
                    if let Some((t, c)) =
                        self.walk_expr(k, scope, sigs, out, effects, failures)?
                    {
                        match &kt {
                            None => kt = Some(t),
                            Some(e) => {
                                if !compatible(e, &t) {
                                    out.push(Violation {
                                        principle: 2,
                                        node: k.clone(),
                                        detail: format!(
                                            "map key is {t:?}, expected {e:?}"
                                        ),
                                    });
                                }
                            }
                        }
                        conf = conf.min(c);
                    }
                    if let Some((t, c)) =
                        self.walk_expr(v, scope, sigs, out, effects, failures)?
                    {
                        match &vt {
                            None => vt = Some(t),
                            Some(e) => {
                                if !compatible(e, &t) {
                                    out.push(Violation {
                                        principle: 2,
                                        node: v.clone(),
                                        detail: format!(
                                            "map value is {t:?}, expected {e:?}"
                                        ),
                                    });
                                }
                            }
                        }
                        conf = conf.min(c);
                    }
                }
                match (kt, vt) {
                    (Some(k), Some(v)) => {
                        Some((Type::Map(Box::new(k), Box::new(v)), conf))
                    }
                    _ => None,
                }
            }
            Node::MapGet { map, key } => {
                let mt = self.walk_expr(&map, scope, sigs, out, effects, failures)?;
                let kt = self.walk_expr(&key, scope, sigs, out, effects, failures)?;
                match mt {
                    Some((Type::Map(k, v), mc)) => {
                        if let Some((t, _)) = &kt {
                            if !compatible(&k, t) {
                                out.push(Violation {
                                    principle: 2,
                                    node: key.clone(),
                                    detail: format!(
                                        "map key is {t:?}, expected {k:?}"
                                    ),
                                });
                            }
                        }
                        let kc = kt.map(|(_, c)| c).unwrap_or(Confidence::Persisted);
                        Some((*v, mc.min(kc)))
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: map.clone(),
                            detail: format!("map_get on a non-Map type {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::MapTryGet { map, key } => {
                let mt = self.walk_expr(&map, scope, sigs, out, effects, failures)?;
                let kt = self.walk_expr(&key, scope, sigs, out, effects, failures)?;
                match mt {
                    Some((Type::Map(k, v), mc)) => {
                        if let Some((t, _)) = &kt {
                            if !compatible(&k, t) {
                                out.push(Violation {
                                    principle: 2,
                                    node: key.clone(),
                                    detail: format!(
                                        "map key is {t:?}, expected {k:?}"
                                    ),
                                });
                            }
                        }
                        let kc = kt.map(|(_, c)| c).unwrap_or(Confidence::Persisted);
                        Some((Type::Option(v), mc.min(kc)))
                    }
                    Some((Type::Never, c)) => Some((Type::Never, c)),
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: map.clone(),
                            detail: format!("map_try_get on a non-Map type {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::MapLen(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((Type::Map(_, _), c)) => Some((Type::Number, c)),
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: arg.clone(),
                            detail: format!("map_len expects a Map, got {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::Log(arg) => {
                // Performs the Log effect; passes the value through
                // unchanged (same type and confidence).
                effects.insert(Effect::Log);
                self.walk_expr(&arg, scope, sigs, out, effects, failures)?
            }
            Node::Publish(arg) => {
                // Performs the Live effect. `topic` must be a String;
                // yields Number (0). The checker forces `requires Live`
                // on any function that can publish — liveness visible.
                effects.insert(Effect::Live);
                let t =
                    self.walk_expr(&arg, scope, sigs, out, effects, failures)?;
                if let Some((ty, _)) = t {
                    if ty != Type::String && ty != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: arg.clone(),
                            detail: format!(
                                "publish topic is {ty:?}, expected String"
                            ),
                        });
                    }
                }
                Some((Type::Number, Confidence::Structural))
            }
            Node::SetHeader { name, value } => {
                // Performs the Resp effect. `name` and `value` must be
                // String; yields Number (0) so it sequences like
                // `publish`. The checker forces `requires Resp` on any
                // function that can set a header — visible, not hidden.
                effects.insert(Effect::Resp);
                for (label, arg) in
                    [("name", &name), ("value", &value)]
                {
                    let t = self.walk_expr(
                        arg, scope, sigs, out, effects, failures,
                    )?;
                    if let Some((ty, _)) = t {
                        if ty != Type::String && ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: (*arg).clone(),
                                detail: format!(
                                    "set_header {label} is {ty:?}, \
                                     expected String"
                                ),
                            });
                        }
                    }
                }
                Some((Type::Number, Confidence::Structural))
            }
            Node::Rand => {
                effects.insert(Effect::Rand);
                Some((Type::Number, Confidence::External))
            }
            Node::MutNew(v) => {
                effects.insert(Effect::Mut);
                self.walk_expr(&v, scope, sigs, out, effects, failures)?
                    .map(|(t, c)| (Type::Cell(Box::new(t)), c))
            }
            Node::MutGet(cell) => {
                match self.walk_expr(&cell, scope, sigs, out, effects, failures)? {
                    Some((Type::Cell(t), c)) => Some((*t, c)),
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: cell.clone(),
                            detail: format!("cell_get on a non-Cell type {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::MutSet { cell, value } => {
                effects.insert(Effect::Mut);
                let ct = self.walk_expr(&cell, scope, sigs, out, effects, failures)?;
                let vt =
                    self.walk_expr(&value, scope, sigs, out, effects, failures)?;
                if let (Some((Type::Cell(et), _)), Some((vty, _))) = (&ct, &vt) {
                    if !compatible(et, vty) {
                        out.push(Violation {
                            principle: 2,
                            node: value.clone(),
                            detail: format!(
                                "cell holds {et:?} but assigned {vty:?}"
                            ),
                        });
                    }
                } else if let Some((other, _)) = &ct {
                    if !matches!(other, Type::Cell(_)) {
                        out.push(Violation {
                            principle: 2,
                            node: cell.clone(),
                            detail: format!("cell_set on a non-Cell type {other:?}"),
                        });
                    }
                }
                vt // pass-through
            }
            Node::DiskWrite { path, content } => {
                effects.insert(Effect::Disk);
                let p = self.walk_expr(&path, scope, sigs, out, effects, failures)?;
                let cn =
                    self.walk_expr(&content, scope, sigs, out, effects, failures)?;
                for (n, t) in [(&path, &p), (&content, &cn)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::String && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: n.clone(),
                                detail: format!("disk_write expects String, got {ty:?}"),
                            });
                        }
                    }
                }
                Some((Type::Number, Confidence::External))
            }
            Node::DiskRead(path) => {
                effects.insert(Effect::Disk);
                if let Some((t, _)) =
                    self.walk_expr(&path, scope, sigs, out, effects, failures)?
                {
                    if t != Type::String && t != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: path.clone(),
                            detail: format!("disk_read expects String, got {t:?}"),
                        });
                    }
                }
                // Returns the file's contents (host→wasm allocation), at
                // external confidence (it comes from outside the program).
                Some((Type::String, Confidence::External))
            }
            Node::NetGet(url) => {
                effects.insert(Effect::Net);
                if let Some((t, _)) =
                    self.walk_expr(&url, scope, sigs, out, effects, failures)?
                {
                    if t != Type::String && t != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: url.clone(),
                            detail: format!("net_get expects String, got {t:?}"),
                        });
                    }
                }
                Some((Type::Number, Confidence::External))
            }
            Node::DbQuery { sql, params } => {
                effects.insert(Effect::Db);
                if let Some((t, _)) =
                    self.walk_expr(&sql, scope, sigs, out, effects, failures)?
                {
                    if t != Type::String && t != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: sql.clone(),
                            detail: format!("db_query expects String, got {t:?}"),
                        });
                    }
                }
                if let Some((t, _)) =
                    self.walk_expr(&params, scope, sigs, out, effects, failures)?
                {
                    let ok = matches!(&t, Type::List(e) if **e == Type::String)
                        || t == Type::Never;
                    if !ok {
                        out.push(Violation {
                            principle: 2,
                            node: params.clone(),
                            detail: format!(
                                "db_query params must be List<String>, got {t:?}"
                            ),
                        });
                    }
                }
                // Reading back from the system of record yields a `String`
                // result at `persisted` confidence — the decided definition.
                Some((Type::String, Confidence::Persisted))
            }
            Node::StrConcat(a, b) => {
                let at = self.walk_expr(&a, scope, sigs, out, effects, failures)?;
                let bt = self.walk_expr(&b, scope, sigs, out, effects, failures)?;
                for (n, t) in [(&a, &at), (&b, &bt)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::String && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: n.clone(),
                                detail: format!("str_concat expects String, got {ty:?}"),
                            });
                        }
                    }
                }
                let c = at
                    .map(|(_, c)| c)
                    .unwrap_or(Confidence::Persisted)
                    .min(bt.map(|(_, c)| c).unwrap_or(Confidence::Persisted));
                Some((Type::String, c))
            }
            Node::StrSlice { s, start, len } => {
                let st = self.walk_expr(&s, scope, sigs, out, effects, failures)?;
                let stt =
                    self.walk_expr(&start, scope, sigs, out, effects, failures)?;
                let lnt = self.walk_expr(&len, scope, sigs, out, effects, failures)?;
                if let Some((t, _)) = &st {
                    if *t != Type::String && *t != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: s.clone(),
                            detail: format!("str_slice expects String, got {t:?}"),
                        });
                    }
                }
                for (n, t) in [(&start, &stt), (&len, &lnt)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::Number && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: n.clone(),
                                detail: format!("str_slice index is {ty:?}, expected Number"),
                            });
                        }
                    }
                }
                let c = [st, stt, lnt]
                    .into_iter()
                    .flatten()
                    .map(|(_, c)| c)
                    .min()
                    .unwrap_or(Confidence::Structural);
                Some((Type::String, c))
            }
            Node::StrEq(a, b)
            | Node::StrContains { haystack: a, needle: b }
            | Node::StrStartsWith { s: a, prefix: b } => {
                let at = self.walk_expr(&a, scope, sigs, out, effects, failures)?;
                let bt = self.walk_expr(&b, scope, sigs, out, effects, failures)?;
                for (n, t) in [(&a, &at), (&b, &bt)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::String && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: n.clone(),
                                detail: format!("string op expects String, got {ty:?}"),
                            });
                        }
                    }
                }
                let c = at
                    .map(|(_, c)| c)
                    .unwrap_or(Confidence::Persisted)
                    .min(bt.map(|(_, c)| c).unwrap_or(Confidence::Persisted));
                Some((Type::Bool, c))
            }
            Node::StrIndexOf { haystack, needle } => {
                let ht =
                    self.walk_expr(&haystack, scope, sigs, out, effects, failures)?;
                let nt =
                    self.walk_expr(&needle, scope, sigs, out, effects, failures)?;
                for (node, t) in [(&haystack, &ht), (&needle, &nt)] {
                    if let Some((ty, _)) = t {
                        if *ty != Type::String && *ty != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: node.clone(),
                                detail: format!(
                                    "string op expects String, got {ty:?}"
                                ),
                            });
                        }
                    }
                }
                let c = ht
                    .map(|(_, c)| c)
                    .unwrap_or(Confidence::Persisted)
                    .min(nt.map(|(_, c)| c).unwrap_or(Confidence::Persisted));
                Some((Type::Number, c))
            }
            Node::StrLen(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((t, c)) => {
                        if t != Type::String && t != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!("str_len expects String, got {t:?}"),
                            });
                        }
                        Some((Type::Number, c))
                    }
                    None => None,
                }
            }
            Node::StrLower(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((t, c)) => {
                        if t != Type::String && t != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "str_lower expects String, got {t:?}"
                                ),
                            });
                        }
                        Some((Type::String, c))
                    }
                    None => None,
                }
            }
            Node::StrFromCode(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((t, c)) => {
                        if t != Type::Number && t != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "str_from_code expects Number, got {t:?}"
                                ),
                            });
                        }
                        Some((Type::String, c))
                    }
                    None => None,
                }
            }
            Node::NumberToStr(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((t, c)) => {
                        if t != Type::Number && t != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "number_to_str expects Number, got {t:?}"
                                ),
                            });
                        }
                        Some((Type::String, c))
                    }
                    None => None,
                }
            }
            Node::StrToNumber(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((t, c)) => {
                        if t != Type::String && t != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "str_to_number expects String, got {t:?}"
                                ),
                            });
                        }
                        Some((Type::Number, c))
                    }
                    None => None,
                }
            }
            Node::StrToNumberOpt(arg) => {
                match self.walk_expr(&arg, scope, sigs, out, effects, failures)? {
                    Some((t, c)) => {
                        if t != Type::String && t != Type::Never {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "str_to_number_opt expects String, got {t:?}"
                                ),
                            });
                        }
                        Some((Type::Option(Box::new(Type::Number)), c))
                    }
                    None => None,
                }
            }
            Node::Hole { .. } => None,
            Node::Ref(name) => {
                match scope.iter().rev().find(|(n, _)| n == &name) {
                    Some((_, v)) => v.clone(),
                    None => {
                        out.push(Violation {
                            principle: 1,
                            node: hash.clone(),
                            detail: format!("unresolved reference: `{name}`"),
                        });
                        None
                    }
                }
            }
            Node::Step { value, .. } => {
                self.walk_expr(&value, scope, sigs, out, effects, failures)?
            }
            Node::Fail(f) => {
                // Diverges: contributes the variant to the propagated failure
                // set (the existing P6 coverage check enforces `on_failure`),
                // has type Never, and carries top confidence so it never
                // drags a weakest-input minimum.
                failures.insert(f);
                Some((Type::Never, Confidence::Persisted))
            }
            Node::Handle { body, handlers } => {
                // Body failures are scoped here: handled variants are caught
                // and do not propagate; everything else does.
                let mut body_f = BTreeSet::new();
                let b = self.walk_expr(&body, scope, sigs, out, effects, &mut body_f)?;
                for f in &body_f {
                    if !handlers.iter().any(|(v, _)| v == f) {
                        failures.insert(f.clone());
                    }
                }
                match b {
                    None => None,
                    Some((bt, bc)) => {
                        let mut conf = bc;
                        for (_, recover) in &handlers {
                            if let Some((rt, rc)) = self
                                .walk_expr(recover, scope, sigs, out, effects, failures)?
                            {
                                if !compatible(&rt, &bt) {
                                    out.push(Violation {
                                        principle: 2,
                                        node: recover.clone(),
                                        detail: format!(
                                            "handler recovers as {rt:?} but the value is {bt:?}"
                                        ),
                                    });
                                }
                                conf = conf.min(rc);
                            }
                        }
                        Some((bt, conf))
                    }
                }
            }
            Node::If {
                cond,
                then_branch,
                else_branch,
            } => {
                let c = self.walk_expr(&cond, scope, sigs, out, effects, failures)?;
                let t = self.walk_expr(&then_branch, scope, sigs, out, effects, failures)?;
                let e = self.walk_expr(&else_branch, scope, sigs, out, effects, failures)?;
                if let Some((ct, _)) = &c {
                    if *ct != Type::Bool && *ct != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: cond.clone(),
                            detail: format!("condition is {ct:?}, expected Bool"),
                        });
                    }
                }
                match (t, e) {
                    (Some((tt, tc)), Some((et, ec))) => {
                        if !compatible(&tt, &et) {
                            out.push(Violation {
                                principle: 2,
                                node: hash.clone(),
                                detail: format!(
                                    "branch types differ: {tt:?} vs {et:?}"
                                ),
                            });
                        }
                        // A `fail` branch is Never; the if's type is the other
                        // branch's. Weakest input over condition and branches.
                        let rty = if tt == Type::Never { et } else { tt };
                        let mut conf = tc.min(ec);
                        if let Some((_, cc)) = c {
                            conf = conf.min(cc);
                        }
                        Some((rty, conf))
                    }
                    _ => None,
                }
            }
            Node::BinOp { op, lhs, rhs } => {
                let l = self.walk_expr(&lhs, scope, sigs, out, effects, failures)?;
                let r = self.walk_expr(&rhs, scope, sigs, out, effects, failures)?;
                match (l, r) {
                    (Some((lt, lc)), Some((rt, rc))) => {
                        // Weakest-input propagation (the decided rule, now with
                        // a real site): a derived value's confidence is the
                        // minimum of its inputs'.
                        let conf = lc.min(rc);
                        if op.is_logical() {
                            for (operand, ty) in [(&lhs, &lt), (&rhs, &rt)] {
                                if *ty != Type::Bool && *ty != Type::Never {
                                    out.push(Violation {
                                        principle: 2,
                                        node: operand.clone(),
                                        detail: format!(
                                            "logical operand is {ty:?}, expected Bool"
                                        ),
                                    });
                                }
                            }
                            Some((Type::Bool, conf))
                        } else if op.is_comparison() {
                            if !compatible(&lt, &rt) {
                                out.push(Violation {
                                    principle: 2,
                                    node: hash.clone(),
                                    detail: format!(
                                        "comparison operands differ: {lt:?} vs {rt:?}"
                                    ),
                                });
                            }
                            Some((Type::Bool, conf))
                        } else {
                            if lt != Type::Number && lt != Type::Never {
                                out.push(Violation {
                                    principle: 2,
                                    node: lhs.clone(),
                                    detail: format!(
                                        "arithmetic operand is {lt:?}, expected Number"
                                    ),
                                });
                            }
                            if rt != Type::Number && rt != Type::Never {
                                out.push(Violation {
                                    principle: 2,
                                    node: rhs.clone(),
                                    detail: format!(
                                        "arithmetic operand is {rt:?}, expected Number"
                                    ),
                                });
                            }
                            Some((Type::Number, conf))
                        }
                    }
                    _ => None,
                }
            }
            Node::Call { func, args } => {
                let Some(sig) = sigs.get(&func) else {
                    out.push(Violation {
                        principle: 1,
                        node: hash.clone(),
                        detail: format!("unresolved function: `{func}`"),
                    });
                    for arg in &args {
                        self.walk_expr(arg, scope, sigs, out, effects, failures)?;
                    }
                    return Ok(None);
                };
                if args.len() != sig.params.len() {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: format!(
                            "`{func}` takes {} argument(s), {} given",
                            sig.params.len(),
                            args.len()
                        ),
                    });
                }
                // Unify each parameter type (which may mention a type
                // variable) against the actual argument type, building a
                // substitution. For a monomorphic function this is just
                // structural equality.
                let mut subst: HashMap<String, Type> = HashMap::new();
                for (i, arg) in args.iter().enumerate() {
                    let inferred =
                        self.walk_expr(arg, scope, sigs, out, effects, failures)?;
                    if let (Some((at, ac)), Some(p)) = (inferred, sig.params.get(i)) {
                        if !unify(&p.ty, &at, &mut subst) {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "argument `{}` is {:?} but `{func}` expects {:?}",
                                    p.name, at, p.ty
                                ),
                            });
                        }
                        if ac < p.min_confidence {
                            out.push(Violation {
                                principle: 7,
                                node: arg.clone(),
                                detail: format!(
                                    "argument `{}` is {:?} but `{func}` requires at least {:?}",
                                    p.name, ac, p.min_confidence
                                ),
                            });
                        }
                    }
                }
                effects.extend(sig.requires.iter().copied());
                failures.extend(sig.on_failure.iter().cloned());
                let result_ty = substitute(&sig.produces.ty, &subst);
                // A type parameter occurring in the result must also occur
                // in some parameter, else no argument can pin it (e.g.
                // `make<T>() -> T`). A still-`Var` result *after*
                // unification is fine — it may be bound to the caller's
                // own opaque type variable, as in generic recursion
                // (`fold` calling `fold_at`).
                for tp in &sig.type_params {
                    if ty_mentions(&sig.produces.ty, tp)
                        && !sig.params.iter().any(|p| ty_mentions(&p.ty, tp))
                    {
                        out.push(Violation {
                            principle: 2,
                            node: hash.clone(),
                            detail: format!(
                                "type parameter `{tp}` of `{func}` appears only \
                                 in the result and cannot be inferred"
                            ),
                        });
                    }
                }
                Some((result_ty, sig.produces.confidence))
            }
            Node::FuncRef(name) => {
                let Some(sig) = sigs.get(&name) else {
                    out.push(Violation {
                        principle: 1,
                        node: hash.clone(),
                        detail: format!("unresolved function: `{name}`"),
                    });
                    return Ok(None);
                };
                // K1 boundary (documented): a function *value* lowers to one
                // `call_indirect` of a fixed type, so it cannot be generic
                // (no instantiation site) nor fallible (its `[tag,val]`
                // return would leak as the value). Both are honest
                // restrictions, not fakes — closures/lambdas come next.
                if !sig.type_params.is_empty() {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: format!(
                            "cannot take a function value of generic `{name}` (v0.4)"
                        ),
                    });
                }
                if !sig.on_failure.is_empty() {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: format!(
                            "cannot take a function value of fallible `{name}` (v0.4)"
                        ),
                    });
                }
                let fn_ty = Type::Fn {
                    params: sig.params.iter().map(|p| p.ty.clone()).collect(),
                    ret: Box::new(sig.produces.ty.clone()),
                    effects: sig.requires.clone(),
                };
                Some((fn_ty, Confidence::Structural))
            }
            Node::CallValue { callee, args } => {
                let c =
                    self.walk_expr(&callee, scope, sigs, out, effects, failures)?;
                let (cty, cconf) = match c {
                    Some(v) => v,
                    None => {
                        for arg in &args {
                            self.walk_expr(
                                arg, scope, sigs, out, effects, failures,
                            )?;
                        }
                        return Ok(None);
                    }
                };
                let Type::Fn {
                    params,
                    ret,
                    effects: fx,
                } = cty
                else {
                    if cty != Type::Never {
                        out.push(Violation {
                            principle: 2,
                            node: callee.clone(),
                            detail: format!(
                                "callee is {cty:?}, not a function value"
                            ),
                        });
                    }
                    for arg in &args {
                        self.walk_expr(
                            arg, scope, sigs, out, effects, failures,
                        )?;
                    }
                    return Ok(None);
                };
                if args.len() != params.len() {
                    out.push(Violation {
                        principle: 2,
                        node: hash.clone(),
                        detail: format!(
                            "function value takes {} argument(s), {} given",
                            params.len(),
                            args.len()
                        ),
                    });
                }
                // Weakest-input propagation across callee and arguments.
                let mut conf = cconf;
                for (i, arg) in args.iter().enumerate() {
                    let inferred =
                        self.walk_expr(arg, scope, sigs, out, effects, failures)?;
                    if let (Some((at, ac)), Some(pt)) = (inferred, params.get(i)) {
                        if !compatible(pt, &at) {
                            out.push(Violation {
                                principle: 2,
                                node: arg.clone(),
                                detail: format!(
                                    "argument {i} is {at:?} but the function \
                                     value expects {pt:?}"
                                ),
                            });
                        }
                        conf = conf.min(ac);
                    }
                }
                effects.extend(fx.iter().copied());
                Some((*ret, conf))
            }
            Node::Lambda { params, body } => {
                // The body sees the enclosing scope plus the lambda's own
                // params. Effects and failures are isolated: making a
                // closure performs nothing — its effects belong to the
                // `Fn` and fire at the call site (`CallValue` unions them).
                let mut s2 = scope.to_vec();
                for p in &params {
                    s2.push((
                        p.name.clone(),
                        Some((p.ty.clone(), p.min_confidence)),
                    ));
                }
                let mut lam_fx = BTreeSet::new();
                let mut lam_fail = BTreeSet::new();
                let bt = self.walk_expr(
                    &body, &s2, sigs, out, &mut lam_fx, &mut lam_fail,
                )?;
                if !lam_fail.is_empty() {
                    out.push(Violation {
                        principle: 6,
                        node: hash.clone(),
                        detail: format!(
                            "a lambda may not raise an uncaught failure: {} (v0.4)",
                            lam_fail.iter().cloned().collect::<Vec<_>>().join(", ")
                        ),
                    });
                }
                let ret = bt.map(|(t, _)| t).unwrap_or(Type::Never);
                let fn_ty = Type::Fn {
                    params: params.iter().map(|p| p.ty.clone()).collect(),
                    ret: Box::new(ret),
                    effects: lam_fx,
                };
                Some((fn_ty, Confidence::Structural))
            }
            Node::Record { type_name, fields } => {
                match self.records.get(&type_name).cloned() {
                    None => {
                        out.push(Violation {
                            principle: 1,
                            node: hash.clone(),
                            detail: format!("unknown record type: `{type_name}`"),
                        });
                        for (_, fh) in &fields {
                            self.walk_expr(fh, scope, sigs, out, effects, failures)?;
                        }
                        None
                    }
                    Some(def_fields) => {
                        let mut conf = Confidence::Persisted;
                        for (fname, fty) in &def_fields {
                            match fields.iter().find(|(n, _)| n == fname) {
                                None => out.push(Violation {
                                    principle: 2,
                                    node: hash.clone(),
                                    detail: format!(
                                        "missing field `{fname}` for `{type_name}`"
                                    ),
                                }),
                                Some((_, fh)) => {
                                    if let Some((vt, vc)) = self.walk_expr(
                                        fh, scope, sigs, out, effects, failures,
                                    )? {
                                        if !compatible(&vt, fty) {
                                            out.push(Violation {
                                                principle: 2,
                                                node: fh.clone(),
                                                detail: format!(
                                                    "field `{fname}` is {vt:?}, expected {fty:?}"
                                                ),
                                            });
                                        }
                                        conf = conf.min(vc);
                                    }
                                }
                            }
                        }
                        for (n, fh) in &fields {
                            if !def_fields.iter().any(|(dn, _)| dn == n) {
                                out.push(Violation {
                                    principle: 2,
                                    node: fh.clone(),
                                    detail: format!("`{type_name}` has no field `{n}`"),
                                });
                                self.walk_expr(fh, scope, sigs, out, effects, failures)?;
                            }
                        }
                        if def_fields.is_empty() {
                            conf = Confidence::Structural;
                        }
                        Some((Type::Named(type_name.clone()), conf))
                    }
                }
            }
            Node::Field {
                base,
                type_name,
                field,
            } => {
                match self.walk_expr(&base, scope, sigs, out, effects, failures)? {
                    Some((Type::Named(rec), bc)) => {
                        if rec != type_name {
                            out.push(Violation {
                                principle: 2,
                                node: hash.clone(),
                                detail: format!(
                                    "field access typed as `{type_name}` but base is `{rec}`"
                                ),
                            });
                        }
                        match self.records.get(&rec) {
                        Some(fs) => match fs.iter().find(|(n, _)| n == &field) {
                            Some((_, fty)) => Some((fty.clone(), bc)),
                            None => {
                                out.push(Violation {
                                    principle: 2,
                                    node: hash.clone(),
                                    detail: format!("`{rec}` has no field `{field}`"),
                                });
                                None
                            }
                        },
                        None => {
                            out.push(Violation {
                                principle: 1,
                                node: hash.clone(),
                                detail: format!("unknown record type: `{rec}`"),
                            });
                            None
                        }
                        }
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: base.clone(),
                            detail: format!(
                                "field access on non-record type {other:?}"
                            ),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::Variant {
                type_name,
                case,
                fields,
            } => match self.variants.get(&type_name).cloned() {
                None => {
                    out.push(Violation {
                        principle: 1,
                        node: hash.clone(),
                        detail: format!("unknown variant type: `{type_name}`"),
                    });
                    for (_, fh) in &fields {
                        self.walk_expr(fh, scope, sigs, out, effects, failures)?;
                    }
                    None
                }
                Some(cases) => match cases.iter().find(|(c, _)| c == &case) {
                    None => {
                        out.push(Violation {
                            principle: 2,
                            node: hash.clone(),
                            detail: format!("`{type_name}` has no case `{case}`"),
                        });
                        for (_, fh) in &fields {
                            self.walk_expr(fh, scope, sigs, out, effects, failures)?;
                        }
                        None
                    }
                    Some((_, payload)) => {
                        let payload = payload.clone();
                        let mut conf = Confidence::Persisted;
                        for (fname, fty) in &payload {
                            match fields.iter().find(|(n, _)| n == fname) {
                                None => out.push(Violation {
                                    principle: 2,
                                    node: hash.clone(),
                                    detail: format!(
                                        "missing field `{fname}` for `{type_name}.{case}`"
                                    ),
                                }),
                                Some((_, fh)) => {
                                    if let Some((vt, vc)) = self.walk_expr(
                                        fh, scope, sigs, out, effects, failures,
                                    )? {
                                        if !compatible(&vt, fty) {
                                            out.push(Violation {
                                                principle: 2,
                                                node: fh.clone(),
                                                detail: format!(
                                                    "field `{fname}` is {vt:?}, expected {fty:?}"
                                                ),
                                            });
                                        }
                                        conf = conf.min(vc);
                                    }
                                }
                            }
                        }
                        for (n, fh) in &fields {
                            if !payload.iter().any(|(dn, _)| dn == n) {
                                out.push(Violation {
                                    principle: 2,
                                    node: fh.clone(),
                                    detail: format!(
                                        "`{type_name}.{case}` has no field `{n}`"
                                    ),
                                });
                                self.walk_expr(fh, scope, sigs, out, effects, failures)?;
                            }
                        }
                        if payload.is_empty() {
                            conf = Confidence::Structural;
                        }
                        Some((Type::Named(type_name.clone()), conf))
                    }
                },
            },
            Node::Match {
                scrutinee,
                type_name,
                arms,
            } => {
                match self.walk_expr(&scrutinee, scope, sigs, out, effects, failures)? {
                    Some((Type::Named(vname), sconf)) => {
                        if vname != type_name {
                            out.push(Violation {
                                principle: 2,
                                node: hash.clone(),
                                detail: format!(
                                    "match typed as `{type_name}` but scrutinee is `{vname}`"
                                ),
                            });
                        }
                        match self.variants.get(&vname).cloned() {
                            None => {
                                out.push(Violation {
                                    principle: 1,
                                    node: hash.clone(),
                                    detail: format!("unknown variant type: `{vname}`"),
                                });
                                None
                            }
                            Some(cases) => {
                                for (cname, _) in &cases {
                                    if !arms.iter().any(|a| &a.case == cname) {
                                        out.push(Violation {
                                            principle: 2,
                                            node: hash.clone(),
                                            detail: format!(
                                                "non-exhaustive match: case `{cname}` not covered"
                                            ),
                                        });
                                    }
                                }
                                let mut result_ty: Option<Type> = None;
                                let mut conf = sconf;
                                for arm in &arms {
                                    let Some((_, payload)) =
                                        cases.iter().find(|(c, _)| c == &arm.case)
                                    else {
                                        out.push(Violation {
                                            principle: 2,
                                            node: hash.clone(),
                                            detail: format!(
                                                "`{vname}` has no case `{}`",
                                                arm.case
                                            ),
                                        });
                                        continue;
                                    };
                                    if arm.bindings.len() != payload.len() {
                                        out.push(Violation {
                                            principle: 2,
                                            node: hash.clone(),
                                            detail: format!(
                                                "case `{}` has {} field(s), {} bound",
                                                arm.case,
                                                payload.len(),
                                                arm.bindings.len()
                                            ),
                                        });
                                    }
                                    let mut s2 = scope.to_vec();
                                    for (i, b) in arm.bindings.iter().enumerate() {
                                        let entry = payload
                                            .get(i)
                                            .map(|(_, ft)| (ft.clone(), sconf));
                                        s2.push((b.clone(), entry));
                                    }
                                    if let Some((bt, bc)) = self.walk_expr(
                                        &arm.body, &s2, sigs, out, effects, failures,
                                    )? {
                                        match &result_ty {
                                            None => result_ty = Some(bt),
                                            Some(rt) => {
                                                if !compatible(rt, &bt) {
                                                    out.push(Violation {
                                                        principle: 2,
                                                        node: hash.clone(),
                                                        detail: format!(
                                                            "match arms differ: {rt:?} vs {bt:?}"
                                                        ),
                                                    });
                                                }
                                            }
                                        }
                                        conf = conf.min(bc);
                                    }
                                }
                                result_ty.map(|t| (t, conf))
                            }
                        }
                    }
                    Some((other, _)) => {
                        out.push(Violation {
                            principle: 2,
                            node: scrutinee.clone(),
                            detail: format!("match on non-variant type {other:?}"),
                        });
                        None
                    }
                    None => None,
                }
            }
            Node::Function { .. }
            | Node::Module { .. }
            | Node::RecordDef { .. }
            | Node::VariantDef { .. } => None,
        })
    }
}

/// Two types are compatible if equal, or if either is `Never` — an
/// expression that diverges can stand wherever a value is expected.
fn compatible(a: &Type, b: &Type) -> bool {
    a == b || *a == Type::Never || *b == Type::Never
}

/// Unify a (possibly type-variable-bearing) parameter type against an actual
/// type, recording type-variable bindings. Monomorphic types unify only by
/// structural equality; `Never` unifies with anything.
fn unify(pat: &Type, actual: &Type, subst: &mut HashMap<String, Type>) -> bool {
    if *actual == Type::Never {
        return true;
    }
    match pat {
        Type::Var(v) => match subst.get(v) {
            Some(bound) => compatible(&bound.clone(), actual),
            None => {
                subst.insert(v.clone(), actual.clone());
                true
            }
        },
        Type::List(a) => {
            if let Type::List(b) = actual {
                unify(a, b, subst)
            } else {
                false
            }
        }
        Type::Option(a) => {
            if let Type::Option(b) = actual {
                unify(a, b, subst)
            } else {
                false
            }
        }
        Type::Cell(a) => {
            if let Type::Cell(b) = actual {
                unify(a, b, subst)
            } else {
                false
            }
        }
        Type::Map(ka, va) => {
            if let Type::Map(kb, vb) = actual {
                unify(ka, kb, subst) && unify(va, vb, subst)
            } else {
                false
            }
        }
        Type::Result(oa, ea) => {
            if let Type::Result(ob, eb) = actual {
                unify(oa, ob, subst) && unify(ea, eb, subst)
            } else {
                false
            }
        }
        Type::Fn {
            params: pa,
            ret: ra,
            ..
        } => {
            if let Type::Fn {
                params: pb,
                ret: rb,
                ..
            } = actual
            {
                pa.len() == pb.len()
                    && pa.iter().zip(pb).all(|(x, y)| unify(x, y, subst))
                    && unify(ra, rb, subst)
            } else {
                false
            }
        }
        _ => pat == actual,
    }
}

/// Apply a type-variable substitution.
fn substitute(t: &Type, subst: &HashMap<String, Type>) -> Type {
    match t {
        Type::Var(v) => subst.get(v).cloned().unwrap_or_else(|| t.clone()),
        Type::List(a) => Type::List(Box::new(substitute(a, subst))),
        Type::Option(a) => Type::Option(Box::new(substitute(a, subst))),
        Type::Cell(a) => Type::Cell(Box::new(substitute(a, subst))),
        Type::Map(k, v) => Type::Map(
            Box::new(substitute(k, subst)),
            Box::new(substitute(v, subst)),
        ),
        Type::Result(o, e) => Type::Result(
            Box::new(substitute(o, subst)),
            Box::new(substitute(e, subst)),
        ),
        Type::Fn {
            params,
            ret,
            effects,
        } => Type::Fn {
            params: params.iter().map(|p| substitute(p, subst)).collect(),
            ret: Box::new(substitute(ret, subst)),
            effects: effects.clone(),
        },
        _ => t.clone(),
    }
}

/// Whether type `t` mentions the named type variable.
fn ty_mentions(t: &Type, name: &str) -> bool {
    match t {
        Type::Var(v) => v == name,
        Type::List(a) | Type::Option(a) | Type::Cell(a) => ty_mentions(a, name),
        Type::Map(k, v) | Type::Result(k, v) => {
            ty_mentions(k, name) || ty_mentions(v, name)
        }
        Type::Fn { params, ret, .. } => {
            params.iter().any(|p| ty_mentions(p, name)) || ty_mentions(ret, name)
        }
        _ => false,
    }
}

/// The child hashes a node references, in order.
pub(crate) fn child_hashes(node: &Node) -> Vec<&NodeHash> {
    match node {
        Node::Lit(_)
        | Node::FloatLit(_)
        | Node::DecimalLit(_)
        | Node::Bool(_)
        | Node::Str(_)
        | Node::Now
        | Node::Rand
        | Node::Ref(_)
        | Node::FuncRef(_)
        | Node::Hole { .. }
        | Node::Fail(_)
        | Node::RecordDef { .. }
        | Node::VariantDef { .. } => Vec::new(),
        Node::StrLen(arg)
        | Node::StrLower(arg)
        | Node::StrFromCode(arg)
        | Node::IntToFloat(arg)
        | Node::FloatToInt(arg)
        | Node::IntToDecimal(arg)
        | Node::DecimalToInt(arg)
        | Node::DecimalRaw(arg)
        | Node::Not(arg)
        | Node::NumberToStr(arg)
        | Node::StrToNumber(arg)
        | Node::StrToNumberOpt(arg) => vec![arg],
        Node::StrConcat(a, b) | Node::StrEq(a, b) => vec![a, b],
        Node::StrSlice { s, start, len } => vec![s, start, len],
        Node::StrContains { haystack, needle } => vec![haystack, needle],
        Node::StrStartsWith { s, prefix } => vec![s, prefix],
        Node::StrIndexOf { haystack, needle } => vec![haystack, needle],
        Node::List(elems) => elems.iter().collect(),
        Node::ListEmpty { .. } => Vec::new(),
        Node::ListCons { head, tail } => vec![head, tail],
        Node::OptionSome(v) => vec![v],
        Node::OptionNone { .. } => Vec::new(),
        Node::OptionElse { opt, default } => vec![opt, default],
        Node::OptionMatch {
            opt,
            some_body,
            none_body,
            ..
        } => vec![opt, some_body, none_body],
        Node::ListTryGet { list, index } => vec![list, index],
        Node::ListLen(arg) => vec![arg],
        Node::ListGet { list, index } => vec![list, index],
        Node::Map(pairs) => {
            let mut v = Vec::with_capacity(pairs.len() * 2);
            for (k, val) in pairs {
                v.push(k);
                v.push(val);
            }
            v
        }
        Node::MapGet { map, key } => vec![map, key],
        Node::MapTryGet { map, key } => vec![map, key],
        Node::MapLen(arg) => vec![arg],
        Node::Log(arg) | Node::Publish(arg) => vec![arg],
        Node::SetHeader { name, value } => vec![name, value],
        Node::MutNew(v) => vec![v],
        Node::MutGet(cell) => vec![cell],
        Node::MutSet { cell, value } => vec![cell, value],
        Node::DiskWrite { path, content } => vec![path, content],
        Node::DiskRead(path) => vec![path],
        Node::NetGet(url) => vec![url],
        Node::DbQuery { sql, params } => vec![sql, params],
        Node::Record { fields, .. } => fields.iter().map(|(_, h)| h).collect(),
        Node::Variant { fields, .. } => fields.iter().map(|(_, h)| h).collect(),
        Node::Field { base, .. } => vec![base],
        Node::Match {
            scrutinee, arms, ..
        } => {
            let mut v = vec![scrutinee];
            v.extend(arms.iter().map(|a| &a.body));
            v
        }
        Node::Handle { body, handlers } => {
            let mut v = vec![body];
            v.extend(handlers.iter().map(|(_, h)| h));
            v
        }
        Node::Call { args, .. } => args.iter().collect(),
        Node::CallValue { callee, args } => {
            let mut v = vec![callee];
            v.extend(args.iter());
            v
        }
        Node::Lambda { body, .. } => vec![body],
        Node::Step { value, .. } => vec![value],
        Node::BinOp { lhs, rhs, .. }
        | Node::FloatOp { lhs, rhs, .. }
        | Node::DecimalOp { lhs, rhs, .. } => vec![lhs, rhs],
        Node::If {
            cond,
            then_branch,
            else_branch,
        } => vec![cond, then_branch, else_branch],
        Node::Function { body, result, .. } => {
            let mut v: Vec<&NodeHash> = body.iter().collect();
            v.push(result);
            v
        }
        Node::Module {
            types, functions, ..
        } => {
            let mut v: Vec<&NodeHash> = types.iter().collect();
            v.extend(functions.iter());
            v
        }
    }
}

/// The structural inverse of [`child_hashes`]: rebuild `node` with its
/// child hashes replaced by `kids`, in the **exact order**
/// `child_hashes` yields them, preserving every non-hash field (ops,
/// names, types, case labels, bindings). `kids.len()` must equal
/// `child_hashes(node).len()` — this is the substitution primitive
/// `replace_node`/`fill_hole` build on; the invariant
/// `child_hashes(&with_child_hashes(n, child_hashes(n))) == child_hashes(n)`
/// is asserted by `with_child_hashes_round_trips`.
pub(crate) fn with_child_hashes(node: &Node, kids: &[NodeHash]) -> Node {
    let k = |i: usize| kids[i].clone();
    match node {
        // Leaves — no children; identity.
        Node::Lit(_)
        | Node::FloatLit(_)
        | Node::DecimalLit(_)
        | Node::Bool(_)
        | Node::Str(_)
        | Node::Now
        | Node::Rand
        | Node::Ref(_)
        | Node::FuncRef(_)
        | Node::Hole { .. }
        | Node::Fail(_)
        | Node::RecordDef { .. }
        | Node::VariantDef { .. }
        | Node::ListEmpty { .. }
        | Node::OptionNone { .. } => node.clone(),

        Node::StrLen(_) => Node::StrLen(k(0)),
        Node::StrLower(_) => Node::StrLower(k(0)),
        Node::StrFromCode(_) => Node::StrFromCode(k(0)),
        Node::IntToFloat(_) => Node::IntToFloat(k(0)),
        Node::FloatToInt(_) => Node::FloatToInt(k(0)),
        Node::IntToDecimal(_) => Node::IntToDecimal(k(0)),
        Node::DecimalToInt(_) => Node::DecimalToInt(k(0)),
        Node::DecimalRaw(_) => Node::DecimalRaw(k(0)),
        Node::Not(_) => Node::Not(k(0)),
        Node::NumberToStr(_) => Node::NumberToStr(k(0)),
        Node::StrToNumber(_) => Node::StrToNumber(k(0)),
        Node::StrToNumberOpt(_) => Node::StrToNumberOpt(k(0)),
        Node::ListLen(_) => Node::ListLen(k(0)),
        Node::MapLen(_) => Node::MapLen(k(0)),
        Node::OptionSome(_) => Node::OptionSome(k(0)),
        Node::Log(_) => Node::Log(k(0)),
        Node::Publish(_) => Node::Publish(k(0)),
        Node::SetHeader { .. } => Node::SetHeader {
            name: k(0),
            value: k(1),
        },
        Node::MutNew(_) => Node::MutNew(k(0)),
        Node::MutGet(_) => Node::MutGet(k(0)),
        Node::DiskRead(_) => Node::DiskRead(k(0)),
        Node::NetGet(_) => Node::NetGet(k(0)),

        Node::StrConcat(_, _) => Node::StrConcat(k(0), k(1)),
        Node::StrEq(_, _) => Node::StrEq(k(0), k(1)),
        Node::StrContains { .. } => Node::StrContains {
            haystack: k(0),
            needle: k(1),
        },
        Node::StrStartsWith { .. } => Node::StrStartsWith {
            s: k(0),
            prefix: k(1),
        },
        Node::StrIndexOf { .. } => Node::StrIndexOf {
            haystack: k(0),
            needle: k(1),
        },
        Node::StrSlice { .. } => Node::StrSlice {
            s: k(0),
            start: k(1),
            len: k(2),
        },
        Node::ListCons { .. } => Node::ListCons {
            head: k(0),
            tail: k(1),
        },
        Node::OptionElse { .. } => Node::OptionElse {
            opt: k(0),
            default: k(1),
        },
        Node::OptionMatch {
            some_bind,
            ..
        } => Node::OptionMatch {
            opt: k(0),
            some_bind: some_bind.clone(),
            some_body: k(1),
            none_body: k(2),
        },
        Node::ListTryGet { .. } => Node::ListTryGet {
            list: k(0),
            index: k(1),
        },
        Node::ListGet { .. } => Node::ListGet {
            list: k(0),
            index: k(1),
        },
        Node::MapGet { .. } => Node::MapGet {
            map: k(0),
            key: k(1),
        },
        Node::MapTryGet { .. } => Node::MapTryGet {
            map: k(0),
            key: k(1),
        },
        Node::MutSet { .. } => Node::MutSet {
            cell: k(0),
            value: k(1),
        },
        Node::DiskWrite { .. } => Node::DiskWrite {
            path: k(0),
            content: k(1),
        },
        Node::DbQuery { .. } => Node::DbQuery {
            sql: k(0),
            params: k(1),
        },
        Node::BinOp { op, .. } => Node::BinOp {
            op: *op,
            lhs: k(0),
            rhs: k(1),
        },
        Node::FloatOp { op, .. } => Node::FloatOp {
            op: *op,
            lhs: k(0),
            rhs: k(1),
        },
        Node::DecimalOp { op, .. } => Node::DecimalOp {
            op: *op,
            lhs: k(0),
            rhs: k(1),
        },
        Node::If { .. } => Node::If {
            cond: k(0),
            then_branch: k(1),
            else_branch: k(2),
        },
        Node::List(elems) => {
            Node::List((0..elems.len()).map(k).collect())
        }
        Node::Map(pairs) => Node::Map(
            (0..pairs.len()).map(|i| (k(2 * i), k(2 * i + 1))).collect(),
        ),
        Node::Record {
            type_name, fields, ..
        } => Node::Record {
            type_name: type_name.clone(),
            fields: fields
                .iter()
                .enumerate()
                .map(|(i, (n, _))| (n.clone(), k(i)))
                .collect(),
        },
        Node::Variant {
            type_name,
            case,
            fields,
        } => Node::Variant {
            type_name: type_name.clone(),
            case: case.clone(),
            fields: fields
                .iter()
                .enumerate()
                .map(|(i, (n, _))| (n.clone(), k(i)))
                .collect(),
        },
        Node::Field {
            type_name, field, ..
        } => Node::Field {
            base: k(0),
            type_name: type_name.clone(),
            field: field.clone(),
        },
        Node::Match {
            type_name, arms, ..
        } => Node::Match {
            scrutinee: k(0),
            type_name: type_name.clone(),
            arms: arms
                .iter()
                .enumerate()
                .map(|(i, a)| MatchArm {
                    body: k(i + 1),
                    ..a.clone()
                })
                .collect(),
        },
        Node::Handle { handlers, .. } => Node::Handle {
            body: k(0),
            handlers: handlers
                .iter()
                .enumerate()
                .map(|(i, (n, _))| (n.clone(), k(i + 1)))
                .collect(),
        },
        Node::Call { func, args } => Node::Call {
            func: func.clone(),
            args: (0..args.len()).map(k).collect(),
        },
        Node::CallValue { args, .. } => Node::CallValue {
            callee: k(0),
            args: (0..args.len()).map(|i| k(i + 1)).collect(),
        },
        Node::Lambda { params, .. } => Node::Lambda {
            params: params.clone(),
            body: k(0),
        },
        Node::Step { binding, .. } => Node::Step {
            binding: binding.clone(),
            value: k(0),
        },
        Node::Function {
            name,
            type_params,
            params,
            produces,
            requires,
            on_failure,
            body,
            ..
        } => Node::Function {
            name: name.clone(),
            type_params: type_params.clone(),
            params: params.clone(),
            produces: produces.clone(),
            requires: requires.clone(),
            on_failure: on_failure.clone(),
            body: (0..body.len()).map(k).collect(),
            result: k(body.len()),
        },
        Node::Module {
            name,
            types,
            functions,
        } => Node::Module {
            name: name.clone(),
            types: (0..types.len()).map(k).collect(),
            functions: (0..functions.len())
                .map(|i| k(types.len() + i))
                .collect(),
        },
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::node::{BinOp, MatchArm, Param};

    fn p(name: &str, ty: Type, c: Confidence) -> Param {
        Param {
            name: name.into(),
            ty,
            min_confidence: c,
        }
    }

    fn produces(ty: Type, confidence: Confidence) -> Produces {
        Produces { ty, confidence }
    }

    #[allow(clippy::too_many_arguments)]
    fn function(
        store: &Store,
        name: &str,
        params: Vec<Param>,
        prod: Produces,
        requires: BTreeSet<Effect>,
        on_failure: Vec<&str>,
        body: Vec<NodeHash>,
        result: NodeHash,
    ) -> NodeHash {
        store
            .put(&Node::Function {
                name: name.into(),
                type_params: vec![],
                params,
                produces: prod,
                requires,
                on_failure: on_failure.into_iter().map(String::from).collect(),
                body,
                result,
            })
            .unwrap()
    }

    /// `add(a: Number@External, b: Number@External) -> Number@Structural`,
    /// pure, no failures — a callee used by other tests. Its result is a
    /// structural literal, so it honors its own `produces`.
    fn add_fn(s: &Store) -> NodeHash {
        let sum = s.put(&Node::Lit(0)).unwrap();
        function(
            s,
            "add",
            vec![
                p("a", Type::Number, Confidence::External),
                p("b", Type::Number, Confidence::External),
            ],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            sum,
        )
    }

    #[test]
    fn a_well_typed_module_is_clean_and_complete() {
        let s = Store::open_in_memory().unwrap();
        let add = add_fn(&s);
        let n = s.put(&Node::Ref("n".into())).unwrap();
        let call = s
            .put(&Node::Call {
                func: "add".into(),
                args: vec![n.clone(), n],
            })
            .unwrap();
        let step = s
            .put(&Node::Step {
                binding: "d".into(),
                value: call,
            })
            .unwrap();
        let res = s.put(&Node::Ref("d".into())).unwrap();
        let double = function(
            &s,
            "double",
            vec![p("n", Type::Number, Confidence::External)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![step],
            res,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![add, double],
            })
            .unwrap();

        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
        assert_eq!(r.status, Status::Complete);
        assert_eq!(r.failures, Failures::Exhaustive);
    }

    #[test]
    fn the_boolean_layer_type_checks() {
        let s = Store::open_in_memory().unwrap();
        // `!(true) || (1 < 2)` : Bool — the literal, the unary, and a
        // logical operator over a comparison.
        let t = s.put(&Node::Bool(true)).unwrap();
        let nott = s.put(&Node::Not(t.clone())).unwrap();
        let one = s.put(&Node::Lit(1)).unwrap();
        let two = s.put(&Node::Lit(2)).unwrap();
        let lt = s
            .put(&Node::BinOp {
                op: BinOp::Lt,
                lhs: one.clone(),
                rhs: two,
            })
            .unwrap();
        let or = s
            .put(&Node::BinOp {
                op: BinOp::Or,
                lhs: nott,
                rhs: lt,
            })
            .unwrap();
        let ok = function(
            &s,
            "ok",
            vec![],
            produces(Type::Bool, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            or,
        );
        let r = Checker::new(&s).check(&ok).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);

        // `!5` — a Number operand to `!` is a Principle 2 violation.
        let five = s.put(&Node::Lit(5)).unwrap();
        let badnot = s.put(&Node::Not(five)).unwrap();
        let bf = function(
            &s,
            "bf",
            vec![],
            produces(Type::Bool, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            badnot,
        );
        let r2 = Checker::new(&s).check(&bf).unwrap();
        assert!(!r2.ok());
        assert!(r2
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("expected Bool")));

        // `1 && true` — a Number operand to `&&` is a Principle 2 violation.
        let andbad = s
            .put(&Node::BinOp {
                op: BinOp::And,
                lhs: one,
                rhs: t,
            })
            .unwrap();
        let ab = function(
            &s,
            "ab",
            vec![],
            produces(Type::Bool, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            andbad,
        );
        let r3 = Checker::new(&s).check(&ab).unwrap();
        assert!(!r3.ok());
        assert!(r3
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("logical operand")));
    }

    #[test]
    fn function_values_type_check() {
        let s = Store::open_in_memory().unwrap();
        let fn_num_num = Type::Fn {
            params: vec![Type::Number],
            ret: Box::new(Type::Number),
            effects: BTreeSet::new(),
        };
        // double(n) -> Number ; apply(f: Fn(Number)->Number, x) -> Number
        // is `f(x)` ; main = apply(&double, 21).
        let dbl = function(
            &s,
            "double",
            vec![p("n", Type::Number, Confidence::Structural)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Ref("n".into())).unwrap(),
        );
        let call_f = s
            .put(&Node::CallValue {
                callee: s.put(&Node::Ref("f".into())).unwrap(),
                args: vec![s.put(&Node::Ref("x".into())).unwrap()],
            })
            .unwrap();
        let apply = function(
            &s,
            "apply",
            vec![
                p("f", fn_num_num.clone(), Confidence::Structural),
                p("x", Type::Number, Confidence::Structural),
            ],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            call_f,
        );
        let main = function(
            &s,
            "main",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "apply".into(),
                args: vec![
                    s.put(&Node::FuncRef("double".into())).unwrap(),
                    s.put(&Node::Lit(21)).unwrap(),
                ],
            })
            .unwrap(),
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![dbl, apply, main],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);

        // `&identity` — a function value of a generic function is rejected.
        let id = identity_fn(&s);
        let badgen = function(
            &s,
            "bg",
            vec![],
            produces(fn_num_num.clone(), Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::FuncRef("identity".into())).unwrap(),
        );
        let mg = s
            .put(&Node::Module {
                name: "mg".into(),
                types: vec![],
                functions: vec![id, badgen],
            })
            .unwrap();
        let rg = Checker::new(&s).check(&mg).unwrap();
        assert!(rg
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("generic")));

        // `&boom` — a function value of a fallible function is rejected.
        let boom = function(
            &s,
            "boom",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec!["Boom"],
            vec![],
            s.put(&Node::Fail("Boom".into())).unwrap(),
        );
        let badfal = function(
            &s,
            "bf2",
            vec![],
            produces(fn_num_num, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::FuncRef("boom".into())).unwrap(),
        );
        let mf = s
            .put(&Node::Module {
                name: "mf".into(),
                types: vec![],
                functions: vec![boom, badfal],
            })
            .unwrap();
        let rf = Checker::new(&s).check(&mf).unwrap();
        assert!(rf
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("fallible")));

        // Calling a non-function value is a Principle 2 violation.
        let badcall = function(
            &s,
            "bc",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::CallValue {
                callee: s.put(&Node::Lit(5)).unwrap(),
                args: vec![],
            })
            .unwrap(),
        );
        let rc = Checker::new(&s).check(&badcall).unwrap();
        assert!(rc
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("not a function value")));
    }

    #[test]
    fn closures_type_check_and_isolate_effects() {
        let s = Store::open_in_memory().unwrap();
        let lam_param = |name: &str| Param {
            name: name.into(),
            ty: Type::Number,
            min_confidence: Confidence::External,
        };
        // mk(k) -> Fn(Number)->Number is `|x| x + k` (captures k).
        let body = s
            .put(&Node::BinOp {
                op: BinOp::Add,
                lhs: s.put(&Node::Ref("x".into())).unwrap(),
                rhs: s.put(&Node::Ref("k".into())).unwrap(),
            })
            .unwrap();
        let lam = s
            .put(&Node::Lambda {
                params: vec![lam_param("x")],
                body,
            })
            .unwrap();
        let fn_num_num = Type::Fn {
            params: vec![Type::Number],
            ret: Box::new(Type::Number),
            effects: BTreeSet::new(),
        };
        let mk = function(
            &s,
            "mk",
            vec![p("k", Type::Number, Confidence::Structural)],
            produces(fn_num_num.clone(), Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            lam,
        );
        let r = Checker::new(&s)
            .check(
                &s.put(&Node::Module {
                    name: "m".into(),
                    types: vec![],
                    functions: vec![mk],
                })
                .unwrap(),
            )
            .unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);

        // Effect isolation: `mklog = |x| log(x)` returns a closure whose
        // Fn type carries Log. *Creating* it performs nothing — mklog
        // needs no `requires` — but the returned type honestly declares
        // the effect. A function that *calls* it must declare Log (P5).
        let fn_log = Type::Fn {
            params: vec![Type::Number],
            ret: Box::new(Type::Number),
            effects: [Effect::Log].into_iter().collect(),
        };
        let log_body = s
            .put(&Node::Log(s.put(&Node::Ref("x".into())).unwrap()))
            .unwrap();
        let log_lam = s
            .put(&Node::Lambda {
                params: vec![lam_param("x")],
                body: log_body,
            })
            .unwrap();
        let mklog = function(
            &s,
            "mklog",
            vec![],
            produces(fn_log.clone(), Confidence::Structural),
            BTreeSet::new(), // no requires — creating a closure is pure
            vec![],
            vec![],
            log_lam,
        );
        let r2 = Checker::new(&s)
            .check(
                &s.put(&Node::Module {
                    name: "m2".into(),
                    types: vec![],
                    functions: vec![mklog],
                })
                .unwrap(),
            )
            .unwrap();
        assert!(
            r2.ok(),
            "creating an effectful closure must be pure: {:?}",
            r2.violations
        );

        // Calling a Log-effecting function value without declaring Log
        // is a Principle 5 violation.
        let call_f = s
            .put(&Node::CallValue {
                callee: s.put(&Node::Ref("f".into())).unwrap(),
                args: vec![s.put(&Node::Lit(0)).unwrap()],
            })
            .unwrap();
        let runner = function(
            &s,
            "runner",
            vec![p("f", fn_log, Confidence::Structural)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(), // missing Log
            vec![],
            vec![],
            call_f,
        );
        let r3 = Checker::new(&s)
            .check(
                &s.put(&Node::Module {
                    name: "m3".into(),
                    types: vec![],
                    functions: vec![runner],
                })
                .unwrap(),
            )
            .unwrap();
        assert!(r3
            .violations
            .iter()
            .any(|v| v.principle == 5 && v.detail.contains("Log")));

        // A lambda may not raise an uncaught failure (v0.4 boundary).
        let fail_lam = s
            .put(&Node::Lambda {
                params: vec![lam_param("x")],
                body: s.put(&Node::Fail("Boom".into())).unwrap(),
            })
            .unwrap();
        let mkfail = function(
            &s,
            "mkfail",
            vec![],
            produces(fn_num_num, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            fail_lam,
        );
        let r4 = Checker::new(&s)
            .check(
                &s.put(&Node::Module {
                    name: "m4".into(),
                    types: vec![],
                    functions: vec![mkfail],
                })
                .unwrap(),
            )
            .unwrap();
        assert!(r4
            .violations
            .iter()
            .any(|v| v.principle == 6 && v.detail.contains("uncaught failure")));
    }

    #[test]
    fn option_match_type_checks() {
        let s = Store::open_in_memory().unwrap();
        // f(o: Option<Number>) -> Number = match o { Some(v) -> v+1, None -> 0 }
        let good = s
            .put(&Node::OptionMatch {
                opt: s.put(&Node::Ref("o".into())).unwrap(),
                some_bind: "v".into(),
                some_body: s
                    .put(&Node::BinOp {
                        op: BinOp::Add,
                        lhs: s.put(&Node::Ref("v".into())).unwrap(),
                        rhs: s.put(&Node::Lit(1)).unwrap(),
                    })
                    .unwrap(),
                none_body: s.put(&Node::Lit(0)).unwrap(),
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![p(
                "o",
                Type::Option(Box::new(Type::Number)),
                Confidence::Structural,
            )],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            good,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);

        // Scrutinee not an Option -> Principle 2.
        let bad_scrut = s
            .put(&Node::OptionMatch {
                opt: s.put(&Node::Lit(5)).unwrap(),
                some_bind: "v".into(),
                some_body: s.put(&Node::Ref("v".into())).unwrap(),
                none_body: s.put(&Node::Lit(0)).unwrap(),
            })
            .unwrap();
        let bf = function(
            &s,
            "bf",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            bad_scrut,
        );
        let r2 = Checker::new(&s).check(&bf).unwrap();
        assert!(r2
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("expected Option")));

        // Arms of different types -> Principle 2.
        let bad_arms = s
            .put(&Node::OptionMatch {
                opt: s.put(&Node::Ref("o".into())).unwrap(),
                some_bind: "v".into(),
                some_body: s.put(&Node::Str("x".into())).unwrap(),
                none_body: s.put(&Node::Lit(0)).unwrap(),
            })
            .unwrap();
        let ba = function(
            &s,
            "ba",
            vec![p(
                "o",
                Type::Option(Box::new(Type::Number)),
                Confidence::Structural,
            )],
            produces(Type::String, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            bad_arms,
        );
        let r3 = Checker::new(&s).check(&ba).unwrap();
        assert!(r3
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("arms differ")));
    }

    #[test]
    fn float_type_checks() {
        let s = Store::open_in_memory().unwrap();
        let f = |v: f64| s.put(&Node::FloatLit(v.to_bits())).unwrap();

        // f() -> Float = 1.5 * 2.0
        let good = function(
            &s,
            "g",
            vec![],
            produces(Type::Float, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::FloatOp {
                op: BinOp::Mul,
                lhs: f(1.5),
                rhs: f(2.0),
            })
            .unwrap(),
        );
        let r = Checker::new(&s).check(&good).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);

        // Float op with a Number operand -> Principle 2.
        let mixed = function(
            &s,
            "mx",
            vec![],
            produces(Type::Float, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::FloatOp {
                op: BinOp::Add,
                lhs: f(1.0),
                rhs: s.put(&Node::Lit(2)).unwrap(),
            })
            .unwrap(),
        );
        let r2 = Checker::new(&s).check(&mixed).unwrap();
        assert!(r2
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("expected Float")));

        // `%` is not defined on Float -> Principle 2.
        let modf = function(
            &s,
            "mf",
            vec![],
            produces(Type::Float, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::FloatOp {
                op: BinOp::Mod,
                lhs: f(5.0),
                rhs: f(2.0),
            })
            .unwrap(),
        );
        let r3 = Checker::new(&s).check(&modf).unwrap();
        assert!(r3
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("not defined on Float")));
    }

    #[test]
    fn decimal_type_checks() {
        let s = Store::open_in_memory().unwrap();
        let d = |v: i64| s.put(&Node::DecimalLit(v)).unwrap();

        let good = function(
            &s,
            "g",
            vec![],
            produces(Type::Decimal, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::DecimalOp {
                op: BinOp::Mul,
                lhs: d(12500),
                rhs: d(40000),
            })
            .unwrap(),
        );
        assert!(Checker::new(&s).check(&good).unwrap().ok());

        // Number operand to a Decimal op -> Principle 2.
        let mixed = function(
            &s,
            "mx",
            vec![],
            produces(Type::Decimal, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::DecimalOp {
                op: BinOp::Add,
                lhs: d(10000),
                rhs: s.put(&Node::Lit(2)).unwrap(),
            })
            .unwrap(),
        );
        let r2 = Checker::new(&s).check(&mixed).unwrap();
        assert!(r2
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("expected Decimal")));

        // `%` is not defined on Decimal -> Principle 2.
        let modd = function(
            &s,
            "md",
            vec![],
            produces(Type::Decimal, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::DecimalOp {
                op: BinOp::Mod,
                lhs: d(50000),
                rhs: d(20000),
            })
            .unwrap(),
        );
        let r3 = Checker::new(&s).check(&modd).unwrap();
        assert!(r3
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("not defined on Decimal")));
    }

    #[test]
    fn publish_requires_the_live_effect() {
        let s = Store::open_in_memory().unwrap();
        let body = || s.put(&Node::Publish(
            s.put(&Node::Str("items".into())).unwrap(),
        )).unwrap();
        // requires Live → clean.
        let ok = function(
            &s,
            "notify",
            vec![],
            produces(Type::Number, Confidence::Structural),
            [Effect::Live].into_iter().collect(),
            vec![],
            vec![],
            body(),
        );
        assert!(Checker::new(&s).check(&ok).unwrap().ok());
        // missing requires Live → Principle 5.
        let bad = function(
            &s,
            "notify2",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            body(),
        );
        let r = Checker::new(&s).check(&bad).unwrap();
        assert!(
            r.violations
                .iter()
                .any(|v| v.principle == 5 && v.detail.contains("Live")),
            "publish without `requires Live` must be P5: {:?}",
            r.violations
        );
    }

    #[test]
    fn numeric_and_closure_soundness() {
        // Adversarial: every program here MUST be rejected. Number,
        // Decimal, and Float-bits are all i64 at runtime, so a missed
        // rejection is silent corruption, not a trap — the worst failure
        // for a trust-the-checker language. A failing assertion here is a
        // real soundness hole, not a test bug.
        let s = Store::open_in_memory().unwrap();
        let flt = |v: f64| s.put(&Node::FloatLit(v.to_bits())).unwrap();
        let dec = |v: i64| s.put(&Node::DecimalLit(v)).unwrap();
        let lit = |v: i64| s.put(&Node::Lit(v)).unwrap();
        let rf = |n: &str| s.put(&Node::Ref(n.into())).unwrap();
        let rejects = |f: &NodeHash, why: &str| {
            let r = Checker::new(&s).check(f).unwrap();
            assert!(
                !r.ok() && r.violations.iter().any(|v| v.principle == 2),
                "UNSOUND: checker accepted `{why}` — {:?}",
                r.violations
            );
        };
        let module = |fns: Vec<NodeHash>| {
            s.put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: fns,
            })
            .unwrap()
        };
        let pnum = |n: &str| p(n, Type::Number, Confidence::Structural);

        // 1. Float returned where Number is declared.
        rejects(
            &function(
                &s,
                "r1",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                flt(1.0),
            ),
            "Float as Number result",
        );
        // 2. Number arithmetic with a Float operand.
        rejects(
            &function(
                &s,
                "r2",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::BinOp {
                    op: BinOp::Add,
                    lhs: lit(1),
                    rhs: flt(2.0),
                })
                .unwrap(),
            ),
            "Number + Float",
        );
        // 3. Float op with a Decimal operand (both i64 — the silent one).
        rejects(
            &function(
                &s,
                "r3",
                vec![],
                produces(Type::Float, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::FloatOp {
                    op: BinOp::Add,
                    lhs: flt(1.0),
                    rhs: dec(20000),
                })
                .unwrap(),
            ),
            "Float + Decimal",
        );
        // 4. Float passed to a Number parameter across a call.
        let idn = function(
            &s,
            "idn",
            vec![pnum("n")],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            rf("n"),
        );
        let c4 = function(
            &s,
            "c4",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "idn".into(),
                args: vec![flt(3.0)],
            })
            .unwrap(),
        );
        rejects(&module(vec![idn, c4]), "Float arg to Number param");
        // 5. CallValue arity mismatch (closure of 1 param, 2 args).
        rejects(
            &function(
                &s,
                "r5",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::CallValue {
                    callee: s
                        .put(&Node::Lambda {
                            params: vec![pnum("x")],
                            body: rf("x"),
                        })
                        .unwrap(),
                    args: vec![lit(1), lit(2)],
                })
                .unwrap(),
            ),
            "closure arity mismatch",
        );
        // 6. CallValue arg-type mismatch (Float into Fn(Number)).
        rejects(
            &function(
                &s,
                "r6",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::CallValue {
                    callee: s
                        .put(&Node::Lambda {
                            params: vec![pnum("x")],
                            body: rf("x"),
                        })
                        .unwrap(),
                    args: vec![flt(1.0)],
                })
                .unwrap(),
            ),
            "Float into Fn(Number)",
        );
        // 7. Lambda return type vs. expected Fn return (unify Fn ret).
        let apply = function(
            &s,
            "apply",
            vec![p(
                "f",
                Type::Fn {
                    params: vec![Type::Number],
                    ret: Box::new(Type::Number),
                    effects: BTreeSet::new(),
                },
                Confidence::Structural,
            )],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::CallValue {
                callee: rf("f"),
                args: vec![lit(1)],
            })
            .unwrap(),
        );
        let c7 = function(
            &s,
            "c7",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "apply".into(),
                args: vec![s
                    .put(&Node::Lambda {
                        params: vec![pnum("x")],
                        body: s.put(&Node::Str("nope".into())).unwrap(),
                    })
                    .unwrap()],
            })
            .unwrap(),
        );
        rejects(
            &module(vec![apply, c7]),
            "Fn(Number)->String where Fn(Number)->Number expected",
        );
        // 8. Type parameter that occurs only in the result (uninferable).
        let phantom = s
            .put(&Node::Function {
                name: "phantom".into(),
                type_params: vec!["T".into()],
                params: vec![pnum("x")],
                produces: produces(
                    Type::Option(Box::new(Type::Var("T".into()))),
                    Confidence::Structural,
                ),
                requires: BTreeSet::new(),
                on_failure: vec![],
                body: vec![],
                result: s
                    .put(&Node::OptionNone {
                        elem: Type::Var("T".into()),
                    })
                    .unwrap(),
            })
            .unwrap();
        let usep = function(
            &s,
            "usep",
            vec![],
            produces(
                Type::Option(Box::new(Type::Number)),
                Confidence::Structural,
            ),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "phantom".into(),
                args: vec![lit(0)],
            })
            .unwrap(),
        );
        rejects(
            &module(vec![phantom, usep]),
            "type param only in result (uninferable)",
        );
        // 9. OptionMatch arms of different numeric types.
        rejects(
            &function(
                &s,
                "r9",
                vec![p(
                    "o",
                    Type::Option(Box::new(Type::Number)),
                    Confidence::Structural,
                )],
                produces(Type::Float, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::OptionMatch {
                    opt: rf("o"),
                    some_bind: "v".into(),
                    some_body: flt(1.0),
                    none_body: lit(0),
                })
                .unwrap(),
            ),
            "OptionMatch Float/Number arms",
        );
        // 10. IntToFloat applied to a String.
        rejects(
            &function(
                &s,
                "r10",
                vec![],
                produces(Type::Float, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::IntToFloat(
                    s.put(&Node::Str("x".into())).unwrap(),
                ))
                .unwrap(),
            ),
            "to_float(String)",
        );
    }

    #[test]
    fn effect_failure_confidence_soundness() {
        // The other three core guarantees, adversarially. A hole here is
        // a "pure" function that does I/O, an uncaught failure that
        // escapes typing, or unvalidated data reaching a validated sink —
        // each a direct thesis violation, and each silent.
        let s = Store::open_in_memory().unwrap();
        let lit = |v: i64| s.put(&Node::Lit(v)).unwrap();
        let rf = |n: &str| s.put(&Node::Ref(n.into())).unwrap();
        let module = |fns: Vec<NodeHash>| {
            s.put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: fns,
            })
            .unwrap()
        };
        let rej = |f: &NodeHash, principle: u8, why: &str| {
            let r = Checker::new(&s).check(f).unwrap();
            assert!(
                !r.ok() && r.violations.iter().any(|v| v.principle == principle),
                "UNSOUND: accepted `{why}` (expected P{principle}) — {:?}",
                r.violations
            );
        };
        let truth = || {
            s.put(&Node::BinOp {
                op: BinOp::Eq,
                lhs: lit(0),
                rhs: lit(0),
            })
            .unwrap()
        };

        // P5 — a Log effect, undeclared.
        rej(
            &function(
                &s,
                "e1",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::Log(lit(1))).unwrap(),
            ),
            5,
            "Log with requires {}",
        );
        // P5 — effect performed inside an If branch must still surface.
        rej(
            &function(
                &s,
                "e2",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::If {
                    cond: truth(),
                    then_branch: s.put(&Node::Log(lit(1))).unwrap(),
                    else_branch: lit(0),
                })
                .unwrap(),
            ),
            5,
            "Log inside an If branch with requires {}",
        );
        // P5 — effect propagates across a call (callee Time, caller {}).
        let timed = function(
            &s,
            "timed",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::from([Effect::Time]),
            vec![],
            vec![],
            s.put(&Node::Now).unwrap(),
        );
        let caller5 = function(
            &s,
            "caller5",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "timed".into(),
                args: vec![],
            })
            .unwrap(),
        );
        rej(
            &module(vec![timed, caller5]),
            5,
            "calling a Time fn without declaring Time",
        );
        // P6 — Fail inside an If branch, uncovered.
        rej(
            &function(
                &s,
                "f1",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::If {
                    cond: truth(),
                    then_branch: s.put(&Node::Fail("Boom".into())).unwrap(),
                    else_branch: lit(0),
                })
                .unwrap(),
            ),
            6,
            "Fail in a branch, on_failure []",
        );
        // P6 — a partial Handle leaves a different failure uncaught.
        rej(
            &function(
                &s,
                "f2",
                vec![],
                produces(Type::Number, Confidence::Structural),
                BTreeSet::new(),
                vec![],
                vec![],
                s.put(&Node::Handle {
                    body: s.put(&Node::Fail("Y".into())).unwrap(),
                    handlers: vec![("X".into(), lit(0))],
                })
                .unwrap(),
            ),
            6,
            "Handle X but body fails Y",
        );
        // P6 — failure propagates across a call.
        let raiser = function(
            &s,
            "raiser",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec!["Boom"],
            vec![],
            s.put(&Node::Fail("Boom".into())).unwrap(),
        );
        let caller6 = function(
            &s,
            "caller6",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "raiser".into(),
                args: vec![],
            })
            .unwrap(),
        );
        rej(
            &module(vec![raiser, caller6]),
            6,
            "calling a fallible fn without covering its failure",
        );
        // P7 — External value into a Validated-min parameter.
        let sink = function(
            &s,
            "sink",
            vec![p("x", Type::Number, Confidence::Validated)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            rf("x"),
        );
        let weak = function(
            &s,
            "weak",
            vec![p("e", Type::Number, Confidence::External)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "sink".into(),
                args: vec![rf("e")],
            })
            .unwrap(),
        );
        rej(
            &module(vec![sink, weak]),
            7,
            "External arg into a Validated param",
        );
        // P7 — weakest-input propagation: External + 1 is still External.
        let sink2 = function(
            &s,
            "sink2",
            vec![p("x", Type::Number, Confidence::Validated)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            rf("x"),
        );
        let derived = function(
            &s,
            "derived",
            vec![p("e", Type::Number, Confidence::External)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Call {
                func: "sink2".into(),
                args: vec![s
                    .put(&Node::BinOp {
                        op: BinOp::Add,
                        lhs: rf("e"),
                        rhs: lit(1),
                    })
                    .unwrap()],
            })
            .unwrap(),
        );
        rej(
            &module(vec![sink2, derived]),
            7,
            "weakest-input: (External + 1) into Validated param",
        );
    }

    #[test]
    fn a_type_mismatch_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        // f() -> String  but result is a Number literal.
        let lit = s.put(&Node::Lit(1)).unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::String, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            lit.clone(),
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(!r.ok());
        let v = &r.violations[0];
        assert_eq!(v.principle, 2);
        assert_eq!(v.node, lit);
        assert!(v.detail.contains("String"));
    }

    #[test]
    fn passing_weaker_confidence_than_required_is_a_principle_7_violation() {
        let s = Store::open_in_memory().unwrap();
        // need(x: Number@Validated) and a caller passing an External param.
        let xref = s.put(&Node::Ref("x".into())).unwrap();
        let need = function(
            &s,
            "need",
            vec![p("x", Type::Number, Confidence::Validated)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            xref,
        );
        let raw = s.put(&Node::Ref("raw".into())).unwrap();
        let call = s
            .put(&Node::Call {
                func: "need".into(),
                args: vec![raw.clone()],
            })
            .unwrap();
        let caller = function(
            &s,
            "caller",
            vec![p("raw", Type::Number, Confidence::External)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            call,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![need, caller],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 7 && v.node == raw));
    }

    #[test]
    fn an_undeclared_effect_is_a_principle_5_violation() {
        let s = Store::open_in_memory().unwrap();
        // writer requires Db; caller calls it but declares no effects.
        let unit = s.put(&Node::Lit(0)).unwrap();
        let mut db = BTreeSet::new();
        db.insert(Effect::Db);
        let writer = function(
            &s,
            "writer",
            vec![],
            produces(Type::Number, Confidence::Structural),
            db,
            vec![],
            vec![],
            unit,
        );
        let call = s
            .put(&Node::Call {
                func: "writer".into(),
                args: vec![],
            })
            .unwrap();
        let caller = function(
            &s,
            "caller",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(), // declares no effects, but calls writer (Db)
            vec![],
            vec![],
            call,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![writer, caller],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 5));
        assert!(r.effects.contains(&Effect::Db));
    }

    #[test]
    fn an_uncovered_failure_is_a_principle_6_violation() {
        let s = Store::open_in_memory().unwrap();
        let unit = s.put(&Node::Lit(0)).unwrap();
        let risky = function(
            &s,
            "risky",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec!["Boom"],
            vec![],
            unit.clone(),
        );
        let call = s
            .put(&Node::Call {
                func: "risky".into(),
                args: vec![],
            })
            .unwrap();
        let caller = function(
            &s,
            "caller",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![], // does not cover `Boom`
            vec![],
            call,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![risky, caller],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 6));
        assert_eq!(r.failures, Failures::Uncovered(vec!["Boom".into()]));
    }

    #[test]
    fn an_unresolved_reference_is_a_principle_1_violation() {
        let s = Store::open_in_memory().unwrap();
        let ghost = s.put(&Node::Ref("ghost".into())).unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            ghost.clone(),
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 1 && v.node == ghost));
    }

    #[test]
    fn a_hole_makes_it_incomplete_but_not_invalid() {
        let s = Store::open_in_memory().unwrap();
        let hole = s
            .put(&Node::Hole {
                expects: "Number".into(),
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![hole.clone()],
            s.put(&Node::Lit(0)).unwrap(),
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert_eq!(r.status, Status::Incomplete);
        assert_eq!(r.holes, vec![hole]);
        assert!(r.ok());
    }

    #[test]
    fn a_missing_child_is_a_principle_4_violation() {
        let s = Store::open_in_memory().unwrap();
        let dangling = Node::Ref("never".into()).hash();
        let step = s
            .put(&Node::Step {
                binding: "x".into(),
                value: dangling.clone(),
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![step],
            s.put(&Node::Lit(0)).unwrap(),
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 4 && v.node == dangling));
    }

    #[test]
    fn a_step_binding_is_not_in_scope_for_its_own_value() {
        let s = Store::open_in_memory().unwrap();
        let aref = s.put(&Node::Ref("a".into())).unwrap();
        let step = s
            .put(&Node::Step {
                binding: "a".into(),
                value: aref.clone(),
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![step],
            s.put(&Node::Lit(0)).unwrap(),
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 1 && v.node == aref));
    }

    #[test]
    fn unchanged_subtrees_are_not_recomputed() {
        let s = Store::open_in_memory().unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            s.put(&Node::Lit(1)).unwrap(),
        );
        let mut c = Checker::new(&s);
        c.check(&f).unwrap();
        let after_first = c.computed_count();
        assert!(after_first > 0);
        c.check(&f).unwrap();
        assert_eq!(c.computed_count(), after_first);
    }

    /// `a + b` with `a@Validated, b@External` yields `Number@External`
    /// (weakest input). Declaring `produces … @ Validated` is then a P7
    /// violation — the decided weakest-input rule, now with a real site.
    #[test]
    fn arithmetic_confidence_is_the_weakest_input() {
        let s = Store::open_in_memory().unwrap();
        let a = s.put(&Node::Ref("a".into())).unwrap();
        let b = s.put(&Node::Ref("b".into())).unwrap();
        let sum = s
            .put(&Node::BinOp {
                op: BinOp::Add,
                lhs: a,
                rhs: b,
            })
            .unwrap();
        let f = function(
            &s,
            "combine",
            vec![
                p("a", Type::Number, Confidence::Validated),
                p("b", Type::Number, Confidence::External),
            ],
            produces(Type::Number, Confidence::Validated),
            BTreeSet::new(),
            vec![],
            vec![],
            sum.clone(),
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(
            r.violations
                .iter()
                .any(|v| v.principle == 7 && v.node == sum),
            "expected weakest-input P7, got {:?}",
            r.violations
        );
        assert_eq!(r.confidence, Some(Confidence::External));
    }

    #[test]
    fn a_comparison_yields_bool() {
        let s = Store::open_in_memory().unwrap();
        let a = s.put(&Node::Ref("a".into())).unwrap();
        let b = s.put(&Node::Ref("b".into())).unwrap();
        let cmp = s
            .put(&Node::BinOp {
                op: BinOp::Lt,
                lhs: a,
                rhs: b,
            })
            .unwrap();
        let f = function(
            &s,
            "less",
            vec![
                p("a", Type::Number, Confidence::Structural),
                p("b", Type::Number, Confidence::Structural),
            ],
            produces(Type::Bool, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            cmp,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
    }

    #[test]
    fn arithmetic_on_a_bool_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        let a = s.put(&Node::Ref("a".into())).unwrap();
        let b = s.put(&Node::Ref("b".into())).unwrap();
        let cmp = s
            .put(&Node::BinOp {
                op: BinOp::Lt,
                lhs: a.clone(),
                rhs: b,
            })
            .unwrap();
        // (a < b) + a  — Bool operand in arithmetic.
        let bad = s
            .put(&Node::BinOp {
                op: BinOp::Add,
                lhs: cmp,
                rhs: a,
            })
            .unwrap();
        let f = function(
            &s,
            "bad",
            vec![
                p("a", Type::Number, Confidence::Structural),
                p("b", Type::Number, Confidence::Structural),
            ],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            bad,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 2));
    }

    #[test]
    fn a_non_bool_condition_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        let one = s.put(&Node::Lit(1)).unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let iff = s
            .put(&Node::If {
                cond: one.clone(), // Number, not Bool
                then_branch: one.clone(),
                else_branch: zero,
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            iff,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.node == one));
    }

    /// `abs(n) = if n < 0 then 0 - n else n end` — a real conditional that
    /// type-checks clean.
    #[test]
    fn a_well_typed_conditional_is_clean() {
        let s = Store::open_in_memory().unwrap();
        let n = s.put(&Node::Ref("n".into())).unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let cond = s
            .put(&Node::BinOp {
                op: BinOp::Lt,
                lhs: n.clone(),
                rhs: zero.clone(),
            })
            .unwrap();
        let neg = s
            .put(&Node::BinOp {
                op: BinOp::Sub,
                lhs: zero,
                rhs: n.clone(),
            })
            .unwrap();
        let iff = s
            .put(&Node::If {
                cond,
                then_branch: neg,
                else_branch: n,
            })
            .unwrap();
        let f = function(
            &s,
            "abs",
            vec![p("n", Type::Number, Confidence::External)],
            produces(Type::Number, Confidence::External),
            BTreeSet::new(),
            vec![],
            vec![],
            iff,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
        assert_eq!(r.confidence, Some(Confidence::External));
    }

    #[test]
    fn an_uncovered_fail_is_a_principle_6_violation() {
        let s = Store::open_in_memory().unwrap();
        let boom = s.put(&Node::Fail("Boom".into())).unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![], // does NOT declare Boom
            vec![],
            boom,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 6));
        assert_eq!(r.failures, Failures::Uncovered(vec!["Boom".into()]));
    }

    /// `safe_div(a, b) on_failure DivByZero =
    ///    if b == 0 then fail DivByZero else a / b end`
    /// — a real fallible function that type-checks clean. The `fail` branch
    /// is `Never` and unifies with the `Number` branch; the failure is
    /// covered by `on_failure`.
    #[test]
    fn a_fallible_function_with_a_covered_failure_is_clean() {
        let s = Store::open_in_memory().unwrap();
        let a = s.put(&Node::Ref("a".into())).unwrap();
        let b = s.put(&Node::Ref("b".into())).unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let is_zero = s
            .put(&Node::BinOp {
                op: BinOp::Eq,
                lhs: b.clone(),
                rhs: zero,
            })
            .unwrap();
        let boom = s.put(&Node::Fail("DivByZero".into())).unwrap();
        let div = s
            .put(&Node::BinOp {
                op: BinOp::Div,
                lhs: a,
                rhs: b,
            })
            .unwrap();
        let iff = s
            .put(&Node::If {
                cond: is_zero,
                then_branch: boom,
                else_branch: div,
            })
            .unwrap();
        let f = function(
            &s,
            "safe_div",
            vec![
                p("a", Type::Number, Confidence::Structural),
                p("b", Type::Number, Confidence::Structural),
            ],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec!["DivByZero"],
            vec![],
            iff,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
        assert_eq!(r.failures, Failures::Exhaustive);
    }

    #[test]
    fn handle_catches_a_failure_so_it_need_not_propagate() {
        let s = Store::open_in_memory().unwrap();
        // risky() on_failure [Boom]
        let unit = s.put(&Node::Lit(0)).unwrap();
        let risky = function(
            &s,
            "risky",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec!["Boom"],
            vec![],
            unit,
        );
        // caller: step x = risky() on Boom -> 0 ;  result x
        let call = s
            .put(&Node::Call {
                func: "risky".into(),
                args: vec![],
            })
            .unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let handle = s
            .put(&Node::Handle {
                body: call,
                handlers: vec![("Boom".into(), zero)],
            })
            .unwrap();
        let step = s
            .put(&Node::Step {
                binding: "x".into(),
                value: handle,
            })
            .unwrap();
        let xref = s.put(&Node::Ref("x".into())).unwrap();
        let caller = function(
            &s,
            "caller",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![], // declares NO failures — Boom is handled, so this is fine
            vec![step],
            xref,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![risky, caller],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
        assert_eq!(r.failures, Failures::Exhaustive);
    }

    fn point_def(s: &Store) -> NodeHash {
        s.put(&Node::RecordDef {
            name: "Point".into(),
            fields: vec![
                ("x".into(), Type::Number),
                ("y".into(), Type::Number),
            ],
        })
        .unwrap()
    }

    #[test]
    fn a_record_module_typechecks_clean() {
        let s = Store::open_in_memory().unwrap();
        let pd = point_def(&s);

        // mk(a) -> Point { x: a, y: 0 }
        let a = s.put(&Node::Ref("a".into())).unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let rec = s
            .put(&Node::Record {
                type_name: "Point".into(),
                fields: vec![("x".into(), a), ("y".into(), zero)],
            })
            .unwrap();
        let mk = function(
            &s,
            "mk",
            vec![p("a", Type::Number, Confidence::Structural)],
            produces(Type::Named("Point".into()), Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            rec,
        );

        // getx(pt) -> pt.x
        let pref = s.put(&Node::Ref("pt".into())).unwrap();
        let fx = s
            .put(&Node::Field {
                base: pref,
                type_name: "Point".into(),
                field: "x".into(),
            })
            .unwrap();
        let getx = function(
            &s,
            "getx",
            vec![p(
                "pt",
                Type::Named("Point".into()),
                Confidence::Structural,
            )],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            fx,
        );

        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![pd],
                functions: vec![mk, getx],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
    }

    #[test]
    fn a_wrong_field_type_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        let pd = point_def(&s);
        // x given a Bool (a < b) instead of Number.
        let a = s.put(&Node::Ref("a".into())).unwrap();
        let b = s.put(&Node::Ref("b".into())).unwrap();
        let cmp = s
            .put(&Node::BinOp {
                op: BinOp::Lt,
                lhs: a,
                rhs: b,
            })
            .unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let rec = s
            .put(&Node::Record {
                type_name: "Point".into(),
                fields: vec![("x".into(), cmp), ("y".into(), zero)],
            })
            .unwrap();
        let mk = function(
            &s,
            "mk",
            vec![
                p("a", Type::Number, Confidence::Structural),
                p("b", Type::Number, Confidence::Structural),
            ],
            produces(Type::Named("Point".into()), Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            rec,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![pd],
                functions: vec![mk],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 2));
    }

    #[test]
    fn an_unknown_record_type_is_a_principle_1_violation() {
        let s = Store::open_in_memory().unwrap();
        let z = s.put(&Node::Lit(0)).unwrap();
        let rec = s
            .put(&Node::Record {
                type_name: "Nope".into(),
                fields: vec![("a".into(), z)],
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Named("Nope".into()), Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            rec,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 1));
    }

    /// `type Status = variant { Active, Closed(reason: Number) }` and a
    /// function that constructs and exhaustively matches it.
    fn status_def(s: &Store) -> NodeHash {
        s.put(&Node::VariantDef {
            name: "Status".into(),
            cases: vec![
                ("Active".into(), vec![]),
                ("Closed".into(), vec![("reason".into(), Type::Number)]),
            ],
        })
        .unwrap()
    }

    #[test]
    fn a_variant_module_with_exhaustive_match_is_clean() {
        let s = Store::open_in_memory().unwrap();
        let sd = status_def(&s);

        // describe(st) -> match st { Active -> 0, Closed(reason) -> reason }
        let st = s.put(&Node::Ref("st".into())).unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        let rref = s.put(&Node::Ref("reason".into())).unwrap();
        let m = s
            .put(&Node::Match {
                scrutinee: st,
                type_name: "Status".into(),
                arms: vec![
                    MatchArm {
                        case: "Active".into(),
                        bindings: vec![],
                        body: zero,
                    },
                    MatchArm {
                        case: "Closed".into(),
                        bindings: vec!["reason".into()],
                        body: rref,
                    },
                ],
            })
            .unwrap();
        let describe = function(
            &s,
            "describe",
            vec![p(
                "st",
                Type::Named("Status".into()),
                Confidence::Structural,
            )],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            m,
        );
        let module = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![sd],
                functions: vec![describe],
            })
            .unwrap();
        let r = Checker::new(&s).check(&module).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
    }

    #[test]
    fn a_non_exhaustive_match_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        let sd = status_def(&s);
        let st = s.put(&Node::Ref("st".into())).unwrap();
        let zero = s.put(&Node::Lit(0)).unwrap();
        // Only covers Active; Closed missing.
        let m = s
            .put(&Node::Match {
                scrutinee: st,
                type_name: "Status".into(),
                arms: vec![MatchArm {
                    case: "Active".into(),
                    bindings: vec![],
                    body: zero,
                }],
            })
            .unwrap();
        let f = function(
            &s,
            "f",
            vec![p(
                "st",
                Type::Named("Status".into()),
                Confidence::Structural,
            )],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            m,
        );
        let module = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![sd],
                functions: vec![f],
            })
            .unwrap();
        let r = Checker::new(&s).check(&module).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("Closed")));
    }

    #[test]
    fn constructing_an_unknown_case_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        let sd = status_def(&s);
        let bad = s
            .put(&Node::Variant {
                type_name: "Status".into(),
                case: "Nope".into(),
                fields: vec![],
            })
            .unwrap();
        let f = function(
            &s,
            "mk",
            vec![],
            produces(Type::Named("Status".into()), Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            bad,
        );
        let module = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![sd],
                functions: vec![f],
            })
            .unwrap();
        let r = Checker::new(&s).check(&module).unwrap();
        assert!(r
            .violations
            .iter()
            .any(|v| v.principle == 2 && v.detail.contains("Nope")));
    }

    /// `identity<T>(x: T) -> T` used at `Number` — the type parameter is
    /// inferred from the argument and substituted into the result.
    fn identity_fn(s: &Store) -> NodeHash {
        let x = s.put(&Node::Ref("x".into())).unwrap();
        s.put(&Node::Function {
            name: "identity".into(),
            type_params: vec!["T".into()],
            params: vec![p("x", Type::Var("T".into()), Confidence::Structural)],
            produces: Produces {
                ty: Type::Var("T".into()),
                confidence: Confidence::Structural,
            },
            requires: BTreeSet::new(),
            on_failure: vec![],
            body: vec![],
            result: x,
        })
        .unwrap()
    }

    #[test]
    fn a_generic_function_resolves_at_the_call_site() {
        let s = Store::open_in_memory().unwrap();
        let id = identity_fn(&s);
        let n = s.put(&Node::Ref("n".into())).unwrap();
        let call = s
            .put(&Node::Call {
                func: "identity".into(),
                args: vec![n],
            })
            .unwrap();
        let f = function(
            &s,
            "use_id",
            vec![p("n", Type::Number, Confidence::Structural)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            call,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![id, f],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
    }

    #[test]
    fn a_generic_argument_conflict_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        // pair<T>(a: T, b: T) -> T
        let aref = s.put(&Node::Ref("a".into())).unwrap();
        let pair = s
            .put(&Node::Function {
                name: "pair".into(),
                type_params: vec!["T".into()],
                params: vec![
                    p("a", Type::Var("T".into()), Confidence::Structural),
                    p("b", Type::Var("T".into()), Confidence::Structural),
                ],
                produces: Produces {
                    ty: Type::Var("T".into()),
                    confidence: Confidence::Structural,
                },
                requires: BTreeSet::new(),
                on_failure: vec![],
                body: vec![],
                result: aref,
            })
            .unwrap();
        // g(n) = pair(n, n < n)  — T bound to Number then to Bool.
        let n1 = s.put(&Node::Ref("n".into())).unwrap();
        let n2 = s.put(&Node::Ref("n".into())).unwrap();
        let n3 = s.put(&Node::Ref("n".into())).unwrap();
        let cmp = s
            .put(&Node::BinOp {
                op: BinOp::Lt,
                lhs: n2,
                rhs: n3,
            })
            .unwrap();
        let call = s
            .put(&Node::Call {
                func: "pair".into(),
                args: vec![n1, cmp],
            })
            .unwrap();
        let g = function(
            &s,
            "g",
            vec![p("n", Type::Number, Confidence::Structural)],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            call,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![pair, g],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 2));
    }

    #[test]
    fn string_literal_and_str_len_typecheck() {
        let s = Store::open_in_memory().unwrap();
        // greet() -> String { yield "hello" }
        let hello = s.put(&Node::Str("hello".into())).unwrap();
        let greet = function(
            &s,
            "greet",
            vec![],
            produces(Type::String, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            hello,
        );
        // size() -> Number { yield str_len("hello") }
        let h2 = s.put(&Node::Str("hello".into())).unwrap();
        let sl = s.put(&Node::StrLen(h2)).unwrap();
        let size = function(
            &s,
            "size",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            sl,
        );
        let m = s
            .put(&Node::Module {
                name: "m".into(),
                types: vec![],
                functions: vec![greet, size],
            })
            .unwrap();
        let r = Checker::new(&s).check(&m).unwrap();
        assert!(r.ok(), "unexpected: {:?}", r.violations);
    }

    #[test]
    fn str_len_on_a_number_is_a_principle_2_violation() {
        let s = Store::open_in_memory().unwrap();
        let n = s.put(&Node::Lit(3)).unwrap();
        let sl = s.put(&Node::StrLen(n)).unwrap();
        let f = function(
            &s,
            "f",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            sl,
        );
        let r = Checker::new(&s).check(&f).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 2));
    }

    #[test]
    fn a_homogeneous_list_typechecks_and_a_mixed_one_does_not() {
        let s = Store::open_in_memory().unwrap();
        // ok: [1,2,3] -> List<Number>; list_get(...,0) -> Number
        let e0 = s.put(&Node::Lit(1)).unwrap();
        let e1 = s.put(&Node::Lit(2)).unwrap();
        let lst = s.put(&Node::List(vec![e0, e1])).unwrap();
        let idx = s.put(&Node::Lit(0)).unwrap();
        let g = s
            .put(&Node::ListGet {
                list: lst,
                index: idx,
            })
            .unwrap();
        let ok = function(
            &s,
            "ok",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            g,
        );
        assert!(Checker::new(&s).check(&ok).unwrap().ok());

        // bad: [1, "x"] -> P2 (mixed element types)
        let n = s.put(&Node::Lit(1)).unwrap();
        let t = s.put(&Node::Str("x".into())).unwrap();
        let mixed = s.put(&Node::List(vec![n, t])).unwrap();
        let len = s.put(&Node::ListLen(mixed)).unwrap();
        let bad = function(
            &s,
            "bad",
            vec![],
            produces(Type::Number, Confidence::Structural),
            BTreeSet::new(),
            vec![],
            vec![],
            len,
        );
        let r = Checker::new(&s).check(&bad).unwrap();
        assert!(r.violations.iter().any(|v| v.principle == 2));
    }
}