flan/lib/check.ml

(** The checker: AST → typed IR.

    Two passes, because top-level names in a package are order-independent
    (plan.org, Modules): the first collects every type, signature and global,
    the second checks bodies against them. Mutually recursive functions need no
    forward declaration, and a struct may be used above where it is declared.

    Checking is *bidirectional*. An expression is checked against an expected
    type when there is one and inferred when there is not, which is what makes
    [None], a bare [0] and a struct literal work without any inference engine:
    the expected type flows in from the function's return type, the parameter
    it is being passed to, or the field it is being stored in.

    The rule from the two misparse bugs applies here too: *anything not yet
    implemented is rejected by name*, never approximated. Milestone 2 is
    calc-me.flan and nothing more (plan.org, Build sequence), so [Vec], [Map],
    [Result]/[try], user unions, closures, [dotimes], [defer], generics and
    cross-package imports are all errors with a message that says which
    milestone they belong to. *)

let fail = Loc.fail

(* [List.map]'s evaluation order is unspecified, and checking allocates frame
   slots as a side effect. Left-to-right is required, not a preference: a later
   let binding sees an earlier one, and slot numbering must be reproducible. *)
let rec map_lr f = function
  | [] -> []
  | x :: rest -> let y = f x in y :: map_lr f rest

let rec map2_lr f xs ys =
  match xs, ys with
  | [], [] -> []
  | x :: xs, y :: ys -> let z = f x y in z :: map2_lr f xs ys
  | _ -> invalid_arg "map2_lr"

(* ── Environments ──────────────────────────────────────────────────── *)

type binding = {
  slot       : int;
  bty        : Types.t;
  assignable : bool;   (* locals are places; parameters are not — spec-memory *)
}

type env = {
  structs : (string, Tast.structure) Hashtbl.t;
  unions  : (string, Tast.union) Hashtbl.t;
  aliases : (string, Ast.texpr) Hashtbl.t;
  consts  : (string, int64) Hashtbl.t;         (* compile-time array lengths *)
  locs    : (string, Loc.t) Hashtbl.t;         (* where each type was declared *)
  (* Enum name -> its members, in declaration order. A keyword at a call site
     resolves against this and nothing else. *)
  enums   : (string, (string * int64) list) Hashtbl.t;
  (* Flan name -> the C symbol it is really called by. A foreign function is an
     ordinary entry in [fns] as well; this only records how to name it. *)
  externs : (string, string) Hashtbl.t;
  fns     : (string, Types.t list * Types.t) Hashtbl.t;
  globals : (string, Types.t * bool) Hashtbl.t;   (* type, is a constant *)
  (* Functions the checker made up: a handler-bind clause is lifted into one,
     because a handler is called from wherever the signal was and cannot be a
     branch in the function that established it. *)
  mutable lifted : Tast.fn list;
}

let new_env () = {
  structs = Hashtbl.create 16;
  unions  = Hashtbl.create 16;
  aliases = Hashtbl.create 16;
  consts  = Hashtbl.create 16;
  locs    = Hashtbl.create 16;
  enums   = Hashtbl.create 8;
  externs = Hashtbl.create 32;
  fns     = Hashtbl.create 32;
  globals = Hashtbl.create 16;
  lifted = [];
}

(* Per-function state. Slots are never reused, so [slots] is also the frame
   size — the interpreter allocates one array of this length per call. *)
type ctx = {
  env           : env;
  ret           : Types.t;
  mutable slots : int;
  (* The type of each slot, newest first. A backend needs it to size the
     frame — nothing else records it, since the IR refers to slots by index. *)
  mutable slot_tys : Types.t list;
  (* The source name of each slot, newest first, parallel to [slot_tys].
     [None] for a slot the checker invented -- see [Tast.fn.snames]. Recorded
     here rather than recovered later because this scope list is the only place
     that ever knows it. *)
  mutable slot_names : string option list;
  mutable scope : (string * binding) list;   (* innermost first *)
  (* Deferred forms, most recently registered first — which is also the order
     they run in. At milestone 4 [defer] is function-scoped (see [check_fn]),
     so this list belongs to the function and not to a block. *)
  mutable defers : Tast.expr list;
  (* Only for the two things a handler clause cannot do. [outer] is the
     establishing function's scope, kept so that a reference to one of its
     locals can be refused for the reason it is really refused for rather than
     as an unknown name. *)
  outer : (string * binding) list;
  mutable in_handler : bool;
  (* True wherever handler or restart frames established by this function are
     on the stack. A [return] from there would leave them pointing into a frame
     that has gone, so it is refused — the same rule as [defer] inside a
     block. *)
  mutable in_frames : string option;
  (* True inside a [defer]'s forms. A defer is the cleanup a transfer runs on
     its way out (§5), so a transfer *starting* there has no answer: this
     function's defers are already half run and the first transfer's target is
     already in hand. Refused where it is written. *)
  mutable in_defer : bool;
  (* Move tracking, spec-memory.md's "(Vec T) and (Map K V) are move-only".
     [dead] is the slots whose value has been moved out, with where it went, so
     that a second use names the first rather than reporting a type error about
     nothing. It is flow-sensitive at an [if]: the two arms are checked from
     the same starting set and the *union* survives the join, so moving in one
     arm only is still a move afterwards — and moving in both arms, which is
     legal, is not two errors.

     [borrow] is set only while checking the *target* of an operation that
     reads a container without consuming it ([at], [len], [as-slice], [push],
     [reserve], [clone]). Without it every one of those would look like a move
     and no program could push twice. *)
  mutable dead : (int * Loc.t) list;
  mutable borrow : bool;
  (* The function being checked, so a clause lifted out of it can be named
     after it. The name has to be stable and has to say whose it is: a
     redefinition module emits the clauses belonging to the bodies it is
     replacing, and nothing else in the program can tell it which those are. *)
  owner : string;
}

(* [?name] is the source name, when there is one. It is optional so that the
   several places that allocate a hidden slot say nothing and get [None] --
   a synthesized slot cannot accidentally acquire a name it was never given. *)
let fresh_slot ?name ctx ty =
  let s = ctx.slots in
  ctx.slots <- s + 1;
  ctx.slot_tys <- ty :: ctx.slot_tys;
  ctx.slot_names <- name :: ctx.slot_names;
  s

(* Shadowing is legal -- [(let [v 11] (let [v 22] ...))] is two slots, both
   named [v] -- and the debug info has nowhere to put the distinction. Every
   [!DILocalVariable] is scoped to the subprogram, because the typed IR has no
   block structure for a [!DILexicalBlock] to be built from, so two variables
   called [v] land in one flat scope and lldb answers [p v] with whichever it
   finds first. Measured, not assumed: it answers with the *outer* one, so it
   prints 11 while the body it is stopped in is computing with 22, and the
   inner binding is not listed at all.

   That is the one outcome worse than printing [s3]: a name the debugger is
   confident about and wrong about. So a repeat of a name already bound in this
   function gets a suffix, and both bindings are then visible and unambiguous.
   [~] is the reader's delimiter and cannot occur in a source symbol (the same
   reason [destructure~nth] is spelled that way), so [v~2] is visibly the
   compiler's doing and can never collide with something the programmer wrote.

   This is a way of not lying, not a way of being right: [v] is still the outer
   binding everywhere, including inside the inner one's extent. Scoping the
   variables properly means emitting a [!DILexicalBlock] per [Let] and moving
   the [llvm.dbg.declare]s out of the entry block to the binding sites, which
   needs block structure this IR does not carry. *)
let bind ctx name bty ~assignable =
  let taken n = List.exists (fun s -> s = Some n) ctx.slot_names in
  let name' =
    if not (taken name) then name
    else
      let rec go k =
        let c = Printf.sprintf "%s~%d" name k in
        if taken c then go (k + 1) else c
      in
      go 2
  in
  let slot = fresh_slot ~name:name' ctx bty in
  (* [ctx.scope] keeps the *source* name: the suffix is a debug-info artifact
     and resolving [v] must still find the innermost binding. *)
  ctx.scope <- (name, { slot; bty; assignable }) :: ctx.scope;
  slot

let lookup ctx name = List.assoc_opt name ctx.scope

(* A handler clause is lifted into a function of its own, so the establishing
   function's locals are simply not there. Capturing them is a closure with an
   explicit environment — spec-memory.md's case 2, a non-escaping [fn] capturing
   by value into a stack environment, since a handler frame does not outlive the
   function that pushed it — and until that exists a reference to one is refused
   for the reason it is really refused for, rather than as a name nobody has
   heard of. *)
let captured ctx loc name =
  if ctx.in_handler && List.mem_assoc name ctx.outer then
    raise
      (Loc.Error
         (loc,
          Printf.sprintf
            "a handler cannot see %s: it is a local of the function that \
             established the handler, and a handler runs from wherever the \
             signal was. Use a global, or pass it on the condition." name))

let scoped ctx f =
  let saved = ctx.scope in
  let r = f () in
  ctx.scope <- saved;
  r

(* ── Type resolution ───────────────────────────────────────────────── *)

let unimplemented loc what milestone =
  fail loc "%s is not implemented yet — milestone %d (see plan.org)"
    what milestone

let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
  let loc = t.Ast.tloc in
  match t.Ast.t with
  | Ast.Tname n -> resolve_name env ~seen loc n
  | Ast.Tslice e -> Types.Slice (resolve env ~seen e)
  | Ast.Tarray (l, e) -> Types.Array (array_len env loc l, resolve env ~seen e)
  | Ast.Tmap _ -> unimplemented loc "the Map type" 6
  (* The function *value* is refused where it is written; the annotation was
     not refused anywhere, so [(defn f [g (Fn [] i32)])] type checked and then
     died in emit with "no layout for". Refused here, beside the Map line
     above, which is the same shape of not-yet. *)
  | Ast.Tfn _ -> unimplemented loc "a function type" 5
  | Ast.Tapp (name, args) ->
    (match name, args with
     | "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a)
     | "Option", [ a ] -> Types.Option (resolve env ~seen a)
     | ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
     | "Vec", [ a ] ->
       let e = resolve env ~seen a in
       (* A Vec of a Vec is representable and would be wrong. spec-memory.md
          makes [clone] a deep copy and makes [free] recurse structurally into
          owning fields; the type-erased runtime does neither — it memcpys, so
          a clone would duplicate inner headers and a free would drop their
          buffers on the floor. Recursive teardown is what step 5's [drop]
          brings, and this is refused until it does rather than shipping the
          shallow answer under the deep name. *)
       if Types.is_move_only e then
         fail loc
           "(Vec %s) holds a move-only element, and the type-erased runtime \
            copies and releases elements bytewise — so clone would duplicate \
            headers instead of copying, and free would leak what they own. \
            Recursive teardown arrives with drop (step 5 in NEXT.md)"
           (Types.to_string e);
       Types.Vec e
     | "Vec", _ -> fail loc "(Vec T) takes exactly one type"
     | "Map", _ -> unimplemented loc "(Map K V)" 6
     | "Result", _ -> unimplemented loc "(Result T E)" 6
     | "Handle", _ -> unimplemented loc "(Handle T)" 6
     | _ ->
       fail loc
         "%s takes no type arguments — generics are milestone 5" name)

(* One edit away from a type that exists — a substitution, an insertion, a
   deletion or a transposition of neighbours. Bounded at one, because two edits
   is no longer a typo, it is a guess. *)
and near_miss env n =
  let one_edit a b =
    let la = String.length a and lb = String.length b in
    if abs (la - lb) > 1 then false
    else begin
      (* Walk both until they diverge, then require the tails to match with the
         single edit applied. *)
      let i = ref 0 in
      while !i < la && !i < lb && a.[!i] = b.[!i] do incr i done;
      let ta s k = String.sub s k (String.length s - k) in
      if la = lb then
        !i < la
        && (ta a (!i + 1) = ta b (!i + 1)
            (* stirng/string: two neighbours swapped. *)
            || (!i + 1 < la && a.[!i] = b.[!i + 1] && a.[!i + 1] = b.[!i]
                && ta a (!i + 2) = ta b (!i + 2)))
      else if la < lb then ta a !i = ta b (!i + 1)
      else ta a (!i + 1) = ta b !i
    end
  in
  let candidates =
    Types.primitive_names
    @ Hashtbl.fold (fun k _ acc -> k :: acc) env.aliases []
    @ Hashtbl.fold (fun k _ acc -> k :: acc) env.structs []
    @ Hashtbl.fold (fun k _ acc -> k :: acc) env.unions []
    @ Hashtbl.fold (fun k _ acc -> k :: acc) env.enums []
  in
  List.find_opt (fun c -> c <> n && one_edit n c) candidates

and resolve_name env ~seen loc n =
  match Types.ikind_of_name n with
  | Some k -> Types.Int k
  | None ->
    match Types.fkind_of_name n with
    | Some k -> Types.Float k
    | None ->
      match n with
      | "bool" -> Types.Bool
      | "string" -> Types.String
      | "Unit" -> Types.Unit
      | "Never" -> Types.Never
      (* A builtin opaque type, the way [string] is a builtin ptr+len. There is
         no user-writable constructor and no way to name its procedure: see
         Types, and NEXT.md's "the escape is real". *)
      | "Allocator" -> Types.Alloc
      | _ when Hashtbl.mem env.aliases n ->
        if List.mem n seen then
          fail loc "the type alias %s is defined in terms of itself" n
        else resolve env ~seen:(n :: seen) (Hashtbl.find env.aliases n)
      | _ when Hashtbl.mem env.structs n -> Types.Named n
      (* A union has no layout in emit — nothing there mentions unions at all —
         so a union-typed global reached clang as a reference to an undefined
         %"U". Constructing one and reading a field of one are already refused,
         so there is nothing to lower: only a declaration that got through. *)
      | _ when Hashtbl.mem env.unions n ->
        unimplemented loc (Printf.sprintf "the union type %s" n) 6
      | _ when Hashtbl.mem env.enums n -> Types.Enum n
      (* A typo in a primitive is lowercase too, and the type-variable rule
         below would otherwise report [f65] as unimplemented generics and send
         you to plan.org instead of to the character you mistyped. *)
      | _ when near_miss env n <> None ->
        fail loc "unknown type %s — did you mean %s?" n
          (Option.get (near_miss env n))
      (* Lowercase is a type variable, Capitalized is concrete — no sigil
         (plan.org, Types). A variable parses, but nothing at milestone 2 can
         give a value one, so it is rejected here rather than later. *)
      | _ when n <> "" && n.[0] = Char.lowercase_ascii n.[0] ->
        unimplemented loc
          (Printf.sprintf "generic code over the type variable %s" n) 5
      | _ -> fail loc "unknown type %s" n

and array_len env loc = function
  | Ast.Lint n -> n
  | Ast.Lname n ->
    (match Hashtbl.find_opt env.consts n with
     | Some v -> v
     | None ->
       fail loc "%s is not a compile-time integer constant, so it cannot be \
                 an array length" n)

(* ── Small helpers over the AST ────────────────────────────────────── *)

(* Untyped literals: their machine type comes from context, so when one is an
   operand of a binary operator we look at the *other* operand first. *)
let is_literal (e : Ast.expr) =
  match e.Ast.e with Ast.Int _ | Ast.Float _ | Ast.Byte _ -> true | _ -> false

(* [addr] takes the address of a place, but the parser only builds places for
   [set]. Recover one from the expression it parsed instead. *)
let place_of_expr (e : Ast.expr) : Ast.place option =
  match e.Ast.e with
  | Ast.Var s -> Some (Ast.Pvar s)
  | Ast.Field (t, f) -> Some (Ast.Pfield (t, f))
  | Ast.Call ({ Ast.e = Ast.Var "at"; _ }, t :: idx) when idx <> [] ->
    Some (Ast.Pindex (t, idx))
  | Ast.Call ({ Ast.e = Ast.Var "deref"; _ }, [ p ]) -> Some (Ast.Pderef p)
  | _ -> None

let mk loc ty e : Tast.expr = { Tast.e; ty; loc }

let unit_at loc = mk loc Types.Unit Tast.Unit

(* A source location as a value, for a runtime trap that has to name the site
   rather than the runtime. The bounds and slice traps get theirs from [Emit],
   which renders the [Loc.t] it is already carrying; a trap reached through a
   plain runtime call has no such carrier, so the string is built here and
   crosses as ptr+len like any other. *)
let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))

(* A runtime call, with the result type spelled at the site. *)
let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))

let i64_at loc n = mk loc (Types.Int Types.I64) (Tast.Int (n, Types.I64))

(* spec-memory.md, "Alignment": the number is produced where the concrete
   element type is known, which without generics is simply the call site. *)
let size_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.SizeOf t, []))
let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, []))

(* The address of an expression, place or not: the type-erased runtime takes
   the element [push] copies by pointer. *)
let addr_of loc (e : Tast.expr) =
  mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))

(* Every integer index into an array or slice is i32 at milestone 2. *)
let index_ty = Types.Int Types.I32

(* A condition's type at run time is a number, and it has to be the *same*
   number in a module compiled later against a program already running. So it
   is a hash of the name and not an index into anything: an index would shift
   the moment a struct were added, and every handler pushed by the old code
   would then match the wrong type. FNV-1a over the name, 32 bits. *)
let type_id name =
  let h = ref 0x811c9dc5 in
  String.iter
    (fun c ->
       h := (!h lxor Char.code c) land 0xffffffff;
       h := (!h * 0x01000193) land 0xffffffff)
    name;
  !h

(* How a restart's parameter list is spelled, and with it what the two ends of
   an [invoke-restart] compare — spec-conditions.md §3's run-time check. A
   restart is found by name on a dynamic stack, so neither end can see the
   other and nothing static can be checked: what is compared at run time is
   this string's hash, alongside the count, and the string itself is carried so
   that a mismatch can say what was wanted and what was given.

   Comparing a 32-bit hash means two different parameter lists could in
   principle collide. The count is checked separately, which rules out every
   practical case (a collision would have to be between two lists of the same
   length), and the types are parenthesised so that [(Option i32)] cannot read
   as two parameters. *)
let restart_sig tys =
  "(" ^ String.concat " " (List.map Types.to_string tys) ^ ")"

let expect loc ~want (got : Tast.expr) =
  match want with
  | None -> got
  | Some w ->
    if Types.fits ~expected:w ~actual:got.Tast.ty then got
    else
      fail loc "expected %s, found %s" (Types.to_string w)
        (Types.to_string got.Tast.ty)

(* ── Expressions ───────────────────────────────────────────────────── *)

let rec check ctx ?want (e : Ast.expr) : Tast.expr =
  let loc = e.Ast.loc in
  match e.Ast.e with
  | Ast.Int n -> int_literal loc ~want n
  | Ast.Byte b -> int_literal loc ~want ~default:Types.U8 (Int64.of_int b)
  | Ast.Float x ->
    let k =
      match want with
      | Some (Types.Float k) -> k
      | Some other when other <> Types.Never ->
        fail loc "expected %s, found the float literal %g"
          (Types.to_string other) x
      | _ -> Types.F64
    in
    mk loc (Types.Float k) (Tast.Float (x, k))
  | Ast.Str s -> expect loc ~want (mk loc Types.String (Tast.Str s))
  | Ast.Kw k ->
    (* A keyword resolves at compile time against the enum the site expects,
       and a typo is an error here rather than a wrong number at run time
       (plan.org, settled: keywords at typed call sites). It has no meaning
       without that expectation — there is no keyword type to fall back on. *)
    (match want with
     | Some (Types.Enum name) ->
       let members = Hashtbl.find ctx.env.enums name in
       (match List.assoc_opt k members with
        | Some v -> mk loc (Types.Enum name) (Tast.Int (v, Types.I32))
        | None ->
          fail loc "%s has no member :%s — it has %s" name k
            (String.concat " "
               (List.map (fun (m, _) -> ":" ^ m) members)))
     | Some other ->
       fail loc ":%s is an enum member, but %s is expected here" k
         (Types.to_string other)
     | None ->
       fail loc
         ":%s only means something where an enum type is expected — there is \
          no keyword type" k)
  | Ast.Quote _ ->
    unimplemented loc "a quoted symbol (restart names)" 6
  | Ast.Var name -> var ctx loc ~want name
  | Ast.Do body -> block ctx ?want loc body
  | Ast.Let (bs, body) -> check_let ctx ?want loc bs body
  | Ast.If (c, t, e') -> check_if ctx ?want loc c t e'
  | Ast.While (c, body) ->
    let c = check ctx ~want:Types.Bool c in
    let body = in_loop ctx (fun () ->
      scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
    in
    expect loc ~want (mk loc Types.Unit (Tast.While (c, body)))
  | Ast.Return v when ctx.in_frames <> None ->
    ignore v;
    (* The frames are pushed and popped around the body, so an early exit would
       leave them on the handler or restart stack pointing into a frame that
       has gone. Rejected rather than left to corrupt it, the same rule as
       defer inside a block. *)
    fail loc
      "return is not allowed inside %s yet — the frames it established are \
       popped on the way out and an early exit would leave them on the stack"
      (match ctx.in_frames with Some n -> n | None -> assert false)

  | Ast.Return v ->
    let v =
      match v with
      | None ->
        if not (Types.equal ctx.ret Types.Unit) then
          fail loc "this function returns %s, so return needs a value"
            (Types.to_string ctx.ret);
        None
      | Some v -> Some (check ctx ~want:ctx.ret v)
    in
    (* Whatever has been deferred *so far* runs first: a defer written below
       this return has not executed yet and must not fire. *)
    let r = mk loc Types.Never (Tast.Return v) in
    (match ctx.defers with
     | [] -> r
     | ds -> mk loc Types.Never (Tast.Do (ds @ [ r ])))
  | Ast.Set (p, v) ->
    let p, pty = check_place ctx loc p in
    let v = check ctx ~want:pty v in
    expect loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
  | Ast.Field (target, name) ->
    let target, sname = struct_target ctx target in
    let s = Hashtbl.find ctx.env.structs sname in
    (match Tast.field_index s name with
     | None -> fail loc "%s has no field %s" sname name
     | Some i ->
       let fty = (List.nth s.Tast.fields i).Tast.fty in
       expect loc ~want (mk loc fty (Tast.Field (target, i))))
  | Ast.Struct (name, kvs) -> check_struct ctx ~want loc name kvs
  | Ast.Arr items -> check_arr ctx ~want loc items
  | Ast.Match (scrutinee, arms) -> check_match ctx ?want loc scrutinee arms
  | Ast.Call (head, args) -> check_call ctx ~want loc head args
  | Ast.Unwrap (Ast.Usome, v) ->
    (* Unwrap Some, else early-return None from the enclosing function, so the
       enclosing function must itself return an Option (plan.org). *)
    (match ctx.ret with
     | Types.Option _ ->
       let v = check ctx v in
       (match v.Tast.ty with
        | Types.Option t ->
          expect loc ~want (mk loc t (Tast.UnwrapSome v))
        | other ->
          fail loc "some takes an (Option T), found %s" (Types.to_string other))
     | other ->
       fail loc
         "some early-returns None, so the enclosing function must return an \
          Option; this one returns %s" (Types.to_string other))
  | Ast.Unwrap (Ast.Utry, _) -> unimplemented loc "try (Result)" 6
  | Ast.Fn _ -> unimplemented loc "fn values" 5
  | Ast.Dotimes (name, count, body) -> check_dotimes ctx ~want loc name count body
  (* (signal c) : Unit, always — spec-conditions.md §1. A handler that returns
     normally leaves the signalling function to carry on, and with nothing
     matching this is a no-op, so nothing about it alters control flow. That is
     what makes it checkable here rather than needing the transfer machinery
     restart-case will want. *)
  | Ast.Signal (kind, c) ->
    let c = check ctx c in
    let name =
      match c.Tast.ty with
      | Types.Named n -> n
      | t ->
        fail c.Tast.loc
          "a condition is a struct, not %s — matching is by type and there is \
           no condition hierarchy"
          (Types.to_string t)
    in
    (* §1 and §2. [signal] is Unit whatever it finds; [error] is Never,
       because the only way past it is a handler that transfers — one that
       returns normally has not answered it, and the program stops. *)
    let ty, kind =
      match kind with
      | Ast.Ssignal -> (Types.Unit, Tast.Ssignal)
      | Ast.Serror -> (Types.Never, Tast.Serror)
    in
    expect loc ~want (mk loc ty (Tast.Signal (kind, type_id name, c)))

  | Ast.HandlerBind (clauses, body) -> check_handler_bind ctx ?want loc clauses body

  (* spec-conditions.md §3–§6: the transfer. Neither of these is a call — one
     establishes frames around a body, and the other leaves the function it is
     written in — so both are their own nodes all the way down. *)
  | Ast.RestartCase (body, clauses) -> check_restart_case ctx ?want loc body clauses
  | Ast.InvokeRestart (name, args) ->
    (* Never: control resumes at the restart-case, which yields the clause's
       value to *its* continuation, so nothing here has a value and nothing
       after it runs. The lookup is at run time because restarts are
       dynamically scoped and named — §4 — and so, for the same reason, is the
       check that these arguments are the ones the clause takes (§3). *)
    if ctx.in_defer then
      fail loc
        "invoke-restart is not allowed inside a defer — a defer is the cleanup \
         a transfer runs on its way out, so starting one there would leave \
         this function's defers half run with two targets and no way to \
         choose";
    let args = map_lr (fun a -> check ctx a) args in
    List.iter
      (fun (a : Tast.expr) ->
         match a.Tast.ty with
         | Types.Unit | Types.Never ->
           fail a.Tast.loc
             "a restart argument must be a value, and this one is %s"
             (Types.to_string a.Tast.ty)
         | _ -> ())
      args;
    let sg = restart_sig (List.map (fun (a : Tast.expr) -> a.Tast.ty) args) in
    (* Evaluated into slots first, so that an argument which transfers on its
       own is guarded before this form aims the channel, and so that a call
       written in an argument is on the ordinary walk rather than hidden
       inside a node that [Reach] and [Load] treat as a leaf. *)
    let binds =
      List.map (fun (a : Tast.expr) -> (fresh_slot ctx a.Tast.ty, a)) args
    in
    let locals =
      List.map
        (fun (s, (a : Tast.expr)) -> mk a.Tast.loc a.Tast.ty (Tast.Local s))
        binds
    in
    let invoke =
      mk loc Types.Never
        (Tast.InvokeRestart (type_id name, name, locals, sg, type_id sg, loc))
    in
    expect loc ~want
      (if binds = [] then invoke
       else mk loc Types.Never (Tast.Let (binds, [ invoke ])))

  | Ast.Defer _ ->
    (* Registered by [check_fn], which is the only place that sees a form's
       position. A defer anywhere else would run at function exit rather than
       at the exit of the block it is written in — once for a loop body that
       runs a thousand times — so it is rejected instead of quietly differing. *)
    fail loc
      "defer must be a top-level form in a function body — block-scoped defer \
       is not implemented yet (milestone 4)"

and int_literal loc ~want ?(default = Types.I32) n =
  match want with
  | Some (Types.Int k) -> mk loc (Types.Int k) (Tast.Int (in_range loc k n, k))
  (* An untyped integer constant is usable where a float is wanted, as in
     Odin. A float literal is never usable where an integer is wanted. *)
  | Some (Types.Float k) ->
    mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k))
  | Some other when other <> Types.Never ->
    fail loc "expected %s, found the integer literal %Ld"
      (Types.to_string other) n
  | _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))

(* Arithmetic wraps, but a literal that does not fit its type is a typo, not a
   wrap — 300 is never what someone meant by a u8. *)
and in_range loc k n =
  let bits = Types.bits k in
  let ok =
    if Types.signed k then
      bits = 64
      || (Int64.compare n (Int64.neg (Int64.shift_left 1L (bits - 1))) >= 0
          && Int64.compare n (Int64.shift_left 1L (bits - 1)) < 0)
    else if bits = 64 then
      (* A u64 literal is its 64-bit pattern, so anything at or above 2^63
         arrives here as a negative [int64] and is still in range —
         0xcbf29ce484222325 is a real u64 and not an error. The cost is that a
         negative *decimal* literal is accepted as a u64 too, because the
         reader records only the value and not how it was written. Narrower
         unsigned types keep the strict check, which is where a typo like 300
         for a u8 actually shows up. *)
      true
    else
      Int64.compare n 0L >= 0
      && Int64.compare n (Int64.shift_left 1L bits) < 0
  in
  if ok then n
  else fail loc "%Ld does not fit in %s" n (Types.ikind_name k)

and var ctx loc ~want name =
  match name with
  | "true" | "false" ->
    expect loc ~want (mk loc Types.Bool (Tast.Bool (name = "true")))
  | "None" ->
    (match want with
     | Some (Types.Option t) -> mk loc (Types.Option t) Tast.None_
     | Some other when other <> Types.Never ->
       fail loc "expected %s, found None" (Types.to_string other)
     | _ ->
       fail loc
         "nothing here says what None is an Option of — annotate the \
          function's return type or the binding")
  (* spec-memory.md puts the allocator in the calling convention as
     [context/allocator] and [context/temp]. They read as names rather than
     calls because that is how the spec writes them, and they are dynamic
     variables at run time rather than extra parameters — see BUILT.md for why
     the literal reading of "calling convention" is deferred. *)
  | "context/allocator" ->
    expect loc ~want
      (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_context_allocator", [])))
  | "context/temp" ->
    expect loc ~want
      (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_context_temp", [])))
  | _ ->
    match lookup ctx name with
    | Some b ->
      if Types.is_move_only b.bty then moved ctx loc name b.slot;
      expect loc ~want (mk loc b.bty (Tast.Local b.slot))
    | None ->
      match Hashtbl.find_opt ctx.env.globals name with
      | Some (ty, _) -> expect loc ~want (mk loc ty (Tast.Global name))
      | None ->
        if Hashtbl.mem ctx.env.fns name then
          unimplemented loc
            (Printf.sprintf "the function value %s (a name used as a value)" name) 5
        else begin captured ctx loc name; fail loc "unknown name %s" name end

(* Reading a move-only local. Every read is a move unless the site said it was
   a borrow, which is the conservative direction: passing one to a function,
   binding it, returning it and [free]ing it are all moves and all reach here,
   and the handful of operations that only look at a container say so. *)
and moved ctx loc name slot =
  (match List.assoc_opt slot ctx.dead with
   | Some where ->
     fail loc
       "%s was moved at %s and cannot be used again — a Vec is move-only, so \
        binding, passing or returning one transfers ownership and the source \
        binding is dead afterwards (spec-memory.md). That rule is what makes a \
        double free unrepresentable; (clone %s) if you wanted a second one"
       name (Loc.to_string where) name
   | None -> ());
  if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead

(* The target of an operation that reads a container without consuming it. Only
   a syntactically simple target is treated as a borrow: in [(len (f v))] the
   call still moves [v], and setting the flag over the whole subexpression
   would have hidden that. *)
and borrowed ctx (a : Ast.expr) f =
  let simple =
    match a.Ast.e with
    | Ast.Var _ | Ast.Field _ -> true
    | Ast.Call ({ Ast.e = Ast.Var "at"; _ }, _) -> true
    | _ -> false
  in
  if not simple then f ()
  else begin
    let saved = ctx.borrow in
    ctx.borrow <- true;
    let r = f () in
    ctx.borrow <- saved;
    r
  end

and block ctx ?want loc body =
  match body with
  | [] -> expect loc ~want (unit_at loc)
  | _ ->
    let rec go = function
      | [ last ] -> let l = check ctx ?want last in [ l ], l.Tast.ty
      | x :: rest -> let x = check ctx x in
        let rest, ty = go rest in x :: rest, ty
      | [] -> assert false
    in
    let body, ty = go body in
    mk loc ty (Tast.Do body)

(* A handler runs where the *signal* was, not where it was established, so it
   cannot be a branch in the function that wrote it: it is lifted into a
   function of its own and reached through a pointer.

   Which means it cannot see the establishing function's locals. Capturing them
   is a closure with an explicit environment — the non-escaping kind, captured
   by value onto this frame — and until that exists a reference to one is
   rejected by name rather than silently resolving to something else. Globals and the condition itself are
   in scope, which is enough for the accumulation case §1 is about.

   The body may not [return] either. The frames are pushed and popped around
   it, and an early exit would leave them on the stack pointing into a function
   that has gone. *)
and check_handler_bind ctx ?want loc clauses body =
  ignore want;
  let frames =
    List.map
      (fun (c : Ast.hclause) ->
         let ty = resolve ctx.env c.Ast.hty in
         let name =
           match ty with
           | Types.Named n -> n
           | t ->
             fail c.Ast.hloc
               "a handler matches a struct type, not %s" (Types.to_string t)
         in
         (* Its own context: a fresh frame, an empty scope, and no way to reach
            the enclosing one. *)
         let hctx =
           { env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = [];
             scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" }
         in
         (* The condition crosses as a pointer, because the handler runs while
            the signalling frame is still alive and there is nothing to copy.
            What the clause binds is the condition itself, though, so the
            pointer is a hidden parameter and the name is a slot loaded from
            it — a handler that passed [c] to something expecting the struct
            would otherwise be handed an address. *)
         let pslot = fresh_slot hctx (Types.Ptr ty) in
         let cslot = bind hctx c.Ast.hname ty ~assignable:false in
         let hbody = map_lr (fun e -> check hctx e) c.Ast.hbody in
         let hbody =
           [ mk c.Ast.hloc Types.Unit
               (Tast.Let
                  ([ (cslot,
                      mk c.Ast.hloc ty
                        (Tast.Deref
                           (mk c.Ast.hloc (Types.Ptr ty) (Tast.Local pslot)))) ],
                   hbody)) ]
         in
         (* Named after the function it came out of, and numbered within it:
            stable against an unrelated handler-bind being added elsewhere,
            which an index into the whole program's lifted list would not be. *)
         let fname =
           Printf.sprintf "handler/%s/%d/%s" ctx.owner
             (List.length
                (List.filter
                   (fun (l : Tast.fn) -> l.Tast.fparent = Some ctx.owner)
                   ctx.env.lifted))
             name
         in
         ctx.env.lifted <-
           { Tast.name = fname; params = [ Types.Ptr ty ];
             slots = Array.of_list (List.rev hctx.slot_tys);
             snames = Array.of_list (List.rev hctx.slot_names);
             ret = Types.Unit; body = hbody; fdefers = [];
             fparent = Some ctx.owner; floc = c.Ast.hloc }
           :: ctx.env.lifted;
         { Tast.htype = type_id name; hfn = fname })
      clauses
  in
  (* The flag is set on [ctx] itself and restored, not on a copy: [ctx.slots]
     and [ctx.slot_tys] are mutable, so a copy would allocate the body's slots
     into a record the function never sees again and the indices would
     collide. *)
  let saved = ctx.in_frames in
  ctx.in_frames <- Some "handler-bind";
  let body = map_lr (fun e -> check ctx e) body in
  ctx.in_frames <- saved;
  mk loc Types.Unit (Tast.Handled (frames, body))

(* (restart-case BODY (name [] BODY-1) ...) — spec-conditions.md §3 and §6.

   Unlike a handler, a clause runs *at* the restart-case, which is where it was
   written, so it is a branch in this function and sees this function's scope.
   What arrives from elsewhere is only the answer to "which clause": a transfer
   names the frame it is aimed at, and this form compares that against the
   frames it itself pushed.

   Every clause body and the body have the same type, and that is the type of
   the whole form — which is what makes the fall-through path visible in the
   source (§1): a restart-case in value position has to produce its type when
   no restart is invoked too. *)
and check_restart_case ctx ?want loc body clauses =
  let saved = ctx.in_frames in
  ctx.in_frames <- Some "restart-case";
  let tbody = check ctx ?want body in
  ctx.in_frames <- saved;
  (* With no expectation from outside, the body's own type is the expectation
     the clauses are checked against — unless it produced no value at all, in
     which case the first clause that does decides. *)
  let want =
    match want with
    | Some _ -> want
    | None -> if tbody.Tast.ty = Types.Never then None else Some tbody.Tast.ty
  in
  let ty = ref (match want with Some t -> Some t | None -> None) in
  let seen = ref [] in
  let clauses =
    map_lr
      (fun (c : Ast.rclause) ->
         (* Two clauses of one name would make §4's "the first frame offering
            the name" pick between them by an order nothing in the source
            shows. *)
         if List.mem c.Ast.rname !seen then
           fail c.Ast.rloc "this restart-case offers %s twice" c.Ast.rname;
         seen := c.Ast.rname :: !seen;
         (* §3's parameters. They are slots in *this* function — a clause runs
            here, not where the invoke was — and the invoker stores into a
            buffer this frame owns, because its own frame is gone by the time
            the clause body starts (§5). Bound like a function's parameters:
            visible only in the clause, and not assignable. *)
         let params, b =
           scoped ctx (fun () ->
             let params =
               List.map
                 (fun (p : Ast.field) ->
                    let ty = resolve ctx.env p.Ast.fty in
                    (match ty with
                     | Types.Unit | Types.Never ->
                       fail p.Ast.floc
                         "%s would be a restart parameter of type %s, which is \
                          not a value" p.Ast.fname (Types.to_string ty)
                     | _ -> ());
                    (bind ctx p.Ast.fname ty ~assignable:false, ty))
                 c.Ast.rparams
             in
             (* Each is checked against what the form has settled on so far, so
                a clause that disagrees fails where it is written. The first one
                to produce a value is what settles it when nothing outside
                did. *)
             (params, block ctx ?want:!ty c.Ast.rloc c.Ast.rbody))
         in
         if !ty = None && b.Tast.ty <> Types.Never then ty := Some b.Tast.ty;
         let sg = restart_sig (List.map snd params) in
         { Tast.rname_id = type_id c.Ast.rname; rname = c.Ast.rname;
           rparams = params; rsig = sg; rsig_id = type_id sg; rbody = [ b ] })
      clauses
  in
  let ty = match !ty with Some t -> t | None -> Types.Never in
  mk loc ty (Tast.RestartCase (clauses, tbody))

and check_let ctx ?want loc bs body =
  scoped ctx (fun () ->
    let bs =
      map_lr
        (fun (b : Ast.binding) ->
           let want = Option.map (resolve ctx.env) b.Ast.bty in
           let v = check ctx ?want b.Ast.bval in
           (match v.Tast.ty with
            | Types.Unit | Types.Never ->
              fail b.Ast.bloc "%s would be bound to %s, which is not a value"
                b.Ast.bname (Types.to_string v.Tast.ty)
            | _ -> ());
           (* Locals are assignable places; parameters are not. *)
           let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
           (slot, v))
        bs
    in
    let body = block ctx ?want loc body in
    mk loc body.Tast.ty (Tast.Let (bs, [ body ])))

(* (dotimes [i n] body...) is a counting loop, not a new IR node: bind [i] to 0
   and the bound to a hidden slot — [n] is evaluated once, before the loop, so
   a body that changes it cannot change the trip count — then step [i] at the
   end of the body. [i] is not assignable, so the step below is the only writer. *)
(* A loop body that moves a binding declared outside the loop is refused, and
   this is the one place the dead set cannot answer on its own: the second
   iteration would use what the first moved, and a set that is merged once at
   the end of the body sees one move, not two. So it is a rule rather than an
   inference, stated as one. *)
and in_loop ctx f =
  let outer_slots = List.map (fun (_, b) -> b.slot) ctx.scope in
  let before = ctx.dead in
  let r = f () in
  List.iter
    (fun (slot, where) ->
       if (not (List.mem_assoc slot before)) && List.mem slot outer_slots then
         fail where
           "this moves a value that was bound outside the loop, so the next \
            iteration would use what this one gave away. Move it out of the \
            loop, or bind a fresh value inside it")
    ctx.dead;
  r

and check_dotimes ctx ~want loc name count body =
  let count = check ctx ~want:index_ty count in
  scoped ctx (fun () ->
    let i = bind ctx name index_ty ~assignable:false in
    let limit = fresh_slot ctx index_ty in
    let body = in_loop ctx (fun () -> map_lr (fun b -> check ctx b) body) in
    let iv = mk loc index_ty (Tast.Local i) in
    let one = mk loc index_ty (Tast.Int (1L, Types.I32)) in
    let cond =
      mk loc Types.Bool
        (Tast.Prim (Tast.Lt, [ iv; mk loc index_ty (Tast.Local limit) ]))
    in
    let step =
      mk loc Types.Unit
        (Tast.Set (Tast.Plocal i,
                   mk loc index_ty (Tast.Prim (Tast.Add, [ iv; one ]))))
    in
    let zero = mk loc index_ty (Tast.Int (0L, Types.I32)) in
    let loop = mk loc Types.Unit (Tast.While (cond, body @ [ step ])) in
    expect loc ~want
      (mk loc Types.Unit (Tast.Let ([ (i, zero); (limit, count) ], [ loop ]))))

and check_if ctx ?want loc c t e =
  let c = check ctx ~want:Types.Bool c in
  match e with
  | None ->
    (* A one-armed if produces Unit whatever the branch evaluates to: there is
       no value on the missing side. `when` desugars to this. *)
    let t = scoped ctx (fun () -> check ctx t) in
    expect loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
  | Some e ->
    (* Both arms start from the same dead set and the union survives: moving in
       one arm only still kills the binding afterwards, and moving in both —
       which is legal and common — is not reported twice. A flat set would have
       refused [(if c (free v) (free v))] and allowed the use after a one-armed
       move, which are the two ways to be wrong here. *)
    let before = ctx.dead in
    let t = scoped ctx (fun () -> check ctx ?want t) in
    let after_then = ctx.dead in
    ctx.dead <- before;
    (* With no expectation the then-branch supplies one for the else-branch,
       unless it diverges, in which case the else-branch decides. *)
    let ewant =
      match want with
      | Some _ -> want
      | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
    in
    let e = scoped ctx (fun () -> check ctx ?want:ewant e) in
    ctx.dead <-
      after_then
      @ List.filter (fun (k, _) -> not (List.mem_assoc k after_then)) ctx.dead;
    let ty =
      if t.Tast.ty = Types.Never then e.Tast.ty
      else if e.Tast.ty = Types.Never then t.Tast.ty
      else if Types.equal t.Tast.ty e.Tast.ty then t.Tast.ty
      else
        fail loc "the branches of this if have different types: %s and %s"
          (Types.to_string t.Tast.ty) (Types.to_string e.Tast.ty)
    in
    mk loc ty (Tast.If (c, t, e))

and check_struct ctx ~want loc name kvs =
  match Hashtbl.find_opt ctx.env.structs name with
  | None ->
    if Hashtbl.mem ctx.env.unions name then
      unimplemented loc "constructing a union value" 6
    else fail loc "unknown struct %s" name
  | Some s ->
    let seen = Hashtbl.create 8 in
    List.iter
      (fun (k, (v : Ast.expr)) ->
         if Hashtbl.mem seen k then
           fail v.Ast.loc "field %s is given twice" k;
         if Tast.field_index s k = None then
           fail v.Ast.loc "%s has no field %s" name k;
         Hashtbl.add seen k v)
      kvs;
    (* Omitted fields are zeroed — ZII, the same rule as a declaration with no
       initialiser (plan.org, Data model). Every field is present from here on,
       in declaration order, so no backend has to know about omission. *)
    let fields =
      map_lr
        (fun (f : Tast.field) ->
           match Hashtbl.find_opt seen f.Tast.fname with
           | Some v -> check ctx ~want:f.Tast.fty v
           | None -> mk loc f.Tast.fty (Tast.Zero f.Tast.fty))
        s.Tast.fields
    in
    expect loc ~want (mk loc (Types.Named name) (Tast.Make (name, fields)))

and check_arr ctx ~want loc items =
  let elem_want =
    match want with
    | Some (Types.Array (_, t)) -> Some t
    | Some (Types.Slice t) -> Some t
    | _ -> None
  in
  let items = map_lr (fun i -> check ctx ?want:elem_want i) items in
  let n = Int64.of_int (List.length items) in
  let elem =
    match elem_want, items with
    | Some t, _ -> t
    | None, first :: _ -> first.Tast.ty
    | None, [] ->
      fail loc "an empty array literal needs a type — annotate the binding"
  in
  List.iter
    (fun (i : Tast.expr) ->
       if not (Types.fits ~expected:elem ~actual:i.Tast.ty) then
         fail i.Tast.loc "this array's elements are %s, but this one is %s"
           (Types.to_string elem) (Types.to_string i.Tast.ty))
    items;
  (match want with
   | Some (Types.Array (m, _)) when not (Int64.equal m n) ->
     fail loc "expected %Ld elements, found %Ld" m n
   | _ -> ());
  (* [n T] and [T] are distinct in type and in ownership (spec-memory.md), so
     an array literal does not satisfy a slice expectation. *)
  expect loc ~want (mk loc (Types.Array (n, elem)) (Tast.Arr items))

and check_match ctx ?want loc scrutinee arms =
  let s = check ctx scrutinee in
  let elem =
    match s.Tast.ty with
    | Types.Option t -> t
    (* An enum is the one scrutinee that is not a milestone away: it is an i32
       at run time and its members are all known, so the arms would be a chain
       of [=] with an exhaustiveness check over [env.enums] — a desugaring, not
       a new IR node. What blocks it is upstream of here: a keyword has no case
       in [Ast.pattern], and [lib/load.ml] matches that type exhaustively, so
       the variant cannot be added. Said as itself rather than folded into the
       milestone answer below, because the milestone is not the reason. *)
    | Types.Enum n ->
      fail loc
        "match over the enum %s is not implemented — the lowering is a chain \
         of (= k :member), but a keyword has no case in the pattern type yet. \
         Use cond" n
    | other ->
      (* Union matching arrives with unions themselves, at milestone 6. *)
      fail loc "match works on an Option at milestone 2, not on %s"
        (Types.to_string other)
  in
  let want = ref want in
  let saw_some = ref false and saw_none = ref false and saw_wild = ref false in
  (* The same rule as [if], and for the same reason: the arms are alternatives,
     so each is checked from the state before the match and the union of what
     they moved survives the join. Checked in sequence against one mutating set
     they would report the second arm's (free v) as a use after the first arm's
     move, which is a legal program refused. *)
  let before = ctx.dead in
  let joined = ref [] in
  let arms =
    map_lr
      (fun (a : Ast.arm) ->
         let ctor, binds =
           match a.Ast.pat with
           | Ast.Pwild -> saw_wild := true; None, []
           | Ast.Pctor ("Some", [ x ]) -> saw_some := true; Some "Some", [ x ]
           | Ast.Pctor ("Some", _) ->
             fail a.Ast.aloc "the Some pattern binds exactly one name"
           | Ast.Pctor ("None", []) -> saw_none := true; Some "None", []
           | Ast.Pctor ("None", _) -> fail a.Ast.aloc "None binds no names"
           | Ast.Pctor (c, _) ->
             fail a.Ast.aloc
               "%s is not a case of Option — the cases are Some and None" c
         in
         ctx.dead <- before;
         let arm =
           scoped ctx (fun () ->
             let binds =
               List.map (fun n -> bind ctx n elem ~assignable:false) binds
             in
             let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
             if !want = None && body.Tast.ty <> Types.Never then
               want := Some body.Tast.ty;
             { Tast.acase = ctor; binds; abody = [ body ] })
         in
         joined :=
           !joined
           @ List.filter (fun (k, _) -> not (List.mem_assoc k !joined)) ctx.dead;
         arm)
      arms
  in
  ctx.dead <- !joined;
  if not (!saw_wild || (!saw_some && !saw_none)) then
    fail loc
      "this match is not exhaustive — Option needs both Some and None, or a \
       _ arm";
  let ty = match !want with Some t -> t | None -> Types.Never in
  mk loc ty (Tast.Match (s, arms))

(* ── Places ────────────────────────────────────────────────────────── *)

(* The target of [.field] is a struct, or one level of pointer to one. The
   auto-deref is inserted here as a real node, so no backend re-derives it. *)
and struct_target ctx (target : Ast.expr) : Tast.expr * string =
  let t = check ctx target in
  match t.Tast.ty with
  | Types.Named n when Hashtbl.mem ctx.env.structs n -> t, n
  | Types.Ptr (Types.Named n) when Hashtbl.mem ctx.env.structs n ->
    mk t.Tast.loc (Types.Named n) (Tast.Deref t), n
  | other ->
    fail target.Ast.loc "%s is not a struct, so it has no fields"
      (Types.to_string other)

and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
  match p with
  | Ast.Pvar name ->
    (match lookup ctx name with
     | Some b ->
       if not b.assignable then
         fail loc
           "%s is a parameter, and parameters are not assignable places \
            (spec-memory.md) — bind a local with let" name;
       Tast.Plocal b.slot, b.bty
     | None ->
       match Hashtbl.find_opt ctx.env.globals name with
       | Some (_, true) -> fail loc "%s is a constant" name
       | Some (ty, false) -> Tast.Pglobal name, ty
       | None -> captured ctx loc name; fail loc "unknown name %s" name)
  | Ast.Pfield (target, name) ->
    let target, sname = struct_target ctx target in
    let s = Hashtbl.find ctx.env.structs sname in
    (match Tast.field_index s name with
     | None -> fail loc "%s has no field %s" sname name
     | Some i -> Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
  | Ast.Pindex (target, idx) ->
    let target = borrowed ctx target (fun () -> check ctx target) in
    (match target.Tast.ty with
     (* The same bounds and epoch check the value form gets, through the same
        helper: an element of a Vec is a place because a Vec element is
        assignable, and a set that skipped the checks would be the asymmetry
        [nth] was removed for. *)
     | Types.Vec _ ->
       let p, ty = vec_at ctx loc target idx in
       Tast.Pderef p, ty
     | _ ->
       let idx, ty = indexed ctx target idx in
       Tast.Pindex (target, idx), ty)
  | Ast.Pderef target ->
    let target = check ctx target in
    (match target.Tast.ty with
     | Types.Ptr t -> Tast.Pderef target, t
     | other ->
       fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))

(* An index or a slice bound that is a literal is known now, so it is an error
   now rather than a trap later. Only literals: a [defconst] is a global in the
   typed IR, not a folded constant, so [(at arr size)] still traps at runtime —
   which is what the emitted bounds check is for. A negative literal is wrong
   whatever the target, but a length is static only for [n T]. *)
and static_index loc (ty : Types.t) ~past_end what k =
  if k < 0L then
    fail loc "%s %Ld is negative — indices count from 0" what k;
  match ty with
  (* [past_end] is the difference between an index and a slice bound: the last
     valid index is len - 1, but a slice may end at len. *)
  | Types.Array (n, _) when if past_end then k > n else k >= n ->
    fail loc "%s %Ld is out of bounds for length %Ld" what k n
  | _ -> ()

(* The literal value of a checked expression, if it has one. *)
and literal (e : Tast.expr) =
  match e.Tast.e with Tast.Int (k, _) -> Some k | _ -> None

(* An index is [i32] internally, but a *narrower* integer may be written as
   one: indexing is not arithmetic on the value, so there is nothing for a
   visible cast to warn about, and requiring (i32 c) at every subscript would
   be noise. A u32 is included because it cannot lose a value the bounds check
   would then miss — anything above 2^31 truncates to a negative i32, which
   the unsigned comparison rejects. i64 and u64 are not: 2^32 + 5 truncates to
   5 and would read the wrong element with no trap at all, so those need the
   cast written out. *)
and index_expr ctx (e : Ast.expr) =
  (* No [want]: an expectation of [i32] would reject a [u32] index outright,
     before there is anything here to convert. An untyped literal still
     defaults to [i32] on its own. *)
  let v = check ctx e in
  match v.Tast.ty with
  | Types.Int Types.I32 -> v
  | Types.Int k when Types.bits k <= 32 ->
    { v with Tast.ty = index_ty;
             Tast.e = Tast.Prim (Tast.Cast index_ty, [ v ]) }
  | Types.Int k ->
    fail e.Ast.loc
      "an index is an i32, and %s is wider — write (i32 …), because a value \
       that does not fit truncates to one that does and would read the wrong \
       element without tripping the bounds check" (Types.ikind_name k)
  | other ->
    fail e.Ast.loc "an index is an integer, found %s" (Types.to_string other)

(* [(at a i)] and [(at grid row col)]: one index per dimension. *)
and indexed ctx (target : Tast.expr) (idx : Ast.expr list) =
  let rec go ty = function
    | [] -> [], ty
    | i :: rest ->
      let elem =
        match ty with
        | Types.Array (_, t) | Types.Slice t -> t
        | other ->
          fail i.Ast.loc "%s cannot be indexed" (Types.to_string other)
      in
      let loc = i.Ast.loc in
      let i = index_expr ctx i in
      (match literal i with
       | Some k -> static_index loc ty ~past_end:false "index" k
       | None -> ());
      let rest, ty = go elem rest in
      i :: rest, ty
  in
  go target.Tast.ty idx

(* ── Calls ─────────────────────────────────────────────────────────── *)

and check_call ctx ~want loc (head : Ast.expr) (args : Ast.expr list) =
  match head.Ast.e with
  | Ast.Var name -> named_call ctx ~want loc name args
  | _ ->
    unimplemented loc "calling something other than a named function" 5

and arity loc name n args =
  if List.length args <> n then
    fail loc "%s takes %d argument%s, given %d" name n
      (if n = 1 then "" else "s") (List.length args)

(* The operators that fold: [+ - * /], [min]/[max] and the three bitwise
   combining operators all take two operands or more, and mean the same thing
   applied left to right. [%] and the shifts are not in that set — a chain of
   remainders or of shifts has no reading a reader would agree on in advance,
   so there the arity error is the useful answer.

   Two is the floor, and the two missing cases are refused rather than
   invented. Zero operands would have to mean an identity element, 0 for + and
   1 for *, and a sum with no terms in it is a typo far more often than it is
   an intent. One operand would have to mean negation for [-] and reciprocal
   for [/], and this language has no unary minus anywhere: the prelude writes
   every negation as [(- 0 n)] or [(- 0.0 x)], and [(- x)] meaning something
   else than the [-] two lines above it is a rule a reader has to carry rather
   than see. *)
and fold_arity loc name args =
  match args with
  | _ :: _ :: _ -> ()
  | [ _ ] when String.equal name "-" ->
    fail loc
      "- takes two arguments or more, given 1 — there is no unary minus; \
       write (- 0 x) to negate, which is what the prelude does"
  | [ _ ] when String.equal name "/" ->
    fail loc
      "/ takes two arguments or more, given 1 — there is no reciprocal; \
       write (/ 1.0 x)"
  | _ ->
    fail loc "%s takes two arguments or more, given %d" name (List.length args)

(* The first two operands decide the type — [binary] picks which of them is
   allowed to, and that decision is not re-made per pair — and every operand
   after them is checked against it. *)
and fold_left_prim ctx ~want loc name p ok what args =
  let x, y, rest =
    match args with x :: y :: rest -> x, y, rest | _ -> assert false
  in
  let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
  if not (ok a.Tast.ty) then
    fail loc "%s takes %s, found %s" name what (Types.to_string a.Tast.ty);
  let ty = a.Tast.ty in
  let acc =
    List.fold_left
      (fun acc arg ->
         mk loc ty (Tast.Prim (p, [ acc; check ctx ~want:ty arg ])))
      (mk loc ty (Tast.Prim (p, [ a; b ])))
      rest
  in
  expect loc ~want acc

(* ── Allocation failure, spec-memory.md ────────────────────────────────
   No allocating operation returns an error and none can fail silently. When
   the allocator cannot satisfy a request the operation signals

     (StorageExhausted {:bytes n :align a :allocator id})

   with [error] — whose type is Never — inside a [restart-case] offering
   [retry]. That is one rule over every allocating operation, which is what
   keeps [push] and [reserve] at Unit, [clone] at the container, and no
   signature anywhere growing a Result. Odin's [append] returns an ignorable
   Allocator_Error and its type-erased path returns the old length on a failed
   reserve; an append that appends nothing and says nothing is the outcome this
   rule exists to make impossible.

   It is *compiler-emitted at the point of failure*, which spec-memory.md names
   as the exception to plan.org's "restarts go at the resync point, once": a
   restart established at a parser's top-level loop cannot re-attempt an
   allocation, and only the allocation site can.

   The shape is built out of nodes that already exist — a while, a restart-case
   and an error — so the backend learns nothing new about allocation:

     (let [ok false]
       (while (not ok)
         (restart-case
           (do (set ok ATTEMPT)
               (if (not ok) (error (StorageExhausted {...}))))
           (retry []))))

   A handler that frees something, releases a scratch region or grows the arena
   and then invokes [retry] lands in the clause, the clause falls through, and
   the while re-tests and re-attempts the *same* request. With nothing handling
   it, [error] stops the program on the frame that erred, as §2 says.

   [attempt] must be a call that can be repeated: every argument to it is bound
   to a slot before the loop, so a retry does not re-evaluate the element
   expression a push was given. *)
and alloc_guard ctx loc (attempt : Tast.expr) =
  let ok = fresh_slot ctx Types.Bool in
  let okv = mk loc Types.Bool (Tast.Local ok) in
  let notok () = mk loc Types.Bool (Tast.Prim (Tast.Not, [ okv ])) in
  let i8 n = mk loc (Types.Int Types.I8) (Tast.Int (n, Types.I8)) in
  (* The runtime answers 1 or 0 and never reports failure any other way. *)
  let attempt = mk loc Types.Bool (Tast.Prim (Tast.Ne, [ attempt; i8 0L ])) in
  (* A value struct on the signalling frame's stack, with fixed numeric fields
     and no rendered message: formatting would allocate, and this is the one
     path that must not. Rendering happens in the handler or the break loop,
     where a working allocator is known. *)
  let cond =
    mk loc (Types.Named "StorageExhausted")
      (Tast.Make
         ("StorageExhausted",
          [ rt loc (Types.Int Types.I64) "flan_alloc_fail_bytes" [];
            rt loc (Types.Int Types.I64) "flan_alloc_fail_align" [];
            rt loc (Types.Int Types.I64) "flan_alloc_fail_id" [] ]))
  in
  let signal =
    mk loc Types.Never
      (Tast.Signal (Tast.Serror, type_id "StorageExhausted", cond))
  in
  let attempt_then_signal =
    mk loc Types.Unit
      (Tast.Do
         [ mk loc Types.Unit (Tast.Set (Tast.Plocal ok, attempt));
           mk loc Types.Unit (Tast.If (notok (), signal, unit_at loc)) ])
  in
  let clause =
    (* Compiler-emitted, so it takes no parameters: nothing outside can hand
       this one a value. [rsig] is therefore the empty signature, and its hash
       the same one a written [(retry [] ...)] gets — the two must agree, since
       an [invoke-restart] cannot tell them apart. *)
    let sg = restart_sig [] in
    { Tast.rname_id = type_id "retry"; rname = "retry"; rparams = [];
      rsig = sg; rsig_id = type_id sg; rbody = [ unit_at loc ] }
  in
  let body =
    mk loc Types.Unit (Tast.RestartCase ([ clause ], attempt_then_signal))
  in
  mk loc Types.Unit
    (Tast.Let ([ (ok, mk loc Types.Bool (Tast.Bool false)) ],
               [ mk loc Types.Unit (Tast.While (notok (), [ body ])) ]))

(* The element type for [vec-new]: a leading bare symbol naming a type, or the
   expectation at the site. A bare symbol shadowed by a local or a global is
   that binding — an allocator, in practice — and not a type. *)
and vec_new_elem ctx ~want loc args =
  let named =
    match args with
    | { Ast.e = Ast.Var n; _ } :: rest
      when lookup ctx n = None
        && (not (Hashtbl.mem ctx.env.globals n))
        && (List.mem n Types.primitive_names
            || Hashtbl.mem ctx.env.structs n
            || Hashtbl.mem ctx.env.enums n
            || Hashtbl.mem ctx.env.aliases n) ->
      Some (resolve_name ctx.env ~seen:[] loc n, rest)
    | _ -> None
  in
  match named with
  | Some (t, rest) -> t, rest
  | None ->
    (match want with
     | Some (Types.Vec t) -> t, args
     | _ ->
       fail loc
         "nothing here says what (vec-new) is a Vec of — write the element \
          type, as (vec-new i32), or give the binding a type")

(* The element type, or the reason this is not a Vec. *)
and vec_elem loc what (t : Types.t) =
  match t with
  | Types.Vec e -> e
  | other -> fail loc "%s takes a (Vec T), found %s" what (Types.to_string other)

(* The allocator an operation uses: the one named at the site, or the current
   implicit one. spec-memory.md: an operation never falls back to a hidden
   global allocator, and an explicit allocator can override the context. *)
and allocator_arg ctx loc = function
  | [] -> rt loc Types.Alloc "flan_context_allocator" []
  | [ a ] -> check ctx ~want:Types.Alloc a
  | _ -> fail loc "at most one allocator may be named here"

(* The address of an element, bounds-checked, with the allocator's epoch
   checked first. Both the value form [(at v i)] and the place form
   [(set (at v i) x)] come through here, so they cannot drift apart — which is
   the asymmetry [nth] was removed for. *)
and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
  let elem = vec_elem loc "at" target.Tast.ty in
  match idx with
  | [ i ] ->
    let i = index_expr ctx i in
    rt loc (Types.Ptr elem) "flan_vec_at"
      [ target; i; size_of loc elem; here loc ], elem
  | _ ->
    fail loc
      "a Vec takes exactly one index — (at v i) — and its element is indexed \
       separately"

and named_call ctx ~want loc name args =
  let prim p ty args = expect loc ~want (mk loc ty (Tast.Prim (p, args))) in
  match name with
  (* ── arithmetic and comparison ─────────────────────────────────── *)
  | "+" | "-" | "*" | "/" ->
    let p = match name with
      | "+" -> Tast.Add | "-" -> Tast.Sub | "*" -> Tast.Mul
      | _ -> Tast.Div
    in
    fold_arity loc name args;
    fold_left_prim ctx ~want loc name p Types.is_numeric "numbers" args
  (* Remainder stays at two: (% a b c) is (% (% a b) c), which is a thing
     nobody writes on purpose. *)
  | "%" ->
    arity loc name 2 args;
    let a, b = binary ctx name loc ~want:(numeric_want want) args in
    if not (Types.is_numeric a.Tast.ty) then
      fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
    prim Tast.Rem a.Tast.ty [ a; b ]
  | "=" | "!=" | "<" | "<=" | ">" | ">=" ->
    let p = match name with
      | "=" -> Tast.Eq | "!=" -> Tast.Ne | "<" -> Tast.Lt
      | "<=" -> Tast.Le | ">" -> Tast.Gt | _ -> Tast.Ge
    in
    arity loc name 2 args;
    let a, b = binary ctx name loc ~want:None args in
    if not (Types.is_comparable a.Tast.ty) then
      fail loc
        "%s compares machine numbers; %s has no built-in comparison \
         (plan.org, Types)" name (Types.to_string a.Tast.ty);
    prim p Types.Bool [ a; b ]
  | "not" ->
    arity loc name 1 args;
    prim Tast.Not Types.Bool [ check ctx ~want:Types.Bool (List.hd args) ]
  (* Bitwise operators are integers-only, and the shift count has the same type
     as the value shifted — there is no implicit widening anywhere else either. *)
  | "bit-and" | "bit-or" | "bit-xor" ->
    let p = match name with
      | "bit-and" -> Tast.BitAnd | "bit-or" -> Tast.BitOr
      | _ -> Tast.BitXor
    in
    fold_arity loc name args;
    fold_left_prim ctx ~want loc name p
      (function Types.Int _ -> true | _ -> false) "integers" args
  (* The shifts stay at two, and not only because a shift chain reads badly:
     each count would be checked against the same width below, so (<< x 30 30)
     would pass two legal shifts and still shift the value away entirely. *)
  | "<<" | ">>" ->
    let p = if String.equal name "<<" then Tast.Shl else Tast.Shr in
    arity loc name 2 args;
    let a, b = binary ctx name loc ~want:(numeric_want want) args in
    (match a.Tast.ty with
     | Types.Int _ -> ()
     | other -> fail loc "%s takes integers, found %s" name
                  (Types.to_string other));
    (* A shift by the operand's own width or more is poison in LLVM, which at
       -O2 turns the whole function into an undefined value rather than into a
       wrong number. A literal count is rejected here — that is the typo — and
       [emit] masks a computed one, so no shift can reach the hardware out of
       range. *)
    (match a.Tast.ty, b.Tast.e with
     | Types.Int k, Tast.Int (n, _) when p = Tast.Shl || p = Tast.Shr ->
       let w = Int64.of_int (Types.bits k) in
       if Int64.unsigned_compare n w >= 0 then
         fail loc
           "%s by %Ld is out of range for %s, which is %d bits wide" name n
           (Types.to_string a.Tast.ty) (Types.bits k)
     | _ -> ());
    prim p a.Tast.ty [ a; b ]
  (* (min a b) and (max a b) evaluate each operand once — hence the slots —
     because a min over two calls must not call either of them twice.

     Which is also why this one does not go through [fold_left_prim]: there is
     no Prim to fold, and the pair it folds is a whole comparison. Each step
     puts *both* of its sides in slots, the accumulated pick included, so the
     three-operand form is two nested lets and still exactly one evaluation of
     each operand — where reusing the previous [If] as an operand of the next
     would have duplicated everything inside it. *)
  | "min" | "max" ->
    fold_arity loc name args;
    let x, y, rest =
      match args with x :: y :: rest -> x, y, rest | _ -> assert false
    in
    let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
    if not (Types.is_numeric a.Tast.ty) then
      fail loc "%s takes numbers, found %s" name (Types.to_string a.Tast.ty);
    let ty = a.Tast.ty in
    let cmp = if String.equal name "min" then Tast.Lt else Tast.Gt in
    let pick a b =
      let sa = fresh_slot ctx ty and sb = fresh_slot ctx ty in
      let la = mk loc ty (Tast.Local sa) and lb = mk loc ty (Tast.Local sb) in
      let test = mk loc Types.Bool (Tast.Prim (cmp, [ la; lb ])) in
      mk loc ty (Tast.Let ([ (sa, a); (sb, b) ],
                           [ mk loc ty (Tast.If (test, la, lb)) ]))
    in
    expect loc ~want
      (List.fold_left (fun acc arg -> pick acc (check ctx ~want:ty arg))
         (pick a b) rest)
  (* (zeroed) is the all-bytes-zero value of whatever it is being stored into,
     so it only means anything where a type is expected of it. *)
  | "zeroed" ->
    arity loc name 0 args;
    (match want with
     | Some ty when ty <> Types.Never -> mk loc ty (Tast.Zero ty)
     | _ ->
       fail loc
         "zeroed needs to know the type it is zeroing — use it where one is \
          expected, as in (set grid (zeroed))")

  (* The one half of a destructuring [let] that [Parse] cannot do on its own.
     Everything else about a pattern is bindings and field accesses it already
     wrote; the arity is a *type* question — how many elements the value has —
     and there are no types in the parser. So the pattern's shape travels here
     as arguments: which element this binding wants, how many names the pattern
     binds, and whether that count is exact or a minimum (it is a minimum when
     the pattern ends in [& rest]).

     No source symbol can contain a [~] — the reader makes it a delimiter — so
     this name is unspellable and nothing but [Parse] can reach it. *)
  | "destructure~nth" ->
    (match args with
     | [ target;
         { Ast.e = Ast.Int i; _ }; { Ast.e = Ast.Int n; _ };
         { Ast.e = Ast.Int exact; _ } ] ->
       let plural k = if Int64.equal k 1L then "" else "s" in
       let target = check ctx target in
       (match target.Tast.ty with
        | Types.Array (m, elem) ->
          if Int64.equal exact 1L && not (Int64.equal m n) then
            fail loc
              "this pattern binds %Ld name%s, but %s has %Ld element%s — a \
               pattern over a fixed array names every element, or ends in \
               [& rest]"
              n (plural n) (Types.to_string target.Tast.ty) m (plural m);
          if Int64.equal exact 0L && Int64.compare m n < 0 then
            fail loc
              "this pattern binds %Ld name%s before the &, but %s has only %Ld \
               element%s" n (plural n) (Types.to_string target.Tast.ty) m
              (plural m);
          prim Tast.At elem
            [ target; mk loc index_ty (Tast.Int (i, Types.I32)) ]
        (* The asymmetry is real and is the reason this is refused rather than
           lowered to a bounds-checked [at]: a fixed array's length is in its
           type, so [[a b]] over a [[2 f32]] is a claim the checker can settle,
           and over a [[T]] it is a claim about a number that does not exist
           until the program runs. Turning it into a runtime trap would be a
           pattern that type checks and then kills the program, which is the
           trade this language does not make. *)
        | Types.Slice _ ->
          fail loc
            "a pattern cannot destructure %s: a slice's length is a runtime \
             value, so nothing here can check that it has %Ld element%s. Use \
             (at s i) and test (len s) yourself"
            (Types.to_string target.Tast.ty) n (plural n)
        | other ->
          fail loc
            "%s is not a fixed array, so [a b ...] cannot destructure it"
            (Types.to_string other))
     | _ ->
       fail loc
         "destructure~nth is written by the compiler and cannot be called")

  (* ── allocators, spec-memory.md ────────────────────────────────── *)
  (* Every one of these is an ordinary named call, which is the whole of the
     escape NEXT.md describes: [check_call] already routes a named call through
     here, so none of the four function-value refusals is anywhere near it. *)
  (* A *user-written* allocator is the one thing in this tier that does need
     milestone 5, and it is refused by name rather than left as an unknown
     one. "Here is my proc, make an Allocator from it" needs a defn's name in
     value position, which is the refusal a few hundred lines below this. The
     built-in set needs nothing from milestone 5 because its procedures are C
     symbols the emitter names and no Flan type mentions them. *)
  | "make-allocator" | "allocator-from" | "allocator" ->
    fail loc
      "a user-written allocator is not implemented yet — milestone 5. It needs \
       a defn's name in value position, which is a function value; the \
       built-in allocators (heap-allocator, arena-new) need none of that \
       because their procedures are runtime symbols and no Flan type names \
       them"
  | "heap-allocator" ->
    arity loc name 0 args;
    expect loc ~want
      (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_heap_allocator", [])))
  (* The capacity is explicit and there is no growing backing store: an arena
     whose size is decided by the program is one a program can reason about,
     and it is the only shape under which "exhausted" is a state a test can
     reach on purpose. *)
  | "arena-new" ->
    arity loc name 1 args;
    let cap = check ctx ~want:(Types.Int Types.I64) (List.hd args) in
    expect loc ~want
      (mk loc Types.Alloc (Tast.Prim (Tast.Rt "flan_arena_new", [ cap ])))
  (* Hands the pages back, which [free-all] deliberately does not — see
     BUILT.md, "free-all is retain-capacity". *)
  | "arena-destroy" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc Types.Unit (Tast.Prim (Tast.Rt "flan_arena_destroy", [ a ])))
  (* One of spec-memory.md's two release points. It takes the source location
     as a string so that an allocator with no region to release names the site
     rather than the runtime. *)
  | "free-all" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc Types.Unit
         (Tast.Prim (Tast.Rt "flan_alloc_free_all", [ a; here loc ])))
  (* The capability set, read off the allocator value. Odin asks its procedure
     (Query_Features returning an Allocator_Mode_Set); a field is the same
     answer without the round trip, which is NEXT.md's call. *)
  | "can-free?" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc Types.Bool
         (Tast.Prim (Tast.Ne,
                     [ mk loc (Types.Int Types.I8)
                         (Tast.Prim (Tast.Rt "flan_alloc_can_free", [ a ]));
                       mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ])))
  | "can-free-all?" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc Types.Bool
         (Tast.Prim (Tast.Ne,
                     [ mk loc (Types.Int Types.I8)
                         (Tast.Prim (Tast.Rt "flan_alloc_can_free_all", [ a ]));
                       mk loc (Types.Int Types.I8) (Tast.Int (0L, Types.I8)) ])))
  (* The counter [free-all] bumps. A container records it and traps if it
     moved; this is the same number, readable, so a program can say what it
     saw. *)
  | "alloc-epoch" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc (Types.Int Types.I64)
         (Tast.Prim (Tast.Rt "flan_alloc_epoch", [ a ])))
  (* The allocator's identity — its address — which is what the condition's
     :allocator field carries, so a handler holding several regions can tell
     which one ran out. *)
  | "alloc-id" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Rt "flan_alloc_id", [ a ])))
  (* A ceiling on live bytes, 0 for none. spec-memory.md's retry restart is
     answerable only by a handler that can make the *same* request succeed, and
     for a fixed backing store the handler that works is the one that grows it:
     releasing the region a container lives in invalidates the container, which
     is what the epoch check catches. So the spec's "grows the arena and then
     invokes retry" needs a ceiling to raise, and this is it. It is also how a
     program exhausts an allocator on purpose. *)
  | "alloc-budget" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc (Types.Int Types.I64)
         (Tast.Prim (Tast.Rt "flan_alloc_budget", [ a ])))
  | "set-alloc-budget" ->
    arity loc name 2 args;
    (match args with
     | [ a; n ] ->
       let a = check ctx ~want:Types.Alloc a in
       let n = check ctx ~want:(Types.Int Types.I64) n in
       expect loc ~want
         (mk loc Types.Unit (Tast.Prim (Tast.Rt "flan_alloc_set_budget", [ a; n ])))
     | _ -> assert false)
  (* "Did you forget to free" is an allocator-tier question and this is the
     tier answering it — spec-memory.md, "Leaking is defined behaviour". *)
  | "alloc-live-blocks" ->
    arity loc name 1 args;
    let a = check ctx ~want:Types.Alloc (List.hd args) in
    expect loc ~want
      (mk loc (Types.Int Types.I64)
         (Tast.Prim (Tast.Rt "flan_alloc_live_blocks", [ a ])))
  (* (with-allocator A BODY...). It rebinds and releases nothing: not at the
     end of the body, not anywhere. spec-memory.md is explicit that this is not
     a scope-end release point and that it is the point on which Odin's
     [defer delete] and Carp's scope-end frees were both rejected. *)
  | "with-allocator" ->
    (match args with
     | [] -> fail loc "with-allocator is (with-allocator allocator body ...)"
     | a :: body ->
       let a = check ctx ~want:Types.Alloc a in
       let body, ty =
         scoped ctx (fun () ->
           match body with
           | [] -> [ unit_at loc ], Types.Unit
           | _ ->
             let rec go = function
               | [ last ] -> let l = check ctx ?want last in [ l ], l.Tast.ty
               | e :: rest ->
                 let e = check ctx e in
                 let rest, ty = go rest in
                 e :: rest, ty
               | [] -> assert false
             in
             go body)
       in
       expect loc ~want (mk loc ty (Tast.WithAlloc (a, body))))

  (* ── (Vec T), spec-memory.md ───────────────────────────────────── *)
  (* Every one of these is a named call over a type-erased runtime, with
     size_of and align_of produced here because here is where the concrete
     element type is known. No generics are involved and none are needed. *)
  (* (vec-new), (vec-new T), (vec-new a), (vec-new T a).
     [let] has no type annotation — parse.ml settles that a triple binding is
     ambiguous and types are inferred — so a local Vec has nowhere to say what
     it holds, and the element type is written at the call instead. This is not
     the explicit instantiation syntax the generics section rules out: nothing
     here is generic, and the name is resolved as an ordinary type, not bound
     to a type variable. Where the context does say — a defvar's type, a
     function's return type, an argument — it is not needed and may be left
     out. *)
  | "vec-new" ->
    let elem, args = vec_new_elem ctx ~want loc args in
    let a = allocator_arg ctx loc args in
    let v = fresh_slot ctx (Types.Vec elem) in
    let attempt =
      rt loc (Types.Int Types.I8) "flan_vec_init"
        [ mk loc (Types.Vec elem) (Tast.Local v); a; i64_at loc 0L;
          size_of loc elem; align_of loc elem; here loc ]
    in
    expect loc ~want
      (mk loc (Types.Vec elem)
         (Tast.Let ([ (v, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
                    [ alloc_guard ctx loc attempt;
                      mk loc (Types.Vec elem) (Tast.Local v) ])))
  (* Unit, not a Result and not an ignorable error code: see [alloc_guard]. *)
  | "push" ->
    arity loc name 2 args;
    (match args with
     | [ target; x ] ->
       let target = borrowed ctx target (fun () -> check ctx target) in
       let elem = vec_elem loc "push" target.Tast.ty in
       let x = check ctx ~want:elem x in
       (* The element is bound before the loop so that a [retry] re-attempts
          the allocation and not the expression that produced the value. *)
       let e = fresh_slot ctx elem in
       let attempt =
         rt loc (Types.Int Types.I8) "flan_vec_push"
           [ target; addr_of loc (mk loc elem (Tast.Local e));
             size_of loc elem; align_of loc elem; here loc ]
       in
       expect loc ~want
         (mk loc Types.Unit
            (Tast.Let ([ (e, x) ], [ alloc_guard ctx loc attempt ])))
     | _ -> assert false)
  | "reserve" ->
    arity loc name 2 args;
    (match args with
     | [ target; n ] ->
       let target = borrowed ctx target (fun () -> check ctx target) in
       let elem = vec_elem loc "reserve" target.Tast.ty in
       let n = check ctx ~want:index_ty n in
       let n64 =
         mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
       in
       let attempt =
         rt loc (Types.Int Types.I8) "flan_vec_reserve"
           [ target; n64; size_of loc elem; align_of loc elem; here loc ]
       in
       expect loc ~want (alloc_guard ctx loc attempt)
     | _ -> assert false)
  (* (as-slice v) and (as-slice v lo hi) — spec-memory.md, "Borrowing". The
     result is a non-owning view: copying it copies ptr+len and never the
     elements, and it carries no allocator, so freeing through one is not
     expressible. A push, a put or a reserve may invalidate it; that is the
     explicit Zig/Odin contract the spec chose over a borrow checker. *)
  | "as-slice" ->
    (match args with
     | target :: rest when List.length rest = 0 || List.length rest = 2 ->
       let target = borrowed ctx target (fun () -> check ctx target) in
       let elem = vec_elem loc "as-slice" target.Tast.ty in
       let lo, hi =
         match rest with
         | [] ->
           mk loc index_ty (Tast.Int (0L, Types.I32)),
           (* -1 is "to the end": (as-slice v) has no static length to pass. *)
           mk loc index_ty (Tast.Int (-1L, Types.I32))
         | [ lo; hi ] -> index_expr ctx lo, index_expr ctx hi
         | _ -> assert false
       in
       let out = fresh_slot ctx (Types.Slice elem) in
       let fill =
         rt loc Types.Unit "flan_vec_as_slice"
           [ target; addr_of loc (mk loc (Types.Slice elem) (Tast.Local out));
             lo; hi; size_of loc elem; here loc ]
       in
       expect loc ~want
         (mk loc (Types.Slice elem)
            (Tast.Let ([ (out, mk loc (Types.Slice elem)
                                 (Tast.Zero (Types.Slice elem))) ],
                       [ fill; mk loc (Types.Slice elem) (Tast.Local out) ])))
     | _ -> fail loc "as-slice is (as-slice v) or (as-slice v lo hi)")
  (* spec-memory.md's first release point. It consumes its argument exactly as
     any other move does — the source binding is dead afterwards and using it
     is a compile error — which is the rule that already makes a double free
     unrepresentable, so [free] needs no analysis of its own. *)
  | "free" ->
    arity loc name 1 args;
    let target = check ctx (List.hd args) in
    (match target.Tast.ty with
     | Types.Vec elem ->
       expect loc ~want
         (rt loc Types.Unit "flan_vec_free"
            [ target; size_of loc elem; align_of loc elem; here loc ])
     | other ->
       (* A field is never freed on its own: it would leave its owner partly
          dead with no way to say so. *)
       fail loc
         "free takes a move-only value — a Vec, or a struct that owns one — \
          found %s. A resource type with a drop hook is step 5 and does not \
          exist yet"
         (Types.to_string other))
  (* (clone v) uses the current allocator, (clone v a) names one. A deep,
     independent copy: spec-memory.md's "copying is always explicit". *)
  | "clone" ->
    (match args with
     | target :: rest when List.length rest <= 1 ->
       let target = borrowed ctx target (fun () -> check ctx target) in
       let elem = vec_elem loc "clone" target.Tast.ty in
       let a = allocator_arg ctx loc rest in
       let d = fresh_slot ctx (Types.Vec elem) in
       let attempt =
         rt loc (Types.Int Types.I8) "flan_vec_clone"
           [ mk loc (Types.Vec elem) (Tast.Local d); target; a;
             size_of loc elem; align_of loc elem; here loc ]
       in
       expect loc ~want
         (mk loc (Types.Vec elem)
            (Tast.Let ([ (d, mk loc (Types.Vec elem) (Tast.Zero (Types.Vec elem))) ],
                       [ alloc_guard ctx loc attempt;
                         mk loc (Types.Vec elem) (Tast.Local d) ])))
     | _ -> fail loc "clone is (clone v) or (clone v allocator)")

  (* ── containers ────────────────────────────────────────────────── *)
  (* [at] and [len] were already the names for a fixed array and a slice, so a
     Vec extends them rather than adding a parallel pair — which is the
     asymmetry [nth] was removed for. A Vec's length is i32 like every other
     length here (index_ty): widening indices is one change across all of them
     and not a Vec question. *)
  | "len" ->
    arity loc name 1 args;
    let target = List.hd args in
    let a = borrowed ctx target (fun () -> check ctx target) in
    (match a.Tast.ty with
     | Types.Array _ | Types.Slice _ | Types.String ->
       prim Tast.Len index_ty [ a ]
     | Types.Vec _ ->
       let n = rt loc (Types.Int Types.I64) "flan_vec_len" [ a; here loc ] in
       expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
     | other ->
       fail loc "len takes an array, a slice, a string or a Vec, found %s"
         (Types.to_string other))
  | "at" ->
    (match args with
     | target :: idx when idx <> [] ->
       let target = borrowed ctx target (fun () -> check ctx target) in
       (match target.Tast.ty with
        | Types.Vec _ ->
          let p, elem = vec_at ctx loc target idx in
          expect loc ~want (mk loc elem (Tast.Deref p))
        | _ ->
          let idx, ty = indexed ctx target idx in
          prim Tast.At ty (target :: idx))
     | _ -> fail loc "%s is (%s collection index ...)" name name)
  | "slice" ->
    arity loc name 3 args;
    (match args with
     | [ target; lo; hi ] ->
       let target = check ctx target in
       let elem = match target.Tast.ty with
         | Types.Array (_, t) | Types.Slice t -> t
         | other -> fail loc "slice takes an array or a slice, found %s"
                      (Types.to_string other)
       in
       prim Tast.Slice (Types.Slice elem)
         (let lo_loc = lo.Ast.loc and hi_loc = hi.Ast.loc in
          let lo = check ctx ~want:index_ty lo in
          let hi = check ctx ~want:index_ty hi in
          let ty = target.Tast.ty in
          (* A bound may sit one past the end, so the length is checked against
             lo and hi both, not against the last valid index. *)
          (match literal lo with
           | Some k -> static_index lo_loc ty ~past_end:true "slice bound" k
           | None -> ());
          (match literal hi with
           | Some k -> static_index hi_loc ty ~past_end:true "slice bound" k
           | None -> ());
          (match literal lo, literal hi with
           | Some a, Some b when a > b ->
             fail loc "slice [%Ld %Ld) runs backwards — lo must not exceed hi" a b
           | _ -> ());
          [ target; lo; hi ])
     | _ -> assert false)

  (* ── pointers ──────────────────────────────────────────────────── *)
  | "addr" ->
    arity loc name 1 args;
    let a = List.hd args in
    (match place_of_expr a with
     | None ->
       fail a.Ast.loc
         "addr takes the address of a place — a name, (.field x), (at a i) \
          or (deref p)"
     | Some p ->
       let p, ty = check_place ctx a.Ast.loc p in
       expect loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p)))
  | "deref" ->
    arity loc name 1 args;
    let a = check ctx (List.hd args) in
    (match a.Tast.ty with
     | Types.Ptr t -> expect loc ~want (mk loc t (Tast.Deref a))
     | other -> fail loc "deref takes a (Ptr T), found %s"
                  (Types.to_string other))

  (* ── Option ────────────────────────────────────────────────────── *)
  | "Some" ->
    arity loc name 1 args;
    let inner = match want with Some (Types.Option t) -> Some t | _ -> None in
    let a = check ctx ?want:inner (List.hd args) in
    expect loc ~want (mk loc (Types.Option a.Tast.ty) (Tast.Some_ a))

  (* ── the milestone-2 host primitives (plan.org) ────────────────── *)
  | "bytes" ->
    arity loc name 1 args;
    prim Tast.Bytes (Types.Slice (Types.Int Types.U8))
      [ check ctx ~want:Types.String (List.hd args) ]

  (* (string b): a [u8] seen as a string. The mirror of (bytes s), spelled the
     same way — a type name in head position, like (bytes s) and unlike the
     numeric casts, which go through [is_cast] and really do convert.

     It costs nothing. emit.ml lowers Types.String and Types.Slice _ to the
     same %slice, 16 bytes at align 8, so a string and a [u8] are already the
     identical value at run time; both this and [Bytes] emit as the argument
     itself. What changes is only what the checker will let the value be
     passed to — which is the whole gap: i64->bytes answers a [u8] and every
     declare-c text parameter wants a string, and nothing joined them.

     Two decisions are baked in here.

     1. It does NOT check UTF-8, because `string` does not claim UTF-8. The
        prelude settles this: valid-utf8? is an ordinary function you call when
        you care, decode-rune/rune-at/rune-count all take [u8] rather than
        string, and decode-rune answers {:ok false :width 1} on a malformed
        byte rather than assuming its input is well-formed. The one place the
        runtime treats a string differently from a byte slice is
        flan_escape_bytes, for a string nested in a printed structure, and that
        is a byte-wise escape table with no decoding in it. So there is no code
        that would be wrong about a string of arbitrary bytes, and a check here
        would be the only enforcement point in the language — a claim the rest
        of it does not make.

     2. It does not widen the literal-write hole (NEXT.md, "Writing through a
        string literal"). That hole is the other direction: (bytes "Hi") hands
        you a writable-looking slice over constant data. This direction only
        loses the ability to write — a string is read-only everywhere — so the
        result of (string b) can reach strictly fewer stores than b could.
        Provenance is still what the other direction needs; nothing here
        depends on having it.

     The one sharp edge is not new but is easier to trip over now: the slice
     that i64->bytes / f64->bytes / u64->bytes answer is a view into one shared
     static buffer in the runtime, overwritten by the next such call. Calling
     it a string does not copy it. Use it before formatting the next number;
     you cannot hold two at once. *)
  | "string" ->
    arity loc name 1 args;
    prim Tast.StrOfBytes Types.String [ byte_slice ctx (List.hd args) ]
  | "bytes->f64" ->
    arity loc name 1 args;
    prim Tast.BytesToF64 (Types.Float Types.F64) [ byte_slice ctx (List.hd args) ]
  | "bytes->i64" ->
    arity loc name 1 args;
    prim Tast.BytesToI64 (Types.Int Types.I64) [ byte_slice ctx (List.hd args) ]
  | "f64->bytes" ->
    arity loc name 1 args;
    prim Tast.F64ToBytes (Types.Slice (Types.Int Types.U8))
      [ check ctx ~want:(Types.Float Types.F64) (List.hd args) ]
  | "i64->bytes" ->
    arity loc name 1 args;
    prim Tast.I64ToBytes (Types.Slice (Types.Int Types.U8))
      [ check ctx ~want:(Types.Int Types.I64) (List.hd args) ]
  | "write-stdout" ->
    arity loc name 1 args;
    prim Tast.WriteStdout Types.Unit [ byte_slice ctx (List.hd args) ]

  (* (println x) and (print x): the structural printer, selected on the type
     the argument checked to. plan.org, Milestone 5 — "compiler-provided,
     per concrete type". That is not overloading and needs no type variables:
     there is no dispatch at run time and no user-supplied printer to pick
     between. The walk itself is render.ml, shared with the REPL, which is what
     stops the two from drifting apart.

     [min]/[max]/[zeroed] above dispatch on the resolved argument type the same
     way. The slots the slice arm needs come out of the frame of whatever
     function this call is written in, via [fresh_slot] — allocated once per
     call site, at check time, not once per iteration of a loop around it.

     A string prints raw here and quoted inside a structure. Those are not in
     conflict: (println "hello") has to print hello or it is useless, and
     (println b) where b has a string field has to quote it or the field
     cannot be told from the punctuation. The split is exactly top level vs
     nested, which is why it lives here and not in the walk. *)
  | "print" | "println" ->
    arity loc name 1 args;
    (* Printing is a read, not a move: the walk goes over the value and keeps
       nothing. Without this, (println v) would consume a Vec and every
       printing of one would be its last. *)
    let target = List.hd args in
    let a = borrowed ctx target (fun () -> check ctx target) in
    let bslice = Types.Slice (Types.Int Types.U8) in
    let write x = mk loc Types.Unit (Tast.Prim (Tast.WriteStdout, [ x ])) in
    let conv pr x = mk loc bslice (Tast.Prim (pr, [ x ])) in
    let emitter : Render.emitter =
      { Render.ebytes = write;
        estr = (fun x -> write (conv Tast.EscapeBytes x));
        ei64 = (fun x -> write (conv Tast.I64ToBytes x));
        eu64 = (fun x -> write (conv Tast.U64ToBytes x));
        ef64 = (fun x -> write (conv Tast.F64ToBytes x)) }
    in
    let rc =
      { Render.structs =
          Hashtbl.fold (fun _ v acc -> v :: acc) ctx.env.structs [];
        enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) ctx.env.enums [];
        emit = emitter;
        alloc = (fun ty -> fresh_slot ctx ty) }
    in
    let parts =
      match a.Tast.ty with
      | Types.String | Types.Slice (Types.Int Types.U8) ->
        [ write (mk loc bslice (Tast.Prim (Tast.Bytes, [ a ]))) ]
      | _ -> Render.render rc 0 a
    in
    let nl =
      if String.equal name "println" then
        [ write
            (mk loc bslice
               (Tast.Prim (Tast.Bytes, [ mk loc Types.String (Tast.Str "\n") ])))
        ]
      else []
    in
    expect loc ~want (mk loc Types.Unit (Tast.Do (parts @ nl)))
  | "exit" ->
    arity loc name 1 args;
    prim Tast.Exit Types.Never [ check ctx ~want:index_ty (List.hd args) ]
  | "argv" ->
    arity loc name 0 args;
    prim Tast.Argv (Types.Slice Types.String) []

  (* ── casts: (i32 x), (f64 x), and an enum both ways ────────────────

     (i32 e) and (GamepadAxis n) are written here rather than in an arm of
     their own because they are the same operation: an enum is an i32 at run
     time — Types.Enum says so — and emit.ml's [cast] already reduces one to
     its i32 before choosing an instruction. So both directions cost nothing:
     src and target are equal after that reduction and [cast] answers the
     value unchanged.

     Why this does not give the typo back. The property worth keeping is that
     :spcae at a call site is an error at that site, and it still is: a
     keyword resolves against the parameter's enum and a bare integer does not
     fit one. What changes is only that a program can *say* it means the
     conversion, by name, at the site. The rule was never "an integer is
     dangerous", it was "an integer must not arrive silently", and a written
     (GamepadAxis i) is not silent.

     Three sub-decisions:

     1. enum → any numeric is always allowed and never checked. It is lossless
        to i32 by construction, and a narrower target truncates by the same
        rule every int→int cast already follows — no special case, and (f32 e)
        means (f32 (i32 e)) rather than an arbitrary refusal.

     2. integer → enum accepts a value that is not a declared member. raylib's
        gesture is a bitfield and an OR of flags is a legal Gesture that is no
        single member, so refusing it would refuse correct programs; and
        session.ml's printer already falls through to the number for an
        out-of-range enum, on purpose, so refusing to *construct* one while
        blessing its display would be incoherent. An Option would make every
        site unwrap for no safety bought, and a literal-only refusal would
        catch nothing — the bitfield case is a run-time value.

     3. Only an integer converts *to* an enum. Not a float, which has no
        meaning here, and not another enum: an enum-to-enum hop goes through
        (i32 x) so that both ends are written down. *)
  | _ when Hashtbl.mem ctx.env.enums name ->
    arity loc name 1 args;
    let target = resolve_name ctx.env ~seen:[] loc name in
    let a = check ctx (List.hd args) in
    (match a.Tast.ty with
     | Types.Int _ -> ()
     | other ->
       fail loc "%s converts an integer to an enum, found %s — an enum or a \
                 float goes through (i32 x) first" name
         (Types.to_string other));
    prim (Tast.Cast target) target [ a ]
  | _ when is_cast name && List.length args = 1 ->
    let target = resolve_name ctx.env ~seen:[] loc name in
    let a = check ctx (List.hd args) in
    (match a.Tast.ty with
     | Types.Enum _ -> ()
     | t when Types.is_numeric t -> ()
     | t -> fail loc "%s converts a number, found %s" name (Types.to_string t));
    prim (Tast.Cast target) target [ a ]

  (* ── ordinary calls ────────────────────────────────────────────── *)
  | _ ->
    match Hashtbl.find_opt ctx.env.fns name with
    | Some (params, ret) ->
      if List.length args <> List.length params then
        fail loc "%s takes %d argument%s, given %d" name
          (List.length params)
          (if List.length params = 1 then "" else "s")
          (List.length args);
      let args = map2_lr (fun p a -> check ctx ~want:p a) params args in
      expect loc ~want (mk loc ret (Tast.Call (name, args)))
    | None ->
      if Hashtbl.mem ctx.env.structs name || Hashtbl.mem ctx.env.unions name
      then
        fail loc
          "%s is a type — a struct value is written (%s {:field value ...})"
          name name
      else if String.contains name '/' then
        unimplemented loc
          (Printf.sprintf "the call %s into an imported package" name) 4
      else fail loc "unknown function %s" name

and is_cast name =
  Types.ikind_of_name name <> None || Types.fkind_of_name name <> None

and byte_slice ctx (a : Ast.expr) =
  check ctx ~want:(Types.Slice (Types.Int Types.U8)) a

and numeric_want want =
  match want with Some (Types.Int _ | Types.Float _) -> want | _ -> None

(* Both operands of a binary operator have one type, and there is no implicit
   widening, so one side has to decide it. Check the side that carries the most
   information first: a non-literal over a literal, and a float literal over an
   integer one, since an integer constant converts to a float and not back. *)
and binary ctx name loc ~want args =
  match args with
  | [ x; y ] ->
    let y_decides =
      (is_literal x && not (is_literal y))
      || (match x.Ast.e, y.Ast.e with
          | (Ast.Int _ | Ast.Byte _), Ast.Float _ -> true
          | _ -> false)
    in
    if y_decides then begin
      let b = check ctx ?want y in
      let a = check ctx ~want:b.Tast.ty x in
      a, b
    end else begin
      let a = check ctx ?want x in
      let b = check ctx ~want:a.Tast.ty y in
      a, b
    end
  | _ -> fail loc "%s takes two arguments" name

(* ── Declarations: pass 1, collect ─────────────────────────────────── *)

(* Constant folding, only over integers and only for defconst — enough for an
   array length like (/ screen-height cell-size). *)
let rec const_int env (e : Ast.expr) : int64 option =
  match e.Ast.e with
  | Ast.Int n -> Some n
  | Ast.Byte b -> Some (Int64.of_int b)
  | Ast.Var n -> Hashtbl.find_opt env.consts n
  (* Left to right over any number of operands, because that is how the
     checker reads the same form: an array length that type-checks as a
     product of three literals and is then not a constant would be a
     distinction with nothing behind it. [%] is still two, as it is there. *)
  | Ast.Call ({ Ast.e = Ast.Var op; _ }, x :: y :: rest) ->
    let step a b =
      match op with
      | "+" -> Some (Int64.add a b)
      | "-" -> Some (Int64.sub a b)
      | "*" -> Some (Int64.mul a b)
      | "/" when b <> 0L -> Some (Int64.div a b)
      | "%" when b <> 0L && rest = [] -> Some (Int64.rem a b)
      | _ -> None
    in
    List.fold_left
      (fun acc e ->
         match acc, const_int env e with
         | Some a, Some b -> step a b
         | _ -> None)
      (const_int env x) (y :: rest)
  | _ -> None

let collect env (decls : Ast.decl list) =
  (* One pass over every declaration kind before any of the others, because
     the tables below are per-kind — structs, unions, aliases, enums, functions
     and globals each have their own — and a collision between two of them
     would otherwise be found by LLVM, as [redefinition of function
     '@flan.item'], or not at all. A [defn item] and a [defvar item] are two
     declarations of one name and are rejected here. *)
  let claimed = Hashtbl.create 64 in
  List.iter
    (fun (d : Ast.decl) ->
       match Ast.declared_name d with
       | None -> ()
       | Some n ->
         if Hashtbl.mem claimed n then
           fail d.Ast.dloc "%s is defined twice" n;
         Hashtbl.add claimed n ())
    decls;
  (* Names first, so a struct may mention one declared below it. *)
  List.iter
    (fun (d : Ast.decl) ->
       match d.Ast.d with
       | Ast.Defstruct (n, _) ->
         Hashtbl.replace env.locs n d.Ast.dloc;
         Hashtbl.replace env.structs n { Tast.sname = n; fields = [] }
       | Ast.Defunion (n, _) ->
         Hashtbl.replace env.locs n d.Ast.dloc;
         Hashtbl.replace env.unions n { Tast.uname = n; cases = [] }
       | Ast.Defalias (n, t) -> Hashtbl.replace env.aliases n t
       | _ -> ())
    decls;
  (* Compile-time integer constants next, to a fixpoint, because an array
     length may name a constant declared below it — top-level names in a
     package are order-independent (plan.org, Modules). *)
  let fold_consts () =
    let progress = ref false in
    List.iter
      (fun (d : Ast.decl) ->
         match d.Ast.d with
         | Ast.Defconst (n, _, v) when not (Hashtbl.mem env.consts n) ->
           (match const_int env v with
            | Some i -> Hashtbl.replace env.consts n i; progress := true
            | None -> ())
         | _ -> ())
      decls;
    !progress
  in
  while fold_consts () do () done;
  let field (f : Ast.field) : Tast.field =
    { Tast.fname = f.Ast.fname; fty = resolve env f.Ast.fty }
  in
  (* Constants with no declared type are inferred from their value, which needs
     every other signature in hand — so they are deferred to a pass of their
     own below. *)
  let untyped = ref [] in
  (* Enums come first, in a pass of their own: a signature below may name one,
     and [resolve] has to find it before it resolves that signature. *)
  List.iter
    (fun (d : Ast.decl) ->
       match d.Ast.d with
       | Ast.Defenum (n, members) ->
         let names = List.map fst members in
         if List.length (List.sort_uniq compare names) <> List.length names then
           fail d.Ast.dloc "%s declares the same member twice" n;
         Hashtbl.replace env.enums n members;
         Hashtbl.replace env.locs n d.Ast.dloc
       | _ -> ())
    decls;
  List.iter
    (fun (d : Ast.decl) ->
       let loc = d.Ast.dloc in
       match d.Ast.d with
       | Ast.Package _ -> ()
       | Ast.Defenum _ -> ()
       (* Imports are gone by now: [Load] resolved them into these very decls,
          so one reaching the checker is a driver that skipped that step. *)
       | Ast.Import (alias, _) ->
         fail loc "internal: the import of %s was not resolved before checking"
           alias
       (* [Shim.expand] rewrote every one of these into a [Declare] and a
          [Defn] before [collect] ran, so one arriving here is a driver that
          skipped that step. *)
       | Ast.DeclareC (fn, _) ->
         fail loc "internal: the declare-c of %s was not expanded before checking"
           fn.Ast.name
       | Ast.Declare (fn, csym) ->
         if Hashtbl.mem env.fns fn.Ast.name then
           fail loc "%s is declared twice" fn.Ast.name;
         let params =
           List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
         in
         let ret =
           match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t
         in
         (* What may cross the boundary. A slice or a string goes as ptr+len,
            a scalar as itself; an aggregate does not go at all, because how
            one is passed differs per target and reproducing that here would
            be three calling conventions to maintain. Pass (Ptr T) instead and
            let the C shim dereference it — that is what the shim is for. *)
         let crossable what (t : Types.t) =
           match t with
           | Types.Int _ | Types.Float _ | Types.Bool | Types.Ptr _
           | Types.Enum _ | Types.Unit -> ()
           | Types.String | Types.Slice _ when what = "a parameter" -> ()
           | _ ->
             fail loc
               "%s of %s is %s, which cannot cross to C directly — pass \
                (Ptr %s) and let the shim read it" what fn.Ast.name
               (Types.to_string t) (Types.to_string t)
         in
         List.iter (crossable "a parameter") params;
         crossable "the return type" ret;
         Hashtbl.replace env.fns fn.Ast.name (params, ret);
         Hashtbl.replace env.externs fn.Ast.name csym
       | Ast.Defalias _ -> ()
       | Ast.Defstruct (n, fs) ->
         let names = List.map (fun (f : Ast.field) -> f.Ast.fname) fs in
         if List.length (List.sort_uniq compare names) <> List.length names then
           fail loc "%s declares the same field twice" n;
         let fields = List.map field fs in
         (* spec-memory.md: "Ownership is structural, not declared" — a struct
            containing a Vec is itself move-only, and freeing one recurses into
            its owning fields while (free (.items b)) is refused because it
            would leave the owner partly dead. None of that transitive
            machinery exists yet: it is the same recursive teardown [drop]
            brings, and it lands with it. Until then the field is refused at
            the declaration, where the message can say so, rather than
            accepted into a struct that copies its header on assignment and
            gives two owners one buffer. *)
         List.iter
           (fun (f : Tast.field) ->
              if Types.is_move_only f.Tast.fty then
                fail loc
                  "%s's field %s is %s, which is move-only, and a struct that \
                   owns one is move-only too — transitively, with recursive \
                   teardown and with a field that cannot be freed on its own. \
                   That rule arrives with drop (step 5 in NEXT.md); until then \
                   hold the %s in a local and pass it"
                  n f.Tast.fname (Types.to_string f.Tast.fty)
                  (Types.to_string f.Tast.fty))
           fields;
         Hashtbl.replace env.structs n { Tast.sname = n; fields }
       | Ast.Defunion (n, vs) ->
         Hashtbl.replace env.unions n
           { Tast.uname = n;
             cases = List.map (fun (v : Ast.variant) ->
               { Tast.vname = v.Ast.vname;
                 vfields = List.map field v.Ast.vfields }) vs }
       | Ast.Defn fn ->
         let params =
           List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
         in
         let ret =
           match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t
         in
         Hashtbl.replace env.fns fn.Ast.name (params, ret)
       | Ast.Defvar (n, t, _) ->
         let ty = match t with
           | Some t -> resolve env t
           | None -> fail loc "defvar %s needs a type" n
         in
         Hashtbl.replace env.globals n (ty, false)
       | Ast.Defconst (n, Some t, _) ->
         Hashtbl.replace env.globals n (resolve env t, true)
       | Ast.Defconst (n, None, v) -> untyped := (n, v) :: !untyped)
    decls;
  (* Also to a fixpoint, and for the same reason: one untyped constant may be
     defined in terms of another declared after it. A constant that still does
     not check once no progress is left has a real error, so the last round is
     run without swallowing it. *)
  let infer (_, v) =
    (check { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
      outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" } v).Tast.ty
  in
  let pending = ref (List.rev !untyped) in
  let rec settle () =
    let left =
      List.filter
        (fun ((n, _) as c) ->
           match infer c with
           | ty -> Hashtbl.replace env.globals n (ty, true); false
           | exception Loc.Error _ -> true)
        !pending
    in
    let progressed = List.length left < List.length !pending in
    pending := left;
    if progressed && left <> [] then settle ()
  in
  settle ();
  List.iter (fun c -> ignore (infer c)) !pending

(* A type that contains itself by value has no finite size. [(Ptr T)] and a
   slice are indirections and break the cycle; a fixed array does not, because
   it is inline. Caught here rather than when a backend tries to lay the type
   out or a zero value is built for it — which would not fail, it would hang. *)
let check_finite env =
  let rec walk seen name =
    if List.mem name seen then
      fail (Option.value (Hashtbl.find_opt env.locs name) ~default:Loc.unknown)
        "%s contains itself by value, so it has no size — go through (Ptr %s)"
        name name;
    let seen = name :: seen in
    match Hashtbl.find_opt env.structs name with
    | Some s -> List.iter (fun (f : Tast.field) -> ty seen f.Tast.fty) s.Tast.fields
    | None ->
      match Hashtbl.find_opt env.unions name with
      | None -> ()
      | Some u ->
        List.iter
          (fun (c : Tast.variant) ->
             List.iter (fun (f : Tast.field) -> ty seen f.Tast.fty) c.Tast.vfields)
          u.Tast.cases
  and ty seen = function
    | Types.Named n -> walk seen n
    | Types.Array (_, e) | Types.Option e -> ty seen e
    | _ -> ()
  in
  Hashtbl.iter (fun n _ -> walk [] n) env.structs;
  Hashtbl.iter (fun n _ -> walk [] n) env.unions

(* ── Declarations: pass 2, check bodies ────────────────────────────── *)

let check_fn env (fn : Ast.fn) : Tast.fn =
  let params, ret = Hashtbl.find env.fns fn.Ast.name in
  let ctx = { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
                outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false;
                owner = fn.Ast.name } in
  List.iter2
    (fun (p : Ast.field) ty ->
       if List.mem_assoc p.Ast.fname ctx.scope then
         fail p.Ast.floc "%s has two parameters named %s" fn.Ast.name p.Ast.fname;
       ignore (bind ctx p.Ast.fname ty ~assignable:false))
    fn.Ast.params params;
  let body =
    match fn.Ast.fbody with
    | [] ->
      if Types.equal ret Types.Unit then []
      else fail fn.Ast.nloc "%s returns %s but has no body" fn.Ast.name
             (Types.to_string ret)
    | body ->
      (* The last form is the return value, unless the function returns Unit,
         in which case whatever it evaluates to is discarded. *)
      let want = if Types.equal ret Types.Unit then None else Some ret in
      (* [defer] is recognised here and nowhere else, because this is the only
         place that knows a form is at the top level of the function body. Each
         one is checked in place — so it sees the scope it is written in — and
         then registered on the context; it emits nothing where it stands. *)
      let defer_here (e : Ast.expr) =
        match e.Ast.e with
        | Ast.Defer forms ->
          ctx.in_defer <- true;
          let forms = map_lr (fun d -> check ctx d) forms in
          ctx.in_defer <- false;
          let d = mk e.Ast.loc Types.Unit (Tast.Do forms) in
          ctx.defers <- d :: ctx.defers;
          Some (unit_at e.Ast.loc)
        | _ -> None
      in
      let rec go = function
        | [ last ] ->
          (match defer_here last with
           | Some u -> [ u ]
           | None -> [ check ctx ?want last ])
        | x :: rest ->
          let x = match defer_here x with Some u -> u | None -> check ctx x in
          x :: go rest
        | [] -> assert false
      in
      go body
  in
  (* Function exit runs the defers, innermost first. An explicit [return] ran
     its own (see [check]); this is the fall-off-the-end path. A trap does not
     run them — it is [noreturn] and then [unreachable] — and that is the same
     rule the bounds checks already follow. *)
  let body =
    match ctx.defers with
    | [] -> body
    | ds when Types.equal ret Types.Unit -> body @ ds
    | ds ->
      (* The result is computed before the defers run and returned after, so it
         goes through a slot rather than staying the last form. *)
      let rec split = function
        | [ last ] -> ([], last)
        | x :: rest -> let (init, last) = split rest in (x :: init, last)
        | [] -> assert false
      in
      let init, last = split body in
      let s = fresh_slot ctx ret in
      let loc = last.Tast.loc in
      init @ [ mk loc ret
                 (Tast.Let ([ (s, last) ], ds @ [ mk loc ret (Tast.Local s) ])) ]
  in
  { Tast.name = fn.Ast.name; params;
    slots = Array.of_list (List.rev ctx.slot_tys);
    snames = Array.of_list (List.rev ctx.slot_names);
    (* The same defers again, for the transfer exit path §5 describes. The
       normal path has them spliced into [body] above. *)
    ret; body; fdefers = ctx.defers; fparent = None; floc = fn.Ast.nloc }

(* A global of move-only type is refused. The dead set is per function, so two
   functions each freeing the same global is a double free nothing here could
   see; and within one function a global read does not go through [var]'s move
   path at all, so even the local case would be accepted. Rather than half a
   rule, the type is refused where it is declared. A global *Allocator* is not
   this — an allocator is a copyable opaque handle — which is what makes the
   handler-owns-the-arena shape in exhausted.flan expressible. *)
let no_move_only_global loc n (ty : Types.t) =
  if Types.is_move_only ty then
    fail loc
      "the global %s is %s, which is move-only, and ownership of a global \
       cannot be tracked: the dead set is per function, so two functions each \
       freeing it is a double free nothing would catch. Hold it in a local and \
       pass it, or hold the allocator globally instead"
      n (Types.to_string ty)

let check_global env (d : Ast.decl) : Tast.global option =
  let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
      outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" } in
  match d.Ast.d with
  | Ast.Defvar (n, _, init) ->
    let ty, _ = Hashtbl.find env.globals n in
    no_move_only_global d.Ast.dloc n ty;
    let ginit =
      match init with
      | Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc }
      | Ast.Uninit -> { Tast.e = Tast.Uninit ty; ty; loc = d.Ast.dloc }
      | Ast.Init v -> check (ctx ()) ~want:ty v
    in
    Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false }
  | Ast.Defconst (n, _, v) ->
    let ty, _ = Hashtbl.find env.globals n in
    no_move_only_global d.Ast.dloc n ty;
    (* [collect] already folded the integer constants, because an array length
       has to be known before any type resolves. Use that value here rather
       than the expression it came from: a global's initialiser has to be a
       compile-time constant, and [(/ screen-height cell-size)] is one — the
       folding pass is the only thing that knows it. *)
    let ginit =
      match Hashtbl.find_opt env.consts n, ty with
      | Some k, Types.Int kind ->
        (* Still range-checked: this path skips [check], and [in_range] is the
           only thing that rejects 300 as a u8. *)
        { Tast.e = Tast.Int (in_range d.Ast.dloc kind k, kind); ty;
          loc = d.Ast.dloc }
      | _ -> check (ctx ()) ~want:ty v
    in
    (* [env.consts] holds exactly the constants the folding pass consumed, so
       membership is the question "is this value in the program's shape?" *)
    Some { Tast.gname = n; gty = ty; ginit; gconst = true;
           gfolded = Hashtbl.mem env.consts n }
  | _ -> None

(* The entry point, plan.org: (defn main [args [string]] i32), with both the
   parameter and the return type optional. *)
let check_main env =
  match Hashtbl.find_opt env.fns "main" with
  | None -> ()   (* a library, or a file being checked on its own *)
  | Some (params, ret) ->
    let ok_params =
      match params with
      | [] -> true
      | [ Types.Slice Types.String ] -> true
      | _ -> false
    in
    if not ok_params then
      fail Loc.unknown
        "main takes no parameters or one [string], not (%s)"
        (String.concat " " (List.map Types.to_string params));
    if not (Types.equal ret Types.Unit || Types.equal ret (Types.Int Types.I32))
    then
      fail Loc.unknown "main returns i32 or nothing, not %s"
        (Types.to_string ret)

(* The environment as well as the program. A session needs it to check an
   expression typed at a REPL against the program the process is running — and
   it has to be this one rather than anything rebuilt from declarations,
   because [program] prepends the prelude and no accumulated AST contains it. *)
let program_with_env (decls : Ast.decl list) : Tast.program * env =
  let env = new_env () in
  let decls = Parse.program (Prelude.forms ()) @ decls in
  (* Before anything is collected: every (declare-c ...) becomes an ordinary
     flattened [declare] with a Flan [defn] over it, and the C that does the
     flattening comes back to be compiled into the build. Nothing below this
     line knows the form exists. *)
  let decls, cshim = Shim.expand decls in
  collect env decls;
  check_finite env;
  check_main env;
  let globals = List.filter_map (check_global env) decls in
  let fns =
    List.filter_map
      (fun (d : Ast.decl) ->
         match d.Ast.d with
         | Ast.Defn fn -> Some (check_fn env fn)
         | _ -> None)
      decls
  in
  (* The handler clauses lifted out along the way. They are ordinary functions
     from here down; nothing in the backend knows they were written inside
     something else. *)
  let fns = fns @ List.rev env.lifted in
  (* Sorted, so the emitted IR is reproducible build to build: a Hashtbl's
     fold order is not. *)
  let values name tbl =
    Hashtbl.fold (fun _ v acc -> v :: acc) tbl []
    |> List.sort (fun a b -> String.compare (name a) (name b))
  in
  let externs =
    Hashtbl.fold
      (fun name esym acc ->
         let eparams, eret = Hashtbl.find env.fns name in
         { Tast.ename = name; esym; eparams; eret } :: acc)
      env.externs []
    |> List.sort (fun (a : Tast.extern) b -> String.compare a.Tast.esym b.Tast.esym)
  in
  ({ Tast.structs = values (fun (s : Tast.structure) -> s.Tast.sname) env.structs;
     unions = values (fun (u : Tast.union) -> u.Tast.uname) env.unions;
     globals; externs; fns; cshim },
   env)

let program (decls : Ast.decl list) : Tast.program = fst (program_with_env decls)

(* One expression, checked against a program that is already running. The
   frame is empty — a REPL expression has no parameters and no enclosing
   function — so the slots it needs are whatever its own [let]s allocate. *)
let expression env (e : Ast.expr) :
  Tast.expr * Types.t array * string option array =
  let ctx =
    { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
      outer = []; in_handler = false; in_frames = None; in_defer = false; dead = []; borrow = false; owner = "<none>" }
  in
  let t = check ctx e in
  (t, Array.of_list (List.rev ctx.slot_tys),
   Array.of_list (List.rev ctx.slot_names))