diff --git a/NEXT.md b/NEXT.md
index 2fcaeb2..a743829 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -1905,7 +1905,7 @@ run one lane at a time; item 4 is disjoint and runs alongside any of them.
 
    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
+   namespace before `collect` runs, so a `defdata 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.
 
    **Macros landed on top of this** and needed no `load.ml` change for `Form`, exactly as this said. See
diff --git a/bin/main.ml b/bin/main.ml
index 13ee066..52ac753 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -39,7 +39,9 @@ let summarise (d : Flan.Ast.decl) =
   | Import (a, p) -> Printf.sprintf "import %s %S" a p
   | Defalias (n, _) -> Printf.sprintf "defalias %s" n
   | Defstruct (n, fs) -> Printf.sprintf "defstruct %s (%d fields)" n (List.length fs)
-  | Defunion (n, vs) -> Printf.sprintf "defunion %s (%d cases)" n (List.length vs)
+  | Defdata (n, vs) -> Printf.sprintf "defdata %s (%d cases)" n (List.length vs)
+  | Defunion (n, ms) ->
+    Printf.sprintf "defunion %s (%d members)" n (List.length ms)
   | Defvar (n, _, _) -> Printf.sprintf "defvar %s" n
   | Defconst (n, _, _) -> Printf.sprintf "defconst %s" n
   | Declare (fn, csym) ->
@@ -226,6 +228,14 @@ let () =
              | _ -> None)
           ds
       in
+      let unions =
+        List.filter_map
+          (fun (d : Flan.Ast.decl) ->
+             match d.Flan.Ast.d with
+             | Flan.Ast.Defunion (n, ms) -> Some (n, ms)
+             | _ -> None)
+          ds
+      in
       let known_enums =
         List.filter_map
           (fun (d : Flan.Ast.decl) ->
@@ -251,7 +261,8 @@ let () =
       in
       let imported, dump, env =
         Flan.Cimport.header ~loc:(Flan.Loc.make header 0 0) ~header ~flags
-          ~known_structs:(List.map fst structs) ~known_enums ~taken ~bound_syms
+          ~known_structs:(List.map fst structs)
+          ~known_unions:(List.map fst unions) ~known_enums ~taken ~bound_syms
           ~config:
             (match pkg with
              | f :: _ -> Flan.Load.binding_config (Filename.dirname f)
@@ -275,6 +286,14 @@ let () =
          List.iter
            (fun (n, why) -> Printf.printf ";; DISAGREES %s: %s\n" n why)
            bad);
+      (match Flan.Cimport.check_unions ~env ~unions dump with
+       | [] ->
+         if unions <> [] then
+           Printf.printf ";; every defunion agrees with the header\n"
+       | bad ->
+         List.iter
+           (fun (n, why) -> Printf.printf ";; DISAGREES %s: %s\n" n why)
+           bad);
       (* And the bindings the package already wrote by hand, against the
          header's own signatures. Nothing else in the build can do this: a
          wrong declare-c is wrong in the generated prototype too, so the two
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 3b1cbed..76f4e49 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -724,7 +724,7 @@ reason, and a `defmacro` typed at the REPL becomes an ordinary `Ast.Defn` that n
 it was rather than half-fixed here, and pinned in `test_session` so that changing it is a decision.
 
 **An expression that expands to a declaration is refused, by name.** `defn`, `defvar`, `defconst`, `defstruct`,
-`defunion`, `defenum`, `defalias`, `defmacro` and `import` are heads `Parse.expr` now rejects — the arm that used to
+`defdata`, `defenum`, `defalias`, `defmacro` and `import` are heads `Parse.expr` now rejects — the arm that used to
 say it for `defmacro` alone, generalised. It sits in the head dispatch and not in a walk over what the expander
 answered, so it catches a declaration nested anywhere in the expansion for free, catches one **typed** by hand with the
 same sentence instead of "unknown name defvar", and cannot drift out of sync with `decl`'s list the way a second copy
@@ -2732,7 +2732,7 @@ are involved, and none are needed" — and monomorphisation is what would buy it
 
 ## 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
+`defdata` 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`
@@ -2785,7 +2785,7 @@ the payload at offset 8, and 40/8 for a struct holding one.
 ### The surface
 
 ```clojure
-(defunion Shape
+(defdata Shape
   [Empty
    (Dot  [x f64  y f64])
    (Rect [w i32  h i32])
@@ -2847,13 +2847,13 @@ is a layout change, the same way reordering a struct's fields is.
 
 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
+chance: `check_finite` already walked a union's cases, so `(defdata 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])])
+(defdata Tree [Leaf (Node [l (Ptr Tree)  n i32])])
 
 (defn depth [t (Ptr Tree)] i32
   (match (deref t)
@@ -2888,7 +2888,7 @@ enum arm already had, and for the same reason: the name is erased before any bac
 
 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
+`defdata 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.
@@ -3068,7 +3068,7 @@ qualified under the alias the package was imported as. See "A package may declar
 
 ### `Form`, and the three numbers
 
-A macro's parameter and its result are `Form`, so `Form` has to exist on the Flan side: a `defunion` in `prelude.ml`
+A macro's parameter and its result are `Form`, so `Form` has to exist on the Flan side: a `defdata` in `prelude.ml`
 mirroring `lib/form.ml`. It mirrors `Form.value` and **not** `Form.t` — there is no `loc` field, deliberately. A macro
 cannot invent a source location, so the unmarshaller stamps the **call site's** `Loc.t` onto every node of what a
 macro returns. That is the structural answer to "keep the source location of the call site attached to what a macro
@@ -3792,7 +3792,7 @@ the thing it calls. `Prelude.bootstrap` is the hook, a ref rather than a paramet
 `Check.program` and it cannot be told.
 
 Only `defn`s are dropped: the functions that survive still mention the prelude's types, and a reduced prelude missing
-them would not check. A `defstruct`, `defunion`, `defalias`, `defenum` or `defvar` therefore stays whatever it names.
+them would not check. A `defstruct`, `defdata`, `defalias`, `defenum` or `defvar` therefore stays whatever it names.
 There used to be a sharper reason — `Parse.prelude_types` memoised the prelude's type names for the parser's
 return-type guess, and it can be forced for the first time inside a bootstrap build, so a reduced set cached there
 would have been wrong for every compile afterwards. That set is gone with the guess; see *The return type is the slot*
diff --git a/emacs/flan-inspect.el b/emacs/flan-inspect.el
index 10a4416..c77d2e1 100644
--- a/emacs/flan-inspect.el
+++ b/emacs/flan-inspect.el
@@ -62,7 +62,7 @@
 ;;   frame it means;
 ;;
 ;;   the slot root names one frame and one slot, so it is exact, and it
-;;   reaches an option's payload and a union case's fields, which have offsets
+;;   reaches an option's payload and a data type case's fields, which have offsets
 ;;   but no accessor.  It needs a stopped program, it is refused if the
 ;;   frame's body was redefined since it was entered — the same slot
 ;;   fingerprint the listing is refused by — and it cannot root at an
@@ -275,7 +275,7 @@ whatever the value came from."
 ;; is walking a type, so a field is its name and an element is its number.
 ;; Two cases need more than the name.
 ;;
-;;   A union's payload sits at an offset that depends on which case the value
+;;   A data type's payload sits at an offset that depends on which case the value
 ;;   is in, and only the renderer knows which case it currently is — it wrote
 ;;   `(Union.case {.f …})'.  So the type travels with the step and the wire
 ;;   spelling is `Union.case.f'.  Guessing the case from a field name two
@@ -686,14 +686,14 @@ root, which is what makes a mixed stack unconstructible."
     (unless step (user-error "flan: nothing to inspect on this line"))
     (let ((why (flan-inspect-refusal node flan-inspect--root)))
       (when why (user-error "flan: %s" why)))
-    ;; A union case's field, under an expression root.  This is a refusal of
+    ;; A data type case's field, under an expression root.  This is a refusal of
     ;; the *parent* and not of the value at point, which is why it is here and
     ;; not in `flan-inspect-refusal\=': a struct field that happens to hold a
-    ;; union is reached by an ordinary accessor and must stay enterable; it is
-    ;; a field *of the union itself* that has no accessor.  `(match ...)\=' is
-    ;; how a union is opened in the language, and it binds names rather than
+    ;; data type is reached by an ordinary accessor and must stay enterable;
+    ;; it is a field *of the data type itself* that has no accessor.  `(match ...)\=' is
+    ;; how a data type is opened in the language, and it binds names rather than
     ;; producing a value to send, so there is nothing to build here.  The
-    ;; renderer wrote the head as `Union.case\=', which is the one type spelling
+    ;; renderer wrote the head as `Type.case\=', which is the one type spelling
     ;; with a dot in it — a package qualifies with a slash.
     (let ((ty (plist-get flan-inspect--node :type)))
       (when (and (not (eq (car-safe flan-inspect--root) :slot))
@@ -701,14 +701,14 @@ root, which is what makes a mixed stack unconstructible."
                  (string-match-p "\\." ty))
         (user-error
          "flan: %s"
-         (concat "a union case's field: it is reached by (match ...) in the "
+         (concat "a data type case's field: it is reached by (match ...) in the "
                  "language, not by an accessor, so there is no expression to "
                  "send. `i' on a local in the break buffer roots at the frame's "
                  "slot instead, and that root steps into it by offset"))))
     ;; The line carries the step that names the field; what the wire needs
     ;; beyond the name is the type it is a field *of*, and that is this
-    ;; buffer's own node — the parent of the one at point.  A union's payload
-    ;; sits at an offset that depends on the case, so `Union.case\=' has to
+    ;; buffer's own node — the parent of the one at point.  A data type's payload
+    ;; sits at an offset that depends on the case, so `Type.case\=' has to
     ;; travel with the name.  An option's payload has no name at all and is
     ;; the symbol `some\='.
     (let* ((step (if (eq (plist-get flan-inspect--node :kind) 'option)
diff --git a/emacs/flan-mode.el b/emacs/flan-mode.el
index 69adbe9..491c1ff 100644
--- a/emacs/flan-mode.el
+++ b/emacs/flan-mode.el
@@ -93,7 +93,8 @@
   :prefix "flan-")
 
 (defconst flan--definers
-  '("defn" "defvar" "defconst" "defstruct" "defunion" "defenum" "defalias"
+  '("defn" "defvar" "defconst" "defstruct" "defdata" "defunion" "defenum"
+    "defalias"
     "declare" "import" "package")
   "Forms that introduce a top-level name.")
 
@@ -136,7 +137,7 @@ below — and not again here.")
 ;; that ignored the column would offer one.
 (defvar flan-imenu-generic-expression
   `(("Functions" ,(concat "^(defn\\s-+" flan--name-re) 1)
-    ("Types" ,(concat "^(def\\(?:struct\\|union\\|enum\\|alias\\)\\s-+"
+    ("Types" ,(concat "^(def\\(?:struct\\|data\\|union\\|enum\\|alias\\)\\s-+"
                       flan--name-re)
      1)
     ("Variables" ,(concat "^(def\\(?:var\\|const\\)\\s-+" flan--name-re) 1)
@@ -445,8 +446,9 @@ decision to `calculate-lisp-indent'."
         (flan--count-indent method indent-point last-sexp head-column))
        ((eq method :defn) (+ lisp-body-indent head-column))
        ;; No spec.  Anything else spelled `def…' is a definition and indents
-       ;; like one, which covers `defstruct', `defunion', `defenum', `defvar',
-       ;; `defconst' and `defalias' without naming them.
+       ;; like one, which covers `defstruct', `defdata', `defunion',
+       ;; `defenum', `defvar', `defconst' and `defalias' without naming
+       ;; them.
        ((and name (string-match-p "\\`def" name))
         (+ lisp-body-indent head-column))
        ;; A clause: `(name [params] body…)'.  `handler-bind', `handler-case'
diff --git a/emacs/test-flan-cider.el b/emacs/test-flan-cider.el
index 767ef19..f9e912a 100644
--- a/emacs/test-flan-cider.el
+++ b/emacs/test-flan-cider.el
@@ -562,10 +562,10 @@ unwind would send the next one to a daemon that is not there."
    (test-flan--check "and the trail says so"
                      (string-match-p "\\`o \\[frame 0\\]\\.some\n" (buffer-string)))))
 
-;; A union case's field.  The payload sits at an offset that depends on which
+;; A data type case's field.  The payload sits at an offset that depends on which
 ;; case the value is in, and only the renderer knows which it currently holds
 ;; — it wrote the head `Shape.circle'.  So the case travels with the name.
-(test-flan--check "a union field carries its case on the wire"
+(test-flan--check "a data type field carries its case on the wire"
                   (equal (flan-inspect-wire-step '(:field "r" "Shape.circle"))
                          "Shape.circle.r"))
 (test-flan--check "a struct field does not"
@@ -576,15 +576,15 @@ unwind would send the next one to a daemon that is not there."
 
 ;; And the other half of that pair: under an *expression* root there is no
 ;; accessor to send, so RET refuses there rather than sending `(.at s)' for
-;; the checker to reject.  A union's fields are reached by `(match ...)' in
+;; the checker to reject.  A data type's fields are reached by `(match ...)' in
 ;; the language, which binds names rather than producing a value.  It is a
 ;; refusal of the parent, not of the value at point — a struct field that
-;; merely *holds* a union is an ordinary accessor and stays enterable.
+;; merely *holds* a data type is an ordinary accessor and stays enterable.
 (let ((buf (test-flan--inspect "s" "(Shape.circle {.at (V {.x 1 .y 2})})")))
   (with-current-buffer buf
     (goto-char (point-min))
     (flan-inspect-next)
-    (test-flan--check "an expression root refuses a union case's field"
+    (test-flan--check "an expression root refuses a data type case's field"
                       (string-match-p
                        "reached by (match"
                        (or (test-flan--caught #'flan-inspect-into) "")))))
@@ -600,7 +600,7 @@ unwind would send the next one to a daemon that is not there."
       (flan-inspect--show '(:expr "c") nil)
       (with-current-buffer " *test-inspect*"
         (goto-char (point-min))
-        (flan-inspect-next) (flan-inspect-next)   ; .s, which holds the union
+        (flan-inspect-next) (flan-inspect-next)   ; .s, which holds the data type
         (test-flan--check "but a struct field that merely holds one is enterable"
                           (progn (flan-inspect-into) (equal (car asked) "(.s c)")))))))
 
@@ -615,7 +615,7 @@ unwind would send the next one to a daemon that is not there."
    (goto-char (point-min))
    (flan-inspect-next)
    (flan-inspect-into)
-   (test-flan--check "RET into a union field names the case it is in"
+   (test-flan--check "RET into a data type field names the case it is in"
                      (equal (plist-get (car test-flan--asked) :path)
                             '("Shape.circle.at")))))
 
diff --git a/lib/ast.ml b/lib/ast.ml
index 2edcf93..e80f8ae 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -152,7 +152,13 @@ and decl_kind =
   | Import   of string * string       (* alias, path *)
   | Defalias of string * texpr
   | Defstruct of string * field list
-  | Defunion of string * variant list
+  | Defdata of string * variant list
+  (* C's union: the members overlay one another at offset zero, the size is
+     the largest of them and the alignment the strictest. It carries the same
+     [field list] a struct does, because that is what it is — the difference
+     is entirely in the layout, and saying it with a second field type would
+     only mean every walk had two shapes to handle for one idea. *)
+  | Defunion of string * field list
   | Defn     of fn
   (* No body, so no [defn]: a foreign function, and the string is the C symbol
      it is actually called by (plan.org, Types — [declare] is kept only where
@@ -182,8 +188,8 @@ and init = Zeroed | Uninit | Init of expr
    drift apart. *)
 let declared_name (d : decl) =
   match d.d with
-  | Defenum (n, _) | Defalias (n, _) | Defstruct (n, _) | Defunion (n, _)
-  | Defvar (n, _, _) | Defconst (n, _, _) -> Some n
+  | Defenum (n, _) | Defalias (n, _) | Defstruct (n, _) | Defdata (n, _)
+  | Defunion (n, _) | Defvar (n, _, _) | Defconst (n, _, _) -> Some n
   | Declare (fn, _) | DeclareC (fn, _) | Defn fn -> Some fn.name
   | Package _ | Import _ -> None
 
diff --git a/lib/check.ml b/lib/check.ml
index 9253654..6b1fcf0 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -14,7 +14,7 @@
     The rule from the two misparse bugs applies here too: *anything not yet
     implemented is rejected by name*, never approximated. Milestone 2 is
     calc-me.flan and nothing more (plan.org, Build sequence), so [Vec], [Map],
-    [Result]/[try], user unions, closures, [dotimes], [defer], generics and
+    [Result]/[try], user data types, closures, [dotimes], [defer], generics and
     cross-package imports are all errors with a message that says which
     milestone they belong to. *)
 
@@ -43,17 +43,24 @@ 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
+  datas  : (string, Tast.data) Hashtbl.t;
+  (* The untagged unions, by name, and they are [Tast.structure] values on
+     purpose: a union's members *are* a field list, and every one of them is at
+     offset zero. Giving them a record of their own would have meant a second
+     shape for [field_index] and for every walk over a member list, to say
+     nothing new — which table the name is in is already what says whether the
+     offsets are cumulative or all zero, exactly as it is for a data type. *)
+  unions  : (string, Tast.structure) Hashtbl.t;
+  (* Every data type 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
+     the use site, because a data type'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 —
+     "C is a case of U, write (U.C ...)". Two data types 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. *)
@@ -124,6 +131,7 @@ type env = {
 
 let new_env () = {
   structs = Hashtbl.create 16;
+  datas  = Hashtbl.create 16;
   unions  = Hashtbl.create 16;
   cases   = Hashtbl.create 32;
   aliases = Hashtbl.create 16;
@@ -161,9 +169,12 @@ let declared_note env name =
       match Hashtbl.find_opt env.structs name with
       | Some s -> List.map (fun (f : Tast.field) -> f.Tast.fname) s.Tast.fields
       | None ->
-        (match Hashtbl.find_opt env.unions name with
+        (match Hashtbl.find_opt env.datas name with
          | Some u -> List.map (fun (c : Tast.variant) -> c.Tast.vname) u.Tast.cases
-         | None -> [])
+         | None ->
+           match Hashtbl.find_opt env.unions name with
+           | Some u -> List.map (fun (f : Tast.field) -> f.Tast.fname) u.Tast.fields
+           | None -> [])
     in
     let what =
       if names = [] then name ^ " is declared here"
@@ -282,7 +293,7 @@ type ctx = {
      [dead] is the slots whose value has been moved out, with where it went, so
      that a second use names the first rather than reporting a type error about
      nothing. It is flow-sensitive at an [if]: the two arms are checked from
-     the same starting set and the *union* survives the join, so moving in one
+     the same starting set and the *data type* survives the join, so moving in one
      arm only is still a move afterwards — and moving in both arms, which is
      legal, is not two errors.
 
@@ -538,7 +549,7 @@ let map_type ?(preds = []) loc (k : Types.t) (v : Types.t) =
    elements, a [defvar] with no initialiser are all all-bytes-zero — and a
    zeroed function value is a null pointer with a signature on it, which is the
    one kind of zero that cannot be used for anything. Every other type's zero
-   is a value: 0, false, an empty slice, [None], a union's first case. So these
+   is a value: 0, false, an empty slice, [None], a data type's first case. So these
    are refused where they are written rather than left to crash at the call.
 
    A parameter, a return type, a [let] binding and an [(Option (Fn ...))] are
@@ -658,6 +669,7 @@ and near_miss env n =
     Types.primitive_names
     @ Hashtbl.fold (fun k _ acc -> k :: acc) env.aliases []
     @ Hashtbl.fold (fun k _ acc -> k :: acc) env.structs []
+    @ Hashtbl.fold (fun k _ acc -> k :: acc) env.datas []
     @ Hashtbl.fold (fun k _ acc -> k :: acc) env.unions []
     @ Hashtbl.fold (fun k _ acc -> k :: acc) env.enums []
   in
@@ -711,11 +723,15 @@ 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 is [Named] exactly as a struct is: one case in [Types.t]
+      (* A data type 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
+         Keeping them one case is what lets a data type be a field, a parameter, a
          return type and a slot without a single one of those paths learning
-         that unions exist. *)
+         that data types exist. *)
+      | _ when Hashtbl.mem env.datas n -> Types.Named n
+      (* And so is an untagged union, for the same reason: it is a value of a
+         size and an alignment, and nothing that carries one has to know it is
+         a union rather than a struct. *)
       | _ 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
@@ -1250,18 +1266,29 @@ 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
+  (* A data type 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 ->
+  | Types.Named n when Hashtbl.mem env.datas 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 \
+      "%s is a data type, and a data type 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
+  (* And an untagged union is refused for the half of that reason which has
+     nothing to do with a tag: a member smaller than the union leaves the rest
+     of the storage indeterminate, so two values that agree about every byte
+     anybody wrote hash differently. There is no per-member walk to write here
+     either — nothing records which member was written, which is the type. *)
+  | Types.Named n when Hashtbl.mem env.unions n ->
+    fail loc
+      "%s is a union, and a union is not a map key: a member narrower than \
+       the union leaves the rest of the bytes indeterminate, so two values \
+       that agree about everything written would still hash differently. Key \
+       on the member 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.
@@ -1558,7 +1585,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     expect loc ~want (mk loc Types.Unit (Tast.Set (p, v)))
   | Ast.Field (target, name) ->
     let target, sname = struct_target ctx target in
-    let s = Hashtbl.find ctx.env.structs sname in
+    let s = Option.get (fields_named ctx.env sname) in
     (match Tast.field_index s name with
      | None ->
        Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
@@ -1768,19 +1795,19 @@ and var ctx loc ~want name =
            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 '.' ->
+        | Some (dname, 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) ->
+            (mk loc (Types.Named dname)
+               (Tast.MakeCase (dname, c.Tast.vname, [])))
+        | Some (dname, 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
+            "%s is a case of the data type %s, and a data type value names both — \
+             write %s.%s" name dname dname c.Tast.vname
         | None ->
           (* A bare function name *is* the function. This is a Lisp-1 — one
              top-level namespace, enforced, so a defn and a defvar cannot share
@@ -2483,7 +2510,7 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     let t = branch ctx (fun () -> in_tail (fun () -> check ctx t)) in
     expect loc ~want (mk loc Types.Unit (Tast.If (c, t, unit_at loc)))
   | Some e ->
-    (* Both arms start from the same dead set and the union survives: moving in
+    (* Both arms start from the same dead set and the data type survives: moving in
        one arm only still kills the binding afterwards, and moving in both —
        which is legal and common — is not reported twice. A flat set would have
        refused [(if c (free v) (free v))] and allowed the use after a one-armed
@@ -2514,31 +2541,33 @@ and check_if ctx ?(tail = false) ?want loc c t e =
     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
+   same syntax whether [Name] is a struct or a data type 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 when Hashtbl.mem ctx.env.unions name ->
+    check_union ctx ~want loc name kvs
   | None ->
     (match Hashtbl.find_opt ctx.env.cases name with
-     (* The full spelling [U.C], which is how a union value is written. Checked
+     (* The full spelling [U.C], which is how a data type 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
+     | Some (dname, c) when String.contains name '.' ->
+       check_case ctx ~want loc dname 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
+        not yet fixed": [(A {.x 1})] on a case of a data type 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) ->
+     | Some (dname, c) ->
        fail loc
-         "%s is a case of the union %s, not a struct — a union value names \
+         "%s is a case of the data type %s, not a struct — a data type value names \
           both, as (%s.%s {.field value ...})"
-         name uname uname c.Tast.vname
+         name dname dname c.Tast.vname
      | None ->
-       if Hashtbl.mem ctx.env.unions name then
+       if Hashtbl.mem ctx.env.datas name then
          fail loc
-           "%s is a union, and a union value names the case as well as the \
+           "%s is a data type, and a data type 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
@@ -2573,25 +2602,88 @@ 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
+(* [(U {.member v})] — an untagged union value.
+
+   At most one member, because the members are one storage: giving two would
+   be writing two values over each other and the result would be whichever the
+   compiler happened to store last. That is a real question with no answer, so
+   it is refused rather than ordered. Giving none is the ordinary ZII value and
+   is all-bytes-zero, the same as a struct with every field omitted.
+
+   The one member is lowered here into a zeroed temporary and a store, rather
+   than into a node of its own. A union value *is* a store into overlaid
+   storage — [Set] over [Pfield] is exactly that operation and every backend
+   already has it — so a [MakeUnion] node would have been the same three
+   instructions written a fourth and fifth time, in each backend, with the
+   layout rule spelled out again in each. Nothing downstream learns anything
+   new from this form. *)
+and check_union ctx ~want loc name kvs =
+  let u = Hashtbl.find ctx.env.unions name in
+  List.iter
+    (fun (k, (v : Ast.expr)) ->
+       if Tast.field_index u k = None then
+         Loc.failk "check/unknown-field" v.Ast.loc
+           ~notes:(declared_note ctx.env name)
+           "%s has no member %s" name k)
+    kvs;
+  let seen = Hashtbl.create 8 in
+  List.iter
+    (fun (k, (v : Ast.expr)) ->
+       (* Before the two-member refusal below, so [(U {.i 1 .i 2})] is told it
+          named one member twice rather than that [i] and [i] are the same
+          bytes — which is true and useless. Same words and same note as the
+          struct path, because it is the same mistake. *)
+       (match Hashtbl.find_opt seen k with
+        | Some (first : Ast.expr) ->
+          Loc.failk "check/duplicate-field" v.Ast.loc
+            ~notes:[ Loc.note first.Ast.loc (k ^ " is given here first") ]
+            "member %s is given twice" k
+        | None -> ());
+       Hashtbl.add seen k v)
+    kvs;
+  (match kvs with
+   | (a, _) :: (b, (second : Ast.expr)) :: _ ->
+     Loc.failk "check/union-two-members" second.Ast.loc
+       "%s is a union, so %s and %s are the same bytes and only one of them \
+        can be written — give the one this value is, and read the other \
+        member when you want to see those bytes that way"
+       name a b
+   | _ -> ());
+  match kvs with
+  (* The two-member case left above, so this sees one or none. *)
+  | _ :: _ :: _ -> assert false
+  | [] -> expect loc ~want (mk loc (Types.Named name) (Tast.Zero (Types.Named name)))
+  | [ (k, v) ] ->
+    let i = Option.get (Tast.field_index u k) in
+    let fty = (List.nth u.Tast.fields i).Tast.fty in
+    let v = check ctx ~want:fty v in
+    let slot = fresh_slot ctx (Types.Named name) in
+    let here = mk loc (Types.Named name) (Tast.Local slot) in
+    expect loc ~want
+      (mk loc (Types.Named name)
+         (Tast.Let
+            ([ (slot, mk loc (Types.Named name) (Tast.Zero (Types.Named name))) ],
+             [ mk loc Types.Unit (Tast.Set (Tast.Pfield (here, i), v)); here ])))
+
+(* The cases of a data type, as written, for a message that has to name them. *)
+and case_list env dname =
+  match Hashtbl.find_opt env.datas dname with
   | None -> "its cases"
   | Some u ->
     String.concat ", "
-      (List.map (fun (c : Tast.variant) -> uname ^ "." ^ c.Tast.vname)
+      (List.map (fun (c : Tast.variant) -> dname ^ "." ^ c.Tast.vname)
          u.Tast.cases)
 
-and first_case_name env uname =
-  match Hashtbl.find_opt env.unions uname with
+and first_case_name env dname =
+  match Hashtbl.find_opt env.datas dname 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
+and check_case ctx ~want loc dname (c : Tast.variant) kvs =
+  let full = dname ^ "." ^ c.Tast.vname in
   let seen = Hashtbl.create 8 in
   List.iter
     (fun (k, (v : Ast.expr)) ->
@@ -2603,7 +2695,7 @@ and check_case ctx ~want loc uname (c : Tast.variant) kvs =
         | None -> ());
        if Tast.vfield_index c k = None then
          Loc.failk "check/unknown-field" v.Ast.loc
-           ~notes:(declared_note ctx.env uname)
+           ~notes:(declared_note ctx.env dname)
            "%s has no field %s" full k;
        Hashtbl.add seen k v)
     kvs;
@@ -2616,7 +2708,7 @@ and check_case ctx ~want loc uname (c : Tast.variant) kvs =
       c.Tast.vfields
   in
   expect loc ~want
-    (mk loc (Types.Named uname) (Tast.MakeCase (uname, c.Tast.vname, fields)))
+    (mk loc (Types.Named dname) (Tast.MakeCase (dname, c.Tast.vname, fields)))
 
 and check_arr ctx ~want loc items =
   let elem_want =
@@ -2650,17 +2742,17 @@ and check_arr ctx ~want loc items =
 
 and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   let s = check ctx scrutinee in
-  (* What the arms are alternatives over. An [Option] is a two-case union
+  (* What the arms are alternatives over. An [Option] is a two-case data type
      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
+     them apart here rather than desugaring [Option] into a declared data type is
+     deliberate — [Option] is generic and no declared data type is, so the coat is
      the part that cannot yet be taken off. *)
   let subject =
     match s.Tast.ty with
     | Types.Option t -> `Option t
-    | Types.Named n when Hashtbl.mem ctx.env.unions n ->
-      `Union (Hashtbl.find ctx.env.unions n)
+    | Types.Named n when Hashtbl.mem ctx.env.datas n ->
+      `Data (Hashtbl.find ctx.env.datas 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
@@ -2673,8 +2765,20 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
         "match over the enum %s is not implemented — the lowering is a chain \
          of (= k :member), but a keyword has no case in the pattern type yet. \
          Use cond" n
+    (* An untagged union has nothing for the arms to be alternatives over.
+       This is not a milestone and not a missing lowering: [match] reads a tag
+       and decides, and the absence of a tag is the whole definition of this
+       type. Said by name, because the two kinds of union are one keyword
+       apart in the source and someone will write it. *)
+    | Types.Named n when Hashtbl.mem ctx.env.unions n ->
+      fail loc
+        "%s is a union, and there is nothing in one to match on: its members \
+         overlay the same bytes and nothing records which was written. Read \
+         the member you mean with (.member u), or keep a tag of your own \
+         beside it in a struct and match on that. A tagged alternative is \
+         what defdata is" n
     | other ->
-      fail loc "match works on an Option or a union, not on %s"
+      fail loc "match works on an Option or a data type, not on %s"
         (Types.to_string other)
   in
   (* Which case each arm names, and the type of each name it binds. This is the
@@ -2691,13 +2795,14 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
     | `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) ->
+    | `Data 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
+         data type, so [(Node l r)] is unambiguous even where two data types
+         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 full = u.Tast.dname ^ "." 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)
@@ -2706,7 +2811,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
       (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
+           u.Tast.dname
            (String.concat ", "
               (List.map (fun (v : Tast.variant) -> v.Tast.vname) u.Tast.cases))
        | Some (_, v) ->
@@ -2718,7 +2823,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
            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)
+             u.Tast.dname bare (List.length v.Tast.vfields)
              (if List.length v.Tast.vfields = 1 then "" else "s")
              (List.length names)
              (String.concat " "
@@ -2732,7 +2837,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   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
+     so each is checked from the state before the match and the data type of what
      they moved survives the join. Checked in sequence against one mutating set
      they would report the second arm's (free v) as a use after the first arm's
      move, which is a legal program refused. *)
@@ -2772,25 +2877,25 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
   ctx.dead <- !joined;
   (* 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
+     and there is no such value for most types; and the case a data type 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 ->
+    | `Data 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))
+           else Some (u.Tast.dname ^ "." ^ c.Tast.vname))
         u.Tast.cases
   in
   if not !saw_wild && missing <> [] then
-    (* The union's declaration, because that is where the case list this match
+    (* The data type's declaration, because that is where the case list this match
        failed to cover actually lives, and because adding a case there is what
        makes a match non-exhaustive in the first place. *)
     Loc.failk "check/non-exhaustive-match" loc
-      ~notes:(match subject with `Union u -> declared_note ctx.env u.Tast.uname
+      ~notes:(match subject with `Data u -> declared_note ctx.env u.Tast.dname
                                | _ -> [])
       "this match is not exhaustive — %s %s no arm. Add %s, or a _ arm for \
        the rest"
@@ -2802,23 +2907,35 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms =
 
 (* ── Places ────────────────────────────────────────────────────────── *)
 
-(* The target of [.field] is a struct, or one level of pointer to one. The
-   auto-deref is inserted here as a real node, so no backend re-derives it. *)
+(* The fields a name has, whether it is a struct or an untagged union. The two
+   are one record and differ only in what the offsets come out as, which is a
+   question for the layout and not for this — so [.x] is one path and not two,
+   and a union member is read with the accessor everything else is read with.
+   That is the whole of what makes punning ordinary code. *)
+and fields_named env n : Tast.structure option =
+  match Hashtbl.find_opt env.structs n with
+  | Some s -> Some s
+  | None -> Hashtbl.find_opt env.unions n
+
+(* The target of [.field] is a struct or an untagged union, or one level of
+   pointer to one. The auto-deref is inserted here as a real node, so no
+   backend re-derives it. *)
 and struct_target ctx (target : Ast.expr) : Tast.expr * string =
   let t = check ctx target in
+  let has n = fields_named ctx.env n <> None in
   match t.Tast.ty with
-  | Types.Named n when Hashtbl.mem ctx.env.structs n -> t, n
-  | Types.Ptr (Types.Named n) when Hashtbl.mem ctx.env.structs n ->
+  | Types.Named n when has n -> t, n
+  | Types.Ptr (Types.Named n) when has 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. *)
+  (* A data type'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
+     data type 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 ->
+    when Hashtbl.mem ctx.env.datas 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 ...), \
+      "%s is a data type, and a data type'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 ->
@@ -2843,7 +2960,7 @@ and check_place ctx loc (p : Ast.place) : Tast.place * Types.t =
          Loc.failk "check/unknown-name" loc "unknown name %s" name)
   | Ast.Pfield (target, name) ->
     let target, sname = struct_target ctx target in
-    let s = Hashtbl.find ctx.env.structs sname in
+    let s = Option.get (fields_named ctx.env sname) in
     (match Tast.field_index s name with
      | None ->
        Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
@@ -3174,9 +3291,9 @@ and file_guard ctx loc ~path_slot ~op mk_steps =
                [ mk loc Types.Unit (Tast.While (notok (), [ body ], [])) ]))
 
 (* Is this bare symbol the name of a type? Every table [resolve_name] will look
-   in, and the union table is one of them: a union is [Named] exactly as a
+   in, and the data type table is one of them: a data type is [Named] exactly as a
    struct is, so (vec-new Form) is as ordinary as (vec-new Cell). It was left
-   out when unions landed, which made the prelude's own (vec-new Form) fail
+   out when data types landed, which made the prelude's own (vec-new Form) fail
    with "nothing here says what (vec-new) is a Vec of" — a message about a
    missing annotation for a program that had written one. One list, read by
    both callers, so the next kind of type added cannot be added to one of
@@ -3191,6 +3308,7 @@ and type_named ctx n =
   || List.mem_assoc n ctx.env.subst
   || List.mem n Types.primitive_names
   || Hashtbl.mem ctx.env.structs n
+  || Hashtbl.mem ctx.env.datas n
   || Hashtbl.mem ctx.env.unions n
   || Hashtbl.mem ctx.env.enums n
   || Hashtbl.mem ctx.env.aliases n
@@ -4758,6 +4876,7 @@ and named_call ctx ~want loc name args =
     let rc =
       { Render.structs =
           Hashtbl.fold (fun _ v acc -> v :: acc) ctx.env.structs [];
+        datas = Hashtbl.fold (fun _ v acc -> v :: acc) ctx.env.datas [];
         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;
@@ -4900,18 +5019,18 @@ 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.unions name then
+      if Hashtbl.mem ctx.env.datas name then
         fail loc
-          "%s is a union type — a union value names the case too, as (%s.%s            {.field value ...})"
+          "%s is a data type — a data type 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
+        let dname, c = Hashtbl.find ctx.env.cases name in
         fail loc
-          "%s is a case of the union %s — write (%s.%s {.field value ...}), \
+          "%s is a case of the data type %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
+          name dname dname c.Tast.vname dname 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 ...})"
@@ -5161,7 +5280,7 @@ let rec const_int env (e : Ast.expr) : int64 option =
 
 let collect env (decls : Ast.decl list) =
   (* One pass over every declaration kind before any of the others, because
-     the tables below are per-kind — structs, unions, aliases, enums, functions
+     the tables below are per-kind — structs, data types, aliases, enums, functions
      and globals each have their own — and a collision between two of them
      would otherwise be found by LLVM, as [redefinition of function
      '@flan.item'], or not at all. A [defn item] and a [defvar item] are two
@@ -5190,9 +5309,12 @@ let collect env (decls : Ast.decl list) =
        | Ast.Defstruct (n, _) ->
          Hashtbl.replace env.locs n d.Ast.dloc;
          Hashtbl.replace env.structs n { Tast.sname = n; fields = [] }
+       | Ast.Defdata (n, _) ->
+         Hashtbl.replace env.locs n d.Ast.dloc;
+         Hashtbl.replace env.datas n { Tast.dname = n; cases = [] }
        | Ast.Defunion (n, _) ->
          Hashtbl.replace env.locs n d.Ast.dloc;
-         Hashtbl.replace env.unions n { Tast.uname = n; cases = [] }
+         Hashtbl.replace env.unions n { Tast.sname = n; fields = [] }
        | Ast.Defalias (n, t) -> Hashtbl.replace env.aliases n t
        | _ -> ())
     decls;
@@ -5310,15 +5432,15 @@ let collect env (decls : Ast.decl list) =
                   (Types.to_string f.Tast.fty))
            fields;
          Hashtbl.replace env.structs n { Tast.sname = n; fields }
-       | Ast.Defunion (n, vs) ->
-         (* A union with no cases has no value, so nothing could ever be given
+       | Ast.Defdata (n, vs) ->
+         (* A data type 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;
+             "%s declares no cases, so no value of it can exist — a data type is \
+              (defdata %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;
@@ -5334,18 +5456,19 @@ let collect env (decls : Ast.decl list) =
                     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
+                   and in the same words: a data type case's fields are a struct,
+                   the data type 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
+                   — a data type 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 \
+                          data type case that owns one makes the data type \
+                          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"
@@ -5355,12 +5478,104 @@ let collect env (decls : Ast.decl list) =
                 { Tast.vname = v.Ast.vname; vfields })
              vs
          in
-         Hashtbl.replace env.unions n { Tast.uname = n; cases };
+         Hashtbl.replace env.datas n { Tast.dname = 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
+       (* ── The untagged union ──────────────────────────────────────────
+          C's semantics, deliberately and in full: the members overlay one
+          storage, the size is the largest of them, the alignment the
+          strictest, and nothing anywhere records which member was written
+          last.
+
+          {2 What Flan says about reading a member that was not written}
+
+          It reads the bytes that are there, through that member's type. Not
+          undefined behaviour, and not a refusal either — a *definition*, and
+          this is the one place in the checker that chooses bytes over safety
+          on purpose, so it is worth saying why.
+
+          Refusing it was the alternative, and it would have made the feature
+          nothing: type punning *is* reading the member that was not written,
+          and both uses this type exists for are that read. Binding a C header
+          means holding the union the library holds and reading whichever
+          member the library's own tag says is live — a tag Flan cannot see,
+          because it is a field of the enclosing struct and the rule that
+          relates them is prose in a manual. Overlaying an f32 on a u32 to look
+          at its bits is the other use and is the same read. A checker that
+          refused it would be refusing the type.
+
+          So the promise is the one C's implementations actually make and
+          C's standard does not: the layout is the target's, the bytes are the
+          bytes, and a read is a reinterpretation of them. What is *not*
+          promised is anything about bytes never written — a member larger
+          than the one last stored reads its own size, and the tail is
+          indeterminate exactly as a struct's padding is. That is the honest
+          line, and it is narrower than it sounds: the ZII rule means a union
+          starts all-bytes-zero unless [uninit] says otherwise, so the tail is
+          zero rather than garbage in every program that did not ask for
+          garbage.
+
+          {2 uninit}
+
+          Allowed, unlike on a data type. The refusal there is not about
+          garbage — [uninit] is garbage everywhere and says so — it is that a
+          data type's tag *steers*, and a tag no case names falls past every
+          comparison in a [match] into a block LLVM is entitled to treat as
+          unreachable. An untagged union steers nothing. Reading a member of
+          one is already a reinterpretation of whatever bytes are there, so
+          [uninit] makes those bytes arbitrary and changes nothing else, which
+          is exactly what it means on an [i64].
+
+          {2 Why bool is not a member}
+
+          An [i1] loaded out of a byte that is neither 0 nor 1 is not a
+          [false], it is a value the optimiser is entitled to assume cannot
+          exist, and a union is the one type that can hand it one — write the
+          [u8] member 2, read the [bool] member. Nothing about that is visible
+          at the read, so it cannot be refused there. The alternative was to
+          load a union's bool as an [i8] and compare it against zero in both
+          backends, which is a correct answer and a real cost paid by every
+          bool in the language to make one type safe. Refused at the
+          declaration instead, where the message can name the replacement:
+          [u8], compared explicitly. The check below is recursive, because a
+          bool inside a struct member is the same byte.
+
+          {2 Why no member may be move-only}
+
+          Because nothing knows which member is live, so nothing can tear one
+          down. That is not a limitation of today's compiler, which is what
+          the struct and data type refusals above say about themselves; it is
+          a property of the type, and it does not go away when recursive
+          teardown lands. A [drop] of a union would have to free whichever
+          member is live and there is no such fact — freeing the wrong one is
+          a free of a pointer that was an f64 a moment ago. *)
+       | Ast.Defunion (n, ms) ->
+         if ms = [] then
+           fail loc
+             "%s declares no members, so it has no size and nothing could be \
+              read out of it — a union is (defunion %s [member Type ...])" n n;
+         let names = List.map (fun (f : Ast.field) -> f.Ast.fname) ms in
+         if List.length (List.sort_uniq compare names) <> List.length names then
+           fail loc "%s declares the same member twice" n;
+         let fields = List.map field ms in
+         List.iter
+           (fun (f : Tast.field) ->
+              if Types.is_move_only f.Tast.fty then
+                fail loc
+                  "%s's member %s is %s, which is move-only, and a union may \
+                   not own one: the members overlay one storage and nothing \
+                   records which was written, so nothing can free the right \
+                   one. Unlike a struct's, this is not waiting on recursive \
+                   teardown — there is no fact for teardown to read. Hold the \
+                   %s beside the union, or in a struct with a tag you check \
+                   yourself"
+                  n f.Tast.fname (Types.to_string f.Tast.fty)
+                  (Types.to_string f.Tast.fty))
+           fields;
+         Hashtbl.replace env.unions n { Tast.sname = n; fields }
        | Ast.Defn fn ->
          (* A signature that introduces a type variable is a *pattern*, not a
             signature: it goes in [gsigs] and the function goes nowhere near
@@ -5451,21 +5666,91 @@ let check_finite env =
     match Hashtbl.find_opt env.structs name with
     | Some s -> List.iter (fun (f : Tast.field) -> ty seen f.Tast.fty) s.Tast.fields
     | None ->
-      match Hashtbl.find_opt env.unions name with
-      | None -> ()
+      match Hashtbl.find_opt env.datas name with
       | Some u ->
         List.iter
           (fun (c : Tast.variant) ->
              List.iter (fun (f : Tast.field) -> ty seen f.Tast.fty) c.Tast.vfields)
           u.Tast.cases
+      | None ->
+        (* A union whose member is itself is the same infinite type a struct's
+           is — the size is the largest member and the largest member is the
+           whole thing. Nothing about overlaying storage makes the recursion
+           finite, so it is on the same walk rather than left to hang the
+           layout calculator. *)
+        match Hashtbl.find_opt env.unions name with
+        | None -> ()
+        | Some u ->
+          List.iter (fun (f : Tast.field) -> ty seen f.Tast.fty) u.Tast.fields
   and ty seen = function
     | Types.Named n -> walk seen n
     | Types.Array (_, e) | Types.Option e -> ty seen e
     | _ -> ()
   in
   Hashtbl.iter (fun n _ -> walk [] n) env.structs;
+  Hashtbl.iter (fun n _ -> walk [] n) env.datas;
   Hashtbl.iter (fun n _ -> walk [] n) env.unions
 
+(* No [bool] and no data type anywhere inside a union, at any depth — see the [Defunion] arm in
+   [collect] for why an [i1] read out of a union is the one punning hazard
+   Flan refuses rather than defines. It runs here, after [collect], because it
+   has to look through a member's *struct* to reach the fields inside it and
+   the struct table is only complete once every declaration has been walked. A
+   union that contains itself is impossible by [check_finite] above, so the
+   recursion terminates without a seen set — except through a [Ptr], which
+   this does not follow: a bool behind a pointer is a bool in someone else's
+   storage and is loaded from an address, not reinterpreted out of a blob. *)
+let check_union_members env =
+  let rec walk uname where (t : Types.t) =
+    match t with
+    | Types.Bool ->
+      fail (Option.value (Hashtbl.find_opt env.locs uname) ~default:Loc.unknown)
+        "%s is a bool, and a union may not hold one at any depth: writing a \
+         member that overlays it leaves a byte that is neither 0 nor 1, and \
+         an i1 with that byte in it is a value the optimiser is entitled to \
+         assume cannot exist. Hold a u8 in the union and compare it yourself"
+        where
+    (* An [Option] is deliberately not on this list, and the difference is
+       worth stating because a reader will ask. Its [match] lowers to a test of
+       the tag byte and a branch, so a scribbled tag reads as a [Some] with a
+       garbage payload — a number nobody stored, which is exactly what this
+       language says a union read is. A data type's lowers to a chain of
+       comparisons with an [unreachable] after the last one. *)
+    | Types.Array (_, e) | Types.Option e -> walk uname where e
+    | Types.Named n when Hashtbl.mem env.datas n ->
+      fail (Option.value (Hashtbl.find_opt env.locs uname) ~default:Loc.unknown)
+        "%s is %s, a data type, and a union may not hold one at any depth: a \
+         data type's tag steers every match over it, and overlaying another \
+         member leaves that tag arbitrary — a tag no case names falls past \
+         every comparison into a block the optimiser may treat as \
+         unreachable. This is the same refusal uninit on a data type gets, \
+         and it arrives here because a union is the other way to hand one \
+         bytes nobody wrote. Hold the %s beside the union"
+        where n n
+    | Types.Named n ->
+      (match Hashtbl.find_opt env.structs n with
+       | Some st ->
+         List.iter
+           (fun (f : Tast.field) ->
+              walk uname (where ^ "." ^ f.Tast.fname) f.Tast.fty)
+           st.Tast.fields
+       | None ->
+         match Hashtbl.find_opt env.unions n with
+         | None -> ()
+         | Some u ->
+           List.iter
+             (fun (f : Tast.field) ->
+                walk uname (where ^ "." ^ f.Tast.fname) f.Tast.fty)
+             u.Tast.fields)
+    | _ -> ()
+  in
+  Hashtbl.iter
+    (fun n (u : Tast.structure) ->
+       List.iter
+         (fun (f : Tast.field) -> walk n (n ^ "'s member " ^ f.Tast.fname) f.Tast.fty)
+         u.Tast.fields)
+    env.unions
+
 (* ── Declarations: pass 2, check bodies ────────────────────────────── *)
 
 let rec check_fn env (fn : Ast.fn) : Tast.fn =
@@ -5648,6 +5933,28 @@ let no_move_only_defconst loc n (ty : Types.t) =
        declared as. Write (defvar %s %s) and fill it in a function"
       n (Types.to_string ty) (Types.to_string ty) n (Types.to_string ty)
 
+(* A union member written into a global would have to be encoded into the blob
+   at link time, which is the byte-level encoder a data type case does not have
+   either — and a global's initialiser is a constant, while a union value is a
+   store. Refused here, where the message can name the way through, rather than
+   at the emitter as "this one is computed", which is true and says nothing. A
+   zeroed union needs none of this and is the ordinary declaration. Both kinds
+   of global, because a defconst reaches the same emitter by a different
+   path. *)
+let no_union_init env loc n what (v : Tast.expr) =
+  match v.Tast.ty, v.Tast.e with
+  (* The all-bytes-zero value is a constant and needs none of this, so it is
+     the one initialiser that goes through — which is what makes (U {}) and a
+     declaration with no value the same thing here as everywhere else. *)
+  | _, (Tast.Zero _ | Tast.Uninit _) -> ()
+  | Types.Named un, _ when Hashtbl.mem env.unions un ->
+    fail loc
+      "the global %s is the union %s, and a union member cannot be written \
+       into a %s: the initialiser is a constant and storing a member is a \
+       store. Leave it zeroed and write the member in a function"
+      n un what
+  | _ -> ()
+
 let check_global env (d : Ast.decl) : Tast.global option =
   let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = [];
       outer = []; outer_what = None; in_frames = None; loops = []; tail = false; in_defer = false; defer_ok = false; defer_block = "a nested form"; dead = []; borrow = false; owner = "<none>" } in
@@ -5661,7 +5968,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
       | Ast.Zeroed -> { Tast.e = Tast.Zero 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
+           whatever they were: a garbage f64 is a garbage number. A data type 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
@@ -5669,18 +5976,20 @@ let check_global env (d : Ast.decl) : Tast.global option =
            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 ->
+         | Types.Named un when Hashtbl.mem env.datas un ->
            fail d.Ast.dloc
-             "%s is a union, and uninit on one is refused: its tag steers \
+             "%s is a data type, 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
+             (match Hashtbl.find_opt env.datas 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
+      | Ast.Init v ->
+        let v = check (ctx ()) ~want:ty v in
+        no_union_init env d.Ast.dloc n "global" v; v
     in
     Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false }
   | Ast.Defconst (n, _, v) ->
@@ -5701,6 +6010,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
           loc = d.Ast.dloc }
       | _ -> check (ctx ()) ~want:ty v
     in
+    no_union_init env d.Ast.dloc n "constant" ginit;
     (* [env.consts] holds exactly the constants the folding pass consumed, so
        membership is the question "is this value in the program's shape?" *)
     Some { Tast.gname = n; gty = ty; ginit; gconst = true;
@@ -5756,6 +6066,7 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env =
      resync point that needs no resynchronising. *)
   collect env decls;
   check_finite env;
+  check_union_members env;
   let s = Loc.sink ~on:keep_going in
   ignore (Loc.caught s (fun () -> check_main env));
   (* Every generic body, checked once with its variables left abstract, and
@@ -5815,7 +6126,8 @@ let build_program ~keep_going (decls : Ast.decl list) : Tast.program * env =
     |> List.sort (fun (a : Tast.extern) b -> String.compare a.Tast.esym b.Tast.esym)
   in
   ({ Tast.structs = values (fun (s : Tast.structure) -> s.Tast.sname) env.structs;
-     unions = values (fun (u : Tast.union) -> u.Tast.uname) env.unions;
+     datas = values (fun (u : Tast.data) -> u.Tast.dname) env.datas;
+     unions = values (fun (u : Tast.structure) -> u.Tast.sname) env.unions;
      globals; externs; fns; cshim },
    env)
 
diff --git a/lib/cimport.ml b/lib/cimport.ml
index 6b9bdf0..bc63572 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -142,8 +142,14 @@ type cfn = {
   cloc     : Loc.t;                   (* the line of the header it is on *)
 }
 
-(* One C struct, for checking a [defstruct] against. *)
-type crecord = { rname : string; rfields : (string * string) list }
+(* One C record, for checking a [defstruct] or a [defunion] against. [runion]
+   is which of the two it was declared as, and it is on the record rather than
+   inferred at the comparison because the two are checked by different rules:
+   a struct's members are ordered and a union's are not, and matching a
+   [defstruct] against a C union would report a field order that means
+   nothing. *)
+type crecord =
+  { rname : string; rfields : (string * string) list; runion : bool }
 
 type dump = {
   fns      : cfn list;
@@ -292,8 +298,17 @@ let read_dump ~header (root : Cjson.t) : dump =
          (* A bitfield has no address and no Flan spelling; a record holding
             one is not one this can check, so it is not recorded and the
             [defstruct] beside it is left unchecked rather than checked
-            wrongly. Same for an unnamed field, which is an anonymous union or
-            struct. *)
+            wrongly. Same for an unnamed field, which is an *anonymous* union
+            or struct — it has no name for a Flan field to carry and no way to
+            reach its members, so there is still nothing to compare.
+
+            What is no longer skipped is the case this used to be read as
+            covering all unions: a record with a *named* union member. That
+            field has a name and a type, [union Overlay], and now that Flan has
+            a union of its own the name resolves to a [defunion] and the whole
+            record is checked field by field like any other. The gap that
+            remains is the anonymous one, and it is a gap in the Flan side
+            rather than here — there is nothing to declare. *)
          let ok =
            List.for_all
              (fun f ->
@@ -302,7 +317,11 @@ let read_dump ~header (root : Cjson.t) : dump =
                     && Cjson.str "name" f <> None))
              (Cjson.arr "inner" d)
          in
-         if ok then records := { rname = nm; rfields } :: !records
+         if ok then
+           records :=
+             { rname = nm; rfields;
+               runion = Cjson.str "tagUsed" d = Some "union" }
+             :: !records
        (* An enumerator with no [= n] carries no [ConstantExpr] in the dump at
           all, so the value has to be counted the way C counts it: one more
           than the one before, starting at zero. That is not an edge case —
@@ -352,6 +371,7 @@ let read_dump ~header (root : Cjson.t) : dump =
    it either finds a Flan name for a C type here or refuses the function. *)
 type env = {
   known_structs : string list;   (* the package's defstruct names *)
+  known_unions  : string list;   (* and its defunion names *)
   known_enums   : string list;   (* its defenum names *)
   d             : dump;
 }
@@ -431,6 +451,10 @@ let width_varies =
    describes, an enum, or nothing this can hold. *)
 let rec named env (n : string) : Ast.texpr =
   if List.mem n env.known_structs then tname n
+  (* A [union Overlay] parameter or field renders as the package's [defunion
+     Overlay], on the same terms a struct does: the package says the layout
+     exists and [check_unions] below says whether it agrees. *)
+  else if List.mem n env.known_unions then tname n
   else if List.mem n env.known_enums then tname n
   else if List.mem n env.d.enums then
     (* A C enum is an int, which is what [Shim] lowers a Flan [defenum] to, so
@@ -928,17 +952,26 @@ let ptr_agrees env ~(c : string) (t : Ast.texpr) =
 let agrees_c env ~(c : string) (want : Ast.texpr) (got : Ast.texpr) =
   agrees env want got || ptr_agrees env ~c got
 
+(* The header's record of a given name and a given kind. [want_union] is part
+   of the lookup rather than checked afterwards because a name is only one
+   half of the question: a [defstruct Overlay] and a C [union Overlay] are not
+   the same layout with a spelling disagreement, they are two different
+   layouts, and running the struct comparison over the union's members would
+   report a field order where a union has none. A kind mismatch is reported by
+   the caller, which has the Flan declaration to name. *)
+let record_named (d : dump) ~want_union n =
+  let ofkind r = r.runion = want_union in
+  match List.find_opt (fun r -> r.rname = n && ofkind r) d.records with
+  | Some r -> Some r
+  | None ->
+    (* [defstruct Texture2D] against a header whose record is [Texture] and
+       whose typedef says so. *)
+    (match List.assoc_opt n d.typedefs with
+     | Some u -> List.find_opt (fun r -> r.rname = bare u && ofkind r) d.records
+     | None -> None)
+
 let check_structs ~env ~(structs : (string * Ast.field list) list) (d : dump) =
-  let record n =
-    match List.find_opt (fun r -> r.rname = n) d.records with
-    | Some r -> Some r
-    | None ->
-      (* [defstruct Texture2D] against a header whose record is [Texture] and
-         whose typedef says so. *)
-      (match List.assoc_opt n d.typedefs with
-       | Some u -> List.find_opt (fun r -> r.rname = bare u) d.records
-       | None -> None)
-  in
+  let record n = record_named d ~want_union:false n in
   (* Names and widths both. Order is what a permuted [defstruct] gets wrong and
      what docs/BUILT.md says only a test can catch; width is the other half of the
      same hazard and the one it calls out by name — [f64] where the library
@@ -977,10 +1010,103 @@ let check_structs ~env ~(structs : (string * Ast.field list) list) (d : dump) =
   List.filter_map
     (fun (n, (fs : Ast.field list)) ->
        match record n with
-       | None -> None
-       | Some r -> Option.map (fun m -> (n, m)) (field_mismatch fs r))
+       | Some r -> Option.map (fun m -> (n, m)) (field_mismatch fs r)
+       (* The mirror of the finding [check_unions] makes, and it has to be
+          here or the kind mismatch goes quiet in one of its two directions:
+          asking for a struct of this name finds nothing when the header's
+          record is a union, and "nothing" is how a package the header says
+          nothing about is reported. Two different layouts under one name is
+          not that. *)
+       | None ->
+         match record_named d ~want_union:true n with
+         | Some r ->
+           Some (n,
+                 Printf.sprintf
+                   "%s is a union in the header and a defstruct here — its \
+                    members are laid out over one another there and one after \
+                    another here" r.rname)
+         | None -> None)
     structs
 
+(* The same claim for a [defunion], and it is deliberately a second function
+   rather than a flag on the one above.
+
+   What a struct check is *for* is order: a permuted [Texture2D] reads as five
+   plausible numbers, and the offsets are what moved. A union has no order to
+   permute. Every member is at offset zero, so a [defunion] that lists its
+   members in a different order from the header is not merely acceptable, it
+   is the same type — reporting it would be a false finding, and a check that
+   cries wolf is how a real disagreement gets ignored.
+
+   So: members by name, and the type of each. A member the header has and the
+   [defunion] does not is still a finding, and this is the one that matters
+   most, because it is the one that changes the *size*: a union missing its
+   widest member is narrower than C's, and a struct that holds one by value
+   then puts every field after it in the wrong place. The reverse — a member
+   Flan declares and C does not — is a finding too, for the same reason read
+   the other way, and because it is usually a typo in a name.
+
+   A member whose C type this cannot render says nothing, exactly as a
+   struct's does: the check is a second opinion, and having no opinion is not
+   a disagreement. *)
+let check_unions ~env ~(unions : (string * Ast.field list) list) (d : dump) =
+  let mismatch (ms : Ast.field list) (r : crecord) =
+    let cnames = List.map (fun (n, _) -> kebab n) r.rfields in
+    let fnames = List.map (fun (f : Ast.field) -> f.Ast.fname) ms in
+    let missing = List.filter (fun n -> not (List.mem n fnames)) cnames in
+    let extra = List.filter (fun n -> not (List.mem n cnames)) fnames in
+    if missing <> [] then
+      Some
+        (Printf.sprintf
+           "%s has the member%s %s and the defunion does not — a union is as \
+            wide as its widest member, so a missing one makes the whole type \
+            narrower than C's"
+           r.rname (if List.length missing = 1 then "" else "s")
+           (String.concat " " missing))
+    else if extra <> [] then
+      Some
+        (Printf.sprintf
+           "the defunion has the member%s %s and %s does not"
+           (if List.length extra = 1 then "" else "s")
+           (String.concat " " extra) r.rname)
+    else
+      List.find_map
+        (fun (f : Ast.field) ->
+           match
+             List.find_opt (fun (cn, _) -> kebab cn = f.Ast.fname) r.rfields
+           with
+           | None -> None
+           | Some (_, ct) ->
+             match (try Some (value_ty env ct) with Refused _ -> None) with
+             | None -> None
+             | Some want ->
+               let a = ty_source want and b = ty_source f.Ast.fty in
+               if agrees env want f.Ast.fty then None
+               else
+                 Some
+                   (Printf.sprintf
+                      "member %s is %s in the defunion and %s (%s) in %s"
+                      f.Ast.fname b a ct r.rname))
+        ms
+  in
+  List.filter_map
+    (fun (n, (ms : Ast.field list)) ->
+       match record_named d ~want_union:true n with
+       | Some r -> Option.map (fun m -> (n, m)) (mismatch ms r)
+       (* The header has the name, and it is a struct. Two different layouts
+          under one name is worth saying out loud — it is the same class of
+          finding a permuted struct is, and the fix is the other keyword. *)
+       | None ->
+         match record_named d ~want_union:false n with
+         | Some r ->
+           Some (n,
+                 Printf.sprintf
+                   "%s is a struct in the header and a defunion here — its \
+                    members are laid out one after another there and over one \
+                    another here" r.rname)
+         | None -> None)
+    unions
+
 (* ── Checking the package's constants against the header's ─────────── *)
 
 (* The half of the claim that was missing, and the one with the worst failure
@@ -1305,10 +1431,10 @@ let dump_of ~loc ~header ~flags =
     Hashtbl.replace dumps k d;
     d
 
-let env_of ~known_structs ~known_enums d = { known_structs; known_enums; d }
+let env_of ~known_structs ~known_unions ~known_enums d =
+  { known_structs; known_unions; known_enums; d }
 
-let header ~loc ~header:h ~flags ~known_structs ~known_enums ~taken ~bound_syms
-    ~config =
+let header ~loc ~header:h ~flags ~known_structs ~known_unions ~known_enums ~taken ~bound_syms ~config =
   let k =
     (* Sorted, because neither the taken table nor the declaration order is a
        fact about the package — two loads of the same file that enumerate them
@@ -1317,6 +1443,7 @@ let header ~loc ~header:h ~flags ~known_structs ~known_enums ~taken ~bound_syms
     String.concat "\000"
       (header_key ~header:h ~flags
        :: "\001" :: sorted known_structs
+       @ ("\001" :: sorted known_unions)
        @ ("\001" :: sorted known_enums)
        @ ("\001" :: sorted (Hashtbl.fold (fun n () acc -> n :: acc) taken []))
        @ ("\001" :: sorted bound_syms)
@@ -1333,7 +1460,7 @@ let header ~loc ~header:h ~flags ~known_structs ~known_enums ~taken ~bound_syms
   | Some r -> r
   | None ->
     let d = dump_of ~loc ~header:h ~flags in
-    let env = env_of ~known_structs ~known_enums d in
+    let env = env_of ~known_structs ~known_unions ~known_enums d in
     let r = (of_dump ~env ~taken ~bound_syms ~config d, d, env) in
     Hashtbl.replace imports k r;
     r
@@ -1560,7 +1687,8 @@ let regenerate ~loc ~header:h ~flags ~(ds : Ast.decl list) ~config ~out =
   in
   let imported, dump, env =
     header ~loc ~header:h ~flags ~known_structs:(List.map fst structs)
-      ~known_enums:(List.map fst enums) ~taken ~bound_syms ~config
+      ~known_unions:[] ~known_enums:(List.map fst enums) ~taken ~bound_syms
+      ~config
   in
   let gstructs = check_structs ~env ~structs dump in
   let gsigs = diff_bound ~env ~bound dump in
diff --git a/lib/dev.ml b/lib/dev.ml
index 0ffc092..c671d76 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -864,26 +864,27 @@ let layout t ~ty =
   | None ->
     (* Two types the checker knows and this op cannot describe. An enum's
        members are erased to i32 before [Tast.program] exists, which is the
-       same fact that makes a defenum unreloadable; a union is declared and
+       same fact that makes a defenum unreloadable; a data type is declared and
        has no values yet. Either way, saying which kind it is beats "no such
        type" for a name that plainly exists. *)
     if Hashtbl.mem t.session.Session.env.Check.enums ty then
       error (ty ^ " is an enum, not a struct; its members are erased to i32")
     else if
-      List.exists (fun (u : Tast.union) -> String.equal u.Tast.uname ty)
-        t.session.Session.program.Tast.unions
+      List.exists (fun (u : Tast.data) -> String.equal u.Tast.dname ty)
+        t.session.Session.program.Tast.datas
     then
-      (* Unions have landed, so "milestone 6" was stale — but what replaces it
-         is not a layout. This op's reply is a flat [:fields] list, and a union
+      (* Data types have landed, so "milestone 6" was stale — but what replaces it
+         is not a layout. This op's reply is a flat [:fields] list, and a data type
          is a tag and one payload per case: there is no one field list to
          answer with, and flattening the cases into one would describe storage
          no value ever has. So it says which kind of type this is, and where
          the question it was probably asked for *is* answered — the renderer
-         walks a union now, so a union value prints in a frame's locals and at
+         walks a data type now, so a data type value prints in a frame's
+         locals and at
          `C-x C-e' with its case and that case's fields. *)
       error
         (ty
-         ^ " is a union, not a struct; a union is a tag and one payload per case, so it has no single field list for this op to answer with. Its value renders with its case and fields in a frame's locals and at C-x C-e")
+         ^ " is a data type, not a struct; a data type is a tag and one payload per case, so it has no single field list for this op to answer with. Its value renders with its case and fields in a frame's locals and at C-x C-e")
     else
       let suffix = "/" ^ ty in
       let candidates =
@@ -1381,6 +1382,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t)
   let extra = ref [] and nslots = ref 0 in
   let c =
     { Render.structs = s.Session.program.Tast.structs;
+      datas = s.Session.program.Tast.datas;
       unions = s.Session.program.Tast.unions;
       enums =
         Hashtbl.fold (fun k v acc -> (k, v) :: acc) s.Session.env.Check.enums [];
diff --git a/lib/emit.ml b/lib/emit.ml
index fdae2c3..b9efc14 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -220,12 +220,16 @@ 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
+  (* The declared data types, by name. [Types.Named] covers both a struct and a
+     data type, 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
+     a data type is a type like any other everywhere except at its layout, its
      construction and its match. *)
-  unions  : (string, Tast.union) Hashtbl.t;
+  datas  : (string, Tast.data) Hashtbl.t;
+  (* The untagged unions, by name. A third table for the same [Types.Named],
+     on the same principle as the second: the name says which, and the members
+     are a field list whose offsets are all zero. *)
+  unions  : (string, Tast.structure) 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. *)
@@ -268,8 +272,14 @@ type m = {
    Spelled once so the [define] sites and [finish] cannot disagree. *)
 let attrs m = if m.sanitize then " #0" else ""
 
+(* The type of one member, of a struct or of a union alike — the index means
+   the same thing in both, and only the offset it lands at differs. *)
 let field_ty m sn i =
-  let s = Hashtbl.find m.structs sn in
+  let s =
+    match Hashtbl.find_opt m.structs sn with
+    | Some s -> s
+    | None -> Hashtbl.find m.unions sn
+  in
   (List.nth s.Tast.fields i).Tast.fty
 
 (* Size and alignment in bytes. *)
@@ -300,7 +310,7 @@ let rec lay m (t : Types.t) : int * int =
        in
        s, a
      | None ->
-       match Hashtbl.find_opt m.unions n with
+       match Hashtbl.find_opt m.datas 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
@@ -315,7 +325,10 @@ let rec lay m (t : Types.t) : int * int =
                               Types.Int (int_kind (align * 8))) ]
            in
            s, a
-       | None -> failwith ("no layout for struct " ^ n))
+       | None ->
+         match Hashtbl.find_opt m.unions n with
+         | Some u -> union_lay m u
+         | None -> failwith ("no layout for struct " ^ n))
   | Types.Var _ -> failwith ("no layout for " ^ Types.to_string t)
 
 (* Size, alignment, and the offset of every member. *)
@@ -332,11 +345,29 @@ 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
+(* C's union rule, and it is the only thing about this type that is not a
+   struct's: room for the largest member, the alignment the strictest member
+   needs, and the size rounded up to that alignment so an array of the union
+   keeps every element aligned. Written through [lay] and [align_up] rather
+   than with arithmetic of its own, so it cannot drift from the payload
+   measurement below — which is the same rule over a data type's cases, and
+   was here first. *)
+and union_lay m (u : Tast.structure) : int * int =
+  let align = ref 1 and size = ref 0 in
+  List.iter
+    (fun (fl : Tast.field) ->
+       let s, a = lay m fl.Tast.fty in
+       let a = if a < 1 then 1 else a in
+       if a > !align then align := a;
+       if s > !size then size := s)
+    u.Tast.fields;
+  align_up !size !align, !align
+
+(* The size and alignment of a data type'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
+   to it so the blob divides evenly into [k x iA]. A data type of payload-less
    cases has a zero-size payload and is a bare tag. *)
-and payload_lay m (u : Tast.union) : int * int =
+and payload_lay m (u : Tast.data) : int * int =
   let align = ref 1 and size = ref 0 in
   List.iter
     (fun (c : Tast.variant) ->
@@ -440,7 +471,7 @@ let rec dty m d (t : Types.t) : int =
              (List.map (fun (fl : Tast.field) -> (fl.Tast.fname, fl.Tast.fty))
                 st.Tast.fields)
          | None ->
-           match Hashtbl.find_opt m.unions sn with
+           match Hashtbl.find_opt m.datas 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
@@ -455,7 +486,37 @@ let rec dty m d (t : Types.t) : int =
                      [ ("payload",
                         Types.Array (Int64.of_int (size / align),
                                      Types.Int (int_kind (align * 8)))) ]))
-           | None -> failwith ("no debug type for struct " ^ sn))
+           | None ->
+             (* DW_TAG_union_type, which is the one place a DWARF tag says
+                exactly what the Flan type is — every member at offset zero,
+                each with its own type. lldb's C support reads this and prints
+                every member of a union side by side, which is the only honest
+                thing to show: the debugger cannot know which one is live
+                either. *)
+             match Hashtbl.find_opt m.unions sn with
+             | Some u ->
+               let id = dalloc d in
+               Hashtbl.replace d.dtys key id;
+               let size, al = union_lay m u in
+               let ms =
+                 List.map
+                   (fun (fl : Tast.field) ->
+                      let fs, fa = lay m fl.Tast.fty in
+                      let base = dty m d fl.Tast.fty in
+                      dnode d
+                        (Printf.sprintf
+                           "!DIDerivedType(tag: DW_TAG_member, name: \"%s\", baseType: !%d, size: %d, align: %d, offset: 0)"
+                           (dstr fl.Tast.fname) base (fs * 8) (fa * 8)))
+                   u.Tast.fields
+               in
+               dput d id
+                 (Printf.sprintf
+                    "!DICompositeType(tag: DW_TAG_union_type, name: \"%s\", size: %d, align: %d, elements: !{%s})"
+                    (dstr sn) (size * 8) (al * 8)
+                    (String.concat ", "
+                       (List.map (fun i -> Printf.sprintf "!%d" i) ms)));
+               id
+             | 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. *)
@@ -1110,8 +1171,8 @@ 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.MakeCase (dname, case, fields) ->
+    emit_make_case f dname 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
@@ -1248,6 +1309,16 @@ and addr f (e : Tast.expr) : string =
 
 and field_addr f (target : Tast.expr) i =
   let base = addr f target in
+  (* A union's members all start where the union starts, so the address of one
+     is the address of the whole thing and there is no gep to do. The member's
+     own type is what the load or the store that follows uses, which is what
+     makes the read a reinterpretation of the bytes — with opaque pointers
+     that is the entire implementation of punning, and the [i32] and the [f32]
+     views of one storage differ in nothing but the instruction that reads
+     them. *)
+  match target.Tast.ty with
+  | Types.Named n when Hashtbl.mem f.md.unions n -> base
+  | _ ->
   (* An Option is { i8, T } and has no declared name to gep through, so its
      layout is spelled out instead. Nothing in the surface language reaches a
      field of one -- [match] and [some] are how an Option is opened -- but the
@@ -1312,26 +1383,26 @@ 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
+(* A data type 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
+and emit_make_case f dname case fields =
+  let ty = Types.Named dname in
+  let u = Hashtbl.find f.md.datas dname in
   let tag = match Tast.case_index u case with
     | Some (i, _) -> i
-    | None -> failwith ("no case " ^ case ^ " of " ^ uname)
+    | None -> failwith ("no case " ^ case ^ " of " ^ dname)
   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 "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 0" tp (sname dname) 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
+    let pp = payload_addr f dname tmp in
+    let cty = sname (dname ^ "." ^ case) in
     List.iteri
       (fun i (p : Tast.expr) ->
          let v = value f p in
@@ -1342,26 +1413,26 @@ and emit_make_case f uname case fields =
   end;
   load f tmp ty
 
-(* The payload blob's address. A union with no payload has no field 1, so this
+(* The payload blob's address. A data type 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 =
+and payload_addr f dname base =
   let p = fresh f in
-  ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 1" p (sname uname) base;
+  ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 1" p (sname dname) base;
   p
 
-(* The address of one field of one case of a union value. The single place in
+(* The address of one field of one case of a data type 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
+  let dname = 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 pp = payload_addr f dname 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 (sname (dname ^ "." ^ case)) pp i;
   p
 
 and aggregate f ty parts =
@@ -1787,17 +1858,17 @@ and emit_while f c body latch =
 and emit_match f ty scrut arms =
   (* 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
+     data type 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 =
+  let dname =
     match scrut.Tast.ty with
-    | Types.Named n when Hashtbl.mem f.md.unions n -> Some n
+    | Types.Named n when Hashtbl.mem f.md.datas n -> Some n
     | Types.Option _ -> None
     | t -> failwith ("match on " ^ Types.to_string t)
   in
   let tag, read_tag, bind_of =
-    match uname with
+    match dname with
     | None ->
       let sv = value f scrut in
       let sty = ll scrut.Tast.ty in
@@ -1813,7 +1884,7 @@ and emit_match f ty scrut arms =
          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
+      let u = Hashtbl.find f.md.datas 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
@@ -2551,22 +2622,22 @@ 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
+  (* A data type'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, _) ->
+  | Tast.MakeCase (dname, case, _) ->
     fail e.Tast.loc
-      "a global cannot be initialised with %s.%s — a union's payload is a \
+      "a global cannot be initialised with %s.%s — a data type'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
+      dname case dname
+      (match Hashtbl.find_opt m.datas dname with
        | Some { Tast.cases = c :: _; _ } -> c.Tast.vname
        | _ -> "its first case")
   | _ ->
@@ -2808,7 +2879,8 @@ 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; unions = Hashtbl.create 16;
+    structs = Hashtbl.create 16; datas = Hashtbl.create 16;
+    unions = Hashtbl.create 16;
     globals = Hashtbl.create 16;
     externs = Hashtbl.create 32;
     checks; dev; known; nstr = 0; nfi = 0; sanitize;
@@ -2816,7 +2888,9 @@ let new_module ~checks ~dev ~known ?(debug = false) ?(sanitize = false)
   } 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)
+  List.iter (fun (u : Tast.data) -> Hashtbl.replace m.datas u.Tast.dname u)
+    p.Tast.datas;
+  List.iter (fun (u : Tast.structure) -> Hashtbl.replace m.unions u.Tast.sname u)
     p.Tast.unions;
   List.iter (fun (g : Tast.global) -> Hashtbl.replace m.globals g.Tast.gname g.Tast.gty)
     p.Tast.globals;
@@ -2829,7 +2903,20 @@ 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
+  (* A union is its blob and nothing else: [k x iA], where A is the alignment
+     the strictest member needs and k*A is the size of the largest. LLVM has no
+     union type, and this is the shape clang gives one — the same shape the
+     data type payload below uses, for the same reason, which is that it makes
+     LLVM align the storage without an explicit [align] anywhere. Nothing geps
+     into it: a member is read through the union's own address. *)
+  List.iter
+    (fun (u : Tast.structure) ->
+       let size, align = union_lay m u in
+       Buffer.add_string m.out
+         (Printf.sprintf "%s = type { [%d x i%d] }\n" (sname u.Tast.sname)
+            (if align = 0 then 0 else size / align) (align * 8)))
+    p.Tast.unions;
+  (* A data type 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.
@@ -2841,25 +2928,25 @@ let new_module ~checks ~dev ~known ?(debug = false) ?(sanitize = false)
      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) ->
+    (fun (u : Tast.data) ->
        List.iter
          (fun (c : Tast.variant) ->
             Buffer.add_string m.out
               (Printf.sprintf "%s = type { %s }\n"
-                 (sname (u.Tast.uname ^ "." ^ c.Tast.vname))
+                 (sname (u.Tast.dname ^ "." ^ c.Tast.vname))
                  (String.concat ", "
                     (List.map (fun (f : Tast.field) -> ll f.Tast.fty)
                        c.Tast.vfields))))
          u.Tast.cases)
-    p.Tast.unions;
+    p.Tast.datas;
   List.iter
-    (fun (u : Tast.union) ->
+    (fun (u : Tast.data) ->
        let size, align = payload_lay m u in
        Buffer.add_string m.out
-         (Printf.sprintf "%s = type { i32%s }\n" (sname u.Tast.uname)
+         (Printf.sprintf "%s = type { i32%s }\n" (sname u.Tast.dname)
             (if size = 0 then ""
              else Printf.sprintf ", [%d x i%d]" (size / align) (align * 8))))
-    p.Tast.unions;
+    p.Tast.datas;
   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/expand.ml b/lib/expand.ml
index 9cef480..a179009 100644
--- a/lib/expand.ml
+++ b/lib/expand.ml
@@ -19,10 +19,10 @@
    offset 8. Those three numbers are the whole agreement between this file and
    the compiled macro, and they are not taken on trust — test_acceptance.ml's
    "Form's image format" asks LLVM for each of them through the same ptrtoint
-   oracle the DWARF offsets go through. Change the prelude's defunion and that
+   oracle the DWARF offsets go through. Change the prelude's defdata and that
    test says which number moved.
 
-   The tag is the case's position in the prelude's (defunion Form ...), which
+   The tag is the case's position in the prelude's (defdata Form ...), which
    is why that list is a layout contract and says so. *)
 
 let form_size = 24
@@ -48,7 +48,7 @@ let tag_of_int = function
     failwith
       (Printf.sprintf
          "a macro returned a Form with tag %ld, and Form has nine cases. The \
-          prelude's (defunion Form ...) and lib/expand.ml's tag list are one \
+          prelude's (defdata Form ...) and lib/expand.ml's tag list are one \
           contract and have come apart"
          n)
 
diff --git a/lib/load.ml b/lib/load.ml
index b1fc2d3..b2d01df 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -308,6 +308,14 @@ let qualify_decl owned alias (d : Ast.decl) : Ast.decl =
                     rename_expr owned alias [] v)
     | Ast.Defstruct (n, fs) ->
       Ast.Defstruct (qualify alias n, List.map (rename_field owned alias) fs)
+    (* An untagged union imports exactly as a struct does, and for the reason
+       the data type above does not: it is a field list and a layout, with no
+       case table for the use site to resolve names against. The FFI is the
+       use that asked for it — a package binding a C library holds the union
+       its header declares, and the file that imports the package has to be
+       able to name the type. *)
+    | Ast.Defunion (n, ms) ->
+      Ast.Defunion (qualify alias n, List.map (rename_field owned alias) ms)
     | Ast.Defvar (n, t, init) ->
       Ast.Defvar (qualify alias n, Option.map (rename_texpr owned alias) t,
                   (match init with
@@ -328,8 +336,9 @@ let qualify_decl owned alias (d : Ast.decl) : Ast.decl =
        than anything a user wrote. *)
     | Ast.Import (a, _) ->
       fail loc "internal: the import of %s was not resolved before qualifying" a
-    | Ast.Defunion (n, _) ->
-      fail loc "%s is a union, and an imported union is not implemented yet \
+    | Ast.Defdata (n, _) ->
+      fail loc "%s is a data type, and an imported data type is not \
+               implemented yet \
                 (milestone 4)" n
   in
   { d with Ast.d = k }
@@ -358,7 +367,7 @@ let qualify_decl owned alias (d : Ast.decl) : Ast.decl =
    binders tracked are the ones a macro body can hold — its own parameter,
    [let], [loop], [fn] and [dotimes]. A [match] pattern's names and a
    [restart-case] clause's parameters are not tracked, which is a gap and a
-   narrow one: it takes a macro body that both destructures a union and binds a
+   narrow one: it takes a macro body that both destructures a data type and binds a
    name the package also declares at the top level. *)
 
 let rec form_syms (f : Form.t) acc =
@@ -592,8 +601,8 @@ let decl_uses acc (d : Ast.decl) =
   match d.Ast.d with
   | Ast.Package _ | Ast.Import _ | Ast.Defenum _ -> ()
   | Ast.Defalias (_, t) -> texpr_uses acc t
-  | Ast.Defstruct (_, fs) -> List.iter field fs
-  | Ast.Defunion (_, vs) ->
+  | Ast.Defstruct (_, fs) | Ast.Defunion (_, fs) -> List.iter field fs
+  | Ast.Defdata (_, vs) ->
     List.iter (fun (v : Ast.variant) -> List.iter field v.Ast.vfields) vs
   | Ast.Defn f -> fn f
   (* Both declaration forms name types in their signature and nothing else.
@@ -922,6 +931,13 @@ let rec import ~seen ~open_ ~loc alias dir =
                     | Ast.Defstruct (n, _) -> Some n
                     | _ -> None)
                  ds
+             and known_unions =
+               List.filter_map
+                 (fun (d : Ast.decl) ->
+                    match d.Ast.d with
+                    | Ast.Defunion (n, _) -> Some n
+                    | _ -> None)
+                 ds
              and enums =
                List.filter_map
                  (fun (d : Ast.decl) ->
@@ -952,7 +968,7 @@ let rec import ~seen ~open_ ~loc alias dir =
              in
              let config = binding_config dir in
              let r, dump, env =
-               Cimport.header ~loc ~header:h ~flags ~known_structs
+               Cimport.header ~loc ~header:h ~flags ~known_structs ~known_unions
                  ~known_enums:(List.map fst enums) ~taken ~bound_syms ~config
              in
              (* The point of reading the header, and the reason it is not
@@ -996,6 +1012,29 @@ let rec import ~seen ~open_ ~loc alias dir =
                     "the defstruct %s disagrees with %s: %s" n h why)
                (Cimport.check_structs ~env
                   ~structs:(List.map (fun (n, fs, _) -> (n, fs)) structs) dump);
+             (* And the same claim for the package's unions, which the header
+                read could not make at all until Flan had a union: a record
+                with a union member was skipped entirely, so the [defstruct]
+                beside it went unchecked as well. *)
+             let unions =
+               List.filter_map
+                 (fun (d : Ast.decl) ->
+                    match d.Ast.d with
+                    | Ast.Defunion (n, ms) -> Some (n, ms, d.Ast.dloc)
+                    | _ -> None)
+                 ds
+             in
+             List.iter
+               (fun (n, why) ->
+                  let at =
+                    List.find_map
+                      (fun (m, _, l) -> if String.equal m n then Some l else None)
+                      unions
+                  in
+                  fail (Option.value ~default:loc at)
+                    "the defunion %s disagrees with %s: %s" n h why)
+               (Cimport.check_unions ~env
+                  ~unions:(List.map (fun (n, ms, _) -> (n, ms)) unions) dump);
              (* And the hand-written bindings, against the header's own
                 signatures. These are the lines the importer deliberately
                 leaves alone, which is exactly why they are the ones nothing
diff --git a/lib/macro.ml b/lib/macro.ml
index 7be9038..26de4f2 100644
--- a/lib/macro.ml
+++ b/lib/macro.ml
@@ -108,7 +108,7 @@ let building = ref false
    depends on a macro *removed*. Directly or transitively, because a function
    calling a dropped one is as unbuildable as the dropped one itself.
 
-   Only [defn]s are dropped. A [defstruct], [defunion], [defalias], [defenum]
+   Only [defn]s are dropped. A [defstruct], [defdata], [defalias], [defenum]
    or [defvar] stays whatever it names: the functions that survive still
    mention those types, and a reduced prelude missing them would not check.
    There used to be a sharper reason — [Parse.prelude_types] memoised the
diff --git a/lib/parse.ml b/lib/parse.ml
index bdfb134..a511938 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -455,7 +455,8 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
      a head, which is the same property that makes a quasiquoted macro call
      output rather than a dependency. Building a declaration as a value is what
      a macro is for. *)
-  | Sym ("defmacro" | "defn" | "defvar" | "defconst" | "defstruct" | "defunion"
+  | Sym ("defmacro" | "defn" | "defvar" | "defconst" | "defstruct" | "defdata"
+        | "defunion"
         | "defenum" | "defalias" | "import" as name) ->
     fail f
       "%s is a top-level declaration, not an expression. A quasiquoted one is \
@@ -850,10 +851,55 @@ let rec decl (f : Form.t) : Ast.decl =
      | [ n; { v = Vec fs; _ } ] -> mk (Ast.Defstruct (sym n, fields f fs))
      | _ -> fail f "defstruct is (defstruct Name [field Type ...])")
 
+  | List ({ v = Sym "defdata"; _ } :: args) ->
+    (match args with
+     | [ n; { v = Vec vs; _ } ] -> mk (Ast.Defdata (sym n, List.map variant vs))
+     | _ -> fail f "defdata is (defdata Name [(Case [field Type ...]) ...])")
+
+  (* C's union: one storage, as many ways of reading it as there are members.
+     It carries a field list and not a case list, which is the whole surface
+     difference from [defdata] — there is no tag, so there is nothing to name
+     a case with.
+
+     The tagged sum was spelled [defunion] until this form wanted the name, and
+     a file written before the rename is the hazard this arm exists for. It is
+     not an alias and it is not a near-miss: the old text would *parse* under
+     the new meaning. [(defunion U [A B])] is two bare symbols, which is
+     exactly the shape of one member [A] of type [B], and it would have gone on
+     compiling as an untagged union of one member — the silent misparse the
+     [defn] case above was rewritten to make impossible, with no diagnostic
+     anywhere and nothing in the source that looks wrong.
+
+     So the name slots are read before anything is built. A member name is
+     lowercase and a case name is capitalised, and a case *with* fields is a
+     list where a member name would be; either one means the text in hand is a
+     tagged sum wearing the old spelling, and it is refused by name. A file
+     that really did mean an untagged union whose first member is capitalised
+     is refused too, and it is the right trade: that is not a thing anyone has
+     written, and being told to rename a member is nothing beside being given
+     the wrong type in silence. *)
   | List ({ v = Sym "defunion"; _ } :: args) ->
     (match args with
-     | [ n; { v = Vec vs; _ } ] -> mk (Ast.Defunion (sym n, List.map variant vs))
-     | _ -> fail f "defunion is (defunion Name [(Case [field Type ...]) ...])")
+     | [ n; { v = Vec ms; _ } ] ->
+       List.iteri
+         (fun i (m : Form.t) ->
+            let looks_tagged =
+              i mod 2 = 0
+              && (match m.v with
+                  | List _ -> true
+                  | Sym s -> s <> "" && s.[0] = Char.uppercase_ascii s.[0]
+                  | _ -> false)
+            in
+            if looks_tagged then
+              Loc.failk "parse/defunion-renamed" f.loc
+                "the tagged sum is defdata now — (defdata Name [(Case [field \
+                 Type ...]) ...]) — and defunion is C's untagged union, whose \
+                 members overlay one storage: (defunion Name [member Type \
+                 ...]). This reads as the tagged one, so it is refused rather \
+                 than quietly given the other meaning")
+         ms;
+       mk (Ast.Defunion (sym n, fields f ms))
+     | _ -> fail f "defunion is (defunion Name [member Type ...])")
 
   (* The slot after the parameters is unconditionally the return type. It used
      to be optional, and the parser decided return-type-versus-body by looking
@@ -1060,7 +1106,7 @@ and variant (f : Form.t) : Ast.variant =
   | List [ { v = Sym n; _ }; { v = Vec fs; _ } ] ->
     { Ast.vname = n; vfields = fields f fs; vloc = f.loc }
   | List [ { v = Sym n; _ } ] -> { Ast.vname = n; vfields = []; vloc = f.loc }
-  | _ -> fail f "a union case is Name or (Name [field Type ...])"
+  | _ -> fail f "a data type case is Name or (Name [field Type ...])"
 
 (* Macro expansion, which runs over [Form] and therefore before anything in
    this file. It cannot be called directly: expanding a macro means compiling
diff --git a/lib/prelude.ml b/lib/prelude.ml
index 473026a..3ed65e6 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -1466,9 +1466,9 @@ let source = {flan|
 ;; site attached to what a macro produces", and it is what the queued
 ;; structured-error work will read.
 ;;
-;; Case order is the tag order (docs/BUILT.md, unions), so this list is a layout
+;; Case order is the tag order (docs/BUILT.md, data types), so this list is a layout
 ;; contract with lib/expand.ml's marshaller and may not be reordered.
-(defunion Form
+(defdata Form
   [(Sym   [s string])
    (Kw    [s string])
    (Int   [i i64])
diff --git a/lib/reach.ml b/lib/reach.ml
index 331f4cf..d9f0ec8 100644
--- a/lib/reach.ml
+++ b/lib/reach.ml
@@ -18,7 +18,7 @@
       calls [@InitWindow] only moves the failure from the linker's argument
       list to its symbol table.
 
-    Only [fns] and [externs] are pruned. Globals, structs and unions stay:
+    Only [fns] and [externs] are pruned. Globals, structs and data types stay:
     a dropped function is a loud link error, a dropped global would be a
     silently different program, and an unreferenced global is bytes in BSS that
     cost nothing. A [defvar brush rl/Texture2D] in a headless build is exactly
diff --git a/lib/render.ml b/lib/render.ml
index 218c1e3..384231e 100644
--- a/lib/render.ml
+++ b/lib/render.ml
@@ -57,10 +57,14 @@ type pointers = {
 
 type ctx = {
   structs : Tast.structure list;
-  (* The declared unions. [Types.Named] covers a struct and a union alike, so
+  (* The declared data types. [Types.Named] covers a struct and a data type
+     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;
+  datas  : Tast.data list;
+  (* The untagged unions, which this prints by name and does not walk. See the
+     arm below for why. *)
+  unions  : Tast.structure list;
   enums   : (string * (string * int64) list) list;
   emit    : emitter;
   (* [None] in a build with no registry to ask, which is every release build
@@ -225,15 +229,15 @@ 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
+    (* A data type, 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 ->
+      when List.exists (fun (u : Tast.data) -> String.equal u.Tast.dname n)
+             c.datas ->
       let u =
-        List.find (fun (u : Tast.union) -> String.equal u.Tast.uname n) c.unions
+        List.find (fun (u : Tast.data) -> String.equal u.Tast.dname n) c.datas
       in
       let tag = { Tast.e = Tast.Field (e, 0); ty = Types.Int Types.I32; loc } in
       let one i (v : Tast.variant) otherwise =
@@ -269,7 +273,7 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
         in
         unit_ (Tast.If (is, body, otherwise))
       in
-      (* The fallback is a tag no case names, which only a scribbled-over union
+      (* The fallback is a tag no case names, which only a scribbled-over data type
          could hold. Showing the number is more use than showing a case it is
          not. *)
       let base =
@@ -278,6 +282,25 @@ let rec render c depth (e : Tast.expr) : Tast.expr list =
       in
       [ List.fold_left (fun acc x -> x acc) base
           (List.rev (List.mapi one u.Tast.cases)) ]
+    (* A union, named and not walked, and this is the one value in the language
+       the printer refuses to show the contents of.
+
+       Not squeamishness about indeterminate bytes — a printer that showed a
+       number nobody stored would be fine, and every member of a union is a
+       legal read by this language's own rule. It is that one of those members
+       may be a [string] or a [Ptr], and rendering it would dereference
+       whatever bytes happen to be in the union's storage. A tagged data type
+       is safe to print because its tag says which case is live; there is no
+       such fact here, so the printer would be following a pointer it invented.
+       Showing four members of which three are made up is also not obviously
+       better than showing none.
+
+       So: the type, and nothing else. What the value means is the caller's
+       knowledge, and [(.member u)] prints whichever member that is. *)
+    | Types.Named n
+      when List.exists (fun (u : Tast.structure) -> String.equal u.Tast.sname n)
+             c.unions ->
+      [ lit ("<" ^ n ^ " union>") ]
     | 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 f6b0ba3..0a3e4cb 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -748,6 +748,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;
+      datas = t.program.Tast.datas;
       unions = t.program.Tast.unions;
       enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
       emit = dev_emitter;
@@ -874,8 +875,8 @@ let render_locals ?(origin = "<locals>") t ~frame ~(fn : Tast.fn) ~bound
    is not an option. A pointer is still never followed — that is the
    renderer's rule and not this mode's. *)
 
-(* A step, as the editor sends it. [Sfield] on a union carries the case as
-   well, because a union's payload is at an offset that depends on which case
+(* A step, as the editor sends it. [Sfield] on a data type carries the case as
+   well, because a data type's payload is at an offset that depends on which case
    it is, and the renderer is what told the editor which case this value
    currently holds. Guessing the case from a field name that two cases share
    would read one case's layout over another's payload. *)
@@ -937,21 +938,21 @@ let step_into t (v : Tast.expr) (s : step) : (Tast.expr, string) result =
   | Sfield spec ->
     (match ty with
      | Types.Named n
-       when List.exists (fun (u : Tast.union) -> String.equal u.Tast.uname n)
-              t.program.Tast.unions ->
+       when List.exists (fun (u : Tast.data) -> String.equal u.Tast.dname n)
+              t.program.Tast.datas ->
        let u =
-         List.find (fun (u : Tast.union) -> String.equal u.Tast.uname n)
-           t.program.Tast.unions
+         List.find (fun (u : Tast.data) -> String.equal u.Tast.dname n)
+           t.program.Tast.datas
        in
-       (* The editor spells this `Union.case.field', which is the head the
-          renderer wrote — `(Union.case {.field …})' — with the field appended.
+       (* The editor spells this `Type.case.field', which is the head the
+          renderer wrote — `(Type.case {.field …})' — with the field appended.
           A bare `case.field' is taken too, since that is the same fact said
           shorter. *)
        (match String.rindex_opt spec '.' with
         | None ->
           no
             (Printf.sprintf
-               "%s is a union: a field of it has to name the case that holds \
+               "%s is a data type: a field of it has to name the case that holds \
                 it, because the payload's offset depends on which case the \
                 value is in"
                n)
@@ -1045,6 +1046,7 @@ let render_slot ?(origin = "<inspect>") t ~frame ~(fn : Tast.fn) ~slot ~path
       let extra = ref [] and nslots = ref 0 in
       let c =
         { Render.structs = t.program.Tast.structs;
+          datas = t.program.Tast.datas;
           unions = t.program.Tast.unions;
           enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
           emit = dev_emitter;
@@ -1137,6 +1139,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;
+      datas = t.program.Tast.datas;
       unions = t.program.Tast.unions;
       enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
       emit = dev_emitter;
@@ -1244,6 +1247,7 @@ let eval_expr ?(origin = "<eval>") ?(pause = false) t src : change =
   let extra = ref [] and nslots = ref (Array.length base) in
   let c =
     { Render.structs = t.program.Tast.structs;
+      datas = t.program.Tast.datas;
       unions = t.program.Tast.unions;
       enums = Hashtbl.fold (fun k v acc -> (k, v) :: acc) t.env.Check.enums [];
       emit = dev_emitter;
diff --git a/lib/shim.ml b/lib/shim.ml
index 00aed2c..c3958cf 100644
--- a/lib/shim.ml
+++ b/lib/shim.ml
@@ -46,7 +46,7 @@
     struct layout is C's, and [emit.ml] writes no datalayout, so clang applies
     the target's own rules to both halves and they land in the same place.
     Everything where the two could diverge — a fixed array, a slice, an
-    [Option], a map, a union — is refused at the field, by name.
+    [Option], a map, a data type — is refused at the field, by name.
 
     Trusted: that the [defstruct] describes the library's real struct, and that
     the [declare-c] signature is the function's real signature. No library
@@ -121,6 +121,7 @@ let out_tmp = "%out"
 type env = {
   structs : (string, Ast.field list) Hashtbl.t;
   enums   : (string, unit) Hashtbl.t;
+  datas  : (string, unit) Hashtbl.t;
   unions  : (string, unit) Hashtbl.t;
   aliases : (string, Ast.texpr) Hashtbl.t;
 }
@@ -128,13 +129,15 @@ type env = {
 let scan (decls : Ast.decl list) =
   let env =
     { structs = Hashtbl.create 32; enums = Hashtbl.create 32;
-      unions = Hashtbl.create 8; aliases = Hashtbl.create 16 }
+      datas = Hashtbl.create 8; unions = Hashtbl.create 8;
+      aliases = Hashtbl.create 16 }
   in
   List.iter
     (fun (d : Ast.decl) ->
        match d.Ast.d with
        | Ast.Defstruct (n, fs) -> Hashtbl.replace env.structs n fs
        | Ast.Defenum (n, _) -> Hashtbl.replace env.enums n ()
+       | Ast.Defdata (n, _) -> Hashtbl.replace env.datas n ()
        | Ast.Defunion (n, _) -> Hashtbl.replace env.unions n ()
        | Ast.Defalias (n, t) -> Hashtbl.replace env.aliases n t
        | _ -> ())
@@ -190,11 +193,23 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
          (* A C enum is an int, and Flan's [Enum] is an i32 — the same thing on
             every target this compiles for. *)
          "int32_t"
-       else if Hashtbl.mem env.unions n then
+       else if Hashtbl.mem env.datas n then
          fail loc
-           "%s is %s, a union, and a Flan union has no C layout — the shim \
+           "%s is %s, a data type, and a Flan data type has no C layout — the shim \
             cannot be generated for it"
            what n
+       (* A union is the one refusal here that is not about the type. It has a
+          C layout — it *is* a C layout, which is the whole reason it exists —
+          and what is missing is the generator: [typedefs] writes structs, and
+          a union would need its own spelling and its own closure over the
+          member types. Refused by name rather than written untested, and the
+          way through is the way every other aggregate crosses. *)
+       else if Hashtbl.mem env.unions n then
+         fail loc
+           "%s is %s, a union, and the shim generator writes structs only — a \
+            union has a C layout but nothing here emits the declaration for \
+            it yet. Pass (Ptr %s) and let the C side read it"
+           what n n
        else if String.equal n "string" then
          fail loc
            "%s is a string, and a string only crosses as a parameter — a C \
diff --git a/lib/tast.ml b/lib/tast.ml
index 5900d77..5335f16 100644
--- a/lib/tast.ml
+++ b/lib/tast.ml
@@ -133,15 +133,16 @@ 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
+  (* A data type value: the data type'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
+     value's *type* is the data type 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
+  (* One field of one case of a data type 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
@@ -243,7 +244,7 @@ type structure = { sname : string; fields : field list }
 
 type variant = { vname : string; vfields : field list }
 
-type union = { uname : string; cases : variant list }
+type data = { dname : string; cases : variant list }
 
 type fn = {
   name    : string;
@@ -300,7 +301,12 @@ type extern = {
 
 type program = {
   structs : structure list;
-  unions  : union list;
+  datas  : data list;
+  (* The untagged unions, carried as [structure] values: a union's members are
+     a field list whose every offset is zero, so the record a struct uses says
+     all of it. Which list a name came out of is what a backend reads to know
+     whether to accumulate the offsets or not. *)
+  unions : structure list;
   globals : global list;              (* in declaration order *)
   externs : extern list;
   fns     : fn list;
@@ -316,10 +322,10 @@ type program = {
 }
 
 (* 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
+   are declaration order from zero, so an all-bytes-zero data type 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 =
+   [None], and the reason case order is part of a data type's contract. *)
+let case_index (u : data) name =
   let rec go i = function
     | [] -> None
     | (c : variant) :: rest ->
diff --git a/lib/types.ml b/lib/types.ml
index 90f700f..be8e5aa 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -22,7 +22,7 @@ type t =
   | String
   | Unit                              (* the zero-sized type, not C's void *)
   | Never                             (* return, exit, error: no value at all *)
-  | Named  of string                  (* a struct or union declared in the file *)
+  | Named  of string                  (* a struct or data type, declared here *)
   (* A C enum: an i32 at run time, but its own type, so a keyword at a call
      site has something to resolve against and a plain integer does not fit. *)
   | Enum   of string
diff --git a/lib/x86.ml b/lib/x86.ml
index 9eecf2a..a06c10c 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -429,16 +429,19 @@ let xorps b ~dst = rex b ~w:false ~r:dst ~x:0 ~m:dst; u8 b 0x0f; u8 b 0x57; modr
 
 (* ── Types ───────────────────────────────────────────────────────────── *)
 
-(* [Emit.m] carries the struct and union tables [Emit.lay] reads. Built here
+(* [Emit.m] carries the struct and data type tables [Emit.lay] reads. Built here
    rather than imported so that this module adds no line to [emit.ml]: the
    record has no signature hiding it and every field it needs is inert. *)
 let layout_ctx ~checks ~dev (p : Tast.program) : Emit.m =
-  let structs = Hashtbl.create 16 and unions = Hashtbl.create 16 in
+  let structs = Hashtbl.create 16 and datas = Hashtbl.create 16 in
+  let unions = Hashtbl.create 16 in
   List.iter (fun (s : Tast.structure) -> Hashtbl.replace structs s.Tast.sname s)
     p.Tast.structs;
-  List.iter (fun (u : Tast.union) -> Hashtbl.replace unions u.Tast.uname u)
+  List.iter (fun (u : Tast.data) -> Hashtbl.replace datas u.Tast.dname u)
+    p.Tast.datas;
+  List.iter (fun (u : Tast.structure) -> Hashtbl.replace unions u.Tast.sname u)
     p.Tast.unions;
-  { Emit.out = Buffer.create 1; strs = Buffer.create 1; structs; unions;
+  { Emit.out = Buffer.create 1; strs = Buffer.create 1; structs; datas; unions;
     globals = Hashtbl.create 1; externs = Hashtbl.create 1; checks;
     dev; known = (fun _ -> true); dbg = None; sanitize = false;
     nstr = 0; nfi = 0 }
@@ -1068,7 +1071,7 @@ let imm_into f ~reg (n : int64) = movabs f.b ~dst:reg n
 
 (* ── Struct layout, through [Emit] ───────────────────────────────────── *)
 
-let union_payload_off f (u : Tast.union) =
+let data_payload_off f (u : Tast.data) =
   let size, align = Emit.payload_lay f.md u in
   if size = 0 then 0
   else
@@ -1089,22 +1092,30 @@ let field_offsets f (sn : string) =
     in
     offs
   | None ->
-    (* A union is a struct too, at this level: [emit.ml] lays it out as a tag
+    (* A data type is a struct too, at this level: [emit.ml] lays it out as a tag
        and a payload blob, and the structural printer reads the tag as field 0
        without unwrapping the value. *)
-    (match Hashtbl.find_opt f.md.Emit.unions sn with
-     | Some (u : Tast.union) -> [ 0; union_payload_off f u ]
-     | None -> unsupported "no struct %s" sn)
+    (match Hashtbl.find_opt f.md.Emit.datas sn with
+     | Some (u : Tast.data) -> [ 0; data_payload_off f u ]
+     | None ->
+       (* And a union is a struct at this level too, with the one difference
+          that makes it a union: every member starts where the union starts,
+          so the offsets are zeros and the member's own type is what the load
+          or the store reads the bytes as. One list per member and not a
+          single zero, because the caller indexes it by member. *)
+       match Hashtbl.find_opt f.md.Emit.unions sn with
+       | Some (u : Tast.structure) -> List.map (fun _ -> 0) u.Tast.fields
+       | None -> unsupported "no struct %s" sn)
 
-(* A union is { i32 tag, [k x iA] payload }, the same two fields [Emit.lay]
+(* A data type is { i32 tag, [k x iA] payload }, the same two fields [Emit.lay]
    measures it as — so the payload's offset is whatever [lay_fields] puts the
-   second one at, and not a rule spelled a second time here. A union whose
+   second one at, and not a rule spelled a second time here. A data type whose
    cases are all payload-less is a bare tag and has no second field. *)
 
-let union_of f n =
-  match Hashtbl.find_opt f.md.Emit.unions n with
+let data_of f n =
+  match Hashtbl.find_opt f.md.Emit.datas n with
   | Some u -> u
-  | None -> unsupported "no union %s" n
+  | None -> unsupported "no data type %s" n
 
 (* The offsets of one case's fields inside the payload blob. The single place
    in this backend that knows how a payload is read, so [match]'s binds,
@@ -1549,12 +1560,12 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit =
     jmp_lbl f.b f.retlbl;
     lbl f.b lsome;
     move f ~dst ~src:(shift src ov) payload
-  | Tast.MakeCase (uname, case, fields) ->
-    let u = union_of f uname in
+  | Tast.MakeCase (dname, case, fields) ->
+    let u = data_of f dname in
     let i, c =
       match Tast.case_index u case with
       | Some (i, c) -> i, c
-      | None -> unsupported "no case %s of %s" case uname
+      | None -> unsupported "no case %s of %s" case dname
     in
     (* Zeroed first: an omitted field is ZII and the payload blob is wider
        than this case, so the bytes past its last field have to be something
@@ -1562,7 +1573,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit =
     zero_loc f dst (sizeof f.md t);
     imm_into f ~reg:rax (Int64.of_int i);
     store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:4;
-    let poff = union_payload_off f u in
+    let poff = data_payload_off f u in
     let offs = case_offsets f c in
     List.iteri
       (fun k (x : Tast.expr) ->
@@ -1956,25 +1967,25 @@ and lvalue f (e : Tast.expr) : loc =
   | Tast.CaseField (target, case, i) -> case_field f target case i
   | _ -> eval f e
 
-(* The address of one field of one case of a union value. Only ever reached
+(* The address of one field of one case of a data type value. Only ever reached
    under an arm that proved the tag — [match] is the only thing that proves
    it — or from the structural printer, which compares the same tag first. *)
 and case_field f (target : Tast.expr) case i =
-  let uname =
+  let dname =
     match target.Tast.ty with
     | Types.Named n -> n
     | ty -> unsupported "case field of %s" (Types.to_string ty)
   in
-  let u = union_of f uname in
+  let u = data_of f dname in
   let c =
     match Tast.case_index u case with
     | Some (_, c) -> c
-    | None -> unsupported "no case %s of %s" case uname
+    | None -> unsupported "no case %s of %s" case dname
   in
-  shift (lvalue f target) (union_payload_off f u + List.nth (case_offsets f c) i)
+  shift (lvalue f target) (data_payload_off f u + List.nth (case_offsets f c) i)
 
 (* [match]. The two subjects are the same shape and are read differently: an
-   [Option] is an i8 tag and a payload at a known offset, a declared union is
+   [Option] is an i8 tag and a payload at a known offset, a declared data type is
    an i32 tag and a blob the arm's case reinterprets. Everything past the tag
    and the binds is shared, which is the arrangement [emit.ml] settled on for
    the same reason. *)
@@ -1982,9 +1993,9 @@ and emit_match f (scrut : Tast.expr) (arms : Tast.arm list) dst t =
   let base = lvalue f scrut in
   let tag_size, tag_of, bind_at =
     match scrut.Tast.ty with
-    | Types.Named n when Hashtbl.mem f.md.Emit.unions n ->
-      let u = union_of f n in
-      let poff = union_payload_off f u in
+    | Types.Named n when Hashtbl.mem f.md.Emit.datas n ->
+      let u = data_of f n in
+      let poff = data_payload_off f u in
       ( 4,
         (fun case ->
            match Tast.case_index u case with
@@ -1998,7 +2009,7 @@ and emit_match f (scrut : Tast.expr) (arms : Tast.arm list) dst t =
           | None -> unsupported "no case %s of %s" case n )
     | Types.Option el ->
       (* [lay_fields] puts the i8 tag at 0, so [base] is the tag's address the
-         way it is for a union. *)
+         way it is for a data type. *)
       let _, ov = option_lay f el in
       ( 1,
         (fun case -> if String.equal case "Some" then 1 else 0),
diff --git a/spec-memory.md b/spec-memory.md
index 5eb17f6..90f45ed 100644
--- a/spec-memory.md
+++ b/spec-memory.md
@@ -447,6 +447,48 @@ type**, so that every site computing `align-of T` gets the raised number with no
 further plumbing. The surface syntax for that declaration is deliberately not
 fixed here; nothing is built that needs it yet.
 
+### Untagged unions and what a read of one means
+
+`defunion` is C's union: the members overlay one storage, the size is the
+largest of them, the alignment the strictest, and **nothing records which
+member was written**. It is not `defdata`, which is the tagged sum — a case, its
+fields, and a tag that steers every `match`.
+
+**Reading a member that was not the one last written is defined**, and it is
+the one place in this language where bytes win over safety on purpose. It reads
+the storage through that member's type: the layout is the target's, the bytes
+are the bytes, and the read is a reinterpretation of them. C leaves this to the
+implementation; Flan does not, because both uses the type exists for *are* that
+read. Binding a C header means holding the union the library holds and reading
+whichever member the library's own tag says is live — a tag the compiler cannot
+see, since the rule relating them is prose in a manual. Overlaying an `f32` on a
+`u32` to look at its bits is the same read. A rule that refused it would be
+refusing the type.
+
+What is **not** promised is anything about bytes nobody wrote. A member wider
+than the one last stored reads its own size, and the tail is indeterminate
+exactly as a struct's padding is. ZII narrows that to almost nothing in
+practice: a union is all-bytes-zero unless `uninit` says otherwise.
+
+Three things a union may not do, and each for a reason that does not expire:
+
+- **No move-only member.** Nothing knows which member is live, so nothing can
+  tear one down. Unlike the struct and `defdata` refusals, this is not waiting
+  on recursive teardown — there is no fact for teardown to read, and freeing
+  the wrong member is a free of a pointer that was an `f64` a moment ago.
+- **No `bool` member, at any depth.** An `i1` loaded out of a byte that is
+  neither 0 nor 1 is a value the optimiser is entitled to assume cannot exist,
+  and a union is the only type that can produce one. Hold a `u8` and compare it.
+- **Not a map key.** A member narrower than the union leaves the rest of the
+  bytes indeterminate, so two values agreeing about everything written would
+  still hash apart.
+
+`uninit` on a union **is** allowed, unlike on a `defdata`. The refusal there is
+not about garbage: it is that a tag no case names falls past every comparison in
+a `match` into a block the optimiser may treat as unreachable. An untagged union
+steers nothing, so `uninit` makes its bytes arbitrary and changes nothing else —
+which is what it means on an `i64`.
+
 ### Allocation failure
 
 **No allocating operation returns an error, and none can fail silently.** When
diff --git a/syntax-sketch.flan b/syntax-sketch.flan
index 78e30fe..32462cb 100644
--- a/syntax-sketch.flan
+++ b/syntax-sketch.flan
@@ -49,7 +49,7 @@
    hp   i32
    spr  (Handle Texture)])
 
-(defunion Shape
+(defdata Shape
   [(Circle [r f32])
    (Rect   [w f32  h f32])])
 
diff --git a/test/headers/sample.h b/test/headers/sample.h
index e578c86..f1f77c7 100644
--- a/test/headers/sample.h
+++ b/test/headers/sample.h
@@ -81,3 +81,20 @@ Undescribed make_undescribed(void);          /* no defstruct for it */
  * arriving at the checker as a duplicate declaration nobody wrote. */
 int Spin2D(int n);
 int spin2d(int n);
+
+/* A union, and the two records that go with it.
+ *
+ * `Slot' is the shape the FFI actually meets: a C library keeps the tag
+ * beside the union and states the rule relating them in prose, so the Flan
+ * side holds both and reads the member the tag names. It is here because the
+ * importer used to record *no* record containing a union member at all --
+ * which meant the defstruct beside it went unchecked as well -- and now a
+ * named one is checked member by member like anything else.
+ *
+ * `Anon' is the case that is still skipped, and the reason is not a
+ * limitation of the check: an anonymous union member has no name for a Flan
+ * field to carry and no way to reach its members, so there is nothing on the
+ * Flan side to compare against. */
+typedef union Overlay { int i; float f; } Overlay;
+typedef struct Slot { int kind; Overlay v; } Slot;
+typedef struct Anon { int kind; union { int i; float f; }; } Anon;
diff --git a/test/programs/datas.flan b/test/programs/datas.flan
new file mode 100644
index 0000000..bb23d13
--- /dev/null
+++ b/test/programs/datas.flan
@@ -0,0 +1,110 @@
+;;;; 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.
+
+(defdata 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.
+(defdata 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 "")
+
+  ;; A union names an element type the same way a struct does. It reads as
+  ;; trivia and it was not: the type-name test (vec-new) and (map-new) use to
+  ;; read a leading bare symbol listed structs, enums, aliases and primitives
+  ;; and not unions, so (vec-new Shape) was refused for not saying what it
+  ;; held -- by a program that had said.
+  (let [vs (vec-new Shape)
+        ms (map-new string Shape)]
+    (push vs (Shape.Rect {.w 2 .h 3}))
+    (push vs Shape.Empty)
+    (put ms "only" (Shape.Tag {.name "in a map" .n 1}))
+    (print (i64 (area (at vs 0)))) (println "")
+    (println (describe (at vs 1)))
+    (println (match (get ms "only") (Some s) (describe s) None "missing")))
+  0)
diff --git a/test/programs/dev-inspect.flan b/test/programs/dev-inspect.flan
index 753a8aa..748971a 100644
--- a/test/programs/dev-inspect.flan
+++ b/test/programs/dev-inspect.flan
@@ -17,7 +17,7 @@
 (defstruct Point [x f32  y f32])
 (defstruct Boom [why i32])
 
-(defunion Shape
+(defdata Shape
   [Empty
    (Dot  [x f64  y f64])
    (Rect [w i32  h i32])])
diff --git a/test/programs/unions.flan b/test/programs/unions.flan
index 070687c..1c49454 100644
--- a/test/programs/unions.flan
+++ b/test/programs/unions.flan
@@ -1,110 +1,89 @@
-;;;; 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.
+;; The untagged union: one storage, several ways of reading it.
+;;
+;; Every line here is a fact about *bytes*, which is the whole reason the
+;; program exists rather than a checker row. A union's layout is the only
+;; thing about it that can be wrong silently: reading the member that was not
+;; written is defined behaviour in Flan, so nothing at run time would notice a
+;; member placed at the wrong offset or a type sized to the wrong member --
+;; the numbers would simply be different ones. So the numbers are written
+;; down, and both backends have to produce them.
+;;
+;; 0x3F800000 is 1.0f and 0x4000000000000000 is 2.0. They are here as decimal
+;; literals because that is what a reader who doubts the output has to be able
+;; to check by hand against IEEE 754, and a hex literal would only move the
+;; question.
 
-(defunion Shape
-  [Empty
-   (Dot   [x f64  y f64])
-   (Rect  [w i32  h i32])
-   (Tag   [name string  n u8])])
+(defstruct P [x f32  y f32])
 
-;; 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))
+(defunion Bits [i i32  f f32  bs [4 u8]])
+(defunion Wide [n i64  d f64  p P  bs [8 u8]])
 
-(defn widen [n i32] Shape (Shape.Rect {.w n .h (* n 2)}))
+;; A union inside a struct, which is the FFI shape: the C library keeps the
+;; tag beside the union and the rule relating them is prose in its manual, so
+;; `kind' here is an ordinary field this program reads itself.
+(defstruct Slot [kind i32  v Bits])
 
-;; 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])
+;; Zeroed and uninit, side by side. A data type refuses uninit because its tag
+;; steers a match; this one has no tag to steer anything, so both are legal
+;; and the zeroed one is all-bytes-zero.
+(defvar zeroed Bits)
+(defvar scratch Bits uninit)
 
-(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))
+(defn as-float [b Bits] f32 (.f b))
 
-;; 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 of-float [x f32] Bits (Bits {.f x}))
 
 (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})))
+  ;; Punning, both directions, through the same storage.
+  (let [b (Bits {.i 1065353216})]
+    (println (.f b))
+    (println (.i b))
+    ;; The bytes little-endian: 0x3F800000 is 00 00 80 3F.
+    (println (at (.bs b) 0))
+    (println (at (.bs b) 3))
+    ;; A member written through a place, which is the other half of the same
+    ;; claim -- the read above could have been folded from the literal, and a
+    ;; store into the union could not.
+    (set (.f b) 2.0)
+    (println (.i b)))
 
-  ;; ZII: omitted fields are zeroed, exactly as in a struct literal.
-  (println (describe (Shape.Rect {.w 0})))
+  ;; The union crosses a call boundary in both directions by value.
+  (println (as-float (of-float 0.5)))
 
-  ;; 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 "")
+  ;; A wider union: the size is the widest member and not the first one. An
+  ;; array of two is where that shows up -- writing element 1 would land
+  ;; inside element 0 if the type were sized to its i64 member alone and the
+  ;; f64 or the [8 u8] were wider, and every element's value would change
+  ;; under the other's write.
+  (let [w (Wide {.d 2.0})]
+    (println (.n w))
+    (println (.x (.p w))))
 
-  ;; 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)))))
+  (let [ws (array 2 Wide)]
+    (set (.n (at ws 0)) 11)
+    (set (.n (at ws 1)) 22)
+    (println (.n (at ws 0)))
+    (println (.n (at ws 1))))
 
-  ;; 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)))
+  ;; ZII: a union with no member given is all-bytes-zero, and so is a global
+  ;; declared with no value.
+  (let [empty (Bits {})]
+    (println (.i empty)))
+  (println (.i zeroed))
+  ;; And a global is written and read like any other place.
+  (set (.i scratch) 7)
+  (println (.i scratch))
 
-  ;; 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 ""))
+  ;; A union inside a struct, with the tag the program keeps itself.
+  (let [s (Slot {.kind 1  .v (Bits {.f 1.5})})]
+    (println (.kind s))
+    (println (.f (.v s)))
+    (set (.kind s) 2)
+    (set (.i (.v s)) 9)
+    (println (.kind s))
+    (println (.i (.v s))))
 
-  ;; 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 "")
-
-  ;; A union names an element type the same way a struct does. It reads as
-  ;; trivia and it was not: the type-name test (vec-new) and (map-new) use to
-  ;; read a leading bare symbol listed structs, enums, aliases and primitives
-  ;; and not unions, so (vec-new Shape) was refused for not saying what it
-  ;; held -- by a program that had said.
-  (let [vs (vec-new Shape)
-        ms (map-new string Shape)]
-    (push vs (Shape.Rect {.w 2 .h 3}))
-    (push vs Shape.Empty)
-    (put ms "only" (Shape.Tag {.name "in a map" .n 1}))
-    (print (i64 (area (at vs 0)))) (println "")
-    (println (describe (at vs 1)))
-    (println (match (get ms "only") (Some s) (describe s) None "missing")))
+  ;; Printed by name and not walked: the printer cannot know which member is
+  ;; live, and a member may be a pointer.
+  (println zeroed)
   0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 10d12f4..cd05671 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2141,10 +2141,10 @@ ERR@7 unexpected token: not the kind the caller was reading
     shim_refuses "declare-c: an Option"
       (v2 ^ "(declare-c maybe [] (Option Vector2) \"Maybe\")")
       "which is a Flan shape and not a C one";
-    shim_refuses "declare-c: a union"
-      ("(defunion Shape [(Circle [r f32]) (Square [s f32])])\n\
+    shim_refuses "declare-c: a data type"
+      ("(defdata Shape [(Circle [r f32]) (Square [s f32])])\n\
         (declare-c area [s Shape] f32 \"Area\")")
-      "a union, and a Flan union has no C layout";
+      "a data type, and a Flan data type has no C layout";
     shim_refuses "declare-c: a fixed array"
       "(declare-c takes [xs [4 f32]] \"Takes\")"
       "which C passes as a pointer and Flan as a value";
@@ -2299,19 +2299,19 @@ 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
+    (* ── Data type values ───────────────────────────────────────────
+       defdata 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,
+       string, a data type in a struct, a data type through a call in both directions,
        ZII, reassignment and printing.
 
-       -O0 as well, for the reason every aggregate here gets it: a union value
+       -O0 as well, for the reason every aggregate here gets it: a data type 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
+       indirection cell there and a data type crosses one as a parameter and as a
        return value. *)
-    let unions_out =
+    let datas_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\
@@ -2463,6 +2463,26 @@ ERR@7 unexpected token: not the kind the caller was reading
     refuses "a macro that does not settle" "programs/macro-spin.flan"
       "did not settle after";
 
+    outputs "data types" "programs/datas.flan" datas_out;
+    outputs ~opt:"-O0" "data types, -O0" "programs/datas.flan" datas_out;
+    outputs ~dev:true "data types, dev" "programs/datas.flan" datas_out;
+    (* ── The untagged union ─────────────────────────────────────────
+       Reading a member that was not written is defined here rather than
+       refused, which means nothing at run time would notice a member at the
+       wrong offset or a type sized to the wrong member: the numbers would
+       just be different numbers. So the numbers are written down. The layout
+       itself is checked against the backend that computes it, through the
+       DWARF/LLVM oracle further down; this is what the bytes *do*.
+
+       -O0 for the reason the data type above gets it, and more so: a union
+       value is a zeroed alloca and a store, and mem2reg is exactly what would
+       turn a store to the wrong half of one into a register nobody reads.
+       The x86-64 backend runs the same file under the @x86 alias, which
+       compares both backends on every program in this directory. *)
+    let unions_out =
+      "1\n1065353216\n0\n63\n1073741824\n0.5\n4611686018427387904\n0\n\
+       11\n22\n0\n0\n7\n1\n1.5\n2\n9\n<Bits union>\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;
@@ -2471,62 +2491,62 @@ ERR@7 unexpected token: not the kind the caller was reading
        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 data type case written as a struct"
+      "(defdata U [(A [x i32])])\n(defn main [] i32 (let [v (A {.x 1})] 0))"
+      "A is a case of the data type U";
+    refuses_src "a data type type used as a constructor"
+      "(defdata U [(A [x i32])])\n(defn main [] i32 (let [v (U {.x 1})] 0))"
+      "a data type 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))"
+      "(defdata 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
+       nothing, and the case a data type 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\
+      "(defdata 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))"
+    refuses_src "a match arm naming a case the data type does not have"
+      "(defdata 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\
+      "(defdata 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))"
+      "(defdata 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
+    (* The declaration's own refusals. A data type 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
+    (* A data type 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
+       which already traversed a data type's cases. Both shapes: direct, and two
+       data types 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)"
+    refuses_src "a data type that contains itself by value"
+      "(defdata 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)"
+    refuses_src "two data types that contain each other by value"
+      "(defdata A [(X [b B])])\n(defdata 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)"
+    refuses_src "a data type with no cases"
+      "(defdata 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)"
+    refuses_src "a data type case that owns a Vec"
+      "(defdata 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\
+       pair is emitted. A data type reaches the same place. *)
+    refuses_src "a data type is not a map key"
+      "(defdata 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
@@ -2535,14 +2555,14 @@ ERR@7 unexpected token: not the kind the caller was reading
        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 name = "a global initialised with a data type case" in
      let src =
-       "(defunion U [A (B [x i32])])\n(defvar g U (U.B {.x 1}))\n\
+       "(defdata 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)))
+         (Check.program (Parse.program (Reader.read_all ~file:"<defdata>" src)))
      with
      | _ ->
        incr failures;
@@ -2554,26 +2574,26 @@ ERR@7 unexpected token: not the kind the caller was reading
          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
+       bytes. On a data type 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)"
+    refuses_src "uninit on a data type global"
+      "(defdata 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
+    (* A data type'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))"
+    refuses_src "reading a field of a data type directly"
+      "(defdata 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
+    (let name = "a zeroed data type 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\
+               (Reader.read_all ~file:"<defdata>"
+                  "(defdata U [A (B [x i32])])\n(defvar g U)\n\
                    (defn main [] i32 (match g A 0 (B x) x))")))
      with
      | _ -> ()
@@ -2695,7 +2715,7 @@ ERR@7 unexpected token: not the kind the caller was reading
     in
     (* Every (member name, byte offset) of a named struct, in declaration
        order, as the emitted DWARF states it. *)
-    let dwarf_members ir sname =
+    let dwarf_members ?(tag = "DW_TAG_structure_type") ir sname =
       let ls = lines_of ir in
       let node id =
         List.find_opt
@@ -2704,7 +2724,7 @@ ERR@7 unexpected token: not the kind the caller was reading
       let composite =
         List.find_opt
           (fun l ->
-             index_of l "!DICompositeType(tag: DW_TAG_structure_type" >= 0
+             index_of l (Printf.sprintf "!DICompositeType(tag: %s" tag) >= 0
              && attr l "name" = Some (Printf.sprintf "\"%s\"" sname))
           ls
       in
@@ -2875,7 +2895,7 @@ 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
+    (* A data type, 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.
@@ -2887,18 +2907,109 @@ ERR@7 unexpected token: not the kind the caller was reading
        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\
+    layout_case "DWARF offsets agree with LLVM: a data type"
+      ("(defdata 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
+    (* And the same data type 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\
+    layout_case "DWARF offsets agree with LLVM: a narrow data type"
+      ("(defdata 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" ];
 
+    (* An untagged union, which the case above cannot serve: its DWARF tag is
+       DW_TAG_union_type and its members are not a struct's, so there is no
+       [getelementptr] per member to compare against. What there is to check
+       is exactly C's three rules, and each is asked of the backend rather
+       than of a table beside the code:
+
+       - every member is at offset zero, which is the DWARF's claim;
+       - the size is the widest member, rounded up to the alignment, which is
+         [ptrtoint (getelementptr (%U, ptr null, i32 1))];
+       - the alignment is the strictest member's, which is where the type
+         lands after a single byte.
+
+       The type here is chosen so that no two of those numbers agree by
+       accident: [f64] is the widest and strictest at 8, [i32] is narrower,
+       and [[5 u8]] is five bytes at alignment one — so the size is 8 only if
+       it is the max *rounded up*, and a union sized to its first member, or
+       to the last, or aligned to the array, comes out at a different number
+       and this says so. *)
+    let union_layout_case name src uname members =
+      let ir = debug_ir src in
+      match dwarf_members ~tag:"DW_TAG_union_type" ir uname with
+      | None ->
+        incr failures;
+        Printf.printf "FAIL  %s\n        no DWARF union type for %s\n" name uname
+      | Some (got, size) ->
+        if List.map fst got <> members then begin
+          incr failures;
+          Printf.printf "FAIL  %s\n        DWARF members: %s\n     wanted: %s\n"
+            name (String.concat " " (List.map fst got))
+            (String.concat " " members)
+        end;
+        List.iter
+          (fun (mname, off) ->
+             if off <> 0 then begin
+               incr failures;
+               Printf.printf
+                 "FAIL  %s\n        %s.%s is at byte %d, and a union member is \
+                  at zero\n" name uname mname off
+             end)
+          got;
+        (match llvm_members ir uname 0 with
+         | None ->
+           Printf.printf "acceptance: %s — llc unavailable, size unchecked\n" name
+         | Some oracle ->
+           (match List.assoc_opt "sz" oracle with
+            | Some want when want <> size ->
+              incr failures;
+              Printf.printf
+                "FAIL  %s\n        %s is %d bytes in the DWARF, %d in LLVM\n"
+                name uname size want
+            | _ -> ()));
+        (match llvm_align ir uname with
+         | None -> ()
+         | Some al ->
+           (* The DWARF states the alignment too, and it has to be the one
+              LLVM lays the type out at -- a debugger reading 8 where the
+              storage is aligned to 4 would step through an array of them
+              wrongly. *)
+           let dwarf_align =
+             List.find_map
+               (fun l ->
+                  if index_of l "!DICompositeType(tag: DW_TAG_union_type" >= 0
+                     && attr l "name" = Some (Printf.sprintf "\"%s\"" uname)
+                  then
+                    Option.map (fun a -> int_of_string (String.trim a) / 8)
+                      (attr l "align")
+                  else None)
+               (lines_of ir)
+           in
+           (match dwarf_align with
+            | Some d when d <> al ->
+              incr failures;
+              Printf.printf
+                "FAIL  %s\n        %s is aligned to %d in the DWARF, %d in LLVM\n"
+                name uname d al
+            | _ -> ()))
+    in
+    union_layout_case "DWARF and LLVM agree on a union's layout"
+      ("(defunion U [n i32  d f64  bs [5 u8]])\n\
+        (defn main [] i32 (let [u (U {.n 3})] (.n u)))\n")
+      "U" [ "n"; "d"; "bs" ];
+    (* And one whose widest member is not its strictest, so the round-up is
+       doing something: [11 u8] is eleven bytes at alignment one and [i32]
+       wants four, which is 12 and not 11. A union sized to the widest member
+       alone is 11, and an array of them would misalign every element after
+       the first. *)
+    union_layout_case "DWARF and LLVM agree on a union that rounds up"
+      ("(defunion R [bs [11 u8]  n i32])\n\
+        (defn main [] i32 (let [r (R {.n 3})] (.n r)))\n")
+      "R" [ "bs"; "n" ];
+
     (* -- Form: the one layout two programs have to agree on --------
        Every layout above is checked because a debugger reads it. This one is
        checked because the *compiler* reads it. A macro is compiled into a .so
@@ -3254,7 +3365,7 @@ ERR@7 unexpected token: not the kind the caller was reading
     (match
        Build.executable
          ~opts:{ Build.default with debug = true; target = Some "wasm32-wasi" }
-         { Tast.structs = []; unions = []; globals = []; externs = []; fns = [];
+         { Tast.structs = []; datas = []; unions = []; globals = []; externs = []; fns = [];
            cshim = [] }
          ~out:(Filename.concat scratch "flan-dbg-wasm")
      with
diff --git a/test/test_dev.ml b/test/test_dev.ml
index a968c39..32c67df 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -366,14 +366,14 @@ let () =
       end;
       let r =
         request c
-          "(:op \"eval\" :code \"(defunion Shape [(Circle [r f32])])\" :file \"/tmp/buf.flan\")"
+          "(:op \"eval\" :code \"(defdata Shape [(Circle [r f32])])\" :file \"/tmp/buf.flan\")"
       in
-      if status r <> "ok" then fail "a new union: %s" (refusal r)
+      if status r <> "ok" then fail "a new data type: %s" (refusal r)
       else begin
         let r = request c "(:op \"layout\" :type \"Shape\")" in
-        if status r <> "error" then fail "a union answered a struct layout"
-        else if not (contains (refusal r) "is a union") then
-          fail "a union is refused as: %s" (refusal r)
+        if status r <> "error" then fail "a data type answered a struct layout"
+        else if not (contains (refusal r) "is a data type") then
+          fail "a data type is refused as: %s" (refusal r)
       end;
 
       (* The identity rule, and the case NEXT.md named: a second [Blob] typed
@@ -1275,7 +1275,7 @@ let () =
 
        It also carries the two shapes an expression cannot reach at all: an
        option's payload, which no accessor form in the language names, and a
-       union case's field, whose offset depends on which case the value is
+       data type case's field, whose offset depends on which case the value is
        in. *)
     let isock = tmp "inspect.sock" and iout = tmp "inspect.out" in
     (try Sys.remove isock with Sys_error _ -> ());
@@ -1410,7 +1410,7 @@ let () =
             [ ("mark", "(\"nope\")", "no field called nope");
               ("mark", "(some)", "not an option");
               ("xs", "(9)", "past the end");
-              (* A union field without its case: the payload's offset depends
+              (* A data type field without its case: the payload's offset depends
                  on the case, so guessing one that two cases share would read
                  one case's layout over another's payload. *)
               ("s", "(\"w\")", "name the case") ]
diff --git a/test/test_flan.ml b/test/test_flan.ml
index bbf2c74..b6b475e 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -470,6 +470,24 @@ let () =
   parse_rejects "defmacro in expression position" "(defn f [] () (defmacro m [] 1))"
     ~needle:"top-level declaration";
 
+  (* The tagged sum is [defdata] now. The old spelling is refused by name
+     rather than aliased, because the name is reserved for a type with
+     different semantics — a file that kept [defunion] must be made to say
+     which of the two it means instead of being quietly given one of them. *)
+  parse_rejects "the old defunion spelling"
+    "(defunion Shape [(Circle [r f32]) (Square [s f32])])"
+    ~needle:"the tagged sum is defdata now";
+  (* The shape that would otherwise parse: two bare case names read as one
+     member of a type. Same refusal, and this is the one that matters — it
+     would have compiled. *)
+  parse_rejects "the old defunion spelling with payload-less cases"
+    "(defunion U [A B])"
+    ~needle:"the tagged sum is defdata now";
+  (match read "(defunion U [A B])" |> Parse.program with
+   | _ -> check "the old spelling has a kind" false
+   | exception Loc.Error { Loc.kind; _ } ->
+     check "the old spelling has a kind" (kind = "parse/defunion-renamed"));
+
   (* The return type is not optional. A void function writes (), and the
      refusal says so rather than leaving someone to find it in a grammar. *)
   parse_rejects "defn with no return type" "(defn f [] (g))"
@@ -1497,11 +1515,11 @@ let () =
     "(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, and the
-     milestone has since arrived: match now works over a declared union as
+     milestone has since arrived: match now works over a declared data type 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 or a union, not on i32";
+    ~needle:"match works on an Option or a data type, 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"
@@ -1515,6 +1533,134 @@ let () =
     "(defn f [] i32 (let [xs [1 2]] (destructure~nth xs 0 2 1)))"
     ~needle:"means nothing outside a quasiquote";
 
+  (* ── The untagged union ────────────────────────────────────────── *)
+
+  (* Every one of these is a rule the type would be unsound or useless
+     without, and each says so in its own words rather than falling through to
+     something generic. The layout itself is pinned where a layout can only be
+     pinned, against the backend that computes it — see the DWARF/LLVM oracle
+     in test_acceptance.ml — and what it *does* is pinned by a program that
+     writes one member and reads another, which is the whole point of the
+     type. What is here is the catalogue of what it refuses. *)
+  (match (parse_decl "(defunion U [i i32  f f32])").Ast.d with
+   | Ast.Defunion ("U", [ a; b ]) ->
+     check "defunion parses as a member list"
+       (a.Ast.fname = "i" && b.Ast.fname = "f")
+   | _ -> check "defunion parses as a member list" false);
+
+  (* Nothing to read out of, and no size. It parses; it is refused where the
+     message can name the shape. *)
+  rejects_check "a union with no members"
+    "(defunion U [])\n(defn f [u U] i32 0)"
+    ~needle:"declares no members";
+  rejects_check "a union that declares a member twice"
+    "(defunion U [x i32  x f32])\n(defn f [u U] i32 0)"
+    ~needle:"declares the same member twice";
+  (* The size is the largest member and the largest member is the whole type,
+     so this is the same infinite type a self-containing struct is. *)
+  rejects_check "a union that contains itself by value"
+    "(defunion U [a i32  b U])\n(defn f [u U] i32 0)"
+    ~needle:"contains itself by value";
+  (* Not waiting on drop, unlike the struct and data type refusals: nothing
+     records which member is live, so there is no fact recursive teardown
+     could read. *)
+  rejects_check "a union member that is move-only"
+    "(defunion U [n i64  v (Vec i32)])\n(defn f [u U] i32 0)"
+    ~needle:"nothing records which was written";
+  (* And the one the optimiser would otherwise be handed: a byte that is
+     neither 0 nor 1 read as an i1. Refused at any depth, which is why the
+     second row goes through a struct. *)
+  rejects_check "a bool member"
+    "(defunion U [b bool  n u8])\n(defn f [u U] i32 0)"
+    ~needle:"a union may not hold one at any depth";
+  rejects_check "a bool inside a struct member"
+    "(defstruct S [flag bool  n i32])\n\
+     (defunion U [s S  n i64])\n(defn f [u U] i32 0)"
+    ~needle:"a union may not hold one at any depth";
+  (* The same hazard as uninit on a data type, arriving the other way round: a
+     member written over the tag leaves a tag no case names, and a match on it
+     falls into a block the optimiser may treat as unreachable. Refused at any
+     depth for the reason bool is. *)
+  rejects_check "a data type member"
+    "(defdata D [A (B [x i32])])\n\
+     (defunion U [d D  n i64])\n(defn f [u U] i32 0)"
+    ~needle:"a data type's tag steers every match";
+  rejects_check "a data type inside a struct member"
+    "(defdata D [A B])\n(defstruct S [d D  n i32])\n\
+     (defunion U [s S  n i64])\n(defn f [u U] i32 0)"
+    ~needle:"a data type's tag steers every match";
+  (* An Option is not on that list, and the difference is the lowering: its
+     match is a test of the tag byte and a branch, so a scribbled tag reads as
+     a Some with a payload nobody stored — which is what this language says a
+     union read is. *)
+  (match checked "(defunion U [o (Option i32)  n i64])\n\
+                  (defn f [u U] i32 (match (.o u) (Some x) x None 0))" with
+   | _ -> check "an Option member is allowed" true
+   | exception Loc.Error { Loc.dmsg = msg; _ } ->
+     incr failures;
+     Printf.printf "FAIL  an Option member is allowed: %s\n" msg);
+  (* One member named twice is a different mistake from two members named, and
+     it gets the refusal the struct path already had. *)
+  rejects_check "a union literal naming one member twice"
+    "(defunion U [i i32])\n\
+     (defn f [] i32 (let [u (U {.i 1  .i 2})] (.i u)))"
+    ~needle:"member i is given twice";
+
+  (* Two members is one storage written twice, and which one survived would be
+     whatever the compiler happened to do last. *)
+  rejects_check "a union literal giving two members"
+    "(defunion U [i i32  f f32])\n\
+     (defn f [] i32 (let [u (U {.i 1  .f 2.0})] (.i u)))"
+    ~needle:"only one of them can be written";
+  rejects_check "a union literal giving a member it does not have"
+    "(defunion U [i i32])\n(defn f [] i32 (let [u (U {.z 1})] (.i u)))"
+    ~needle:"U has no member z";
+  (* There is no tag, so there is nothing for the arms to be alternatives
+     over. Said by name because the two kinds of union are one keyword apart
+     and somebody will write it. *)
+  rejects_check "match on a union"
+    "(defunion U [i i32  f f32])\n\
+     (defn f [u U] i32 (match u _ 0))"
+    ~needle:"there is nothing in one to match on";
+  (* A member narrower than the union leaves the rest indeterminate, so two
+     values that agree about everything anybody wrote would hash apart. *)
+  rejects_check "a union as a map key"
+    "(defunion U [i i32  f f32])\n\
+     (defn f [m (Map U i32) k U] () (put m k 1))"
+    ~needle:"a union is not a map key";
+  (* A global's initialiser is a constant and writing a member is a store. The
+     zeroed and uninit forms need none of that and are accepted below. *)
+  rejects_check "a global initialised with a union member"
+    "(defunion U [i i32])\n(defvar g U (U {.i 1}))\n(defn f [] i32 0)"
+    ~needle:"cannot be written into a global";
+  (* A defconst reaches the same emitter by a different path, so it gets the
+     same refusal rather than coming back as "this one is computed". *)
+  rejects_check "a constant initialised with a union member"
+    "(defunion U [i i32])\n(defconst c U (U {.i 1}))\n(defn f [] i32 0)"
+    ~needle:"cannot be written into a constant";
+  (* The all-bytes-zero value is a constant and goes through, which is what
+     makes (U {}) and a declaration with no value the same thing. *)
+  (match checked "(defunion U [i i32])\n(defvar g U (U {}))\n\
+                  (defn f [] i32 (.i g))" with
+   | _ -> check "a global zeroed through a literal is allowed" true
+   | exception Loc.Error { Loc.dmsg = msg; _ } ->
+     incr failures;
+     Printf.printf "FAIL  a global zeroed through a literal is allowed: %s\n" msg);
+  (* uninit is refused on a data type because its tag steers a match into a
+     block LLVM may treat as unreachable. An untagged union steers nothing, so
+     the argument does not carry over and the answer is different. *)
+  (match checked "(defunion U [i i32  f f32])\n(defvar g U uninit)\n\
+                  (defn f [] i32 (.i g))" with
+   | _ -> check "uninit on a union is allowed" true
+   | exception Loc.Error { Loc.dmsg = msg; _ } ->
+     incr failures;
+     Printf.printf "FAIL  uninit on a union is allowed: %s\n" msg);
+  (* The shim writes structs and has no spelling for a union yet — a refusal
+     about the generator, not about the type, and it says so. *)
+  rejects_check "a union crossing to C by value"
+    "(defunion U [i i32])\n(declare-c take [u U] () \"take\")"
+    ~needle:"the shim generator writes structs only";
+
   (* ── Reading a C header (cimport.ml, cjson.ml) ─────────────────── *)
 
   (* Against test/headers/sample.h, which is one function per decision the
@@ -1530,7 +1676,9 @@ let () =
     let fixture =
       "(defstruct Pair [x f32  y f32])\n\
        (defstruct Shade [r u8  g u8  b u8  a u8])\n\
-       (defenum Mood [calm 0  cross 1])\n"
+       (defenum Mood [calm 0  cross 1])\n\
+       (defunion Overlay [i i32  f f32])\n\
+       (defstruct Slot [kind i32  v Overlay])\n"
     in
     let ds = program fixture in
     let taken = Hashtbl.create 16 in
@@ -1545,6 +1693,11 @@ let () =
         (fun (d : Ast.decl) ->
            match d.Ast.d with Ast.Defstruct (n, _) -> Some n | _ -> None)
         ds
+    and known_unions =
+      List.filter_map
+        (fun (d : Ast.decl) ->
+           match d.Ast.d with Ast.Defunion (n, _) -> Some n | _ -> None)
+        ds
     and known_enums =
       List.filter_map
         (fun (d : Ast.decl) ->
@@ -1553,7 +1706,8 @@ let () =
     in
     let i, d, e =
       Cimport.header ~loc:Loc.unknown ~header:"headers/sample.h" ~flags:[]
-        ~known_structs ~known_enums ~taken ~bound_syms:[] ~config:Cimport.no_config
+        ~known_structs ~known_unions ~known_enums ~taken ~bound_syms:[]
+        ~config:Cimport.no_config
     in
     (i, d, e, ds)
   in
@@ -1632,6 +1786,11 @@ let () =
         (fun (d : Ast.decl) ->
            match d.Ast.d with Ast.Defstruct (n, _) -> Some n | _ -> None)
         fixture_ds
+    and known_unions =
+      List.filter_map
+        (fun (d : Ast.decl) ->
+           match d.Ast.d with Ast.Defunion (n, _) -> Some n | _ -> None)
+        fixture_ds
     and known_enums =
       List.filter_map
         (fun (d : Ast.decl) ->
@@ -1640,7 +1799,7 @@ let () =
     in
     let i, _, _ =
       Cimport.header ~loc:Loc.unknown ~header:"headers/sample.h" ~flags:[]
-        ~known_structs ~known_enums ~taken ~bound_syms:[] ~config
+        ~known_structs ~known_unions ~known_enums ~taken ~bound_syms:[] ~config
     in
     (List.map Cimport.decl_source i.Cimport.decls, i.Cimport.hidden)
   in
@@ -1801,6 +1960,91 @@ let () =
      | [ ("Feel", why) ] -> contains why "i64"
      | _ -> false);
 
+  (* The same claim for a [defunion], and what it unlocked. A record holding a
+     union member used to be skipped entirely — not recorded, so the
+     [defstruct] beside it was unchecked too — because there was no Flan type
+     to compare the member against. There is one now, and [Slot] in the
+     fixture is checked member by member like any other struct. *)
+  let unions_of ds =
+    List.filter_map
+      (fun (d : Ast.decl) ->
+         match d.Ast.d with Ast.Defunion (n, ms) -> Some (n, ms) | _ -> None)
+      ds
+  in
+  check "a defunion that matches the header is not reported"
+    (Cimport.check_unions ~env ~unions:(unions_of fixture_ds) dump = []);
+  check "and the struct holding it is checked rather than skipped"
+    (Cimport.check_structs ~env ~structs:(structs_of fixture_ds) dump = []);
+  check "a struct whose union member is given the wrong type is reported"
+    (match
+       Cimport.check_structs ~env
+         ~structs:(structs_of (program "(defstruct Slot [kind i32  v Pair])\n"))
+         dump
+     with
+     | [ ("Slot", why) ] -> contains why "Overlay"
+     | _ -> false);
+  (* Order is the whole hazard for a struct and means nothing for a union:
+     every member is at offset zero, so a permuted defunion is the same type
+     and reporting it would be a finding that is not one. *)
+  check "a permuted defunion is not reported"
+    (Cimport.check_unions ~env
+       ~unions:(unions_of (program "(defunion Overlay [f f32  i i32])\n")) dump
+     = []);
+  (* Missing is the one that changes the size, and a union embedded by value
+     puts every field after it in the wrong place. *)
+  check "a defunion missing a member is reported"
+    (match
+       Cimport.check_unions ~env
+         ~unions:(unions_of (program "(defunion Overlay [i i32])\n")) dump
+     with
+     | [ ("Overlay", why) ] -> contains why "f" && contains why "widest"
+     | _ -> false);
+  check "a defunion with a member the header lacks is reported"
+    (match
+       Cimport.check_unions ~env
+         ~unions:(unions_of
+                    (program "(defunion Overlay [i i32  f f32  d f64])\n")) dump
+     with
+     | [ ("Overlay", why) ] -> contains why "d"
+     | _ -> false);
+  check "a defunion whose member is the wrong width is reported"
+    (match
+       Cimport.check_unions ~env
+         ~unions:(unions_of (program "(defunion Overlay [i i32  f f64])\n")) dump
+     with
+     | [ ("Overlay", why) ] -> contains why "f64" && contains why "f32"
+     | _ -> false);
+  (* Two different layouts under one name, which is the same class of finding
+     a permuted struct is and has a one-keyword fix. *)
+  check "a defstruct against a union in the header is reported"
+    (match
+       Cimport.check_structs ~env
+         ~structs:(structs_of (program "(defstruct Overlay [i i32  f f32])\n"))
+         dump
+     with
+     | [ ("Overlay", why) ] -> contains why "union in the header"
+     | _ -> false);
+  check "a defunion against a struct in the header is reported"
+    (match
+       Cimport.check_unions ~env
+         ~unions:(unions_of (program "(defunion Pair [x f32  y f32])\n")) dump
+     with
+     | [ ("Pair", why) ] -> contains why "struct in the header"
+     | _ -> false);
+  check "a union the header does not describe is left alone"
+    (Cimport.check_unions ~env
+       ~unions:(unions_of (program "(defunion Nowhere [q i32])\n")) dump
+     = []);
+  (* And the gap that remains, said out loud so it is a decision rather than
+     an oversight: an anonymous union member has no name and no Flan
+     spelling, so the record holding one is still not recorded and the
+     defstruct beside it is still unchecked rather than checked wrongly. *)
+  check "a record with an anonymous union member is still skipped"
+    (Cimport.check_structs ~env
+       ~structs:(structs_of (program "(defstruct Anon [kind i32  junk i32])\n"))
+       dump
+     = []);
+
   (* ── The constants (Cimport.check_constants) ───────────────────── *)
 
   (* The half of generate-c's claim that used to be missing. A wrong flag bit
diff --git a/test/test_valgrind.ml b/test/test_valgrind.ml
index 523f42f..cf70ed7 100644
--- a/test/test_valgrind.ml
+++ b/test/test_valgrind.ml
@@ -240,7 +240,7 @@ let corpus =
     "programs/stale-region.flan", [];
     "programs/string-of-bytes.flan", [];
     "programs/text.flan", [];
-    "programs/unions.flan", [];
+    "programs/datas.flan", [];
     "programs/unit-main.flan", [];
     "programs/utf8.flan", [];
     "programs/values.flan", [];
@@ -271,7 +271,7 @@ let unchecked_subset =
     "programs/slices.flan", [];
     "programs/slurp.flan", [];
     "programs/text.flan", [];
-    "programs/unions.flan", [];
+    "programs/datas.flan", [];
     "programs/utf8.flan", [];
     "programs/vec.flan", [];
     "../calc-me.flan", [ "1 + 2 * (3 - 0.5) / 2" ] ]
diff --git a/web/index.html b/web/index.html
index 3ac93c3..a4ab6ec 100644
--- a/web/index.html
+++ b/web/index.html
@@ -522,7 +522,8 @@ notation reads as exactly one data item.</p>
 <tr><td><code>Allocator</code></td><td>an opaque builtin: a proc, its data and a capability set</td><td>a pointer to that</td></tr>
 <tr><td><code>$t</code></td><td>a type variable — see <a href="#generics">generics</a></td><td>whatever it is instantiated at</td></tr>
 <tr><td>a struct</td><td>value type</td><td>fields in declaration order</td></tr>
-<tr><td>a union</td><td><code>defunion</code>, matched by case</td><td>tag + the widest payload</td></tr>
+<tr><td>a tagged data type</td><td><code>defdata</code>, matched by case</td><td>tag + the widest payload</td></tr>
+<tr><td>an untagged union</td><td><code>defunion</code>, C's: read any member, no tag</td><td>the widest member, at the strictest alignment</td></tr>
 <tr><td>an enum</td><td>its own type in the checker</td><td><code>i32</code></td></tr>
 <tr><td><code>()</code></td><td>one value, zero size</td><td>empty</td></tr>
 <tr><td><code>Never</code></td><td>fits anywhere; nothing has it</td><td>empty</td></tr>
@@ -762,7 +763,7 @@ as <code>first-even</code> does above.</p>
 
 <p><code>(Option T)</code> is how absence is spelled: a lookup miss, an empty
 collection, the end of a stream. <code>match</code> works on an <code>Option</code> and
-on a <code>defunion</code>, and on nothing else. <code>some</code> unwraps
+on a <code>defdata</code>, and on nothing else. <code>some</code> unwraps
 <code>Some</code> and early-returns <code>None</code> from the enclosing function.</p>
 
 <pre><code>(defconst nums [4 i32] [4 8 15 16])
@@ -2108,7 +2109,7 @@ disagree with the first.</p>
 <script>
 // A small hand-written highlighter for the Flan blocks. One pass, no library.
 (function () {
-  var FORMS = new Set(("defn defstruct defenum defunion defconst defvar defalias " +
+  var FORMS = new Set(("defn defstruct defenum defdata defunion defconst defvar defalias " +
     "declare declare-c import package let if when unless cond do and or not while " +
     "until dotimes match set return some try defer signal error handler-bind " +
     "restart-case invoke-restart fn quote defmacro gensym").split(" "));