The two cases the tests did not cover, and one leak of a permission

A type-changing (map f) is the case into's single shadowed element name
would break if the shadowing were a trick rather than the language's
rule; it is not, because each stage is a fresh slot at its own type, and
into.flan now runs an i32 source into a (Vec f32) to say so.

A move-only accumulator carried round by recur is the shape BUILT.md
pitches the form on and was untested. It works, and recur.flan now
carries a Vec three times round and answers with it.

block's empty-body arm returned before the loop that distributes the
tail, so (do) in a tail position left ctx.tail set for whatever was
checked next. Latent rather than live — every consumer sets it
immediately before use, and the leaking form is always Unit-typed — but
it is one line to close and the invariant is easier to state closed.

Also the PORTING.md line listing loop/recur among the things with no
customer: it was built, and the half of that finding that still stands is
tail calls, which were not.

BUILT.md

@@ -3058,7 +3058,9 @@ is. So `into` collects, and a reducing macro of the same shape is a separate for
   in that position should borrow — `into.flan`'s does — and the day `drop` exists this stops being a question.
 - **One element name throughout**, shadowed by each `(map f)` stage: `(let [x (f x)] ...)`. A `let` binding's value is
   checked before its name is bound, so the initialiser reads the outer `x` — that is the language's rule, not an
-  accident, and `bind`'s `x~2` debug suffix exists precisely so a debugger does not lie about which is which.
+  accident, and `bind`'s `x~2` debug suffix exists precisely so a debugger does not lie about which is which. A
+  **type-changing** `map` is the case this most plausibly breaks and it does not: each stage is a fresh slot at the
+  stage's own type, and `into.flan` runs an `i32` source into a `(Vec f32)` to say so.
 
 ### What the prelude's macro limits cost, exactly
 
@@ -3111,6 +3113,9 @@ it: the machinery was already there, and the question `recur` asks — *may this
 - **`recur` rebinds every name at once.** The new values go into temporaries and are written afterwards, so
   `(recur y x)` swaps. Interleaved writes would give `y y`, and `recur.flan` asserts the swap for exactly that
   reason.
+- **A move-only accumulator goes round.** `(loop [acc (vec-new i32) i 0] ... (recur acc (+ i 1)))` is the shape the
+  form exists for, and it is the one the move tracker had to be taught about (below). `recur.flan` carries a `Vec`
+  round three iterations and answers with it.
 
 `tast.ml` said a `While` the checker *invents* contains no jumps, because the depths would be minted against a stack
 it is not on. `check_loop`'s `While` is the exception, and it is the exception because it is pushed on `ctx.loops`

NEXT.md

@@ -115,7 +115,9 @@ abandoned frame leaving half-written state behind; rollback is what finishes tha
 **What `PORTING.md` says NOT to build, with evidence:** escaping closures (one capture site, fixed by one parameter),
 `Handle`/pools, `Result`/`try`, `handler-case`, `loop`/`recur` and tail calls, user allocators, structural typing —
 **none has a customer in that code**. (`Handle` and the pool were built anyway, and on the other reason: they are the
-gate on classes. The finding stands and is why they were built small — see [`BUILT.md`](BUILT.md).) And **generics is not the blocker** there either: the element-changing maps are
+gate on classes. The finding stands and is why they were built small — see [`BUILT.md`](BUILT.md). `loop`/`recur` was
+built too, and the finding stands there as well: what it is not is **tail calls**, which are still not built and still
+have no customer.) And **generics is not the blocker** there either: the element-changing maps are
 five-line load-time loops. That last one hangs on a design decision the report states flatly — whether the game's
 state holds fixed arrays or `Vec`s.
 

lib/check.ml

@@ -1367,7 +1367,9 @@ and borrowed ctx (a : Ast.expr) f =
    [let] is the case the relaxation exists for. *)
 and block ctx ?want ?(defer_ok = false) loc body =
   match body with
-  | [] -> expect loc ~want (unit_at loc)
+  (* Withdrawn here too. An empty body has no last form to be the tail, so
+     leaving the permission set would hand it to whatever is checked next. *)
+  | [] -> ctx.tail <- false; expect loc ~want (unit_at loc)
   | _ ->
     (* A block's tail is its last form and nothing else. Callers that must not
        pass one on need do nothing: [check] withdrew it before they were

test/programs/into.flan

@@ -35,6 +35,9 @@
   (set builds (+ builds 1))
   (slice xs 0 (len xs)))
 
+(defn wide [x i32] f32 (f32 x))
+(defn bigf? [x f32] bool (> x 2.5))
+
 (defn show [v [i32]] ()
   (dotimes [i (len v)] (print (at v i)) (print " "))
   (println ""))
@@ -71,6 +74,16 @@
     (free v)
     (free src))
 
+  ;; A type-changing map: the chain's element name is rebound at the new type
+  ;; by each stage, and the push sees the destination's element type. One name,
+  ;; shadowed — a let binding's value is checked before its name is bound, so
+  ;; each stage reads the stage before it.
+  (let [xs [1 2 3 4]
+        v (into xs (vec-new f32) (map wide) (filter bigf?))]
+    (dotimes [i (len v)] (print (at v i)) (print " "))
+    (println "")                                 ; 3 4
+    (free v))
+
   ;; A source that is a call is bound once, so it is made once however many
   ;; elements come out of it.
   (let [xs [1 2 3 4]

test/programs/recur.flan

@@ -81,6 +81,18 @@
                (recur (+ i 1) (+ acc hit))))))
   (println "")                                  ; 4
 
+  ;; A move-only accumulator, carried round by recur and answered with. This
+  ;; is the shape the form exists for: no mutable local, no sentinel flag, and
+  ;; the Vec is the loop's value. recur writes every name on the way round, so
+  ;; the "moves a value bound outside the loop" rule is not about acc.
+  (let [v (loop [acc (vec-new i32)  i 0]
+            (if (= i 3)
+              acc
+              (do (push acc i) (recur acc (+ i 1)))))]
+    (dotimes [i (len v)] (print (at v i)))
+    (println "")                                ; 012
+    (free v))
+
   ;; A match arm is a tail too.
   (print (loop [i 0  acc 0]
            (match (step i)

test/test_acceptance.ml

@@ -131,13 +131,13 @@ let () =
        rather than running out of stack. The swap line is the other — recur
        rebinds every name at once, and interleaved writes would print 1. *)
     outputs "loop and recur" "programs/recur.flan"
-      "10\n2\n21\n8\n10000000\n64\n012\n0\n4\n6\n";
+      "10\n2\n21\n8\n10000000\n64\n012\n0\n4\n012\n6\n";
     (* into. The count of pulls is the assertion a unit test cannot make: one
        pass, one call per element per stage it reaches, and no intermediate
        collection anywhere. The two show lines either side of it are the same
        source transformed in two orders, which have to differ. *)
     outputs "into" "programs/into.flan"
-      "7 8 9 \n2 4 6 8 10 12 \n4 8 12 \n21\n6 2 4 \n3 1 2 \n2 4 \n1\n";
+      "7 8 9 \n2 4 6 8 10 12 \n4 8 12 \n21\n6 2 4 \n3 1 2 \n3 4 \n2 4 \n1\n";
     (* The prelude's slice algorithms. Every assertion here is over an input a
        wrong implementation fails: unsorted with duplicates, negatives and an
        odd length; a reverse-sorted slice; and a sort of a subslice whose