(* SPDX-License-Identifier: MPL-2.0 *)
(* SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) *)

(** Bidirectional type checker for AffineScript.

    Implements a Hindley-Milner-style type checker with bidirectional
    mode switching (synth/check), let-polymorphism via levels, and
    integration with the unification engine ({!Unify}).

    Design:
    - [synth]: infer a type for an expression (mode ⇒)
    - [check]: verify an expression against an expected type (mode ⇐)
    - At application sites we synth the function and check the argument
    - At let-bindings we generalize to produce polymorphic schemes
    - Effect annotations are unified alongside types

    Limitations (Phase 1):
    - Quantity checking is a separate pass (see {!Quantity})
    - Refinement types are checked structurally, not via SMT
    - Trait resolution uses name matching (see {!Trait})
    - Effect inference is basic: we unify declared effects
*)

open Types
open Ast

let string_of_binary_op = function
  | OpAdd -> "+"
  | OpSub -> "-"
  | OpMul -> "*"
  | OpDiv -> "/"
  | OpMod -> "%"
  | OpEq -> "=="
  | OpNe -> "!="
  | OpLt -> "<"
  | OpLe -> "<="
  | OpGt -> ">"
  | OpGe -> ">="
  | OpAnd -> "&&"
  | OpOr -> "||"
  | OpBitAnd -> "&"
  | OpBitOr -> "|"
  | OpBitXor -> "^"
  | OpShl -> "<<"
  | OpShr -> ">>"
  | OpConcat -> "++"

let rec expr_summary (expr : expr) : string =
  match expr with
  | ExprVar id -> id.name
  | ExprLit (LitBool (b, _)) -> string_of_bool b
  | ExprLit (LitInt (i, _)) -> string_of_int i
  | ExprLit (LitFloat (f, _)) -> string_of_float f
  | ExprLit (LitChar (c, _)) -> Printf.sprintf "%c" c
  | ExprLit (LitString (s, _)) -> Printf.sprintf "\"%s\"" s
  | ExprLit (LitUnit _) -> "()"
  | ExprBinary (l, op, r) ->
    Printf.sprintf "(%s %s %s)" (expr_summary l) (string_of_binary_op op) (expr_summary r)
  | ExprUnary (_, inner) -> expr_summary inner
  | ExprApp (f, args) ->
    let fdesc = expr_summary f in
    let argsdesc = match args with
      | [] -> ""
      | hd :: _ -> expr_summary hd
    in
    Printf.sprintf "%s(%s...)" fdesc argsdesc
  | ExprField (e, id) ->
    Printf.sprintf "%s.%s" (expr_summary e) id.name
  | ExprTuple _ -> "<tuple>"
  | ExprRecord _ -> "<record>"
  | ExprBlock _ -> "{...}"
  | ExprIf _ -> "if(...)"
  | ExprLet _ -> "let(...)"
  | ExprMatch _ -> "match(...)"
  | ExprRowRestrict _ -> "row_restrict"
  | ExprTupleIndex _ -> "tuple_index"
  | ExprIndex _ -> "index"
  | ExprArray _ -> "array"
  | ExprReturn _ -> "return"
  | ExprBreak _ -> "break"
  | ExprContinue _ -> "continue"
  | ExprTry _ -> "try"
  | ExprHandle _ -> "handle"
  | ExprResume _ -> "resume"
  | ExprUnsafe _ -> "unsafe"
  | ExprVariant (id, _) -> id.name
  | ExprSpan (inner, _) -> expr_summary inner
  | _ -> "<expr>"

(** {1 Errors} *)

(** Type checking error *)
type type_error =
  | UnboundVariable of string
  | TypeMismatch of { expected : ty; got : ty }
  | OccursCheck of string * ty
  | NotImplemented of string
  | ArityMismatch of { name : string; expected : int; got : int }
  | NotAFunction of ty
  | FieldNotFound of { field : string; record_ty : ty }
  | TupleIndexOutOfBounds of { index : int; length : int }
  | DuplicateField of string
  | UnificationError of Unify.unify_error
  | PatternTypeMismatch of string
  | BranchTypeMismatch of { then_ty : ty; else_ty : ty }
  | QuantityError of Quantity.quantity_error * Span.t
      (** QTT quantity violation detected after type checking. *)
  | UnknownEffect of string
      (** Effect name not in the v1 registry, not a legacy alias, and
          not a user-declared effect (issue #59). *)
  | EffectNotDeclared of { inferred : string; declared : string }
      (** The function body performs an effect (v1: `Partial`, from a
          catch-less `try` / the `?` desugar) that is absent from the
          function's explicitly declared effect row (issue #59). Only
          raised when a row is declared; an undeclared row stays
          permissive under tracking-only v1. *)
  | UnknownModule of string
      (** A module-qualified type/effect reference (`Mod.T` / `Mod::E`)
          named a module qualifier not introduced by any `use` in the
          current program (ADR-014, #228). Symmetric to the value-path
          resolution check done by #178. *)
  | NotInLoop of string
      (** `break` / `continue` used outside any enclosing loop body
          (issue #459). The string carries the keyword name for the
          error message. *)
  | TraitCoherenceError of string
      (** Two impls of the same trait have overlapping (unifiable) self
          types, so method resolution would be ambiguous (#559). The string
          is the human-readable overlap description. *)

(* Known exports of stdlib/prelude.affine. Mirrors the same list in
   lib/face.ml — when an UnboundVariable fires at type-check time with
   one of these names, the formatter suggests `use prelude::{...}`.
   Same discoverability fix as the resolver path; the typechecker has
   its own miss path (e.g. match arms reference unbound constructors
   that the resolver missed). Keep in sync with stdlib/prelude.affine. *)
let prelude_exports = [
  "Option"; "Result";
  "Some"; "None"; "Ok"; "Err";
  "map"; "filter"; "fold"; "contains";
  "sum"; "product"; "min"; "max"; "clamp";
  "not"; "all"; "any"; "range"; "repeat";
]

let prelude_hint (name : string) : string =
  if List.mem name prelude_exports then
    Printf.sprintf "\n  hint: `%s` is defined in `stdlib/prelude.affine` — add `use prelude::{%s};` (or `use prelude::*;`) at the top of the file."
      name name
  else ""

(** Format a type error for human consumption. *)
let show_type_error = function
  | UnboundVariable v -> "Unbound variable: " ^ v ^ prelude_hint v
  | TypeMismatch { expected; got } ->
    Printf.sprintf "Type mismatch: expected %s, got %s"
      (ty_to_string expected) (ty_to_string got)
  | OccursCheck (v, ty) ->
    Printf.sprintf "Occurs check: %s in %s" v (ty_to_string ty)
  | NotImplemented msg -> "Not implemented: " ^ msg
  | ArityMismatch { name; expected; got } ->
    Printf.sprintf "Function %s expects %d arguments, got %d" name expected got
  | NotAFunction ty ->
    Printf.sprintf "Expected a function type, got %s" (ty_to_string ty)
  | FieldNotFound { field; record_ty } ->
    Printf.sprintf "Field '%s' not found in type %s" field (ty_to_string record_ty)
  | TupleIndexOutOfBounds { index; length } ->
    Printf.sprintf "Tuple index %d out of bounds (tuple has %d elements)" index length
  | DuplicateField f ->
    Printf.sprintf "Duplicate field: %s" f
  | UnificationError ue ->
    Printf.sprintf "Unification error: %s" (Unify.show_unify_error ue)
  | PatternTypeMismatch msg ->
    Printf.sprintf "Pattern type mismatch: %s" msg
  | BranchTypeMismatch { then_ty; else_ty } ->
    Printf.sprintf "Branch type mismatch: then-branch has type %s, else-branch has type %s"
      (ty_to_string then_ty) (ty_to_string else_ty)
  | QuantityError (qerr, _span) ->
    Printf.sprintf "Quantity error: %s" (Quantity.format_quantity_error qerr)
  | UnknownEffect name ->
    Printf.sprintf
      "Unknown effect '%s'. Use a v1 effect (%s), a reserved name (%s), \
       or declare it with `effect %s;`."
      name
      (String.concat ", " Effect.v1_effects)
      (String.concat ", " Effect.reserved_effects)
      name
  | EffectNotDeclared { inferred; declared } ->
    Printf.sprintf
      "Effect mismatch (issue #59): the function body performs %s but its \
       declared effect row is /{%s}. A catch-less `try` / the `?` operator \
       performs `Partial` — add it to the row, e.g. /{%s}."
      inferred declared
      (if declared = "" then "Partial" else declared ^ ", Partial")
  | UnknownModule m ->
    Printf.sprintf
      "Unknown module '%s' in qualified type/effect reference (ADR-014, #228). \
       Add `use %s;` to bring the module into scope, or `use %s::{Item};` to \
       import items unqualified."
      m m m
  | NotInLoop kw ->
    Printf.sprintf
      "`%s` used outside a loop body (#459). `break` and `continue` must be \
       lexically enclosed by a `while` or `for` loop."
      kw
  | TraitCoherenceError msg ->
    Printf.sprintf
      "Trait coherence violation (#559): %s. Two implementations whose self \
       types can unify would make method resolution ambiguous; remove or \
       narrow one of the overlapping impls."
      msg

let format_type_error = show_type_error

(** Raised by [lower_effect_expr] for an unknown effect name; caught at
    the [check_program] boundary and converted to [UnknownEffect]
    (lowering is not in the result monad). *)
exception Effect_validation_error of string

(** Raised by [strip_module_qualifier] when a qualified type/effect
    reference names a module that no `use` decl introduced; caught at
    [check_program] and converted to [UnknownModule]. Mirrors the
    [Effect_validation_error] exception/boundary pattern. *)
exception Module_resolution_error of string

(** {1 Context} *)

(** Type checking context.

    [level] tracks the current let-nesting depth for generalization.
    Variables bound at a deeper level than the current one can be
    generalized when we exit back to a shallower level. *)
type context = {
  var_types : (Symbol.symbol_id, scheme) Hashtbl.t;
  (** Symbol-ID-keyed type map — used by resolve.ml for imports *)
  name_types : (string, scheme) Hashtbl.t;
  (** Name-keyed type map — used by the type checker for lookups *)
  type_env : (string, ty) Hashtbl.t;
  (** Named type constructors → their definition types *)
  constructor_env : (string, ty) Hashtbl.t;
  (** Data constructors (enum variants) → their function types *)
  symbols : Symbol.t;
  mutable level : int;
  mutable current_eff : eff;
  (** The current effect context — unified with declared effects *)
  trait_registry : Trait.trait_registry;
  (** Trait registry — stores trait definitions and impls for dispatch *)
  declared_effects : (string, unit) Hashtbl.t;
  (** User-declared effect names (`effect <name>;`). Consulted by
      [lower_effect_expr] alongside the v1 registry (issue #59). *)
  call_effects : (int, eff) Hashtbl.t;
  (** ADR-016 / #234 S2b: per-call-site effect rows, keyed by the
      shared [Effect_sites] ordinal. Populated after a successful check
      pass; the value is the callee's declared effect row (EPure when
      the callee is not a statically-named function). Built here but
      NOT yet consulted by codegen — S3 threads & switches the WasmGC
      CPS boundary predicate onto it (the structural recogniser remains
      the sound table-miss fallback). *)
  module_quals : (string, unit) Hashtbl.t;
  (** ADR-014 / #228: set of module-name qualifiers introduced by
      [`use Mod;`] (ImportSimple) decls in the current program. Used by
      [lower_type_expr]/[lower_effect_expr] to strip a qualified
      `Mod::T` reference back to `T` when `Mod` is in scope, or raise
      [Module_resolution_error] when it isn't. Symmetric to the
      value-path lowering done by [Resolve.lower_qualified_value_paths]
      (#178). Populated at [check_program] entry from
      [prog.prog_imports]. *)
  mutable in_loop : bool;
  (** #459: tracks whether the synth/check walker is currently inside
      a loop body. Set true on entry to a [StmtWhile]/[StmtFor] body,
      restored on exit. Read by [ExprBreak]/[ExprContinue] handlers to
      reject loop-control expressions outside of a loop with
      [NotInLoop]. *)
}

type 'a result = ('a, type_error) Result.t

let ( let* ) = Result.bind

(** Lift a unification result into a type-checking result. *)
let unify_or_err (t1 : ty) (t2 : ty) : unit result =
  match Unify.unify t1 t2 with
  | Ok () -> Ok ()
  | Error ue -> Error (UnificationError ue)

let unify_eff_or_err (e1 : eff) (e2 : eff) : unit result =
  match Unify.unify_eff e1 e2 with
  | Ok () -> Ok ()
  | Error ue -> Error (UnificationError ue)

(** {1 Context management} *)

let create_context (symbols : Symbol.t) : context =
  {
    var_types = Hashtbl.create 128;
    name_types = Hashtbl.create 128;
    type_env = Hashtbl.create 64;
    constructor_env = Hashtbl.create 64;
    symbols;
    level = 0;
    current_eff = fresh_effvar 0;
    trait_registry = Trait.create_registry ();
    declared_effects = Hashtbl.create 16;
    call_effects = Hashtbl.create 64;
    module_quals = Hashtbl.create 4;
    in_loop = false;
  }

(** ADR-014 / #228. Strip a leading `Mod::` qualifier from a folded
    type/effect name. Returns the unqualified tail when `Mod` was
    introduced by a `use Mod;` decl; raises [Module_resolution_error]
    when the qualifier is unknown; passes the name through unchanged
    when not qualified. Only the first `::`-separated head is treated
    as a module qualifier — deeper segments (`A::B::T`) carry through
    unchanged so a nested module reference still errors symmetrically
    when its head isn't in scope. *)
let strip_module_qualifier (ctx : context) (name : string) : string =
  match String.index_opt name ':' with
  | None -> name
  | Some _ ->
    let parts = String.split_on_char ':' name
                |> List.filter (fun s -> s <> "") in
    (match parts with
     | head :: (_ :: _ as rest) ->
       if Hashtbl.mem ctx.module_quals head then
         String.concat "::" rest
       else
         raise (Module_resolution_error head)
     | _ -> name)

(** Enter a deeper let-level. *)
let enter_level (ctx : context) : unit =
  ctx.level <- ctx.level + 1

(** Exit a let-level. *)
let exit_level (ctx : context) : unit =
  ctx.level <- ctx.level - 1

(** Bind a variable to a monomorphic type (no generalization). *)
let bind_var (ctx : context) (name : string) (ty : ty) : unit =
  let sc = { sc_tyvars = []; sc_effvars = []; sc_rowvars = []; sc_body = ty } in
  Hashtbl.replace ctx.name_types name sc

(** Bind a variable to a polymorphic scheme. *)
let bind_scheme (ctx : context) (name : string) (sc : scheme) : unit =
  Hashtbl.replace ctx.name_types name sc

(** {1 Instantiation and generalization} *)

(** Instantiate a polymorphic scheme by replacing bound variables
    with fresh unification variables at the current level. *)
let instantiate (level : int) (sc : scheme) : ty =
  let subst = Hashtbl.create 8 in
  (* Create fresh type variables for each quantified tyvar *)
  List.iter (fun (tv, _kind) ->
    let fresh = fresh_tyvar level in
    Hashtbl.replace subst tv fresh
  ) sc.sc_tyvars;
  (* Apply substitution to the body *)
  let rec apply_subst ty =
    match repr ty with
    | TVar r ->
      begin match !r with
        | Unbound (v, _) ->
          begin match Hashtbl.find_opt subst v with
            | Some fresh -> fresh
            | None -> ty
          end
        | Link t -> apply_subst t
      end
    | TCon _ -> ty
    | TApp (t, args) ->
      TApp (apply_subst t, List.map apply_subst args)
    | TArrow (a, q, b, e) ->
      TArrow (apply_subst a, q, apply_subst b, e)
    | TTuple tys ->
      TTuple (List.map apply_subst tys)
    | TRecord row ->
      TRecord (apply_subst_row row)
    | TVariant row ->
      TVariant (apply_subst_row row)
    | TForall (v, k, body) ->
      TForall (v, k, apply_subst body)
    | TExists (v, k, body) ->
      TExists (v, k, apply_subst body)
    | TRef t -> TRef (apply_subst t)
    | TMut t -> TMut (apply_subst t)
    | TOwn t -> TOwn (apply_subst t)
  and apply_subst_row row =
    match repr_row row with
    | REmpty -> REmpty
    | RExtend (l, ty, rest) ->
      RExtend (l, apply_subst ty, apply_subst_row rest)
    | RVar _ -> row
  in
  apply_subst sc.sc_body

(** Generalize a type by quantifying over all type variables
    that were introduced at a level deeper than the context's
    current level. *)
let generalize (ctx : context) (ty : ty) : scheme =
  let tyvars = ref [] in
  let rec collect ty =
    match repr ty with
    | TVar r ->
      begin match !r with
        | Unbound (v, lev) when lev > ctx.level ->
          if not (List.exists (fun (v', _) -> v' = v) !tyvars) then
            tyvars := (v, Types.KType) :: !tyvars
        | Unbound _ -> ()
        | Link t -> collect t
      end
    | TCon _ -> ()
    | TApp (t, args) ->
      collect t; List.iter collect args
    | TArrow (a, _, b, _) ->
      collect a; collect b
    | TTuple tys ->
      List.iter collect tys
    | TRecord row | TVariant row ->
      collect_row row
    | TForall (_, _, body) | TExists (_, _, body) ->
      collect body
    | TRef t | TMut t | TOwn t ->
      collect t
  and collect_row row =
    match repr_row row with
    | REmpty -> ()
    | RExtend (_, ty, rest) ->
      collect ty; collect_row rest
    | RVar _ -> ()
  in
  collect ty;
  { sc_tyvars = !tyvars; sc_effvars = []; sc_rowvars = [];
    sc_body = ty }

(** Look up a variable, returning a fresh instantiation of its scheme. *)
let lookup_var (ctx : context) (name : string) : ty result =
  match Hashtbl.find_opt ctx.name_types name with
  | Some sc -> Ok (instantiate ctx.level sc)
  | None -> Error (UnboundVariable name)

(** {1 Kind checking} *)

let rec infer_kind (ctx : context) (ty : ty) : kind result =
  match repr ty with
  | TVar r ->
    begin match !r with
      | Unbound (_, _) -> Ok KType
      | Link t -> infer_kind ctx t
    end
  | TCon name ->
    begin match name with
      | "Array" | "Option" | "List" | "Vec" | "Cmd" | "Ref" -> Ok (KArrow (KType, KType))
      | "Result" -> Ok (KArrow (KType, KArrow (KType, KType)))
      | _ -> Ok KType
    end
  | TApp (head, args) ->
    let* k = infer_kind ctx head in
    check_kind_app ctx k args
  | TArrow (_, _, _, _) | TTuple _ | TRecord _ | TVariant _ ->
    Ok KType
  | TForall (_, _, body) | TExists (_, _, body) ->
    let* _ = infer_kind ctx body in
    Ok KType
  | TRef t | TMut t | TOwn t ->
    infer_kind ctx t

and check_kind (ctx : context) (ty : ty) (expected : kind) : unit result =
  let* got = infer_kind ctx ty in
  if got = expected then Ok ()
  else Error (NotImplemented (Printf.sprintf "Kind mismatch: expected %s, got %s" (show_kind expected) (show_kind got)))

and check_kind_app (ctx : context) (k : kind) (args : ty list) : kind result =
  match args with
  | [] -> Ok k
  | arg :: rest ->
    begin match k with
      | KArrow (param_k, ret_k) ->
        let* () = check_kind ctx arg param_k in
        check_kind_app ctx ret_k rest
      | _ -> Error (NotImplemented "Too many arguments for kind")
    end

(** {1 AST type_expr → internal ty conversion} *)

let lower_quantity (q : Ast.quantity) : Types.quantity =
  match q with
  | QZero -> QZero
  | QOne -> QOne
  | QOmega -> QOmega

(** Convert an AST [type_expr] to an internal [ty].

    Type variables are looked up in [type_env]; unknown names become
    fresh unification variables so that inference can resolve them. *)
let rec lower_type_expr (ctx : context) (te : type_expr) : ty =
  match te with
  | TyVar { name; _ } ->
    begin match Hashtbl.find_opt ctx.type_env name with
      | Some ty -> ty
      | None ->
        (* Unresolved type variable: create a fresh unification var *)
        let tv = fresh_tyvar ctx.level in
        Hashtbl.replace ctx.type_env name tv;
        tv
    end
  | TyCon { name; _ } ->
    let name = strip_module_qualifier ctx name in
    begin match name with
      | "Int" -> ty_int
      | "Float" -> ty_float
      | "Bool" -> ty_bool
      | "String" -> ty_string
      | "Char" -> ty_char
      | "Unit" | "()" -> ty_unit
      | "Never" -> ty_never
      | _ ->
        begin match Hashtbl.find_opt ctx.type_env name with
          | Some ty -> ty
          | None -> TCon name
        end
    end
  | TyApp ({ name; _ }, args) ->
    let name = strip_module_qualifier ctx name in
    let head = match Hashtbl.find_opt ctx.type_env name with
      | Some ty -> ty
      | None -> TCon name
    in
    let arg_tys = List.map (fun arg ->
      match arg with
      | TyArg te -> lower_type_expr ctx te
    ) args in
    TApp (head, arg_tys)
  | TyArrow (a, q_opt, b, eff_opt) ->
    let a' = lower_type_expr ctx a in
    let b' = lower_type_expr ctx b in
    let q = match q_opt with
      | Some q -> lower_quantity q
      | None -> QOmega  (* Default to unrestricted *)
    in
    let eff = match eff_opt with
      | Some e -> lower_effect_expr ctx e
      | None -> EPure
    in
    TArrow (a', q, b', eff)
  | TyTuple [] ->
    ty_unit
  | TyTuple tes ->
    TTuple (List.map (lower_type_expr ctx) tes)
  | TyRecord (fields, _row_var) ->
    let row = List.fold_right (fun (rf : row_field) acc ->
      RExtend (rf.rf_name.name, lower_type_expr ctx rf.rf_ty, acc)
    ) fields REmpty in
    TRecord row
  | TyOwn te -> TOwn (lower_type_expr ctx te)
  | TyRef (_, te) -> TRef (lower_type_expr ctx te)
  | TyMut (_, te) -> TMut (lower_type_expr ctx te)
  | TyHole ->
    fresh_tyvar ctx.level

and lower_effect_expr (ctx : context) (ee : effect_expr) : eff =
  (* Resolve a source effect name to a canonical singleton (issue #59):
     Pure → pure; v1/reserved/legacy-alias → canonical registry name;
     user-declared (`effect <name>;`) → kept as written; anything else
     is rejected so contributors cannot silently invent effect names. *)
  let resolve (name : string) : eff =
    let name = strip_module_qualifier ctx name in
    if name = "Pure" then EPure
    else match Effect.canonical_effect_name name with
      | Some canonical -> ESingleton canonical
      | None ->
        if Hashtbl.mem ctx.declared_effects name then ESingleton name
        else raise (Effect_validation_error name)
  in
  match ee with
  | EffVar { name; _ } -> resolve name
  | EffCon ({ name; _ }, args) ->
    (* Parametric effect, e.g. `Throws[MyErr]` (issue #59). Effect
       *tracking* only: carry the type argument by mangling it into the
       singleton name, so `Throws[A]`, `Throws[B]` and bare `Throws` are
       distinct under the string-equality unification of `eff` — without
       growing the `eff` ADT (which would ripple across every effect
       operation). The base name is still validated via `resolve`. *)
    (match resolve name with
     | ESingleton base when args <> [] ->
       let arg_str =
         args
         |> List.map (fun (TyArg te) -> ty_to_string (lower_type_expr ctx te))
         |> String.concat ", "
       in
       ESingleton (base ^ "[" ^ arg_str ^ "]")
     | other -> other)
  | EffUnion (e1, e2) ->
    EUnion [lower_effect_expr ctx e1; lower_effect_expr ctx e2]

(** {1 Binary/unary operator typing} *)

(** Return the type of a binary operator given its operand types. *)
let type_of_binop (op : binary_op) : ty * ty * ty =
  match op with
  (* Arithmetic: Int -> Int -> Int *)
  | OpAdd | OpSub | OpMul | OpDiv | OpMod ->
    (ty_int, ty_int, ty_int)
  (* Comparison: Int -> Int -> Bool *)
  | OpLt | OpLe | OpGt | OpGe ->
    (ty_int, ty_int, ty_bool)
  (* Equality: polymorphic, but we approximate as 'a -> 'a -> Bool *)
  | OpEq | OpNe ->
    let tv = fresh_tyvar 0 in
    (tv, tv, ty_bool)
  (* Logical: Bool -> Bool -> Bool *)
  | OpAnd | OpOr ->
    (ty_bool, ty_bool, ty_bool)
  (* Bitwise: Int -> Int -> Int *)
  | OpBitAnd | OpBitOr | OpBitXor | OpShl | OpShr ->
    (ty_int, ty_int, ty_int)
  | OpConcat ->
    (ty_string, ty_string, ty_string)

let type_of_unop (op : unary_op) : ty * ty =
  match op with
  | OpNeg -> (ty_int, ty_int)
  | OpNot -> (ty_bool, ty_bool)
  | OpBitNot -> (ty_int, ty_int)
  | OpRef | OpMutRef ->
    (* `&mut e` types exactly like `&e` — a reference. Exclusivity is a
       static borrow-checker property only (CORE-01 pt2 / #177). *)
    let tv = fresh_tyvar 0 in
    (tv, TRef tv)
  | OpDeref ->
    let tv = fresh_tyvar 0 in
    (TRef tv, tv)

(** {1 Pattern typing} *)

(** Type-check a pattern and return the list of bindings it introduces.
    Each binding is [(name, ty)].  The pattern is checked against [expected_ty]
    when in checking mode. *)
let rec check_pattern (ctx : context) (pat : pattern) (expected : ty)
    : ((string * ty) list) result =
  match pat with
  | PatWildcard _ ->
    Ok []
  | PatVar { name; _ } ->
    Ok [(name, expected)]
  | PatLit lit ->
    let lit_ty = type_of_literal lit in
    let* () = unify_or_err expected lit_ty in
    Ok []
  | PatTuple pats ->
    let n = List.length pats in
    let elem_tys = List.init n (fun _ -> fresh_tyvar ctx.level) in
    let* () = unify_or_err expected (TTuple elem_tys) in
    let* bindings_list = check_patterns ctx pats elem_tys in
    Ok (List.concat bindings_list)
  | PatCon ({ name; _ }, sub_pats) ->
    (* Resolve the constructor's type, freshly instantiated *per use-site*.
       Prefer the polymorphic scheme bound in [name_types] (set via
       [bind_scheme] for both builtin Ok/Err/Some/None/RuntimeError and
       user-declared variants) so every occurrence gets independent type
       variables — exactly as [lookup_var] does for ordinary identifiers.
       Fall back to the monomorphic [constructor_env] entry only when no
       scheme is registered. Previously this read [constructor_env] alone
       and wrapped it as a 0-tyvar scheme, so all occurrences *shared* one
       set of variables: two `Ok(_)` patterns in one match then forced both
       payloads to the same type (`Unify ((_ -> _), T)` in result.affine). *)
    let ctor_ty_opt =
      match Hashtbl.find_opt ctx.name_types name with
      | Some sc -> Some (instantiate ctx.level sc)
      | None ->
        (match Hashtbl.find_opt ctx.constructor_env name with
         | Some ctor_ty ->
           Some (instantiate ctx.level
             { sc_tyvars = []; sc_effvars = []; sc_rowvars = [];
               sc_body = ctor_ty })
         | None -> None)
    in
    begin match ctor_ty_opt with
      | Some ctor_ty' ->
        (* Constructor type should be T1 -> T2 -> ... -> ResultType *)
        let rec peel_arrows ty pats acc =
          match pats with
          | [] ->
            let* () = unify_or_err expected ty in
            Ok (List.rev acc)
          | p :: rest ->
            begin match repr ty with
              | TArrow (param_ty, _, ret_ty, _) ->
                let* binds = check_pattern ctx p param_ty in
                peel_arrows ret_ty rest (binds :: acc)
              | _ ->
                Error (ArityMismatch { name; expected = List.length sub_pats;
                                       got = List.length pats - List.length rest })
            end
        in
        let* bindings_list = peel_arrows ctor_ty' sub_pats [] in
        Ok (List.concat bindings_list)
      | None ->
        (* Unknown constructor — if it has no arguments, treat as a variant tag *)
        if sub_pats = [] then begin
          (* Unify expected with a variant containing this tag *)
          Ok []
        end else
          Error (UnboundVariable name)
    end
  | PatRecord (fields, _has_rest) ->
    let bindings = ref [] in
    List.iter (fun (({ name; _ } : ident), pat_opt) ->
      let field_ty = fresh_tyvar ctx.level in
      begin match pat_opt with
        | Some sub_pat ->
          begin match check_pattern ctx sub_pat field_ty with
            | Ok bs -> bindings := bs @ !bindings
            | Error _ -> ()
          end
        | None ->
          bindings := (name, field_ty) :: !bindings
      end
    ) fields;
    Ok !bindings
  | PatOr (p1, _p2) ->
    (* Both branches must produce the same bindings; we check the first *)
    check_pattern ctx p1 expected
  | PatAs ({ name; _ }, sub_pat) ->
    let* binds = check_pattern ctx sub_pat expected in
    Ok ((name, expected) :: binds)

and check_patterns (ctx : context) (pats : pattern list) (tys : ty list)
    : ((string * ty) list list) result =
  match pats, tys with
  | [], [] -> Ok []
  | p :: ps, t :: ts ->
    let* binds = check_pattern ctx p t in
    let* rest = check_patterns ctx ps ts in
    Ok (binds :: rest)
  | _ -> Error (PatternTypeMismatch "pattern/type list length mismatch")

(** {1 Literal typing} *)

and type_of_literal (lit : literal) : ty =
  match lit with
  | LitInt _ -> ty_int
  | LitFloat _ -> ty_float
  | LitBool _ -> ty_bool
  | LitChar _ -> ty_char
  | LitString _ -> ty_string
  | LitUnit _ -> ty_unit

(** String-wall slice 8b. Physical-identity record of the `++` ([OpConcat])
    nodes that typed as {b String} concatenation (rather than array concat).
    Populated by {!synth} while checking, consumed by
    {!elaborate_string_concat} to rewrite exactly those nodes into
    {!Ast.ExprStringConcat} for the byte-concat wasm lowering.

    Keyed by physical identity ([==], via [List.memq]) and not by span/value:
    [ExprBinary] carries no span, and two distinct same-text `++` occurrences
    are value-equal. This is sound because typecheck and the elaboration run
    over the {e same} program object — [parse_with_face]'s lowered [prog],
    shared by resolve/typecheck/codegen — so the node [synth] records is
    physically the node the elaboration rewrites. Stale entries from a prior
    compile never match the current [prog]'s nodes, so accumulation across
    compiles is harmless; {!elaborate_string_concat} clears the list when it
    consumes it. *)
let string_concat_sites : expr list ref = ref []

(** Discard any recorded String-concat sites (e.g. before re-checking). *)
let reset_string_concat_sites () : unit = string_concat_sites := []

(** String-wall slice 9. Physical-identity record of the `==`/`!=` ([OpEq]/
    [OpNe]) nodes whose operands typed as {b String}. Polymorphic equality
    ([type_of_binop] gives `'a -> 'a -> Bool`) lets String `==` typecheck and
    then fall to the [I32Eq] *pointer* comparison in codegen — wrong for the
    `[len][utf8]` layout (two equal-valued strings at distinct addresses
    compare unequal). Populated by {!synth}, consumed by
    {!elaborate_string_concat} (which clears it) to rewrite exactly those
    nodes into {!Ast.ExprStringEq} for the byte-comparison wasm lowering.
    Same physical-identity ([List.memq]) discipline as
    {!string_concat_sites}. *)
let string_eq_sites : expr list ref = ref []

(** Discard any recorded String-equality sites (e.g. before re-checking). *)
let reset_string_eq_sites () : unit = string_eq_sites := []

(** String-wall slice 10 (#458). Physical-identity record of the relational
    ([OpLt] / [OpLe] / [OpGt] / [OpGe]) nodes whose operands typed as {b
    String}. These typecheck in {!synth}'s [comparison] branch (returning
    Bool), but codegen would otherwise lower them to a signed-integer compare
    on the two `[len][utf8]` *pointers*, which is meaningless. Populated by
    {!synth}, consumed by {!elaborate_string_concat} (which clears it) to
    rewrite them into {!Ast.ExprStringRel} for the byte-wise lexicographic
    wasm lowering. Same physical-identity ([List.memq]) discipline as
    {!string_eq_sites}. *)
let string_rel_sites : expr list ref = ref []

(** Discard any recorded String-relational sites (e.g. before re-checking). *)
let reset_string_rel_sites () : unit = string_rel_sites := []

(** Float wall. Physical-identity record of the `Float`-typed binary-op nodes
    (`+`/`-`/`*`/`/`, `<`/`<=`/`>`/`>=`, `==`/`!=`). They type-check (synth
    dispatches `Float`) but codegen's [gen_binop] returns only the i32
    instruction family, so an f64 operand reaches `i32.lt_s`/`i32.add`/… and
    fails wasm validation. Populated by {!synth} (three sites: the arith
    branch's `Float` case, the `comparison` branch's `Float` case, and the
    `==`/`!=` else branch when the operands are `Float`); consumed by
    {!elaborate_string_concat} (which clears it) to rewrite them into
    {!Ast.ExprFloatBinary} for the f64 lowering. *)
let float_binop_sites : expr list ref = ref []

(** Discard any recorded Float-binop sites (e.g. before re-checking). *)
let reset_float_binop_sites () : unit = float_binop_sites := []

(** Float heap wall (issue-draft 05, durable fix). Physical-identity record of
    the heap nodes whose *cell* type is `Float`: an [ExprArray] whose element
    typed as `Float` (→ {!Ast.ExprFloatArray}, 8-byte f64 cells) and an
    [ExprIndex] whose result typed as `Float` (→ {!Ast.ExprFloatIndex}, 8-byte
    f64 load). Because `synth` sees every node's *checked* type, recording is
    total — every Float construction and every Float-yielding access is caught,
    regardless of how the array flowed there — so codegen never has to guess a
    cell width (the gap that forced the interim loud-fail). Same physical-
    identity ([List.memq]) discipline and same-program-object soundness as
    {!float_binop_sites}; consumed and cleared by {!elaborate_string_concat}. *)
let float_heap_sites : expr list ref = ref []

(** Discard any recorded Float-heap sites (e.g. before re-checking). *)
let reset_float_heap_sites () : unit = float_heap_sites := []

(** Float heap wall — heterogeneous tuples. A tuple with at least one scalar
    `Float` field is laid out with uniform 8-byte cells (see {!Ast.ExprCellTuple}).
    These two physical-identity *maps* carry the per-cell kinds (a set is not
    enough): [cell_tuple_sites] maps an [ExprTuple] node to its per-field "is f64
    cell?" flags (for construction); [cell_tuple_index_sites] maps an
    [ExprTupleIndex] node to whether the accessed field is f64 (for the load).
    `synth` populates both; {!elaborate_string_concat} consumes ([List.assq]) and
    clears them. A field that is itself a float aggregate is stored as an i32
    pointer (flag = false), so only *scalar* `Float` fields flag an f64 cell. *)
let cell_tuple_sites : (expr * bool list) list ref = ref []
let reset_cell_tuple_sites () : unit = cell_tuple_sites := []
let cell_tuple_index_sites : (expr * bool) list ref = ref []
let reset_cell_tuple_index_sites () : unit = cell_tuple_index_sites := []

(** Float heap wall — float-bearing records (closed rows only). Uniform 8-byte
    cells, fields placed by name sorted ascending (see {!Ast.ExprCellRecord}).
    [cell_record_sites] maps an [ExprRecord] node to its per-field
    [(field_name, is_f64)]; [cell_field_sites] maps an [ExprField] access node to
    the accessed field's [(byte_offset, is_f64)] (offset = sorted-name position ×
    8, computed from the CLOSED record row — an open/polymorphic row is left on
    the i32 path and loud-fails via the guard). Same physical-identity ([List.assq])
    discipline; consumed/cleared by {!elaborate_string_concat}. *)
let cell_record_sites : (expr * (string * bool) list) list ref = ref []
let reset_cell_record_sites () : unit = cell_record_sites := []
let cell_field_sites : (expr * (int * bool)) list ref = ref []
let reset_cell_field_sites () : unit = cell_field_sites := []

(** A closed record row's fields as [(name, ty)], or [None] if the row is open
    (ends in a row variable) — in which case the heap layout cannot be fixed. *)
let rec closed_row_fields (row : row) : (string * ty) list option =
  match repr_row row with
  | REmpty -> Some []
  | RExtend (l, t, rest) ->
    (match closed_row_fields rest with Some fs -> Some ((l, t) :: fs) | None -> None)
  | RVar _ -> None

(** Sorted-by-name (offset, is_f64) layout for a closed float-bearing record:
    cell i (in ascending-name order) at byte offset i*8, f64 iff scalar Float.
    Returns [None] unless the row is closed AND has at least one scalar Float. *)
let record_cell_layout (row : row) : (string * (int * bool)) list option =
  match closed_row_fields row with
  | None -> None
  | Some fields ->
    let sorted = List.sort (fun (a, _) (b, _) -> String.compare a b) fields in
    let is_f t = match repr t with TCon "Float" -> true | _ -> false in
    if not (List.exists (fun (_, t) -> is_f t) sorted) then None
    else Some (List.mapi (fun i (name, t) -> (name, (i * 8, is_f t))) sorted)

(** {1 Expression synthesis (mode ⇒)} *)

(** Synthesize a type for an expression. *)
let rec synth (ctx : context) (expr : expr) : ty result =
  match expr with
  (* Literals *)
  | ExprLit lit ->
    Ok (type_of_literal lit)

  (* Variables — instantiate their scheme *)
  | ExprVar { name; _ } ->
    lookup_var ctx name

  (* Let bindings: let pat = e1 in e2 *)
  | ExprLet { el_pat; el_ty; el_value; el_body; el_mut = _; el_quantity = _ } ->
    (* Synthesize or check the value *)
    enter_level ctx;
    let* val_ty = begin match el_ty with
      | Some te ->
        let ann_ty = lower_type_expr ctx te in
        let* () = check ctx el_value ann_ty in
        Ok ann_ty
      | None ->
        synth ctx el_value
    end in
    exit_level ctx;
    (* Generalize the value type *)
    let sc = generalize ctx val_ty in
    (* Bind pattern variables *)
    let* bindings = check_pattern ctx el_pat val_ty in
    let old_bindings = List.map (fun (name, _) ->
      (name, Hashtbl.find_opt ctx.name_types name)
    ) bindings in
    List.iter (fun (name, _ty) ->
      bind_scheme ctx name sc
    ) bindings;
    (* Type-check the body if present, else return Unit *)
    let result = begin match el_body with
      | Some body -> synth ctx body
      | None -> Ok ty_unit
    end in
    (* Restore old bindings *)
    List.iter (fun (name, old) ->
      match old with
      | Some sc' -> Hashtbl.replace ctx.name_types name sc'
      | None -> Hashtbl.remove ctx.name_types name
    ) old_bindings;
    result

  (* If-then-else *)
  | ExprIf { ei_cond; ei_then; ei_else } ->
    let* () = check ctx ei_cond ty_bool in
    let* then_ty = synth ctx ei_then in
    begin match ei_else with
      | Some else_expr ->
        let* else_ty = synth ctx else_expr in
        let* () = unify_or_err then_ty else_ty in
        Ok then_ty
      | None ->
        (* No else branch: result is Unit *)
        let* () = unify_or_err then_ty ty_unit in
        Ok ty_unit
    end

  (* Match expressions *)
  | ExprMatch { em_scrutinee; em_arms } ->
    let* scrut_ty = synth ctx em_scrutinee in
    let result_ty = fresh_tyvar ctx.level in
    let* () = List.fold_left (fun acc (arm : match_arm) ->
      let* () = acc in
      let* bindings = check_pattern ctx arm.ma_pat scrut_ty in
      (* Save and bind pattern variables *)
      let old = List.map (fun (n, _) ->
        (n, Hashtbl.find_opt ctx.name_types n)
      ) bindings in
      List.iter (fun (n, t) -> bind_var ctx n t) bindings;
      (* Check guard if present *)
      let* () = match arm.ma_guard with
        | Some guard -> check ctx guard ty_bool
        | None -> Ok ()
      in
      (* Body must unify with result type *)
      let* arm_ty = synth ctx arm.ma_body in
      let* () = unify_or_err result_ty arm_ty in
      (* Restore *)
      List.iter (fun (n, old_sc) ->
        match old_sc with
        | Some sc -> Hashtbl.replace ctx.name_types n sc
        | None -> Hashtbl.remove ctx.name_types n
      ) old;
      Ok ()
    ) (Ok ()) em_arms in
    Ok result_ty

  (* Lambda *)
  | ExprLambda { elam_params; elam_ret_ty; elam_body } ->
    let param_tys = List.map (fun (p : param) ->
      lower_type_expr ctx p.p_ty
    ) elam_params in
    (* Save old bindings, bind params *)
    let old = List.map2 (fun (p : param) ty ->
      let old = Hashtbl.find_opt ctx.name_types p.p_name.name in
      bind_var ctx p.p_name.name ty;
      (p.p_name.name, old)
    ) elam_params param_tys in
    (* Synthesize or check body *)
    let* body_ty = begin match elam_ret_ty with
      | Some te ->
        let ret_ty = lower_type_expr ctx te in
        let* () = check ctx elam_body ret_ty in
        Ok ret_ty
      | None ->
        synth ctx elam_body
    end in
    (* Restore *)
    List.iter (fun (n, old_sc) ->
      match old_sc with
      | Some sc -> Hashtbl.replace ctx.name_types n sc
      | None -> Hashtbl.remove ctx.name_types n
    ) old;
    (* Build the arrow type: curried for multi-param.
       Each arrow carries the declared quantity of the corresponding parameter.
       If the parameter has no explicit annotation, we default to QOmega
       (unrestricted), matching the convention used by check_fn_decl. *)
    let eff = fresh_effvar ctx.level in
    let param_qty_pairs = List.map2 (fun (p : param) param_ty ->
      let q = match p.p_quantity with
        | Some q -> lower_quantity q
        | None   -> QOmega
      in
      (q, param_ty)
    ) elam_params param_tys in
    let ty = List.fold_right (fun (q, param_ty) acc ->
      TArrow (param_ty, q, acc, eff)
    ) param_qty_pairs body_ty in
    Ok ty

  (* Function application *)
  | ExprApp (fn_expr, args) ->
    let* fn_ty = synth ctx fn_expr in
    begin match args with
      | [] ->
        (* A zero-argument call [f()]. Zero-parameter function
           *declarations* are typed as their bare return type (the param
           fold in [check_fn_decl] is over []), so [apply_args fn_ty []]
           correctly yields that type. But an explicit [() -> T] thunk
           type — a record field, a parameter, a lambda — lowers to
           [TArrow (Unit, _, T, _)]; invoking it must consume the unit and
           yield [T]. Curried/partial application never reaches this branch
           with [args = []] (it always carries a non-empty arg list at the
           [ExprApp] site), so peeling a single unit arrow here is sound. *)
        begin match repr fn_ty with
          | TArrow (param_ty, _q, ret_ty, _eff)
            when repr param_ty = ty_unit -> Ok ret_ty
          | _ -> apply_args ctx fn_ty args
        end
      | _ -> apply_args ctx fn_ty args
    end

  (* Tuple *)
  | ExprTuple exprs as tup_node ->
    let* tys = synth_list ctx exprs in
    (* Float heap wall: a tuple with any scalar `Float` field uses uniform 8-byte
       cells (ExprCellTuple). Record the per-field "is f64 cell?" flags (scalar
       Float → f64; anything else, incl. pointers to float aggregates → i32). *)
    let cell_kinds = List.map (fun t -> match repr t with TCon "Float" -> true | _ -> false) tys in
    if List.exists Fun.id cell_kinds
    then cell_tuple_sites := (tup_node, cell_kinds) :: !cell_tuple_sites;
    Ok (TTuple tys)

  (* Array *)
  | ExprArray exprs as arr_node ->
    begin match exprs with
      | [] ->
        let elem_ty = fresh_tyvar ctx.level in
        Ok (TApp (TCon "Array", [elem_ty]))
      | first :: rest ->
        let* first_ty = synth ctx first in
        let* () = List.fold_left (fun acc e ->
          let* () = acc in
          check ctx e first_ty
        ) (Ok ()) rest in
        (* Float heap wall: an [Float]-element array literal must lay out 8-byte
           f64 cells — record it for rewrite to {!Ast.ExprFloatArray}. *)
        (match repr first_ty with
         | TCon "Float" -> float_heap_sites := arr_node :: !float_heap_sites
         | _ -> ());
        Ok (TApp (TCon "Array", [first_ty]))
    end

  (* Record literal *)
  | ExprRecord { er_fields; er_spread } as rec_node ->
    let* field_tys = List.fold_left (fun acc (({ name; _ } : ident), expr_opt) ->
      let* fields = acc in
      let* ty = begin match expr_opt with
        | Some e -> synth ctx e
        | None -> lookup_var ctx name
      end in
      Ok ((name, ty) :: fields)
    ) (Ok []) er_fields in
    let row = List.fold_right (fun (name, ty) acc ->
      RExtend (name, ty, acc)
    ) field_tys REmpty in
    (* Float heap wall: a float-bearing record literal (closed, no spread) lays
       out uniform 8-byte cells, fields sorted by name. Record per-field f64
       flags. A spread (`{..r, x: 1.0}`) adds fields not in this row, so the
       layout would be incomplete — skip it (keeps loud-failing). *)
    (match er_spread, record_cell_layout row with
     | None, Some layout ->
       let kinds = List.map (fun (name, (_off, is_f64)) -> (name, is_f64)) layout in
       cell_record_sites := (rec_node, kinds) :: !cell_record_sites
     | _ -> ());
    Ok (TRecord row)

  (* Field access — first try record-field projection, then trait method lookup *)
  | ExprField (obj, { name = field; _ }) as field_node ->
    let* obj_ty = synth ctx obj in
    (* Auto-deref reference/owned wrappers before record projection
       (issue #122 v2): `c.field` where `c : ref/own/mut S` projects the
       field of S — the borrow checker still governs aliasing separately.
       Without this, `fn(c: ref S) = c.field` failed with
       "Field 'field' not found in type ref {...}". *)
    let rec strip_ref t =
      match repr t with
      | TRef u | TMut u | TOwn u -> strip_ref u
      | u -> u
    in
    let obj_ty_deref = strip_ref obj_ty in
    let field_ty = fresh_tyvar ctx.level in
    let rest_row = fresh_rowvar ctx.level in
    let expected_record = TRecord (RExtend (field, field_ty, rest_row)) in
    begin match Unify.unify (repr obj_ty_deref) expected_record with
    | Ok () ->
      (* Float heap wall: if obj is a CLOSED float-bearing record, `r.field`
         loads from the sorted-by-name uniform-8 layout (every field access on
         such a record is rewritten, since the whole record uses 8-byte cells).
         An open row yields no layout → stays on the i32 path / loud-fails. *)
      (match repr obj_ty_deref with
       | TRecord row ->
         (match record_cell_layout row with
          | Some layout ->
            (match List.assoc_opt field layout with
             | Some (offset, is_f64) ->
               cell_field_sites := (field_node, (offset, is_f64)) :: !cell_field_sites
             | None -> ())
          | None -> ())
       | _ -> ());
      Ok field_ty
    | Error _ ->
      (* Record projection failed — try trait method dispatch.
         We search all registered impls for a method named [field]
         whose self type unifies with [obj_ty]. *)
      begin match Trait.find_method_for_type ctx.trait_registry obj_ty field with
      | Some (_impl, method_decl) ->
        (* Build the method's monomorphic type from the fn_decl.
           Parameters: each p_ty is lowered to an internal ty.
           Return type defaults to a fresh type variable when omitted.
           Effects are left as a fresh effect variable (unannotated). *)
        let param_tys = List.map (fun (p : Ast.param) ->
          lower_type_expr ctx p.p_ty
        ) method_decl.Ast.fd_params in
        let ret_ty = match method_decl.Ast.fd_ret_ty with
          | Some te -> lower_type_expr ctx te
          | None -> fresh_tyvar ctx.level
        in
        let eff = fresh_effvar ctx.level in
        (* Fold params into a curried arrow, right-to-left *)
        let method_ty = List.fold_right (fun (param_and_ty) acc ->
          let (p, pt) = (param_and_ty : Ast.param * ty) in
          let q = match p.Ast.p_quantity with
            | Some q -> lower_quantity q
            | None -> QOmega
          in
          TArrow (pt, q, acc, eff)
        ) (List.combine method_decl.Ast.fd_params param_tys) ret_ty in
        Ok method_ty
      | None ->
        (* Neither record field nor trait method — report a field-not-found error *)
        Error (FieldNotFound { field; record_ty = obj_ty })
      end
    end

  (* Tuple indexing *)
  | ExprTupleIndex (tup, idx) as tidx_node ->
    let* tup_ty = synth ctx tup in
    begin match repr tup_ty with
      | TTuple tys ->
        if idx >= 0 && idx < List.length tys then begin
          (* Float heap wall: if the tuple has ANY scalar `Float` field it uses
             uniform 8-byte cells, so EVERY access (not just float fields) must
             be rewritten to the i*8 layout. Record whether the accessed field
             is itself f64 (→ f64 load) or i32. *)
          if List.exists (fun t -> match repr t with TCon "Float" -> true | _ -> false) tys
          then begin
            let accessed_is_float =
              match repr (List.nth tys idx) with TCon "Float" -> true | _ -> false in
            cell_tuple_index_sites := (tidx_node, accessed_is_float) :: !cell_tuple_index_sites
          end;
          Ok (List.nth tys idx)
        end
        else
          Error (TupleIndexOutOfBounds { index = idx; length = List.length tys })
      | _ ->
        (* Create a tuple type with enough slots *)
        let n = idx + 1 in
        let elem_tys = List.init n (fun _ -> fresh_tyvar ctx.level) in
        let* () = unify_or_err tup_ty (TTuple elem_tys) in
        Ok (List.nth elem_tys idx)
    end

  (* Array indexing *)
  | ExprIndex (arr, idx_expr) as idx_node ->
    let* arr_ty = synth ctx arr in
    let* () = check ctx idx_expr ty_int in
    let elem_ty = fresh_tyvar ctx.level in
    let* () = unify_or_err arr_ty (TApp (TCon "Array", [elem_ty])) in
    (* Float heap wall: a `Float`-yielding index must load an 8-byte f64 cell —
       record it for rewrite to {!Ast.ExprFloatIndex}. *)
    (match repr elem_ty with
     | TCon "Float" -> float_heap_sites := idx_node :: !float_heap_sites
     | _ -> ());
    Ok elem_ty

  (* Binary operators

     Arithmetic and comparison ops are dispatched on the lhs type so that
     [Float] kernels typecheck without requiring a typeclass system. Order:
     synthesise lhs, walk through repr to pierce variables; if it's a Float,
     pin rhs to Float and return the matching result type; otherwise fall
     through to the legacy [type_of_binop] path which is Int-monomorphic. *)
  | ExprBinary (lhs, op, rhs) as concat_node ->
    let arith_or_bitwise = match op with
      | OpAdd | OpSub | OpMul | OpDiv | OpMod
      | OpBitAnd | OpBitOr | OpBitXor | OpShl | OpShr -> true
      | _ -> false
    in
    let comparison = match op with
      | OpLt | OpLe | OpGt | OpGe -> true
      | _ -> false
    in
    if arith_or_bitwise then begin
      let* lhs_ty = synth ctx lhs in
      match repr lhs_ty with
      | TCon "Float" ->
        let* () = check ctx rhs ty_float in
        (* Float wall: record this arith node so elaboration rewrites it to
           ExprFloatBinary (codegen must emit f64 ops, not the i32 family). *)
        float_binop_sites := concat_node :: !float_binop_sites;
        Ok ty_float
      | _ ->
        let (lhs_ty', rhs_ty, result_ty) = type_of_binop op in
        let* () = unify_or_err lhs_ty lhs_ty' in
        let* () = check ctx rhs rhs_ty in
        Ok result_ty
    end else if comparison then begin
      let* lhs_ty = synth ctx lhs in
      match repr lhs_ty with
      | TCon "Float" ->
        let* () = check ctx rhs ty_float in
        (* Float wall: relational Float comparison -> ExprFloatBinary (f64 cmp). *)
        float_binop_sites := concat_node :: !float_binop_sites;
        Ok ty_bool
      | TCon "String" ->
        (* String relational ops are byte-wise lexicographic, matching
           JS / Lua / Rust convention. Surfaced by #458 (was the
           rate-limiter for several TS→AS ports). *)
        let* () = check ctx rhs ty_string in
        (* String-wall slice 10: record this relational node for elaboration
           to ExprStringRel. The [comparison] branch only fires for
           OpLt/OpLe/OpGt/OpGe, so every recorded node carries one of those
           ops; without this, codegen lowers `<` to a signed compare of the
           two string *pointers*. *)
        string_rel_sites := concat_node :: !string_rel_sites;
        Ok ty_bool
      | _ ->
        let (lhs_ty', rhs_ty, result_ty) = type_of_binop op in
        let* () = unify_or_err lhs_ty lhs_ty' in
        let* () = check ctx rhs rhs_ty in
        Ok result_ty
    end else if (match op with OpConcat -> true | _ -> false) then begin
      (* `++` is polymorphic over String and [T] (issue #122 v2.5):
         `a ++ b` (string concat) and `acc ++ [x]` (array concat) — the
         latter is how stdlib/string.affine's split/join/etc. accumulate.
         Dispatch on the synthesised lhs type. *)
      let* lhs_ty = synth ctx lhs in
      (match repr lhs_ty with
       | TApp (TCon "Array", [elem]) ->
         let* () = check ctx rhs (TApp (TCon "Array", [elem])) in
         Ok (TApp (TCon "Array", [elem]))
       | TCon "String" ->
         let* () = check ctx rhs ty_string in
         (* String-wall slice 8b: record this `++` node (physical identity)
            as a String concat, so elaborate_string_concat can rewrite it to
            ExprStringConcat for the byte-concat wasm lowering. *)
         string_concat_sites := concat_node :: !string_concat_sites;
         Ok ty_string
       | _ ->
         (* lhs type not yet determined (e.g. `let mut acc = []`):
            disambiguate on the rhs rather than defaulting to String. *)
         let* rhs_ty = synth ctx rhs in
         (match repr rhs_ty with
          | TApp (TCon "Array", [elem]) ->
            let* () = unify_or_err lhs_ty (TApp (TCon "Array", [elem])) in
            Ok (TApp (TCon "Array", [elem]))
          | _ ->
            let* () = unify_or_err lhs_ty ty_string in
            let* () = unify_or_err rhs_ty ty_string in
            (* Slice 8b: also a String concat (lhs was undetermined). *)
            string_concat_sites := concat_node :: !string_concat_sites;
            Ok ty_string))
    end else begin
      let (lhs_ty, rhs_ty, result_ty) = type_of_binop op in
      let* () = check ctx lhs lhs_ty in
      let* () = check ctx rhs rhs_ty in
      (* String-wall slice 9: `==`/`!=` are polymorphic ('a -> 'a -> Bool),
         so a String comparison lands here rather than in the [comparison]
         branch. After the checks pin [lhs_ty], record the node (physical
         identity) for elaboration to [ExprStringEq] — otherwise codegen
         lowers it to [I32Eq], comparing string *pointers* not bytes. *)
      (match op with
       | OpEq | OpNe ->
         (match repr lhs_ty with
          | TCon "String" -> string_eq_sites := concat_node :: !string_eq_sites
          | TCon "Float" -> float_binop_sites := concat_node :: !float_binop_sites
          | _ -> ())
       | _ -> ());
      Ok result_ty
    end

  (* Unary operators — OpNeg dispatches Int/Float on operand, like binops. *)
  | ExprUnary (op, operand) ->
    (match op with
     | OpNeg ->
       let* operand_ty = synth ctx operand in
       (match repr operand_ty with
        | TCon "Float" -> Ok ty_float
        | _ ->
          let* () = unify_or_err operand_ty ty_int in
          Ok ty_int)
     | OpDeref ->
       (* Lenient deref: `*e` peels one borrow layer when `e` is a
          reference type, but is the identity on a value type. Params
          declared with a `ref`/`mut` mode are lowered to their bare
          value type (the borrow checker tracks the actual borrow), so
          stdlib code that reads them via `*self` / `*other` must still
          type-check. Real `TRef`/`TMut`/`TOwn` still peel to the inner
          type. *)
       let* operand_ty = synth ctx operand in
       (match repr operand_ty with
        | TRef t | TMut t | TOwn t -> Ok t
        | t -> Ok t)
     | _ ->
       let (operand_ty, result_ty) = type_of_unop op in
       let* () = check ctx operand operand_ty in
       Ok result_ty)

  (* Block *)
  | ExprBlock blk ->
    synth_block ctx blk

  (* Return — return type is Never (it doesn't produce a value locally) *)
  | ExprReturn expr_opt ->
    begin match expr_opt with
      | Some e ->
        let* _ty = synth ctx e in
        Ok ty_never
      | None ->
        Ok ty_never
    end

  (* Break / continue — diverging like return.  Loop-context check
     happens at the statement-walker boundary (StmtWhile/StmtFor flip
     ctx.in_loop); top-level break/continue is rejected there. #459. *)
  | ExprBreak _ ->
    if ctx.in_loop then Ok ty_never
    else Error (NotInLoop "break")
  | ExprContinue _ ->
    if ctx.in_loop then Ok ty_never
    else Error (NotInLoop "continue")

  (* Variant constructor: Type::Variant *)
  | ExprVariant ({ name = _type_name; _ }, { name = variant_name; _ }) ->
    begin match Hashtbl.find_opt ctx.constructor_env variant_name with
      | Some ctor_ty -> Ok ctor_ty
      | None ->
        (* Unknown variant — return a fresh variable *)
        Ok (fresh_tyvar ctx.level)
    end

  (* Row restriction *)
  | ExprRowRestrict (obj, { name = field; _ }) ->
    let* obj_ty = synth ctx obj in
    let field_ty = fresh_tyvar ctx.level in
    let rest_row = fresh_rowvar ctx.level in
    let* () = unify_or_err obj_ty (TRecord (RExtend (field, field_ty, rest_row))) in
    Ok (TRecord rest_row)

  (* Span wrapper — unwrap and recurse *)
  | ExprSpan (inner, _span) ->
    synth ctx inner

  (* Effect handling *)
  | ExprHandle { eh_body; _ } ->
    synth ctx eh_body

  (* Resume *)
  | ExprResume expr_opt ->
    begin match expr_opt with
      | Some e -> synth ctx e
      | None -> Ok ty_unit
    end

  (* Try-catch-finally.
     Body type is synthesised first and becomes the overall result type.
     Each catch arm is type-checked against a fresh error-type variable
     (the effect system will constrain this once effect inference is
     complete) and its body type must unify with the result type.
     The finally block (if present) is checked for unit — its value is
     discarded at runtime; a non-unit finally type is a type error. *)
  | ExprTry { et_body; et_catch; et_finally } ->
    let* body_ty = synth_block ctx et_body in
    let result_ty = fresh_tyvar ctx.level in
    let* () = unify_or_err result_ty body_ty in
    let* () = match et_catch with
      | None -> Ok ()
      | Some arms ->
          (* All catch arms match against a single opaque error type. *)
          let err_ty = fresh_tyvar ctx.level in
          List.fold_left (fun acc (arm : match_arm) ->
            let* () = acc in
            let* bindings = check_pattern ctx arm.ma_pat err_ty in
            (* Save bindings that will be shadowed, then install new ones. *)
            let old = List.map (fun (n, _) ->
              (n, Hashtbl.find_opt ctx.name_types n)
            ) bindings in
            List.iter (fun (n, t) -> bind_var ctx n t) bindings;
            let* arm_ty = synth ctx arm.ma_body in
            let* () = unify_or_err result_ty arm_ty in
            (* Restore previous bindings. *)
            List.iter (fun (n, old_sc) ->
              match old_sc with
              | Some sc -> Hashtbl.replace ctx.name_types n sc
              | None    -> Hashtbl.remove ctx.name_types n
            ) old;
            Ok ()
          ) (Ok ()) arms
    in
    let* () = match et_finally with
      | None -> Ok ()
      | Some blk ->
          (* Finally must be unit — its value is always discarded. *)
          let* fin_ty = synth_block ctx blk in
          unify_or_err fin_ty ty_unit
    in
    (* issue #59: a catch-less `try` — including the `e?` desugar
       (parser.mly: `expr_postfix QUESTION`) — lets failure
       short-circuit out of the body, so the enclosing function
       performs `Partial`. A handled `try` (a catch arm is present)
       discharges the failure locally and adds no effect. This is the
       single concrete effect source wired for tracking-only v1; the
       row is enforced against the declared one in [check_fn_decl]. *)
    (match et_catch with
     | None ->
       ctx.current_eff <- Effect.union_eff ctx.current_eff (ESingleton "Partial")
     | Some _ -> ());
    Ok result_ty

  (* Unsafe *)
  | ExprUnsafe _ ->
    Ok (fresh_tyvar ctx.level)

(** Apply a function type to a list of arguments. *)
and apply_args (ctx : context) (fn_ty : ty) (args : expr list) : ty result =
  match args with
  | [] -> Ok fn_ty
  | arg :: rest ->
    let fn_ty' = repr fn_ty in
    match fn_ty' with
      | TArrow (param_ty, _q, ret_ty, _eff) ->
        let* () = check ctx arg param_ty in
        apply_args ctx ret_ty rest
      | TVar _ ->
        (* Unknown function type: create fresh arrow *)
        let param_ty = fresh_tyvar ctx.level in
        let ret_ty = fresh_tyvar ctx.level in
        let eff = fresh_effvar ctx.level in
        let q = lower_quantity QOmega in (* Default for unknown *)
        let* () = unify_or_err fn_ty' (TArrow (param_ty, q, ret_ty, eff)) in
        let* () = check ctx arg param_ty in
        apply_args ctx ret_ty rest
      | _ ->
        Error (NotAFunction fn_ty')
and synth_list (ctx : context) (exprs : expr list) : (ty list) result =
  List.fold_right (fun e acc ->
    let* tys = acc in
    let* ty = synth ctx e in
    Ok (ty :: tys)
  ) exprs (Ok [])

(** {1 Block and statement typing} *)

(** Returns true if an expression always diverges — i.e., it never produces
    a value in normal control flow. Used to give blocks a Never type when
    all paths exit via return. *)
and always_diverges (e : expr) : bool =
  match e with
  | ExprReturn _ -> true
  | ExprBreak _ -> true
  | ExprContinue _ -> true
  | ExprBlock blk -> block_always_diverges blk
  | ExprIf { ei_cond = _; ei_then; ei_else = Some else_e } ->
    always_diverges ei_then && always_diverges else_e
  | _ -> false

(** Returns true if a block always diverges (all paths return). *)
and block_always_diverges (blk : block) : bool =
  match blk.blk_expr with
  | Some e -> always_diverges e
  | None ->
    begin match List.rev blk.blk_stmts with
    | StmtExpr e :: _ -> always_diverges e
    | _ -> false
    end

and synth_block (ctx : context) (blk : block) : ty result =
  (* Type-check each statement for side effects *)
  let* () = List.fold_left (fun acc stmt ->
    let* () = acc in
    check_stmt ctx stmt
  ) (Ok ()) blk.blk_stmts in
  (* The block's type is the type of the final expression, or Unit *)
  match blk.blk_expr with
  | Some e -> synth ctx e
  | None ->
    (* When all paths through the block diverge (every code path ends with
       return/break/etc.), the block has type Never rather than Unit. This
       allows functions declared as returning T to have bodies that exclusively
       use `return expr;` rather than a final expression. *)
    if block_always_diverges blk
    then Ok ty_never
    else Ok ty_unit

and check_stmt (ctx : context) (stmt : stmt) : unit result =
  match stmt with
  | StmtLet { sl_pat; sl_ty; sl_value; sl_mut = _; sl_quantity = _ } ->
    enter_level ctx;
    let* val_ty = begin match sl_ty with
      | Some te ->
        let ann_ty = lower_type_expr ctx te in
        let* () = check ctx sl_value ann_ty in
        Ok ann_ty
      | None ->
        synth ctx sl_value
    end in
    exit_level ctx;
    let* bindings = check_pattern ctx sl_pat val_ty in
    (* Bind each name to *its own* type. For a plain [let x = e] the sole
       binding's type is [val_ty], so this generalizes exactly as before;
       for a destructuring [let (a, b) = e] / record pattern each name is
       generalized at its component type rather than the whole tuple. *)
    List.iter (fun (name, ty) ->
      bind_scheme ctx name (generalize ctx ty)
    ) bindings;
    Ok ()
  | StmtExpr e ->
    let* _ty = synth ctx e in
    Ok ()
  | StmtAssign (lhs, _op, rhs) ->
    let* lhs_ty = synth ctx lhs in
    check ctx rhs lhs_ty
  | StmtWhile (cond, body) ->
    let* () = check ctx cond ty_bool in
    let prev = ctx.in_loop in
    ctx.in_loop <- true;
    let res = synth_block ctx body in
    ctx.in_loop <- prev;
    let* _ty = res in
    Ok ()
  | StmtFor (pat, iter_expr, body) ->
    let* iter_ty = synth ctx iter_expr in
    let elem_ty = fresh_tyvar ctx.level in
    let* () = unify_or_err iter_ty (TApp (TCon "Array", [elem_ty])) in
    let* bindings = check_pattern ctx pat elem_ty in
    let old = List.map (fun (n, _) ->
      (n, Hashtbl.find_opt ctx.name_types n)
    ) bindings in
    List.iter (fun (n, t) -> bind_var ctx n t) bindings;
    let prev = ctx.in_loop in
    ctx.in_loop <- true;
    let res = synth_block ctx body in
    ctx.in_loop <- prev;
    let* _ty = res in
    List.iter (fun (n, old_sc) ->
      match old_sc with
      | Some sc -> Hashtbl.replace ctx.name_types n sc
      | None -> Hashtbl.remove ctx.name_types n
    ) old;
    Ok ()

(** {1 Checking mode (mode ⇐)} *)

(** Check that an expression has the expected type. *)
and check (ctx : context) (expr : expr) (expected : ty) : unit result =
  match expr with
  (* Lambda against arrow type: check mode is more precise.
     We peel the expected arrow type one param at a time.  For each param:
     - If the param has an explicit quantity annotation, we verify it is
       consistent with the arrow quantity from the expected type.
     - The arrow quantity from the expected type is used as the definitive
       quantity for binding (so an unannotated lambda param correctly inherits
       the quantity from its context, e.g. a @linear annotation on the let). *)
  | ExprLambda { elam_params; elam_body; elam_ret_ty = _ }
    when (match repr expected with TArrow _ -> true | _ -> false) ->
    let rec peel_arrows ty params =
      match params, repr ty with
      | [], _ -> Ok ()
      | p :: rest, TArrow (param_ty, q, ret_ty, _eff) ->
        (* Validate explicit quantity annotation against the expected arrow. *)
        let* () = match p.p_quantity with
          | Some pq ->
            let pq' = lower_quantity pq in
            if pq' = q then Ok ()
            else Error (TypeMismatch {
              expected = TArrow (param_ty, q,   ret_ty, EPure);
              got      = TArrow (param_ty, pq', ret_ty, EPure);
            })
          | None -> Ok ()
        in
        bind_var ctx p.p_name.name param_ty;
        peel_arrows ret_ty rest
      | _ -> synth_and_unify ctx expr expected
    in
    let old = List.map (fun (p : param) ->
      (p.p_name.name, Hashtbl.find_opt ctx.name_types p.p_name.name)
    ) elam_params in
    let* () = peel_arrows expected elam_params in
    (* Now check the body against the final return type *)
    let final_ret = List.fold_left (fun ty _ ->
      match repr ty with
      | TArrow (_, _, ret, _) -> ret
      | _ -> ty
    ) expected elam_params in
    let* () = check ctx elam_body final_ret in
    (* Restore *)
    List.iter (fun (n, old_sc) ->
      match old_sc with
      | Some sc -> Hashtbl.replace ctx.name_types n sc
      | None -> Hashtbl.remove ctx.name_types n
    ) old;
    Ok ()

  (* If without else against Unit *)
  | ExprIf { ei_cond; ei_then; ei_else = None } ->
    let* () = check ctx ei_cond ty_bool in
    let* () = check ctx ei_then ty_unit in
    unify_or_err expected ty_unit

  (* Default: synth and unify *)
  | _ ->
    synth_and_unify ctx expr expected

and synth_and_unify (ctx : context) (expr : expr) (expected : ty) : unit result =
  let* got = synth ctx expr in
  unify_or_err expected got

(** {1 String-concat elaboration (slice 8b)} *)

(* Rewrite every `++` node {!synth} recorded as a String concat into
   [ExprStringConcat], leaving array `++` as [ExprBinary _ OpConcat _]. The
   traversal mirrors {!Resolve.lower_expr} exactly so it is total over the
   expression grammar — any constructor it failed to descend into would leave
   a String `++` un-elaborated, where the slice-8a guard would (loudly) catch
   the obvious cases and a var-var case could still miscompile. *)
let rec elab_expr (e : expr) : expr =
  match e with
  | ExprBinary (l, op, r) ->
    let l' = elab_expr l in
    let r' = elab_expr r in
    if List.memq e !string_concat_sites
    then ExprStringConcat (l', r')
    else if List.memq e !string_eq_sites
    then ExprStringEq (l', r', (match op with OpNe -> true | _ -> false))
    else if List.memq e !string_rel_sites
    then ExprStringRel (l', r', op)
    else if List.memq e !float_binop_sites
    then ExprFloatBinary (l', op, r')
    else ExprBinary (l', op, r')
  | ExprStringConcat (l, r) -> ExprStringConcat (elab_expr l, elab_expr r)
  | ExprStringEq (l, r, neg) -> ExprStringEq (elab_expr l, elab_expr r, neg)
  | ExprStringRel (l, r, op) -> ExprStringRel (elab_expr l, elab_expr r, op)
  | ExprFloatBinary (l, op, r) -> ExprFloatBinary (elab_expr l, op, elab_expr r)
  | ExprSpan (e', sp) -> ExprSpan (elab_expr e', sp)
  | ExprLit _ | ExprVar _ | ExprVariant _ -> e
  | ExprField (base, fld) ->
    (* Float heap wall: rewrite `r.f` on a closed float-bearing record. *)
    (match List.assq_opt e !cell_field_sites with
     | Some (offset, is_f64) -> ExprCellField (elab_expr base, offset, is_f64)
     | None -> ExprField (elab_expr base, fld))
  | ExprCellField (base, off, k) -> ExprCellField (elab_expr base, off, k)
  | ExprLet r ->
    ExprLet { r with el_value = elab_expr r.el_value;
                     el_body = Option.map elab_expr r.el_body }
  | ExprIf r ->
    ExprIf { ei_cond = elab_expr r.ei_cond;
             ei_then = elab_expr r.ei_then;
             ei_else = Option.map elab_expr r.ei_else }
  | ExprMatch r ->
    ExprMatch { em_scrutinee = elab_expr r.em_scrutinee;
                em_arms = List.map elab_arm r.em_arms }
  | ExprLambda r -> ExprLambda { r with elam_body = elab_expr r.elam_body }
  | ExprApp (f, args) -> ExprApp (elab_expr f, List.map elab_expr args)
  | ExprTupleIndex (e1, i) ->
    (* Float heap wall: rewrite a float-bearing tuple's `t.i` into the cell load. *)
    (match List.assq_opt e !cell_tuple_index_sites with
     | Some is_f64 -> ExprCellTupleIndex (elab_expr e1, i, is_f64)
     | None -> ExprTupleIndex (elab_expr e1, i))
  | ExprCellTupleIndex (e1, i, k) -> ExprCellTupleIndex (elab_expr e1, i, k)
  | ExprIndex (a, i) ->
    (* Float heap wall: rewrite a `Float`-yielding index into the f64 load. *)
    if List.memq e !float_heap_sites
    then ExprFloatIndex (elab_expr a, elab_expr i)
    else ExprIndex (elab_expr a, elab_expr i)
  | ExprFloatIndex (a, i) -> ExprFloatIndex (elab_expr a, elab_expr i)
  | ExprTuple es ->
    (* Float heap wall: rewrite a float-bearing tuple into uniform 8-byte cells. *)
    (match List.assq_opt e !cell_tuple_sites with
     | Some kinds -> ExprCellTuple (List.map2 (fun el k -> (elab_expr el, k)) es kinds)
     | None -> ExprTuple (List.map elab_expr es))
  | ExprCellTuple kes -> ExprCellTuple (List.map (fun (el, k) -> (elab_expr el, k)) kes)
  | ExprArray es ->
    (* Float heap wall: rewrite an [Float]-element array into 8-byte f64 cells. *)
    if List.memq e !float_heap_sites
    then ExprFloatArray (List.map elab_expr es)
    else ExprArray (List.map elab_expr es)
  | ExprFloatArray es -> ExprFloatArray (List.map elab_expr es)
  | ExprRecord r ->
    (* Float heap wall: rewrite a closed float-bearing record literal. *)
    (match List.assq_opt e !cell_record_sites with
     | Some kinds ->
       ExprCellRecord (List.map (fun (id, eo) ->
         let v = match eo with Some ex -> elab_expr ex | None -> ExprVar id in
         let is_f64 = match List.assoc_opt id.name kinds with Some b -> b | None -> false in
         (id, v, is_f64)) r.er_fields)
     | None ->
       ExprRecord
         { er_fields =
             List.map (fun (id, eo) -> (id, Option.map elab_expr eo)) r.er_fields;
           er_spread = Option.map elab_expr r.er_spread })
  | ExprCellRecord fs ->
    ExprCellRecord (List.map (fun (id, ex, k) -> (id, elab_expr ex, k)) fs)
  | ExprRowRestrict (e1, id) -> ExprRowRestrict (elab_expr e1, id)
  | ExprUnary (op, e1) -> ExprUnary (op, elab_expr e1)
  | ExprBlock b -> ExprBlock (elab_block b)
  | ExprReturn eo -> ExprReturn (Option.map elab_expr eo)
  | ExprBreak _ | ExprContinue _ -> e
  | ExprTry r ->
    ExprTry { et_body = elab_block r.et_body;
              et_catch = Option.map (List.map elab_arm) r.et_catch;
              et_finally = Option.map elab_block r.et_finally }
  | ExprHandle r ->
    ExprHandle { eh_body = elab_expr r.eh_body;
                 eh_handlers = List.map elab_handler r.eh_handlers }
  | ExprResume eo -> ExprResume (Option.map elab_expr eo)
  | ExprUnsafe ops -> ExprUnsafe (List.map elab_unsafe ops)

and elab_arm a =
  { a with ma_guard = Option.map elab_expr a.ma_guard;
           ma_body = elab_expr a.ma_body }

and elab_handler = function
  | HandlerReturn (p, e) -> HandlerReturn (p, elab_expr e)
  | HandlerOp (id, ps, e) -> HandlerOp (id, ps, elab_expr e)

and elab_unsafe = function
  | UnsafeRead e -> UnsafeRead (elab_expr e)
  | UnsafeWrite (a, b) -> UnsafeWrite (elab_expr a, elab_expr b)
  | UnsafeOffset (a, b) -> UnsafeOffset (elab_expr a, elab_expr b)
  | UnsafeTransmute (t1, t2, e) -> UnsafeTransmute (t1, t2, elab_expr e)
  | UnsafeForget e -> UnsafeForget (elab_expr e)

and elab_block b =
  { blk_stmts = List.map elab_stmt b.blk_stmts;
    blk_expr = Option.map elab_expr b.blk_expr }

and elab_stmt = function
  | StmtLet r -> StmtLet { r with sl_value = elab_expr r.sl_value }
  | StmtExpr e -> StmtExpr (elab_expr e)
  | StmtAssign (a, op, b) -> StmtAssign (elab_expr a, op, elab_expr b)
  | StmtWhile (e, b) -> StmtWhile (elab_expr e, elab_block b)
  | StmtFor (p, e, b) -> StmtFor (p, elab_expr e, elab_block b)

let elab_fn_body = function
  | FnBlock b -> FnBlock (elab_block b)
  | FnExpr e -> FnExpr (elab_expr e)
  | FnExtern -> FnExtern

let elab_top = function
  | TopFn fd -> TopFn { fd with fd_body = elab_fn_body fd.fd_body }
  | TopConst r -> TopConst { r with tc_value = elab_expr r.tc_value }
  | TopImpl ib ->
    TopImpl { ib with ib_items = List.map (function
      | ImplFn fd -> ImplFn { fd with fd_body = elab_fn_body fd.fd_body }
      | ImplType _ as it -> it) ib.ib_items }
  | TopTrait td ->
    TopTrait { td with trd_items = List.map (function
      | TraitFnDefault fd ->
        TraitFnDefault { fd with fd_body = elab_fn_body fd.fd_body }
      | other -> other) td.trd_items }
  | (TopType _ | TopEffect _ | TopExternType _ | TopExternFn _) as t -> t

(** Rewrite the String case of `++` to {!Ast.ExprStringConcat} across [program],
    using the sites {!synth} recorded during type-checking. Pure apart from
    clearing the recorded sites; returns [program] unchanged when nothing was
    recorded. Intended to run on the wasm-codegen path only (the interpreter
    and other backends handle String `++` directly). *)
let elaborate_string_concat (program : program) : program =
  (* Drives both the slice-8b String-`++` rewrite and the slice-9 String
     `==`/`!=` rewrite — [elab_expr] consults both site lists, so one walk
     (and the existing single wasm-path call site) covers both. *)
  let any_sites =
    !string_concat_sites <> [] || !string_eq_sites <> [] || !string_rel_sites <> []
    || !float_binop_sites <> [] || !float_heap_sites <> []
    || !cell_tuple_sites <> [] || !cell_tuple_index_sites <> []
    || !cell_record_sites <> [] || !cell_field_sites <> []
  in
  let result =
    if any_sites
    then { program with prog_decls = List.map elab_top program.prog_decls }
    else program
  in
  reset_string_concat_sites ();
  reset_string_eq_sites ();
  reset_string_rel_sites ();
  reset_float_binop_sites ();
  reset_float_heap_sites ();
  reset_cell_tuple_sites ();
  reset_cell_tuple_index_sites ();
  reset_cell_record_sites ();
  reset_cell_field_sites ();
  result

(** {1 Declaration checking} *)

(** Register built-in types and functions. *)
let register_builtins (ctx : context) : unit =
  (* Arithmetic builtins *)
  let int_binop = TArrow (ty_int, QOmega, TArrow (ty_int, QOmega, ty_int, EPure), EPure) in
  let float_binop = TArrow (ty_float, QOmega, TArrow (ty_float, QOmega, ty_float, EPure), EPure) in
  bind_var ctx "print" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
  bind_var ctx "println" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
  (* ADR-015 S4a (#180): WASI clock primitive. `clock_now_ms(clock_id)`
     -> Int (monotonic/realtime milliseconds, clock_id 0=realtime/
     1=monotonic). Tracking effect `Time` (reserved). Lowers to a
     `wasi_snapshot_preview1.clock_time_get` import on the wasm
     target; on the S3 component path the reactor adapter bridges to
     `wasi:clocks`. *)
  bind_var ctx "clock_now_ms"
    (TArrow (ty_int, QOmega, ty_int, ESingleton "Time"));
  (* ADR-015 S4b (#180): WASI environment / argv COUNTS. The Unit arg
     satisfies the zero-param-fn collapse wart (`fn()->T` lowers to
     bare `T`; callable zero-arg builtins take `Unit -> R`). String
     accessors (env_at/arg_at) need byte-level wasm IR ops — tracked
     follow-up. Effect row `Time` (reserved). *)
  bind_var ctx "env_count" (TArrow (ty_unit, QOmega, ty_int, ESingleton "Time"));
  bind_var ctx "arg_count" (TArrow (ty_unit, QOmega, ty_int, ESingleton "Time"));
  (* ADR-015 S5 (#180): env_at(i) / arg_at(i) -> String / Time.
     Lowers via [Wasi_runtime.gen_str_at_via_get] (8-local scratch +
     byte-scan + heap-allocated AS string). Effect row matches the
     count siblings since they share the WASI environ/args surface. *)
  bind_var ctx "env_at" (TArrow (ty_int, QOmega, ty_string, ESingleton "Time"));
  bind_var ctx "arg_at" (TArrow (ty_int, QOmega, ty_string, ESingleton "Time"));
  (* ADR-015 S6b (#180): WASI socket primitive. `net_shutdown(fd, how)`
     -> Int errno (0 on success, ENOTSOCK on a non-socket fd, etc.).
     `how`: 1 = RD, 2 = WR, 3 = RDWR. Lowers to a
     `wasi_snapshot_preview1.sock_shutdown` import; under the S3+S6a
     component path the command adapter bridges to `wasi:sockets/tcp`.
     Larger socket primitives (recv/send/accept) need byte-level wasm
     IR for buffer / network-address marshalling and remain a tracked
     follow-up alongside env_at/arg_at. Effect row `Net`. *)
  bind_var ctx "net_shutdown"
    (TArrow (ty_int, QOmega,
             TArrow (ty_int, QOmega, ty_int, ESingleton "Net"),
             ESingleton "Net"));
  bind_var ctx "eprint" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
  bind_var ctx "eprintln" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
  bind_var ctx "read_line"
    (TArrow (ty_unit, QOmega, TApp (TCon "Result", [ty_string; ty_string]), ESingleton "IO"));
  bind_var ctx "int_to_string" (TArrow (ty_int, QOmega, ty_string, EPure));
  bind_var ctx "int" (TArrow (ty_float, QOmega, ty_int, EPure));
  bind_var ctx "float" (TArrow (ty_int, QOmega, ty_float, EPure));
  bind_var ctx "float_to_string" (TArrow (ty_float, QOmega, ty_string, EPure));
  bind_var ctx "string_length" (TArrow (ty_string, QOmega, ty_int, EPure));
  bind_var ctx "sqrt" (TArrow (ty_float, QOmega, ty_float, EPure));
  bind_var ctx "abs" int_binop;
  bind_var ctx "max" int_binop;
  bind_var ctx "min" int_binop;
  bind_var ctx "pow_float" float_binop;
  (* `len` / `show` are TRULY polymorphic — bound as generalized schemes
     so each call site instantiates a fresh tyvar. v2.5/v2.6 mistakenly
     bound them via bind_var as `'a -> _` with a SINGLE SHARED tyvar:
     the first `len(String)` pinned it, then `len([T])` failed with
     `Unify TypeMismatch (String, Array[T])` (diagnosed via the sb7
     minimal repro; blocked the ubicity#30 storage port). issue #122. *)
  let poly1 (body_of : ty -> ty) : scheme =
    let tv = fresh_tyvar 0 in
    let v = (match tv with
      | TVar r -> (match !r with Unbound (v, _) -> v | _ -> assert false)
      | _ -> assert false) in
    { sc_tyvars = [(v, Types.KType)]; sc_effvars = []; sc_rowvars = [];
      sc_body = body_of tv }
  in
  bind_scheme ctx "len" (poly1 (fun a -> TArrow (a, QOmega, ty_int, EPure)));
  (* slice : a -> Int -> Int -> a  (issue #135 slice 2; arrays and strings,
     mirroring `len`'s permissive `a`).  Curried like other builtin schemes. *)
  bind_scheme ctx "slice"
    (poly1 (fun a ->
       TArrow (a, QOmega,
         TArrow (ty_int, QOmega,
           TArrow (ty_int, QOmega, a, EPure), EPure), EPure)));
  (* Honest string/char primitives underpinning stdlib/string.affine
     (issue #122 v2.5). Concrete String/Char types; the Deno-ESM backend
     lowers each to a JS intrinsic. char ::= TCon "Char". *)
  let ty_char = TCon "Char" in
  (* Option/Result type constructors, used only to spell the *types* of
     builtin signatures (parse_int, read_file, …) — not the value
     constructors. *)
  let opt t = TApp (TCon "Option", [t]) in
  let res a b = TApp (TCon "Result", [a; b]) in
  (* #138: Some/None/Ok/Err are no longer seeded as polymorphic builtin
     schemes. The stdlib now resolves them through the proper module
     path — prelude.affine declares `type Option`/`type Result` and
     every consumer does `use prelude::{Some, None, Ok, Err}`. Removing
     the b895374 / #122 front-end band-aid keeps it from becoming
     load-bearing now that real resolution + the module model have
     landed (stdlib 19/19). Codegen still provides the runtime. *)
  let fresh_named () =
    let tv = fresh_tyvar 0 in
    let v = (match tv with
      | TVar r -> (match !r with Unbound (v, _) -> v | _ -> assert false)
      | _ -> assert false) in
    (v, tv)
  in
  (* [RuntimeError(String)] is the interpreter's builtin exception variant
     (see [Interp]: panics surface as [VVariant ("RuntimeError", VString
     msg)]). The honest stdlib pattern-matches it in [try/catch] arms
     (stdlib/testing.affine, stdlib/result.affine). The catch error type is
     opaque (a fresh tyvar per [try]), so the result is left polymorphic and
     unifies with whatever the arm expects. *)
  let (v_rte, t_rte) = fresh_named () in
  let rte_ty = TArrow (ty_string, QOmega, t_rte, EPure) in
  bind_scheme ctx "RuntimeError"
    { sc_tyvars = [(v_rte, Types.KType)]; sc_effvars = []; sc_rowvars = [];
      sc_body = rte_ty };
  Hashtbl.replace ctx.constructor_env "RuntimeError" rte_ty;
  bind_var ctx "string_get"
    (TArrow (ty_string, QOmega, TArrow (ty_int, QOmega, ty_char, EPure), EPure));
  bind_var ctx "string_sub"
    (TArrow (ty_string, QOmega,
       TArrow (ty_int, QOmega,
         TArrow (ty_int, QOmega, ty_string, EPure), EPure), EPure));
  bind_var ctx "string_find"
    (TArrow (ty_string, QOmega,
       TArrow (ty_string, QOmega, ty_int, EPure), EPure));
  bind_var ctx "to_lowercase" (TArrow (ty_string, QOmega, ty_string, EPure));
  bind_var ctx "to_uppercase" (TArrow (ty_string, QOmega, ty_string, EPure));
  bind_var ctx "trim"         (TArrow (ty_string, QOmega, ty_string, EPure));
  bind_var ctx "parse_int"    (TArrow (ty_string, QOmega, opt ty_int, EPure));
  bind_var ctx "parse_float"  (TArrow (ty_string, QOmega, opt ty_float, EPure));
  bind_var ctx "char_to_int"  (TArrow (ty_char, QOmega, ty_int, EPure));
  bind_var ctx "int_to_char"  (TArrow (ty_int, QOmega, ty_char, EPure));
  (* Byte-oriented String accessors underpinning stdlib/encoding.affine's
     base64. Unlike string_get/int_to_char (which traffic in [Char] and, on
     the interpreter, clamp to ASCII), these go String<->Int directly so a
     byte 0..255 round-trips on both the interpreter and the Deno-ESM
     backend. string_from_char_code masks its argument to the low 8 bits. *)
  bind_var ctx "string_char_code_at"
    (TArrow (ty_string, QOmega, TArrow (ty_int, QOmega, ty_int, EPure), EPure));
  bind_var ctx "string_from_char_code"
    (TArrow (ty_int, QOmega, ty_string, EPure));
  bind_scheme ctx "show"
    (poly1 (fun a -> TArrow (a, QOmega, ty_string, EPure)));
  (* Reconcile with the resolver builtin-seed list (resolve.ml seed_builtins):
     file-I/O / env / time / float-math builtins were seeded for resolution
     but never typed here, so stdlib files using them failed typecheck with
     "Unbound variable". Signatures per the io.affine / math.affine headers. *)
  (* File I/O — effectful, Result/Option-returning *)
  bind_var ctx "read_file"
    (TArrow (ty_string, QOmega, res ty_string ty_string, ESingleton "IO"));
  bind_var ctx "write_file"
    (TArrow (ty_string, QOmega,
       TArrow (ty_string, QOmega, res ty_unit ty_string, ESingleton "IO"), EPure));
  bind_var ctx "append_file"
    (TArrow (ty_string, QOmega,
       TArrow (ty_string, QOmega, res ty_unit ty_string, ESingleton "IO"), EPure));
  bind_var ctx "file_exists" (TArrow (ty_string, QOmega, ty_bool, ESingleton "IO"));
  bind_var ctx "is_directory" (TArrow (ty_string, QOmega, ty_bool, ESingleton "IO"));
  (* Environment / process / time *)
  bind_var ctx "getenv" (TArrow (ty_string, QOmega, opt ty_string, ESingleton "IO"));
  bind_var ctx "getcwd" (TArrow (ty_unit, QOmega, res ty_string ty_string, ESingleton "IO"));
  bind_var ctx "time_now" (TArrow (ty_unit, QOmega, ty_float, ESingleton "IO"));
  (* Float math — pure; floor/ceil/round/trunc truncate to Int per headers *)
  let f_to_i = TArrow (ty_float, QOmega, ty_int, EPure) in
  let f_to_f = TArrow (ty_float, QOmega, ty_float, EPure) in
  bind_var ctx "floor" f_to_i; bind_var ctx "ceil" f_to_i;
  bind_var ctx "round" f_to_i; bind_var ctx "trunc" f_to_i;
  bind_var ctx "sin" f_to_f; bind_var ctx "cos" f_to_f; bind_var ctx "tan" f_to_f;
  bind_var ctx "atan" f_to_f; bind_var ctx "exp" f_to_f; bind_var ctx "cbrt" f_to_f;
  bind_var ctx "log" f_to_f; bind_var ctx "log10" f_to_f; bind_var ctx "log2" f_to_f;
  bind_var ctx "atan2"
    (TArrow (ty_float, QOmega, TArrow (ty_float, QOmega, ty_float, EPure), EPure));
  bind_var ctx "panic" (TArrow (ty_string, QOmega, ty_never, EPure));
  bind_var ctx "exit" (TArrow (ty_int, QOmega, ty_never, ESingleton "IO"));
  (* TEA runtime — accepts any record, returns unit with IO effect *)
  let tea_tv = fresh_tyvar 0 in
  bind_var ctx "tea_run" (TArrow (tea_tv, QOmega, ty_unit, ESingleton "IO"));
  (* Cmd Msg — linear side-effect obligation type (Stage 11).
     Cmd has kind * → *.
     cmd_none : Cmd 'a — the no-op command; a linear value obligating zero IO.
     cmd_perform : (unit ->{IO} unit) -> Cmd 'a — wraps an IO action as a Cmd.
     Cmd values bound with a [Cmd _] type annotation are automatically
     treated as QOne (linear) by the quantity checker. *)
  let cmd_tv  = fresh_tyvar 0 in
  let cmd_tv2 = fresh_tyvar 0 in
  bind_var ctx "cmd_none"
    (TApp (TCon "Cmd", [cmd_tv]));
  bind_var ctx "cmd_perform"
    (TArrow (TArrow (ty_unit, QOmega, ty_unit, ESingleton "IO"),
             QOmega,
             TApp (TCon "Cmd", [cmd_tv2]),
             EPure))

(** Check a top-level function declaration. *)
let check_fn_decl (ctx : context) (fd : fn_decl) : unit result =
  (* #135 slice 7: register the explicit `<T>` type parameters as fresh,
     generalizable unification variables before lowering param/return
     types.  Without this, an uppercase param like `x: T` lowered to a
     *rigid* `TCon "T"` (lower_type_expr TyCon fallthrough), which
     `generalize` ignores — so every generic top-level function was
     effectively monomorphic and the second instantiation blew up with
     `Unify.TypeMismatch (T, Int)` (and `use prelude::{…}` import-checks
     failed transitively).  Mirrors the let-generalization discipline:
     enter a deeper level, create the vars there, generalize at the outer
     level so they become the scheme's quantified tyvars. *)
  let tp_names = List.map (fun (tp : type_param) -> tp.tp_name.name)
      fd.fd_type_params in
  let saved_tp = List.map (fun n -> (n, Hashtbl.find_opt ctx.type_env n))
      tp_names in
  enter_level ctx;
  List.iter (fun n ->
    Hashtbl.replace ctx.type_env n (fresh_tyvar ctx.level)) tp_names;
  let restore_tp () =
    List.iter (fun (n, old) -> match old with
      | Some t -> Hashtbl.replace ctx.type_env n t
      | None -> Hashtbl.remove ctx.type_env n) saved_tp
  in
  (* Extern functions have no body — register the signature so callers can
     typecheck against it, then bail out before the body-check pass. *)
  if fd.fd_body = FnExtern then begin
    let* param_tys = List.fold_left (fun acc (p : param) ->
      let* tys = acc in
      let ty = lower_type_expr ctx p.p_ty in
      let* () = check_kind ctx ty KType in
      Ok (ty :: tys)
    ) (Ok []) fd.fd_params in
    let param_tys = List.rev param_tys in
    let* ret_ty = match fd.fd_ret_ty with
      | Some te ->
        let ty = lower_type_expr ctx te in
        let* () = check_kind ctx ty KType in
        Ok ty
      | None -> Ok (fresh_tyvar ctx.level)
    in
    let fn_eff = match fd.fd_eff with
      | Some ee -> lower_effect_expr ctx ee
      | None -> fresh_effvar ctx.level
    in
    let fn_ty = List.fold_right2 (fun param_ty (p : param) acc ->
      let q = match p.p_quantity with
        | Some q -> lower_quantity q
        | None -> QOmega
      in
      TArrow (param_ty, q, acc, fn_eff)
    ) param_tys fd.fd_params ret_ty in
    exit_level ctx;
    let sc = generalize ctx fn_ty in
    bind_scheme ctx fd.fd_name.name sc;
    restore_tp ();
    Ok ()
  end
  else
  (* Lower parameter types *)
  let* param_tys = List.fold_left (fun acc (p : param) ->
    let* tys = acc in
    let ty = lower_type_expr ctx p.p_ty in
    let* () = check_kind ctx ty KType in
    Ok (ty :: tys)
  ) (Ok []) fd.fd_params in
  let param_tys = List.rev param_tys in
  (* Lower return type *)
  let* ret_ty = match fd.fd_ret_ty with
    | Some te ->
      let ty = lower_type_expr ctx te in
      let* () = check_kind ctx ty KType in
      Ok ty
    | None -> Ok (fresh_tyvar ctx.level)
  in
  (* Lower effect *)
  (* Build the function type *)
  let fn_eff = match fd.fd_eff with
    | Some ee -> lower_effect_expr ctx ee
    | None -> fresh_effvar ctx.level
  in
  let fn_ty = List.fold_right2 (fun param_ty (p : param) acc ->
    let q = match p.p_quantity with
      | Some q -> lower_quantity q
      | None -> QOmega
    in
    TArrow (param_ty, q, acc, fn_eff)
  ) param_tys fd.fd_params ret_ty in
  (* Bind the function name (allows recursion) *)
  bind_var ctx fd.fd_name.name fn_ty;
  (* Bind parameters *)
  let old = List.map2 (fun (p : param) ty ->
    let old = Hashtbl.find_opt ctx.name_types p.p_name.name in
    bind_var ctx p.p_name.name ty;
    (p.p_name.name, old)
  ) fd.fd_params param_tys in
  (* issue #59 — effect inference spine: infer this body's effect row
     into a fresh accumulator, then (only if a row was explicitly
     declared) require the inferred row to be a subset of it. An
     undeclared row stays permissive under tracking-only v1. *)
  let saved_eff = ctx.current_eff in
  ctx.current_eff <- EPure;
  (* Check the body against the return type *)
  let* () = begin match fd.fd_body with
    | FnBlock blk ->
      let* body_ty = synth_block ctx blk in
      unify_or_err ret_ty body_ty
    | FnExpr e ->
      check ctx e ret_ty
  end in
  (* Restore parameter bindings *)
  List.iter (fun (n, old_sc) ->
    match old_sc with
    | Some sc -> Hashtbl.replace ctx.name_types n sc
    | None -> Hashtbl.remove ctx.name_types n
  ) old;
  let inferred_eff = ctx.current_eff in
  ctx.current_eff <- saved_eff;
  let* () =
    match fd.fd_eff with
    | Some _ when not (Effect.eff_subset inferred_eff fn_eff) ->
      Error (EffectNotDeclared {
        inferred = Effect.string_of_eff inferred_eff;
        declared = Effect.string_of_eff fn_eff;
      })
    | _ -> Ok ()
  in
  (* Generalize and rebind the function with its polymorphic type.
     exit_level first so the `<T>` type-param vars (created at the deeper
     level above) are quantified by `generalize` (#135 slice 7). *)
  exit_level ctx;
  let sc = generalize ctx fn_ty in
  bind_scheme ctx fd.fd_name.name sc;
  restore_tp ();
  Ok ()

(** Register a type declaration in the context. *)
let register_type_decl (ctx : context) (td : type_decl) : unit result =
  let* ty = match td.td_body with
    | TyAlias te ->
      let ty = lower_type_expr ctx te in
      let* () = check_kind ctx ty KType in
      Ok ty
    | TyStruct fields ->
      (* Register struct as a record type constructor *)
      let row = List.fold_right (fun (sf : struct_field) acc ->
        RExtend (sf.sf_name.name, lower_type_expr ctx sf.sf_ty, acc)
      ) fields REmpty in
      let ty = TRecord row in
      let* () = check_kind ctx ty KType in
      Ok ty
    | TyEnum variants ->
      (* Register each variant as a constructor.

         Bind the declared type-param names (e.g. T, E) to fresh tyvars in
         the type env so that BOTH the result type and the field types
         resolve to the *same* variables (previously the result tyvars were
         anonymous `fresh_tyvar 0` and each field `T` became its own
         unrelated var via lower_type_expr's TyVar fallback).

         The param tyvars are created one level deeper than the current
         context so that `generalize` (which quantifies vars with
         level > ctx.level) actually quantifies them — at level 0 it was a
         no-op, leaving imported ctor schemes monomorphic with shared vars
         (the import-path bug behind result.affine's Unify ((_->_), T)). *)
      let param_names =
        List.map (fun (tp : type_param) -> tp.tp_name.name) td.td_type_params
      in
      enter_level ctx;
      let param_tvs = List.map (fun n ->
        let tv = fresh_tyvar ctx.level in
        Hashtbl.replace ctx.type_env n tv;
        tv
      ) param_names in
      let result_ty = match param_tvs with
        | [] -> TCon td.td_name.name
        | tvs -> TApp (TCon td.td_name.name, tvs)
      in
      let ctors = List.map (fun (vd : variant_decl) ->
        let ctor_ty = List.fold_right (fun field_te acc ->
          TArrow (lower_type_expr ctx field_te, QOmega, acc, EPure)
        ) vd.vd_fields result_ty in
        (vd.vd_name.name, ctor_ty)
      ) variants in
      exit_level ctx;
      (* Don't let this decl's param names leak into sibling type decls. *)
      List.iter (fun n -> Hashtbl.remove ctx.type_env n) param_names;
      List.iter (fun (name, ctor_ty) ->
        let sc = match param_names with
          | [] -> { sc_tyvars = []; sc_effvars = []; sc_rowvars = []; sc_body = ctor_ty }
          | _ -> generalize ctx ctor_ty
        in
        Hashtbl.replace ctx.constructor_env name ctor_ty;
        bind_scheme ctx name sc
      ) ctors;
      Ok (TCon td.td_name.name)
    | TyExtern ->
      (* Opaque host-supplied type. Register a TCon so user code can name it
         in signatures; the body is intentionally absent. *)
      Ok (TCon td.td_name.name)
  in
  Hashtbl.replace ctx.type_env td.td_name.name ty;
  Ok ()

(** Register an effect declaration. *)
let register_effect_decl (ctx : context) (ed : effect_decl) : unit result =
  Hashtbl.replace ctx.declared_effects ed.ed_name.name ();
  List.iter (fun (op : effect_op_decl) ->
    let param_tys = List.map (fun (p : param) ->
      lower_type_expr ctx p.p_ty
    ) op.eod_params in
    let ret_ty = match op.eod_ret_ty with
      | Some te -> lower_type_expr ctx te
      | None -> ty_unit
    in
    let eff = ESingleton ed.ed_name.name in
    let op_ty = List.fold_right (fun pty acc ->
      TArrow (pty, QOmega, acc, eff)
    ) param_tys ret_ty in
    bind_var ctx op.eod_name.name op_ty
  ) ed.ed_ops;
  Ok ()

(** Check a single top-level declaration. *)
let check_decl (ctx : context) (decl : top_level) : (unit, type_error) Result.t =
  match decl with
  | TopFn fd ->
    check_fn_decl ctx fd
  | TopType td ->
    register_type_decl ctx td
  | TopEffect ed ->
    register_effect_decl ctx ed
  | TopTrait _td ->
    (* Trait declarations are registered in the forward pass; nothing to
       re-check here since there are no bodies to type-check in Phase 1. *)
    Ok ()
  | TopImpl ib ->
    (* Type-check each method body in the impl against the trait's declared
       method signatures (where those exist).  Methods whose trait signature
       cannot be found are still checked for internal consistency.

       We also verify that the impl satisfies its trait (all required methods
       are present) using [Trait.check_impl_satisfies_trait]. *)
    let self_ty = lower_type_expr ctx ib.ib_self_ty in
    (* Make Self available as a type alias inside method bodies *)
    let old_self = Hashtbl.find_opt ctx.type_env "Self" in
    Hashtbl.replace ctx.type_env "Self" self_ty;
    (* Build a synthetic trait_impl record for the satisfaction check *)
    let synth_impl = {
      Trait.ti_trait_name = (match ib.ib_trait_ref with
        | Some tr -> tr.Ast.tr_name.name
        | None -> "");
      Trait.ti_trait_args = (match ib.ib_trait_ref with
        | Some tr -> tr.Ast.tr_args
        | None -> []);
      Trait.ti_self_ty = self_ty;
      Trait.ti_type_params = ib.ib_type_params;
      Trait.ti_methods = List.filter_map (fun item ->
        match item with
        | Ast.ImplFn fd -> Some (fd.Ast.fd_name.name, fd)
        | Ast.ImplType _ -> None
      ) ib.ib_items;
      Trait.ti_assoc_types = [];
      Trait.ti_where = ib.ib_where;
    } in
    (* Verify method presence (trait satisfaction) — convert trait errors to
       type errors so they surface through the standard pipeline. *)
    let* () = match ib.ib_trait_ref with
      | None -> Ok ()  (* Inherent impl — no trait to satisfy *)
      | Some _ ->
        begin match Trait.check_impl_satisfies_trait ctx.trait_registry synth_impl with
        | Ok () -> Ok ()
        | Error re ->
          Error (NotImplemented (Trait.show_resolution_error re))
        end
    in
    (* Type-check each method body *)
    let result = List.fold_left (fun acc item ->
      let* () = acc in
      match item with
      | Ast.ImplFn fd ->
        (* Type-check the method body using the standard function checker *)
        check_fn_decl ctx fd
      | Ast.ImplType _ ->
        (* Associated type definitions carry no body to check *)
        Ok ()
    ) (Ok ()) ib.ib_items in
    (* Restore the previous Self binding *)
    begin match old_self with
    | Some ty -> Hashtbl.replace ctx.type_env "Self" ty
    | None -> Hashtbl.remove ctx.type_env "Self"
    end;
    result
  | TopConst { tc_name; tc_ty; tc_value; _ } ->
    let expected = lower_type_expr ctx tc_ty in
    let* () = check ctx tc_value expected in
    bind_var ctx tc_name.name expected;
    Ok ()

(** {1 Program-level entry point} *)

(** Type-check an entire program.

    First registers all type and effect declarations (forward pass),
    then checks all function declarations and constants.

    [?import_types] seeds [name_types] with cross-module imports — supplied by
    [Resolve.resolve_program_with_loader] so that [ExprApp (ExprVar f, ...)]
    can resolve [f] to the imported function's scheme even though [f] does
    not appear in [prog.prog_decls]. *)
(* ADR-016 / #234 S2b: build the per-call-site effect side-table.
   Keyed by the shared [Effect_sites] ordinal so the (future) codegen
   consumer agrees with this producer. A call's effect row is the
   callee's *declared* row when the callee is a statically-named
   function (`f(..)`, `m.f(..)`, through `ExprSpan`); otherwise EPure
   (sound: S3's predicate is "row ⊇ Async ⇒ boundary", and an
   over-conservative EPure just defers to the structural fallback —
   exactly today's behaviour). Extern fns parse as [TopFn] with
   [FnExtern]/[fd_eff] (parser.mly), so this covers the stdlib async
   primitives and user `Async` fns uniformly. Pure traversal; built,
   not yet consumed. *)
let populate_call_effects (ctx : context) (prog : Ast.program) : unit =
  let fn_eff : (string, eff) Hashtbl.t = Hashtbl.create 64 in
  List.iter
    (function
      | Ast.TopFn fd ->
        let e =
          match fd.fd_eff with
          | Some ee -> (try lower_effect_expr ctx ee with _ -> EPure)
          | None -> EPure
        in
        Hashtbl.replace fn_eff fd.fd_name.name e
      | _ -> ())
    prog.prog_decls;
  let rec callee_name (e : Ast.expr) : string option =
    match e with
    | Ast.ExprVar id -> Some id.name
    | Ast.ExprField (_, id) -> Some id.name
    | Ast.ExprSpan (e, _) -> callee_name e
    | _ -> None
  in
  (* The local `fd_eff` map only covers callees declared in *this*
     unit's `prog_decls`. On WasmGC, imported async primitives
     (`http_request_thenable`, …) and any cross-module callee are NOT
     in `prog_decls` (the backend does not flatten imports) — their
     resolved effect row lives in the callee's scheme in
     `ctx.name_types` (populated by resolve, incl. imports). Fall back
     to that: union the effect components along the arrow spine (the
     declared row is among them; a superset is sound for the
     boundary predicate "row ⊇ Async"). Without this the side-table
     was silently empty for imported async primitives — masked by S3's
     structural disjunct and exposed when S4 retires it. *)
  let rec eff_of_ty (t : ty) : eff =
    match t with
    | TArrow (_, _, b, e) ->
      (match e with
       | EPure -> eff_of_ty b
       | _ -> (match eff_of_ty b with
               | EPure -> e
               | e2 -> EUnion [ e; e2 ]))
    | _ -> EPure
  in
  let scheme_eff (n : string) : eff =
    match Hashtbl.find_opt ctx.name_types n with
    | Some sc -> (try eff_of_ty (instantiate ctx.level sc) with _ -> EPure)
    | None -> EPure
  in
  Effect_sites.iter
    (fun ord call ->
      let row =
        match call with
        | Ast.ExprApp (head, _) ->
          (match callee_name head with
           | Some n ->
             (match Hashtbl.find_opt fn_eff n with
              | Some e when e <> EPure -> e
              | _ -> scheme_eff n)
           | None -> EPure)
        | _ -> EPure
      in
      Hashtbl.replace ctx.call_effects ord row)
    prog;
  (* ADR-016 / #234 S3: publish the ordinal→has-Async view for the
     codegen consumer. `Async` lowers to the canonical `ESingleton
     "Async"` (or appears in an `EUnion`, e.g. `/{Net,Async}`). *)
  let rec eff_has_async (e : eff) : bool =
    match e with
    | EPure | EVar _ -> false
    | ESingleton s -> s = "Async"
    | EUnion es -> List.exists eff_has_async es
  in
  let async_tbl : (int, bool) Hashtbl.t = Hashtbl.create 64 in
  Hashtbl.iter
    (fun ord e -> Hashtbl.replace async_tbl ord (eff_has_async e))
    ctx.call_effects;
  Effect_sites.set_async_by_ord async_tbl

let check_program ?(import_types : (string, scheme) Hashtbl.t option)
    (symbols : Symbol.t) (prog : Ast.program)
    : (context, type_error) Result.t =
  try
  let ctx = create_context symbols in
  register_builtins ctx;
  (* ADR-014 / #228: record `use Mod;` qualifiers so qualified type/effect
     references can be stripped & resolved (or rejected with a clear
     UnknownModule error). Only [ImportSimple] binds a qualifier; List/Glob
     imports bring names unqualified, matching [Resolve.import_qualifiers]
     for value paths. *)
  List.iter (fun imp -> match imp with
    | Ast.ImportSimple (path, alias) ->
      let name = match alias with
        | Some id -> id.name
        | None -> (match List.rev path with id :: _ -> id.name | [] -> "")
      in
      if name <> "" then Hashtbl.replace ctx.module_quals name ()
    | Ast.ImportList _ | Ast.ImportGlob _ -> ()
  ) prog.prog_imports;
  Option.iter (fun tbl ->
    Hashtbl.iter (fun name sc -> Hashtbl.replace ctx.name_types name sc) tbl
  ) import_types;
  (* Forward pass: register all types, effects, traits, impls, and
     function signatures so that mutually recursive declarations resolve. *)
  let* () = List.fold_left (fun acc decl ->
    let* () = acc in
    match decl with
    | TopType td -> register_type_decl ctx td
    | TopEffect ed -> register_effect_decl ctx ed
    | TopFn fd ->
      (* Pre-register function with a fresh type for mutual recursion *)
      let fn_ty = fresh_tyvar ctx.level in
      bind_var ctx fd.fd_name.name fn_ty;
      Ok ()
    | TopTrait td ->
      (* Register trait definition in the trait registry so that
         find_impl / find_method_for_type can locate it. *)
      Trait.register_trait ctx.trait_registry td;
      Ok ()
    | TopImpl ib ->
      (* Lower the self type and register the impl in the trait registry.
         This makes impl methods visible to ExprField trait fallback. *)
      let self_ty = lower_type_expr ctx ib.ib_self_ty in
      Trait.register_impl ctx.trait_registry ib self_ty;
      Ok ()
    | _ -> Ok ()
  ) (Ok ()) prog.prog_decls in
  (* #559: trait coherence — now that every impl is registered, reject
     overlapping impls of the same trait (self types that unify). Done before
     the check pass so an ambiguous instance base is reported up front. *)
  let* () = match Trait.check_all_coherence ctx.trait_registry with
    | Ok () -> Ok ()
    | Error re -> Error (TraitCoherenceError (Trait.show_resolution_error re))
  in
  (* Check pass: verify all declarations *)
  let result = List.fold_left (fun acc decl ->
    let* () = acc in
    check_decl ctx decl
  ) (Ok ()) prog.prog_decls in
  match result with
  | Ok () ->
    (* Quantity checking pass: verify QTT quantity annotations.
       This runs after type checking succeeds so that we report type
       errors first (they are more fundamental). *)
    begin match Quantity.check_program_quantities prog with
    | Ok () ->
      (* ADR-016 / #234 S2b: build the per-call-site effect side-table
         on the fully-checked program. Built, not yet consumed. *)
      populate_call_effects ctx prog;
      Ok ctx
    | Error (qerr, span) ->
      Error (QuantityError (qerr, span))
    end
  | Error e -> Error e
  with
  | Effect_validation_error name -> Error (UnknownEffect name)
  | Module_resolution_error m -> Error (UnknownModule m)
