diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 8ca995a..00450a6 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1643,6 +1643,119 @@ ERR@7 unexpected token: not the kind the caller was reading
     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";
+    (* ── Union values ───────────────────────────────────────────
+       defunion parsed and its shape was checked; naming the type and
+       constructing a value were refused as milestone 6. The program covers a
+       case with no fields, a case wider than another, a case holding a
+       string, a union in a struct, a union through a call in both directions,
+       ZII, reassignment and printing.
+
+       -O0 as well, for the reason every aggregate here gets it: a union value
+       is built in an alloca and mem2reg is exactly what would hide a store to
+       the wrong half of it. And a dev build, because every body goes behind an
+       indirection cell there and a union crosses one as a parameter and as a
+       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\
+       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"
+    in
+    outputs "unions" "programs/unions.flan" unions_out;
+    outputs ~opt:"-O0" "unions, -O0" "programs/unions.flan" unions_out;
+    outputs ~dev:true "unions, dev" "programs/unions.flan" unions_out;
+
+    (* The refusals, each by name. The first is the diagnostics bug NEXT.md
+       listed and this lane fixed: a case name written as if it were a struct
+       reported "unknown struct A", because nothing in the environment could
+       tell a case from a misspelling. It can now. *)
+    refuses_src "a union case written as a struct"
+      "(defunion U [(A [x i32])])\n(defn main [] i32 (let [v (A {.x 1})] 0))"
+      "A is a case of the union U";
+    refuses_src "a union type used as a constructor"
+      "(defunion U [(A [x i32])])\n(defn main [] i32 (let [v (U {.x 1})] 0))"
+      "a union value names the case as well as the type";
+    refuses_src "a case with fields written bare"
+      "(defunion U [(A [x i32])])\n(defn main [] i32 (let [v U.A] 0))"
+      "has fields, so it needs them";
+    (* Exhaustiveness is refused rather than defaulted: a match that fell
+       through would have to produce a value of the match's type out of
+       nothing, and the case a union grows tomorrow is the one a reader wants
+       to be told about today. *)
+    refuses_src "a match that misses a case"
+      "(defunion U [A B C])\n\
+       (defn main [] i32 (match U.A A 0 B 1))"
+      "this match is not exhaustive";
+    refuses_src "a match arm naming a case the union does not have"
+      "(defunion U [A B])\n(defn main [] i32 (match U.A A 0 B 1 Q 2))"
+      "Q is not a case of U";
+    (* All of a case's fields or none: a pattern binding some of them would be
+       reading the wrong field the moment one is inserted above it. *)
+    refuses_src "a case pattern binding the wrong number of names"
+      "(defunion U [(A [x i32  y i32])])\n\
+       (defn f [u U] i32 (match u (A x) x))"
+      "binds every field, in declaration order";
+    refuses_src "two arms for one case"
+      "(defunion U [A B])\n(defn main [] i32 (match U.A A 0 A 1 B 2))"
+      "two A arms";
+    (* 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. *)
+    refuses_src "a union with no cases"
+      "(defunion U [])\n(defn f [u U] 0)"
+      "declares no cases";
+    refuses_src "a union case that owns a Vec"
+      "(defunion U [(A [v (Vec i32)])])\n(defn f [u U] 0)"
+      "which is move-only";
+    (* At the operation, not at the type: a struct key is decided by walking
+       its fields and the struct table is not necessarily complete while a
+       type is resolving, so both are answered where the hash and equality
+       pair is emitted. A union reaches the same place. *)
+    refuses_src "a union is not a map key"
+      "(defunion U [A B])\n\
+       (defn f [m (Map U i32) k U] (put m k 1))"
+      "the payload past the case in hand is indeterminate";
+    (* A global cannot hold a case, because writing one at link time means
+       serialising the fields into the payload blob and a string field is a
+       relocation a byte array has nowhere to put. Zeroed is fine and is the
+       first declared case. Refused in the emitter, where the rest of the
+       same rule about a global's initialiser already lives, so the assertion
+       has to get that far rather than stopping at the checker. *)
+    (let name = "a global initialised with a union case" in
+     let src =
+       "(defunion U [A (B [x i32])])\n(defvar g U (U.B {.x 1}))\n\
+        (defn main [] i32 0)"
+     in
+     match
+       Emit.program
+         (Check.program (Parse.program (Reader.read_all ~file:"<unions>" src)))
+     with
+     | _ ->
+       incr failures;
+       Printf.printf "FAIL  %s\n        it was accepted\n" name
+     | exception Loc.Error (_, m) ->
+       if not (contains m "needs a byte-level encoder that does not exist")
+       then begin
+         incr failures;
+         Printf.printf "FAIL  %s\n        said: %S\n" name m
+       end);
+    (* And a zeroed one is fine, which is the other half of the same rule: it
+       is the first declared case, all bytes zero, and needs no encoder. *)
+    (let name = "a zeroed union global" in
+     match
+       Emit.program
+         (Check.program
+            (Parse.program
+               (Reader.read_all ~file:"<unions>"
+                  "(defunion U [A (B [x i32])])\n(defvar g U)\n\
+                   (defn main [] i32 (match g A 0 (B x) x))")))
+     with
+     | _ -> ()
+     | exception Loc.Error (_, m) ->
+       incr failures;
+       Printf.printf "FAIL  %s\n        refused: %S\n" name m);
+
     let signed_out = "-4\n-1\nbig is not small\nbig is large\n1\n" in
     outputs "signedness" "programs/signedness.flan" signed_out;
     outputs ~opt:"-O0" "signedness, -O0" "programs/signedness.flan" signed_out;
@@ -1907,6 +2020,29 @@ ERR@7 unexpected token: not the kind the caller was reading
         (defstruct Board [tag u8  cells [4 P]  here P  edge (Ptr P)  seen (Option i64)])\n\
         (defn main [] i32 (let [b (Board {.tag 1})] (i32 (.tag b))))\n")
       "Board" [ "tag"; "cells"; "here"; "edge"; "seen" ];
+    (* A union, through the same oracle, because its layout is the one thing
+       about it that has to be exactly right: the macro expander's Form has to
+       be the same bytes in the compiler and in the dlopened macro, and there
+       is nothing at run time that would notice a disagreement.
+
+       Two members, a tag and a blob, which is what DWARF 5's variant_part
+       would describe more precisely and lldb's C support would not read. The
+       size is the oracle's: room for the widest case at the alignment the
+       widest member of any case needs. Here that is (f64, f64) for the size
+       and f64 for the alignment, so a tag of 4 padded to 8 and 16 bytes of
+       payload -- 24. A blob sized to the *first* case, or one aligned to the
+       tag, comes out at a different number and this says so. *)
+    layout_case "DWARF offsets agree with LLVM: a union"
+      ("(defunion U [Nil (Pair [a f64  b f64]) (One [n i32])])\n\
+        (defn main [] i32 (let [u U.Nil] (match u Nil 0 _ 1)))\n")
+      "U" [ "tag"; "payload" ];
+    (* And the same union with a narrower widest case, so the payload is not a
+       constant this could have hard-coded: three i32 cases want 4-byte
+       alignment and 4 bytes of payload, which is 8 in total. *)
+    layout_case "DWARF offsets agree with LLVM: a narrow union"
+      ("(defunion N [(A [x i32]) (B [y i32]) (C [z i32])])\n\
+        (defn main [] i32 (let [n (N.A {.x 3})] (match n (A x) x _ 1)))\n")
+      "N" [ "tag"; "payload" ];
 
     (* Permuting the fields must actually move them. Asserting that the two
        orderings disagree is what makes the two cases above a test: an offset
diff --git a/test/test_flan.ml b/test/test_flan.ml
index e181819..7767c51 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1107,11 +1107,12 @@ let () =
   rejects_check "match over an enum, members written as names"
     "(defenum K [lo 0  hi 1])\n(defn f [k K] i32 (match k lo 1 hi 2))"
     ~needle:"match over the enum K is not implemented";
-  (* The old message blamed milestone 2, which was never the reason. An Option
-     still gets that answer, and still should. *)
+  (* The old message blamed milestone 2, which was never the reason, and the
+     milestone has since arrived: match now works over a declared union as
+     well, so the message names both subjects and no milestone. *)
   rejects_check "match over something that is neither"
     "(defn f [n i32] i32 (match n _ 2))"
-    ~needle:"match works on an Option at milestone 2, not on i32";
+    ~needle:"match works on an Option or a union, not on i32";
   (* A destructuring pattern in an arm's binds is a name position like any
      other. *)
   rejects_check "a pattern inside a match arm's binds"