The flow analysis is repealed: ownership lives in the types, the allocator, and the dev runtime

lib/check.ml

@@ -289,20 +289,6 @@ type ctx = {
      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 *data type* 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
@@ -541,9 +527,8 @@ let tyvar_of (t : Types.t) = match t with Types.Var v -> Some v | _ -> None
    double-frees. [copyable?] is the opt-out, exactly as Rust's [T: Copy] is.
 
    In the body this means a generic may not use a parameter twice without
-   declaring [copyable?]: [(defn twice [x $t] $t (+ x x))] is refused, which
+   declaring [copyable?]. Since the repeal this gates the structural rules
-   is right — correct at [i32], a double read of a moved value at [(Vec i32)],
+   only — what a struct, union or pool may own — not any use of a binding.
-   and the checker cannot tell which until it substitutes.
 
    A [Var] only ever survives the abstract pass. Inside an instantiation
    [env.subst] has made everything concrete, so this is [Types.is_move_only]
@@ -1368,7 +1353,7 @@ let invented_ctx env ret =
   { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
     defers = []; outer = []; outer_what = None; in_frames = None; loops = []; tail = false;
     in_defer = false; defer_ok = false; defer_block = "a nested form";
-    dead = []; borrow = false; owner = "<none>" }
+    owner = "<none>" }
 
 (* The address of field [i] of the struct the pointer in slot [p] points at. *)
 let field_addr_of loc sty fty p i =
@@ -1687,24 +1672,11 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e'
   | Ast.While (label, c, body) ->
     (* The condition is part of the loop even though it is written outside the
-       braces: emit puts it in the header block, so it is re-evaluated at the
+       braces — emit puts it in the header block, so it is re-evaluated at the
-       top of every trip, and a condition that gives a value away frees it once
+       top of every trip — but it stays outside [in_loop], because a [break]
-       per trip. So it is held to the loop's rule on moves and to nothing else
+       in a condition still means the enclosing loop and a [defer] there is
-       the loop changes: it stays outside [in_loop], because a [break] in a
+       still the outer block's. *)
-       condition still means the enclosing loop and a [defer] there is still
-       the outer block's, but its moves are diffed against the same dead set.
-       [dotimes]' count and a [loop]'s initial values are checked outside this
-       regime on purpose: they are evaluated exactly once, before the first
-       trip, so giving one away there is no more than giving it away before
-       the loop. *)
-    let before = ctx.dead in
-    let outer = List.map (fun (_, b) -> b.slot) ctx.scope in
     let c = check ctx ~want:Types.Bool c in
-    moved_across_iterations ctx ~before ~outer
-      "this while condition moves a value that was bound outside the loop, and \
-       the condition is evaluated again at the top of every trip, so the second \
-       one would use what the first gave away. Move it out of the loop, or \
-       test something the loop does not give away";
     let body = in_loop ctx ?label (fun () ->
       scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
     in
@@ -1951,13 +1923,10 @@ and var ctx loc ~want name =
   | _ ->
     match lookup ctx name with
     | Some b ->
-      if move_only ctx.env.tvpreds b.bty then
-        moved ~ty:b.bty 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, _) ->
-        if Types.is_move_only ty then global_borrow ctx loc name ty;
         expect loc ~want (mk loc ty (Tast.Global name))
       | None ->
         match Hashtbl.find_opt ctx.env.cases name with
@@ -2003,95 +1972,16 @@ and var ctx loc ~want name =
            | None -> captured ctx loc name;
          Loc.failk "check/unknown-name" loc "unknown name %s" name)
 
-(* Reading a move-only local. Every read is a move unless the site said it was
+(* What remains of spec-memory.md's ownership section after the repeal of
-   a borrow, which is the conservative direction: passing one to a function,
+   2026-09-18 is entirely in the types: move-only decides what may be copied,
-   binding it, returning it and [free]ing it are all moves and all reach here,
+   the struct/union/pool rules below decide what may own what, and the
-   and the handful of operations that only look at a container say so. *)
+   allocator's capability decides what a free means at run time. Which frees
-and moved ?ty ctx loc name slot =
+   run, and in what order, is the program's own business — the same contract
-  (match List.assoc_opt slot ctx.dead with
+   Odin ships with — and the dev build's generation words are the net under
-   | Some where ->
+   it. The flow analysis that used to live here (a per-function dead set, a
-     fail loc
+   borrow flag over container reads, a loop-iteration diff) tracked use-after-
-       "%s was moved at %s and cannot be used again — %s is move-only, so \
+   move and double-free statically; it was repealed rather than repaired when
-        binding, passing or returning one transfers ownership and the source \
+   its holes proved structural. See spec-memory.md, "The repeal". *)
-        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)
-       (match ty with Some t -> Types.to_string t | None -> "a Vec") name
-   | None -> ());
-  if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead
-
-(* Reading a move-only *global*, which is the same fork as [moved] with the
-   other answer: a global is never moved out of, so a site that would have
-   taken ownership is refused rather than recorded.
-
-   The rule this enforces is one sentence — reading a move-only global is
-   always a borrow. It is sound for a reason that does not generalise to
-   locals: the lifetime question, which ownership tracking exists to answer,
-   has a constant answer here. A global lives as long as the process, so
-   nothing may free it and nothing needs to; there is no frame whose exit it
-   could outlive and no second owner to disagree with. What would break the
-   argument is exactly one thing — someone taking ownership — and that is a
-   move, and every move reaches this function because [ctx.borrow] is false
-   everywhere except the operations that said they only look.
-
-   So the dead set is not consulted and not extended. A global cannot be dead:
-   two functions reading the same one are both borrowing it, which is why the
-   per-function dead set that the declaration site used to argue from was
-   never the obstacle it looked like. It could not track a global's ownership;
-   with this rule there is no ownership to track.
-
-   Mutation is not a move and is not refused. [push], [put] and [set] all take
-   their target through [borrowed], so a global (Vec u8) is filled and grown in
-   place, and the aliasing that raises — a push that reallocates invalidating a
-   slice into the same Vec — is the programmer's, exactly as it is for a local
-   (spec-memory.md, "Borrowing", and the note on [as-slice] below). Globals get
-   no rule locals do not have: the dev build's generation word lives on the Vec
-   and traps on a stale slice whether the Vec is a global or not. *)
-and global_borrow ctx loc name (ty : Types.t) =
-  if not ctx.borrow then
-    (* The last clause is conditional, because [clone] stopped being offerable
-       for one of these. A global whose elements own storage is admitted — a
-       move-only global starts zeroed and this one is no different — but
-       cloning it is refused, on the grounds that a bytewise copy is an alias
-       under a name that promises independence. Offering it anyway would send a
-       reader to a second refusal, and there is no other route to an
-       independent copy: the region owns the graph, and [free-all] is the only
-       thing that releases any of it. *)
-    fail loc
-      "%s is %s, which is move-only, and a global of one is only ever \
-       borrowed: its lifetime is the process's, so nothing may take ownership \
-       of it, and this site would. A free through the new owner would leave \
-       every other reader of %s pointing at released memory. Read and mutate \
-       it where it is — (len %s), (at %s i), (push %s x), (set (at %s i) x) \
-       — or take a view with (as-slice %s) or a pointer with (addr %s)%s"
-      name (Types.to_string ty) name name name name name name name
-      (if region_only ctx.env ty then
-         ". There is no independent copy of this one: its elements own \
-          storage, so a clone would alias rather than copy and is refused"
-       else
-         Printf.sprintf
-           ", or an independent copy with (clone %s), which is the one of \
-            these that something else may own" name)
-
-(* 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
 
 (* [defer_ok] is granted again before *every* form, not once before the block:
    [check] withdraws it as it starts, so granting it once would let the first
@@ -2170,7 +2060,7 @@ and check_fn ctx ~want loc (params : string list) body =
       scope = []; defers = []; outer = ctx.scope;
       outer_what = Some "an fn"; in_frames = None; loops = []; tail = false;
       in_defer = false; defer_ok = false; defer_block = "a nested form";
-      dead = []; borrow = false; owner = ctx.owner }
+      owner = ctx.owner }
   in
   List.iter2
     (fun n t -> ignore (bind fctx n t ~assignable:false)) params pts;
@@ -2244,7 +2134,7 @@ and check_handler_bind ctx ?want loc clauses body =
             the enclosing one. *)
          let hctx =
            { env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = [];
-             scope = []; defers = []; outer = ctx.scope; outer_what = Some "a handler"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" }
+             scope = []; defers = []; outer = ctx.scope; outer_what = Some "a handler"; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; 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.
@@ -2422,53 +2312,24 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
    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
+(* What a loop still contributes to checking after the repeal is scoping, not
-   this is the one place the dead set cannot answer on its own: the second
+   ownership: the entry below is what [break] and [continue] resolve against,
-   iteration would use what the first moved, and a set that is merged once at
+   and the defer_block name is what makes a [defer] in here refused as "a loop
-   the end of the body sees one move, not two. So it is a rule rather than an
+   body" — it would fire once at function exit rather than once per iteration,
-   inference, stated as one. *)
+   and the message says so. [fresh] and the iteration move-diff that used it
-and in_loop ctx ?label ?entry ?(fresh = []) f =
+   are gone with the flow analysis. *)
-  let outer_slots =
+and in_loop ctx ?label ?entry f =
-    List.filter (fun s -> not (List.mem s fresh))
-      (List.map (fun (_, b) -> b.slot) ctx.scope)
-  in
-  let before = ctx.dead in
   (* The loop goes on the stack before the body is checked and comes off after,
      so a [break] inside it can see it and one outside it cannot. *)
   let loops = ctx.loops in
-  (* [fresh] is a [loop]'s own names. They are bound before the entry is pushed
-     — their initial values are evaluated once, outside — but [recur] writes
-     every one of them on the way round, so the next iteration never sees what
-     this one gave away and the rule below is not about them. *)
   ctx.loops <- (match entry with Some e -> e | None -> Lloop label) :: loops;
-  (* Named so that a defer written in here is refused as "a loop body" rather
-     than as a nested form: the reason is specific — it would fire once at
-     function exit rather than once per iteration — and the message says it. *)
   let blocker = ctx.defer_block in
   ctx.defer_block <- "a loop body";
   let r = f () in
   ctx.defer_block <- blocker;
   ctx.loops <- loops;
-  moved_across_iterations ctx ~before ~outer:outer_slots
-    "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";
   r
 
-(* The rule a loop adds to the move checker, in one place because two forms
-   need it and they need it for the same reason. Everything that runs more
-   than once runs against the dead set it left behind last time: a slot that
-   was live on the way in and is dead on the way out was given away by code
-   that is about to run again, and the second run would be using what the
-   first one released. Slots bound inside the repeated region are not in
-   [outer] and are not the question — they are born again every trip. *)
-and moved_across_iterations ctx ~before ~outer why =
-  List.iter
-    (fun (slot, where) ->
-       if (not (List.mem_assoc slot before)) && List.mem slot outer then
-         fail where "%s" why)
-    ctx.dead
-
 (* Which loop a [break] or a [continue] means, as a count of loops outwards
    from the innermost — which is what [Tast.Break] carries and what [emit]
    indexes. Refuses three things, each by its own reason: nothing to break out
@@ -2606,7 +2467,7 @@ and check_loop ctx ?want loc bs body =
        is therefore monomorphic, and every other caller hands it a list. *)
     let tbody =
       match
-        in_loop ctx ~entry:(Lrecur names) ~fresh:(List.map fst binds) (fun () ->
+        in_loop ctx ~entry:(Lrecur names) (fun () ->
           [ scoped ctx (fun () ->
               (* The body's last form is the loop's tail, which is the only
                  place a [recur] may stand. [block] distributes it. *)
@@ -2704,15 +2565,7 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     let t = branch ctx (fun () -> in_tail (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 data type 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 = branch ctx (fun () -> in_tail (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 =
@@ -2721,9 +2574,6 @@ and check_if ctx ?(tail = false) ?want loc c t e =
       | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
     in
     let e = branch ctx (fun () -> in_tail (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
@@ -3030,13 +2880,6 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   let want = ref want in
   let seen = Hashtbl.create 8 in
   let 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 data type 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) ->
@@ -3047,28 +2890,20 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
             if Hashtbl.mem seen c then
               fail a.Ast.aloc "this match has two %s arms" c;
             Hashtbl.add seen c ());
-         ctx.dead <- before;
+         branch ctx (fun () ->
-         let arm =
+           let binds =
-           branch ctx (fun () ->
+             List.map
-             let binds =
+               (fun (n, ty) -> bind ctx n ty ~assignable:false) binds
-               List.map
+           in
-                 (fun (n, ty) -> bind ctx n ty ~assignable:false) binds
+           (* Every arm is the tail, exactly as an [if]'s two arms are.
-             in
+              Restored here because checking the scrutinee withdrew it. *)
-             (* Every arm is the tail, exactly as an [if]'s two arms are.
+           ctx.tail <- tail;
-                Restored here because checking the scrutinee withdrew it. *)
+           let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
-             ctx.tail <- tail;
+           if !want = None && body.Tast.ty <> Types.Never then
-             let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
+             want := Some body.Tast.ty;
-             if !want = None && body.Tast.ty <> Types.Never then
+           { Tast.acase = ctor; binds; abody = [ body ] }))
-               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;
   (* Exhaustiveness is refused, not defaulted. A match that silently fell
      through would have to produce a value of the match's type out of nothing,
      and there is no such value for most types; and the case a data type grows
@@ -3161,7 +2996,7 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
          "%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
+    let target = 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
@@ -3993,7 +3828,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; x ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = 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
@@ -4021,7 +3856,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; n ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target 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 ]))
@@ -4064,7 +3899,7 @@ and named_call ctx ~want loc name args =
   | "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 target = check ctx target in
        let elem = vec_elem loc "as-slice" target.Tast.ty in
        let lo, hi =
          match rest with
@@ -4087,10 +3922,12 @@ and named_call ctx ~want loc name args =
                                  (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
+  (* spec-memory.md's first release point. Since the repeal, what it consumes
-     any other move does — the source binding is dead afterwards and using it
+     it consumes at run time only: nothing marks the binding dead, so a second
-     is a compile error — which is the rule that already makes a double free
+     [free] or a read after this one type-checks and misbehaves at run time —
-     unrepresentable, so [free] needs no analysis of its own. *)
+     the allocator aborts on a double free it can see, and the dev build's
+     generation word traps a stale read. That is the Odin contract: free is a
+     thing you write, and writing it twice is yours to not do. *)
   | "free" ->
     arity loc name 1 args;
     let target = check ctx (List.hd args) in
@@ -4166,7 +4003,7 @@ and named_call ctx ~want loc name args =
        (* Checked once, then dispatched on what it turned out to be: checking
           it inside a guard as well would allocate the target's slots twice and
           evaluate whatever it was written as twice. *)
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let a = allocator_arg ctx loc rest in
        (match target.Tast.ty with
         (* The refusal that did *not* come down with the type-level ones, and
@@ -4294,7 +4131,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; x ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "insert" target.Tast.ty in
        let x = check ctx ~want:elem x in
        let hty = Types.Handle elem in
@@ -4344,7 +4181,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; h ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "resolve" target.Tast.ty in
        let h = check ctx ~want:(Types.Handle elem) h in
        (match h.Tast.ty with
@@ -4400,7 +4237,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; h ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "release" target.Tast.ty in
        let h = check ctx ~want:(Types.Handle elem) h in
        (match h.Tast.ty with
@@ -4425,7 +4262,7 @@ and named_call ctx ~want loc name args =
      quiet wrong answer this whole type exists to remove. *)
   | "live" ->
     arity loc name 1 args;
-    let target = borrowed ctx (List.hd args) (fun () -> check ctx (List.hd args)) in
+    let target = check ctx (List.hd args) in
     ignore (pool_elem loc "live" target.Tast.ty);
     let n = rt loc (Types.Int Types.I64) "flan_pool_live" [ target; here loc ] in
     expect loc ~want (mk loc index_ty (Tast.Prim (Tast.Cast index_ty, [ n ])))
@@ -4444,7 +4281,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; i ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let elem = pool_elem loc "pool-handle" target.Tast.ty in
        let i = check ctx ~want:index_ty i in
        let hty = Types.Handle elem in
@@ -4510,7 +4347,7 @@ and named_call ctx ~want loc name args =
     arity loc name 3 args;
     (match args with
      | [ target; k; v ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "put" target.Tast.ty in
        let k = check ctx ~want:kt k in
        let v = check ctx ~want:vt v in
@@ -4549,7 +4386,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "get" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred, and the placeholder is [None] rather than [Unit]: this
@@ -4607,7 +4444,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "map-remove!" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred exactly as [get] is, and with [None] for the same reason:
@@ -4668,7 +4505,7 @@ and named_call ctx ~want loc name args =
     arity loc name 4 args;
     (match args with
      | [ target; cur; k; v ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "map-next!" target.Tast.ty in
        let cur = check ctx ~want:(Types.Ptr (Types.Int Types.I64)) cur in
        let k = check ctx ~want:(Types.Ptr kt) k in
@@ -4692,7 +4529,7 @@ and named_call ctx ~want loc name args =
     arity loc name 2 args;
     (match args with
      | [ target; k ] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        let kt, vt = map_kv loc "has-key?" target.Tast.ty in
        let k = check ctx ~want:kt k in
        (* Deferred, and the placeholder is a [bool] — the form a condition
@@ -4967,7 +4804,7 @@ and named_call ctx ~want loc name args =
   | "len" ->
     arity loc name 1 args;
     let target = List.hd args in
-    let a = borrowed ctx target (fun () -> check ctx target) in
+    let a = check ctx target in
     (match a.Tast.ty with
      | Types.Array _ | Types.Slice _ | Types.String ->
        prim Tast.Len index_ty [ a ]
@@ -4993,7 +4830,7 @@ and named_call ctx ~want loc name args =
   | "at" ->
     (match args with
      | target :: idx when idx <> [] ->
-       let target = borrowed ctx target (fun () -> check ctx target) in
+       let target = check ctx target in
        (match target.Tast.ty with
         | Types.Vec _ ->
           let p, elem = vec_at ctx loc target idx in
@@ -5208,7 +5045,7 @@ and named_call ctx ~want loc name args =
        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 a = check ctx target in
     (* ── The allow-list, and what it takes to get on it ───────────────
        plan.org names [println] as the one compiler-provided exception — it
        "selects a structural printer at each concrete instantiation" — and
@@ -6081,7 +5918,7 @@ let collect env (decls : Ast.decl list) =
      run without swallowing it. *)
   let infer (_, v) =
     (check { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
-      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" } v).Tast.ty
+      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "<none>" } v).Tast.ty
   in
   let pending = ref (List.rev !untyped) in
   let rec settle () =
@@ -6204,7 +6041,7 @@ let check_union_members env =
 let rec 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false;
+                outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form";
                 owner = fn.Ast.name } in
   List.iter2
     (fun (p : Ast.field) ty ->
@@ -6323,10 +6160,12 @@ and check_generic env (fn : Ast.fn) =
    checking a function. *)
 let () = check_fn_ref := check_fn
 
-(* A global of move-only type is legal, and what makes it legal is [var]'s
+(* A global of move-only type is legal. Before the repeal what made it legal
-   refusal rather than anything here: reading one is always a borrow, so no
+   was a flow rule — reading one was always a borrow, so nothing could take
-   function can take it, and none can free it. See [global_borrow] for why that
+   or free it. That rule is gone with the rest of the flow analysis: a global
-   one sentence is enough where a general ownership model would not be.
+   Vec may now be handed to a function, bound, or freed, and keeping its
+   process-long lifetime honest is the program's business, on the same terms
+   as every other free.
 
    What this pass still decides is how such a global may be *started*, and the
    answer is zeroed and nothing else. A zeroed Vec is a real empty Vec — null
@@ -6405,7 +6244,7 @@ let no_union_init env loc n what (v : Tast.expr) =
 
 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" } in
+      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "<none>" } in
   match d.Ast.d with
   | Ast.Defvar (n, _, init) ->
     let ty, _ = Hashtbl.find env.globals n in
@@ -6668,7 +6507,7 @@ 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 = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" }
+      outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; owner = "<none>" }
   in
   let t = check ctx e in
   (t, Array.of_list (List.rev ctx.slot_tys),

test/test_acceptance.ml

@@ -1958,17 +1958,11 @@ let () =
        pointer-width. Two reasons, both named, neither a function value. *)
     refuses "a user-written allocator" "programs/user-allocator.flan"
       "is no longer what is missing";
-    (* Move-only, spec-memory.md. Each of these would otherwise be a double
+    (* Move-only, spec-memory.md, since the repeal: the three fixtures that
-       free or a use-after-free at run time, and each is refused at the second
+       were refused here — a use after a pass, a double free, a move inside a
-       use with the first one's location in the message. *)
+       loop — now compile, and what they do at run time is the allocator's and
-    refuses "a Vec used after it was passed" "programs/vec-moved.flan"
+       the dev build's to catch. They are kept as programs (the double-free
-      "was moved at";
+       one is what the sanitize sweep watches) but no longer as refusals. *)
-    refuses "a Vec freed twice" "programs/vec-double-free.flan"
-      "double free unrepresentable";
-    (* The one case the dead set cannot answer on its own: merged once at the
-       end of the body it counts one move, not two. *)
-    refuses "a Vec moved inside a loop" "programs/vec-moved-in-loop.flan"
-      "the next iteration would use what this one gave away";
     (* let has no type annotation, so with no element type and no expectation
        there is nothing to infer from — and guessing is the alternative. *)
     refuses "vec-new with nothing saying what of" "programs/vec-untyped.flan"
@@ -2537,11 +2531,6 @@ ERR@7 unexpected token: not the kind the caller was reading
     refuses_src "map-new with nothing to say what it maps"
       "(defn main [] i32 (let [m (map-new)] (free m)) 0)"
       "nothing here says what (map-new) maps";
-    (* A map is move-only like a Vec, and the refusal names the type that was
-       moved rather than saying "a Vec" whatever it was. *)
-    refuses_src "a map used after it was moved"
-      "(defn main [] i32 (let [m (map-new i32 i32)] (free m) (put m 1 2)) 0)"
-      "cannot be used again";
     (* ── Data type values ───────────────────────────────────────────
        defdata parsed and its shape was checked; naming the type and
        constructing a value were refused as milestone 6. The program covers a

test/test_flan.ml

@@ -1078,26 +1078,11 @@ let () =
     ~needle:"cannot be cloned";
 
   (* ── A move-only global ─────────────────────────────────────────────
-     Legal now, and legal because of one rule: reading one is always a borrow.
+     Legal, started zeroed, and since the repeal of the flow analysis it is
-     The accepted side is programs/vec-global.flan, which has to run to say
+     ownable like anything else: passing, binding and freeing one all
-     anything; these are the four things the rule refuses, and between them
+     type-check, and the process-long lifetime is the program's to keep. The
-     they are the whole of it.
+     accepted side is programs/vec-global.flan. What is still refused about
-
+     one is declaration-shaped, below. *)
-     The first two are the rule itself. Ownership is what may not be taken, and
-     the two ways to take it — hand the global to something that owns its
-     parameter, or bind it to a local that owns it — are the same refusal at
-     the read, because that is where a move would have been recorded for a
-     local. [free] is the third of them and reaches it the same way: it does
-     not borrow its target, so nothing special had to be written for it. *)
-  rejects_check "passing a global Vec to a function"
-    "(defvar g (Vec u8)) (defn eat [v (Vec u8)] () (free v)) (defn f [] () (eat g))"
-    ~needle:"only ever borrowed";
-  rejects_check "freeing a global Vec"
-    "(defvar g (Vec u8)) (defn f [] () (free g))"
-    ~needle:"only ever borrowed";
-  rejects_check "binding a global Vec to a local"
-    "(defvar g (Vec u8)) (defn f [] () (let [v g] (free v)))"
-    ~needle:"only ever borrowed";
   (* And the two declaration shapes. A computed initialiser would have to run
      before main, which is a path [Emit.const] does not have and which
      [x86.ml] deliberately leaves out of a reload module; a defconst could
@@ -1224,14 +1209,7 @@ let () =
   rejects_check "a labelled break may not leave a loop"
     "(defn f [] () (while :o true (loop [i 0] (break :o))))"
     ~needle:"no value to give";
-  (* A while's condition runs once per trip, so it lives under the same rule
+  accepts "a while condition is an ordinary expression"
-     as the body: what it gives away, it gives away again next time round.
-     Before this was checked the program below compiled and aborted in free(). *)
-  rejects_check "a while condition may not move what the loop is standing on"
-    "(defn eat [v (Vec i32)] bool (do (free v) true)) \
-     (defn f [] () (let [v (vec-new i32)] (while (eat v) (break))))"
-    ~needle:"evaluated again at the top of every trip";
-  accepts "a condition that only looks at what it tests is fine"
     "(defn f [] () (let [v (vec-new i32)  n 0] \
        (while (and (< n 10) (> (len v) 0)) (set n (+ n 1))) (free v)))";
   rejects_check "loop takes no label"
@@ -2687,16 +2665,12 @@ let () =
     ~needle:"is not a type variable of f"
     "(defn f [a i32] i32 {:where (ordered? $t)} a)";
 
-  (* Move-only by default, which is the other half of the where clause and the
+  (* Move-only by default still decides the structural rules for a $t — what
-     one with no Odin counterpart: Odin has no move semantics, so its $T never
+     may own one — but since the repeal a double use of a binding is not
-     has to answer. The prior art is Rust's T: Copy, and the difference is
+     checked, so both of these are accepted with and without the clause. *)
-     that copyable? is a question the compiler answers rather than a trait a
+  accepts "a type variable is usable twice without copyable?"
-     user implements. Conservative in the safe direction — move is the
-     stricter rule, so assuming it can only refuse a valid program. *)
-  rejects_check "a type variable is move-only until it says otherwise"
-    ~needle:"cannot be used again"
     "(defn twice [a $t b (Fn [$t $t] $t)] $t (b a a))";
-  accepts "and copyable? is the opt-out"
+  accepts "and copyable? is still a clause a signature may state"
     "(defn twice [a $t b (Fn [$t $t] $t)] $t {:where (copyable? $t)} (b a a))";
 
   (* The allow-list, and it has two members. println over a type variable is