Ownership is not transitive yet, so refuse the three shapes that assume it is

spec-memory.md says ownership is structural: a struct containing a Vec is
itself move-only, free recurses into owning fields, and a field cannot be
freed on its own. None of that machinery exists — it is the recursive teardown
drop brings — and the move rule as written covered only the types Vec appears
in directly. Three ways past it, each of which hands out a second owner of one
buffer:

A struct field of Vec type. The struct copies its header on assignment and
nothing records a move.

A global of Vec type. The dead set is per function, so two functions each
freeing it is a double free nothing could see, and a global read does not go
through the move path at all — even the one-function case was accepted. Half a
rule is worse than none, so the type is refused where it is declared. A global
Allocator is not this and stays legal: an allocator is a copyable handle, and
it is what makes a handler that owns the arena expressible.

A Vec of a Vec. The runtime is type-erased and copies elements bytewise, so
clone would duplicate inner headers rather than copying what they own and free
would drop their buffers. Shipping the shallow answer under the deep name was
the alternative.

All three name drop as what they wait on.

Also: match arms shared one dead set, so `(match o (Some k) (free v) None
(free v))` reported the second arm as a use after the first arm's move — a
legal program refused, the same case that was already fixed for `if`. Arms are
alternatives, so each starts from the state before the match and the union
survives the join.

And a Vec reaching declare-c now says what to pass instead. It was already
refused, by the shim generator's catch-all for a type it does not know; the
reason it is refused is that handing a header that owns storage to C hands out
an owner, and that is worth saying at the declaration.

lib/check.ml

@@ -226,7 +226,23 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
      | "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 ] -> Types.Vec (resolve env ~seen a)
+     | "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
@@ -994,6 +1010,13 @@ and check_match ctx ?want loc scrutinee arms =
   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) ->
@@ -1009,14 +1032,24 @@ and check_match ctx ?want loc scrutinee arms =
              fail a.Ast.aloc
                "%s is not a case of Option — the cases are Some and None" c
          in
-         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 ] }))
+         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 \
@@ -2247,8 +2280,29 @@ let collect env (decls : Ast.decl list) =
          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;
-         Hashtbl.replace env.structs n
-           { Tast.sname = n; fields = List.map field fs }
+         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;
@@ -2406,12 +2460,29 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
        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 }
@@ -2421,6 +2492,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
     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

lib/shim.ml

@@ -217,6 +217,15 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
        declare (Ptr T) and say which"
       what
   | Ast.Tmap _ -> fail loc "%s is a map, which has no C representation" what
+  (* A Vec owns its storage, so handing its header to C hands out an owner and
+     there is no rule for what C would then be allowed to do with it. The
+     elements cross the way any other run of elements does. *)
+  | Ast.Tapp ("Vec", _) ->
+    fail loc
+      "%s is a Vec, which owns its storage — handing its header to C hands out \
+       an owner. Pass (as-slice v) as (Ptr T) and (len v), the same shape a \
+       slice crosses in"
+      what
   | Ast.Tfn _ ->
     fail loc "%s is a function type, and a C callback is not implemented" what
   | Ast.Tapp (n, _) ->

test/programs/vec-global.flan

@@ -0,0 +1,9 @@
+;;;; A global of move-only type. The dead set is per function, so two functions
+;;;; each freeing this is a double free nothing here could see — and a global
+;;;; read does not go through the move path at all, so even the one-function
+;;;; case would be accepted. Half a rule is worse than none, so the type is
+;;;; refused where it is declared. A global *Allocator* is a different thing
+;;;; and is allowed: an allocator is a copyable opaque handle.
+(defvar everything (Vec i32))
+
+(defn main [] i32 0)

test/programs/vec-in-struct.flan

@@ -0,0 +1,9 @@
+;;;; spec-memory.md: "Ownership is structural, not declared" — a struct
+;;;; containing a Vec is itself move-only, transitively, with recursive
+;;;; teardown, and with a field that cannot be freed on its own. None of that
+;;;; machinery exists: it is the same recursive teardown `drop` brings, and it
+;;;; lands with it. Accepting the field meanwhile would give a struct that
+;;;; copies its header on assignment two owners of one buffer.
+(defstruct Builder [buf (Vec u8)])
+
+(defn main [] i32 0)

test/programs/vec-of-vec.flan

@@ -0,0 +1,10 @@
+;;;; A Vec of a Vec is representable and would be wrong. The runtime is
+;;;; type-erased: it copies and releases elements bytewise, so `clone` would
+;;;; duplicate the inner headers instead of copying what they own, and `free`
+;;;; would drop their buffers on the floor. spec-memory.md makes clone a deep
+;;;; copy and makes free recurse structurally into owning fields; recursive
+;;;; teardown is what `drop` brings, and this is refused until it does rather
+;;;; than shipping the shallow answer under the deep name.
+(defn rows [xs (Vec (Vec i32))] i32 0)
+
+(defn main [] i32 0)

test/programs/vec-to-c.flan

@@ -0,0 +1,8 @@
+;;;; A Vec cannot cross to C. The shim flattens a struct that crosses, and a
+;;;; Vec is not a struct anyone should flatten: it owns storage, and handing
+;;;; its header to C hands out an owner. It falls to the same aggregate
+;;;; refusal every other non-scalar declare-c parameter gets, which is the
+;;;; point — nothing special was needed and nothing special was added.
+(declare-c vec-sum [v (Vec i32)] i32 "vec_sum")
+
+(defn main [] i32 0)

test/test_acceptance.ml

@@ -809,6 +809,21 @@ let () =
        there is nothing to infer from — and guessing is the alternative. *)
     refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
       "write the element type";
+    (* The three shapes ownership is not transitive through yet. Each is
+       refused where it is declared, naming drop as what it waits on, rather
+       than accepted into a path that would copy a header and hand out a
+       second owner. *)
+    refuses "a struct field that owns a Vec" "programs/vec-in-struct.flan"
+      "a struct that owns one is move-only too";
+    refuses "a global Vec" "programs/vec-global.flan"
+      "the dead set is per function";
+    refuses "a Vec of a Vec" "programs/vec-of-vec.flan"
+      "copies and releases elements bytewise";
+    (* And it does not cross to C: the shim would flatten a header that owns
+       storage. Refused by the shim generator, where the message can say what
+       to pass instead. *)
+    refuses "a Vec crossing to C" "programs/vec-to-c.flan"
+      "handing its header to C hands out an owner";
 
     (* ── wasm32 (NEXT.md, deferred item 6) ──────────────────────────────
        The second target, and the reason sand-headless imports no raylib. What