//! Iter 18d.2: shape-compatibility check for `(reuse-as <var> <body>)`.
//!
//! ## Why this is its own pass
//!
//! Reuse-as semantics says: "free `<var>`'s heap slot, write `<body>`'s
//! freshly-allocated payload into it." That is sound only when
//! `<var>`'s ctor on this control-flow path has the same field count
//! and the same per-field LLVM types as `<body>`'s ctor — otherwise
//! the in-place rewrite would either underrun the box (smaller body
//! into bigger source slot, leaving uninitialised tail bytes) or write
//! a field of one LLVM type into a slot built for another (e.g.
//! storing a `ptr` over a previous `i64` slot, both 8-byte but with
//! different drop semantics for the OLD value at the same offset).
//!
//! The typechecker doesn't know enough to do this check: `<var>`'s
//! AILang type is `(con T)` (the binder type), but the *runtime ctor*
//! of the box `<var>` points at depends on the path — `<var>` may
//! flow into the `Cons` arm of a match where the pattern bound it as
//! the scrutinee, in which case its ctor on this arm is `Cons`. The
//! shape check resolves that ctor by walking the same way codegen
//! does, then compares against `<body>`'s ctor (which is always
//! syntactically a `Term::Ctor` once 18d.1's typecheck is satisfied).
//!
//! Mismatches surface as a structured `reuse-as-shape-mismatch`
//! diagnostic with a suggested rewrite that drops the wrapper. The
//! build then fails before codegen runs; the LLM author either fixes
//! the shapes or removes the reuse hint.
//!
//! ## Activation gate
//!
//! Same as `linearity::check_module`: only fns whose `Type::Fn.param_modes`
//! is non-empty AND contains no [`ParamMode::Implicit`]. Reuse-as is
//! part of the explicit-mode discipline; firing the check on legacy
//! all-`Implicit` fns would risk false positives on workloads that
//! never opted into the explicit-mode lane.
//!
//! ## Path-ctor resolution
//!
//! A binder gets a known ctor on the current path if either:
//!
//! 1. It was bound by `Term::Let { value: Term::Ctor { type_name, ctor, .. }, .. }`
//!    — the ctor is syntactically the rhs.
//! 2. It is the scrutinee `Term::Var { name }` of an enclosing
//!    `Term::Match` and we are inside an arm whose `Pattern::Ctor { ctor, .. }`
//!    matched it — the ctor is the arm's pattern.
//!
//! Both forms are tracked on a stack-of-bindings (`PathCtor`s) so that
//! lexical scope is honoured: nested matches and lets shadow correctly,
//! and on arm exit / let exit the binding pops.
//!
//! If the source binder is not in the path-ctor map at the reuse-as
//! site (e.g. complex control flow, or `<var>` is a fn parameter that
//! was never matched), we **conservatively reject** with the same
//! diagnostic — the LLM either spells things to make the path
//! obvious or removes the wrapper.
//!
//! ## Cross-module note
//!
//! Both ctors must be in the same module's ctor index for the field-
//! count and field-type comparison to be meaningful (the field types
//! are written in the owning module's local namespace; cross-module
//! comparison would need the same `qualify_local_types` plumbing
//! `check_in_workspace` uses). For 18d.2 we only inspect ctors with
//! bare type names (no `module.T` prefix) and conservatively reject
//! anything else as shape-indeterminate. Cross-module reuse-as is not
//! exercised by any 18d.2 fixture; lifting the restriction is a
//! mechanical follow-up if it ever lands.

use crate::diagnostic::Diagnostic;
use ailang_core::ast::{Arm, Def, FnDef, Module, ParamMode, Pattern, Term, Type, TypeDef};
use ailang_surface::term_to_form_a;
use std::collections::HashMap;

/// Iter 18d.2: top-level entry. Walks every fn in `m` and emits
/// `reuse-as-shape-mismatch` diagnostics for the all-explicit-mode
/// fns. Other fns are skipped.
///
/// Output ordering: defs in declaration order; within a def, source-
/// order discovery (depth-first left-to-right walk).
pub(crate) fn check_module(m: &Module) -> Vec<Diagnostic> {
    // Collect the module's own type defs once. Cross-module references
    // are out of scope per the module-level note; same-module ctors
    // are the only ones we inspect.
    let mut types: HashMap<String, TypeDef> = HashMap::new();
    for def in &m.defs {
        if let Def::Type(td) = def {
            types.insert(td.name.clone(), td.clone());
        }
    }
    let mut diags = Vec::new();
    for def in &m.defs {
        if let Def::Fn(f) = def {
            check_fn(f, &types, &mut diags);
        }
    }
    diags
}

/// Per-fn check. Skips fns whose signature has any `Implicit` param
/// (legacy back-compat lane) or whose param list is empty (no binders
/// to track).
fn check_fn(f: &FnDef, types: &HashMap<String, TypeDef>, diags: &mut Vec<Diagnostic>) {
    let param_modes: &[ParamMode] = match strip_forall(&f.ty) {
        Type::Fn { param_modes, .. } => param_modes.as_slice(),
        _ => return,
    };
    if param_modes.is_empty()
        || param_modes
            .iter()
            .any(|m| matches!(m, ParamMode::Implicit))
    {
        return;
    }

    let mut checker = Checker {
        types,
        diags,
        def_name: &f.name,
        path_ctors: HashMap::new(),
    };
    checker.walk(&f.body);
}

/// Returns the inner type of a top-level `Forall<Fn ...>` (or `t`
/// unchanged if not a `Forall`).
fn strip_forall(t: &Type) -> &Type {
    match t {
        Type::Forall { body, .. } => body,
        other => other,
    }
}

/// One entry in the path-ctor stack: the bare ctor name `<var>` carries
/// on the current control-flow path.
#[derive(Debug, Clone)]
struct PathCtor {
    /// The bare ctor name (e.g. `"Cons"`).
    ctor: String,
    /// The bare type name (e.g. `"List"`). Used to look the ctor up in
    /// the module's `types` table. Cross-module (`module.T`) prefixes
    /// disable the comparison — see module-level note.
    type_name: String,
}

struct Checker<'a> {
    types: &'a HashMap<String, TypeDef>,
    diags: &'a mut Vec<Diagnostic>,
    def_name: &'a str,
    /// Path-resolved ctor for each in-scope binder. Modified in place
    /// with save/restore at lexical-scope boundaries (let, match arms).
    /// A binder absent from this map is path-ctor-indeterminate at the
    /// current point (e.g. an as-yet-unmatched fn parameter).
    path_ctors: HashMap<String, PathCtor>,
}

impl<'a> Checker<'a> {
    /// Walk `t`, emitting diagnostics for every reuse-as whose
    /// resolved source-ctor is incompatible with the body-ctor.
    fn walk(&mut self, t: &Term) {
        match t {
            Term::Lit { .. } | Term::Var { .. } => {}
            Term::App { callee, args, .. } => {
                self.walk(callee);
                for a in args {
                    self.walk(a);
                }
            }
            Term::Let { name, value, body } => {
                self.walk(value);
                // Push binder→ctor if the rhs is a literal ctor.
                let prev = self.path_ctors.remove(name);
                if let Term::Ctor { type_name, ctor, .. } = value.as_ref() {
                    if let Some(bare_type) = bare_name(type_name) {
                        self.path_ctors.insert(
                            name.clone(),
                            PathCtor {
                                ctor: ctor.clone(),
                                type_name: bare_type,
                            },
                        );
                    }
                }
                self.walk(body);
                self.path_ctors.remove(name);
                if let Some(p) = prev {
                    self.path_ctors.insert(name.clone(), p);
                }
            }
            Term::LetRec { name, body, in_term, .. } => {
                // LetRec binds a fn, not a value — never a ctor.
                let prev = self.path_ctors.remove(name);
                self.walk(body);
                self.walk(in_term);
                self.path_ctors.remove(name);
                if let Some(p) = prev {
                    self.path_ctors.insert(name.clone(), p);
                }
            }
            Term::If { cond, then, else_ } => {
                self.walk(cond);
                // Branches share the pre-If ctor map; neither branch
                // commits a new ctor binding upward (an If-typed value
                // could in principle be a ctor, but we don't refine
                // through If — too narrow a path).
                let saved = self.path_ctors.clone();
                self.walk(then);
                self.path_ctors = saved.clone();
                self.walk(else_);
                self.path_ctors = saved;
            }
            Term::Match { scrutinee, arms } => {
                self.walk(scrutinee);
                let saved = self.path_ctors.clone();
                // The scrutinee's binder name (if it's a bare Var) is
                // refined per-arm by the arm's pattern.
                let scrut_var = match scrutinee.as_ref() {
                    Term::Var { name } => Some(name.clone()),
                    _ => None,
                };
                for arm in arms {
                    self.path_ctors = saved.clone();
                    self.walk_arm(arm, scrut_var.as_deref());
                }
                self.path_ctors = saved;
            }
            Term::Seq { lhs, rhs } => {
                self.walk(lhs);
                self.walk(rhs);
            }
            Term::Ctor { args, .. } => {
                for a in args {
                    self.walk(a);
                }
            }
            Term::Do { args, .. } => {
                for a in args {
                    self.walk(a);
                }
            }
            Term::Lam { body, .. } => {
                // A lam is a closure boundary. We don't refine
                // captured binders through it (their path-ctor is
                // already what we have); the lam's own params are
                // fresh binders with no known ctor.
                self.walk(body);
            }
            Term::Clone { value } => self.walk(value),
            Term::ReuseAs { source, body } => {
                // Walk both sides first so any nested reuse-as gets
                // reported in source order. Then perform the shape
                // check at this site.
                self.walk(source);
                self.walk(body);
                self.check_reuse_as(source, body);
            }
        }
    }

    /// Walk one match arm. If the scrutinee was a bare var and the
    /// pattern is a `Pattern::Ctor`, refine that var's path-ctor to
    /// the pattern's ctor for the arm's body. The pattern's bound
    /// names (h, t) are introduced as path-ctor-indeterminate (they
    /// could be any ctor). Wildcard / Var / Lit patterns leave the
    /// scrutinee's path-ctor untouched.
    fn walk_arm(&mut self, arm: &Arm, scrut_var: Option<&str>) {
        let pattern_binders = collect_pattern_binders(&arm.pat);
        let mut saved: HashMap<String, Option<PathCtor>> = HashMap::new();
        for n in &pattern_binders {
            saved.insert(n.clone(), self.path_ctors.remove(n));
        }
        // Refine the scrutinee's path-ctor for this arm.
        let mut refined_scrut: Option<(String, Option<PathCtor>)> = None;
        if let (Some(sv), Pattern::Ctor { ctor, .. }) = (scrut_var, &arm.pat) {
            // Resolve the type-name of the matched ctor by looking up
            // the ctor in the module's type list. Same-module only —
            // cross-module patterns disable the refinement (consistent
            // with the module-level note).
            if let Some(type_name) = self.find_type_for_ctor(ctor) {
                let prev = self.path_ctors.insert(
                    sv.to_string(),
                    PathCtor {
                        ctor: ctor.clone(),
                        type_name,
                    },
                );
                refined_scrut = Some((sv.to_string(), prev));
            }
        }
        self.walk(&arm.body);
        // Restore pattern-bound names.
        for n in &pattern_binders {
            self.path_ctors.remove(n);
            if let Some(p) = saved.remove(n).flatten() {
                self.path_ctors.insert(n.clone(), p);
            }
        }
        // Restore the scrutinee's pre-arm path-ctor.
        if let Some((sv, prev)) = refined_scrut {
            self.path_ctors.remove(&sv);
            if let Some(p) = prev {
                self.path_ctors.insert(sv, p);
            }
        }
    }

    /// The shape check at one reuse-as site. Pre-conditions handled
    /// upstream:
    /// - 18d.1's typecheck guarantees `body` is `Term::Ctor` (or
    ///   `Term::Lam`, but lams have no ctor and are not in scope here).
    /// - 18d.1's linearity guarantees `source` is a bare `Term::Var`
    ///   referring to an in-scope binder.
    ///
    /// What this method enforces: the source's path-resolved ctor and
    /// the body's ctor declare the same field count AND the same
    /// per-field LLVM-equivalent types. Mismatch → emit
    /// `reuse-as-shape-mismatch`. Source's path-ctor unresolved →
    /// also emit (conservative reject — the codegen seam can't lower
    /// what the static check can't verify).
    fn check_reuse_as(&mut self, source: &Term, body: &Term) {
        let src_var = match source {
            Term::Var { name } => name,
            // Linearity already flagged this; skip the shape check to
            // avoid a duplicate diagnostic.
            _ => return,
        };
        let body_ctor = match body {
            Term::Ctor { type_name, ctor, .. } => (type_name.clone(), ctor.clone()),
            // Typecheck already flagged this; skip.
            _ => return,
        };
        let src_ctor = match self.path_ctors.get(src_var) {
            Some(p) => p.clone(),
            None => {
                self.diags.push(make_shape_mismatch(
                    self.def_name,
                    src_var,
                    /*src=*/ None,
                    &body_ctor,
                    "indeterminate-source-ctor",
                    body,
                ));
                return;
            }
        };
        // Same-module ctor names only — cross-module is conservative
        // reject.
        let body_type = match bare_name(&body_ctor.0) {
            Some(t) => t,
            None => {
                self.diags.push(make_shape_mismatch(
                    self.def_name,
                    src_var,
                    Some(&src_ctor),
                    &body_ctor,
                    "cross-module-body-ctor",
                    body,
                ));
                return;
            }
        };
        // Look up both ctors' declared field types.
        let src_fields = self.lookup_ctor_fields(&src_ctor.type_name, &src_ctor.ctor);
        let body_fields = self.lookup_ctor_fields(&body_type, &body_ctor.1);
        let (sf, bf) = match (src_fields, body_fields) {
            (Some(sf), Some(bf)) => (sf, bf),
            _ => {
                // One or both ctors not resolvable in the local module.
                self.diags.push(make_shape_mismatch(
                    self.def_name,
                    src_var,
                    Some(&src_ctor),
                    &body_ctor,
                    "ctor-not-in-module",
                    body,
                ));
                return;
            }
        };
        if sf.len() != bf.len() {
            self.diags.push(make_shape_mismatch(
                self.def_name,
                src_var,
                Some(&src_ctor),
                &body_ctor,
                "field-count-mismatch",
                body,
            ));
            return;
        }
        for (s, b) in sf.iter().zip(bf.iter()) {
            if !llvm_shape_equiv(s, b) {
                self.diags.push(make_shape_mismatch(
                    self.def_name,
                    src_var,
                    Some(&src_ctor),
                    &body_ctor,
                    "field-type-mismatch",
                    body,
                ));
                return;
            }
        }
    }

    /// Find the bare type name owning the given ctor name in the
    /// current module. Returns the bare type name, or `None` if no
    /// type in the module declares that ctor.
    fn find_type_for_ctor(&self, ctor: &str) -> Option<String> {
        for (tname, td) in self.types {
            if td.ctors.iter().any(|c| c.name == ctor) {
                return Some(tname.clone());
            }
        }
        None
    }

    /// Look up a ctor's declared field types by (type-name, ctor-name)
    /// in the current module. Returns `None` if the type isn't in
    /// `self.types` or the ctor isn't in the type.
    fn lookup_ctor_fields(&self, type_name: &str, ctor: &str) -> Option<Vec<Type>> {
        let td = self.types.get(type_name)?;
        td.ctors
            .iter()
            .find(|c| c.name == ctor)
            .map(|c| c.fields.clone())
    }
}

/// Returns the bare type name if `name` has no `module.` prefix,
/// otherwise `None`. The shape check intentionally doesn't try to
/// reach across module boundaries — see the module-level note.
fn bare_name(name: &str) -> Option<String> {
    if name.contains('.') {
        None
    } else {
        Some(name.to_string())
    }
}

/// LLVM-equivalence of two AILang [`Type`]s, mirroring the
/// `llvm_type` shape codegen uses:
/// - `Int` → `i64`
/// - `Bool` → `i1`
/// - `Unit` → `i8`
/// - `Str` / any other `Con` (ADT) / `Fn` / `Var` → `ptr`
///
/// The shape check uses this to compare two ctors' fields slot-by-
/// slot. Two slots are "shape-equivalent" iff their LLVM lowerings
/// are equal.
fn llvm_shape_equiv(a: &Type, b: &Type) -> bool {
    llvm_kind(a) == llvm_kind(b)
}

fn llvm_kind(t: &Type) -> &'static str {
    match t {
        Type::Con { name, .. } => match name.as_str() {
            "Int" => "i64",
            "Bool" => "i1",
            "Unit" => "i8",
            // Str + every user-declared ADT lower to `ptr`.
            _ => "ptr",
        },
        Type::Fn { .. } | Type::Var { .. } => "ptr",
        // Forall is a top-level wrapper; the shape inspector should
        // never see one in a ctor field. Treat conservatively as
        // `ptr` if it ever appears.
        Type::Forall { .. } => "ptr",
    }
}

fn collect_pattern_binders(p: &Pattern) -> Vec<String> {
    match p {
        Pattern::Wild | Pattern::Lit { .. } => vec![],
        Pattern::Var { name } => vec![name.clone()],
        Pattern::Ctor { fields, .. } => fields
            .iter()
            .flat_map(collect_pattern_binders)
            .collect(),
    }
}

/// Build a `reuse-as-shape-mismatch` diagnostic. The suggested
/// rewrite drops the wrapper and keeps the body alone — the LLM can
/// then either accept the normal allocator path or reshape the body.
///
/// `reason` is a stable kebab-case sub-code carried in `ctx.reason`
/// so consumers can branch on the specific failure mode without
/// parsing prose.
fn make_shape_mismatch(
    def: &str,
    binder: &str,
    src: Option<&PathCtor>,
    body_ctor: &(String, String),
    reason: &str,
    body: &Term,
) -> Diagnostic {
    let replacement = term_to_form_a(body);
    let mut ctx = serde_json::json!({
        "binder": binder,
        "reason": reason,
        "body_type": body_ctor.0,
        "body_ctor": body_ctor.1,
    });
    if let Some(s) = src {
        if let Some(obj) = ctx.as_object_mut() {
            obj.insert(
                "source_type".into(),
                serde_json::Value::String(s.type_name.clone()),
            );
            obj.insert(
                "source_ctor".into(),
                serde_json::Value::String(s.ctor.clone()),
            );
        }
    }
    let msg = match (src, reason) {
        (_, "indeterminate-source-ctor") => format!(
            "reuse-as on `{binder}`: cannot statically determine the source's ctor on this control-flow path; reuse-as requires the source's ctor to be visible from a let or a match arm"
        ),
        (_, "cross-module-body-ctor") => format!(
            "reuse-as on `{binder}`: cross-module body ctors are not yet supported by the shape check"
        ),
        (_, "ctor-not-in-module") => format!(
            "reuse-as on `{binder}`: source or body ctor is not declared in the current module"
        ),
        (Some(s), "field-count-mismatch") => format!(
            "reuse-as on `{binder}`: source ctor `{}` has {} field(s) but body ctor `{}` has {} — reuse requires the same shape",
            s.ctor,
            "?",
            body_ctor.1,
            "?",
        ),
        (Some(s), "field-type-mismatch") => format!(
            "reuse-as on `{binder}`: source ctor `{}` and body ctor `{}` have incompatible per-field LLVM types — reuse requires identical per-slot shapes",
            s.ctor, body_ctor.1
        ),
        _ => format!("reuse-as on `{binder}`: shape mismatch ({reason})"),
    };
    Diagnostic::error("reuse-as-shape-mismatch", msg)
        .with_def(def)
        .with_ctx(ctx)
        .with_suggested_rewrite(
            "drop the reuse-as wrapper; the body alone allocates a fresh box via the normal allocator",
            replacement,
        )
}

#[cfg(test)]
mod tests {
    use super::*;
    use ailang_core::ast::{Ctor, FnDef, Literal};

    fn list_type_def() -> TypeDef {
        TypeDef {
            name: "List".into(),
            vars: vec![],
            ctors: vec![
                Ctor { name: "Nil".into(), fields: vec![] },
                Ctor {
                    name: "Cons".into(),
                    fields: vec![
                        Type::int(),
                        Type::Con { name: "List".into(), args: vec![] },
                    ],
                },
            ],
            doc: None,
            drop_iterative: false,
        }
    }

    fn fn_with_modes(name: &str, modes: Vec<ParamMode>, body: Term) -> Def {
        Def::Fn(FnDef {
            name: name.into(),
            ty: Type::Fn {
                params: modes
                    .iter()
                    .map(|_| Type::Con { name: "List".into(), args: vec![] })
                    .collect(),
                param_modes: modes.clone(),
                ret: Box::new(Type::Con { name: "List".into(), args: vec![] }),
                ret_mode: ParamMode::Implicit,
                effects: vec![],
            },
            params: (0..modes.len()).map(|i| format!("p{i}")).collect(),
            body,
            suppress: vec![],
            doc: None,
        })
    }

    /// Happy-path: `(reuse-as xs (Cons ...))` inside the Cons arm of
    /// a match on xs — both ctors are `Cons`, identical shape. Clean.
    #[test]
    fn reuse_as_same_ctor_in_match_arm_is_clean() {
        // body: (match xs (Nil → Nil) (Cons h t → (reuse-as xs (Cons h t))))
        let body = Term::Match {
            scrutinee: Box::new(Term::Var { name: "p0".into() }),
            arms: vec![
                Arm {
                    pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
                    body: Term::Ctor {
                        type_name: "List".into(),
                        ctor: "Nil".into(),
                        args: vec![],
                    },
                },
                Arm {
                    pat: Pattern::Ctor {
                        ctor: "Cons".into(),
                        fields: vec![
                            Pattern::Var { name: "h".into() },
                            Pattern::Var { name: "t".into() },
                        ],
                    },
                    body: Term::ReuseAs {
                        source: Box::new(Term::Var { name: "p0".into() }),
                        body: Box::new(Term::Ctor {
                            type_name: "List".into(),
                            ctor: "Cons".into(),
                            args: vec![
                                Term::Var { name: "h".into() },
                                Term::Var { name: "t".into() },
                            ],
                        }),
                    },
                },
            ],
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(list_type_def()),
                fn_with_modes("f", vec![ParamMode::Own], body),
            ],
        };
        let diags = check_module(&m);
        assert!(
            diags.is_empty(),
            "happy-path same-ctor reuse-as must be clean; got {diags:?}"
        );
    }

    /// Mismatch: source-ctor is `Cons` (matched in arm) but body-ctor
    /// is `Nil` — different field counts (2 vs 0). Must fire
    /// `reuse-as-shape-mismatch` with reason `field-count-mismatch`.
    #[test]
    fn reuse_as_cons_to_nil_is_shape_mismatch() {
        let body = Term::Match {
            scrutinee: Box::new(Term::Var { name: "p0".into() }),
            arms: vec![
                Arm {
                    pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
                    body: Term::Ctor {
                        type_name: "List".into(),
                        ctor: "Nil".into(),
                        args: vec![],
                    },
                },
                Arm {
                    pat: Pattern::Ctor {
                        ctor: "Cons".into(),
                        fields: vec![
                            Pattern::Var { name: "h".into() },
                            Pattern::Var { name: "t".into() },
                        ],
                    },
                    // BAD: reuse Cons-shaped slot to write Nil.
                    body: Term::ReuseAs {
                        source: Box::new(Term::Var { name: "p0".into() }),
                        body: Box::new(Term::Ctor {
                            type_name: "List".into(),
                            ctor: "Nil".into(),
                            args: vec![],
                        }),
                    },
                },
            ],
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(list_type_def()),
                fn_with_modes("f", vec![ParamMode::Own], body),
            ],
        };
        let diags = check_module(&m);
        assert_eq!(
            diags.len(),
            1,
            "expected one shape-mismatch diagnostic; got {diags:?}"
        );
        let d = &diags[0];
        assert_eq!(d.code, "reuse-as-shape-mismatch");
        assert_eq!(d.def.as_deref(), Some("f"));
        assert_eq!(
            d.ctx.get("reason").and_then(|v| v.as_str()),
            Some("field-count-mismatch")
        );
        assert!(!d.suggested_rewrites.is_empty());
        let rep = &d.suggested_rewrites[0].replacement;
        ailang_surface::parse_term(rep)
            .unwrap_or_else(|e| panic!("suggested rewrite must parse: {rep} ({e})"));
    }

    /// Source-ctor unresolved: `(reuse-as p0 (Cons ...))` outside any
    /// match — `p0` is a fn parameter but never matched, so we have
    /// no path-ctor for it. Conservative reject.
    #[test]
    fn reuse_as_indeterminate_source_ctor_is_rejected() {
        let body = Term::ReuseAs {
            source: Box::new(Term::Var { name: "p0".into() }),
            body: Box::new(Term::Ctor {
                type_name: "List".into(),
                ctor: "Cons".into(),
                args: vec![
                    Term::Lit { lit: Literal::Int { value: 0 } },
                    Term::Ctor {
                        type_name: "List".into(),
                        ctor: "Nil".into(),
                        args: vec![],
                    },
                ],
            }),
        };
        let m = Module {
            schema: ailang_core::SCHEMA.into(),
            name: "t".into(),
            imports: vec![],
            defs: vec![
                Def::Type(list_type_def()),
                fn_with_modes("f", vec![ParamMode::Own], body),
            ],
        };
        let diags = check_module(&m);
        assert_eq!(diags.len(), 1, "got {diags:?}");
        assert_eq!(diags[0].code, "reuse-as-shape-mismatch");
        assert_eq!(
            diags[0].ctx.get("reason").and_then(|v| v.as_str()),
            Some("indeterminate-source-ctor")
        );
    }
}
