diff --git a/TODO.org b/TODO.org
index 39f9bf6b..35c7ec6a 100644
--- a/TODO.org
+++ b/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.
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 5a8a18b8..0eedc7dc 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -2211,10 +2211,10 @@ allocator the language does not have.
 big                       18446744073709551615
 col                       :blue
 (.pos b)                  (V {.x 1.5 .y 0})
-b                         (Blob {.id 7 .name "sandy \"quoted\"" .pos (V {.x 1.5 .y 0}) .tags [ 0 42 0]})
-(slice (.tags b) 0 3)     [ 0 42 0]
+b                         (Blob {.id 7 .name "sandy \"quoted\"" .pos (V {.x 1.5 .y 0}) .tags [0 42 0]})
+(slice (.tags b) 0 3)     [0 42 0]
 (rl/get-color 0x11223344) (rl/Color {.r 17 .g 34 .b 51 .a 68})
-sim/grid                  [ [ 0 0 0 0 0 0 0 0 ...] [ 0 ... ] ...]
+sim/grid                  [[0 0 0 0 0 0 0 0 ...] [0 ...] ...]
 ```
 
 Details that are decisions rather than formatting:
@@ -2625,7 +2625,7 @@ The half the shadow stack was built for. `(:op "locals" :frame N)` answers what
 (:op "locals" :frame 0) → (:status "ok" :frame "look"
                               :locals (("n" "i64" "3") ("label" "string" "\"hello\"")
                                        ("p" "Point" "(Point {:x 1.5 :y 2.5})")
-                                       ("xs" "[3 i32]" "[ 10 20 30]") ("flag" "bool" "true"))
+                                       ("xs" "[3 i32]" "[10 20 30]") ("flag" "bool" "true"))
                               :refused (("after" "not bound yet at the point the program stopped")))
 ```
 
@@ -2706,7 +2706,7 @@ with nowhere to ask it.
 
 ```
 (:op "globals") → (:status "ok"
-                      :globals (("grid" "[4 i32]" "[ 7 5 0 0]" (0 1))
+                      :globals (("grid" "[4 i32]" "[7 5 0 0]" (0 1))
                                 ("pressure" "i64" "12" (0))
                                 ("label" "string" "\"running\"" (1)))
                       :refused () :skipped ())
diff --git a/emacs/MANUAL.md b/emacs/MANUAL.md
index a44a8dce..48d1da8d 100644
--- a/emacs/MANUAL.md
+++ b/emacs/MANUAL.md
@@ -733,7 +733,7 @@ what it wants seen, from inside its own loop, with `(watch "name" value)`:
 
 The value is rendered the way `print` renders it, so a struct, an array, a
 slice, an option or a dyn value watches as it prints: `(Pos {.x 3 .y 1.5})`,
-`[ 1 2 3]`. A string is quoted. The value is evaluated once whether or not a
+`[1 2 3]`. A string is quoted. The value is evaluated once whether or not a
 watch buffer is open.
 
 That is the whole of it. `C-c C-c` on `step` adds or removes a watched value
diff --git a/emacs/flan-inspect.el b/emacs/flan-inspect.el
index 72cc68a4..0cfc956e 100644
--- a/emacs/flan-inspect.el
+++ b/emacs/flan-inspect.el
@@ -175,7 +175,7 @@ reply without a daemon behind them, and so that this file names
             (1+ end)))))
 
 (defun flan-inspect--read-seq (s i)
-  "Read `[ V V]' at I, which is `[' — an array or a slice."
+  "Read `[V V]' at I, which is `[' — an array or a slice."
   (let ((i (1+ i)) (kids nil) (n 0) (more nil) (done nil))
     (while (not done)
       (setq i (flan-inspect--skip-space s i))
diff --git a/emacs/test-flan-cider.el b/emacs/test-flan-cider.el
index c158bdbb..1dbe3214 100644
--- a/emacs/test-flan-cider.el
+++ b/emacs/test-flan-cider.el
@@ -60,7 +60,7 @@
 ;; The whole of the worked example in docs/BUILT.md, "`C-x C-e` — evaluating
 ;; an expression", nested two deep with a string that has escaped quotes in it
 ;; and a slice at the end.
-(let* ((src "(Blob {.id 7 .name \"sandy \\\"quoted\\\"\" .pos (V {.x 1.5 .y 0}) .tags [ 0 42 0]})")
+(let* ((src "(Blob {.id 7 .name \"sandy \\\"quoted\\\"\" .pos (V {.x 1.5 .y 0}) .tags [0 42 0]})")
        (n (flan-inspect-parse src))
        (kids (plist-get n :children)))
   (test-flan--check "every field of a nested struct"
@@ -75,14 +75,14 @@
                            '(0 1 2))))
 
 ;; [ 0 42 0] — Types.Slice and Types.Array both write this.
-(let ((n (flan-inspect-parse "[ 0 42 0]")))
+(let ((n (flan-inspect-parse "[0 42 0]")))
   (test-flan--check "a sequence is a sequence" (eq (plist-get n :kind) 'seq))
   (test-flan--check "indexed from zero"
                     (equal (mapcar #'car (plist-get n :children)) '(0 1 2))))
 
 ;; [ [ 0 0] [ 1 ...] ...] — span truncation at both levels, which is what
 ;; sand's [100 [100 u32]] actually produces.
-(let* ((n (flan-inspect-parse "[ [ 0 0] [ 1 ...] ...]"))
+(let* ((n (flan-inspect-parse "[[0 0] [1 ...] ...]"))
        (kids (plist-get n :children)))
   (test-flan--check "a trailing ... is truncation, not an element"
                     (and (= (length kids) 2) (plist-get n :truncated)))
@@ -823,7 +823,7 @@ would be overwritten. Look again and re-do the edit")
   (test-flan--check "a struct round-trips through the editable spelling"
                     (funcall round "(Blob {.id 7 .name \"sandy\" .pos (V {.x 1.5 .y 0})})"))
   (test-flan--check "an array does too"
-                    (funcall round "[ 10 20 30]"))
+                    (funcall round "[10 20 30]"))
   (test-flan--check "and an option, and a nested one"
                     (funcall round "(some (V {.x 1 .y (some 2)}))")))
 
@@ -863,8 +863,8 @@ would be overwritten. Look again and re-do the edit")
                       (and (null (car d))
                            (string-match-p "does not add or rename" (cdr d))))))
 
-(let ((d (flan-inspect--diff (flan-inspect-parse "[ 1 2 3]")
-                             (flan-inspect-parse "[ 1 2 3 4]"))))
+(let ((d (flan-inspect--diff (flan-inspect-parse "[1 2 3]")
+                             (flan-inspect-parse "[1 2 3 4]"))))
   (test-flan--check "an element added is a change to the container, and refused"
                     (and (null (car d))
                          (string-match-p "3 elements and the buffer has 4" (cdr d)))))
@@ -1763,7 +1763,7 @@ would be overwritten. Look again and re-do the edit")
                                  (list :fn "main" :loc "g.flan:30:1"))
                     ;; Ordered as the daemon orders it: by the innermost frame
                     ;; that touches each one.
-                    :globals '(("grid" "[4 i32]" "[ 7 5 0 0]" (0 1))
+                    :globals '(("grid" "[4 i32]" "[7 5 0 0]" (0 1))
                                ("pressure" "i64" "12" (0))
                                ("label" "string" "\"running\"" (1)))))
        (buf (test-flan--cnr state))
diff --git a/lib/check.ml b/lib/check.ml
index 01f3e36c..76fe205c 100644
--- a/lib/check.ml
+++ b/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) =
-  no_dyn_yet loc ~into:true container
+(* A fix is spelled in the syntax of the file the mistake is in: the checker
+   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 \
-        one of them"
+       "A dyn value can see into a typed container only when its elements \
+        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) =
-  Loc.failk "check/dyn-view-lifetime" loc
-    "%s does not cross into dyn as a view here — its storage is not known \
-     to outlive the view, and a view is exactly as stale-safe as the thing \
-     it is a view of, no more and no less. A global's storage does outlive \
-     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)
+let view_not_permanent loc (e : Tast.expr) =
+  view_refusal "check/dyn-view-lifetime" loc e
+    "A dyn value can see into a typed container only when it is a global: a \
+     local, a parameter or a temporary can be gone while the dyn value still \
+     points at it"
 
 (* 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
-     element type no view can carry — a string, an i32 — the global spelling
-     is refused too, so the wrong order hands the programmer advice that
-     fails when they take it. Whichever refusal is unconditional wins. *)
+     says a global can be seen into, and for an element type no view can
+     carry — a string, an i32 — a global is refused too, so the wrong order
+     hands the programmer a reason that is false for their case. Whichever
+     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
diff --git a/lib/render.ml b/lib/render.ml
index 5cf3f33f..cbf48e54 100644
--- a/lib/render.ml
+++ b/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
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index ea488a33..73deba4a 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -555,11 +555,10 @@ static inline const char *tag_of(flan_dyn v) {
  *     bool     the word                    true / false
  *     text     bare at the top level,      hi   /   "a b"
  *              quoted and escaped inside
- *     vec      a slice's spelling          [ 1 2 3]
+ *     vec      a slice's spelling          [1 2 3]
  *
- * The leading space before every element is not a slip: it is what
- * lib/render.ml's slice loop emits and what a Flan program prints today, and
- * an acceptance test comparing the two would notice a tidier answer.
+ * A space between elements and none inside the brackets, the same as
+ * lib/render.ml's slice loop: an acceptance test compares the two.
  *
  * nil is the one tag with no typed counterpart, and it renders as `nil`.
  *
@@ -681,15 +680,15 @@ 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
-   * every element, 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
-   * insertion order, which is the only order the representation has. */
+  /* The map prints in edn's shape with the vec's spacing: a space between
+   * elements, key and value alike, so {:a 1 :b 2} sits beside the vec's
+   * [1 2 3]. Entries come out in insertion order, which is the only order
+   * the representation has. */
   case FLAN_DYN_TAG_MAP: {
     flan_obj *o = dyn_obj(v);
     int64_t i;
     /* A class instance prints its shape tag in front, Clojure's own spelling
-     * for a record: #point{ :x 1 :y 2}. The tag is not an entry, so it is
+     * for a record: #point{:x 1 :y 2}. The tag is not an entry, so it is
      * written here or it is not written at all. */
     if (o->u.v.klass != NULL) {
       emit(w, "#");
@@ -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;
   }
   }
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
index 7667650b..9d4fe1f2 100644
--- a/runtime/flan_dyn.h
+++ b/runtime/flan_dyn.h
@@ -106,7 +106,7 @@ flan_dyn flan_dyn_map_new(void);
  * is its slot count and no key a program can write collides with it. What can
  * see it is [flan_dyn_class_of], [flan_dyn_eq] (two values of different
  * classes are unequal, and an instance is never equal to a plain map) and
- * [flan_dyn_print] (an instance renders as #point{ :x 1 :y 2}).
+ * [flan_dyn_print] (an instance renders as #point{:x 1 :y 2}).
  *
  * The tag is not traced and does not have to be: an interned keyword entry is
  * immortal and is not a collector object. */
diff --git a/test/dyn_ops.c b/test/dyn_ops.c
index f6c6fe23..efea69bf 100644
--- a/test/dyn_ops.c
+++ b/test/dyn_ops.c
@@ -342,21 +342,21 @@ static void ops(void) {
     FDYN_push(nums, flan_dyn_from_i64(1));
     FDYN_push(nums, flan_dyn_from_i64(2));
     FDYN_push(nums, flan_dyn_from_i64(3));
-    prints(nums, "[ 1 2 3]");
+    prints(nums, "[1 2 3]");
     /* A text inside a structure is quoted and escaped, and bare at the top
        level. That is flan_rt.c's rule and the two have to agree, because the
        REPL parses the printed form back. */
     FDYN_push(strs, text("x"));
     FDYN_push(strs, text("a b"));
     FDYN_push(strs, text("q\"\n"));
-    prints(strs, "[ \"x\" \"a b\" \"q\\\"\\n\"]");
+    prints(strs, "[\"x\" \"a b\" \"q\\\"\\n\"]");
     /* And a vec of vecs, nested twice. */
     {
       flan_dyn outer = flan_dyn_vec_new();
       flan_dyn_root_push(&outer);
       FDYN_push(outer, nums);
       FDYN_push(outer, strs);
-      prints(outer, "[ [ 1 2 3] [ \"x\" \"a b\" \"q\\\"\\n\"]]");
+      prints(outer, "[[1 2 3] [\"x\" \"a b\" \"q\\\"\\n\"]]");
       flan_dyn_root_pop(1);
     }
     prints(flan_dyn_vec_new(), "[]");
@@ -440,14 +440,14 @@ static void view(void) {
   buf[3] = 7;
   check(num(FDYN_at(flat, flan_dyn_from_i64(3))) == 7,
         "the array's own write reaches the view — it is not a copy");
-  prints(flat, "[ 10 20 99 7]");
+  prints(flat, "[10 20 99 7]");
 
   /* Structural equality, view-aware — review's third finding. [dyn_equal]'s
      VEC arm used to read [x->len]/[x->u.v.items] regardless of kind, which
      for a view answers 0 and garbage: two views with different contents
      compared equal, a view and an equal heap vec compared unequal, and a
      map keyed by any view collided with every other view. [buf] now reads
-     [ 10 20 99 7]; [same] is a second, independent view over the identical
+     [10 20 99 7]; [same] is a second, independent view over the identical
      bytes, and [other] a view over one differing element. */
   {
     int64_t same_buf[4] = { 10, 20, 99, 7 };
@@ -1111,7 +1111,7 @@ static void classes(void) {
      A program built and never reloaded has no registry at all, and its
      instances must behave exactly as they did before any of this existed. */
   p = a_point(1, 2);
-  prints(p, "#point{ :x 1 :y 2}");
+  prints(p, "#point{:x 1 :y 2}");
   check(num(slot(p, "x")) == 1, "an unregistered class reads its slot");
   check(num(flan_dyn_len(p)) == 2, "an unregistered class has its length");
 
@@ -1125,7 +1125,7 @@ static void classes(void) {
         "a gained slot arrives as nil");
   check(num(slot(p, "x")) == 1, "a kept slot keeps its value");
   check(num(flan_dyn_len(p)) == 3, "a gained slot is counted");
-  prints(p, "#point{ :x 1 :y 2 :z nil}");
+  prints(p, "#point{:x 1 :y 2 :z nil}");
   /* And the tag survived: a migration must not turn an instance into a map. */
   check(truth(flan_dyn_eq(flan_dyn_class_of(p),
                           flan_dyn_kw((const uint8_t *)"point", 5))),
@@ -1143,7 +1143,7 @@ static void classes(void) {
   check(flan_dyn_tag(slot(p, "y")) == FLAN_DYN_TAG_NIL,
         "a lost slot reads as absent");
   check(num(slot(p, "z")) == 9, "a slot either side of a lost one is kept");
-  prints(p, "#point{ :x 1 :z 9}");
+  prints(p, "#point{:x 1 :z 9}");
 
   /* ── Gained and lost at once, and the third bump ──
      Three definitions have now been registered after the first, so the
@@ -1158,7 +1158,7 @@ static void classes(void) {
   /* The slot order is the class's, not the instance's history: a migrated
      instance has to be indistinguishable from a freshly constructed one, or
      [len], [render] and insertion order would each tell a different story. */
-  prints(p, "#point{ :z 9 :w nil}");
+  prints(p, "#point{:z 9 :w nil}");
 
   /* ── Re-registering the same list changes nothing ──
      This is what makes evaluating a whole file idempotent. If a bump
@@ -1218,7 +1218,7 @@ static void classes(void) {
                     flan_dyn_from_i64(8));
   define("point", "x\ny\nz\nzz");
   check(num(flan_dyn_len(plain)) == 2, "a plain map gains no slot");
-  prints(plain, "{ :y 7 :x 8}");
+  prints(plain, "{:y 7 :x 8}");
   check(flan_dyn_tag(flan_dyn_class_of(plain)) == FLAN_DYN_TAG_NIL,
         "a plain map has no class");
 
diff --git a/test/programs/dyn-class.flan b/test/programs/dyn-class.flan
index 5cb29f46..87f9eeb4 100644
--- a/test/programs/dyn-class.flan
+++ b/test/programs/dyn-class.flan
@@ -7,7 +7,7 @@
 ;;;; object's header and not in the entries: (length p) is the slot count, no
 ;;;; key
 ;;;; a program can write collides with it, and it shows up in exactly three
-;;;; places -- class-of, equality, and the printed form #point{ :x 1 :y 2}.
+;;;; places -- class-of, equality, and the printed form #point{:x 1 :y 2}.
 ;;;;
 ;;;; The two dispatch styles are one mechanism. A defgeneric dispatches on the
 ;;;; class of its first argument, which is Common Lisp's; a defmulti's body IS
diff --git a/test/syntax/algorithms.flan b/test/syntax/algorithms.flan
index c99ccb33..d568e002 100644
--- a/test/syntax/algorithms.flan
+++ b/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)))
-      (++ i))))
+          (-- j))
+        (++ 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)
 
diff --git a/test/syntax/algorithms.fln b/test/syntax/algorithms.fln
index 1f267d09..68ef2af2 100644
--- a/test/syntax/algorithms.fln
+++ b/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
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 0691f63c..30df8cf1 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -593,8 +593,8 @@ let () =
     (* An array literal whose elements agree is typed and one whose elements
        mix is a dyn vector; (the T e) gives any expression its type. *)
     let mixed_out =
-      "3\n301\n2.5\n18446744073709551615\n[ 10 \"Hi\"]\n[ nil 1]\n2\n3\n4\n\
-       3\n1\n9000000004\n[ :a \"b\" 3]\n\
+      "3\n301\n2.5\n18446744073709551615\n[10 \"Hi\"]\n[nil 1]\n2\n3\n4\n\
+       3\n1\n9000000004\n[:a \"b\" 3]\n\
        255\n5000000000\n5\n4.5\n2\n0\n7\n3\n3\n0\n" in
     outputs "mixed array literals and the" "programs/array-mixed.flan" mixed_out;
     outputs ~x86:true "mixed array literals and the, x86"
@@ -713,10 +713,10 @@ let () =
     let println_out =
       "plain string\nplain bytes\n42\n-7\n5\n18446744073709551615\n3.5\n\
        -0.25\ntrue\nfalse\n()\n:green\n:red\n<ptr>\n(some 0)\nnone\n\
-       (Blob {.id 7 .name \"sandy \\\"quoted\\\"\" .pos (V {.x 1.5 .y -2}) .tags [ 0 42 0]})\n\
-       [ 0 0 9 0]\n[ 0 0 0 0 0 0 0 0 ...]\n[ 0 9 0]\n\
-       (D1 {.d (D2 {.d (D3 {.d (D4 {.d (D5 {.n ...})})})})})\n[ 0 0]\n\
-       [ 0 0]\n[ 9 0]\n"
+       (Blob {.id 7 .name \"sandy \\\"quoted\\\"\" .pos (V {.x 1.5 .y -2}) .tags [0 42 0]})\n\
+       [0 0 9 0]\n[0 0 0 0 0 0 0 0 ...]\n[0 9 0]\n\
+       (D1 {.d (D2 {.d (D3 {.d (D4 {.d (D5 {.n ...})})})})})\n[0 0]\n\
+       [0 0]\n[9 0]\n"
       (* The escape buffer is 1024 and the input is 1100 x's, so this is the
          truncation: the ellipsis goes *inside* the quotes, and the count is
          spelled out rather than pasted so that a change to the buffer or to
@@ -5190,13 +5190,13 @@ level "1"
        written against did not do, and the real renderer does on purpose. The
        space is a prefix per element rather than a separator between them, so
        the open bracket is followed by one — runtime/flan_dyn.c's [render],
-       pinned by test/dyn_ops.c's own "[ 1 2 3]". And a text *nested* in a
+       pinned by test/dyn_ops.c's own "[1 2 3]". And a text *nested* in a
        container is escaped and quoted while the same text printed on its own
        is not, which is the third line here: [three] bare, ["three"] inside
        the vector. Both were red against the expectation below until this was
        corrected — on LLVM as much as on x86, because neither is a backend's
        business. *)
-    let dyn_vec_out = "4\n[ 1 2.5 \"three\" true]\n1 2.5 three true \n" in
+    let dyn_vec_out = "4\n[1 2.5 \"three\" true]\n1 2.5 three true \n" in
     outputs "dyn: a heterogeneous vector"
       "programs/dyn-vec.flan" dyn_vec_out;
     outputs ~opt:"-O0" "dyn: a heterogeneous vector, -O0"
@@ -5233,8 +5233,8 @@ level "1"
        that lost a map's keys or values frees something live and the sum
        comes out wrong. *)
     let dyn_map_out =
-      "{ :a 1 :b \"two\" :xs [ 1 2 3] :inner { :c 2.5}}\n4\n1\ntwo\n\
-       [ 1 2 3]\n2.5\nnil\ntrue\ntrue\nfalse\nnil\ntrue\n99\n5\n\
+      "{:a 1 :b \"two\" :xs [1 2 3] :inner {:c 2.5}}\n4\n1\ntwo\n\
+       [1 2 3]\n2.5\nnil\ntrue\ntrue\nfalse\nnil\ntrue\n99\n5\n\
        true\nfalse\nfalse\ntrue\n:standalone\n6\ntext key\nvec key\n\
        true\nfalse\nfalse\n600000\n"
     in
@@ -5266,11 +5266,11 @@ level "1"
        found nothing. The 100000 at the end is 50000 instances allocated
        against one live instance, well past the collector's 1 MiB floor. *)
     let dyn_class_out =
-      "#point{ :x 3 :y 4}\n2\n3\n10\ntrue\nfalse\nnil\n:point\n\
+      "#point{:x 3 :y 4}\n2\n3\n10\ntrue\nfalse\nnil\n:point\n\
        :circle\nnil\nnil\nnil\ntrue\nfalse\nfalse\ntrue\n40\n12\n5\n\
        a round thing, keyed by a string\nthe one keyed by a number\n\
        something else\nsomething else\n2\n:circle\n\
-       [ #point{ :x 10 :y 4} 99]\n[ #point{ :x 10 :y 4} 99]\n\
+       [#point{:x 10 :y 4} 99]\n[#point{:x 10 :y 4} 99]\n\
        a point\nname-of\nnil\n100000\n:point\n"
     in
     outputs "dyn: classes and dispatch" "programs/dyn-class.flan" dyn_class_out;
@@ -5589,15 +5589,15 @@ level "1"
        key. On both backends, because every one of these is a runtime call
        whose arguments the two emit separately. *)
     let slots_out =
-      "#state{ :pause false :step 3 :speed 1.5 :name \"sand\" :tag :x}\n\
-       true\n-7\n[ 1 2]\n2.5\n9\n6\n12\n3.5\ntrue\n2\n:state\n"
+      "#state{:pause false :step 3 :speed 1.5 :name \"sand\" :tag :x}\n\
+       true\n-7\n[1 2]\n2.5\n9\n6\n12\n3.5\ntrue\n2\n:state\n"
     in
     outputs "dyn: typed class slots" "programs/dyn-class-slots.flan" slots_out;
     outputs ~x86:true "dyn: typed class slots, --x86"
       "programs/dyn-class-slots.flan" slots_out;
     outputs "dyn: a package's slot type names its own class"
       "programs/dyn-class-pkg.flan"
-      "#g/seg{ :a #g/pt{ :x 1 :y 2} :b nil :tag :t}\n#pt{ :z 1}\n";
+      "#g/seg{:a #g/pt{:x 1 :y 2} :b nil :tag :t}\n#pt{:z 1}\n";
     let slot_trap ?x86 () =
       let exe = compile ?x86 "programs/dyn-slot-trap.flan" in
       List.iter
@@ -5728,11 +5728,11 @@ level "1"
        write whose dyn tag does not match the element type. The expected
        text for mode 0 was captured from the running program. *)
     let dyn_view_out =
-      "[ 10 20 30]\n999\n777\n4\n40\n\
-       [ 1 2 3 4]\n100\n400\n\
-       [ 1.5 2.5 3.5]\n9.5\n\
-       [ true false]\ntrue\n\
-       [ 111 222]\n3\n333\n"
+      "[10 20 30]\n999\n777\n4\n40\n\
+       [1 2 3 4]\n100\n400\n\
+       [1.5 2.5 3.5]\n9.5\n\
+       [true false]\ntrue\n\
+       [111 222]\n3\n333\n"
     in
     let dyn_view ?opt ?x86 () =
       let exe = compile ?opt ?x86 "programs/dyn-view.flan" in
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 6789224b..cfdf2ab8 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -2552,7 +2552,7 @@ let () =
                  one wire format, and they moved together, which is what the
                  note here used to say was still owed. *)
               ("p", "Point", "(Point {.x 1.5 .y 2.5})");
-              ("xs", "[3 i32]", "[ 10 20 30]");
+              ("xs", "[3 i32]", "[10 20 30]");
               ("flag", "bool", "true");
               (* The byte's character half, in the three shapes it has. The
                  spelling is one [lib/reader.ml]'s [read_byte] accepts, so
@@ -3108,7 +3108,7 @@ let () =
              program. *)
           let r = set "xs" "((:path (1) :code \"(+ 20 5)\"))" in
           if status r <> "ok" then fail "setting xs[1]: %s" (message r)
-          else if value r <> "[ 10 25 30]" then
+          else if value r <> "[10 25 30]" then
             fail "setting xs[1] answered %s" (value r);
 
           (* A value that does not fit is refused in the checker's own words,
@@ -3604,7 +3604,7 @@ let () =
                [grid]'s two writes are the two frames: [main] set element 1
                before calling, [inner] set element 0 after. The value is read
                out of the program's own storage, so both are in it. *)
-            [ ("grid", "[4 i32]", "[ 7 5 0 0]", [ 0; 1 ]);
+            [ ("grid", "[4 i32]", "[7 5 0 0]", [ 0; 1 ]);
               ("pressure", "i64", "12", [ 0 ]);
               ("label", "string", "\"running\"", [ 1 ]) ]
           in
@@ -4886,7 +4886,7 @@ let () =
          | Some v -> fail "watch rendered a struct as %s" v
          | None -> fail "the (watch ...) form never wrote a struct");
         (match List.assoc_opt "row" t with
-         | Some "[ 1 2 3]" -> ()
+         | Some "[1 2 3]" -> ()
          | Some v -> fail "watch rendered a slice as %s" v
          | None -> fail "the (watch ...) form never wrote a slice");
         (match List.assoc_opt "t2" t with
@@ -4894,7 +4894,7 @@ let () =
          | Some v -> fail "watch rendered a computed i64 as %s" v
          | None -> fail "the (watch ...) form never wrote a scalar");
         (match List.assoc_opt "d" t with
-         | Some "{ :a 1}" -> ()
+         | Some "{:a 1}" -> ()
          | Some v -> fail "watch rendered a dyn map as %s" v
          | None -> fail "the (watch ...) form never wrote a dyn value");
         (match List.assoc_opt "s" t with
@@ -6557,7 +6557,7 @@ let () =
             [ ("n", "i64", "3");
               ("label", "string", "\"hello\"");
               ("p", "Point", "(Point {.x 1.5 .y 2.5})");
-              ("xs", "[3 i32]", "[ 10 20 30]");
+              ("xs", "[3 i32]", "[10 20 30]");
               ("flag", "bool", "true");
               (* And the byte's character half under this backend too: the
                  spelling table is the dev runtime's, but the slot the byte
@@ -6668,8 +6668,8 @@ let () =
        the reason the inspector block above gives — a backend the break loop
        can tell apart is a backend the break loop cannot be trusted on. It was
        tellable apart: x86-64 builds an aggregate in its destination, so this
-       daemon used to answer [ 2 2 5 1] for the local and [ 3 3 5 1] for the
-       global where the LLVM one answered [ 1 1 5 1] for both.
+       daemon used to answer [2 2 5 1] for the local and [3 3 5 1] for the
+       global where the LLVM one answered [1 1 5 1] for both.
 
        The local is the half that can only be asked here. A half-built local
        is invisible to the running program — the name is not in scope until
@@ -6729,7 +6729,7 @@ let () =
           if status r <> "ok" then fail "%s half-write locals: %s" flag (said r)
           else
             (match List.filter (fun (n, _, _) -> n = "v") (triples r "locals") with
-             | [ ("v", "[4 u32]", "[ 1 1 5 1]") ] -> ()
+             | [ ("v", "[4 u32]", "[1 1 5 1]") ] -> ()
              | got ->
                fail
                  "%s: a local caught mid-assignment reads %s, not its whole \
@@ -6751,7 +6751,7 @@ let () =
               match
                 List.filter (fun (n, _, _) -> n = "colors") (triples r "globals")
               with
-              | [ ("colors", "[4 u32]", "[ 1 1 5 1]") ] -> ()
+              | [ ("colors", "[4 u32]", "[1 1 5 1]") ] -> ()
               | got ->
                 fail
                   "%s: a global caught mid-assignment reads %s, not its whole \
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 5b63acd7..76439e69 100644
--- a/test/test_flan.ml
+++ b/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"
diff --git a/test/test_repl.ml b/test/test_repl.ml
index 752b0679..95145a1c 100644
--- a/test/test_repl.ml
+++ b/test/test_repl.ml
@@ -87,11 +87,11 @@ let () =
       (* A struct, nested, with a fixed array inside it. *)
       value "a struct" "(.pos b)" "(V {.x 1.5 .y 0})";
       value "a nested struct" "b"
-        "(Blob {.id 7 .name \"sandy \\\"quoted\\\"\" .pos (V {.x 1.5 .y 0}) .tags [ 0 42 0]})";
-      value "a fixed array" "arr" "[ 0 0 9 0]";
+        "(Blob {.id 7 .name \"sandy \\\"quoted\\\"\" .pos (V {.x 1.5 .y 0}) .tags [0 42 0]})";
+      value "a fixed array" "arr" "[0 0 9 0]";
       (* A slice's length is not known until it runs, so this one renders
          through a loop rather than by unrolling. *)
-      value "a slice" "(slice (.tags b) 0 3)" "[ 0 42 0]";
+      value "a slice" "(slice (.tags b) 0 3)" "[0 42 0]";
       (* An enum's members are erased to i32 before the backend sees them, so
          the name is recovered from the checker's table. *)
       value "an enum" "col" ":blue";
diff --git a/test/test_syntax.ml b/test/test_syntax.ml
index 6b83e947..b30fb11d 100644
--- a/test/test_syntax.ml
+++ b/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 =
diff --git a/web/examples/classes.out b/web/examples/classes.out
index 2cc45bd2..5f516c60 100644
--- a/web/examples/classes.out
+++ b/web/examples/classes.out
@@ -3,7 +3,7 @@
 4
 :point
 nil
-#point{ :x 3 :y 4}
+#point{:x 3 :y 4}
 9
 something else
 exit 0
diff --git a/web/index.html b/web/index.html
index a8a8a6e8..584421ad 100644
--- a/web/index.html
+++ b/web/index.html
@@ -770,11 +770,11 @@ once, for every method; a method has no return slot; and every parameter of both
 4
 :point
 nil
-#point{ :x 3 :y 4}
+#point{:x 3 :y 4}
 9
 something else</code></pre>
 
-<p>An instance renders as <code>#point{ :x 3 :y 4}</code>, Clojure's spelling for a
+<p>An instance renders as <code>#point{:x 3 :y 4}</code>, Clojure's spelling for a
 record, and the tag is why two instances of one class compare by their slots while an
 instance is never equal to a plain map with the same entries. A dispatch that matches
 no method signals <code>NoMethod</code>, carrying the generic's name and the value
@@ -2077,10 +2077,10 @@ there too, from its tag. What comes back looks like this:</p>
 <pre><code class="sh">big                       18446744073709551615
 col                       :blue
 (.pos b)                  (V {.x 1.5 .y 0})
-b                         (Blob {.id 7 .name "sandy \"quoted\"" .pos (V {.x 1.5 .y 0}) .tags [ 0 42 0]})
-(slice (.tags b) 0 3)     [ 0 42 0]
+b                         (Blob {.id 7 .name "sandy \"quoted\"" .pos (V {.x 1.5 .y 0}) .tags [0 42 0]})
+(slice (.tags b) 0 3)     [0 42 0]
 (rl/get-color 0x11223344) (rl/Color {.r 17 .g 34 .b 51 .a 68})
-sim/grid                  [ [ 0 0 0 0 0 0 0 0 ...] [ 0 ... ] ...]</code></pre>
+sim/grid                  [[0 0 0 0 0 0 0 0 ...] [0 ...] ...]</code></pre>
 
 <p>A pointer is never followed; it renders as <code>&lt;ptr&gt;</code>. Following one
 would make the walk cycle, and dereferencing a pointer a REPL was handed is not safe.