diff --git a/BUILT.md b/BUILT.md
index d3bb2f3..35a4d5d 100644
--- a/BUILT.md
+++ b/BUILT.md
@@ -2116,6 +2116,169 @@ What remains at 18 ns is the type erasure itself: a non-inlinable call into the
 calls to the pair. That is the trade `spec-memory.md` chose deliberately — "It is type-erased on purpose… No generics
 are involved, and none are needed" — and monomorphisation is what would buy it back, at the cost the spec declined.
 
+## Unions, and the tag they carry
+
+`defunion` parsed and its shape was checked long before this; naming the type (`check.ml:312`) and constructing a
+value (`:1075`) were both refused as milestone 6. They are not any more.
+
+### It is closer than the milestone number suggested, and the reason is `Option`
+
+`Tast.arm` already carried `acase` (a case name) and `binds` (the slots a payload binds to). That is union shape,
+built and exercised, because **`Option` is a two-case union wearing a special coat** and `match` over it worked
+already. So `check_match` grew a second *subject* rather than a second path: one function decides which case each arm
+names and what type each name it binds has, and everything after it — the dead-set join across alternatives, the
+result type, the exhaustiveness check — is the code that was there.
+
+`Option` was **not** desugared into a declared union, and that is deliberate: `Option` is generic and no declared
+union is. The coat is the part that cannot be taken off until generics exist.
+
+A union is `Types.Named` exactly as a struct is. One case in `Types.t` covers both, and *which table the name is in*
+is the only thing that tells them apart. That is what let a union be a field, a parameter, a return type, a slot and a
+copy without a single one of those paths learning that unions exist.
+
+### The layout, which is the part that has to be exactly right
+
+```
+%"U"       = type { i32, [k x iA] }
+%"U.Case"  = type { the case's fields, in declaration order }
+```
+
+A tag, then room for the largest case, with `A` the alignment the *widest member of any case* needs and `k` the size
+rounded up to it. Writing the payload as an array of `iA` rather than of `i8` is what makes LLVM align it without an
+explicit `align` on a type — and it is what makes the whole thing
+
+```c
+struct { int tag; union { ... } u; }
+```
+
+byte for byte. **That agreement is the point.** A macro is `[Form] -> Form`, so `Form` has to be the same bytes in
+the compiler and in the `dlopen`ed macro, and nothing at run time would notice a disagreement.
+
+The tag is an `i32` and not an `i8`. With an 8-byte payload alignment the two cost the same, and `i32` is what a C
+`enum` field is — the spelling the macro lane will have to write by hand on the other side of the boundary.
+
+Both the union and one struct per case are emitted as *named* LLVM types, so every reader geps rather than computing
+byte offsets of its own. Construction is a `store` of the tag and a `store` of the case struct through a gep into the
+payload; `match` is a `load` of the tag and a gep the other way. There is one function that knows how a payload is
+read — `case_field_addr` — because there are two readers: a `match` arm's binds and the structural printer.
+
+The layout goes through the same oracle the DWARF section uses: LLVM's own answer for the emitted type, read back as a
+constant-folded `ptrtoint`. Two unions are checked, one whose widest case is a pair of `f64` and one whose cases are
+all `i32`, so the payload size and alignment cannot be constants the test agreed with by accident. The `Shape` in
+`test/programs/unions.flan` was checked against clang's answer for the same declaration in C: 32 bytes aligned 8 with
+the payload at offset 8, and 40/8 for a struct holding one.
+
+### The surface
+
+```clojure
+(defunion Shape
+  [Empty
+   (Dot  [x f64  y f64])
+   (Rect [w i32  h i32])
+   (Tag  [name string  n u8])])
+
+(Shape.Rect {.w 3 .h 3})     ; a value: the type and the case, then the fields
+(Shape.Rect {.w 3})          ; ZII, exactly as in a struct literal — .h is 0
+Shape.Empty                  ; a case with no fields is a whole value, not a call
+
+(match s
+  Empty        "empty"
+  (Dot x y)    "a dot"       ; positional, in declaration order
+  (Rect w h)   "a rect"
+  (Tag name n) name)
+```
+
+**Construction is qualified and a pattern is bare.** The two are not inconsistent: at a constructor nothing says which
+union is meant, and at a pattern the scrutinee's type already does. The qualified spelling is accepted in a pattern
+too, since that is how the value was written and writing it again should not be an error. Two unions may therefore
+share a case name, and that is not refused — refusing it would be a restriction with no mechanism behind it.
+
+Construction needed **no change to `parse.ml`**. `.` is a symbol constituent, so `Shape.Rect` reads as one name; the
+struct-literal arm fires on a symbol followed by a map; and the field-access arm needs a *leading* dot, so the two
+cannot collide. `(Name {.field value})` is one syntax for both, and which it is, is decided against the tables.
+
+### Tags are declaration order, so case order is part of the contract
+
+Tag *n* is the *n*th declared case, from zero. The consequence is that an all-bytes-zero union is **the first declared
+case with a zeroed payload** — which is exactly the rule that makes an `Option`'s zero a `None`, and it is what makes
+`(defvar u U)` and an omitted union-typed struct field mean something rather than nothing. Reordering a union's cases
+is a layout change, the same way reordering a struct's fields is.
+
+### What is refused, and why each
+
+- **A non-exhaustive `match`.** Refused, not defaulted, and the message names the cases with no arm. 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
+  exactly the one a reader wants to be told about today. `_` is how to say "the rest", written where it can be seen.
+- **A case pattern binding some of a case's fields.** All of them or none, positionally — binding a prefix reads the
+  wrong field the moment one is inserted above it.
+- **Two arms for one case**, which is a mistake and never an intent.
+- **A union with no cases.** No value of it can exist, so a parameter of that type is a function nothing can call.
+- **A case field that is move-only**, in the same words a struct field already gets and for the same reason:
+  recursive teardown arrives with `drop`.
+- **A union as a map key.** The payload past the case in hand is indeterminate, so hashing the blob would make two
+  equal values hash differently. Hashing one properly is a per-case walk driven by a switch — a different shape from
+  the field list `struct_key_pair` emits, and nothing has wanted it.
+- **`uninit` on a union.** This is the one refusal that is *not* the struct rule. Everywhere else `uninit` is an
+  opt-out from ZII and the bytes are whatever they were: a garbage `f64` is a garbage number. A union's tag steers
+  control flow — a tag no case names falls past every comparison in a `match` into a block LLVM is entitled to assume
+  cannot be reached. That is the one place where garbage becomes "the optimiser may do anything".
+- **`(.x u)`.** A union's fields belong to a case, and which case is being held is what the tag says. `match` is how
+  one is opened, and its arms bind the fields of the case they matched.
+- **A global initialised with a case.** `(defvar g U (U.B {.x 1}))` would mean serialising the fields into the payload
+  blob at link time, which is a byte-level encoder this compiler does not have and which could not express a `string`
+  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
+tell a case from a misspelling. It has one now, keyed both by the full spelling `U.C` and by the bare `C`. The full
+spelling is a *key* rather than something split out of a dotted name at the use site, because a union's own name can
+contain a slash — an imported `rl/U` — and string surgery would own an edge this does not have to.
+
+### Printing
+
+`render.ml` walks a concrete type for `print`, the REPL inspector and the break buffer's locals, and a union fell
+through its `Named` arm to `<Shape>`. It recovers the case from the tag by a chain of comparisons — the same shape the
+enum arm already had, and for the same reason: the name is erased before any backend sees it — and reads the fields of
+**that case only**. It prints `(Shape.Dot {.x 1.5 .y -2.5})`, which is what the source would write.
+
+### What is left
+
+An **imported** union is still refused by name at `load.ml:312`, so a union is file-local. That is not a blocker for
+the macro expander: the prelude is parsed and prepended into the same flat namespace before `collect` runs, so a
+`defunion Form` in `prelude.ml` is an ordinary same-file declaration needing no import — verified by declaring one
+there and matching it from a program. `dev.ml`'s inspector still says "union values are milestone 6" for a stopped
+frame's locals, and `shim.ml`'s "a Flan union has no C layout" is now inaccurate as prose though the refusal it guards
+is still right: a union has a C layout and still may not cross to C by value, because the shim flattens aggregates.
+
 ## `defer` may be written in a `let`
 
 The whole of this project's resource-cleanup answer, and NEXT.md records `drop` and a `with-cleanup` form as both
diff --git a/NEXT.md b/NEXT.md
index 6136d21..dec1df5 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -513,14 +513,25 @@ run one lane at a time; item 4 is disjoint and runs alongside any of them.
    friction on every keystroke. `defn` parameter lists and `restart-case` clause parameters were the same shape and
    came with it. What remains in this batch is the break buffer and the inspector, and they are independent.
 
-5. **Union values, then the macro expander, then `Result`/`try`.** Promoted above `Handle` on the author's call —
+5. ~~**Union values**~~, then the macro expander, then `Result`/`try`. Promoted above `Handle` on the author's call —
    macros are the thing most worth wanting, and unions are the only thing between here and them.
 
-   **Unions are closer than the milestone number suggests.** `Tast.arm` already carries `acase` (a case name) and
-   `binds` (the slots a payload binds to) — that is union shape, built and exercised, because `Option` is a two-case
-   union wearing a special coat and `match` over it works today. What is missing is the declared layout (a tag plus the
-   largest variant), construction, and letting `match` bind payloads from a user-declared union. `defunion` already
-   parses and its shape is already checked; `check.ml:312` and `:1075` are the two refusals to remove.
+   **Union values are done.** See *Unions, and the tag they carry* in [`BUILT.md`](BUILT.md). The diagnosis was right:
+   `Option` is a two-case union wearing a special coat, so `Tast.arm`'s `acase` and `binds` already were union shape
+   and `check_match` grew a second subject rather than a second path. A union is `Types.Named` exactly as a struct is,
+   so every path that merely carries a type learned nothing.
+
+   What the spec did not settle and this lane did: the tag is an `i32` and the payload a blob aligned to the widest
+   member of any case, so `%"U" = type { i32, [k x iA] }` is C's `struct { int tag; union {...} u; }` byte for byte —
+   checked against clang's answer for the same declaration. A value is `(U.C {.field value ...})` and construction is
+   **qualified**; a pattern is bare `(C x y)` and resolves against the scrutinee. Tags are declaration order from
+   zero, so **case order is part of a union's contract**: a zeroed union is the first declared case. A non-exhaustive
+   match is **refused**, never defaulted.
+
+   What is left for the macro lane, and it is one thing: **`load.ml:312` refuses an imported union outright**, so a
+   union is file-local. That is not a blocker for `Form` — the prelude is parsed and prepended into the same flat
+   namespace before `collect` runs, so a `defunion Form` in `prelude.ml` is an ordinary same-file declaration and
+   needs no import and no `load.ml` change. Verified by declaring one there and matching it from a program.
 
    **Then macros**, which are blocked on exactly this and nothing else: a macro is `[Form] -> Form`, so `Form` has to be
    a Flan union whose *layout* the compiler and the `dlopen`ed macro agree on byte for byte. `NEXT.md`'s macro section
@@ -1148,8 +1159,11 @@ expander last, on 6's unions.
   with it — `rt_die` is the non-dev path too, where there is no listener and nothing to deadlock against, so whether it
   should be `_exit` unconditionally or only under `--dev` is a decision rather than a typo.
 
-- **`(A {.x 1})` on a union variant says "unknown struct A"** rather than the union refusal `check_struct` plainly
-  intends — `env` has no table of variant names. A diagnostics bug, not a backend death.
+- ~~**`(A {.x 1})` on a union variant says "unknown struct A"**~~ **Fixed** with union values. `env` now carries a
+  case table keyed both by the full spelling `U.C`, which is how a value of it is written, and by the bare `C`, which
+  is how a mistake spells a constructor; the bare entry exists only to say *"A is a case of the union U, not a struct
+  — a union value names both, as `(U.A {.field value ...})`"*. Two unions may share a case name and that is not
+  refused: construction is qualified and a pattern resolves against the scrutinee, so both are unambiguous.
 
 ### Test blind spots, from a mutation pass
 
diff --git a/lib/check.ml b/lib/check.ml
index 3260e5b..9a39427 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -44,6 +44,20 @@ type binding = {
 type env = {
   structs : (string, Tast.structure) Hashtbl.t;
   unions  : (string, Tast.union) Hashtbl.t;
+  (* Every union case, twice over: once under its full spelling ["U.C"], which
+     is how a value of it is written, and once under the bare ["C"], which is
+     how a [match] arm names it and how a mistake spells a constructor. The
+     full spelling is a key rather than something split out of a dotted name at
+     the use site, because a union's own name can contain a slash (an imported
+     [rl/U]) and may one day contain a dot; string surgery would own an edge
+     this does not have to.
+
+     The bare entry is deliberately last-writer-wins and is *only* used to say
+     "C is a case of U, write (U.C ...)". Two unions may share a case name —
+     construction is qualified and a pattern resolves against the scrutinee, so
+     both are unambiguous — and refusing that would be a restriction with no
+     mechanism behind it. *)
+  cases   : (string, string * Tast.variant) Hashtbl.t;
   aliases : (string, Ast.texpr) Hashtbl.t;
   consts  : (string, int64) Hashtbl.t;         (* compile-time array lengths *)
   locs    : (string, Loc.t) Hashtbl.t;         (* where each type was declared *)
@@ -64,6 +78,7 @@ type env = {
 let new_env () = {
   structs = Hashtbl.create 16;
   unions  = Hashtbl.create 16;
+  cases   = Hashtbl.create 32;
   aliases = Hashtbl.create 16;
   consts  = Hashtbl.create 16;
   locs    = Hashtbl.create 16;
@@ -392,12 +407,12 @@ and resolve_name env ~seen loc n =
           fail loc "the type alias %s is defined in terms of itself" n
         else resolve env ~seen:(n :: seen) (Hashtbl.find env.aliases n)
       | _ when Hashtbl.mem env.structs n -> Types.Named n
-      (* A union has no layout in emit — nothing there mentions unions at all —
-         so a union-typed global reached clang as a reference to an undefined
-         %"U". Constructing one and reading a field of one are already refused,
-         so there is nothing to lower: only a declaration that got through. *)
-      | _ when Hashtbl.mem env.unions n ->
-        unimplemented loc (Printf.sprintf "the union type %s" n) 6
+      (* A union is [Named] exactly as a struct is: one case in [Types.t]
+         covers both, and which table the name is in is what tells them apart.
+         Keeping them one case is what lets a union be a field, a parameter, a
+         return type and a slot without a single one of those paths learning
+         that unions exist. *)
+      | _ when Hashtbl.mem env.unions n -> Types.Named n
       | _ when Hashtbl.mem env.enums n -> Types.Enum n
       (* A typo in a primitive is lowercase too, and the type-variable rule
          below would otherwise report [f65] as unimplemented generics and send
@@ -644,6 +659,18 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref =
   | t when bytewise_key t ->
     Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat"
   | Types.Named n when Hashtbl.mem env.structs n -> struct_key_pair env loc n
+  (* A union key would have to hash the tag and then only the bytes the case in
+     hand actually uses — the rest of the payload is indeterminate, exactly as
+     a struct's padding is, so hashing the blob would make two equal values
+     hash differently. That is a per-case walk driven by a switch, which is a
+     different shape from the field list [struct_key_pair] emits and which
+     nothing has yet wanted. Refused by name rather than written untested. *)
+  | Types.Named n when Hashtbl.mem env.unions n ->
+    fail loc
+      "%s is a union, and a union is not a map key: the payload past the case \
+       in hand is indeterminate, so hashing the bytes would make two equal \
+       values hash differently. Hashing one needs a per-case walk, which is \
+       not written — key on the tag, or on a struct holding what you meant" n
   | Types.Array (_, e) ->
     (* A fixed array of a struct or of strings would need the same per-element
        walk a struct key gets, driven by a loop rather than by a field list.
@@ -1077,10 +1104,30 @@ and var ctx loc ~want name =
       match Hashtbl.find_opt ctx.env.globals name with
       | Some (ty, _) -> expect loc ~want (mk loc ty (Tast.Global name))
       | None ->
-        if Hashtbl.mem ctx.env.fns name then
-          unimplemented loc
-            (Printf.sprintf "the function value %s (a name used as a value)" name) 5
-        else begin captured ctx loc name; fail loc "unknown name %s" name end
+        match Hashtbl.find_opt ctx.env.cases name with
+        (* A case with no fields is a whole value on its own, so it is written
+           as a name and not as a call — the same shape [None] has, and for the
+           same reason: there is nothing to put in the braces. A case that does
+           have fields is refused here rather than silently zeroed, because ZII
+           on a constructor would quietly produce a value nobody wrote. *)
+        | Some (uname, c) when String.contains name '.' ->
+          if c.Tast.vfields <> [] then
+            fail loc
+              "%s has fields, so it needs them — write (%s {.%s ...})"
+              name name
+              (List.hd c.Tast.vfields).Tast.fname;
+          expect loc ~want
+            (mk loc (Types.Named uname)
+               (Tast.MakeCase (uname, c.Tast.vname, [])))
+        | Some (uname, c) ->
+          fail loc
+            "%s is a case of the union %s, and a union value names both — \
+             write %s.%s" name uname uname c.Tast.vname
+        | None ->
+          if Hashtbl.mem ctx.env.fns name then
+            unimplemented loc
+              (Printf.sprintf "the function value %s (a name used as a value)" name) 5
+          else begin captured ctx loc name; fail loc "unknown name %s" name end
 
 (* Reading a move-only local. Every read is a move unless the site said it was
    a borrow, which is the conservative direction: passing one to a function,
@@ -1414,12 +1461,35 @@ and check_if ctx ?want loc c t e =
     in
     mk loc ty (Tast.If (c, t, e))
 
+(* A record-shaped literal: one form for both, because [(Name {.f v})] is the
+   same syntax whether [Name] is a struct or a union case, and the two differ
+   only in what is built at the end. Deciding here rather than in the parser is
+   what lets the decision be made against the tables, exactly. *)
 and check_struct ctx ~want loc name kvs =
   match Hashtbl.find_opt ctx.env.structs name with
   | None ->
-    if Hashtbl.mem ctx.env.unions name then
-      unimplemented loc "constructing a union value" 6
-    else fail loc "unknown struct %s" name
+    (match Hashtbl.find_opt ctx.env.cases name with
+     (* The full spelling [U.C], which is how a union value is written. Checked
+        before the diagnostics below, since the bare-name entry in the same
+        table is only ever a hint. *)
+     | Some (uname, c) when String.contains name '.' ->
+       check_case ctx ~want loc uname c kvs
+     (* A bare case name. This is the bug NEXT.md listed under "Bugs found and
+        not yet fixed": [(A {.x 1})] on a case of a union reported "unknown
+        struct A", because nothing in [env] could tell a case name from a
+        misspelling. It can now, so it says what was meant. *)
+     | Some (uname, c) ->
+       fail loc
+         "%s is a case of the union %s, not a struct — a union value names \
+          both, as (%s.%s {.field value ...})"
+         name uname uname c.Tast.vname
+     | None ->
+       if Hashtbl.mem ctx.env.unions name then
+         fail loc
+           "%s is a union, and a union value names the case as well as the \
+            type — write (%s.%s {.field value ...}) for one of %s"
+           name name (first_case_name ctx.env name) (case_list ctx.env name)
+       else fail loc "unknown struct %s" name)
   | Some s ->
     let seen = Hashtbl.create 8 in
     List.iter
@@ -1443,6 +1513,44 @@ and check_struct ctx ~want loc name kvs =
     in
     expect loc ~want (mk loc (Types.Named name) (Tast.Make (name, fields)))
 
+(* The cases of a union, as written, for a message that has to name them. *)
+and case_list env uname =
+  match Hashtbl.find_opt env.unions uname with
+  | None -> "its cases"
+  | Some u ->
+    String.concat ", "
+      (List.map (fun (c : Tast.variant) -> uname ^ "." ^ c.Tast.vname)
+         u.Tast.cases)
+
+and first_case_name env uname =
+  match Hashtbl.find_opt env.unions uname with
+  | Some { Tast.cases = c :: _; _ } -> c.Tast.vname
+  | _ -> "Case"
+
+(* [(U.C {.f v ...})]. The fields are checked and filled in exactly as a
+   struct's are — same ZII, same duplicate and unknown-field refusals — and the
+   only difference is the node at the end and the type it carries. *)
+and check_case ctx ~want loc uname (c : Tast.variant) kvs =
+  let full = uname ^ "." ^ c.Tast.vname in
+  let seen = Hashtbl.create 8 in
+  List.iter
+    (fun (k, (v : Ast.expr)) ->
+       if Hashtbl.mem seen k then fail v.Ast.loc "field %s is given twice" k;
+       if Tast.vfield_index c k = None then
+         fail v.Ast.loc "%s has no field %s" full k;
+       Hashtbl.add seen k v)
+    kvs;
+  let fields =
+    map_lr
+      (fun (f : Tast.field) ->
+         match Hashtbl.find_opt seen f.Tast.fname with
+         | Some v -> check ctx ~want:f.Tast.fty v
+         | None -> mk loc f.Tast.fty (Tast.Zero f.Tast.fty))
+      c.Tast.vfields
+  in
+  expect loc ~want
+    (mk loc (Types.Named uname) (Tast.MakeCase (uname, c.Tast.vname, fields)))
+
 and check_arr ctx ~want loc items =
   let elem_want =
     match want with
@@ -1475,9 +1583,17 @@ and check_arr ctx ~want loc items =
 
 and check_match ctx ?want loc scrutinee arms =
   let s = check ctx scrutinee in
-  let elem =
+  (* What the arms are alternatives over. An [Option] is a two-case union
+     wearing a special coat, so the two shapes below are the same shape: a set
+     of case names, an arity and a payload type per case, and a tag. Keeping
+     them apart here rather than desugaring [Option] into a declared union is
+     deliberate — [Option] is generic and no declared union is, so the coat is
+     the part that cannot yet be taken off. *)
+  let subject =
     match s.Tast.ty with
-    | Types.Option t -> t
+    | Types.Option t -> `Option t
+    | Types.Named n when Hashtbl.mem ctx.env.unions n ->
+      `Union (Hashtbl.find ctx.env.unions n)
     (* An enum is the one scrutinee that is not a milestone away: it is an i32
        at run time and its members are all known, so the arms would be a chain
        of [=] with an exhaustiveness check over [env.enums] — a desugaring, not
@@ -1491,12 +1607,63 @@ and check_match ctx ?want loc scrutinee arms =
          of (= k :member), but a keyword has no case in the pattern type yet. \
          Use cond" n
     | other ->
-      (* Union matching arrives with unions themselves, at milestone 6. *)
-      fail loc "match works on an Option at milestone 2, not on %s"
+      fail loc "match works on an Option or a union, not on %s"
         (Types.to_string other)
   in
+  (* Which case each arm names, and the type of each name it binds. This is the
+     whole of what differs between the two subjects; everything below it is
+     shared. *)
+  let resolve_pat (a : Ast.arm) =
+    match subject, a.Ast.pat with
+    | _, Ast.Pwild -> None, []
+    | `Option elem, Ast.Pctor ("Some", [ x ]) -> Some "Some", [ (x, elem) ]
+    | `Option _, Ast.Pctor ("Some", _) ->
+      fail a.Ast.aloc "the Some pattern binds exactly one name"
+    | `Option _, Ast.Pctor ("None", []) -> Some "None", []
+    | `Option _, Ast.Pctor ("None", _) -> fail a.Ast.aloc "None binds no names"
+    | `Option _, Ast.Pctor (c, _) ->
+      fail a.Ast.aloc
+        "%s is not a case of Option — the cases are Some and None" c
+    | `Union u, Ast.Pctor (c, names) ->
+      (* A pattern names the case bare: the scrutinee's type already says which
+         union, so [(Node l r)] is unambiguous even where two unions share the
+         case name. The qualified spelling is accepted too, since that is how
+         the value was written and writing it again should not be an error. *)
+      let bare =
+        let full = u.Tast.uname ^ "." in
+        let n = String.length full in
+        if String.length c > n && String.sub c 0 n = full then
+          String.sub c n (String.length c - n)
+        else c
+      in
+      (match Tast.case_index u bare with
+       | None ->
+         fail a.Ast.aloc "%s is not a case of %s — the cases are %s" c
+           u.Tast.uname
+           (String.concat ", "
+              (List.map (fun (v : Tast.variant) -> v.Tast.vname) u.Tast.cases))
+       | Some (_, v) ->
+         (* Positional, in declaration order, and all of them or none: a
+            pattern that bound some of a case's fields would be silently
+            reading the wrong one after a field is inserted. Refused with the
+            count, which is the thing that is wrong. *)
+         if List.length names <> List.length v.Tast.vfields then
+           fail a.Ast.aloc
+             "%s.%s has %d field%s, and this pattern binds %d — a case pattern \
+              binds every field, in declaration order (%s)"
+             u.Tast.uname bare (List.length v.Tast.vfields)
+             (if List.length v.Tast.vfields = 1 then "" else "s")
+             (List.length names)
+             (String.concat " "
+                (List.map (fun (f : Tast.field) -> f.Tast.fname)
+                   v.Tast.vfields));
+         Some bare,
+         List.map2 (fun n (f : Tast.field) -> (n, f.Tast.fty))
+           names v.Tast.vfields)
+  in
   let want = ref want in
-  let saw_some = ref false and saw_none = ref false and saw_wild = ref false in
+  let seen = Hashtbl.create 8 in
+  let saw_wild = ref false in
   (* The same rule as [if], and for the same reason: the arms are alternatives,
      so each is checked from the state before the match and the union of what
      they moved survives the join. Checked in sequence against one mutating set
@@ -1507,23 +1674,19 @@ and check_match ctx ?want loc scrutinee arms =
   let arms =
     map_lr
       (fun (a : Ast.arm) ->
-         let ctor, binds =
-           match a.Ast.pat with
-           | Ast.Pwild -> saw_wild := true; None, []
-           | Ast.Pctor ("Some", [ x ]) -> saw_some := true; Some "Some", [ x ]
-           | Ast.Pctor ("Some", _) ->
-             fail a.Ast.aloc "the Some pattern binds exactly one name"
-           | Ast.Pctor ("None", []) -> saw_none := true; Some "None", []
-           | Ast.Pctor ("None", _) -> fail a.Ast.aloc "None binds no names"
-           | Ast.Pctor (c, _) ->
-             fail a.Ast.aloc
-               "%s is not a case of Option — the cases are Some and None" c
-         in
+         let ctor, binds = resolve_pat a in
+         (match ctor with
+          | None -> saw_wild := true
+          | Some c ->
+            if Hashtbl.mem seen c then
+              fail a.Ast.aloc "this match has two %s arms" c;
+            Hashtbl.add seen c ());
          ctx.dead <- before;
          let arm =
            branch ctx (fun () ->
              let binds =
-               List.map (fun n -> bind ctx n elem ~assignable:false) binds
+               List.map
+                 (fun (n, ty) -> bind ctx n ty ~assignable:false) binds
              in
              let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in
              if !want = None && body.Tast.ty <> Types.Never then
@@ -1537,10 +1700,28 @@ and check_match ctx ?want loc scrutinee arms =
       arms
   in
   ctx.dead <- !joined;
-  if not (!saw_wild || (!saw_some && !saw_none)) then
+  (* Exhaustiveness is refused, not defaulted. A match that silently fell
+     through would have to produce a value of the match's type out of nothing,
+     and there is no such value for most types; and the case a union grows
+     tomorrow is exactly the one a reader wants to be told about today. A [_]
+     arm is the way to say "the rest", written where it can be seen. *)
+  let missing =
+    match subject with
+    | `Option _ -> List.filter (fun c -> not (Hashtbl.mem seen c)) [ "Some"; "None" ]
+    | `Union u ->
+      List.filter_map
+        (fun (c : Tast.variant) ->
+           if Hashtbl.mem seen c.Tast.vname then None
+           else Some (u.Tast.uname ^ "." ^ c.Tast.vname))
+        u.Tast.cases
+  in
+  if not !saw_wild && missing <> [] then
     fail loc
-      "this match is not exhaustive — Option needs both Some and None, or a \
-       _ arm";
+      "this match is not exhaustive — %s %s no arm. Add %s, or a _ arm for \
+       the rest"
+      (String.concat ", " missing)
+      (if List.length missing = 1 then "has" else "have")
+      (if List.length missing = 1 then "it" else "them");
   let ty = match !want with Some t -> t | None -> Types.Never in
   mk loc ty (Tast.Match (s, arms))
 
@@ -1554,6 +1735,17 @@ and struct_target ctx (target : Ast.expr) : Tast.expr * string =
   | Types.Named n when Hashtbl.mem ctx.env.structs n -> t, n
   | Types.Ptr (Types.Named n) when Hashtbl.mem ctx.env.structs n ->
     mk t.Tast.loc (Types.Named n) (Tast.Deref t), n
+  (* A union's fields belong to one case, and which case it is holding is only
+     known after the tag has been read. [.field] would have to be a read that
+     might be reading something else, so it is not one: [match] is how a union
+     is opened, and it binds the fields it has proved are there. *)
+  | (Types.Named n | Types.Ptr (Types.Named n))
+    when Hashtbl.mem ctx.env.unions n ->
+    fail target.Ast.loc
+      "%s is a union, and a union's fields belong to a case — which one it is \
+       holding is what the tag says, so they are reached by (match ...), \
+       whose arms bind the fields of the case they matched"
+      n
   | other ->
     fail target.Ast.loc "%s is not a struct, so it has no fields"
       (Types.to_string other)
@@ -2938,6 +3130,7 @@ and named_call ctx ~want loc name args =
     let rc =
       { Render.structs =
           Hashtbl.fold (fun _ v acc -> v :: acc) ctx.env.structs [];
+        unions = Hashtbl.fold (fun _ v acc -> v :: acc) ctx.env.unions [];
         enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) ctx.env.enums [];
         emit = emitter;
         alloc = (fun ty -> fresh_slot ctx ty) }
@@ -3032,8 +3225,19 @@ and named_call ctx ~want loc name args =
       let args = map2_lr (fun p a -> check ctx ~want:p a) params args in
       expect loc ~want (mk loc ret (Tast.Call (name, args)))
     | None ->
-      if Hashtbl.mem ctx.env.structs name || Hashtbl.mem ctx.env.unions name
-      then
+      if Hashtbl.mem ctx.env.unions name then
+        fail loc
+          "%s is a union type — a union value names the case too, as (%s.%s            {.field value ...})"
+          name name (first_case_name ctx.env name)
+      else if Hashtbl.mem ctx.env.cases name then
+        (* [(U.C)] and [(C)]: a case written as a call. Both are how someone
+           reaches for a constructor, and neither is one. *)
+        let uname, c = Hashtbl.find ctx.env.cases name in
+        fail loc
+          "%s is a case of the union %s — write (%s.%s {.field value ...}), \
+           or %s.%s on its own when it has no fields"
+          name uname uname c.Tast.vname uname c.Tast.vname
+      else if Hashtbl.mem ctx.env.structs name then
         fail loc
           "%s is a type — a struct value is written (%s {.field value ...})"
           name name
@@ -3248,11 +3452,56 @@ let collect env (decls : Ast.decl list) =
            fields;
          Hashtbl.replace env.structs n { Tast.sname = n; fields }
        | Ast.Defunion (n, vs) ->
-         Hashtbl.replace env.unions n
-           { Tast.uname = n;
-             cases = List.map (fun (v : Ast.variant) ->
-               { Tast.vname = v.Ast.vname;
-                 vfields = List.map field v.Ast.vfields }) vs }
+         (* A union with no cases has no value, so nothing could ever be given
+            one, and a parameter of that type would be a function nothing can
+            call. It parses; it is refused here rather than surviving to a
+            layout with a tag and no case for the tag to name. *)
+         if vs = [] then
+           fail loc
+             "%s declares no cases, so no value of it can exist — a union is \
+              (defunion %s [(Case [field Type ...]) ...])" n n;
+         let cnames = List.map (fun (v : Ast.variant) -> v.Ast.vname) vs in
+         if List.length (List.sort_uniq compare cnames) <> List.length cnames
+         then fail loc "%s declares the same case twice" n;
+         let cases =
+           List.map
+             (fun (v : Ast.variant) ->
+                let fnames =
+                  List.map (fun (f : Ast.field) -> f.Ast.fname) v.Ast.vfields
+                in
+                if List.length (List.sort_uniq compare fnames)
+                   <> List.length fnames then
+                  fail v.Ast.vloc "%s.%s declares the same field twice"
+                    n v.Ast.vname;
+                let vfields = List.map field v.Ast.vfields in
+                (* The same refusal a struct field gets, for the same reason
+                   and in the same words: a union case's fields are a struct,
+                   the union copies bytewise on assignment, and recursive
+                   teardown arrives with [drop]. Refusing it here rather than
+                   at a use keeps the two declarations honest with each other
+                   — a union that could hold a Vec where a struct could not
+                   would be a hole in the same rule. *)
+                List.iter
+                  (fun (f : Tast.field) ->
+                     if Types.is_move_only f.Tast.fty then
+                       fail v.Ast.vloc
+                         "%s.%s's field %s is %s, which is move-only, and a \
+                          union case that owns one makes the union move-only \
+                          too — transitively, with recursive teardown. That \
+                          rule arrives with drop (step 5 in NEXT.md); until \
+                          then hold the %s in a local and pass it"
+                         n v.Ast.vname f.Tast.fname (Types.to_string f.Tast.fty)
+                         (Types.to_string f.Tast.fty))
+                  vfields;
+                { Tast.vname = v.Ast.vname; vfields })
+             vs
+         in
+         Hashtbl.replace env.unions n { Tast.uname = n; cases };
+         List.iter
+           (fun (c : Tast.variant) ->
+              Hashtbl.replace env.cases (n ^ "." ^ c.Tast.vname) (n, c);
+              Hashtbl.replace env.cases c.Tast.vname (n, c))
+           cases
        | Ast.Defn fn ->
          let params =
            List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params
@@ -3427,7 +3676,27 @@ let check_global env (d : Ast.decl) : Tast.global option =
     let ginit =
       match init with
       | Ast.Zeroed -> { Tast.e = Tast.Zero ty; ty; loc = d.Ast.dloc }
-      | Ast.Uninit -> { Tast.e = Tast.Uninit ty; ty; loc = d.Ast.dloc }
+      | Ast.Uninit ->
+        (* Everywhere else [uninit] is an opt-out from ZII and the bytes are
+           whatever they were: a garbage f64 is a garbage number. A union is
+           the one type where that is qualitatively worse — the tag steers
+           control flow, a tag no case names falls past every comparison in a
+           [match], and the block after them is [unreachable], which LLVM is
+           entitled to assume cannot happen. So the one place where garbage
+           becomes "the optimiser may do anything" is refused by name, and the
+           zeroed form, which is the first declared case, is named beside it. *)
+        (match ty with
+         | Types.Named un when Hashtbl.mem env.unions un ->
+           fail d.Ast.dloc
+             "%s is a union, and uninit on one is refused: its tag steers \
+              every match, and a tag no case names has no arm to reach. Drop \
+              the uninit — a zeroed %s is %s, which is a real case"
+             (Types.to_string ty) un
+             (match Hashtbl.find_opt env.unions un with
+              | Some { Tast.cases = c :: _; _ } -> un ^ "." ^ c.Tast.vname
+              | _ -> "its first case")
+         | _ -> ());
+        { Tast.e = Tast.Uninit ty; ty; loc = d.Ast.dloc }
       | Ast.Init v -> check (ctx ()) ~want:ty v
     in
     Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false }
diff --git a/lib/emit.ml b/lib/emit.ml
index 26cba22..5693c29 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -195,6 +195,12 @@ type m = {
   out     : Buffer.t;
   strs    : Buffer.t;                        (* string literal constants *)
   structs : (string, Tast.structure) Hashtbl.t;
+  (* The declared unions, by name. [Types.Named] covers both a struct and a
+     union, so which table the name is in is the only thing that says which
+     this is — the same arrangement the checker uses, and for the same reason:
+     a union is a type like any other everywhere except at its layout, its
+     construction and its match. *)
+  unions  : (string, Tast.union) Hashtbl.t;
   globals : (string, Types.t) Hashtbl.t;
   (* Flan name -> C symbol, for the foreign functions. A call to one names the
      symbol directly; there is no thunk. *)
@@ -265,7 +271,23 @@ let rec lay m (t : Types.t) : int * int =
          lay_fields m (List.map (fun (fl : Tast.field) -> fl.Tast.fty) st.Tast.fields)
        in
        s, a
-     | None -> failwith ("no layout for struct " ^ n))
+     | None ->
+       match Hashtbl.find_opt m.unions n with
+       | Some u ->
+         (* The tag then the payload, as one struct, so the answer is the same
+            arithmetic every other aggregate here gets rather than a second
+            rule that could drift from it. *)
+         let size, align = payload_lay m u in
+         if size = 0 then 4, 4
+         else
+           let s, a, _ =
+             lay_fields m
+               [ Types.Int Types.I32;
+                 Types.Array (Int64.of_int (size / align),
+                              Types.Int (int_kind (align * 8))) ]
+           in
+           s, a
+       | None -> failwith ("no layout for struct " ^ n))
   | Types.Fn _ | Types.Var _ ->
     failwith ("no layout for " ^ Types.to_string t)
 
@@ -283,6 +305,27 @@ and lay_fields m tys =
     tys;
   align_up !off !al, !al, List.rev !rev
 
+(* The size and alignment of a union's payload: room for the largest case, with
+   the alignment the widest member of any case needs, and the size rounded up
+   to it so the blob divides evenly into [k x iA]. A union of payload-less
+   cases has a zero-size payload and is a bare tag. *)
+and payload_lay m (u : Tast.union) : int * int =
+  let align = ref 1 and size = ref 0 in
+  List.iter
+    (fun (c : Tast.variant) ->
+       let s, a, _ =
+         lay_fields m (List.map (fun (f : Tast.field) -> f.Tast.fty) c.Tast.vfields)
+       in
+       if a > !align then align := a;
+       if s > !size then size := s)
+    u.Tast.cases;
+  align_up !size !align, !align
+
+(* The integer kind of a given width, for the payload blob's element type. *)
+and int_kind = function
+  | 8 -> Types.I8 | 16 -> Types.I16 | 32 -> Types.I32 | 64 -> Types.I64
+  | n -> failwith ("no integer type of " ^ string_of_int n ^ " bits")
+
 (* A DWARF type node for a Flan type, memoised by the type's printed form so
    the pool holds one node per distinct type. *)
 let rec dty m d (t : Types.t) : int =
@@ -369,7 +412,23 @@ let rec dty m d (t : Types.t) : int =
            composite sn
              (List.map (fun (fl : Tast.field) -> (fl.Tast.fname, fl.Tast.fty))
                 st.Tast.fields)
-         | None -> failwith ("no debug type for struct " ^ sn))
+         | None ->
+           match Hashtbl.find_opt m.unions sn with
+           (* The truth about the bytes, and nothing cleverer: a tag and a blob.
+              DWARF 5 has DW_TAG_variant_part for exactly this, and lldb's C
+              support does not use it — a debugger that was handed one would
+              show less, not more. The reader who wants the payload reads it
+              through the case's own type, which is emitted beside this. *)
+           | Some u ->
+             let size, align = payload_lay m u in
+             composite sn
+               ([ ("tag", Types.Int Types.U32) ]
+                @ (if size = 0 then []
+                   else
+                     [ ("payload",
+                        Types.Array (Int64.of_int (size / align),
+                                     Types.Int (int_kind (align * 8)))) ]))
+           | None -> failwith ("no debug type for struct " ^ sn))
       (* An opaque pointer under lldb, which is the truth: the allocator's
          fields are the runtime's C and lldb already has that type from
          flan_rt.c's own debug info. *)
@@ -762,6 +821,10 @@ and value_at f (e : Tast.expr) : string =
     ins f "store %s %s, ptr %s" (ll ty) v' ptr;
     "zeroinitializer"
   | Tast.Make (_, fields) -> aggregate f e.Tast.ty fields
+  | Tast.MakeCase (uname, case, fields) ->
+    emit_make_case f uname case fields
+  | Tast.CaseField (target, case, i) ->
+    load f (case_field_addr f target case i) e.Tast.ty
   | Tast.Arr items -> aggregate f e.Tast.ty items
   | Tast.Some_ v ->
     let v' = value f v in
@@ -960,6 +1023,58 @@ and place f (p : Tast.place) : string * Types.t =
 (* A struct or fixed-array value, built field by field from zeroinitializer.
    The checker already filled the omitted fields in with Zero, so this is
    simply every field in declaration order. *)
+(* A union value, built in memory rather than with [insertvalue], because the
+   payload's declared type is a blob of integers and the case's fields are not:
+   the two views of the same bytes are what a gep expresses and what a chain of
+   [insertvalue] cannot. The alloca is what [mem2reg] removes when nobody takes
+   an address of it. *)
+and emit_make_case f uname case fields =
+  let ty = Types.Named uname in
+  let u = Hashtbl.find f.md.unions uname in
+  let tag = match Tast.case_index u case with
+    | Some (i, _) -> i
+    | None -> failwith ("no case " ^ case ^ " of " ^ uname)
+  in
+  let tmp = alloca f ty in
+  ins f "store %s zeroinitializer, ptr %s" (ll ty) tmp;
+  let tp = fresh f in
+  ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 0" tp (sname uname) tmp;
+  ins f "store i32 %d, ptr %s" tag tp;
+  if fields <> [] then begin
+    let pp = payload_addr f uname tmp in
+    let cty = sname (uname ^ "." ^ case) in
+    List.iteri
+      (fun i (p : Tast.expr) ->
+         let v = value f p in
+         let fp = fresh f in
+         ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d" fp cty pp i;
+         ins f "store %s %s, ptr %s" (ll p.Tast.ty) v fp)
+      fields
+  end;
+  load f tmp ty
+
+(* The payload blob's address. A union with no payload has no field 1, so this
+   is only ever reached for one that has fields to reach. *)
+and payload_addr f uname base =
+  let p = fresh f in
+  ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 1" p (sname uname) base;
+  p
+
+(* The address of one field of one case of a union value. The single place in
+   this backend that knows how a payload is read, so [match]'s binds and the
+   structural printer cannot come to different conclusions about it. *)
+and case_field_addr f (target : Tast.expr) case i =
+  let uname = match target.Tast.ty with
+    | Types.Named n -> n
+    | t -> failwith ("case field of " ^ Types.to_string t)
+  in
+  let base = addr f target in
+  let pp = payload_addr f uname base in
+  let p = fresh f in
+  ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d"
+    p (sname (uname ^ "." ^ case)) pp i;
+  p
+
 and aggregate f ty parts =
   let t = ll ty in
   let acc = ref "zeroinitializer" in
@@ -1344,12 +1459,60 @@ and emit_while f c body =
   label f le
 
 and emit_match f ty scrut arms =
-  let sv = value f scrut in
-  let sty = ll scrut.Tast.ty in
-  let tag = fresh f in
-  ins f "%s = extractvalue %s %s, 0" tag sty sv;
-  let payload_ty = match scrut.Tast.ty with
-    | Types.Option t -> t | t -> failwith ("match on " ^ Types.to_string t)
+  (* The two subjects are the same shape and are read differently: an [Option]
+     is an SSA aggregate with an i8 tag and its payload in field 1, a declared
+     union is read through its address because its payload is a blob that has
+     to be reinterpreted. So the tag and the binds are each produced by one of
+     two small functions and everything else below is shared. *)
+  let uname =
+    match scrut.Tast.ty with
+    | Types.Named n when Hashtbl.mem f.md.unions n -> Some n
+    | Types.Option _ -> None
+    | t -> failwith ("match on " ^ Types.to_string t)
+  in
+  let tag, read_tag, bind_of =
+    match uname with
+    | None ->
+      let sv = value f scrut in
+      let sty = ll scrut.Tast.ty in
+      let payload_ty = match scrut.Tast.ty with
+        | Types.Option t -> t | t -> failwith ("match on " ^ Types.to_string t)
+      in
+      let tag = fresh f in
+      ins f "%s = extractvalue %s %s, 0" tag sty sv;
+      (tag, (fun c -> ("i8", if c = "Some" then 1 else 0)),
+       fun _case _i slot ->
+         let v = fresh f in
+         ins f "%s = extractvalue %s %s, 1" v sty sv;
+         ins f "store %s %s, ptr %s" (ll payload_ty) v f.slots.(slot);
+         bind_slot f slot)
+    | Some n ->
+      let u = Hashtbl.find f.md.unions n in
+      (* Evaluated once, into a place, so that a scrutinee that is a call is
+         not re-run per arm. [addr] already spills a non-place for us. *)
+      let base = addr f scrut in
+      let tp = fresh f in
+      ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 0" tp (sname n) base;
+      let tag = fresh f in
+      ins f "%s = load i32, ptr %s" tag tp;
+      (tag,
+       (fun c ->
+          match Tast.case_index u c with
+          | Some (i, _) -> ("i32", i)
+          | None -> failwith ("no case " ^ c ^ " of " ^ n)),
+       fun case i slot ->
+         let pp = payload_addr f n base in
+         let fp = fresh f in
+         ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d"
+           fp (sname (n ^ "." ^ case)) pp i;
+         let fty =
+           match Tast.case_index u case with
+           | Some (_, c) -> (List.nth c.Tast.vfields i).Tast.fty
+           | None -> failwith ("no case " ^ case ^ " of " ^ n)
+         in
+         let v = load f fp fty in
+         ins f "store %s %s, ptr %s" (ll fty) v f.slots.(slot);
+         bind_slot f slot)
   in
   let ld = fresh_label f "endmatch" in
   let result = if is_void ty then None else Some (alloca f ty) in
@@ -1361,17 +1524,14 @@ and emit_match f ty scrut arms =
       (match a.Tast.acase with
        | None -> term f "br label %%%s" lb
        | Some c ->
-         let want = if c = "Some" then 1 else 0 in
+         let ity, want = read_tag c in
          let t = fresh f in
-         ins f "%s = icmp eq i8 %s, %d" t tag want;
+         ins f "%s = icmp eq %s %s, %d" t ity tag want;
          term f "br i1 %s, label %%%s, label %%%s" t lb ln);
       label f lb;
-      List.iter
-        (fun slot ->
-           let v = fresh f in
-           ins f "%s = extractvalue %s %s, 1" v sty sv;
-           ins f "store %s %s, ptr %s" (ll payload_ty) v f.slots.(slot);
-           bind_slot f slot)
+      List.iteri
+        (fun i slot ->
+           bind_of (match a.Tast.acase with Some c -> c | None -> "") i slot)
         a.Tast.binds;
       let v = block f a.Tast.abody in
       (match result with
@@ -1956,6 +2116,24 @@ let rec const m (e : Tast.expr) =
      | _ -> "{ " ^ String.concat ", " inner ^ " }")
   | Tast.Some_ v ->
     Printf.sprintf "{ i8 1, %s %s }" (ll v.Tast.ty) (const m v)
+  (* A union's payload is declared as a blob of integers, so a constant of one
+     would have to be the case's fields *serialised into those integers* —
+     which is a byte-level encoder this compiler does not have, and which could
+     not express a string field at all, since that is a pointer the linker has
+     to relocate and a byte array has nowhere to put a relocation. Refused by
+     name, here, where the rest of the same rule is. A zeroed global is fine
+     and needs none of this: it is the first declared case, all-bytes-zero. *)
+  | Tast.MakeCase (uname, case, _) ->
+    fail e.Tast.loc
+      "a global cannot be initialised with %s.%s — a union's payload is a \
+       blob, and writing a case into one at link time needs a byte-level \
+       encoder that does not exist (a string field could not be encoded at \
+       all). Declare the global zeroed, which is %s.%s, and assign the case \
+       you meant in a function"
+      uname case uname
+      (match Hashtbl.find_opt m.unions uname with
+       | Some { Tast.cases = c :: _; _ } -> c.Tast.vname
+       | _ -> "its first case")
   | _ ->
     fail e.Tast.loc
       "a global's value must be a compile-time constant — this one is computed"
@@ -2159,13 +2337,16 @@ let new_module ~checks ~dev ~known ?(debug = false) ?(sanitize = false)
       (p : Tast.program) =
   let m = {
     out = Buffer.create 8192; strs = Buffer.create 512;
-    structs = Hashtbl.create 16; globals = Hashtbl.create 16;
+    structs = Hashtbl.create 16; unions = Hashtbl.create 16;
+    globals = Hashtbl.create 16;
     externs = Hashtbl.create 32;
     checks; dev; known; nstr = 0; nfi = 0; sanitize;
     dbg = (if debug then Some (new_dbg p) else None);
   } in
   List.iter (fun (s : Tast.structure) -> Hashtbl.replace m.structs s.Tast.sname s)
     p.Tast.structs;
+  List.iter (fun (u : Tast.union) -> Hashtbl.replace m.unions u.Tast.uname u)
+    p.Tast.unions;
   List.iter (fun (g : Tast.global) -> Hashtbl.replace m.globals g.Tast.gname g.Tast.gty)
     p.Tast.globals;
   List.iter (fun (e : Tast.extern) -> Hashtbl.replace m.externs e.Tast.ename e.Tast.esym)
@@ -2177,6 +2358,37 @@ let new_module ~checks ~dev ~known ?(debug = false) ?(sanitize = false)
             (String.concat ", "
                (List.map (fun (f : Tast.field) -> ll f.Tast.fty) s.Tast.fields))))
     p.Tast.structs;
+  (* A union is a tag and a blob, and each of its cases is a struct laid over
+     the blob. Both are emitted as named types so that every reader — a
+     construction, a match arm, the structural printer — geps rather than
+     computing byte offsets of its own.
+
+     The blob is [k x iA] where A is the alignment the widest member of any
+     case needs: that is what makes LLVM align the payload without an explicit
+     [align] on a type, and it is what makes the whole agree with C's
+     [struct { int tag; union { ... } u; }] byte for byte. That agreement is
+     the point — the macro expander's [Form] has to be the same bytes in the
+     compiler and in the dlopened macro. *)
+  List.iter
+    (fun (u : Tast.union) ->
+       List.iter
+         (fun (c : Tast.variant) ->
+            Buffer.add_string m.out
+              (Printf.sprintf "%s = type { %s }\n"
+                 (sname (u.Tast.uname ^ "." ^ c.Tast.vname))
+                 (String.concat ", "
+                    (List.map (fun (f : Tast.field) -> ll f.Tast.fty)
+                       c.Tast.vfields))))
+         u.Tast.cases)
+    p.Tast.unions;
+  List.iter
+    (fun (u : Tast.union) ->
+       let size, align = payload_lay m u in
+       Buffer.add_string m.out
+         (Printf.sprintf "%s = type { i32%s }\n" (sname u.Tast.uname)
+            (if size = 0 then ""
+             else Printf.sprintf ", [%d x i%d]" (size / align) (align * 8))))
+    p.Tast.unions;
   Buffer.add_char m.out '\n';
   (* The foreign declarations. Every struct that crosses this boundary was
      flattened by a C shim, so each of these is scalars only and no calling
diff --git a/lib/reach.ml b/lib/reach.ml
index 79b1162..074d357 100644
--- a/lib/reach.ml
+++ b/lib/reach.ml
@@ -56,7 +56,8 @@ let rec expr_refs f (e : Tast.expr) =
   | Tast.Field (t, _) -> go t
   | Tast.Addr p -> place_refs f p
   | Tast.Deref t -> go t
-  | Tast.Make (_, es) -> gos es
+  | Tast.Make (_, es) | Tast.MakeCase (_, _, es) -> gos es
+  | Tast.CaseField (t, _, _) -> go t
   | Tast.Arr es -> gos es
   | Tast.Some_ v -> go v
   | Tast.Match (sc, arms) ->
diff --git a/lib/render.ml b/lib/render.ml
index 7de13dd..0333943 100644
--- a/lib/render.ml
+++ b/lib/render.ml
@@ -35,6 +35,10 @@ type emitter = {
 
 type ctx = {
   structs : Tast.structure list;
+  (* The declared unions. [Types.Named] covers a struct and a union alike, so
+     which list the name is in is what says which this is — the same
+     arrangement the checker and the emitter use. *)
+  unions  : Tast.union list;
   enums   : (string * (string * int64) list) list;
   emit    : emitter;
   (* A slot in the *caller's* frame. Only the slice arm needs one, and it needs
@@ -132,6 +136,59 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
           (Tast.If (is_some,
                     do_ ((lit "(some " :: render c (depth + 1) some) @ [ lit ")" ]),
                     lit "none")) ]
+    (* A union, printed as the source would write it: the case is recovered
+       from the tag by a chain of comparisons, exactly as an enum's member name
+       is, and only the case in hand has its fields read. Reading the others
+       would be reading a payload that is not there. *)
+    | Types.Named n
+      when List.exists (fun (u : Tast.union) -> String.equal u.Tast.uname n)
+             c.unions ->
+      let u =
+        List.find (fun (u : Tast.union) -> String.equal u.Tast.uname n) c.unions
+      in
+      let tag = { Tast.e = Tast.Field (e, 0); ty = Types.Int Types.I32; loc } in
+      let one i (v : Tast.variant) otherwise =
+        let is =
+          { Tast.e =
+              Tast.Prim (Tast.Eq,
+                         [ tag; { Tast.e = Tast.Int (Int64.of_int i, Types.I32);
+                                  ty = Types.Int Types.I32; loc } ]);
+            ty = Types.Bool; loc }
+        in
+        let full = n ^ "." ^ v.Tast.vname in
+        let body =
+          if v.Tast.vfields = [] then lit full
+          else
+            let shown = List.filteri (fun i _ -> i < max_span) v.Tast.vfields in
+            let parts =
+              List.concat
+                (List.mapi
+                   (fun i (f : Tast.field) ->
+                      let fv =
+                        { Tast.e = Tast.CaseField (e, v.Tast.vname, i);
+                          ty = f.Tast.fty; loc }
+                      in
+                      (if i = 0 then [] else [ lit " " ])
+                      @ [ lit ("." ^ f.Tast.fname ^ " ") ]
+                      @ render c (depth + 1) fv)
+                   shown)
+            in
+            do_ ((lit ("(" ^ full ^ " {") :: parts)
+                 @ (if List.length v.Tast.vfields > max_span then [ lit " ..." ]
+                    else [])
+                 @ [ lit "})" ])
+        in
+        unit_ (Tast.If (is, body, otherwise))
+      in
+      (* The fallback is a tag no case names, which only a scribbled-over union
+         could hold. Showing the number is more use than showing a case it is
+         not. *)
+      let base =
+        do_ [ lit ("<" ^ n ^ " tag ");
+              c.emit.ei64 (cast (Types.Int Types.I64) tag); lit ">" ]
+      in
+      [ List.fold_left (fun acc x -> x acc) base
+          (List.rev (List.mapi one u.Tast.cases)) ]
     | Types.Named n ->
       (match
          List.find_opt (fun (s : Tast.structure) -> String.equal s.Tast.sname n)
diff --git a/lib/session.ml b/lib/session.ml
index 2658130..52618e9 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -463,6 +463,7 @@ let render_locals ?(origin = "<locals>") t ~frame ~(fn : Tast.fn) ~bound
   let extra = ref [] and nslots = ref 0 in
   let c =
     { Render.structs = t.program.Tast.structs;
+      unions = t.program.Tast.unions;
       enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
       emit = dev_emitter;
       alloc = (fun ty ->
@@ -582,6 +583,7 @@ let render_globals ?(origin = "<globals>") t ~(globals : Tast.global list)
   let extra = ref [] and nslots = ref 0 in
   let c =
     { Render.structs = t.program.Tast.structs;
+      unions = t.program.Tast.unions;
       enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
       emit = dev_emitter;
       alloc = (fun ty ->
@@ -651,6 +653,7 @@ let eval_expr ?(origin = "<eval>") t src : change =
   let extra = ref [] and nslots = ref (Array.length base) in
   let c =
     { Render.structs = t.program.Tast.structs;
+      unions = t.program.Tast.unions;
       enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
       emit = dev_emitter;
       alloc = (fun ty ->
diff --git a/lib/tast.ml b/lib/tast.ml
index a81b448..7c05b67 100644
--- a/lib/tast.ml
+++ b/lib/tast.ml
@@ -93,6 +93,22 @@ and expr_kind =
   | Addr   of place
   | Deref  of expr
   | Make   of string * expr list      (* struct literal, every field, in order *)
+  (* A union value: the union's name, the case's name, and every field of that
+     case in declaration order with the omitted ones filled in as [Zero] — the
+     same ZII rule [Make] carries, and settled here for the same reason. It is
+     its own node rather than a [Make] over a synthesised struct because the
+     value's *type* is the union and its payload is a byte blob the case is
+     reinterpreted into; a backend that saw only [Make] would have to rederive
+     which of the two it was looking at. *)
+  | MakeCase of string * string * expr list
+  (* One field of one case of a union value, by index. The case name is on the
+     node because the payload is untyped bytes: [Field]'s index alone cannot
+     say which case struct the blob is being read as. [match] is the only thing
+     that proves the case, so this is only ever built under an arm that
+     checked the tag — and by [Render], which reads a field only after the same
+     comparison. One node, so the payload layout is known in exactly one place
+     in each backend rather than once per reader. *)
+  | CaseField of expr * string * int
   | Arr    of expr list               (* fixed-array literal *)
   | Some_  of expr
   | None_
@@ -249,6 +265,26 @@ type program = {
   cshim   : (string * string) list;
 }
 
+(* The declared position of a case, which is its tag, and the case itself. Tags
+   are declaration order from zero, so an all-bytes-zero union is the first
+   case with a zeroed payload — the same rule that makes an [Option]'s zero a
+   [None], and the reason case order is part of a union's contract. *)
+let case_index (u : union) name =
+  let rec go i = function
+    | [] -> None
+    | (c : variant) :: rest ->
+      if String.equal c.vname name then Some (i, c) else go (i + 1) rest
+  in
+  go 0 u.cases
+
+let vfield_index (c : variant) name =
+  let rec go i = function
+    | [] -> None
+    | (f : field) :: rest ->
+      if String.equal f.fname name then Some i else go (i + 1) rest
+  in
+  go 0 c.vfields
+
 let field_index (s : structure) name =
   let rec go i = function
     | [] -> None
diff --git a/test/programs/unions.flan b/test/programs/unions.flan
new file mode 100644
index 0000000..56ad9fb
--- /dev/null
+++ b/test/programs/unions.flan
@@ -0,0 +1,96 @@
+;;;; Union values: declaring one, making one, matching one, printing one.
+;;;;
+;;;; The layout claim is the load-bearing one, so it is asserted rather than
+;;;; described: a union is a tag and room for the largest case, aligned to the
+;;;; widest member of any case, which is C's struct { int tag; union {...}; }.
+;;;; That is what the macro expander will need to agree with byte for byte, so
+;;;; `Shape` here is deliberately the shape a Form has: a case with no fields,
+;;;; a case whose members are wider than another's, and a case holding a
+;;;; string -- the three things a payload blob has to hold without disturbing
+;;;; the alignment of any of them.
+
+(defunion Shape
+  [Empty
+   (Dot   [x f64  y f64])
+   (Rect  [w i32  h i32])
+   (Tag   [name string  n u8])])
+
+;; A union crosses a call boundary in both directions, as a parameter and as a
+;; return type -- a value that cannot do that is not a value.
+(defn area [s Shape] f64
+  (match s
+    (Rect w h) (* (f64 w) (f64 h))
+    (Dot _x _y) 0.0
+    _ -1.0))
+
+(defn widen [n i32] Shape (Shape.Rect {.w n .h (* n 2)}))
+
+;; A union as a struct field, which is the path that makes its size and
+;; alignment visible to something other than a slot.
+(defstruct Cell [id i32  s Shape])
+
+(defn describe [s Shape] string
+  (match s
+    Empty "empty"
+    (Dot x y) (if (= x y) "dot on the diagonal" "dot")
+    (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))
+  (println (describe (Shape.Dot {.x 2.0 .y 2.0})))
+  (println (describe (Shape.Dot {.x 1.0 .y 2.0})))
+  (println (describe (Shape.Rect {.w 3 .h 3})))
+  (println (describe (Shape.Tag {.name "tagged" .n 7})))
+
+  ;; ZII: omitted fields are zeroed, exactly as in a struct literal.
+  (println (describe (Shape.Rect {.w 0})))
+
+  ;; Returned from a call, then matched.
+  (print (i64 (area (widen 4)))) (println "")
+  (print (i64 (area (Shape.Dot {.x 9.0 .y 9.0})))) (println "")
+  (print (i64 (area Shape.Empty))) (println "")
+
+  ;; Through a struct field, and copied: assigning a Cell copies the union's
+  ;; bytes, so the copy's payload must be the original's.
+  (let [c (Cell {.id 1 .s (Shape.Tag {.name "in a cell" .n 3})})
+        d c]
+    (println (describe (.s d)))
+    ;; A zeroed union is the first declared case -- Empty -- which is what
+    ;; makes case order part of the contract.
+    (let [z (Cell {.id 2})]
+      (println (describe (.s z)))))
+
+  ;; A local assigned a second case: the tag moves and the payload is rewritten.
+  (let [v Shape.Empty]
+    (set v (Shape.Rect {.w 5 .h 6}))
+    (print (i64 (area v))) (println "")
+    (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 "")
+  (print (Shape.Dot {.x 1.5 .y -2.5})) (println "")
+  (print (Shape.Tag {.name "printed" .n 9})) (println "")
+  (print (Cell {.id 7 .s (Shape.Rect {.w 1 .h 2})})) (println "")
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 3a6e530..d60033c 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1679,6 +1679,143 @@ 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\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"
+    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. *)
+    (* 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";
+    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);
+    (* uninit is an opt-out from ZII everywhere else and the bytes are just
+       bytes. On a union they steer control flow: a tag no case names falls
+       past every comparison in a match into the block LLVM is entitled to
+       assume cannot be reached. *)
+    refuses_src "uninit on a union global"
+      "(defunion U [A B])\n(defvar g U uninit)\n(defn main [] i32 0)"
+      "its tag steers every match";
+    (* A union's fields belong to a case, so .field is not a read anyone can
+       do without having read the tag first. match is how one is opened. *)
+    refuses_src "reading a field of a union directly"
+      "(defunion U [(A [x i32])])\n(defn f [u U] i32 (.x u))"
+      "reached by (match ...)";
+    (* 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;
@@ -1943,6 +2080,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"