lib.rs

#![forbid(unsafe_code)]
// SPDX-License-Identifier: MPL-2.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

//! Ephapax Abstract Syntax Tree
//!
//! Core syntax definitions aligned with the formal Coq semantics.
//! All types derive `serde::Serialize` for JSON AST dump support.

use serde::Serialize;
use smol_str::SmolStr;

/// Variable identifier
pub type Var = SmolStr;

/// Region name
pub type RegionName = SmolStr;

/// Source location span
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
pub struct Span {
    pub start: usize,
    pub end: usize,
}

impl Span {
    pub fn new(start: usize, end: usize) -> Self {
        Self { start, end }
    }

    pub fn dummy() -> Self {
        Self { start: 0, end: 0 }
    }
}

/// Linearity annotation
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "snake_case")]
pub enum Linearity {
    /// Must use exactly once
    Linear,
    /// May use any number of times
    Unrestricted,
}

/// Base (primitive) types
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "snake_case")]
pub enum BaseTy {
    Unit,
    Bool,
    I32,
    I64,
    F32,
    F64,
}

/// Types with region and linearity annotations
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(tag = "kind", content = "value", rename_all = "snake_case")]
pub enum Ty {
    /// Primitive type
    Base(BaseTy),

    /// String allocated in a region
    String(RegionName),

    /// Reference with linearity
    Ref {
        linearity: Linearity,
        inner: Box<Ty>,
    },

    /// Function type A -> B
    Fun { param: Box<Ty>, ret: Box<Ty> },

    /// Product type A * B
    Prod { left: Box<Ty>, right: Box<Ty> },

    /// Sum type A + B
    Sum { left: Box<Ty>, right: Box<Ty> },

    /// Region-scoped type
    Region { name: RegionName, inner: Box<Ty> },

    /// Second-class borrow `&T` (shared) or `&mut T` (exclusive).
    /// `mutable: true` corresponds to `&mut T`; emitted as `ExclBorrow`
    /// in `typedwasm.ownership` (L7 aliasing enforcement).
    Borrow { inner: Box<Ty>, mutable: bool },

    /// Type variable (for polymorphism)
    Var(SmolStr),

    /// Effectful function type: (param -> ret) with [effects].
    ///
    /// An effectful function carries an effect row — the set of effects
    /// it may perform. `effects` is empty for pure functions.
    /// Effect names are SmolStr (e.g. "IO", "State").
    Effectful {
        param: Box<Ty>,
        ret: Box<Ty>,
        /// Effect row: list of effect names this function may perform.
        effects: Vec<SmolStr>,
    },

    /// Universal quantification: forall a. T
    /// Used for polymorphic function types at the core level.
    ForAll { var: SmolStr, body: Box<Ty> },

    /// Unification variable (internal to type checker, never in user code).
    /// Created during instantiation of ForAll types at use sites.
    Unif(u32),

    /// List type [T]
    List(Box<Ty>),

    /// Tuple type (T, U, ...)
    Tuple(Vec<Ty>),
}

impl Ty {
    /// Check if type is linear (must be used exactly once)
    /// Check if this type references a specific region.
    ///
    /// Used by the region-linear fusion: a value whose type references
    /// region r cannot escape r (NoRegionInType from the formal proofs).
    /// This is ORTHOGONAL to the qualifier — it applies to both affine
    /// and linear bindings identically.
    pub fn references_region(&self, region: &RegionName) -> bool {
        match self {
            Ty::String(r) => r == region,
            Ty::Region { name, inner } => name == region || inner.references_region(region),
            Ty::Ref { inner, .. } => inner.references_region(region),
            Ty::Fun { param, ret } => {
                param.references_region(region) || ret.references_region(region)
            }
            Ty::Prod { left, right } | Ty::Sum { left, right } => {
                left.references_region(region) || right.references_region(region)
            }
            Ty::Borrow { inner, .. } => inner.references_region(region),
            Ty::List(inner) => inner.references_region(region),
            Ty::Tuple(elements) => elements.iter().any(|t| t.references_region(region)),
            Ty::ForAll { body, .. } => body.references_region(region),
            Ty::Effectful { param, ret, .. } => {
                param.references_region(region) || ret.references_region(region)
            }
            Ty::Base(_) | Ty::Var(_) | Ty::Unif(_) => false,
        }
    }

    /// Check if type is linear (must be used exactly once).
    ///
    /// Type variables (`Var`, `Unif`) are conservatively non-linear.
    /// Phase 2 will add linearity bounds (`T: Lin`) for generic linear code.
    pub fn is_linear(&self) -> bool {
        match self {
            Ty::String(_) => true,
            Ty::Ref {
                linearity: Linearity::Linear,
                ..
            } => true,
            Ty::Region { inner, .. } => inner.is_linear(),
            Ty::ForAll { body, .. } => body.is_linear(),
            _ => false,
        }
    }

    /// Substitute a type variable with a concrete type.
    pub fn subst_var(&self, var: &SmolStr, replacement: &Ty) -> Ty {
        match self {
            Ty::Var(v) if v == var => replacement.clone(),
            Ty::Var(_) | Ty::Base(_) | Ty::Unif(_) => self.clone(),
            Ty::ForAll { var: v, body } if v == var => self.clone(), // shadowed
            Ty::ForAll { var: v, body } => Ty::ForAll {
                var: v.clone(),
                body: Box::new(body.subst_var(var, replacement)),
            },
            Ty::Fun { param, ret } => Ty::Fun {
                param: Box::new(param.subst_var(var, replacement)),
                ret: Box::new(ret.subst_var(var, replacement)),
            },
            Ty::Prod { left, right } => Ty::Prod {
                left: Box::new(left.subst_var(var, replacement)),
                right: Box::new(right.subst_var(var, replacement)),
            },
            Ty::Sum { left, right } => Ty::Sum {
                left: Box::new(left.subst_var(var, replacement)),
                right: Box::new(right.subst_var(var, replacement)),
            },
            Ty::String(r) => Ty::String(r.clone()),
            Ty::Ref { linearity, inner } => Ty::Ref {
                linearity: *linearity,
                inner: Box::new(inner.subst_var(var, replacement)),
            },
            Ty::Region { name, inner } => Ty::Region {
                name: name.clone(),
                inner: Box::new(inner.subst_var(var, replacement)),
            },
            Ty::Borrow { inner, mutable } => Ty::Borrow {
                inner: Box::new(inner.subst_var(var, replacement)),
                mutable: *mutable,
            },
            Ty::Effectful { param, ret, effects } => Ty::Effectful {
                param: Box::new(param.subst_var(var, replacement)),
                ret: Box::new(ret.subst_var(var, replacement)),
                effects: effects.clone(),
            },
            Ty::List(inner) => Ty::List(Box::new(inner.subst_var(var, replacement))),
            Ty::Tuple(elems) => Ty::Tuple(
                elems.iter().map(|t| t.subst_var(var, replacement)).collect(),
            ),
        }
    }

    /// Check if this type contains a specific unification variable.
    /// Used for the occurs check during unification.
    pub fn contains_unif(&self, id: u32) -> bool {
        match self {
            Ty::Unif(i) => *i == id,
            Ty::Base(_) | Ty::Var(_) | Ty::String(_) => false,
            Ty::Fun { param, ret } => param.contains_unif(id) || ret.contains_unif(id),
            Ty::Prod { left, right } | Ty::Sum { left, right } => {
                left.contains_unif(id) || right.contains_unif(id)
            }
            Ty::Ref { inner, .. }
            | Ty::Region { inner, .. }
            | Ty::Borrow { inner, .. }
            | Ty::List(inner)
            | Ty::ForAll { body: inner, .. } => inner.contains_unif(id),
            Ty::Effectful { param, ret, .. } => {
                param.contains_unif(id) || ret.contains_unif(id)
            }
            Ty::Tuple(elems) => elems.iter().any(|t| t.contains_unif(id)),
        }
    }

    /// Resolve all unification variables using the given solution map.
    pub fn resolve(&self, solutions: &std::collections::HashMap<u32, Ty>) -> Ty {
        match self {
            Ty::Unif(id) => {
                if let Some(solution) = solutions.get(id) {
                    solution.resolve(solutions)
                } else {
                    self.clone()
                }
            }
            Ty::Base(_) | Ty::Var(_) | Ty::String(_) => self.clone(),
            Ty::Fun { param, ret } => Ty::Fun {
                param: Box::new(param.resolve(solutions)),
                ret: Box::new(ret.resolve(solutions)),
            },
            Ty::Prod { left, right } => Ty::Prod {
                left: Box::new(left.resolve(solutions)),
                right: Box::new(right.resolve(solutions)),
            },
            Ty::Sum { left, right } => Ty::Sum {
                left: Box::new(left.resolve(solutions)),
                right: Box::new(right.resolve(solutions)),
            },
            Ty::Ref { linearity, inner } => Ty::Ref {
                linearity: *linearity,
                inner: Box::new(inner.resolve(solutions)),
            },
            Ty::Region { name, inner } => Ty::Region {
                name: name.clone(),
                inner: Box::new(inner.resolve(solutions)),
            },
            Ty::Borrow { inner, mutable } => Ty::Borrow {
                inner: Box::new(inner.resolve(solutions)),
                mutable: *mutable,
            },
            Ty::ForAll { var, body } => Ty::ForAll {
                var: var.clone(),
                body: Box::new(body.resolve(solutions)),
            },
            Ty::Effectful { param, ret, effects } => Ty::Effectful {
                param: Box::new(param.resolve(solutions)),
                ret: Box::new(ret.resolve(solutions)),
                effects: effects.clone(),
            },
            Ty::List(inner) => Ty::List(Box::new(inner.resolve(solutions))),
            Ty::Tuple(elems) => Ty::Tuple(
                elems.iter().map(|t| t.resolve(solutions)).collect(),
            ),
        }
    }
}

/// Literal values
#[derive(Debug, Clone, PartialEq, Serialize)]
#[serde(tag = "kind", content = "value", rename_all = "snake_case")]
pub enum Literal {
    Unit,
    Bool(bool),
    I32(i32),
    I64(i64),
    F32(f32),
    F64(f64),
    String(String),
}

/// Binary operators
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "snake_case")]
pub enum BinOp {
    // Arithmetic
    Add,
    Sub,
    Mul,
    Div,
    Mod,
    // Comparison
    Lt,
    Le,
    Gt,
    Ge,
    Eq,
    Ne,
    // Logical
    And,
    Or,
}

/// Unary operators
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "snake_case")]
pub enum UnaryOp {
    /// Logical negation
    Not,
    /// Arithmetic negation
    Neg,
}

/// Pattern for destructuring.
///
/// Used in core `ExprKind::Match` arms. Mirror of
/// `ephapax_surface::Pattern` so the core parser's direct path can
/// build structured patterns without round-tripping through surface.
#[derive(Debug, Clone, PartialEq, Serialize)]
#[serde(tag = "kind", content = "value", rename_all = "snake_case")]
pub enum Pattern {
    /// Wildcard _
    Wildcard,
    /// Variable binding
    Var(Var),
    /// Literal value — matches an exact constant (added ephapax#61).
    Literal(Literal),
    /// Pair destructuring (p1, p2)
    Pair(Box<Pattern>, Box<Pattern>),
    /// Unit ()
    Unit,
    /// Tuple pattern (p1, p2, p3, ...)
    Tuple(Vec<Pattern>),
    /// Constructor pattern: `Some(x)`, `None`, `Ok((a, b))` (added
    /// ephapax#61 for core `match` parsing).
    Constructor {
        ctor: SmolStr,
        args: Vec<Pattern>,
    },
}

impl Pattern {
    /// Collect every variable bound by this pattern (recursively).
    /// Wildcards, literals, and unit bind nothing; `Var` binds itself;
    /// constructor/tuple/pair patterns aggregate from sub-patterns.
    pub fn bound_vars(&self) -> Vec<Var> {
        match self {
            Pattern::Wildcard | Pattern::Literal(_) | Pattern::Unit => Vec::new(),
            Pattern::Var(v) => vec![v.clone()],
            Pattern::Constructor { args, .. } => {
                args.iter().flat_map(Pattern::bound_vars).collect()
            }
            Pattern::Pair(l, r) => {
                let mut out = l.bound_vars();
                out.extend(r.bound_vars());
                out
            }
            Pattern::Tuple(ps) => ps.iter().flat_map(Pattern::bound_vars).collect(),
        }
    }
}

/// Resume mode for effect handler continuations.
///
/// Controls whether the continuation can be called once or multiple times.
/// Critical for linear safety: `resume(multi)` is a type error if the
/// continuation captures linear values.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "snake_case")]
pub enum ResumeMode {
    /// One-shot: continuation called at most once. Safe with linear captures.
    Once,
    /// Multi-shot: continuation may be called multiple times.
    /// Type error if linear values are captured.
    Multi,
}

/// A clause in an effect handler.
#[derive(Debug, Clone, PartialEq, Serialize)]
pub struct HandlerClause {
    /// Effect operation name. Empty string = return clause.
    pub op: SmolStr,
    /// Parameter names bound in this clause.
    pub params: Vec<Var>,
    /// Resume mode (None for return clause which has no resume).
    pub resume_mode: Option<ResumeMode>,
    /// Handler body expression.
    pub body: Expr,
}

/// Expressions
#[derive(Debug, Clone, PartialEq, Serialize)]
pub struct Expr {
    pub kind: ExprKind,
    pub span: Span,
}

#[derive(Debug, Clone, PartialEq, Serialize)]
#[serde(tag = "node", rename_all = "snake_case")]
pub enum ExprKind {
    /// Literal value
    Lit(Literal),

    /// Variable reference
    Var(Var),

    // ===== String operations =====
    /// String allocation: String.new@r("...")
    StringNew { region: RegionName, value: String },

    /// String concatenation (consumes both)
    StringConcat { left: Box<Expr>, right: Box<Expr> },

    /// String length (borrows)
    StringLen(Box<Expr>),

    // ===== Bindings =====
    /// Let binding: let x = e1 in e2
    Let {
        name: Var,
        ty: Option<Ty>,
        value: Box<Expr>,
        body: Box<Expr>,
    },

    /// Linear let binding: let! x = e1 in e2
    LetLin {
        name: Var,
        ty: Option<Ty>,
        value: Box<Expr>,
        body: Box<Expr>,
    },

    // ===== Functions =====
    /// Lambda: fn(x: T) -> e
    Lambda {
        param: Var,
        param_ty: Ty,
        body: Box<Expr>,
    },

    /// Application: e1 e2
    App { func: Box<Expr>, arg: Box<Expr> },

    // ===== Products =====
    /// Pair: (e1, e2)
    Pair { left: Box<Expr>, right: Box<Expr> },

    /// First projection: e.0
    Fst(Box<Expr>),

    /// Second projection: e.1
    Snd(Box<Expr>),

    // ===== Sums =====
    /// Left injection: inl[T] e
    Inl { ty: Ty, value: Box<Expr> },

    /// Right injection: inr[T] e
    Inr { ty: Ty, value: Box<Expr> },

    /// Case analysis
    Case {
        scrutinee: Box<Expr>,
        left_var: Var,
        left_body: Box<Expr>,
        right_var: Var,
        right_body: Box<Expr>,
    },

    /// Multi-arm pattern match: `match e of | P1 => e1 | P2 => e2 ... end`.
    ///
    /// Mirror of `SurfaceExprKind::Match`, kept in the core AST so the
    /// core parser's direct path can preserve structured pattern matching
    /// without having to round-trip through the surface→desugar→case
    /// lowering. The surface path still produces `Case` via desugar;
    /// this variant exists for the core-parser-direct path and tooling.
    Match {
        scrutinee: Box<Expr>,
        arms: Vec<MatchArm>,
    },

    // ===== Control flow =====
    /// Conditional: if e1 then e2 else e3
    If {
        cond: Box<Expr>,
        then_branch: Box<Expr>,
        else_branch: Box<Expr>,
    },

    // ===== Regions =====
    /// Region scope: region r { e }
    Region { name: RegionName, body: Box<Expr> },

    // ===== Borrowing =====
    /// Create borrow: `&e` (shared) or `&mut e` (exclusive).
    /// `mutable: true` requires an `&mut T` parameter type and produces
    /// an `ExclBorrow` ownership classification at codegen.
    Borrow { inner: Box<Expr>, mutable: bool },

    /// Dereference: *e
    Deref(Box<Expr>),

    // ===== Resource management =====
    /// Explicit drop: drop(e)
    Drop(Box<Expr>),

    /// Explicit copy (unrestricted only): copy(e)
    Copy(Box<Expr>),

    // ===== Blocks =====
    /// Sequence of expressions
    Block(Vec<Expr>),

    // ===== Foreign Function Interface =====
    /// FFI call: __ffi("symbol_name", arg1, arg2, ...)
    ///
    /// Calls a C ABI function from a loaded shared library (typically
    /// the Zig FFI layer). The symbol name is resolved at link time.
    /// Arguments are marshalled to C-compatible types.
    FFI {
        /// The C symbol name to call (e.g. "gossamer_create")
        symbol: String,
        /// Arguments to pass to the foreign function
        args: Vec<Expr>,
    },

    // ===== Effects =====
    /// Perform an effect operation: `perform Op(args...)`
    Perform {
        /// Effect operation name (e.g. "print", "get", "put")
        op: SmolStr,
        /// Arguments to the operation
        args: Vec<Expr>,
    },

    /// Handle effects: `handle e with { return(x) => ..., |Op(args, resume) => ... }`
    Handle {
        /// The expression whose effects are handled
        body: Box<Expr>,
        /// Handler clauses: (op_name, param_names, resume_mode, handler_body)
        /// Empty op_name = return clause.
        clauses: Vec<HandlerClause>,
    },

    // ===== Operators =====
    /// Binary operation: e1 op e2
    BinOp {
        op: BinOp,
        left: Box<Expr>,
        right: Box<Expr>,
    },

    /// Unary operation: op e
    UnaryOp { op: UnaryOp, operand: Box<Expr> },

    // ===== Lists and Tuples (for self-hosting compiler) =====
    /// List literal [e1, e2, ...]
    ListLit(Vec<Expr>),

    /// List index access list[idx]
    ListIndex { list: Box<Expr>, index: Box<Expr> },

    /// Tuple literal (e1, e2, e3, ...)
    TupleLit(Vec<Expr>),

    /// Tuple field access tuple.N
    TupleIndex { tuple: Box<Expr>, index: usize },
}

impl Expr {
    pub fn new(kind: ExprKind, span: Span) -> Self {
        Self { kind, span }
    }

    pub fn dummy(kind: ExprKind) -> Self {
        Self {
            kind,
            span: Span::dummy(),
        }
    }
}

/// A single arm in an `ExprKind::Match` expression (added ephapax#61).
#[derive(Debug, Clone, PartialEq, Serialize)]
pub struct MatchArm {
    pub pattern: Pattern,
    /// Optional guard `if e`.
    pub guard: Option<Box<Expr>>,
    pub body: Expr,
}

/// Top-level declarations
#[derive(Debug, Clone, PartialEq, Serialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum Decl {
    /// Function definition, optionally polymorphic.
    ///
    /// `type_params` lists universally quantified type variables (e.g. `<T, U>`).
    /// Empty for monomorphic functions.
    Fn {
        name: Var,
        #[serde(skip_serializing_if = "is_private")]
        visibility: Visibility,
        #[serde(skip_serializing_if = "Vec::is_empty")]
        type_params: Vec<SmolStr>,
        params: Vec<(Var, Ty)>,
        ret_ty: Ty,
        body: Expr,
    },

    /// Type alias
    Type {
        name: Var,
        #[serde(skip_serializing_if = "is_private")]
        visibility: Visibility,
        ty: Ty,
    },

    /// Module-level constant binding: `let NAME = expr`
    Const {
        name: Var,
        ty: Option<Ty>,
        value: Expr,
    },

    /// Foreign function and type declarations: `extern "abi" { ... }`.
    ///
    /// Items inside the block have no body — they declare signatures
    /// that resolve to host imports at codegen time. The `abi` string
    /// names the linkage target (e.g. `"gossamer"`, `"c"`, `"wasm"`).
    /// Extern types are opaque to the type checker (no constructors,
    /// no destructors known); extern fns get an ambient binding with
    /// the declared type.
    Extern {
        abi: String,
        items: Vec<ExternItem>,
    },

    /// Algebraic data type declaration: `data Name(a, b) = C1 | C2(T) | ...`.
    ///
    /// Preserves the structured shape (variant names + payloads) for the
    /// surface IR / LSP / tooling layers. The runtime path
    /// (surface → desugar → core) does not use this variant — data
    /// semantics flow through the registry-based encoding in
    /// `ephapax-desugar`. The core parser produces `Decl::Data` directly
    /// (instead of folding into `Decl::Type` with a binary-sum encoding
    /// that discarded constructor names).
    Data {
        name: Var,
        #[serde(skip_serializing_if = "Vec::is_empty")]
        type_params: Vec<SmolStr>,
        constructors: Vec<ConstructorDef>,
    },
}

/// A single constructor inside a `data` declaration.
///
/// Mirror of `ephapax_surface::ConstructorDef` but with core `Ty`
/// field types instead of `SurfaceTy`.
#[derive(Debug, Clone, PartialEq, Serialize)]
pub struct ConstructorDef {
    /// Constructor name (e.g. `"Some"`, `"None"`).
    pub name: Var,
    /// Payload types (empty for nullary constructors).
    #[serde(skip_serializing_if = "Vec::is_empty")]
    pub fields: Vec<Ty>,
}

/// A single declaration inside an `extern "abi" { ... }` block.
///
/// Extern items declare signatures only — no bodies. The checker
/// registers them as ambient bindings; codegen lowers fn items to
/// wasm `import` directives and treats type items as opaque externs.
#[derive(Debug, Clone, PartialEq, Serialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum ExternItem {
    /// `type Foo` — declares an opaque foreign type.
    Type { name: Var },
    /// `fn name(p1: T1, p2: T2): R` — declares a foreign function
    /// signature.
    Fn {
        name: Var,
        params: Vec<(Var, Ty)>,
        ret_ty: Ty,
    },
}

/// Helper for serde skip_serializing_if.
/// Visibility of a declaration.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "snake_case")]
pub enum Visibility {
    /// Accessible from other modules.
    Public,
    /// Only accessible within this module (default).
    Private,
}

impl Default for Visibility {
    fn default() -> Self {
        Visibility::Private
    }
}

/// Helper for serde skip_serializing_if.
fn is_private(v: &Visibility) -> bool {
    *v == Visibility::Private
}

/// An import declaration: `import module_name` or `import module_name (name1, name2)`.
#[derive(Debug, Clone, PartialEq, Serialize)]
pub struct Import {
    /// The module to import from.
    pub module: SmolStr,
    /// Specific names to import. Empty = import all public names.
    pub names: Vec<SmolStr>,
}

/// A complete module
#[derive(Debug, Clone, PartialEq, Serialize)]
pub struct Module {
    pub name: SmolStr,
    /// Import declarations.
    #[serde(skip_serializing_if = "Vec::is_empty")]
    pub imports: Vec<Import>,
    pub decls: Vec<Decl>,
}

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

    #[test]
    fn string_is_linear() {
        let ty = Ty::String("r".into());
        assert!(ty.is_linear());
    }

    #[test]
    fn base_is_unrestricted() {
        let ty = Ty::Base(BaseTy::I32);
        assert!(!ty.is_linear());
    }

    // === Coq ↔ Rust bridge for `is_linear` (proof-debt P28) ===
    //
    // The tests below pin the truth table for every kernel-subset
    // variant of `Ty`, where "kernel" means the subset of Rust `Ty`
    // that corresponds to Coq's `ty` inductive (formal/Syntax.v:48-85).
    //
    // The cross-language specification lives at
    // docs/coq-rust-bridge/is_linear_ty.adoc; the canonical Coq
    // definition at formal/Syntax.v:467-473.
    //
    // Maintenance contract: any change to `Ty::is_linear()` MUST
    // be mirrored in formal/Syntax.v `is_linear_ty` (and the bridge
    // doc updated). If you add a new constructor to either side,
    // add a matching test below.

    fn boxed_base() -> Box<Ty> {
        Box::new(Ty::Base(BaseTy::I32))
    }

    #[test]
    fn coq_bridge_base_all_six_unrestricted() {
        // Coq: TBase _ falls through → false for every base.
        for base in [
            BaseTy::Unit,
            BaseTy::Bool,
            BaseTy::I32,
            BaseTy::I64,
            BaseTy::F32,
            BaseTy::F64,
        ] {
            assert!(
                !Ty::Base(base.clone()).is_linear(),
                "Coq bridge: TBase {base:?} should be NOT linear"
            );
        }
    }

    #[test]
    fn coq_bridge_string_always_linear() {
        // Coq: TString _ → true. Region irrelevant.
        assert!(Ty::String("r0".into()).is_linear());
        assert!(Ty::String("r1".into()).is_linear());
    }

    #[test]
    fn coq_bridge_ref_linearity_decides() {
        // Coq: TRef Lin _ → true; TRef Unr _ → false.
        let inner = boxed_base();
        let lin_ref = Ty::Ref {
            linearity: Linearity::Linear,
            inner: inner.clone(),
        };
        let unr_ref = Ty::Ref {
            linearity: Linearity::Unrestricted,
            inner,
        };
        assert!(lin_ref.is_linear(), "Coq bridge: TRef Lin _ → true");
        assert!(!unr_ref.is_linear(), "Coq bridge: TRef Unr _ → false");
    }

    #[test]
    fn coq_bridge_region_recurses_on_inner() {
        // Coq: TRegion _ T' → is_linear_ty T'.
        let lin_inner = Ty::String("r".into());
        let unr_inner = Ty::Base(BaseTy::I32);
        let lin_region = Ty::Region {
            name: "r".into(),
            inner: Box::new(lin_inner),
        };
        let unr_region = Ty::Region {
            name: "r".into(),
            inner: Box::new(unr_inner),
        };
        assert!(lin_region.is_linear(), "Coq bridge: TRegion _ (linear) → recurse");
        assert!(!unr_region.is_linear(), "Coq bridge: TRegion _ (unrestricted) → recurse");
    }

    #[test]
    fn coq_bridge_fun_prod_sum_borrow_fallthrough_unrestricted() {
        // Coq: TFun / TProd / TSum / TBorrow all fall through → false
        // regardless of constituent linearity. Linearity of CAPTURED
        // resources is tracked at the judgment level (T_Lam_L1_*'s
        // body context discipline), not at the type shape.
        let lin = Box::new(Ty::String("r".into()));
        let unr = boxed_base();

        let fun = Ty::Fun {
            param: lin.clone(),
            ret: unr.clone(),
        };
        let prod = Ty::Prod {
            left: lin.clone(),
            right: unr.clone(),
        };
        let sum = Ty::Sum {
            left: lin.clone(),
            right: unr.clone(),
        };
        let borrow = Ty::Borrow {
            inner: lin.clone(),
            mutable: false,
        };

        assert!(!fun.is_linear(), "Coq bridge: TFun is NOT linear");
        assert!(!prod.is_linear(), "Coq bridge: TProd is NOT linear");
        assert!(!sum.is_linear(), "Coq bridge: TSum is NOT linear");
        assert!(!borrow.is_linear(), "Coq bridge: TBorrow is NOT linear");
    }

    #[test]
    fn coq_bridge_effectful_fallthrough_unrestricted() {
        // Coq: TFunEff _ _ _ _ falls through → false.
        let effectful = Ty::Effectful {
            param: Box::new(Ty::String("r".into())),
            ret: boxed_base(),
            effects: vec!["IO".into()],
        };
        assert!(!effectful.is_linear(), "Coq bridge: TFunEff is NOT linear");
    }

    #[test]
    fn surface_only_forall_recurses_on_body() {
        // Rust-only behaviour: ForAll recurses on body.
        // The Coq kernel has no TForAll; this is documented in
        // docs/coq-rust-bridge/is_linear_ty.adoc as a surface-side
        // extension. Elaboration instantiates ForAll before lowering
        // to the kernel, so the bridge holds after elaboration.
        let lin_body = Ty::ForAll {
            var: "T".into(),
            body: Box::new(Ty::String("r".into())),
        };
        let unr_body = Ty::ForAll {
            var: "T".into(),
            body: boxed_base(),
        };
        assert!(lin_body.is_linear(), "ForAll over a linear body is linear");
        assert!(!unr_body.is_linear(), "ForAll over an unrestricted body is unrestricted");
    }

    #[test]
    fn surface_only_var_unif_list_tuple_unrestricted() {
        // Conservative non-linear for unsubstituted type variables
        // (see is_linear() docstring). Coq kernel has no equivalent —
        // surface-only.
        assert!(!Ty::Var("T".into()).is_linear());
        assert!(!Ty::Unif(0).is_linear());
        assert!(!Ty::List(Box::new(Ty::String("r".into()))).is_linear());
        assert!(
            !Ty::Tuple(vec![Ty::String("r".into()), Ty::Base(BaseTy::I32)]).is_linear()
        );
    }
}