diff --git a/BUILT.md b/BUILT.md
index eb889c0..635bdac 100644
--- a/BUILT.md
+++ b/BUILT.md
@@ -2124,6 +2124,33 @@ is a layout change, the same way reordering a struct's fields is.
   field at all — that is a pointer the linker has to relocate and a byte array has nowhere to put a relocation. A
   *zeroed* global is fine and needs none of it: it is the first declared case.
 
+### Recursion, and the shape `Form` will have
+
+A union that contains itself by value has no finite size, and `payload_lay`
+would recurse forever laying one out rather than failing. It does not get the
+chance: `check_finite` already walked a union's cases, so `(defunion T [Leaf
+(Node [l T r T])])` is refused with *"T contains itself by value, so it has no
+size — go through (Ptr T)"*, and so is a pair of unions that contain each
+other. Through a pointer it works, and that is the shape a `Form` has:
+
+```clojure
+(defunion Tree [Leaf (Node [l (Ptr Tree)  n i32])])
+
+(defn depth [t (Ptr Tree)] i32
+  (match (deref t)
+    Leaf 0
+    (Node l n) (+ n (depth l))))
+```
+
+### Why `match`'s fall-through is still `unreachable`
+
+The block after the last case comparison is `unreachable`, kept from the
+`Option` path. That is only sound if no reachable program can hold a tag no
+case names — and none can: `Zero` is tag 0, which is a real case; every
+construction writes a tag the checker resolved; and `uninit`, the one way to
+get bytes nobody wrote, is refused on a union for exactly this reason. The
+refusal is what pays for the `unreachable`.
+
 ### The diagnostics bug, fixed
 
 `(A {.x 1})` on a case of a union said **"unknown struct A"**, because `env` had no table of case names and could not
diff --git a/test/programs/unions.flan b/test/programs/unions.flan
index e7ec041..56ad9fb 100644
--- a/test/programs/unions.flan
+++ b/test/programs/unions.flan
@@ -36,6 +36,16 @@
     (Rect w h) (if (= w h) "square" "rect")
     (Tag name n) name))
 
+;; A union that names itself through a pointer. check_finite refuses one that
+;; contains itself by value -- the emitter would recurse forever laying it out
+;; -- and this is the shape that works instead.
+(defunion Tree [Leaf (Node [l (Ptr Tree)  n i32])])
+
+(defn depth [t (Ptr Tree)] i32
+  (match (deref t)
+    Leaf 0
+    (Node l n) (+ n (depth l))))
+
 (defn main [] i32
   ;; A case with no fields is a whole value and is written as a name.
   (println (describe Shape.Empty))
@@ -69,6 +79,14 @@
     (set v (Shape.Tag {.name "reassigned" .n 1}))
     (println (describe v)))
 
+  ;; Recursive through a pointer, which is the shape a Form has: a union that
+  ;; contains itself by value has no size and is refused, and (Ptr T) is what
+  ;; breaks the cycle. 5 + 10 + 0.
+  (let [leaf Tree.Leaf
+        mid  (Tree.Node {.l (addr leaf) .n 10})
+        top  (Tree.Node {.l (addr mid)  .n 5})]
+    (print (depth (addr top))) (println ""))
+
   ;; The structural printer, which reads only the case in hand: the other
   ;; cases' fields are not there to read.
   (print Shape.Empty) (println "")
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 2e4f81a..8a59bfa 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1657,7 +1657,7 @@ ERR@7 unexpected token: not the kind the caller was reading
        return value. *)
     let unions_out =
       "empty\ndot on the diagonal\ndot\nsquare\ntagged\nsquare\n\
-       32\n0\n-1\nin a cell\nempty\n30\nreassigned\n\
+       32\n0\n-1\nin a cell\nempty\n30\nreassigned\n15\n\
        Shape.Empty\n(Shape.Dot {.x 1.5 .y -2.5})\n\
        (Shape.Tag {.name \"printed\" .n 9})\n\
        (Cell {.id 7 .s (Shape.Rect {.w 1 .h 2})})\n"
@@ -1702,6 +1702,18 @@ ERR@7 unexpected token: not the kind the caller was reading
     (* The declaration's own refusals. A union with no cases has no value, and
        a case owning a Vec is the refusal a struct field already carries, in
        the same words and for the same reason. *)
+    (* A union that contains itself by value has no finite size, and the
+       emitter would recurse forever laying one out rather than failing. It is
+       refused where every other infinitely-sized type is, by the same walk,
+       which already traversed a union's cases. Both shapes: direct, and two
+       unions through each other. (Ptr T) breaks the cycle and is exercised in
+       the program above -- it is the shape a Form has. *)
+    refuses_src "a union that contains itself by value"
+      "(defunion T [Leaf (Node [l T  r T])])\n(defn f [t T] 0)"
+      "T contains itself by value";
+    refuses_src "two unions that contain each other by value"
+      "(defunion A [(X [b B])])\n(defunion B [(Y [a A])])\n(defn f [a A] 0)"
+      "contains itself by value";
     refuses_src "a union with no cases"
       "(defunion U [])\n(defn f [u U] 0)"
       "declares no cases";