Dyn and typed containers print as [1 2 3] and {:a 1}, a refused dyn view names the value and a dyn fix in the file's own syntax, and a dyn function whose body gives no value says so by name

TODO.org

@@ -304,9 +304,6 @@ compare bools, and a match over a bool takes true/false arms, exhaustive without
 Decided 2026-09-25: a let whose name no later statement of its block mentions prints
 flat, not as a nested block; a one-argument and/or prints as its argument.
 
-** NEXT A dyn vector prints as [1 2 3], a map as {:a 1}
-Decided 2026-09-25: no space after the opening bracket, in every renderer.
-
 ** WAIT ML-style patterns
 Held 2026-09-25 as a future direction, like the JS backend: nested destructuring,
 guards, or-patterns, literals at any depth, exhaustiveness over the nesting.

lib/check.ml

@@ -3451,11 +3451,50 @@ let view_elem (t : Types.t) : int64 option =
 let view_elem_lit loc (k : int64) =
   mk loc (Types.Int Types.I32) (Tast.Int (k, Types.I32))
 
-let view_not_yet loc (container : Types.t) (elem : Types.t) =
+(* A fix is spelled in the syntax of the file the mistake is in: the checker
-  no_dyn_yet loc ~into:true container
+   sees one AST for both, so the location's file is the only thing left that
+   says which one the reader is looking at. *)
+let fln_source (loc : Loc.t) = Filename.check_suffix loc.Loc.file ".fln"
+
+(* The two refusals below share their subject and their fix. The subject is
+   the name as written when the refused value is a bare name, so the message
+   can say [a is a [4 i64]]; anything longer is "this". The fix is the one
+   spelling that works for every container either refusal reaches, whatever
+   its element type or wherever it lives: make it a dyn value where it is
+   built, and there is no view to refuse. *)
+let view_subject (e : Tast.expr) =
+  match Loc.snippet e.Tast.loc with
+  | Some s
+    when s <> ""
+         && String.for_all
+              (fun c -> not (List.mem c [ ' '; '('; ')'; '['; ']'; '{'; '}'; '"' ]))
+              s ->
+    Some s
+  | _ -> None
+
+let view_refusal kind loc (e : Tast.expr) reason =
+  let ty = Types.to_string e.Tast.ty in
+  let fln = fln_source loc in
+  let subject, fix =
+    match view_subject e with
+    | Some n ->
+      ( Printf.sprintf "%s is a %s" n ty,
+        Printf.sprintf "Build %s as a dyn value where it is made, as in %s" n
+          (if fln then Printf.sprintf "let %s: dyn = [...]" n
+           else Printf.sprintf "(let [%s (the dyn [...])] ...)" n) )
+    | None ->
+      ( Printf.sprintf "This is a %s" ty,
+        Printf.sprintf "Build it as a dyn value where it is made, as in %s"
+          (if fln then "the(dyn, [...])" else "(the dyn [...])") )
+  in
+  Loc.failk kind loc "%s, and a dyn value is wanted here. %s. %s" subject
+    reason fix
+
+let view_not_yet loc (e : Tast.expr) (elem : Types.t) =
+  view_refusal "check/dyn-not-yet" loc e
     (Printf.sprintf
-       ". A container view carries i64, f64 or bool elements, and %s is not \
+       "A dyn value can see into a typed container only when its elements \
-        one of them"
+        are i64, f64 or bool, and these are %s"
        (Types.to_string elem))
 
 (* M2 item 3's second guard, added on review: a view's descriptor holds an
@@ -3539,20 +3578,11 @@ let rec permanent_root (e : Tast.expr) : bool =
   | Tast.Prim (Tast.Slice, [ target; _; _ ]) -> permanent_root target
   | _ -> false
 
-let view_not_permanent loc (container : Types.t) =
+let view_not_permanent loc (e : Tast.expr) =
-  Loc.failk "check/dyn-view-lifetime" loc
+  view_refusal "check/dyn-view-lifetime" loc e
-    "%s does not cross into dyn as a view here — its storage is not known \
+    "A dyn value can see into a typed container only when it is a global: a \
-     to outlive the view, and a view is exactly as stale-safe as the thing \
+     local, a parameter or a temporary can be gone while the dyn value still \
-     it is a view of, no more and no less. A global's storage does outlive \
+     points at it"
-     it: (defonce g %s ...) viewed from anywhere reads storage fixed for the \
-     process, and so does a field or an array element of one. A local, a \
-     parameter, a temporary, anything reached through a slice at any index \
-     level — even a global one, which holds only ptr+len and can point at a \
-     frame that is gone — or \
-     anything reached through a (Ptr T) is refused: the checker cannot tell \
-     a heap-durable pointer from a frame's own, and admitting one admits \
-     the other"
-    (Types.to_string container) (Types.to_string container)
 
 (* A value handed out of [f] that points into [f]'s own frame: returned (the
    last form's tails, or a [return]), or stored into a global or a field or
@@ -3860,15 +3890,15 @@ let box loc (e : Tast.expr) : Tast.expr =
      both, and they share [flan_dyn_view_flat]. *)
   (* The element check runs before the lifetime one in all three arms, and
      the order is load-bearing rather than incidental: the lifetime message
-     points at [(defonce g ...)] as the spelling that works, and for an
+     says a global can be seen into, and for an element type no view can
-     element type no view can carry — a string, an i32 — the global spelling
+     carry — a string, an i32 — a global is refused too, so the wrong order
-     is refused too, so the wrong order hands the programmer advice that
+     hands the programmer a reason that is false for their case. Whichever
-     fails when they take it. Whichever refusal is unconditional wins. *)
+     refusal is unconditional wins. *)
   | Types.Vec elem ->
     (match view_elem elem with
-     | None -> view_not_yet loc e.Tast.ty elem
+     | None -> view_not_yet loc e elem
      | Some k ->
-       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
+       if not (permanent_root e) then view_not_permanent loc e
        else dyn "flan_dyn_view_vec" [ e; view_elem_lit loc k ])
   (* A dyn view is written through by (set (at d i) x), and nothing on the
      dyn side can tell a read-only one apart, so a [[const T]] does not
@@ -3881,15 +3911,15 @@ let box loc (e : Tast.expr) : Tast.expr =
       (Types.to_string e.Tast.ty) (Types.to_string elem)
   | Types.Slice (Types.Mut, elem) ->
     (match view_elem elem with
-     | None -> view_not_yet loc e.Tast.ty elem
+     | None -> view_not_yet loc e elem
      | Some k ->
-       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
+       if not (permanent_root e) then view_not_permanent loc e
        else dyn "flan_dyn_view_flat" [ e; view_elem_lit loc k ])
   | Types.Array (n, elem) ->
     (match view_elem elem with
-     | None -> view_not_yet loc e.Tast.ty elem
+     | None -> view_not_yet loc e elem
      | Some k ->
-       if not (permanent_root e) then view_not_permanent loc e.Tast.ty
+       if not (permanent_root e) then view_not_permanent loc e
        else
          dyn "flan_dyn_view_flat"
            [ e; mk loc dyn_i64 (Tast.Int (n, Types.I64)); view_elem_lit loc k ])
@@ -14765,10 +14795,61 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn =
       let is_defer (e : Ast.expr) =
         match e.Ast.e with Ast.Defer _ -> true | _ -> false
       in
+      (* A dyn function whose value-giving form gives none — a [while], a
+         [set] — reaches [box]'s unit refusal, which can only say that () is
+         not a dyn value. Here the function is known, so the refusal is
+         restated as what went wrong with it. Only a refusal at the body's
+         own tail is: one deeper in the last form (a unit argument to a dyn
+         parameter) is about that argument and keeps its own message. *)
+      let rec tail_locs (e : Ast.expr) =
+        e.Ast.loc
+        :: (match e.Ast.e with
+            | Ast.Do es | Ast.Let (_, es) ->
+              (match List.rev es with x :: _ -> tail_locs x | [] -> [])
+            | Ast.If (_, a, b) ->
+              tail_locs a @ (match b with Some b -> tail_locs b | None -> [])
+            | _ -> [])
+      in
+      let restate_unit last (d : Loc.diag) =
+        let at (l : Loc.t) =
+          l.Loc.file = d.Loc.dloc.Loc.file && l.Loc.line = d.Loc.dloc.Loc.line
+          && l.Loc.col = d.Loc.dloc.Loc.col
+        in
+        if d.Loc.kind = "check/dyn-unit" && Types.equal ret Types.Dyn
+           && List.exists at (tail_locs last)
+        then
+          Loc.diag ~kind:"check/dyn-unit" d.Loc.dloc
+            (Printf.sprintf
+               "%s is declared to return dyn, but the last form of its body \
+                gives no value. End the body with the value to return (nil \
+                for none), or declare %s to return nothing: %s"
+               fn.Ast.name fn.Ast.name
+               (if fln_source d.Loc.dloc then
+                  Printf.sprintf "fn %s(...) -> ()" fn.Ast.name
+                else Printf.sprintf "(defn %s [...] () ...)" fn.Ast.name))
+        else d
+      in
+      (* The refusal arrives either raised or, under recovery, recorded on
+         [env.recovered] while checking goes on; both are restated. *)
+      let check_last last =
+        let env = ctx.env in
+        let before = env.recovered in
+        let r =
+          try check ctx ?want last
+          with Loc.Error d -> Loc.raise_diag (restate_unit last d)
+        in
+        let rec fresh = function
+          | l when l == before -> l
+          | d :: rest -> restate_unit last d :: fresh rest
+          | [] -> []
+        in
+        env.recovered <- fresh env.recovered;
+        r
+      in
       let rec go = function
         | [ last ] ->
           ctx.defer_ok <- true;
-          [ (if is_defer last then check ctx last else check ctx ?want last) ]
+          [ (if is_defer last then check ctx last else check_last last) ]
         | x :: rest ->
           ctx.defer_ok <- true;
           let x = check ctx x in

lib/render.ml

@@ -353,7 +353,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis
              let v =
                { Tast.e = Tast.Prim (Tast.At, [ e; i32 i ]); ty = t; loc }
              in
-             lit " " :: render c (depth + 1) v))
+             (if i = 0 then [] else [ lit " " ]) @ render c (depth + 1) v))
       in
       [ do_ ((lit "[" :: parts)
              @ (if Int64.to_int n > shown then [ lit " ..." ] else [])
@@ -377,6 +377,16 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis
             Tast.Prim (Tast.At, [ local sv e.Tast.ty; local iv (Types.Int Types.I32) ]);
           ty = t; loc }
       in
+      (* A space between elements and none after the bracket: [1 2 3], the
+         runtime's spelling for a dyn vector. The empty literal is the else
+         arm because an If needs one; it writes nothing. *)
+      let sep =
+        unit_
+          (Tast.If
+             ({ Tast.e = Tast.Prim (Tast.Gt, [ local iv (Types.Int Types.I32); i32 0 ]);
+                ty = Types.Bool; loc },
+              lit " ", lit ""))
+      in
       let step =
         unit_
           (Tast.Set
@@ -391,7 +401,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis
               [ lit "[";
                 unit_
                   (Tast.While
-                     (cond, lit " " :: render c (depth + 1) elem, [ step ]));
+                     (cond, sep :: render c (depth + 1) elem, [ step ]));
                 lit "]" ])) ]
     (* The one type this walk does not walk. Every other arm is here because a
        Flan value carries no header and only the compiler knows what it is; a

runtime/flan_dyn.c

@@ -557,9 +557,8 @@ static inline const char *tag_of(flan_dyn v) {
  *              quoted and escaped inside
  *     vec      a slice's spelling          [1 2 3]
  *
- * The leading space before every element is not a slip: it is what
+ * A space between elements and none inside the brackets, the same as
- * lib/render.ml's slice loop emits and what a Flan program prints today, and
+ * lib/render.ml's slice loop: an acceptance test compares the two.
- * an acceptance test comparing the two would notice a tidier answer.
  *
  * nil is the one tag with no typed counterpart, and it renders as `nil`.
  *
@@ -681,10 +680,10 @@ static void render(dyn_sink w, flan_dyn v, int depth, int nested) {
     emit_n(w, kw_bytes(k), k->len);
     return;
   }
-  /* The map prints in edn's shape with the vec's spacing: a space before
+  /* The map prints in edn's shape with the vec's spacing: a space between
-   * every element, key and value alike, so { :a 1 :b 2} sits beside the vec's
+   * elements, key and value alike, so {:a 1 :b 2} sits beside the vec's
-   * [ 1 2 3] rather than inventing a fourth convention. Entries come out in
+   * [1 2 3]. Entries come out in insertion order, which is the only order
-   * insertion order, which is the only order the representation has. */
+   * the representation has. */
   case FLAN_DYN_TAG_MAP: {
     flan_obj *o = dyn_obj(v);
     int64_t i;
@@ -697,7 +696,7 @@ static void render(dyn_sink w, flan_dyn v, int depth, int nested) {
     }
     emit(w, "{");
     for (i = 0; i < o->len; i++) {
-      emit(w, " ");
+      if (i > 0) emit(w, " ");
       render(w, o->u.v.items[i * 2], depth + 1, 1);
       emit(w, " ");
       render(w, o->u.v.items[i * 2 + 1], depth + 1, 1);
@@ -710,7 +709,7 @@ static void render(dyn_sink w, flan_dyn v, int depth, int nested) {
     int64_t i, n = o->kind == OBJ_VIEW ? view_len(NULL, 0, "print", o) : o->len;
     emit(w, "[");
     for (i = 0; i < n; i++) {
-      emit(w, " ");
+      if (i > 0) emit(w, " ");
       if (o->kind == OBJ_VIEW)
         render(w, view_box(o->u.view.elem,
                         (const uint8_t *)view_base(o)
@@ -818,12 +817,12 @@ static void say_render(sayer *s, flan_dyn v, int depth) {
     }
     say_puts(s, "{");
     for (i = 0; i < o->len && s->n < s->cap - 8; i++) {
-      say_puts(s, " ");
+      if (i > 0) say_puts(s, " ");
       say_render(s, o->u.v.items[i * 2], depth + 1);
       say_puts(s, " ");
       say_render(s, o->u.v.items[i * 2 + 1], depth + 1);
     }
-    say_puts(s, i < o->len ? " ...}" : "}");
+    say_puts(s, i == o->len ? "}" : i > 0 ? " ...}" : "...}");
     return;
   }
   default: {
@@ -832,7 +831,7 @@ static void say_render(sayer *s, flan_dyn v, int depth) {
     if (depth >= 2) { say_puts(s, "[...]"); return; }
     say_puts(s, "[");
     for (i = 0; i < n && s->n < s->cap - 8; i++) {
-      say_puts(s, " ");
+      if (i > 0) say_puts(s, " ");
       if (o->kind == OBJ_VIEW)
         say_render(s,
                    view_box(o->u.view.elem,
@@ -842,7 +841,7 @@ static void say_render(sayer *s, flan_dyn v, int depth) {
       else
         say_render(s, o->u.v.items[i], depth + 1);
     }
-    say_puts(s, i < n ? " ...]" : "]");
+    say_puts(s, i == n ? "]" : i > 0 ? " ...]" : "...]");
     return;
   }
   }

test/syntax/algorithms.flan

@@ -26,15 +26,28 @@
   {:where (ordered? $t)}
   (let [i 1
         length (length coll)]
-    (while (and (< i length))
+    (while (< i length)
       (let [j i]
         (while (and (> j 0)
                     (< (at coll j) (at coll (dec j))))
           (let [temp (at coll j)]
             (set (at coll j) (at coll (dec j)))
             (set (at coll (dec j)) temp))
-          (-- j)))
+          (-- j))
-      (++ i))))
+        (++ i)))))
+
+(defn insertion-sort-dyn [coll dyn] ()
+  (let [i 1
+        length (length coll)]
+    (while (< i length)
+      (let [j i]
+        (while (and (> j 0)
+                    (< (at coll j) (at coll (dec j))))
+          (let [temp (at coll j)]
+            (set (at coll j) (at coll (dec j)))
+            (set (at coll (dec j)) temp))
+          (-- j))
+        (++ i)))))
 
 (defn main [] i32 0)
 

test/syntax/algorithms.fln

@@ -36,7 +36,7 @@ fn insertion-sort(coll: [$t]) -> () where ordered?($t)
       --(j)
     ++(i)
 
-fn insertion-sort-dyn(coll)
+fn insertion-sort-dyn(coll) -> ()
   let i = 1
   let length = length(coll)
   while i < length

test/test_flan.ml

@@ -1522,12 +1522,12 @@ let () =
     "(defonce v (Vec string) (vec-new string))\n\
      (defn take [d dyn] i32 1)\n\
      (defn main [] i32 (take v))"
-    ~needle:"does not cross into dyn yet";
+    ~needle:"only when its elements are i64, f64 or bool";
   rejects_check "an i32 element is not one of the view's three"
     "(defonce v (Vec i32) (vec-new i32))\n\
      (defn take [d dyn] i32 1)\n\
      (defn main [] i32 (take v))"
-    ~needle:"does not cross into dyn yet";
+    ~needle:"only when its elements are i64, f64 or bool";
   (* A typed (Map K V) is unrelated to item 3 and keeps its own refusal. *)
   rejects_check "a typed Map still refuses into dyn"
     "(defonce m (Map i64 i64) (map-new i64 i64))\n\
@@ -1544,7 +1544,7 @@ let () =
                  lifetime one"
     "(defn take [d dyn] i32 1)\n\
      (defn main [] i32 (let [v (vec-new string)] (take v)))"
-    ~needle:"does not cross into dyn yet";
+    ~needle:"only when its elements are i64, f64 or bool";
   (* ── The lifetime guard, added on review ─────────────────────────
      A local, a parameter and a temporary all answer false to
      [permanent_root], and each gets the same message rather than "cannot be
@@ -1552,16 +1552,16 @@ let () =
   rejects_check "a local Vec does not view into dyn — its frame ends"
     "(defn take [d dyn] i32 1)\n\
      (defn main [] i32 (let [v (vec-new i64)] (take v)))"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   rejects_check "a Vec parameter does not view into dyn"
     "(defn take [d dyn] i32 1)\n\
      (defn give [v (Vec i64)] i32 (take v))\n\
      (defn main [] i32 0)"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   rejects_check "a fixed array local does not view into dyn"
     "(defn take [d dyn] i32 1)\n\
      (defn main [] i32 (let [a (array 4 i64)] (take a)))"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   (* A slice cut from a global is permanent; the same slice expression
      rebound to a local first loses the trace back to it and is refused —
      conservative rather than wrong, and the message says what does work. *)
@@ -1573,7 +1573,7 @@ let () =
     "(defonce xs [3 i64])\n\
      (defn take [d dyn] i32 1)\n\
      (defn main [] i32 (let [s (slice xs 0 3)] (take s)))"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   (* An element of a global is permanent only when the global is an ARRAY.
      An array's elements are inside the global's own storage; a slice's are
      not — a global [[T]] holds ptr+len and nothing more, and what they
@@ -1590,7 +1590,7 @@ let () =
     "(defonce sv [(Vec i64)])\n\
      (defn take [d dyn] i32 1)\n\
      (defn main [] i32 (take (at sv 0)))"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   (* [(at g i j)] is ONE typed node holding both indices, not two nested
      ones, so a guard that reads the target's type alone sees level zero and
      nothing after it. These two rows pin the multi-index spelling on both
@@ -1605,7 +1605,7 @@ let () =
     "(defonce g [2 [[3 i64]]])\n\
      (defn take [d dyn] i32 1)\n\
      (defn main [] i32 (take (at g 0 1)))"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   (* A Vec behind a Ptr is refused even though some Ptrs really are
      heap-durable — the checker cannot tell this one from a Ptr taken off a
      local, and admitting one admits the other. *)
@@ -1613,7 +1613,7 @@ let () =
     "(defn take [d dyn] i32 1)\n\
      (defn use [p (Ptr (Vec i64))] i32 (take (deref p)))\n\
      (defn main [] i32 0)"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   (* A bracket *literal* is not a typed container yet, and where a dyn is
      wanted it builds the runtime's own vec instead — the lowering the map
      literal's values ride on, and what makes {:xs [1 2]} mean what it
@@ -3651,10 +3651,10 @@ let () =
     "grid" ~ty:"[2 [3 u8]]" ~zeroed:false;
   rejects_check "a three-element array-fill defonce is the dyn reading"
     "(defonce xs (array-fill [3] (i64 1))) (defn f [] ())"
-    ~needle:"does not cross into dyn as a view here";
+    ~needle:"only when it is a global";
   rejects_check "and its element type is asked about first"
     "(defonce grid (array-fill [2 3] 255)) (defn f [] ())"
-    ~needle:"does not cross into dyn yet";
+    ~needle:"only when its elements are i64, f64 or bool";
   (* A defconst is not a second path to it: its value is what the linker
      writes into the image, and a fill is a loop. *)
   rejects_check "array-fill is not a constant's value"

test/test_syntax.ml

@@ -547,6 +547,72 @@ let () =
       fail "twin files: %s" d.Loc.dmsg
   | exception e -> fail "twin files: %s" (Printexc.to_string e)
 
+(* ── A refusal's fix is spelled in the file's own syntax, and compiles ── *)
+
+let refused name text needles =
+  let f = Filename.concat scratch name in
+  write f text;
+  match Front.checked f with
+  | _ -> fail "%s checked" name
+  | exception (Loc.Error d | Loc.Errors [ d ]) ->
+    List.iter
+      (fun n ->
+         if not (Test_support.contains d.Loc.dmsg n) then
+           fail "%s: wanted %S in: %s" name n d.Loc.dmsg)
+      needles
+  | exception e -> fail "%s: %s" name (diag_text e)
+
+let checks name text =
+  let f = Filename.concat scratch name in
+  write f text;
+  match Front.checked f with
+  | _ -> ()
+  | exception e -> fail "%s does not check: %s" name (diag_text e)
+
+let () =
+  let poke_fln = "fn poke(coll) -> dyn\n  coll[0] = 99\n  coll\n\n" in
+  let poke_flan = "(defn poke [coll] dyn (set (at coll 0) 99) coll)\n" in
+  (* A typed local is not a global, so no dyn value may see into it. *)
+  refused "view-local.fln"
+    (poke_fln ^ "fn main() -> ()\n  let a: [4 i64] = [6 2 4 9]\n  poke(a)\n")
+    [ "a is a [4 i64], and a dyn value is wanted here";
+      "a local, a parameter or a temporary";
+      "as in let a: dyn = [...]" ];
+  refused "view-local.flan"
+    (poke_flan ^ "(defn main [] () (let [a (array 4 i64)] (poke a)))\n")
+    [ "a is a [4 i64]"; "as in (let [a (the dyn [...])] ...)" ];
+  refused "view-temp.flan"
+    (poke_flan ^ "(defn main [] () (poke (array 4 i64)))\n")
+    [ "This is a [4 i64]"; "as in (the dyn [...])" ];
+  (* An unannotated literal is [4 i32], whose elements no view carries. *)
+  refused "view-elem.fln"
+    (poke_fln ^ "fn main() -> ()\n  let d = [6 2 4 9]\n  poke(d)\n")
+    [ "d is a [4 i32]"; "only when its elements are i64, f64 or bool, and these are i32";
+      "as in let d: dyn = [...]" ];
+  (* The fix both of them name. *)
+  checks "view-fix.fln"
+    (poke_fln ^ "fn main() -> ()\n  let d: dyn = [6 2 4 9]\n  poke(d)\n  poke(the(dyn, [1 2]))\n");
+  checks "view-fix.flan"
+    (poke_flan
+     ^ "(defn main [] () (let [a (the dyn [6 2 4 9])] (poke a)) (poke (the dyn [1 2])))\n");
+  (* A dyn function whose body ends in a while gives no value. *)
+  let loop_fln ret tail =
+    "fn f(coll) -> " ^ ret ^ "\n  let i = 1\n  while i < 3\n    ++(i)\n" ^ tail
+    ^ "\nfn main() -> ()\n  f(1)\n"
+  in
+  refused "unit-tail.fln" (loop_fln "dyn" "")
+    [ "f is declared to return dyn, but the last form of its body gives no value";
+      "fn f(...) -> ()" ];
+  refused "unit-tail.flan"
+    "(defn f [coll] dyn (let [i 1] (while (< i 3) (++ i))))\n(defn main [] () (f 1))\n"
+    [ "f is declared to return dyn"; "(defn f [...] () ...)" ];
+  checks "unit-tail-nil.fln" (loop_fln "dyn" "  nil\n");
+  checks "unit-tail-unit.fln" (loop_fln "()" "");
+  (* A unit argument deeper in the last form is about that argument. *)
+  refused "unit-arg.flan"
+    "(defn g [x dyn] dyn x)\n(defn f [coll] dyn (g (println 1)))\n(defn main [] () (f 1))\n"
+    [ "() does not box into dyn" ]
+
 (* ── Both directions of an import, on both backends ────────────────── *)
 
 let run_both path want =