lex_types/checker/

mod.rs

//! M3: type checker. Walks the canonical AST, infers types via unification,
//! and checks declared signatures and effects.

use crate::builtins::{module_for_import, module_scope};
use crate::env::{TypeDefKind, TypeEnv, ty_from_canon_env};
use crate::error::{PositionedError, TypeError};
use crate::position::Position;
use crate::types::*;
use crate::unifier::{UnifyError, Unifier};
use indexmap::IndexMap;
use lex_ast as a;
use std::collections::{BTreeMap, HashMap};

mod exhaustive;
mod parse_strict;

pub use parse_strict::{rewrite_parse_calls, ParseSite};
use parse_strict::*;

/// Result of checking a whole program.
pub struct ProgramTypes {
    pub fn_signatures: IndexMap<String, Scheme>,
    pub type_env: TypeEnv,
    /// For #168: per-call required-fields map for `module.parse(s)`
    /// calls whose inferred result type is `Result[Record{...}, _]`.
    /// Keyed by the call's [`ParseSite`] (stage index + NodeId), so
    /// the table stays valid for any structurally identical copy of
    /// the checked stages (#777). Empty unless any matching call
    /// sites were found.
    ///
    /// See [`check_and_rewrite_program`] for the function that
    /// populates this and applies the rewrite in one step, and
    /// [`rewrite_parse_calls`] to apply it to a separate copy.
    pub parse_required_fields: HashMap<ParseSite, Vec<String>>,
    /// For #322: per-call type schema alongside the field names.
    /// Each entry is a `Vec<(field_name, type_tag)>` parallel to
    /// `parse_required_fields`. Used by the rewrite pass to inject
    /// the third argument to `parse_strict`.
    pub parse_type_schemas: HashMap<ParseSite, Vec<(String, String)>>,
}

/// Variant of [`check_program`] that stamps a source [`Position`]
/// onto every emitted error (#306 slice 1).
///
/// `positions` is keyed by function name and supplies the position
/// of each `fn` declaration in the source. Errors from a given
/// function are tagged with that function's position; errors that
/// don't map to a single function (e.g. type-decl-level errors)
/// keep `position = None`.
///
/// Slice 1 ships function-level granularity. Slice 1.5 will plumb
/// per-expression spans through canonicalize so deep-body errors
/// land on the offending sub-expression rather than its enclosing
/// function.
pub fn check_program_with_positions(
    stages: &[a::Stage],
    positions: &BTreeMap<String, Position>,
) -> Result<ProgramTypes, Vec<PositionedError>> {
    check_program_inner(stages, Some(positions), &BTreeMap::new(), &BTreeMap::new(), &BTreeMap::new())
        .map_err(|errs| errs.into_iter().map(|(e, fn_name)| {
            let pos = fn_name.as_deref().and_then(|n| positions.get(n)).cloned();
            PositionedError::new(e, pos)
        }).collect())
}

pub fn check_program(stages: &[a::Stage]) -> Result<ProgramTypes, Vec<TypeError>> {
    check_program_inner(stages, None, &BTreeMap::new(), &BTreeMap::new(), &BTreeMap::new())
        .map_err(|errs| errs.into_iter().map(|(e, _)| e).collect())
}

/// Like [`check_program`], but with a set of already-resolved dependency
/// modules the head may import by *reference* (e.g. `"lex-nt/lib"`). Each
/// value is that module's type — a [`Ty::Record`] of its exported
/// functions, the same shape [`crate::builtins::module_scope`] produces for
/// stdlib (build one with [`module_record_from_fields`]). Registry/git
/// dependencies resolve through this map instead of being inlined into
/// `stages` (#930): the op-log keeps the `import` edge and the write-time
/// gate supplies the dependency's signatures here, so the head still
/// type-checks against them without carrying their bodies.
///
/// An empty map reproduces [`check_program`] exactly — only stdlib imports
/// resolve, and any `<alias>.name` reaching an unsupplied dependency is an
/// unbound-reference error, as today.
pub fn check_program_with_modules(
    stages: &[a::Stage],
    modules: &BTreeMap<String, Ty>,
) -> Result<ProgramTypes, Vec<TypeError>> {
    check_program_inner(stages, None, modules, &BTreeMap::new(), &BTreeMap::new())
        .map_err(|errs| errs.into_iter().map(|(e, _)| e).collect())
}

/// Like [`check_program_with_modules`], but a dependency also contributes its
/// exported **type declarations** (#930 completeness gap): non-inlined
/// resolution otherwise carried only a dependency's function signatures, so a
/// package referencing a dependency's exported *type* (e.g. a record used in an
/// annotation, or its ADT constructors in a match) could not resolve it — the
/// type read as opaque, a matching record literal failed to unify, and field
/// access on it errored. `module_types` maps the same import *reference* keys as
/// `modules` to the dependency's type declarations (bare names); they are
/// registered under the importing file's alias (`<alias>.<Name>`), so
/// `<alias>.Type` annotations resolve and the dependency's constructors are in
/// scope — exactly as an inlined dependency's `type` decls used to be.
pub fn check_program_with_module_ifaces(
    stages: &[a::Stage],
    modules: &BTreeMap<String, Ty>,
    module_types: &BTreeMap<String, Vec<a::TypeDecl>>,
) -> Result<ProgramTypes, Vec<TypeError>> {
    check_program_inner(stages, None, modules, module_types, &BTreeMap::new())
        .map_err(|errs| errs.into_iter().map(|(e, _)| e).collect())
}

/// Like [`check_program_with_module_ifaces`], but each dependency import also
/// carries its **module mangle prefix** (#963), when the dependency was
/// resolved as a whole package. In that mode `module_types` are prefix-named
/// (`error_<hash>.DbErr`) and globally unique — registered as-is — and the
/// import alias is mapped to the prefix so an alias-qualified type reference
/// (`e.DbErr`) unfolds to the same type the dependency's own prefix-qualified
/// signatures name. This makes a directly-imported module and the copies of it
/// inlined into its sibling modules one type (the diamond). References with no
/// entry in `module_prefixes` keep the #930 bare/alias-qualified path.
pub fn check_program_with_deps(
    stages: &[a::Stage],
    modules: &BTreeMap<String, Ty>,
    module_types: &BTreeMap<String, Vec<a::TypeDecl>>,
    module_prefixes: &BTreeMap<String, String>,
) -> Result<ProgramTypes, Vec<TypeError>> {
    check_program_inner(stages, None, modules, module_types, module_prefixes)
        .map_err(|errs| errs.into_iter().map(|(e, _)| e).collect())
}

/// Build a dependency module's value type — a record of its exported
/// functions — from `(name, type)` pairs, for [`check_program_with_modules`]
/// (#930). Callers never touch the record representation directly.
///
/// The record is bound under an import alias and generalized *as a whole*
/// (Pass 1: `collect_vars`/`collect_eff_vars` over the record, then
/// `instantiate` per reference). Each export, however, was generalized
/// independently and so numbers its own variables from zero — two exports
/// of one dependency both spelling `Var(0)` would be tied together by that
/// whole-record generalization. So every export is renumbered into a
/// disjoint block: type variables from `0` up, effect-row variables from
/// [`EFF_VAR_BASE`] up (the same type/effect split stdlib's
/// [`crate::stdlib_spec::module_record`] keeps). Monomorphic exports (the
/// common case, e.g. `gcd(Int, Int) -> Int`) carry no variables and pass
/// through unchanged.
pub fn module_record_from_fields(fields: impl IntoIterator<Item = (String, Ty)>) -> Ty {
    let mut next_ty: u32 = 0;
    let mut next_eff: u32 = crate::stdlib_spec::EFF_VAR_BASE;
    let renumbered: IndexMap<String, Ty> = fields
        .into_iter()
        .map(|(name, ty)| (name, renumber_field_vars(&ty, &mut next_ty, &mut next_eff)))
        .collect();
    Ty::Record(renumbered)
}

/// Rewrite every type variable and effect-row variable in `ty` to a fresh
/// id drawn from the running counters, consistently within `ty`: a variable
/// used more than once stays one variable, but distinct variables get
/// distinct fresh ids, and no id is reused across separate calls (the
/// counters advance). See [`module_record_from_fields`].
fn renumber_field_vars(ty: &Ty, next_ty: &mut u32, next_eff: &mut u32) -> Ty {
    fn walk(
        t: &mut Ty,
        ty_map: &mut HashMap<u32, u32>,
        eff_map: &mut HashMap<u32, u32>,
        next_ty: &mut u32,
        next_eff: &mut u32,
    ) {
        match t {
            Ty::Var(v) => {
                let nv = *ty_map.entry(*v).or_insert_with(|| {
                    let x = *next_ty;
                    *next_ty += 1;
                    x
                });
                *v = nv;
            }
            Ty::Prim(_) | Ty::Unit | Ty::Never => {}
            Ty::List(inner) => walk(inner, ty_map, eff_map, next_ty, next_eff),
            Ty::Tuple(items) => {
                for it in items {
                    walk(it, ty_map, eff_map, next_ty, next_eff);
                }
            }
            Ty::Record(fs) => {
                for v in fs.values_mut() {
                    walk(v, ty_map, eff_map, next_ty, next_eff);
                }
            }
            Ty::Con(_, args) => {
                for a in args {
                    walk(a, ty_map, eff_map, next_ty, next_eff);
                }
            }
            Ty::Function { params, effects, ret } => {
                for p in params {
                    walk(p, ty_map, eff_map, next_ty, next_eff);
                }
                if let Some(v) = effects.var {
                    let nv = *eff_map.entry(v).or_insert_with(|| {
                        let x = *next_eff;
                        *next_eff += 1;
                        x
                    });
                    effects.var = Some(nv);
                }
                walk(ret, ty_map, eff_map, next_ty, next_eff);
            }
        }
    }
    let mut out = ty.clone();
    let mut ty_map: HashMap<u32, u32> = HashMap::new();
    let mut eff_map: HashMap<u32, u32> = HashMap::new();
    walk(&mut out, &mut ty_map, &mut eff_map, next_ty, next_eff);
    out
}

/// Register a dependency's exported type declarations under an import `alias`
/// (#930 completeness). Each declaration is registered under `<alias>.<Name>`,
/// and every reference *within* these declarations to a sibling dependency type
/// (a bare `Named` whose name is one of this dependency's own types) is
/// rewritten to the same qualified form, so the registered definitions stay
/// self-consistent inside the alias namespace. Constructors keep their bare
/// names — Lex's flat constructor namespace — and map to the qualified owning
/// type, exactly as an inlined dependency's `type` decls did.
fn register_dep_types(env: &mut TypeEnv, alias: &str, decls: &[a::TypeDecl]) {
    let own: std::collections::HashSet<&str> = decls.iter().map(|d| d.name.as_str()).collect();
    for d in decls {
        let mut def = d.definition.clone();
        qualify_type_expr(&mut def, alias, &own, &d.params);
        let qualified_name = format!("{alias}.{}", d.name);
        let qualified = a::TypeDecl {
            name: qualified_name.clone(),
            params: d.params.clone(),
            definition: def,
        };
        // The only error `add_user_type` raises is a recursive alias with no
        // constructor, which a well-formed published dependency never has;
        // dropping it here just leaves that (malformed) type unresolved.
        let _ = env.add_user_type(&qualified_name, qualified);
    }
}

/// Register a dependency package's exported type declarations when it was
/// resolved as a whole package (#963): the decls are already **prefix-named**
/// (`error_<hash>.DbErr`) and their internal references are prefix-qualified by
/// the loader, so they register as-is (globally unique — no alias
/// qualification). For each type belonging to *this* import's module (name
/// under `prefix`), an `<alias>.<Local>` alias entry is also registered so an
/// alias-qualified annotation unfolds to the canonical prefixed type — the same
/// type the module's own signatures name, and the same the copies inlined into
/// sibling modules carry. `decls` is the whole loaded package, so every type
/// the module's surface exposes resolves; re-registering across sibling imports
/// is idempotent (content-identical).
fn register_dep_types_prefixed(
    env: &mut TypeEnv,
    alias: &str,
    prefix: &str,
    decls: &[a::TypeDecl],
) {
    for d in decls {
        // Register the canonical, prefix-named type as-is (its internal
        // references are already prefix-qualified by the loader, and its name is
        // globally unique — no alias rewriting).
        let _ = env.add_user_type(&d.name, d.clone());
    }
    // Map this import's alias to the module prefix, so `ty_from_canon_env`
    // normalizes an alias-qualified annotation (`e.DbErr`) to the canonical
    // `error_<hash>.DbErr` — the same type the value record and inlined sibling
    // copies name.
    env.dep_alias_prefixes.insert(alias.to_string(), prefix.to_string());
}

/// Rewrite, in place, every `Named` reference in `t` that names one of the
/// dependency's `own` types (and isn't shadowed by a local type `param`) to its
/// `<alias>.`-qualified form. See [`register_dep_types`].
fn qualify_type_expr(
    t: &mut a::TypeExpr,
    alias: &str,
    own: &std::collections::HashSet<&str>,
    params: &[String],
) {
    let qualify = |name: &mut String| {
        if own.contains(name.as_str()) && !params.iter().any(|p| p == name) {
            *name = format!("{alias}.{name}");
        }
    };
    match t {
        a::TypeExpr::Named { name, args } => {
            qualify(name);
            for a_ in args {
                qualify_type_expr(a_, alias, own, params);
            }
        }
        a::TypeExpr::Record { fields } => {
            for f in fields {
                qualify_type_expr(&mut f.ty, alias, own, params);
            }
        }
        a::TypeExpr::Tuple { items } => {
            for it in items {
                qualify_type_expr(it, alias, own, params);
            }
        }
        a::TypeExpr::Function { params: ps, ret, .. } => {
            for p in ps {
                qualify_type_expr(p, alias, own, params);
            }
            qualify_type_expr(ret, alias, own, params);
        }
        a::TypeExpr::Union { variants } => {
            for v in variants {
                if let Some(p) = &mut v.payload {
                    qualify_type_expr(p, alias, own, params);
                }
            }
        }
        a::TypeExpr::RecordWithSpreads { spreads, fields } => {
            for s in spreads.iter_mut() {
                qualify(s);
            }
            for f in fields {
                qualify_type_expr(&mut f.ty, alias, own, params);
            }
        }
        a::TypeExpr::Refined { base, .. } => qualify_type_expr(base, alias, own, params),
    }
}

/// Return a copy of `ty` with every `Ty::Con(name, ..)` whose `name` is one of
/// the dependency's `own` type names rewritten to `<alias>.name` — so a
/// dependency's value-record signatures name the same qualified types that
/// [`register_dep_types`] registers. See the dep-import branch of
/// [`check_program_inner`].
fn qualify_ty_cons(ty: &Ty, alias: &str, own: &std::collections::HashSet<&str>) -> Ty {
    match ty {
        Ty::Con(name, args) => {
            let n = if own.contains(name.as_str()) {
                format!("{alias}.{name}")
            } else {
                name.clone()
            };
            Ty::Con(n, args.iter().map(|a| qualify_ty_cons(a, alias, own)).collect())
        }
        Ty::List(inner) => Ty::List(Box::new(qualify_ty_cons(inner, alias, own))),
        Ty::Tuple(items) => Ty::Tuple(items.iter().map(|a| qualify_ty_cons(a, alias, own)).collect()),
        Ty::Record(fs) => Ty::Record(
            fs.iter().map(|(k, v)| (k.clone(), qualify_ty_cons(v, alias, own))).collect(),
        ),
        Ty::Function { params, effects, ret } => Ty::Function {
            params: params.iter().map(|a| qualify_ty_cons(a, alias, own)).collect(),
            effects: effects.clone(),
            ret: Box::new(qualify_ty_cons(ret, alias, own)),
        },
        Ty::Var(_) | Ty::Prim(_) | Ty::Unit | Ty::Never => ty.clone(),
    }
}

fn check_program_inner(
    stages: &[a::Stage],
    _positions: Option<&BTreeMap<String, Position>>,
    modules: &BTreeMap<String, Ty>,
    module_types: &BTreeMap<String, Vec<a::TypeDecl>>,
    module_prefixes: &BTreeMap<String, String>,
) -> Result<ProgramTypes, Vec<(TypeError, Option<String>)>> {
    let mut tcx = Checker::new();
    // Each entry is (error, optional fn name the error came from)
    // so callers can resolve the error to a source position.
    let mut errors: Vec<(TypeError, Option<String>)> = Vec::new();

    // Pass 1: gather imports → bring module values into scope.
    for stage in stages {
        if let a::Stage::Import(i) = stage {
            // Stdlib modules resolve to a built-in scope.
            if let Some(mod_name) = module_for_import(&i.reference) {
                if let Some(ty) = module_scope(mod_name, &tcx.type_env) {
                    tcx.globals.insert(i.alias.clone(), Scheme {
                        // Module-level signatures use Var(0..n) and
                        // effect-vars on stdlib HOFs (list.map's `[E]`
                        // etc.); generalize both.
                        vars: collect_vars(&ty),
                        eff_vars: collect_eff_vars(&ty),
                        ty,
                    });
                    tcx.module_aliases.insert(i.alias.clone(), mod_name.to_string());
                    continue;
                }
            }
            // #930: a resolved registry/git dependency, supplied by the
            // caller (the write-time gate) keyed by import reference,
            // rather than inlined into `stages`. Bind its record under this
            // file's alias so `<alias>.name` references type-check with the
            // dependency's signatures but without its bodies present. The
            // record is already generalized per export, so generalize it as
            // a whole the same way a stdlib module scope is bound above.
            // #963 prefixed mode: the dependency was resolved as a whole
            // package, so `module_types` are prefix-named (`error_<hash>.DbErr`)
            // and the value record already references them by prefix — register
            // the decls as-is and map this import's alias to the module prefix
            // so an alias-qualified annotation (`e.DbErr`) unfolds to the same
            // canonical type. A reference with no prefix keeps the #930 bare /
            // alias-qualified path.
            match module_prefixes.get(&i.reference) {
                Some(prefix) => {
                    if let Some(ty) = modules.get(&i.reference) {
                        tcx.globals.insert(i.alias.clone(), Scheme {
                            vars: collect_vars(ty),
                            eff_vars: collect_eff_vars(ty),
                            ty: ty.clone(),
                        });
                    }
                    if let Some(decls) = module_types.get(&i.reference) {
                        register_dep_types_prefixed(&mut tcx.type_env, &i.alias, prefix, decls);
                    }
                }
                None => {
                    // #930 completeness (bare mode): the dependency's exported
                    // type names, so both its value-record signatures and its
                    // own `type` decls are rewritten to the alias namespace
                    // consistently (a dependency fn `make() -> Rec` and the
                    // registered `<alias>.Rec` must name the same type).
                    let own: std::collections::HashSet<&str> = module_types
                        .get(&i.reference)
                        .map(|ds| ds.iter().map(|d| d.name.as_str()).collect())
                        .unwrap_or_default();
                    if let Some(ty) = modules.get(&i.reference) {
                        let ty = qualify_ty_cons(ty, &i.alias, &own);
                        tcx.globals.insert(i.alias.clone(), Scheme {
                            vars: collect_vars(&ty),
                            eff_vars: collect_eff_vars(&ty),
                            ty,
                        });
                    }
                    if let Some(decls) = module_types.get(&i.reference) {
                        register_dep_types(&mut tcx.type_env, &i.alias, decls);
                    }
                }
            }
        }
    }

    // Pass 2: register user-declared types.
    for stage in stages {
        if let a::Stage::TypeDecl(td) = stage {
            if let Err(e) = tcx.type_env.add_user_type(&td.name, td.clone()) {
                errors.push((TypeError::RecursiveTypeWithoutConstructor {
                    at_node: "n_0".into(),
                    name: e,
                }, None));
            }
        }
    }

    // Pass 3: register fn signatures (so mutual recursion works).
    for stage in stages {
        if let a::Stage::FnDecl(fd) = stage {
            let scheme = function_scheme(fd, &tcx.type_env);
            tcx.globals.insert(fd.name.clone(), scheme);
            // #209 slice 2: keep the original params so call-site
            // refinement discharge can see the predicate before it
            // gets stripped to its base type by `ty_from_canon`.
            tcx.fn_params.insert(fd.name.clone(), fd.params.clone());
        }
    }

    // Pass 4: check each fn body. With #306 slice 1, every emitted
    // error is paired with the source fn it came from so the public
    // [`check_program_with_positions`] wrapper can stamp the
    // function's source position onto a [`PositionedError`].
    let mut signatures = IndexMap::new();
    // #777: the parse-call side tables are keyed by (stage index,
    // NodeId) rather than by expression address, so each FnDecl's
    // NodeId map is computed up front. The walk is skipped entirely
    // when no import could produce a rewritable call.
    let wants_parse_sites = tcx.has_parse_capable_imports();
    for (stage_idx, stage) in stages.iter().enumerate() {
        if let a::Stage::FnDecl(fd) = stage {
            tcx.stage_ids = if wants_parse_sites {
                Some((stage_idx, a::expr_ids(stage)))
            } else {
                None
            };
            match tcx.check_fn(fd) {
                Ok(scheme) => { signatures.insert(fd.name.clone(), scheme); }
                Err(es) => {
                    errors.extend(es.into_iter().map(|e| (e, Some(fd.name.clone()))));
                }
            }
        }
    }
    tcx.stage_ids = None;

    if errors.is_empty() {
        // #168: walk pending parse-call records and resolve each
        // call's return type now that all unification has settled.
        // A call shows up here only if the call site syntactically
        // looks like `<alias>.parse(s)` for an alias bound to one
        // of {json, toml, yaml} via the import pass.
        let mut parse_required_fields = HashMap::new();
        let mut parse_type_schemas = HashMap::new();
        for (site, ret_ty) in &tcx.pending_parse_calls {
            if let Some((fields, schema)) = extract_record_fields_and_schema(&tcx.u, &tcx.type_env, ret_ty) {
                parse_required_fields.insert(site.clone(), fields);
                parse_type_schemas.insert(site.clone(), schema);
            }
        }
        Ok(ProgramTypes {
            fn_signatures: signatures,
            type_env: tcx.type_env,
            parse_required_fields,
            parse_type_schemas,
        })
    } else {
        Err(errors)
    }
}

/// Type-check `stages` and rewrite every `module.parse(s)` call
/// where the inferred T is a Record into the equivalent
/// `module.parse_strict(s, [field_names])` (#168). Existing
/// [`check_program`] keeps the old immutable signature for tests
/// and tools that don't want the AST rewritten.
pub fn check_and_rewrite_program(
    stages: &mut [a::Stage],
) -> Result<ProgramTypes, Vec<TypeError>> {
    check_and_rewrite_program_with_modules(stages, &BTreeMap::new())
}

/// Like [`check_and_rewrite_program`], but resolving external dependency
/// references through `modules` (#930) — the publish path checks the same
/// non-inlined head its store gate will, so the two agree.
pub fn check_and_rewrite_program_with_modules(
    stages: &mut [a::Stage],
    modules: &BTreeMap<String, Ty>,
) -> Result<ProgramTypes, Vec<TypeError>> {
    let pt = check_program_with_modules(&*stages, modules)?;
    rewrite_parse_calls(stages, &pt);
    Ok(pt)
}

/// Like [`check_and_rewrite_program_with_modules`], but a dependency also
/// contributes its exported type declarations (#930 completeness — see
/// [`check_program_with_module_ifaces`]).
pub fn check_and_rewrite_program_with_module_ifaces(
    stages: &mut [a::Stage],
    modules: &BTreeMap<String, Ty>,
    module_types: &BTreeMap<String, Vec<a::TypeDecl>>,
) -> Result<ProgramTypes, Vec<TypeError>> {
    let pt = check_program_with_module_ifaces(&*stages, modules, module_types)?;
    rewrite_parse_calls(stages, &pt);
    Ok(pt)
}

/// Like [`check_and_rewrite_program_with_module_ifaces`], but each dependency
/// import also carries its module mangle prefix (#963 — see
/// [`check_program_with_deps`]).
pub fn check_and_rewrite_program_with_deps(
    stages: &mut [a::Stage],
    modules: &BTreeMap<String, Ty>,
    module_types: &BTreeMap<String, Vec<a::TypeDecl>>,
    module_prefixes: &BTreeMap<String, String>,
) -> Result<ProgramTypes, Vec<TypeError>> {
    let pt = check_program_with_deps(&*stages, modules, module_types, module_prefixes)?;
    rewrite_parse_calls(stages, &pt);
    Ok(pt)
}

/// `parse` → `parse_strict_typed` / `json_body` → `json_body_typed`
/// (#168, `parse_strict.rs`) are synthesized onto an AST that has
/// already been checked once — `rewrite_parse_calls` mutates a
/// call's callee field name and appends two arguments, producing a
/// call that the module's literal Lex-level record type has no
/// field for (the `_typed` variants are native ops dispatched by
/// name in `lex-runtime`'s `builtins.rs`, not declared Lex members).
/// Re-checking those already-rewritten stages — as lex-store's
/// write-time publish gate does on the same stages its caller just
/// ran `check_and_rewrite_program` over — must accept the field
/// rather than report it unknown. The synthesized signature is
/// derived from the original field's rather than hardcoded, so it
/// stays in sync with any future change to the base op's shape:
/// same params (plus the two extra `List` arguments the rewrite
/// always appends) and the same effects and return type.
fn synthesize_decode_typed_field(field: &str, fields: &IndexMap<String, Ty>) -> Option<Ty> {
    let base_field = match field {
        "parse_strict_typed" => "parse",
        "json_body_typed" => "json_body",
        _ => return None,
    };
    let Ty::Function { params, effects, ret } = fields.get(base_field)? else {
        return None;
    };
    let mut synthesized_params = params.clone();
    synthesized_params.push(Ty::List(Box::new(Ty::Prim(Prim::Str))));
    synthesized_params.push(Ty::List(Box::new(Ty::Tuple(vec![
        Ty::Prim(Prim::Str),
        Ty::Prim(Prim::Str),
    ]))));
    Some(Ty::Function {
        params: synthesized_params,
        effects: effects.clone(),
        ret: ret.clone(),
    })
}

fn collect_vars(t: &Ty) -> Vec<TyVarId> {
    let mut out = Vec::new();
    fn walk(t: &Ty, out: &mut Vec<TyVarId>) {
        match t {
            Ty::Var(v) => { if !out.contains(v) { out.push(*v); } }
            Ty::Prim(_) | Ty::Unit | Ty::Never => {}
            Ty::List(inner) => walk(inner, out),
            Ty::Tuple(items) => for it in items { walk(it, out); },
            Ty::Record(fs) => for v in fs.values() { walk(v, out); },
            Ty::Con(_, args) => for a in args { walk(a, out); },
            Ty::Function { params, ret, .. } => {
                for p in params { walk(p, out); }
                walk(ret, out);
            }
        }
    }
    walk(t, &mut out);
    out
}

/// Walk a type and collect every effect-row variable id that appears
/// inside any function-type's effect set. Used to generalize stdlib
/// HOF schemes alongside ordinary type vars.
fn collect_eff_vars(t: &Ty) -> Vec<u32> {
    let mut out = Vec::new();
    fn walk(t: &Ty, out: &mut Vec<u32>) {
        match t {
            Ty::Var(_) | Ty::Prim(_) | Ty::Unit | Ty::Never => {}
            Ty::List(inner) => walk(inner, out),
            Ty::Tuple(items) => for it in items { walk(it, out); },
            Ty::Record(fs) => for v in fs.values() { walk(v, out); },
            Ty::Con(_, args) => for a in args { walk(a, out); },
            Ty::Function { params, effects, ret } => {
                if let Some(v) = effects.var {
                    if !out.contains(&v) { out.push(v); }
                }
                for p in params { walk(p, out); }
                walk(ret, out);
            }
        }
    }
    walk(t, &mut out);
    out
}

fn function_scheme(fd: &a::FnDecl, env: &TypeEnv) -> Scheme {
    // Collect type-param ids in order; map their names to fresh Var(idx).
    let params: Vec<Ty> = fd.params.iter().map(|p| ty_from_canon_env(&p.ty, &fd.type_params, env)).collect();
    let ret = ty_from_canon_env(&fd.return_type, &fd.type_params, env);
    // Plumb effect args (#207). A canonical-AST `EffectDecl` already
    // carries `Option<EffectArg>`; map it into the type-system kind so
    // subsumption can honor parameterized effects.
    let effects = EffectSet {
        concrete: {
            let mut s = std::collections::BTreeSet::new();
            for e in &fd.effects {
                let arg = e.arg.as_ref().map(|a| match a {
                    a::EffectArg::Str { value } => crate::types::EffectArg::Str(value.clone()),
                    a::EffectArg::Int { value } => crate::types::EffectArg::Int(*value),
                    a::EffectArg::Ident { value } => crate::types::EffectArg::Ident(value.clone()),
                });
                s.insert(crate::types::EffectKind { name: e.name.clone(), arg });
            }
            s
        },
        // Open-row tail on the function's own declared row: `-> [io | E] T`.
        // Resolve `E` to its `type_params` index (shared id space with the
        // type-var numbering; read back via the effect-subst map, so no
        // collision with a same-indexed type param).
        var: fd.effect_row_var
            .as_ref()
            .and_then(|n| fd.type_params.iter().position(|p| p == n))
            .map(|i| i as u32),
    };
    let ty = Ty::Function { params, effects, ret: Box::new(ret) };
    let vars: Vec<TyVarId> = (0..fd.type_params.len() as u32).collect();
    // Generalize over any effect-row variable in the signature — a
    // row-polymorphic parameter (`(Int) -> [io | E] Int`, like the stdlib
    // HOFs) or the function's own open row (`-> [io | E] T`). Each is
    // freshened per call site by `instantiate`, then bound to the caller's
    // actual effects by `unify_effects`. Closed rows collect nothing, so
    // their checking is unchanged.
    let eff_vars = collect_eff_vars(&ty);
    Scheme { vars, eff_vars, ty }
}

struct Checker {
    u: Unifier,
    type_env: TypeEnv,
    globals: IndexMap<String, Scheme>,
    /// Imported alias → canonical module name (e.g. `cfg` → `toml`).
    /// Populated during the import pass; consulted by `check_call`
    /// to recognise `cfg.parse(...)` as a stdlib parse call.
    module_aliases: IndexMap<String, String>,
    /// For #168: every `<alias>.parse(s)` call where alias is in
    /// `module_aliases` and maps to {json, toml, yaml} (or
    /// `http.json_body`, #684), recorded here as
    /// `(call_site, return_type_var)`. After the whole program
    /// type-checks, we walk this and resolve each return type
    /// through the unifier — at that point any `Result[Manifest, _]`
    /// constraints from match patterns or let-annotations have
    /// settled.
    pending_parse_calls: Vec<(ParseSite, Ty)>,
    /// #777: NodeId map for the FnDecl stage currently being checked,
    /// `(stage index, &CExpr address → NodeId)`. Set by
    /// `check_program_inner` before each `check_fn` when the program
    /// imports a decode-capable module, `None` otherwise. Used only to
    /// translate a parse call's address into a stable [`ParseSite`].
    stage_ids: Option<(usize, HashMap<*const a::CExpr, a::NodeId>)>,
    /// Per-function param list, retained so call-site discharge can
    /// see refinement predicates (#209 slice 2). The main `globals`
    /// scheme strips refinements (`Refined` unifies as its base);
    /// this side-table keeps the pre-stripped `TypeExpr` available
    /// for static discharge of literal arguments.
    fn_params: IndexMap<String, Vec<a::Param>>,
    /// Errors recovered from independent sub-expressions within a
    /// function body (discarded `Block` statements, `Let` binding
    /// values) so a single `lex check` run surfaces every independent
    /// error instead of stopping at the first (#566). Drained by
    /// `check_fn` after each body/example check.
    recovered_errors: Vec<TypeError>,
    /// Effect-row variables in scope for the function currently being
    /// checked: surface name (e.g. `E`) → the instantiated fresh effect-var
    /// id allocated for it. Lets a row-polymorphic *lambda* inside the body
    /// (`fn (r) -> [io | E] R { ... }`) resolve its tail `E` to the same id
    /// as the enclosing function's signature, so effects flow through the
    /// closure (e.g. into `net.serve_fn`) instead of being silently dropped.
    /// Empty for closed-row functions.
    eff_row_scope: IndexMap<String, u32>,
}

impl Checker {
    fn new() -> Self {
        Self {
            u: Unifier::new(),
            type_env: TypeEnv::new_with_builtins(),
            globals: IndexMap::new(),
            module_aliases: IndexMap::new(),
            pending_parse_calls: Vec::new(),
            stage_ids: None,
            fn_params: IndexMap::new(),
            recovered_errors: Vec::new(),
            eff_row_scope: IndexMap::new(),
        }
    }

    /// Check an independent sub-expression but, on error, record it and
    /// continue with a fresh type variable rather than aborting the whole
    /// body. Used for positions whose result type does not flow into a
    /// strict constraint — a discarded `Block` statement, or a `Let`
    /// binding's value — so `check_fn` can surface every independent error
    /// in one pass (#566). A fresh var unifies with anything, so recovery
    /// does not manufacture spurious follow-on mismatches.
    fn check_expr_recover(
        &mut self,
        e: &a::CExpr,
        node_id: &str,
        locals: &mut IndexMap<String, Ty>,
        effs: &mut EffectSet,
    ) -> Ty {
        match self.check_expr(e, node_id, locals, effs) {
            Ok(ty) => ty,
            Err(err) => {
                self.recovered_errors.push(err);
                self.u.fresh()
            }
        }
    }

    /// If `ty` is a `Ty::Con(name, args)` whose definition is a type
    /// alias (record or otherwise), return the aliased type with the
    /// alias's formal parameters substituted by `args`. For zero-arg
    /// aliases this is the identity substitution. For parametric
    /// aliases (#439, e.g. `type Box[T] = { value :: T }`), the
    /// formal `Ty::Var(i)` for the i-th param is replaced by `args[i]`
    /// so `Box[Str]` unfolds to `{ value :: Str }` rather than to the
    /// unsubstituted body. Returns `ty` unchanged when arity doesn't
    /// match or the name doesn't resolve to an alias.
    fn unfold_record_alias(&self, ty: Ty) -> Ty {
        if let Ty::Con(ref n, ref args) = ty {
            if let Some(td) = self.type_env.types.get(n) {
                if let TypeDefKind::Alias(inner) = &td.kind {
                    if td.params.len() != args.len() {
                        return ty;
                    }
                    if td.params.is_empty() {
                        return inner.clone();
                    }
                    let mut subst = IndexMap::new();
                    for (i, a) in args.iter().enumerate() {
                        subst.insert(i as u32, a.clone());
                    }
                    return subst_vars(inner, &subst, &IndexMap::new());
                }
            }
        }
        ty
    }

    /// True iff `ty` is a `Ty::Con(name, args)` whose definition is a
    /// `TypeDefKind::Alias` and whose arity matches. Used by
    /// `unify_coerce_inner` to detect the case where both sides are
    /// nominal aliases and unfolding would collapse the nominal
    /// distinction (#323 / #439). For parametric aliases the arity
    /// match guards against `Box[Str]` vs an inconsistent `Box[Str, Int]`.
    fn is_alias_con(&self, ty: &Ty) -> bool {
        if let Ty::Con(name, args) = ty {
            if let Some(td) = self.type_env.types.get(name) {
                if matches!(td.kind, TypeDefKind::Alias(_))
                    && td.params.len() == args.len()
                {
                    return true;
                }
            }
        }
        false
    }

    /// Unify two types, asymmetrically coercing an anonymous record
    /// against a nominal record alias at any level of nesting. So a
    /// `{ x: 1, y: 2 }` literal can be passed to a fn taking
    /// `Inner = { x :: Int, y :: Int }`, even when the literal is the
    /// inner field of an outer record literal.
    ///
    /// We deliberately keep nominal-vs-nominal mismatches strict: two
    /// distinct `Ty::Con` names won't unify just because their record
    /// shapes match. The coercion fires only when one side is a bare
    /// `Ty::Record` and the other is a `Ty::Con` whose alias is a
    /// record.
    fn unify_with_record_coercion(&mut self, a: &Ty, b: &Ty) -> Result<(), UnifyError> {
        let a = self.u.resolve(a);
        let b = self.u.resolve(b);
        self.unify_coerce_inner(a, b)
    }

    fn unify_coerce_inner(&mut self, a: Ty, b: Ty) -> Result<(), UnifyError> {
        // #323: alias unfolding. If exactly one side is an `alias-Con`
        // — a 0-arg `Ty::Con(name, [])` whose definition is a type
        // alias (Record or non-record) — unfold both sides so the
        // structural cases below can match (`Errors` ↔ `List[…]`,
        // `Path` ↔ `Tuple(…)`, `Maybe` ↔ `Option[…]`,
        // `UserId` ↔ `Int`, …).
        //
        // Three cases intentionally bypass unfolding:
        //
        // - **Same-named Cons** (`Test` vs `Test`): preserve nominal
        //   identity. The Con-Con same-name case below recurses on
        //   args; eager unfold here would force the nominal name
        //   to evaporate, breaking unifications elsewhere that
        //   still see the nominal `Con`.
        // - **Var on either side**: don't unfold against an unbound
        //   variable, because the plain unifier would bind the var
        //   to the unfolded shape and lose the nominal name. The
        //   var binds to the nominal `Con` instead, and later
        //   unifications against concrete shapes re-enter this
        //   function and unfold then.
        // - **Two distinct alias-Cons** (`Apple` vs `Box`, both
        //   declared as record aliases with identical shapes):
        //   preserve nominal distinction between aliases. Unfolding
        //   both would collapse the test of "same shape, different
        //   names" into "same shape" and erase the names.
        let (a, b) = match (&a, &b) {
            (Ty::Con(n1, _), Ty::Con(n2, _)) if n1 == n2 => (a, b),
            (Ty::Var(_), _) | (_, Ty::Var(_)) => (a, b),
            (Ty::Con(_, _), Ty::Con(_, _))
                if self.is_alias_con(&a) && self.is_alias_con(&b) =>
            {
                (a, b)
            }
            _ => {
                let a_u = if let Ty::Con(_, _) = &a {
                    self.unfold_record_alias(a.clone())
                } else {
                    a
                };
                let b_u = if let Ty::Con(_, _) = &b {
                    self.unfold_record_alias(b.clone())
                } else {
                    b
                };
                (a_u, b_u)
            }
        };

        match (&a, &b) {
            (Ty::Record(fa), Ty::Record(fb)) => {
                if fa.len() != fb.len() {
                    return Err(UnifyError::Mismatch { a: a.clone(), b: b.clone() });
                }
                for (k, va) in fa.clone() {
                    match fb.get(&k) {
                        Some(vb) => self.unify_coerce_inner(va, vb.clone())?,
                        None => return Err(UnifyError::Mismatch { a: a.clone(), b: b.clone() }),
                    }
                }
                Ok(())
            }
            (Ty::List(ta), Ty::List(tb)) => {
                self.unify_coerce_inner((**ta).clone(), (**tb).clone())
            }
            (Ty::Tuple(xs), Ty::Tuple(ys)) if xs.len() == ys.len() => {
                for (x, y) in xs.clone().into_iter().zip(ys.clone()) {
                    self.unify_coerce_inner(x, y)?;
                }
                Ok(())
            }
            // Recurse into Con-Con pairs so record-alias coercion reaches
            // arbitrary nesting depth (e.g. Result[T, MyAlias]) (#328).
            (Ty::Con(n1, a1), Ty::Con(n2, a2)) if n1 == n2 && a1.len() == a2.len() => {
                for (x, y) in a1.clone().into_iter().zip(a2.clone()) {
                    self.unify_coerce_inner(x, y)?;
                }
                Ok(())
            }
            // #345: recurse into Function types so alias coercion fires on
            // closure params / return types. Without this, a closure annotated
            // `(Errors, Errors) -> Errors` fails to unify with the expected
            // `(List[?n], ?m) -> List[?n]` even though `Errors = List[Error]`.
            (Ty::Function { params: pa, effects: ea, ret: ra },
             Ty::Function { params: pb, effects: eb, ret: rb })
            if pa.len() == pb.len() => {
                for (x, y) in pa.clone().into_iter().zip(pb.clone()) {
                    self.unify_coerce_inner(x, y)?;
                }
                // Propagate the EffectMismatch verbatim (rather than
                // collapsing it into a whole-type Mismatch) so the
                // invariant-effect-row case surfaces as its own
                // rule_tag with the narrow-the-body fix (#565).
                self.u.unify_effects(ea, eb)?;
                self.unify_coerce_inner((**ra).clone(), (**rb).clone())
            }
            _ => self.u.unify(&a, &b),
        }
    }

    fn check_fn(&mut self, fd: &a::FnDecl) -> Result<Scheme, Vec<TypeError>> {
        // Instantiate fn's signature with fresh vars for its type params.
        let scheme = function_scheme(fd, &self.type_env);
        let (inst_ty, eff_subst) = instantiate_with_eff(&scheme, &mut self.u);
        let (param_tys, declared_effects, ret_ty) = match inst_ty {
            Ty::Function { params, effects, ret } => (params, effects, *ret),
            _ => unreachable!(),
        };

        // Map this function's surface row-variable names to their freshly
        // instantiated effect-var ids, so a row-polymorphic lambda in the
        // body can join the enclosing row (see `eff_row_scope`). A type
        // param at index `i` is a row var iff `i` was generalized as an
        // effect var (`scheme.eff_vars`) and thus appears in `eff_subst`.
        let saved_scope = std::mem::take(&mut self.eff_row_scope);
        for (i, name) in fd.type_params.iter().enumerate() {
            if let Some(fresh) = eff_subst.get(&(i as u32)) {
                self.eff_row_scope.insert(name.clone(), *fresh);
            }
        }

        let mut locals: IndexMap<String, Ty> = IndexMap::new();
        for (p, t) in fd.params.iter().zip(param_tys.iter()) {
            locals.insert(p.name.clone(), t.clone());
        }

        // Accumulate all errors within this function rather than returning on the
        // first one (#566). Body errors and example errors are independent — an
        // agent can fix both in one pass instead of running lex check repeatedly.
        let mut errors: Vec<TypeError> = Vec::new();
        let mut inferred_effects = EffectSet::empty();

        // Check body. Save the error but continue to example checking.
        let body_ok = match self.check_expr(&fd.body, "n_0", &mut locals, &mut inferred_effects) {
            Ok(body_ty) => {
                // The body may produce an anonymous record literal where the
                // signature expects a nominal record alias (and vice-versa,
                // and at any nested level). `unify_with_record_coercion`
                // handles that asymmetry while keeping nominal-vs-nominal
                // mismatches strict.
                if let Err(e) = self.unify_with_record_coercion(&body_ty, &ret_ty) {
                    errors.push(mismatch_err("n_0", e, &self.u, vec![format!("in function `{}`", fd.name)]));
                    false
                } else {
                    true
                }
            }
            Err(e) => { errors.push(e); false }
        };

        // Surface errors recovered from independent positions in the body
        // (discarded `Block` statements, `Let` values) so every independent
        // error is reported in one pass (#566), not just the first.
        let body_had_recovered = !self.recovered_errors.is_empty();
        errors.append(&mut self.recovered_errors);

        // Skip the effect-not-declared check when the body had recovered
        // errors: effect inference is incomplete (recovered sub-exprs became
        // fresh vars that contribute no effects), so a missing/extra effect
        // would be misleading noise next to the real errors.
        if body_ok && !body_had_recovered && !inferred_effects.is_subset(&declared_effects) {
            for e in inferred_effects.concrete.iter() {
                if !declared_effects.concrete.iter().any(|d| d.subsumes(e)) {
                    errors.push(TypeError::EffectNotDeclared {
                        at_node: "n_0".into(),
                        effect: e.pretty(),
                    });
                    break;
                }
            }
        }

        // #369: signature-level examples. Pure-only in v1; arg arity
        // must match params; each arg type-checks against its param,
        // each expected type-checks against the return type.
        // Check all examples regardless of body success (#566).
        if !fd.examples.is_empty() {
            if !declared_effects.concrete.is_empty() {
                errors.push(TypeError::ExamplesOnEffectfulFn {
                    at_node: "n_0".into(),
                    fn_name: fd.name.clone(),
                });
            } else {
                for (case_index, ex) in fd.examples.iter().enumerate() {
                    if ex.args.len() != param_tys.len() {
                        errors.push(TypeError::ExampleArityMismatch {
                            at_node: "n_0".into(),
                            fn_name: fd.name.clone(),
                            case_index,
                            expected: param_tys.len(),
                            got: ex.args.len(),
                        });
                        continue;
                    }
                    let mut example_locals: IndexMap<String, Ty> = IndexMap::new();
                    let mut example_effects = EffectSet::empty();
                    let mut args_ok = true;
                    for (i, (arg, expected_ty)) in
                        ex.args.iter().zip(param_tys.iter()).enumerate()
                    {
                        match self.check_expr(arg, "n_0", &mut example_locals, &mut example_effects) {
                            Ok(arg_ty) => {
                                if let Err(e) = self.unify_with_record_coercion(&arg_ty, expected_ty) {
                                    errors.push(mismatch_err(
                                        "n_0", e, &self.u,
                                        vec![format!("in example #{} for `{}`, argument {}", case_index + 1, fd.name, i + 1)],
                                    ));
                                    args_ok = false;
                                }
                            }
                            Err(e) => { errors.push(e); args_ok = false; }
                        }
                    }
                    if args_ok {
                        match self.check_expr(&ex.expected, "n_0", &mut example_locals, &mut example_effects) {
                            Ok(expected_ty) => {
                                if let Err(e) = self.unify_with_record_coercion(&expected_ty, &ret_ty) {
                                    errors.push(mismatch_err(
                                        "n_0", e, &self.u,
                                        vec![format!("in example #{} for `{}`, expected value", case_index + 1, fd.name)],
                                    ));
                                }
                            }
                            Err(e) => errors.push(e),
                        }
                    }
                    // The example's args/expected are expected to be pure
                    // by construction (literals in the common case); if
                    // they invoked effects, they'd break the pure-only
                    // discipline. Reject the first one via the same effect rule.
                    if let Some(e) = example_effects.concrete.iter().next() {
                        errors.push(TypeError::EffectNotDeclared {
                            at_node: "n_0".into(),
                            effect: e.pretty(),
                        });
                    }
                }
            }
        }

        // Catch any errors recovered while checking example sub-expressions.
        errors.append(&mut self.recovered_errors);
        // Restore the enclosing function's row-var scope (functions are
        // checked one at a time, so this is just defensive symmetry).
        self.eff_row_scope = saved_scope;
        if errors.is_empty() { Ok(scheme) } else { Err(errors) }
    }

    fn check_expr(
        &mut self,
        e: &a::CExpr,
        node_id: &str,
        locals: &mut IndexMap<String, Ty>,
        effs: &mut EffectSet,
    ) -> Result<Ty, TypeError> {
        match e {
            a::CExpr::Literal { value } => Ok(lit_type(value)),
            a::CExpr::Var { name } => {
                if let Some(t) = locals.get(name) {
                    return Ok(t.clone());
                }
                if let Some(scheme) = self.globals.get(name).cloned() {
                    return Ok(instantiate(&scheme, &mut self.u));
                }
                Err(TypeError::UnknownIdentifier { at_node: node_id.into(), name: name.clone() })
            }
            a::CExpr::Constructor { name, args } => self.check_constructor(name, args, node_id, locals, effs),
            a::CExpr::Call { callee, args } => self.check_call(e, callee, args, node_id, locals, effs),
            a::CExpr::Let { name, ty, value, body } => {
                // Recover if the bound value fails to check: record the error
                // and bind the name to a fresh var so the `let` body (which
                // may hold further independent errors) is still checked (#566).
                let v_ty = self.check_expr_recover(value, node_id, locals, effs);
                if let Some(declared) = ty {
                    let d = ty_from_canon_env(declared, &[], &self.type_env);
                    if let Err(err) = self.unify_with_record_coercion(&v_ty, &d) {
                        return Err(mismatch_err(node_id, err, &self.u, vec![format!("in let `{}`", name)]));
                    }
                }
                let prev = locals.insert(name.clone(), v_ty);
                let body_ty = self.check_expr(body, node_id, locals, effs)?;
                match prev {
                    Some(p) => { locals.insert(name.clone(), p); }
                    None => { locals.shift_remove(name); }
                }
                Ok(body_ty)
            }
            a::CExpr::Match { scrutinee, arms } => {
                let scrut_ty = self.check_expr(scrutinee, node_id, locals, effs)?;
                if arms.is_empty() {
                    return Err(TypeError::NonExhaustiveMatch {
                        at_node: node_id.into(), missing: vec!["_".into()]
                    });
                }
                let result_ty = self.u.fresh();
                for arm in arms {
                    let mut arm_locals = locals.clone();
                    self.bind_pattern(&arm.pattern, &scrut_ty, &mut arm_locals, node_id)?;
                    let arm_ty = self.check_expr(&arm.body, node_id, &mut arm_locals, effs)?;
                    if let Err(err) = self.unify_with_record_coercion(&arm_ty, &result_ty) {
                        return Err(mismatch_err(node_id, err, &self.u, vec!["in match arm".into()]));
                    }
                }
                // Exhaustiveness (#766). Runs after every arm has been
                // bound so the scrutinee's type is as resolved as it is
                // going to get (a constructor pattern against a type
                // variable pins the variable to its union).
                let rows: Vec<Vec<a::Pattern>> = arms.iter().map(|arm| vec![arm.pattern.clone()]).collect();
                if let Some(witnesses) = self.missing_patterns(&rows, std::slice::from_ref(&scrut_ty)) {
                    return Err(TypeError::NonExhaustiveMatch {
                        at_node: node_id.into(),
                        missing: witnesses.into_iter().map(|w| w.join(", ")).collect(),
                    });
                }
                Ok(result_ty)
            }
            a::CExpr::Block { statements, result } => {
                // Each statement's value is discarded, so an error in one
                // doesn't feed a later type — recover and keep checking the
                // rest so every independent error surfaces in one pass (#566).
                for s in statements {
                    let _ = self.check_expr_recover(s, node_id, locals, effs);
                }
                self.check_expr(result, node_id, locals, effs)
            }
            a::CExpr::RecordLit { fields } => {
                let mut tys = IndexMap::new();
                for f in fields {
                    if tys.contains_key(&f.name) {
                        return Err(TypeError::DuplicateField {
                            at_node: node_id.into(), field: f.name.clone()
                        });
                    }
                    let ft = self.check_expr(&f.value, node_id, locals, effs)?;
                    tys.insert(f.name.clone(), ft);
                }
                Ok(Ty::Record(tys))
            }
            a::CExpr::TupleLit { items } => {
                let mut ts = Vec::new();
                for it in items { ts.push(self.check_expr(it, node_id, locals, effs)?); }
                Ok(Ty::Tuple(ts))
            }
            a::CExpr::ListLit { items } => {
                let elem = self.u.fresh();
                for it in items {
                    let t = self.check_expr(it, node_id, locals, effs)?;
                    if let Err(err) = self.unify_with_record_coercion(&t, &elem) {
                        return Err(mismatch_err(node_id, err, &self.u, vec!["in list literal".into()]));
                    }
                }
                Ok(Ty::List(Box::new(elem)))
            }
            a::CExpr::FieldAccess { value, field } => {
                // #963: `<alias>.Ctor` used as a value — a nullary constructor
                // of a resolved dependency module (a payload constructor used
                // this way is handled in `check_call`). Same rationale as the
                // qualified-constructor call path.
                if let a::CExpr::Var { name: alias } = &**value {
                    if self.type_env.dep_alias_prefixes.contains_key(alias)
                        && self.type_env.ctor_to_type.contains_key(field)
                    {
                        return self.check_constructor(field, &[], node_id, locals, effs);
                    }
                }
                let vt = self.check_expr(value, node_id, locals, effs)?;
                let resolved = self.u.resolve(&vt);
                // Unfold a Record-aliased Con (e.g. `type Request = { ... }`
                // or `type Box[T] = { value :: T }`). For parametric aliases
                // the helper substitutes the actual args for the formal
                // params; the post-unfold shape is only a Record when the
                // alias body was a record, so non-record aliases (e.g.
                // `type UserId = Int`) fall through to the
                // "expected record" error below.
                let resolved = if let Ty::Con(_, _) = &resolved {
                    let unfolded = self.unfold_record_alias(resolved.clone());
                    if matches!(unfolded, Ty::Record(_)) {
                        unfolded
                    } else {
                        resolved
                    }
                } else {
                    resolved
                };
                match resolved {
                    Ty::Record(fields) => fields.get(field).cloned()
                        .or_else(|| synthesize_decode_typed_field(field, &fields))
                        .ok_or_else(|| TypeError::UnknownField {
                            at_node: node_id.into(),
                            record_type: Ty::Record(fields.clone()).pretty(),
                            field: field.clone(),
                        }),
                    other => Err(TypeError::TypeMismatch {
                        at_node: node_id.into(),
                        expected: "record".into(),
                        got: other.pretty(),
                        context: vec![format!("field access `.{}`", field)],
                    }),
                }
            }
            a::CExpr::Lambda { params, return_type, effects: l_effects, effect_row_var: l_row_var, body } => {
                let param_tys: Vec<Ty> = params.iter().map(|p| ty_from_canon_env(&p.ty, &[], &self.type_env)).collect();
                let ret_ty = ty_from_canon_env(return_type, &[], &self.type_env);
                // A row-polymorphic lambda (`fn (..) -> [io | E] ..`) resolves
                // its tail `E` to the enclosing function's instantiated row-var
                // id (recorded in `eff_row_scope`), so effects produced in the
                // body — e.g. by calling a row-poly parameter — flow out through
                // the closure's type (into `net.serve_fn` etc.) rather than
                // being dropped. An unknown name is a plain error.
                let row_var = match l_row_var {
                    Some(name) => match self.eff_row_scope.get(name) {
                        Some(id) => Some(*id),
                        None => {
                            return Err(TypeError::EffectNotDeclared {
                                at_node: node_id.into(),
                                effect: format!("unbound effect-row variable `{}`", name),
                            });
                        }
                    },
                    None => None,
                };
                let declared = EffectSet {
                    concrete: {
                        let mut s = std::collections::BTreeSet::new();
                        for e in l_effects {
                            let arg = e.arg.as_ref().map(|a| match a {
                                a::EffectArg::Str { value } => crate::types::EffectArg::Str(value.clone()),
                                a::EffectArg::Int { value } => crate::types::EffectArg::Int(*value),
                                a::EffectArg::Ident { value } => crate::types::EffectArg::Ident(value.clone()),
                            });
                            s.insert(crate::types::EffectKind { name: e.name.clone(), arg });
                        }
                        s
                    },
                    var: row_var,
                };
                let mut inner_locals = locals.clone();
                for (p, t) in params.iter().zip(param_tys.iter()) {
                    inner_locals.insert(p.name.clone(), t.clone());
                }
                let mut inner_effs = EffectSet::empty();
                let body_ty = self.check_expr(body, node_id, &mut inner_locals, &mut inner_effs)?;
                if let Err(err) = self.unify_with_record_coercion(&body_ty, &ret_ty) {
                    return Err(mismatch_err(node_id, err, &self.u, vec!["in lambda body".into()]));
                }
                if !inner_effs.is_subset(&declared) {
                    for e in inner_effs.concrete.iter() {
                        if !declared.concrete.iter().any(|d| d.subsumes(e)) {
                            return Err(TypeError::EffectNotDeclared {
                                at_node: node_id.into(),
                                effect: e.pretty(),
                            });
                        }
                    }
                }
                // The body produced an open effect row (e.g. by calling a
                // row-polymorphic parameter), but the lambda's declared row
                // doesn't carry that same tail — without `| E` the extra
                // effects would be silently dropped at the closure boundary.
                // Require the lambda to declare the matching open row.
                if let Some(iv) = inner_effs.var {
                    if declared.var != Some(iv) {
                        return Err(TypeError::EffectNotDeclared {
                            at_node: node_id.into(),
                            effect: "open effect row (annotate the lambda's effects with `| <row-var>`)".into(),
                        });
                    }
                }
                Ok(Ty::function(param_tys, declared, ret_ty))
            }
            a::CExpr::BinOp { op, lhs, rhs } => self.check_binop(op, lhs, rhs, node_id, locals, effs),
            a::CExpr::UnaryOp { op, expr } => {
                let t = self.check_expr(expr, node_id, locals, effs)?;
                match op.as_str() {
                    "-" => {
                        // Either Int or Float; we pick Int by default if unconstrained.
                        let r = self.u.resolve(&t);
                        match r {
                            Ty::Prim(Prim::Int) | Ty::Prim(Prim::Float) => Ok(t),
                            Ty::Var(_) => {
                                // default to Int.
                                self.u.unify(&t, &Ty::int()).map_err(|e| mismatch_err(node_id, e, &self.u, vec![]))?;
                                Ok(Ty::int())
                            }
                            other => Err(TypeError::TypeMismatch {
                                at_node: node_id.into(),
                                expected: "Int or Float".into(),
                                got: other.pretty(),
                                context: vec!["unary `-`".into()],
                            }),
                        }
                    }
                    "not" => {
                        self.u.unify(&t, &Ty::bool()).map_err(|e| mismatch_err(node_id, e, &self.u, vec!["unary `not`".into()]))?;
                        Ok(Ty::bool())
                    }
                    other => panic!("unknown unary op: {other}"),
                }
            }
            a::CExpr::Return { value } => {
                // For now treat Return as having type Never; the surrounding
                // context will unify with the actual return type.
                self.check_expr(value, node_id, locals, effs)?;
                Ok(Ty::Never)
            }
        }
    }

    fn check_binop(
        &mut self,
        op: &str,
        lhs: &a::CExpr,
        rhs: &a::CExpr,
        node_id: &str,
        locals: &mut IndexMap<String, Ty>,
        effs: &mut EffectSet,
    ) -> Result<Ty, TypeError> {
        let lt = self.check_expr(lhs, node_id, locals, effs)?;
        let rt = self.check_expr(rhs, node_id, locals, effs)?;
        match op {
            "+" => {
                // #308: `+` is overloaded over Int, Float, and Str.
                // Str concatenation dispatches at the VM layer
                // (Op::NumAdd in bytecode handles all three).
                // #323: unfold one-step type aliases on the resolved
                // type so `type UserId = Int; id + id` works under
                // Option-A transparency. Same below for the other
                // numeric operator groups.
                self.u.unify(&lt, &rt).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                let r = self.unfold_record_alias(self.u.resolve(&lt));
                match r {
                    Ty::Prim(Prim::Int) | Ty::Prim(Prim::Float) | Ty::Prim(Prim::Str) => Ok(lt),
                    Ty::Var(_) => {
                        self.u.unify(&lt, &Ty::int()).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                        Ok(Ty::int())
                    }
                    other => Err(TypeError::TypeMismatch {
                        at_node: node_id.into(),
                        expected: "Int, Float, or Str".into(),
                        got: other.pretty(),
                        context: vec![format!("operator `{op}`")],
                    }),
                }
            }
            "-" | "*" | "/" | "%" => {
                self.u.unify(&lt, &rt).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                let r = self.unfold_record_alias(self.u.resolve(&lt));
                match r {
                    Ty::Prim(Prim::Int) | Ty::Prim(Prim::Float) => Ok(lt),
                    Ty::Var(_) => {
                        self.u.unify(&lt, &Ty::int()).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                        Ok(Ty::int())
                    }
                    other => Err(TypeError::TypeMismatch {
                        at_node: node_id.into(),
                        expected: "Int or Float".into(),
                        got: other.pretty(),
                        context: vec![format!("operator `{op}`")],
                    }),
                }
            }
            "==" | "!=" => {
                self.u.unify(&lt, &rt).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                Ok(Ty::bool())
            }
            "<" | "<=" | ">" | ">=" => {
                self.u.unify(&lt, &rt).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                let r = self.unfold_record_alias(self.u.resolve(&lt));
                match r {
                    Ty::Prim(Prim::Int) | Ty::Prim(Prim::Float) | Ty::Prim(Prim::Str) => Ok(Ty::bool()),
                    Ty::Var(_) => {
                        self.u.unify(&lt, &Ty::int()).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                        Ok(Ty::bool())
                    }
                    other => Err(TypeError::TypeMismatch {
                        at_node: node_id.into(),
                        expected: "Int, Float, or Str".into(),
                        got: other.pretty(),
                        context: vec![format!("operator `{op}`")],
                    }),
                }
            }
            "and" | "or" => {
                self.u.unify(&lt, &Ty::bool()).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                self.u.unify(&rt, &Ty::bool()).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("operator `{op}`")]))?;
                Ok(Ty::bool())
            }
            other => panic!("unknown binop: {other}"),
        }
    }

    fn check_call(
        &mut self,
        call_expr: &a::CExpr,
        callee: &a::CExpr,
        args: &[a::CExpr],
        node_id: &str,
        locals: &mut IndexMap<String, Ty>,
        effs: &mut EffectSet,
    ) -> Result<Ty, TypeError> {
        // #963: a qualified constructor call, `<alias>.Ctor(args)`, where the
        // alias is a resolved dependency module and `Ctor` is one of its
        // exported constructors. Non-inlined resolution keeps the reference
        // qualified (an inlined dependency would have rewritten it to the bare,
        // flat-namespace constructor), so route it to constructor checking
        // rather than letting it read as a field access on the module record.
        if let a::CExpr::FieldAccess { value, field } = callee {
            if let a::CExpr::Var { name: alias } = &**value {
                if self.type_env.dep_alias_prefixes.contains_key(alias)
                    && self.type_env.ctor_to_type.contains_key(field)
                {
                    return self.check_constructor(field, args, node_id, locals, effs);
                }
            }
        }
        // #168: identify the call before the recursive descent so we
        // can later rewrite this exact node. The identity is a stable
        // (stage, NodeId) pair rather than the expression's address
        // (#777), so the resulting table can be applied to any copy
        // of the checked stages. `is_module_parse_call` recognises
        // `<alias>.parse` where alias was bound to one of {json,
        // toml, yaml} during the import pass.
        let parse_site = if self.is_module_parse_call(callee) {
            self.parse_site_of(call_expr)
        } else {
            None
        };
        let callee_ty = self.check_expr(callee, node_id, locals, effs)?;
        let resolved = self.u.resolve(&callee_ty);
        match resolved {
            Ty::Function { params, effects, ret } => {
                if params.len() != args.len() {
                    return Err(TypeError::ArityMismatch {
                        at_node: node_id.into(),
                        expected: params.len(),
                        got: args.len(),
                    });
                }
                for (i, (a, p)) in args.iter().zip(params.iter()).enumerate() {
                    let at = self.check_expr(a, node_id, locals, effs)?;
                    if let Err(err) = self.unify_with_record_coercion(&at, p) {
                        return Err(mismatch_err(node_id, err, &self.u, vec![format!("argument {} of call", i + 1)]));
                    }
                }
                // #209 slice 2: refinement discharge for direct named
                // calls. Look up the callee's original params (kept
                // pre-strip in `fn_params`), and for each refined
                // param attempt static discharge against the call
                // arg. Refuted = type error; Deferred = pass (slice
                // 3 will add a runtime residual check).
                if let a::CExpr::Var { name: callee_name } = callee {
                    if let Some(callee_params) = self.fn_params.get(callee_name).cloned() {
                        for (i, (param, arg)) in callee_params.iter().zip(args.iter()).enumerate() {
                            if let a::TypeExpr::Refined { binding, predicate, .. } = &param.ty {
                                let outcome = crate::discharge::try_discharge(
                                    predicate, binding, arg);
                                if let crate::discharge::DischargeOutcome::Refuted { reason } = outcome {
                                    return Err(TypeError::RefinementViolation {
                                        at_node: node_id.into(),
                                        fn_name: callee_name.clone(),
                                        param_index: i,
                                        binding: binding.clone(),
                                        reason,
                                    });
                                }
                            }
                        }
                    }
                }
                // Re-resolve effects after unifying args: an effect-row
                // variable on the function type may have been bound by
                // an argument's closure type, and we want the
                // *post-binding* set when propagating to the caller.
                let resolved_effects = self.u.resolve_effects(&effects);
                effs.extend(&resolved_effects);
                // #168: snapshot the post-arg-unification return type
                // for stdlib parse calls. Resolution to the eventual
                // `Result[Record{...}, _]` shape happens at the end
                // of `check_program` once the whole program's
                // unification has settled — match-pattern annotations
                // and let-type-annotations may bind T after this
                // point.
                if let Some(site) = parse_site {
                    self.pending_parse_calls.push((site, (*ret).clone()));
                }
                Ok(*ret)
            }
            Ty::Var(_) => {
                // Build a function type and unify.
                let mut p_tys = Vec::new();
                for a in args { p_tys.push(self.check_expr(a, node_id, locals, effs)?); }
                let r = self.u.fresh();
                let f = Ty::function(p_tys, EffectSet::empty(), r.clone());
                self.u.unify(&callee_ty, &f).map_err(|e| mismatch_err(node_id, e, &self.u, vec!["in call".into()]))?;
                Ok(r)
            }
            other => Err(TypeError::TypeMismatch {
                at_node: node_id.into(),
                expected: "function".into(),
                got: other.pretty(),
                context: vec!["in call".into()],
            }),
        }
    }

    fn check_constructor(
        &mut self,
        name: &str,
        args: &[a::CExpr],
        node_id: &str,
        locals: &mut IndexMap<String, Ty>,
        effs: &mut EffectSet,
    ) -> Result<Ty, TypeError> {
        let owning = self.type_env.ctor_to_type.get(name).cloned()
            .ok_or_else(|| TypeError::UnknownVariant {
                at_node: node_id.into(),
                constructor: name.to_string(),
            })?;
        let def = self.type_env.types.get(&owning).cloned()
            .expect("ctor_to_type points to a real type");
        let variants = match &def.kind {
            TypeDefKind::Union(v) => v.clone(),
            _ => return Err(TypeError::UnknownVariant {
                at_node: node_id.into(),
                constructor: name.to_string(),
            }),
        };
        // Instantiate the type's params with fresh vars; substitute into
        // both the variant's payload type and the resulting Con(...).
        let mut subst = IndexMap::new();
        let mut con_args = Vec::with_capacity(def.params.len());
        for (i, _p) in def.params.iter().enumerate() {
            let fresh = self.u.fresh();
            subst.insert(i as u32, fresh.clone());
            con_args.push(fresh);
        }
        let payload = variants.get(name).cloned().flatten();
        match (payload, args) {
            (None, []) => Ok(Ty::Con(owning, con_args)),
            (Some(payload), args) => {
                let inst_payload = subst_vars(&payload, &subst, &IndexMap::new());
                let arg_count = match &inst_payload {
                    Ty::Tuple(items) => items.len(),
                    _ => 1,
                };
                if arg_count != args.len() {
                    return Err(TypeError::ArityMismatch {
                        at_node: node_id.into(),
                        expected: arg_count,
                        got: args.len(),
                    });
                }
                if args.len() == 1 {
                    let at = self.check_expr(&args[0], node_id, locals, effs)?;
                    self.unify_with_record_coercion(&at, &inst_payload).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("constructor `{}`", name)]))?;
                } else if let Ty::Tuple(items) = inst_payload {
                    for (i, (a, t)) in args.iter().zip(items.iter()).enumerate() {
                        let at = self.check_expr(a, node_id, locals, effs)?;
                        self.unify_with_record_coercion(&at, t).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("constructor `{}` arg {}", name, i + 1)]))?;
                    }
                }
                Ok(Ty::Con(owning, con_args))
            }
            (None, _) => Err(TypeError::ArityMismatch {
                at_node: node_id.into(), expected: 0, got: args.len(),
            }),
        }
    }

    fn bind_pattern(
        &mut self,
        pat: &a::Pattern,
        ty: &Ty,
        locals: &mut IndexMap<String, Ty>,
        node_id: &str,
    ) -> Result<(), TypeError> {
        match pat {
            a::Pattern::PWild => Ok(()),
            a::Pattern::PVar { name } => {
                locals.insert(name.clone(), ty.clone());
                Ok(())
            }
            a::Pattern::PLiteral { value } => {
                let lt = lit_type(value);
                self.unify_with_record_coercion(&lt, ty).map_err(|e| mismatch_err(node_id, e, &self.u, vec!["in pattern".into()]))?;
                Ok(())
            }
            a::Pattern::PConstructor { name, args } => {
                // Re-use constructor logic but in pattern position.
                let owning = self.type_env.ctor_to_type.get(name).cloned()
                    .ok_or_else(|| TypeError::UnknownVariant {
                        at_node: node_id.into(), constructor: name.clone(),
                    })?;
                let def = self.type_env.types.get(&owning).cloned().unwrap();
                let mut subst = IndexMap::new();
                let mut con_args = Vec::new();
                for (i, _) in def.params.iter().enumerate() {
                    let fresh = self.u.fresh();
                    subst.insert(i as u32, fresh.clone());
                    con_args.push(fresh);
                }
                let con_ty = Ty::Con(owning.clone(), con_args);
                self.unify_with_record_coercion(&con_ty, ty).map_err(|e| mismatch_err(node_id, e, &self.u, vec![format!("constructor pattern `{}`", name)]))?;
                let payload = match &def.kind {
                    TypeDefKind::Union(v) => v.get(name).cloned().flatten(),
                    _ => None,
                };
                match (payload, args.as_slice()) {
                    (None, []) => Ok(()),
                    (Some(payload), args) => {
                        let inst = subst_vars(&payload, &subst, &IndexMap::new());
                        if args.len() == 1 {
                            self.bind_pattern(&args[0], &inst, locals, node_id)?;
                        } else if let Ty::Tuple(items) = inst {
                            for (a, t) in args.iter().zip(items.iter()) {
                                self.bind_pattern(a, t, locals, node_id)?;
                            }
                        }
                        Ok(())
                    }
                    (None, _) => Err(TypeError::ArityMismatch {
                        at_node: node_id.into(), expected: 0, got: args.len(),
                    }),
                }
            }
            a::Pattern::PRecord { fields } => {
                // Unfold a record-aliased Con (`type Bands = { ... }`)
                // so a structural `{ idea: pat, ... }` pattern can match
                // a nominal-typed scrutinee, mirror of #79's literal
                // coercion at every position.
                let resolved = self.unfold_record_alias(self.u.resolve(ty));
                let rec = match resolved {
                    Ty::Record(r) => r,
                    _ => return Err(TypeError::TypeMismatch {
                        at_node: node_id.into(),
                        expected: "record".into(),
                        got: ty.pretty(),
                        context: vec!["in record pattern".into()],
                    }),
                };
                for f in fields {
                    let ft = rec.get(&f.name).cloned()
                        .ok_or_else(|| TypeError::UnknownField {
                            at_node: node_id.into(),
                            record_type: Ty::Record(rec.clone()).pretty(),
                            field: f.name.clone(),
                        })?;
                    self.bind_pattern(&f.pattern, &ft, locals, node_id)?;
                }
                Ok(())
            }
            a::Pattern::PTuple { items } => {
                // An empty-tuple pattern `()` is equivalent to Unit.
                if items.is_empty() {
                    return self.unify_with_record_coercion(&Ty::Unit, ty)
                        .map_err(|e| mismatch_err(node_id, e, &self.u, vec!["in unit pattern".into()]));
                }
                let resolved = self.u.resolve(ty);
                let tup = match resolved {
                    Ty::Tuple(t) => t,
                    Ty::Var(_) => {
                        let fresh: Vec<Ty> = items.iter().map(|_| self.u.fresh()).collect();
                        let tup_ty = Ty::Tuple(fresh.clone());
                        self.unify_with_record_coercion(&tup_ty, ty).map_err(|e| mismatch_err(node_id, e, &self.u, vec!["in tuple pattern".into()]))?;
                        fresh
                    }
                    other => {
                        return Err(TypeError::TypeMismatch {
                            at_node: node_id.into(),
                            expected: "tuple".into(),
                            got: other.pretty(),
                            context: vec!["in tuple pattern".into()],
                        });
                    }
                };
                if tup.len() != items.len() {
                    return Err(TypeError::ArityMismatch {
                        at_node: node_id.into(), expected: tup.len(), got: items.len(),
                    });
                }
                for (p, t) in items.iter().zip(tup.iter()) {
                    self.bind_pattern(p, t, locals, node_id)?;
                }
                Ok(())
            }
        }
    }
}

fn lit_type(l: &a::CLit) -> Ty {
    match l {
        a::CLit::Int { .. } => Ty::int(),
        a::CLit::Float { .. } => Ty::float(),
        a::CLit::Str { .. } => Ty::str(),
        a::CLit::Bytes { .. } => Ty::bytes(),
        a::CLit::Bool { .. } => Ty::bool(),
        a::CLit::Unit => Ty::Unit,
    }
}

fn instantiate(s: &Scheme, u: &mut Unifier) -> Ty {
    instantiate_with_eff(s, u).0
}

/// Like `instantiate`, but also returns the effect-var substitution
/// (scheme effect-var id → fresh id). `check_fn` uses it to map the
/// function's surface row-variable names to their instantiated ids, so a
/// row-polymorphic lambda in the body can join the same row.
fn instantiate_with_eff(s: &Scheme, u: &mut Unifier) -> (Ty, IndexMap<u32, u32>) {
    let mut ty_subst = IndexMap::new();
    for v in &s.vars { ty_subst.insert(*v, u.fresh()); }
    let mut eff_subst = IndexMap::new();
    for v in &s.eff_vars { eff_subst.insert(*v, u.fresh_eff_id()); }
    let ty = subst_vars(&s.ty, &ty_subst, &eff_subst);
    (ty, eff_subst)
}

fn subst_vars(
    t: &Ty,
    subst: &IndexMap<TyVarId, Ty>,
    eff_subst: &IndexMap<u32, u32>,
) -> Ty {
    match t {
        Ty::Var(v) => subst.get(v).cloned().unwrap_or_else(|| Ty::Var(*v)),
        Ty::Prim(_) | Ty::Unit | Ty::Never => t.clone(),
        Ty::List(inner) => Ty::List(Box::new(subst_vars(inner, subst, eff_subst))),
        Ty::Tuple(items) => Ty::Tuple(items.iter().map(|t| subst_vars(t, subst, eff_subst)).collect()),
        Ty::Record(fs) => {
            let mut out = IndexMap::new();
            for (k, v) in fs { out.insert(k.clone(), subst_vars(v, subst, eff_subst)); }
            Ty::Record(out)
        }
        Ty::Con(n, args) => Ty::Con(n.clone(),
            args.iter().map(|t| subst_vars(t, subst, eff_subst)).collect()),
        Ty::Function { params, effects, ret } => {
            // Refresh the effect-row variable if it's quantified in the
            // scheme; concrete kinds carry through unchanged.
            let new_effects = EffectSet {
                concrete: effects.concrete.clone(),
                var: effects.var.and_then(|v| eff_subst.get(&v).copied()).or(effects.var),
            };
            Ty::Function {
                params: params.iter().map(|t| subst_vars(t, subst, eff_subst)).collect(),
                effects: new_effects,
                ret: Box::new(subst_vars(ret, subst, eff_subst)),
            }
        }
    }
}

fn mismatch_err(node_id: &str, e: UnifyError, u: &Unifier, context: Vec<String>) -> TypeError {
    match e {
        UnifyError::Mismatch { a, b } => TypeError::TypeMismatch {
            at_node: node_id.into(),
            expected: u.resolve(&b).pretty(),
            got: u.resolve(&a).pretty(),
            context,
        },
        UnifyError::Infinite { .. } => TypeError::InfiniteType { at_node: node_id.into() },
        UnifyError::EffectMismatch { a, b } => {
            // Render the two rows in compact form, e.g. `[net]` vs `[]`.
            // Effect rows are invariant, so this is its own rule_tag
            // (#565) rather than a generic type-mismatch — the
            // explanation steers the fix toward narrowing the body.
            let render = |e: &EffectSet| -> String {
                let mut parts: Vec<String> = e.concrete.iter()
                    .map(crate::types::EffectKind::pretty).collect();
                if let Some(v) = e.var { parts.push(format!("?e{}", v)); }
                if parts.is_empty() { "[]".into() } else { format!("[{}]", parts.join(", ")) }
            };
            TypeError::EffectRowMismatch {
                at_node: node_id.into(),
                expected: render(&b),
                got: render(&a),
                context,
            }
        }
    }
}