diff --git a/Data/Ruin.hs b/Data/Ruin.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin.hs
@@ -0,0 +1,429 @@
+{- | Description: -- This is usually the only import.
+
+#TH#
+
+[<#TH TH splice>]
+
+    The 'makeRecords' splice reifies any data type declared with
+    record syntax into instances of this library's classes.
+
+    @
+      data XY y = MkXY {x :: Int, y :: y} deriving (Generic,Show)
+      data YX x = MkYX {y :: Bool, x :: x} deriving (Generic,Show)
+
+      $('makeRecords' [''XY,''YX])
+      -- or $('makeRecords' ['MkXY,'MkYX]) would also work
+    @
+
+    Either @$('makeRecords' [''XY])@ or @$('makeRecords' ['MkXY])@
+    splices in instances that reify the record syntax declaration of
+    @MkXY@ into instances of the @ruin@ package's classes. Naming the
+    constructor lets you reify a data family instance. The generated
+    declarations defer to the "GHC.Generics" defaults as much as possible.
+
+    The field names are used exactly, so use @-XDuplicateRecordFields@
+    so that <#conversion the automatic conversions> work.
+
+#singletons#
+
+[<#singletons Singleton records>]
+
+    The @ruin@ library also supports anonymous record types.
+
+    The ':@' newtype is the singleton record type.
+
+    @
+      *> :t 'dub'
+      'Label' s -> a -> s ':@' a
+
+      *> :t 'dub' \#x   -- This uses -XOverloadedLabels.
+      a -> "x" ':@' a
+
+      *> :t 'undub' \#z
+      "z" ':@' a -> a
+    @
+
+    And a tuple of record types is also a record type if the component
+    record types do not have any fields with the same name. Currently it
+    supports up to 8 tuple components. Note that you can nest them if you
+    need more!
+
+#projection#
+
+[<#projection Projection>]
+
+    The 'Has' class provides the 'extricate' projection, which allows
+    <#careful-strictness careful control of strictness>.
+
+    @
+      *> :t 'Data.Ruin.Eval.runEval' . 'extricate' \#x
+      'Has' "x" t => t -> 'FieldType' "x" t
+    @
+
+    'extricate' can navigate nested records with intuitive syntax.
+
+    @
+      *> :t 'Data.Ruin.Eval.runEval' . 'extricate' (\#x . \#y)
+      ('Has' "y" ('FieldType' "x" t), 'Has' "x" t) =>
+       t -> 'FieldType' "y" ('FieldType' "x" t)
+    @
+
+#conversion#
+
+[<#conversion Conversion>]
+
+    The 'Build' and 'IsSubtypeOf' constraints provide the 'rup' upcast
+    with respect to record types' /width subtyping relationship/.
+    'IsSubtypeOf' and 'rup' essentially delegate to 'Has' and 'extricate'
+    for each necessary field.
+
+    @
+      *> let (y,z) = 'rup' ('dub' \#z (), MkXY {x=undefined,y="ash"})
+      *> ('undub' \#y y,'undub' \#z z)
+      ("ash",())
+    @
+
+    The 'rsym' isomorphism is 'rup' with a specialized type
+    requiring that the two types be subtypes of one another.
+
+    @
+      *> let (y,z,x) = 'rsym' ('dub' \#z (), MkXY {x=1,y="ash"})
+      *> ('undub' \#x x,'undub' \#y y,'undub' \#z z)
+      (1,"ash",())
+    @
+
+#ascription#
+
+[<#ascription Ascription>]
+
+    The 'hoid' function is a family of identity functions, indexed by
+    types of any order. It let's you ascribe types without having to fully
+    apply them, which is often useful for polymorphic record types.
+
+    @
+      *> :t 'hoid' \@XY
+      XY t -> XY t
+
+      *> :t 'hoid' \@(->)
+      (t -> t1) -> t -> t1
+    @
+
+    Record types have a notion of /shape/; see 'Shape' for
+    details. The 'UnifyShape' constraint and the 'asShapeOf' ascription can
+    both be used to drive type inference. There are some combinators whose
+    types are very unweildy until the involved record types' shapes are
+    fixed.
+
+    The \"complement\" of a record type's shape is roughly the types
+    of the record type's fields. The `UnifyFieldTypes` constraint and the
+    `asFieldTypesOf` combinator support ascribing just that.
+
+    @
+      *> :t \\x y rc -> ('dub' \#x x,'dub' \#y y) \``asFieldTypesOf`\` rc
+      'FieldType' "x" rc
+      -> 'FieldType' "y" rc
+      -> proxy rc
+      -> ("x" ':@' 'FieldType' "x" rc, "y" ':@' 'FieldType' "y" rc)
+    @
+
+    Note that the second argument must have at least the fields of the
+    first argument, but may have a different shape, which in particular
+    means it may have \"extra\" fields.
+
+    You'll generally use the 'hoidProxy' and 'proxyOf' combinators to
+    create the second argument of 'asFieldTypesOf'.
+
+    @
+      *> :t 'hoidProxy' \@XY
+      Data.Proxy.Proxy (XY t)
+      *> :t 'proxyOf'
+      a -> Data.Proxy.Proxy a
+    @
+
+#to-fro#
+
+[<#to-fro Directed conversion>]
+
+    The 'rfrom' and 'rto' combinators are 'rsym' but additionally
+    require an explicit type argument (like 'hoid') so that they read
+    well.
+
+    @
+      *> :t (\\(x,y) -> ('undub' \#x x,'undub' \#y y)) . 'rfrom' \@XY
+      XY t -> (Int,t)
+
+      *> 'rto' \@XY ('dub' \#x 1,'dub' \#y False)
+      XY {x = 1, y = False}
+    @
+
+#qq#
+
+[<#qq Quasiquoter>]
+
+    The 'rna' quasiquoter enables named arguments for functions.
+
+    @
+      *> :t \\['rna'|x y|] -> x * x + 3 x * y - 2 * y * y
+      Num a => ("x" ':@' a,"y" ':@' a) -> a
+    @
+
+    It can also create anonymous records.
+
+    @
+      *> :t \\x y -> ['rna'|x y|]
+      a -> a1 -> ("x" ':@' a, "y" ':@' a1)
+    @
+
+    There are some usefuls syntactic sugars; see 'rna' for details.
+
+    @
+      *> :t ['rna'| id\@x show\@y |]
+      Show a1 => ("x" ':@' (a -> a), "y" ':@' (a1 -> String))
+
+      *> :t \\_x' _y' -> ['rna'| XY (_...') x y |]
+      Int -> y -> XY y
+    @
+
+#suppression#
+
+[<#suppression Suppressing fields>]
+
+    The lopsided combinator '<@' allows for left-biased field overlap.
+
+    @
+      *> let xy = ('dub' \#x 1, 'dub' \#y False)
+      *> let yz = ('dub' \#y 4, 'dub' \#z undefined)
+      *> let f ['rna'|x y|] = x + y
+      *> f $ 'rsym' $ yz '<@' xy
+      5
+    @
+
+    The 'hide' combinator hides some fields, without having to replace
+    to them.
+
+    @
+      *> :t 'extricate' \#x $ 'hide' \#x $ 'dub' \#x True
+      \<interactive>:1:1: error:
+          * ruin: The field \`x\' is hidden in the type
+                "x" ':@' Bool
+          * ...
+      *> 'Data.Ruin.runEval' $ 'extricate' \#x $ 'hide' \#y $ 'dub' \#x True
+      True
+    @
+
+    You can hide multiple fields at once:
+
+    @
+      *> :t 'hide' (\#x . \#y)
+      rc -> 'Hide' '["x", "y"] rc
+      True
+    @
+
+    Note that that hides the @x@ field and the @y@ field --- it
+    doesn't hide a nested field @x.y@.
+
+#partitioning#
+
+[<#partitioning Partitioning records>]
+
+    Sometimes suppressing a field isn't enough, and you need to
+    actually remove it. In that case, use the partitioning combinators.
+
+    The 'rdrop' combinator is a stronger version of 'hide'; given a
+    list of labels and a record, it creates an anonymous record with the
+    fields of the given record other than the given labels.
+
+    @
+      *> 'rdrop' (\#x . \#y) ('dub' \#x \'x\','dub' \#y \'y\','dub' \#z \'z\')
+      'MkTup1' ('dub' \#z \'z\')
+    @
+
+    Instead of listing those labels explicitly, you can use
+    'fieldLabelsOf' to take them from another known record type.
+
+    Note that the 'rsym' combinator can split a record type into two
+    other record types that fully partition the full origial.
+
+    @
+      data AB a b = {a::a,b::b} deriving (Generic,Show)
+      data CD c d = {c::c,d::d} deriving (Generic,Show)
+      $(makeRecords [''AB,''CD])
+
+      *> 'hoid' \@AB *** 'hoid' \@CD $ 'rsym' ['rna'|mempty\@a mempty\@b mempty\@c mempty\@d|]
+      (Monoid a3, Monoid a2, Monoid a1, Monoid a) =>
+      t -> (AB a2 a3, CD a a1)
+    @
+
+    The 'rtake' combinator is similar, except it completely infers the
+    type of the second component; specifically, the second component is an
+    anonymous record type whose fields are those that are \"leftover\"
+    from creating the first component. Otherwise, it's just like 'rsym'.
+
+#custom-errors#
+
+[<#custom-errors Custom errors>]
+
+    Most of the error messages are easy to read.
+
+    @
+      *> (\\['rna'|x z|] -> x + z) $ 'rsym' ('dub' \#x 1, 'dub' \#y 2)
+      \<interactive>:3:1: error:
+        * ruin: Could not find a field \`z\' in the type
+              "x" ':@' t
+            or in the type
+              "y" ':@' a
+        * ...
+    @
+
+#fieldwise#
+
+[<#fieldwise Fieldwise combinators>]
+
+    Record types support an interface very similar to Applicative
+    functors, based on fieldwise operations.
+
+    The 'rpure', 'rmonopure', 'rmap', and 'rsplat' combinators are
+    designed to mimic the familiar 'pure', '<$>', and '<*>'
+    combinators.
+
+    @
+      *> let isZero x = 0 == x
+      *> ['rna'|show succ pred isZero|] \``rsplat`\` 'rmonopure' (4 :: Int)
+      ('dub' \#show "4",'dub' \#succ 5,'dub' \#pred 3,'dub' \#isZero False)
+    @
+
+    Others: 'rmempty', 'rmappend', and 'rlabel'. See
+    <#fieldwise-more this section> for more information.
+
+#applicative-variants#
+
+[<#applicative-variants Applicative variants>]
+
+    Many combinators have variants that work in an Applicative
+    functor. In particular, the 'rnaA' quasiquoter only works for
+    expressions, and it builds records in an Applicative functor, with the
+    effects of each field ordered as in the quasiquoter text.
+
+    @
+      *> let x = [1,2]
+      *> let y = ["y1","y2"]
+      *> mapM_ print ['rnaA'|XY x y|]
+      MkXY {x = 1,y = "y1"}
+      MkXY {x = 1,y = "y2"}
+      MkXY {x = 2,y = "y1"}
+      MkXY {x = 2,y = "y2"}
+      *> mapM_ print ['rnaA'|XY y x|]
+      MkXY {x = 1,y = "y1"}
+      MkXY {x = 2,y = "y1"}
+      MkXY {x = 1,y = "y2"}
+      MkXY {x = 2,y = "y2"}
+    @
+
+    Others: 'rfromA', 'rsymA', 'rtoA', 'rupA', 'rmapA', and 'rsplatA'.
+-}
+module Data.Ruin (
+  -- * Singleton records
+  (:@),
+  dub,
+  undub,
+
+  -- * Accessing parts of records
+  Has(..),
+  extricate,
+  rna,
+  rnaA,
+
+  -- * Hiding fields
+  Hide,
+  hide,
+
+  -- * Record types' /width subtyping/
+
+  -- ** Lowest-level combinators
+  Build(..),
+
+  -- ** Pure combinators
+  (<@),
+  rdrop,
+  rfrom,
+  rsym,
+  rtake,
+  rto,
+  rup,
+
+  -- ** Applicative combinators
+  rfromA,
+  rsymA,
+  rtoA,
+  rupA,
+
+  -- * Fieldwise combinators
+  --
+  -- | #fieldwise-more#
+  --
+  -- The types of these combinators are not useful in the
+  -- abstract. However, once the 'Shape' of any argument record type
+  -- or result record type is fixed, the types reduce to something
+  -- plain.
+  --
+  -- @
+  --   *> :t 'rsplat' ['rna'|show\@x id\@y|]
+  --   Show t => ("x" ':@' t, "y" ':@' t1) -> ("x" ':@' String, "y" ':@' t1)
+  -- @
+  --
+  --
+  -- A basic, self-contained example:
+  --
+  -- @
+  --   data PrintAndTime = MkPrintAndTime
+  --
+  --   instance (Show a,f ~ (a -> IO (a,Integer))) => 'FPure' PrintAndTime s f where
+  --     'fpure' _ x = do
+  --       print x
+  --       (,) x \<$> System.CPUTime.getCPUTime
+  --
+  --   *> 'rmapA' MkPrintAndTime ('dub' \#x \"OK", 'dub' \#y ())
+  --   \"OK"
+  --   ()
+  --   ('dub' \#x (\"OK",43062500000000),'dub' \#y ((),43062500000000))
+  -- @
+  FPure(..),
+  rlabel,
+  rmempty,
+  rmap,
+  rmapA,
+  rmappend,
+  rmonopure,
+  rpolypure,
+  rpure,
+  rsappend,
+  rsplat,
+  rsplatA,
+
+  -- * Ascription
+  UnifyFieldTypes,
+  UnifyShape,
+  asFieldTypesOf,
+  asShapeOf,
+  hoid,
+  hoidProxy,
+
+  -- * Conveniences
+  Label,
+  Labels,
+  NoWarnUnusedTopBind(..),
+  fieldLabelsOf,
+  makeRecords,
+  mkLabel,
+  mkLabels,
+  proxyOf,
+  ) where
+
+import Data.Ruin.All
+import Data.Ruin.Deep (Labels,extricate)
+import Data.Ruin.Fieldwise
+import Data.Ruin.Hide
+import Data.Ruin.Hoid (hoid,hoidProxy)
+import Data.Ruin.Internal
+import Data.Ruin.QQ (rna,rnaA)
+import Data.Ruin.TH (makeRecords)
diff --git a/Data/Ruin/All.hs b/Data/Ruin/All.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/All.hs
@@ -0,0 +1,1005 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language ConstraintKinds #-}
+{-# Language DataKinds #-}
+{-# Language DefaultSignatures #-}
+{-# Language DeriveDataTypeable #-}
+{-# Language DeriveFunctor #-}
+{-# Language DeriveGeneric #-}
+{-# Language DeriveLift #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language FunctionalDependencies #-}
+{-# Language GeneralizedNewtypeDeriving #-}
+{-# Language InstanceSigs #-}
+{-# Language KindSignatures #-}
+{-# Language LambdaCase #-}
+{-# Language MagicHash #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language PolyKinds #-}
+{-# Language Rank2Types #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeInType #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableSuperClasses #-}
+{-# Language UndecidableInstances #-}
+{-# Language ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}   -- for TypeError, UnifyShape, et al
+
+{-# OPTIONS_HADDOCK hide,not-home #-}
+
+-- | This internal module has everything in it in order to avoid
+-- orphans and mutually recursive imports.
+
+module Data.Ruin.All (module Data.Ruin.All) where
+
+import           Control.DeepSeq (NFData(..))
+import           Data.Binary (Binary)
+import           Data.Data (Data)
+import           Data.Char (isSpace)
+import           Data.Functor.Compose
+import           Data.Functor.Identity
+import           Data.Kind
+import           Data.Serialize (Serialize)
+import           GHC.Exts (Constraint)
+import           GHC.Prim (Proxy#,proxy#)
+import           GHC.Generics
+import           GHC.TypeLits hiding (type (*))
+import qualified Language.Haskell.TH as TH
+import           Language.Haskell.TH.Syntax (Lift(lift))
+
+import           Data.Ruin.Eval
+import           Data.Ruin.Internal
+import           Data.Ruin.Hoid
+
+-- | A custom tuple type. The library user should avoid mentioning
+-- this type directly. The only constructor exported by "Data.Ruin" is
+-- '<@'.
+--
+-- __Note__ that the instance @'Has' s ('Pair' l r)@ uses @'Has' s l@ if
+-- @s@ is in @'Fields' l@, even if @s@ is also in @'Fields' r@.
+--
+-- __Note__ the comment on the @'Build' ('Pair' l r)@ instance: unlike
+-- tuples, 'Pair's are not record types.
+data Pair (l :: *) (r :: *) = MkPair l r
+  deriving (Lift)
+
+instance (NFData l,NFData r) => NFData (Pair l r) where
+  {-# INLINE rnf #-}
+  rnf (MkPair l r) = rnf (l,r)
+
+unPair :: Pair l r -> (l,r)
+{-# INLINE unPair #-}
+unPair (MkPair l r) = (l,r)
+
+-----
+
+data Loc = Here | L Loc | R Loc
+
+type family Find (rc :: *) (s :: Symbol) :: Maybe Loc where
+  Find (Pair l r) s = SearchBoth (Find l s) (Find r s)
+  Find rc s = FindViaFields (Fields rc) s
+
+type family SearchBoth (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where
+  SearchBoth ('Just loc) _ = 'Just ('L loc)
+  SearchBoth _ ('Just loc) = 'Just ('R loc)
+  SearchBoth _ _ = 'Nothing
+
+type family FindViaFields (fields :: [(Symbol,*)]) (s :: Symbol) :: Maybe Loc where
+  FindViaFields '[] s = 'Nothing
+  FindViaFields ( '(s,ty) ': ss) s = 'Just 'Here
+  FindViaFields ( '(s1,ty) ': ss) s2 = FindViaFields ss s2
+
+-----
+
+instance MightHave (Pair l r) (Find (Pair l r) s) (Pair l r) s (FieldType s (Pair l r)) => Has s (Pair l r) where
+  type FieldType s (Pair l r) = PairFieldType (Find (Pair l r) s) (Pair l r) s
+  {-# INLINE extricate1 #-}
+  extricate1 = \_ -> fmap (undub (mkLabel @s)) . mightExtricate1 @(Pair l r) @(Find (Pair l r) s)
+
+type family PairFieldType (ml :: Maybe Loc) (rc :: *) (s :: Symbol) :: * where
+  PairFieldType ('Just 'Here) rc s = FieldType s rc
+  PairFieldType ('Just ('L loc)) (Pair l r) s = PairFieldType ('Just loc) l s
+  PairFieldType ('Just ('R loc)) (Pair l r) s = PairFieldType ('Just loc) r s
+
+-----
+
+class MightHave
+  (top :: *)
+  (mloc :: Maybe Loc)
+  (rc :: *)
+  (s :: Symbol) (a :: *)
+  where
+    mightExtricate1 :: rc -> Eval (s :@ a)
+
+type family Render (t :: *) :: ErrorMessage where
+  Render (Pair l r) = Render l ':$$: 'Text "  or in the type" ':$$: Render r
+  Render t = 'Text "    " ':<>: 'ShowType t
+
+type NoSuchField (s :: Symbol) (top :: *) =
+             'Text "ruin: Could not find a field `"
+       ':<>: 'Text s
+       ':<>: 'Text "' in the type"
+  ':$$: Render top
+
+instance TypeError (NoSuchField s top) => MightHave top 'Nothing rc s a where
+  mightExtricate1 = undefined
+
+instance MightHave top ('Just loc) l s a => MightHave top ('Just ('L loc)) (Pair l r) s a where
+  {-# INLINE mightExtricate1 #-}
+  mightExtricate1 = mightExtricate1 @top @('Just loc) . (\(MkPair l _) -> l)
+
+instance MightHave top ('Just loc) r s a => MightHave top ('Just ('R loc)) (Pair l r) s a where
+  {-# INLINE mightExtricate1 #-}
+  mightExtricate1 = mightExtricate1 @top @('Just loc) . (\(MkPair _ r) -> r)
+
+instance (Has s rc,a ~ FieldType s rc) => MightHave top ('Just 'Here) rc s a where
+  {-# INLINE mightExtricate1 #-}
+  mightExtricate1 = fmap (dub s) . extricate1 s
+    where
+    s = mkLabel @s
+
+-----
+
+type NoBuildPair =
+        'Text "ruin: `"
+  ':<>: 'ShowType Pair
+  ':<>: 'Text "' cannot be an instance of `"
+  ':<>: 'ShowType Build
+  ':<>: 'Text "'"
+
+-- | This is a non-instance.
+instance TypeError NoBuildPair => Build (Pair l r) where
+  type Fields (Pair l r) = Fields l ++ DifferenceByFst (Fields r) (FieldNames l)
+  build = undefined
+  buildNonStrict = undefined
+  type Shape (Pair l r) o = (Hoid Pair o,ZipShape (Pair l r) o)
+
+-----
+
+-- | These record types share no field names.
+type DisjointFields (a :: *) (b :: *) = MustBeDisjoint a b (Intersection (FieldNames a) (FieldNames b))
+
+type family MustBeDisjoint (a :: *) (b :: *) (ss :: [Symbol]) :: Constraint where
+  MustBeDisjoint a b '[] = ()
+  MustBeDisjoint a b ss = TypeError (
+            'Text "ruin: The record types "
+      ':$$: 'Text "  " ':<>: 'ShowType a
+      ':$$: 'Text "and"
+      ':$$: 'Text "  " ':<>: 'ShowType b
+      ':$$: 'Text "must be disjoint, but both have these fields: " ':<>: 'ShowType ss
+    )
+
+infixr 3 <@, `MkPair`
+
+-- | Combine two types that might have 'Has' instances for the same
+-- 'Symbol' @s@. 'Has' on the result will prefer the first argument.
+--
+-- NOTE WELL: 'Pair's are not record types. They only have 'Has'
+-- instances.
+(<@) :: l -> r -> Pair l r
+{-# INLINE (<@) #-}
+(<@) = MkPair
+
+-----
+
+type FieldNames (t :: *) = MapFst (Fields t)
+
+-----
+
+-- | The key difference betwen 'Gives' and 'Has' is that the codomain
+-- is a class index instead of @'FieldType' s rc@. This enables
+-- instances like @Monoid a => 'Gives' s a 'MEmpty'@.
+class Gives (s :: Symbol) (a :: *) (i :: * -> *) (rc :: *) where get :: rc -> Compose Eval i a
+
+type family GivesThis (field :: (Symbol,*)) (i :: * -> *) (rc :: *) :: Constraint where
+  GivesThis f i rc = Gives (Fst f) (Snd f) i rc
+
+type family GivesThese (fields :: [(Symbol,*)]) (i :: * -> *) (rc :: *) :: Constraint where
+  GivesThese '[] i rc = ()
+  GivesThese (f ': fs) i rc = (GivesThis f i rc,GivesThese fs i rc)
+
+-----
+
+-- | A newtype whose only utility is its parametric 'Gives' instance,
+-- which defers to 'Has'.
+newtype GiveAllItHas rc = MkGiveAllItHas rc
+
+instance (Applicative i,a ~ FieldType s rc,Has s rc) => Gives s a i (GiveAllItHas rc) where
+  {-# INLINE get #-}
+  get = \(MkGiveAllItHas rc) -> Compose $ pure <$> extricate1 (mkLabel @s) rc
+
+-- | Like 'GiveAllItHas', but every field in the record must be
+-- headed by the 'Applicative' functor @i@.
+newtype GiveAllItHasA rc = MkGiveAllItHasA rc
+
+instance (i a ~ FieldType s rc,Has s rc) => Gives s a i (GiveAllItHasA rc) where
+  {-# INLINE get #-}
+  get = \(MkGiveAllItHasA rc) -> Compose $ extricate1 (mkLabel @s) rc
+
+-----
+
+-- | The /width subtyping/ relation, with evidence.
+type rc `IsSubtypeOf` t = GivesThese (Fields t) Identity (GiveAllItHas rc)
+
+-- | Record types: product types where each factor has a static name
+-- (i.e. the 'Fields').
+class Build (t :: *) where
+  -- | Each element of this list is the name of a field and its
+  -- type in @t@. Default: 'GenericFields'.
+  --
+  -- [/Unique Names/] These fields have different names.
+  --
+  --     @
+  --       NubByFst ('Fields' t) = 'Fields' t
+  --     @
+  --
+  -- [/Partitioning/] These fields partition @t@.
+  --
+  --     @
+  --       t is isomorphic to a tuple of the types MapSnd ('Fields' t)
+  --     @
+  type Fields (t :: *) :: [(Symbol,*)]
+  type Fields t = GenericFields t
+
+  -- | The laws for 'build' are given without loss of generality in
+  -- terms of 'rupEval'.
+  --
+  -- [/Eta/] An
+  -- <https://ncatlab.org/nlab/show/eta-conversion#for_product_types eta rule>.
+  --
+  --     @
+  --       t '<$' 'rupEval' t = 'rupEval' t
+  --     @
+  --
+  --     This law reasonably requires that @t@ 'Has' all of its own
+  --     'Fields'.
+  --
+  -- [/Strictness/] The 'rupEval' function is strict in its argument,
+  -- but it's only strict enough to retrieve the thunks for each of
+  -- the necessary fields, without forcing those thunks.
+  --
+  --     @
+  --       seq ('rupEval' rc) =
+  --           seq ('extricate1' \#f1 rc)
+  --         . seq ('extricate1' \#f2 rc)
+  --         ...
+  --         . seq ('extricate1' \#fN rc)
+  --     @
+  --
+  -- If @rc@ is a typical single-constructor record type declared with
+  -- record syntax and has fields for all of @t@'s 'Fields', then the
+  -- /Strictness/ law simplifies to @seq ('rupEval' rc) = seq rc@.
+  --
+  -- [__Note__] A @GHC.Generics@ default is available as
+  -- 'genericBuild'. We do not provide a @DefaultSignature@ because it
+  -- is most often critical for performance that 'build' is inlined,
+  -- which requires an explicit @INLINE@ pragma (the RHS size gets too
+  -- large for inferred inlining with even just three fields). We thus
+  -- recommend the following.
+  --
+  --     @
+  --       instance 'Build' Foo where
+  --         {-\# INLINE 'build' #-}
+  --         'build' = 'genericBuild'
+  --     @
+  build :: (Applicative i,GivesThese (Fields t) i rc) => rc -> Compose Eval i t
+
+  -- | Like 'build', but maximally non-strict instead of having the
+  -- /Strictness/ law. Defaults to 'genericBuildNonStrict', but beware
+  -- that a manual @INLINE@ pragma is likely as useful as it is for
+  -- 'build'.
+  --
+  --     @
+  --       seq ('build' rc) ('buildNonStrict' rc) = 'runEval' ('build' rc)
+  --     @
+  buildNonStrict :: GivesThese (Fields t) Identity rc => rc -> t
+  default buildNonStrict ::
+        ( Fields t ~ GenericFields t
+        , Generic t
+        , GenericBuild t (Rep t)
+        , GivesThese (Fields t) Identity rc
+        )
+     => rc -> t
+  buildNonStrict = genericBuildNonStrict
+
+  -- | The shape of a record type is its most general type, the one
+  -- that all instances of that record type are specializations of.
+  -- Unless you're being clever, the shape of the type class index @t@
+  -- is @t@, since that @t@ is usually as polymorphic as it could be
+  -- (i.e. the value that the type variables within @t@ take on do not
+  -- change how it instantiates 'Build').
+  --
+  -- The @'Shape' t o@ constraint requires --- via @~@ --- that @o@
+  -- has the same shape as @t@. It must use @~@ to assert this
+  -- requirement, so that it can guide type inference.
+  --
+  -- 'Shape' defaults to 'GenericShape', which is correct for data
+  -- types declared with record syntax except for data family
+  -- instances. See 'GenericShape' for more info.
+  type Shape (t :: *) (o :: *) :: Constraint
+  type Shape t o = GenericShape t o
+
+-- | Unify the shape of two record types; see 'Shape'.
+type UnifyShape l r = (Shape l r,Shape r l)
+
+-- | Like 'asTypeOf', but doesn't require that the fields have the
+-- same types, only that the record types have the same shape.
+asShapeOf :: UnifyShape l r => l -> r -> l
+{-# INLINE asShapeOf #-}
+asShapeOf = const
+
+type family UnifyFieldTypes (ss :: [Symbol]) (t :: *) (h :: *) :: Constraint where
+  UnifyFieldTypes '[] _ _ = ()
+  UnifyFieldTypes (s ': ss) t h = (FieldType s t ~ FieldType s h,UnifyFieldTypes ss t h)
+
+asFieldTypesOf :: UnifyFieldTypes (FieldNames t) t rc => t -> proxy rc -> t
+{-# INLINE asFieldTypesOf #-}
+asFieldTypesOf = const
+
+-- | @'GenericShape' t o@ requires that @o@ is headed by the same type
+-- constructor that heads @t@:
+--
+-- @
+--   'GenericShape' (T ...) o = 'Hoid' T o
+-- @
+--
+-- This is the correct definition of 'Shape' for all data types
+-- declared using record syntax, except for data family instances. For
+-- those, the @T@ part should be replaced by the head of the data
+-- family instance: the type up to and including the indices but
+-- excluding the non-index parameters.
+type family GenericShape (t :: k) (o :: *) :: Constraint where
+  GenericShape (f _) o = GenericShape f o
+  GenericShape t o = Hoid t o
+
+-- | When @tup@ is a product of records (e.g. 'Pair' or '(,,,)'),
+-- this constraint applies 'Shape' to the pairwise components.
+type family ZipShape (tup :: k) (o :: k) :: Constraint where
+  ZipShape (f a) (g b) = (ZipShape f g,Shape a b)
+  ZipShape _ _ = ()
+
+-- | 'rup' is an upcast with respect to the /width subtyping/
+-- relationship of records; it 'build's a @t@ from any type that has
+-- all of @t@'s 'Fields'.
+rup :: forall t rc. (Build t,rc `IsSubtypeOf` t) => rc -> t
+{-# INLINE rup #-}
+rup = runEval . rupEval
+
+-- | 'rup' is an upcast with respect to the /width subtyping/
+-- relationship of records; it 'build's a @t@ from any type that has
+-- all of @t@'s 'Fields'.
+rupA :: forall t rc i. (Applicative i,Build t,GivesThese (Fields t) i (GiveAllItHasA rc)) => rc -> i t
+{-# INLINE rupA #-}
+rupA = runEval . getCompose . build . MkGiveAllItHasA
+
+-- | @'rup' = 'runEval' . 'rupEval'@
+--
+-- @'rupEval' = 'build' . 'MkGiveAllItHas'@
+rupEval :: forall t rc. (Build t,rc `IsSubtypeOf` t) => rc -> Eval t
+{-# INLINE rupEval #-}
+rupEval = fmap runIdentity . getCompose . build . MkGiveAllItHas
+
+-- | @'rupNonStrict' = 'buildNonStrict' . 'MkGiveAllItHas'@
+rupNonStrict :: forall t rc. (Build t,rc `IsSubtypeOf` t) => rc -> t
+{-# INLINE rupNonStrict #-}
+rupNonStrict = buildNonStrict . MkGiveAllItHas
+
+-- | "GHC.Generics" implementation of 'Fields'.
+type GenericFields t = GFields (Rep t)
+
+-- | "GHC.Generics" implementation of 'rup'.
+--
+-- Relies on 'extricate1' in order to satisfy the /Strictness/ law of
+-- 'Build'.
+genericBuild ::
+  forall t rc i.
+      ( Fields t ~ GenericFields t
+      , Applicative i
+      , Generic t
+      , GenericBuild t (Rep t)
+      , GivesThese (Fields t) i rc
+      )
+   => rc -> Compose Eval i t
+{-# INLINE genericBuild #-}
+genericBuild = fmap to . gRup @t
+
+-- | "GHC.Generics" implementation of 'buildNonStrict'.
+--
+-- It is maximally non-strict.
+genericBuildNonStrict ::
+  forall t rc.
+      ( Fields t ~ GenericFields t
+      , Generic t
+      , GenericBuild t (Rep t)
+      , GivesThese (Fields t) Identity rc
+      )
+   => rc -> t
+{-# INLINE genericBuildNonStrict #-}
+genericBuildNonStrict = to . gBuildNonStrict @t
+
+-----
+
+type NoFun t =
+        'Text "ruin: There is no meaningful instance of `"
+  ':<>: 'ShowType t
+  ':<>: 'Text "' for functions."
+  ':$$: 'Text "  Perhaps you omitted an argument?"
+
+-- | This is a non-instance.
+instance TypeError (NoFun Build) => Build (a -> b) where
+  type Fields (a -> b) = TypeError (NoFun Build)
+  build = undefined
+  buildNonStrict = undefined
+
+instance Build () where
+  {-# INLINE build #-}
+  build rc = genericBuild rc
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict rc = genericBuildNonStrict rc
+
+instance Build (s :@ a) where
+  type Fields (s :@ a) = '[ '(s,a) ]
+  {-# INLINE build #-}
+  build = fmap (dub mkLabel) . get @s
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = runCEI . build
+  type Shape (s :@ _) o = Hoid ((:@) s) o
+
+instance Build a => Build (Tup1 a) where
+  type Fields (Tup1 a) = Fields a
+  {-# INLINE build #-}
+  build = fmap MkTup1 . build
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = MkTup1 . buildNonStrict
+  type Shape (Tup1 a) o = (Hoid Tup1 o,ZipShape (Tup1 a) o)
+
+type family ShapeTup1 (a :: *) (o :: *) where
+  ShapeTup1 a (Tup1 oa) = Shape a oa
+
+instance
+  ( DisjointFields a b   -- necessary for the eta-rule of 'Build'
+  , Lemma_AppendGivesThese (Fields a)
+  , Build a
+  , Build b
+  ) => Build (a,b) where
+  type Fields (a,b) = Fields a ++ Fields b
+  {-# INLINE build #-}
+  build :: forall i rc. (Applicative i,GivesThese (Fields (a,b)) i rc) => rc -> Compose Eval i (a,b)
+  build rc =
+        (,)
+    <$> lemmaFst @(Fields a) (proxy# :: Proxy# i) (proxy# :: Proxy# (Fields b)) build rc
+    <*> lemmaSnd @(Fields a) (proxy# :: Proxy# i) (proxy# :: Proxy# (Fields b)) build rc
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict rc =
+    ( lemmaFst @(Fields a) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (Fields b)) buildNonStrict rc
+    , lemmaSnd @(Fields a) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (Fields b)) buildNonStrict rc )
+  type Shape (a,b) o = (Hoid (,) o,ZipShape (a,b) o)
+
+instance Build ((a,b),c) => Build (a,b,c) where
+  type Fields (a,b,c) = Fields (a,b) ++ Fields c
+  {-# INLINE build #-}
+  build = \rc -> assoc <$> build rc
+    where
+    assoc ((a,b),c) = (a,b,c)
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = \rc -> assoc (buildNonStrict rc)
+    where
+    assoc ~(~(a,b),c) = (a,b,c)
+  type Shape (a,b,c) o = (Hoid (,,) o,ZipShape (a,b,c) o)
+
+instance Build ((a,b),(c,d)) => Build (a,b,c,d) where
+  type Fields (a,b,c,d) = Fields (a,b) ++ Fields (c,d)
+  {-# INLINE build #-}
+  build = \rc -> assoc <$> build rc
+    where
+    assoc ((a,b),(c,d)) = (a,b,c,d)
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = \rc -> assoc (buildNonStrict rc)
+    where
+    assoc ~(~(a,b),~(c,d)) = (a,b,c,d)
+  type Shape (a,b,c,d) o = (Hoid (,,,) o,ZipShape (a,b,c,d) o)
+
+instance Build ((a,b,c),(d,e)) => Build (a,b,c,d,e) where
+  type Fields (a,b,c,d,e) = Fields (a,b,c) ++ Fields (d,e)
+  {-# INLINE build #-}
+  build = \rc -> assoc <$> build rc
+    where
+    assoc ((a,b,c),(d,e)) = (a,b,c,d,e)
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = \rc -> assoc (buildNonStrict rc)
+    where
+    assoc ~(~(a,b,c),~(d,e)) = (a,b,c,d,e)
+  type Shape (a,b,c,d,e) o = (Hoid (,,,,) o,ZipShape (a,b,c,d,e) o)
+
+instance Build ((a,b,c),(d,e,f)) => Build (a,b,c,d,e,f) where
+  type Fields (a,b,c,d,e,f) = Fields (a,b,c) ++ Fields (d,e,f)
+  {-# INLINE build #-}
+  build = \rc -> assoc <$> build rc
+    where
+    assoc ((a,b,c),(d,e,f)) = (a,b,c,d,e,f)
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = \rc -> assoc (buildNonStrict rc)
+    where
+    assoc ~(~(a,b,c),~(d,e,f)) = (a,b,c,d,e,f)
+  type Shape (a,b,c,d,e,f) o = (Hoid (,,,,,) o,ZipShape (a,b,c,d,e,f) o)
+
+instance Build ((a,b,c,d),(e,f,g)) => Build (a,b,c,d,e,f,g) where
+  type Fields (a,b,c,d,e,f,g) = Fields (a,b,c,d) ++ Fields (e,f,g)
+  {-# INLINE build #-}
+  build = \rc -> assoc <$> build rc
+    where
+    assoc ((a,b,c,d),(e,f,g)) = (a,b,c,d,e,f,g)
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = \rc -> assoc (buildNonStrict rc)
+    where
+    assoc ~(~(a,b,c,d),~(e,f,g)) = (a,b,c,d,e,f,g)
+  type Shape (a,b,c,d,e,f,g) o = (Hoid (,,,,,,) o,ZipShape (a,b,c,d,e,f,g) o)
+
+instance Build ((a,b,c,d),(e,f,g,h)) => Build (a,b,c,d,e,f,g,h) where
+  type Fields (a,b,c,d,e,f,g,h) = Fields (a,b,c,d) ++ Fields (e,f,g,h)
+  {-# INLINE build #-}
+  build = \rc -> assoc <$> build rc
+    where
+    assoc ((a,b,c,d),(e,f,g,h)) = (a,b,c,d,e,f,g,h)
+  {-# INLINE buildNonStrict #-}
+  buildNonStrict = \rc -> assoc (buildNonStrict rc)
+    where
+    assoc ~(~(a,b,c,d),~(e,f,g,h)) = (a,b,c,d,e,f,g,h)
+  type Shape (a,b,c,d,e,f,g,h) o = (Hoid (,,,,,,,) o,ZipShape (a,b,c,d,e,f,g,h) o)
+
+-----
+
+-- | If @'Has' (fs1 '++' fs2) rc@, then @'Has' fs1 rc@ and @'Has' fs2
+-- rc@.
+class Lemma_AppendGivesThese (fs1 :: [(Symbol,*)]) where
+    lemmaFst :: GivesThese (fs1 ++ fs2) i rc => Proxy# i -> Proxy# fs2 -> (GivesThese fs1 i rc => rc -> a) -> rc -> a
+    lemmaSnd :: GivesThese (fs1 ++ fs2) i rc => Proxy# i -> Proxy# fs2 -> (GivesThese fs2 i rc => rc -> a) -> rc -> a
+
+instance Lemma_AppendGivesThese '[] where
+  {-# INLINE lemmaFst #-}
+  lemmaFst _ _ k = k
+  {-# INLINE lemmaSnd #-}
+  lemmaSnd _ _ k = k
+
+instance Lemma_AppendGivesThese fs1 => Lemma_AppendGivesThese (f ': fs1) where
+  {-# INLINE lemmaFst #-}
+  lemmaFst i fs2 k = lemmaFst @fs1 i fs2 k
+  {-# INLINE lemmaSnd #-}
+  lemmaSnd i fs2 k = lemmaSnd @fs1 i fs2 k
+
+-----
+
+type t `IsSymmetricRecordOf` rc =
+  ( t `IsSubtypeOf` rc
+  , NoExtraFields t rc (FieldNames t) (FieldNames rc)
+  )
+
+-- | This layer stalls until both sets of fields are known. This is
+-- just to provide terser constraints in the contexts of inferred polytypes.
+type family NoExtraFields (t :: *) (rc :: *) (sts :: [Symbol]) (srcs :: [Symbol]) :: Constraint where
+  NoExtraFields _ rc '[]       '[]           = MustHaveNoExtras rc (Difference '[] '[])
+  NoExtraFields _ rc (f ': fs) '[]           = MustHaveNoExtras rc (Difference '[] (f ': fs))
+  NoExtraFields _ rc '[]       (src ': srcs) = MustHaveNoExtras rc (Difference (src ': srcs) '[])
+  NoExtraFields _ rc (f ': fs) (src ': srcs) = MustHaveNoExtras rc (Difference (src ': srcs) (f ': fs))
+
+type family MustHaveNoExtras (rc :: *) (ss :: [Symbol]) :: Constraint where
+  MustHaveNoExtras rc '[] = ()
+  MustHaveNoExtras rc ss = TypeError (
+            'Text "ruin: The argument type"
+      ':$$: 'Text "  " ':<>: 'ShowType rc
+      ':$$: 'Text "has unused fields: " ':<>: 'ShowType ss
+    )
+
+-- | An isomorphism based on 'rup', when the two record types have a
+-- symmetric subtyping relation.
+--
+-- [Isomorphism]
+--
+--     @
+--       forall t s.
+--         ( s '`IsSubtypeOf`' t,'Build' s
+--         , t '`IsSubtypeOf`' s,'Build' t
+--         ) => 'rsym' . id \@t . 'rsym' = id \@s
+--     @
+rsym ::
+    (l `IsSymmetricRecordOf` r,Build r)
+ => l -> r
+{-# INLINE rsym #-}
+rsym = rup
+
+-- | @'rto' \@h = 'hoid' \@h . 'rsym'@
+rto :: forall h t rc. (Hoid h t,rc `IsSymmetricRecordOf` t,Build t) => rc -> t
+{-# INLINE rto #-}
+rto = hoid @h . rsym
+
+-- | @'rfrom' \@h = 'rsym' . 'hoid' \@h@
+rfrom :: forall h rc t. (Hoid h rc,rc `IsSymmetricRecordOf` t,Build t) => rc -> t
+{-# INLINE rfrom #-}
+rfrom = rsym . hoid @h
+
+prto :: forall h t rc. (Hoid h t,rc `IsSymmetricRecordOf` t,Build t) => Proxy# h -> rc -> t
+{-# INLINE prto #-}
+prto _ = rto @h
+
+prtoA ::
+  forall h t rc i.
+     (Hoid h t,Applicative i,SymmetricRecordsA t i rc,Build t)
+  => Proxy# h
+  -> rc -> i t
+{-# INLINE prtoA #-}
+prtoA _ = rtoA @h
+
+prfrom :: forall h rc t. (Hoid h rc,rc `IsSymmetricRecordOf` t,Build t) => Proxy# h -> rc -> t
+{-# INLINE prfrom #-}
+prfrom _ = rfrom @h
+
+rsymA ::
+    (Applicative i,SymmetricRecordsA t i rc,Build t)
+ => rc -> i t
+{-# INLINE rsymA #-}
+rsymA = rupA
+
+rtoA ::
+  forall h t rc i.
+     (Hoid h t,Applicative i,SymmetricRecordsA t i rc,Build t)
+  => rc -> i t
+{-# INLINE rtoA #-}
+rtoA = rsymA
+
+rfromA ::
+  forall h rc t i.
+     (Hoid h rc,Applicative i,SymmetricRecordsA t i rc,Build t)
+  => rc -> i t
+{-# INLINE rfromA #-}
+rfromA = rsymA . hoid @h
+
+type SymmetricRecordsA t i rc =
+  ( GivesThese (Fields t) i (GiveAllItHasA rc)
+  , NoExtraFields t rc (FieldNames t) (FieldNames rc)
+  )
+
+-----
+
+type family GFields (rep :: * -> *) :: [(Symbol,*)] where
+  GFields (M1 D c rep) = GFields rep
+  GFields (M1 C c rep) = GFields rep
+  GFields (M1 S ('MetaSel ('Just s) su ss ds) (K1 i c)) = '[ '(s,c) ]
+  GFields (l :*: r) = GFields l ++ GFields r
+  GFields U1 = '[]
+
+-----
+
+-- | Generic defintion of 'rup'.
+class GenericBuild (top :: *) (rep :: * -> *) where
+    gRup :: (Applicative i,GivesThese (GFields rep) i rc) => rc -> Compose Eval i (rep x)
+    gBuildNonStrict :: GivesThese (GFields rep) Identity rc => rc -> rep x
+
+type NoConstructors (dn :: Symbol) =
+        'Text "ruin: Cannot derive "
+  ':<>: 'ShowType Build
+  ':<>: 'Text " for `"
+  ':<>: 'Text dn
+  ':<>: 'Text "' because it doesn't have any constructors."
+
+instance TypeError (NoConstructors dn) => GenericBuild top (M1 D ('MetaData dn mn pn nt) V1) where
+  gRup = undefined
+  gBuildNonStrict = undefined
+
+type TooManyConstructors (dn :: Symbol) =
+        'Text "ruin: Cannot derive "
+  ':<>: 'ShowType Build
+  ':<>: 'Text " for `"
+  ':<>: 'Text dn
+  ':<>: 'Text "' because it has more than one constructor."
+
+instance TypeError (TooManyConstructors dn) => GenericBuild top (M1 D ('MetaData dn mn pn nt) (l :+: r)) where
+  gRup = undefined
+  gBuildNonStrict = undefined
+
+instance GenericBuildConArgs top dn rep => GenericBuild top (M1 D ('MetaData dn mn pn nt) (M1 C c rep)) where
+  {-# INLINE gRup #-}
+  gRup rc = (M1 . M1) <$> gRupConArgs @top @dn rc
+  {-# INLINE gBuildNonStrict #-}
+  gBuildNonStrict rc = M1 (M1 (gBuildNonStrictConArgs @top @dn rc))
+
+class GenericBuildConArgs (top :: *) (dn :: Symbol) (rep :: * -> *) where
+  -- | Use 'Eval' so that we can project out the components from @rc@
+  -- /before/ building the @rep@.
+  gRupConArgs :: (Applicative i,GivesThese (GFields rep) i rc) => rc -> Compose Eval i (rep x)
+  gBuildNonStrictConArgs :: GivesThese (GFields rep) Identity rc => rc -> rep x
+
+instance (Lemma_AppendGivesThese (GFields l),GenericBuildConArgs top dn l,GenericBuildConArgs top dn r) => GenericBuildConArgs top dn (l :*: r) where
+  {-# INLINE gRupConArgs #-}
+  gRupConArgs :: forall i rc x. (Applicative i,GivesThese (GFields (l :*: r)) i rc) => rc -> Compose Eval i ((l :*: r) x)
+  gRupConArgs rc =
+        (:*:)
+    <$> lemmaFst @(GFields l) (proxy# :: Proxy# i) (proxy# :: Proxy# (GFields r)) (gRupConArgs @top @dn) rc
+    <*> lemmaSnd @(GFields l) (proxy# :: Proxy# i) (proxy# :: Proxy# (GFields r)) (gRupConArgs @top @dn) rc
+  {-# INLINE gBuildNonStrictConArgs #-}
+  gBuildNonStrictConArgs rc =
+        lemmaFst @(GFields l) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (GFields r)) (gBuildNonStrictConArgs @top @dn) rc
+    :*: lemmaSnd @(GFields l) (proxy# :: Proxy# Identity) (proxy# :: Proxy# (GFields r)) (gBuildNonStrictConArgs @top @dn) rc
+
+type NotBuildSyntax (dn :: Symbol) =
+        'Text "ruin: Cannot derive "
+  ':<>: 'ShowType Build
+  ':<>: 'Text " for `"
+  ':<>: 'Text dn
+  ':<>: 'Text "' because its definition doesn't use record type syntax."
+
+instance TypeError (NotBuildSyntax dn) => GenericBuildConArgs top dn (M1 S ('MetaSel 'Nothing su ss ds) rep) where
+  gRupConArgs = undefined
+  gBuildNonStrictConArgs = undefined
+
+-- The @'Has' s top@ constraint is not strictly necessary, but gives
+-- the user a more precise error message when they forget that
+-- instance.
+instance (Has s top,rep ~ K1 i c) => GenericBuildConArgs top dn (M1 S ('MetaSel ('Just s) su ss ds) rep) where
+  {-# INLINE gRupConArgs #-}
+  gRupConArgs = fmap (M1 . K1) . get @s
+  {-# INLINE gBuildNonStrictConArgs #-}
+  gBuildNonStrictConArgs = M1 . K1 . runCEI . get @s
+
+instance GenericBuildConArgs top dn U1 where
+  {-# INLINE gRupConArgs #-}
+  gRupConArgs _ = pure U1
+  {-# INLINE gBuildNonStrictConArgs #-}
+  gBuildNonStrictConArgs _ = U1
+
+-----
+
+-- | @t@ has a field named @s@ that inhabits @'FieldType' s t@.
+--
+-- #careful-strictness#
+--
+-- 'extricate1' projects out the field, with special care to
+-- strictness. The 'Eval' layer provides a stopping point for the
+-- projection computation. Without this layer, one would have to force
+-- the value itself in order to force the extrication enough so that
+-- the rest of @t@ could be GC'd. On the contrary, @case 'extricate1' t
+-- of 'Done' x -> x@ neither retains @t@ nor forces @x@.
+--
+-- [/Strictness/] Forcing the 'Done' layer of 'extricate1' forces
+-- enough of @t@ to reach the field but doesn't force the field. This
+-- is difficult to formalize in a general and illuminating way, so
+-- this law is instantiated below for a simple record type.
+--
+--     @
+--       data XY = MkXY {x,y :: Int}
+--
+--       'extricate1' #x (undefined :: XY) = undefined
+--
+--       flip seq () $ 'extricate1' #x (MkXY undefined undefined) = ()
+--     @
+class Has (s :: Symbol) (t :: *) where
+  -- | Default: 'GenericFieldType'
+  type FieldType s t :: *
+  type FieldType s t = GenericFieldType s t
+
+  -- | Default: 'genericExtricate1'
+  extricate1 :: Label s -> t -> Eval (FieldType s t)
+
+  default extricate1 :: (Generic t,GBox (IsABox (Rep t)) t,GenericHas (Rep t) s (FieldType s t)) => Label s -> t -> Eval (FieldType s t)
+  {-# INLINE extricate1 #-}
+  extricate1 = genericExtricate1
+
+-- | "GHC.Generics" implementation of 'FieldType'.
+type GenericFieldType s t = GFieldType (GFind (Rep t) s) (Rep t)
+
+-- | "GHC.Generics" implementation of 'extricate1'.
+genericExtricate1 ::
+  forall s t.
+     (Generic t,GBox (IsABox (Rep t)) t,GenericHas (Rep t) s (FieldType s t))
+  => Label s -> t -> Eval (FieldType s t)
+{-# INLINE genericExtricate1 #-}
+genericExtricate1 = \_ t -> fmap (undub (mkLabel @s)) $ fromEval @(IsABox (Rep t)) t >>= gExtricate1
+
+-- | See 'GBox'.
+type family IsABox (rep :: * -> *) :: Bool where
+  IsABox (M1 D ('MetaData _ _ _ 'False) (M1 C c (M1 S s (K1 k a)))) = 'True
+  IsABox _ = 'False
+
+-- | This class distinguishes between @data T a = MkT a@ and @data T a
+-- = Mk !a@/@newtype T a = MkT a@, since 'Generic''s 'from' conflates
+-- the two.
+--
+-- The first index is assumed to be @('IsABox' (Rep t))@.
+class GBox (isABox :: Bool) (t :: *) where
+  fromEval :: t -> Eval (Rep t x)
+
+instance Generic t => GBox 'False t where
+  {-# INLINE fromEval #-}
+  fromEval = pure . from
+instance Generic t => GBox 'True t where
+  {-# INLINE fromEval #-}
+  fromEval t = t `seq` pure (from t)
+
+-----
+
+type family GFieldType (ml :: Maybe Loc) (rep :: * -> *) :: * where
+  GFieldType ('Just 'Here) (M1 S ('MetaSel ('Just s) su ss ds) (K1 i c)) = c
+  GFieldType ('Just loc) (M1 i c rep) = GFieldType ('Just loc) rep
+  GFieldType ('Just ('L loc)) (l :*: r) = GFieldType ('Just loc) l
+  GFieldType ('Just ('R loc)) (l :*: r) = GFieldType ('Just loc) r
+
+-----
+
+-- | This is a non-instance.
+instance TypeError (NoFun Has) => Has s (a -> b) where
+  type FieldType s (a -> b) = TypeError (NoFun Has)
+  extricate1 = undefined
+
+-- | This is a non-instance.
+instance TypeError (NoSuchField s ()) => Has s () where
+  type FieldType s () = TypeError (NoSuchField s ())
+  extricate1 = undefined
+
+-----
+
+infix 1 :@
+
+-- | A record type with a single field.
+newtype (s :: Symbol) :@ (a :: *) = Dub a
+  deriving (Binary,Data,Eq,Functor,Generic,Generic1,NFData,Ord,Serialize)
+
+type family SingletonType (singleton :: *) :: * where SingletonType (_ :@ a) = a
+type family FunctorType (fa :: *) :: * -> * where FunctorType (f _) = f
+
+instance (s1 ~ s2) => Has s1 (s2 :@ a) where
+  type FieldType s1 (s2 :@ a) = a
+  {-# INLINE extricate1 #-}
+  extricate1 = \_ -> pure . undub mkLabel
+
+instance (Lift a,KnownSymbol s) => Lift (s :@ a) where
+  lift (Dub a) =
+    [| dub (mkLabel :: Label $(TH.litT (TH.strTyLit s))) a |]
+    where
+    s = symbolVal' (proxy# :: Proxy# s)
+
+instance (KnownSymbol s,Show a) => Show (s :@ a) where
+  showsPrec d (Dub a) = showParen (d > app_prec) $
+    prefix . showsPrec (app_prec+1) a
+    where
+    app_prec = 10
+    prefix
+     | hasEscapes || hasSpaces = showString "dub (mkLabel @" . showString s' . showString ") "
+     | otherwise = showString "dub #" . showString s . showString " "
+    s = symbolVal' (proxy# :: Proxy# s)
+    s' = show s
+    hasEscapes = s' /= '"' : s ++ ['"']
+    hasSpaces = any isSpace s
+
+dub :: Label s -> a -> s :@ a
+{-# INLINE dub #-}
+dub = \_ -> Dub
+
+undub :: Label s -> s :@ a -> a
+{-# INLINE undub #-}
+undub = \_ (Dub a) -> a
+
+-----
+
+-- | Generic definition of 'has'.
+class GenericHas (rep :: * -> *) (s :: Symbol) (a :: *) where
+    gExtricate1 :: rep x -> Eval (s :@ a)
+
+instance GArgsHas dn (GFind conargs s) conargs s a => GenericHas (M1 D ('MetaData dn mn pn nt) (M1 C c conargs)) s a where
+  {-# INLINE gExtricate1 #-}
+  gExtricate1 = gArgsExtricate1 @dn @(GFind conargs s) . unM1 . unM1
+
+type Not1ConstructorMessage (dn :: Symbol) =
+        'Text "ruin: The type `"
+  ':<>: 'Text dn
+  ':<>: 'Text "' must have exactly one constructor to derive `"
+  ':<>: 'ShowType Has
+  ':<>: 'Text "'"
+
+instance TypeError (Not1ConstructorMessage dn) => GenericHas (M1 D ('MetaData dn mn pn nt) (l :+: r)) s a where
+  gExtricate1 = undefined
+
+instance TypeError (Not1ConstructorMessage dn) => GenericHas (M1 D ('MetaData dn mn pn nt) V1) s a where
+  gExtricate1 = undefined
+
+type family GFind (rep :: * -> *) (s :: Symbol) :: Maybe Loc where
+  GFind (M1 S ('MetaSel ('Just s) su ss ds) rep) s = 'Just 'Here
+  GFind (M1 i c rep) s = GFind rep s   -- only used for GFieldType
+  GFind (l :*: r) s = MergeLoc (GFind l s) (GFind r s)
+  GFind rep s = 'Nothing
+
+type family MergeLoc (l :: Maybe Loc) (r :: Maybe Loc) :: Maybe Loc where
+  MergeLoc 'Nothing 'Nothing = 'Nothing
+  MergeLoc 'Nothing ('Just r) = 'Just ('R r)
+  MergeLoc ('Just l) _ = 'Just ('L l)
+
+class GArgsHas (dn :: Symbol) (ml :: Maybe Loc) (rep :: * -> *) (s :: Symbol) (a :: *) where
+    gArgsExtricate1 :: rep x -> Eval (s :@ a)
+
+type NoSuchSelector (dn :: Symbol) (s :: Symbol) =
+        'Text "ruin: The type `"
+  ':<>: 'Text dn
+  ':<>: 'Text "' must declare a record selector named `"
+  ':<>: 'Text s
+  ':<>: 'Text "' to derive `"
+  ':<>: 'ShowType Has
+  ':<>: 'Text " "
+  ':<>: 'ShowType s
+  ':<>: 'Text "'"
+
+instance TypeError (NoSuchSelector dn s) => GArgsHas dn 'Nothing rep s a where
+  gArgsExtricate1 = undefined
+
+instance (rep ~ K1 i a) => GArgsHas dn ('Just 'Here) (M1 S ('MetaSel ('Just s) su ss ds) rep) s a where
+  {-# INLINE gArgsExtricate1 #-}
+  gArgsExtricate1 = pure . dub mkLabel . unK1 . unM1
+
+instance GArgsHas dn ('Just loc) l s a => GArgsHas dn ('Just ('L loc)) (l :*: r) s a where
+  {-# INLINE gArgsExtricate1 #-}
+  gArgsExtricate1 (l :*: _) = gArgsExtricate1 @dn @('Just loc) l
+
+instance GArgsHas dn ('Just loc) r s a => GArgsHas dn ('Just ('R loc)) (l :*: r) s a where
+  {-# INLINE gArgsExtricate1 #-}
+  gArgsExtricate1 (_ :*: r) = gArgsExtricate1 @dn @('Just loc) r
+
+-----
+
+instance Has s a => Has s (Tup1 a) where
+  type FieldType s (Tup1 a) = FieldType s a
+  {-# INLINE extricate1 #-}
+  extricate1 s = \(MkTup1 x) -> extricate1 s x
+
+instance (DisjointFields a b,Has s (Pair a b)) => Has s (a,b) where
+  type FieldType s (a,b) = FieldType s (Pair a b)
+  {-# INLINE extricate1 #-}
+  extricate1 s = extricate1 s . uncurry (<@)
+
+instance Has s ((a,b),c) => Has s (a,b,c) where
+  type FieldType s (a,b,c) = FieldType s ((a,b),c)
+  {-# INLINE extricate1 #-}
+  extricate1 = \s -> extricate1 s . reassoc
+    where
+    reassoc (a,b,c) = ((a,b),c)
+
+instance Has s ((a,b),(c,d)) => Has s (a,b,c,d) where
+  type FieldType s (a,b,c,d) = FieldType s ((a,b),(c,d))
+  {-# INLINE extricate1 #-}
+  extricate1 = \s -> extricate1 s . reassoc
+    where
+    reassoc (a,b,c,d) = ((a,b),(c,d))
+
+instance Has s ((a,b,c),(d,e)) => Has s (a,b,c,d,e) where
+  type FieldType s (a,b,c,d,e) = FieldType s ((a,b,c),(d,e))
+  {-# INLINE extricate1 #-}
+  extricate1 = \s -> extricate1 s . reassoc
+    where
+    reassoc (a,b,c,d,e) = ((a,b,c),(d,e))
+
+instance Has s ((a,b,c),(d,e,f)) => Has s (a,b,c,d,e,f) where
+  type FieldType s (a,b,c,d,e,f) = FieldType s ((a,b,c),(d,e,f))
+  {-# INLINE extricate1 #-}
+  extricate1 = \s -> extricate1 s . reassoc
+    where
+    reassoc (a,b,c,d,e,f) = ((a,b,c),(d,e,f))
+
+instance Has s ((a,b,c,d),(e,f,g)) => Has s (a,b,c,d,e,f,g) where
+  type FieldType s (a,b,c,d,e,f,g) = FieldType s ((a,b,c,d),(e,f,g))
+  {-# INLINE extricate1 #-}
+  extricate1 = \s -> extricate1 s . reassoc
+    where
+    reassoc (a,b,c,d,e,f,g) = ((a,b,c,d),(e,f,g))
+
+instance Has s ((a,b,c,d),(e,f,g,h)) => Has s (a,b,c,d,e,f,g,h) where
+  type FieldType s (a,b,c,d,e,f,g,h) = FieldType s ((a,b,c,d),(e,f,g,h))
+  {-# INLINE extricate1 #-}
+  extricate1 = \s -> extricate1 s . reassoc
+    where
+    reassoc (a,b,c,d,e,f,g,h) = ((a,b,c,d),(e,f,g,h))
+
+-----
+
+-- | Get the labels of a record type's fields.
+fieldLabelsOf :: forall t proxy. proxy t -> Labels (FieldNames t)
+fieldLabelsOf _ = mkLabels @(FieldNames t)
diff --git a/Data/Ruin/Ancillaries.hs b/Data/Ruin/Ancillaries.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Ancillaries.hs
@@ -0,0 +1,80 @@
+{-# Language ExplicitNamespaces #-}
+
+-- | How the sausage is made.
+--
+-- These definitions are typically not revealed to the user, unless
+-- you're doing something cheeky. So they are hidden behind this extra
+-- import.
+
+module Data.Ruin.Ancillaries (
+  -- * Type-level basics
+  type (++),
+  Difference,
+  DifferenceByFst,
+  Elem,
+  Fst,
+  Head,
+  Intersection,
+  MapFst,
+  Snd,
+  Tail,
+  -- * Disjointedness
+  DisjointFields,
+  MustBeDisjoint,
+  MustHaveNoExtras,
+  -- * Search
+  Find,
+  FindViaFields,
+  Loc(..),
+  MergeLoc,
+  MightHave,
+  Pair(..),
+  SearchBoth,
+  unPair,
+  -- * Generics
+  GArgsHas,
+  GBox,
+  GFieldType,
+  GFields,
+  GFind,
+  GenericBuildConArgs,
+  IsABox,
+  -- ** @GHC.Generics@ defaults
+  GenericBuild,
+  GenericFieldType,
+  GenericFields,
+  GenericHas,
+  GenericShape,
+  genericExtricate1,
+  genericBuild,
+  genericBuildNonStrict,
+
+  -- * Proxied
+  --
+  -- Template Haskell doesn't yet support type applications, so these
+  -- can be handy.
+  phoid,
+  prfrom,
+  prto,
+  -- * Miscellancy
+  (:@)(..),
+  FieldNames,
+  IsSubtypeOf,
+  IsSymmetricRecordOf,
+  Gives(..),
+  GiveAllItHas(..),
+  GivesThese,
+  GivesThis,
+  Hoid,
+  Label(..),
+  Lemma_AppendGivesThese,
+  SymmetricRecordsA,
+  Tup1(..),
+  mkLabel,
+  rupEval,
+  rupNonStrict,
+  ) where
+
+import Data.Ruin.All
+import Data.Ruin.Hoid
+import Data.Ruin.Internal
diff --git a/Data/Ruin/ClosedHas.hs b/Data/Ruin/ClosedHas.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/ClosedHas.hs
@@ -0,0 +1,76 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language ConstraintKinds #-}
+{-# Language DataKinds #-}
+{-# Language DefaultSignatures #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language KindSignatures #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+-- | This modules makes it possible to declare that a type 'Has'
+-- /only/ its 'Fields'. This can lead to better type error messages.
+--
+-- These classses should be instantiated as follows. Note that
+-- 'Data.Ruin.TH.makeRecords' does this automatically.
+--
+-- @
+--   data XY x y = MkXY {x::x,y::y} deriving Generic
+--
+--   instance 'ClosedHas' s XY => 'Has' s XY where
+--     {-\# INLINE 'extricate1' #-}
+--     'extricate1' = 'closedExtricate1'
+--
+--   instance 'HasCase' "x" XY   -- Just like usual 'Has' instances.
+--   instance 'HasCase' "y" XY
+--
+--   instance 'Build' XY where
+--     {-\# INLINE 'build' #-}
+--     'build' = 'genericBuild'
+-- @
+module Data.Ruin.ClosedHas (
+  ClosedHas,
+  HasCase(..),
+  closedExtricate1,
+  ) where
+
+import GHC.Generics
+import GHC.TypeLits
+
+import Data.Ruin.All
+import Data.Ruin.Eval
+import Data.Ruin.Internal
+
+-- | Exactly the same as 'Has', but 'ClosedHas' delegates to this copy,
+-- so that 'Has' can delegate parametrically to 'ClosedHas'!
+class HasCase (s :: Symbol) (t :: *) where
+  type FieldTypeCase s t :: *
+  type FieldTypeCase s t = GenericFieldType s t
+
+  extricate1Case :: Label s -> t -> Eval (FieldType s t)
+
+  default extricate1Case :: (Generic t,GBox (IsABox (Rep t)) t,GenericHas (Rep t) s (FieldType s t)) => Label s -> t -> Eval (FieldType s t)
+  {-# INLINE extricate1Case #-}
+  extricate1Case = genericExtricate1
+
+-- | Like @'Has' s t@, but gives a type error if @s@ isn't in
+-- @'Fields' t@.
+type ClosedHas s t = HasIf (Elem s (FieldNames t)) s t
+
+closedExtricate1 :: forall s t. ClosedHas s t => Label s -> t -> Eval (FieldType s t)
+{-# INLINE closedExtricate1 #-}
+closedExtricate1 = \_ -> extricate1If @(Elem s (FieldNames t)) @s
+
+class HasIf (t_has_field_s :: Bool) (s :: Symbol) (t :: *) where
+  extricate1If :: t -> Eval (FieldType s t)
+
+instance TypeError (NoSuchField s t) => HasIf 'False s t where
+  extricate1If = undefined
+
+instance HasCase s t => HasIf 'True s t where
+  {-# INLINE extricate1If #-}
+  extricate1If = extricate1Case (mkLabel @s)
diff --git a/Data/Ruin/Core.hs b/Data/Ruin/Core.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Core.hs
@@ -0,0 +1,84 @@
+{-# Language TemplateHaskell #-}
+
+-- | The core subset of the libary interface. "Data.Ruin" offers more.
+--
+-- The basic idea of this module is that anonymous records are only
+-- used to emulate named function arguments. Thus, this module
+-- provides very little in the way of creating records; it expects
+-- that you'll declare and build your record types as usual.
+--
+-- The most solid use case for this module is a data type for parsing
+-- the command-line.
+--
+-- [Step 1] Define a record type for each command.
+--
+-- [Step 2] Define a sum type where each constructor contains only the
+-- corresponding command record type.
+--
+-- [Step 3] Define a command-line parser for each record type using
+-- 'rtoA'.
+--
+-- [Step 4] Combine those parser using 'rupA'.
+
+module Data.Ruin.Core (
+  -- * Records
+  (:@),
+  dub,
+  undub,
+
+  -- * Accessing parts of records
+  rpat,
+
+  -- * Building records
+  Build,
+  rna,
+  rnaA,
+
+  -- * Pure Combinators
+  (<@),
+  rfrom,
+  rsym,
+  rup,
+
+  -- * 'Applicative' Combinators
+  rtoA,
+  rupA,
+
+  -- * Conveniences
+
+  -- ** Avoid unused selectors
+  NoWarnUnusedTopBind(..),
+
+  -- ** Splice
+  makeRecords,
+  ) where
+
+import Data.Ruin.All
+import Data.Ruin.Internal
+import Data.Ruin.QQ hiding (rna,rnaA)
+import Data.Ruin.QQ.Parser (QQ(..),pQQ)
+import Data.Ruin.TH
+
+import qualified Language.Haskell.TH as TH
+import           Language.Haskell.TH.Quote (QuasiQuoter(..))
+import           Text.Parsec (parse)
+
+-- | 'rna' is like 'rpat', but it also works for expressions. All of
+-- the sugar is supported in the dual way.
+rna :: QuasiQuoter
+rna = QuasiQuoter (pars' expQQ) (pars patQQ) nope nope
+  where
+  nope = fail "The `rna' quasiquoter only creates expressions or patterns."
+
+-- | 'rnaA' is like 'rna', but it only works for expressions and it
+-- only works inside an 'Applicative'.
+rnaA :: QuasiQuoter
+rnaA = QuasiQuoter (pars' expQQA) nope nope nope
+  where
+  nope = fail "The `rnaA' quasiquoter only creates expressions."
+
+pars' :: (QQ -> TH.Q a) -> String -> TH.Q a
+pars' k s = either (fail . show) k' $ parse pQQ "rna quasiquote" s
+  where
+  k' qq@(MkQQ Just{} _) = k qq
+  k' _ = fail "The Data.Ruin.Core quasiquoters require a typename when used as expressions."
diff --git a/Data/Ruin/Deep.hs b/Data/Ruin/Deep.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Deep.hs
@@ -0,0 +1,72 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language ConstraintKinds #-}
+{-# Language DataKinds #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language KindSignatures #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+module Data.Ruin.Deep (
+  -- * Sequences of labels
+  Labels,
+  consLabels,
+  mkLabels,
+  nilLabels,
+
+  -- * Deep projection
+  DeepFieldType,
+  DeepHas,
+  extricate,
+  ) where
+
+import GHC.TypeLits
+
+import Data.Ruin.All
+import Data.Ruin.Eval (Eval)
+import Data.Ruin.Internal
+
+-----
+
+class DeepHas_ (ss :: [Symbol]) (t :: *) where
+  type DeepFieldType_ ss t :: *
+  extricate_ :: Labels ss -> t -> Eval (DeepFieldType_ ss t)
+
+instance DeepHas_ '[] t where
+  type DeepFieldType_ '[] t = t
+  {-# INLINE extricate_ #-}
+  extricate_ = \_ -> pure
+
+instance (Has s t,DeepHas ss (FieldType s t)) => DeepHas_ (s ': ss) t where
+  type DeepFieldType_ (s ': ss) t = DeepFieldType ss (FieldType s t)
+  {-# INLINE extricate_ #-}
+  extricate_ = \_ t -> extricate1 (mkLabel @s) t >>= extricate (mkLabels @ss)
+
+-----
+
+-- | This constraint is an implementation detail of 'extricate'. It's
+-- just an iteration of 'Has'.
+type DeepHas = DeepHas_
+
+-- | This constraint is an implementation detail of 'extricate'. It's
+-- just an iteration of 'FieldType'.
+type DeepFieldType ss t = DeepFieldType_ ss t
+
+-- | 'extricate' project a field out of nested records by iterating
+-- 'extricate1'.
+--
+-- The first argument is a function type so that the syntax can use
+-- @.@ to specify a sequence of labels.
+--
+--
+-- @
+--   'extricate' id = return
+--
+--   'extricate' (\#s . ss) = 'extricate1' \#s Control.Monad.'Control.Monad.>=>' 'extricate' ss
+-- @
+extricate :: forall ss t. DeepHas ss t => Labels ss -> t -> Eval (DeepFieldType ss t)
+{-# INLINE extricate #-}
+extricate = extricate_
diff --git a/Data/Ruin/Eval.hs b/Data/Ruin/Eval.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Eval.hs
@@ -0,0 +1,31 @@
+module Data.Ruin.Eval (
+  Eval(..),
+  runEval,
+  ) where
+
+-- | An evaluation box. It is crucially not a newtype nor strict in
+-- its contents.
+--
+-- This data type is a simplification of
+-- 'Control.Parallel.Strategies.Eval'.
+data Eval a = Done a
+
+runEval :: Eval a -> a
+{-# INLINE runEval #-}
+runEval (Done a) = a
+
+instance Functor Eval where
+  {-# INLINE fmap #-}
+  fmap f (Done a) = Done (f a)
+
+instance Applicative Eval where
+  {-# INLINE pure #-}
+  pure = Done
+  {-# INLINE (<*>) #-}
+  Done f <*> Done a = Done (f a)
+
+instance Monad Eval where
+  {-# INLINE return #-}
+  return = Done
+  {-# INLINE (>>=) #-}
+  Done a >>= k = k a
diff --git a/Data/Ruin/Fieldwise.hs b/Data/Ruin/Fieldwise.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Fieldwise.hs
@@ -0,0 +1,315 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language DataKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}   -- UnifyShape
+
+module Data.Ruin.Fieldwise where
+
+import           Data.Functor.Compose
+import           Data.Functor.Identity
+import           Data.Semigroup (Semigroup,(<>))
+import           GHC.TypeLits (Symbol)
+
+import           Data.Ruin.All
+import           Data.Ruin.Eval
+import           Data.Ruin.Internal
+
+-- | How to create a field @s@ of type @b@ from a value of @a@.
+class FPure a (s :: Symbol) b where
+  fpure :: a -> b
+
+-- | Same as 'rmonopure'.
+instance (b ~ (dom -> cod)) => FPure (dom -> cod) s b where
+  {-# INLINE fpure #-}
+  fpure = id
+
+-- | An implementation detail of 'rpure'.
+newtype RPure a = MkRPure a
+
+-- | Defer to 'FPure'.
+instance (Applicative i,FPure a s b) => Gives s b i (RPure a) where
+  {-# INLINE get #-}
+  get = \(MkRPure a) -> pure $ fpure @a @s a
+
+-- | A record where the value of field @s@ is @'fpure' \@a \@s a@, for
+-- the given @a@.
+--
+-- @
+--   > :t 'Data.Ruin.Hoid.hoid' \@((':@') "x") . 'rpure'
+--   'Data.Ruin.Hoid.hoid' \@((':@') "x") . 'rpure' :: 'FPure' a "x" t => a -> "x" ':@' t
+-- @
+rpure :: (Build t,GivesThese (Fields t) Identity (RPure a)) => a -> t
+{-# INLINE rpure #-}
+rpure = runCEI . build . MkRPure
+
+-----
+
+-- | An implementation detail of 'rmonopure'.
+newtype RMonoPure a = MkRMonoPure a
+
+instance (a ~ b) => FPure (RMonoPure a) s b where
+  {-# INLINE fpure #-}
+  fpure = \(MkRMonoPure a) -> a
+
+-- | A record where every field is a given monomorphic value.
+--
+-- @
+--   > :t 'Data.Ruin.Hoid.hoid' \@((':@') "x") . 'rmonopure'
+--   'Data.Ruin.Hoid.hoid' \@((':@') "x") . 'rmonopure' :: t -> "x" ':@' t
+-- @
+rmonopure :: (Build t,GivesThese (Fields t) Identity (RPure (RMonoPure a))) => a -> t
+{-# INLINE rmonopure #-}
+rmonopure = rpure . MkRMonoPure
+
+-- | Alias for 'rpure', symmetric with 'rmonopure'.
+rpolypure :: (Build t,GivesThese (Fields t) Identity (RPure a)) => a -> t
+{-# INLINE rpolypure #-}
+rpolypure = rpure
+
+-----
+
+-- | An implementation detail of 'rmempty'.
+data RMEmpty = MkRMEmpty
+
+instance Monoid a => FPure RMEmpty s a where
+  {-# INLINE fpure #-}
+  fpure = \_ -> mempty
+
+-- | A record where every field is 'mempty'.
+--
+-- @
+--   > :t 'Data.Ruin.Hoid.hoid' \@((':@') "x") 'rmempty'
+--   'Data.Ruin.Hoid.hoid' \@((':@') "x") 'rmempty' :: Monoid t => "x" ':@' t
+-- @
+rmempty :: (Build t,GivesThese (Fields t) Identity (RPure RMEmpty)) => t
+{-# INLINE rmempty #-}
+rmempty = rpure MkRMEmpty
+
+-- | An implementation detail of 'rmappend'.
+data RMAppend l r = MkRMAppend l r
+
+instance
+     ( Applicative i
+     , a ~ FieldType s l
+     , a ~ FieldType s r
+     , Has s l
+     , Has s r
+     , Monoid a
+     )
+  => Gives s a i (RMAppend l r) where
+  {-# INLINE get #-}
+  get = \(MkRMAppend l r) -> Compose $ (\a b -> pure (mappend a b)) <$> extricate1 s l <*> extricate1 s r
+    where
+    s = mkLabel @s
+
+-- | Combine two records if all of the fields are 'Monoid's.
+--
+-- @
+--   > :t \\l r -> 'Data.Ruin.Hoid.hoid' \@((':@') "x") $ 'rmappend' l r
+--   \\l r -> 'Data.Ruin.Hoid.hoid' \@((':@') "x") $ 'rmappend' l r
+--     :: Monoid t => "x" ':@' t -> "x" ':@' t -> "x" ':@' t
+-- @
+rmappend ::
+     ( Build t
+     , GivesThese (Fields t) Identity (RMAppend t t)
+     )
+  => t -> t -> t
+{-# INLINE rmappend #-}
+rmappend = \l r -> runCEI $ build $ MkRMAppend l r
+
+-- | An implementation detail of 'rmappend'.
+data RSAppend l r = MkRSAppend l r
+
+instance
+     ( Applicative i
+     , a ~ FieldType s l
+     , a ~ FieldType s r
+     , Has s l
+     , Has s r
+     , Semigroup a
+     )
+  => Gives s a i (RSAppend l r) where
+  {-# INLINE get #-}
+  get = \(MkRSAppend l r) -> Compose $ (\a b -> pure (a <> b)) <$> extricate1 s l <*> extricate1 s r
+    where
+    s = mkLabel @s
+
+-- | Combine two records if all of the fields are 'Semigroups's.
+--
+-- @
+--   > :t \\l r -> 'Data.Ruin.Hoid.hoid' \@((':@') "x") $ 'rsappend' l r
+--   \\l r -> 'Data.Ruin.Hoid.hoid' \@((':@') "x") $ 'rsappend' l r
+--     :: Semigroup t => "x" ':@' t -> "x" ':@' t -> "x" ':@' t
+-- @
+rsappend ::
+     ( Build t
+     , GivesThese (Fields t) Identity (RSAppend t t)
+     )
+  => t -> t -> t
+{-# INLINE rsappend #-}
+rsappend = \l r -> runCEI $ build $ MkRSAppend l r
+
+-----
+
+-- | An implementation detail of 'rlabel'.
+data RLabel = MkRLabel
+
+instance (a ~ Label s) => FPure RLabel s a where
+  {-# INLINE fpure #-}
+  fpure = \_ -> mkLabel
+
+-- | The record where the type of field @s@ is @Label s@.
+--
+-- @
+--   > :t 'Data.Ruin.Hoid.hoid' \@((':@') "x") 'rlabel'
+--   'Data.Ruin.Hoid.hoid' \@((':@') "x") 'rlabel' :: "x" ':@' 'Label' "x"
+-- @
+rlabel :: (Build t,GivesThese (Fields t) Identity (RPure RLabel)) => t
+{-# INLINE rlabel #-}
+rlabel = rpure MkRLabel
+
+-----
+
+infixl 4 `rmap`
+
+-- | If the following constraint holds for every field @s@ in @t@,
+-- then @fun@ can map @rc@ to @t@.
+--
+-- @
+--   'FPure' fun s ('FieldType' s rc -> 'FieldType' s t)
+-- @
+--
+-- @
+--   > :t \\fun -> 'rmap' fun . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--   \\fun -> 'rmap' fun . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--     :: 'FPure' fun "x" (t -> t1) => fun -> "x" ':@' t -> "x" ':@' t1
+-- @
+rmap ::
+  forall fun rc rfun t.
+     ( Build rfun
+     , Build t
+     , GivesThese (Fields rfun) Identity (RPure fun)
+     , GivesThese (Fields t) Identity (RSplat rfun rc)
+     , UnifyShape rfun t
+     , UnifyShape rc t
+     )
+  => fun -> rc -> t
+{-# INLINE rmap #-}
+rmap = \fun rc -> (rpure fun :: rfun) `rsplat` rc
+
+-----
+
+infixl 4 `rmapA`
+
+-- | If the following constraint holds for every field @s@ in @t@,
+-- then @fun@ can map @rc@ to @t@ within an 'Applicative' functor @i@.
+--
+-- @
+--   'FPure' fun s ('FieldType' s rc -> i ('FieldType' s t))
+-- @
+--
+-- @
+--   > :t \\fun -> 'rmapA' fun . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--   \\fun -> 'rmapA' fun . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--     :: ('FPure' fun "x" (t -> i t1), Applicative i) =>
+--        fun -> "x" ':@' t -> i ("x" ':@' t1)
+-- @
+rmapA ::
+  forall fun i rc rfun t.
+     ( Applicative i
+     , Build rfun
+     , Build t
+     , GivesThese (Fields rfun) Identity (RPure fun)
+     , GivesThese (Fields t) i (RSplatA rfun rc)
+     , UnifyShape rfun t
+     , UnifyShape rc t
+     )
+  => fun -> rc -> i t
+{-# INLINE rmapA #-}
+rmapA = \fun rc -> (rpure fun :: rfun) `rsplatA` rc
+
+-----
+
+-- | An implementation detail of 'rsplat'.
+data RSplat rfun rc = MkRSplat rfun rc
+
+instance
+     ( Applicative i
+     , FieldType s rfun ~ (FieldType s rc -> b)
+     , Has s rfun
+     , Has s rc
+     )
+  => Gives s b i (RSplat rfun rc) where
+  {-# INLINE get #-}
+  get = \(MkRSplat rfun rc) -> Compose $ fmap @Eval pure $ extricate1 s rfun <*> extricate1 s rc
+    where
+    s = mkLabel @s
+
+infixl 4 `rsplat`
+
+-- | A record where the value of field @s@ is @'Data.Eval.runEval'
+-- ('Data.Ruin.Deep.extricate' \#s rfun \<*>
+-- 'Data.Ruin.Deep.extricate' \#s rc)@.
+--
+-- Compare to \"zippy\" instances of '<*>'.
+--
+-- @
+--   > :t 'rsplat' . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--   'rsplat' . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--     :: "x" ':@' (t1 -> t) -> "x" ':@' t1 -> "x" ':@' t
+-- @
+rsplat ::
+     ( Build t
+     , GivesThese (Fields t) Identity (RSplat rfun rc)
+     , UnifyShape rc t
+     , UnifyShape rfun t
+     )
+  => rfun -> rc -> t
+{-# INLINE rsplat #-}
+rsplat = \rfun rc -> runCEI $ build $ MkRSplat rfun rc
+
+-----
+
+-- | An implementation detail of 'rsplatA'.
+data RSplatA rfun rc = MkRSplatA rfun rc
+
+instance
+     ( Applicative i
+     , FieldType s rfun ~ (FieldType s rc -> i b)
+     , Has s rfun
+     , Has s rc
+     )
+  => Gives s b i (RSplatA rfun rc) where
+  {-# INLINE get #-}
+  get = \(MkRSplatA rfun rc) -> Compose $ extricate1 s rfun <*> extricate1 s rc
+    where
+    s = mkLabel @s
+
+infixl 4 `rsplatA`
+
+-- | Like 'rsplat', but in an 'Applicative' functor. Note that every
+-- field in @rfun@ must be a function with an @i@-structured codomain.
+--
+-- @
+--   > :t 'rsplatA' . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--   'rsplatA' . 'Data.Ruin.Hoid.hoid' \@((':@') "x")
+--     Applicative i => :: "x" ':@' (t1 -> i t) -> "x" ':@' t1 -> i ("x" ':@' t)
+-- @
+rsplatA ::
+     ( Applicative i
+     , Build t
+     , GivesThese (Fields t) i (RSplatA rfun rc)
+     , UnifyShape rc t
+     , UnifyShape rfun t
+     )
+  => rfun -> rc -> i t
+{-# INLINE rsplatA #-}
+rsplatA = \rfun rc -> runEval $ getCompose $ build $ MkRSplatA rfun rc
diff --git a/Data/Ruin/Hide.hs b/Data/Ruin/Hide.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Hide.hs
@@ -0,0 +1,88 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language DataKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language KindSignatures #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+{-# OPTIONS_HADDOCK hide,not-home #-}
+
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}   -- rdrop
+
+-- | Hiding fields.
+
+module Data.Ruin.Hide (
+  Hide,
+  hide,
+  rdrop,
+  rtake,
+  ) where
+
+import GHC.TypeLits
+
+import Data.Ruin.All
+import Data.Ruin.Eval
+import Data.Ruin.Internal
+import Data.Ruin.R
+
+-- | Deny the @'Has'@ instance for each of @ss@.
+newtype Hide (ss :: [Symbol]) rc = MkHide rc
+
+-- | Deny (\"forget\") a @'Has' s@ instance.
+hide :: Labels ss -> rc -> Hide ss rc
+hide _ = MkHide
+
+instance Has_Hide (Elem s sHiddens) s rc => Has s (Hide sHiddens rc) where
+  type FieldType s (Hide sHiddens rc) = FieldType s rc
+  {-# INLINE extricate1 #-}
+  extricate1 = extricate1_Hide @(Elem s sHiddens)
+
+class Has_Hide (eq :: Bool) (s :: Symbol) (rc :: *) where
+  extricate1_Hide :: Label s -> Hide sHiddens rc -> Eval (FieldType s rc)
+
+instance TypeError (FieldIsHidden s rc) => Has_Hide 'True s rc where
+  extricate1_Hide = undefined
+
+instance Has s rc => Has_Hide 'False s rc where
+  {-# INLINE extricate1_Hide #-}
+  extricate1_Hide = \s (MkHide rc) -> extricate1 s rc
+
+-----
+
+type FieldIsHidden (s :: Symbol) (top :: *) =
+             'Text "ruin: The field `"
+       ':<>: 'Text s
+       ':<>: 'Text "' is hidden in the type"
+  ':$$: Render top
+
+-----
+
+-- | Create an anonymous record that contains the fields of @t@ that
+-- are not named in @fs@.
+rdrop ::
+     ( rc ~ Rcrd (DifferenceByFst (Fields t) fs)
+     , Build rc
+     , t `IsSubtypeOf` rc
+     )
+  => Labels fs
+  -> t
+  -> rc
+{-# INLINE rdrop #-}
+rdrop = \_ -> rup
+
+-- | Split a record into two separate types, where the second type is
+-- an anonymous record defined as the leftovers from the first type.
+rtake ::
+     ( leftovers ~ Rcrd (DifferenceByFst (Fields t) (FieldNames taken))
+     , Build (taken,leftovers)
+     , t `IsSymmetricRecordOf` (taken,leftovers)
+     )
+  => t
+  -> (taken,leftovers)
+{-# INLINE rtake #-}
+rtake = rsym
diff --git a/Data/Ruin/Hoid.hs b/Data/Ruin/Hoid.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Hoid.hs
@@ -0,0 +1,56 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language ExplicitForAll #-}
+{-# Language MagicHash #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeInType #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+{-# OPTIONS_HADDOCK hide,not-home #-}
+
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
+module Data.Ruin.Hoid (
+  Hoid,
+  hoid,
+  hoidProxy,
+  phoid,
+  ) where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import GHC.Exts (type (~~),Any,Constraint,Proxy#)
+
+-- | A family of identity functions indexed by possibly higher-order
+-- types. @'hoid' \@t@ asserts that @a@ is either equal to @t@ or is
+-- an application of @t@.
+--
+-- The 'Hoid' type family vanishes if the kind of @t@ is defined
+-- enough to fully determine the arity of @t@. If 'Hoid' doesn't
+-- vanish in a use case, then 'hoid' is not intended for use in that
+-- case.
+hoid :: forall t a. Hoid t a => a -> a
+hoid = id
+
+-- | 'hoid' but with a proxy argument.
+phoid :: forall t a. Hoid t a => Proxy# t -> a -> a
+phoid _ = hoid @t
+
+-- | @'hoidProxy \@t' = 'hoid' \@t <$> Proxy@
+hoidProxy :: forall t a. Hoid t a => Proxy a
+hoidProxy = Proxy
+
+-- | Do not reuse; consider this an implementation detail of 'hoid'.
+type family Hoid (t :: k) (a :: k2) :: Constraint where
+  Hoid (t :: _ -> cod) a = Hoid (t (Lookup t cod a)) a
+  Hoid t a = (t ~~ a)
+
+-----
+
+-- | Because of the final case, the user never sees the 'Lookup' type.
+type family Lookup (t :: dom -> k1) (cod :: Type) (a :: k2) :: dom where
+  Lookup t (_ -> cod) (f x) = Lookup t cod f
+  Lookup _ _ (f x) = x
+  Lookup _ _ _ = Any   -- This branch is only involved in type errors.
diff --git a/Data/Ruin/Internal.hs b/Data/Ruin/Internal.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/Internal.hs
@@ -0,0 +1,172 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language DataKinds #-}
+{-# Language DeriveFunctor #-}
+{-# Language ExplicitForAll #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language PolyKinds #-}
+{-# Language Rank2Types #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+{-# OPTIONS_HADDOCK hide,not-home #-}
+
+module Data.Ruin.Internal (module Data.Ruin.Internal) where
+
+import Data.Functor.Compose
+import Data.Functor.Identity
+import Data.Proxy (Proxy(..))
+import Data.Type.Bool (If)
+import GHC.OverloadedLabels
+import GHC.TypeLits
+
+import Data.Ruin.Eval
+import Data.Ruin.Hoid (Hoid)
+
+runCEI :: Compose Eval Identity a -> a
+runCEI = runIdentity . runEval . getCompose
+
+-----
+
+-- | @'proxyOf' = const Proxy@
+proxyOf :: a -> Proxy a
+proxyOf = const Proxy
+
+-----
+
+-- | Use @-XOverloadedLabels@ to create labels. For example, @#x ::
+-- Label "x"@.
+--
+-- Or use 'mkLabel'.
+data Label (s :: Symbol) = MkLabel
+
+-- | Creates a label that is determined either by type inference or
+-- via @-XTypeApplications@.
+mkLabel :: forall s. Label s
+mkLabel = MkLabel
+
+instance (s1 ~ s2) => IsLabel s1 (Label s2) where fromLabel _ = MkLabel
+
+-----
+
+-- | This type is an instance of a type-level difference list, so that
+-- sequences of labels can be written as @\#x . \#y . \#z :: 'Labels'
+-- '["x","y","z"]@, for example.
+type Labels fs = Labels_ '[] -> Labels_ fs
+
+data Labels_ (s :: [Symbol]) = MkLabels_
+
+consLabels :: forall s ss. Labels_ ss -> Labels_ (s ': ss)
+consLabels _ = MkLabels_
+
+mkLabels :: forall fs. Labels fs
+mkLabels _ = MkLabels_
+
+nilLabels :: Labels_ '[]
+nilLabels = MkLabels_
+
+-- | This is essentialy an instance for 'Labels'.
+instance (cod ~ Labels_ (s ': ss)) => IsLabel s (Labels_ ss -> cod) where fromLabel = \_ -> consLabels
+
+-----
+
+type family Difference (xs :: [k]) (ys :: [k]) :: [k] where
+  Difference '[] ys = '[]
+  Difference (x ': xs) ys =
+    If (Elem x ys)
+      (Difference xs ys)
+      (x ': Difference xs ys)
+
+type family Intersection (xs :: [k]) (ys :: [k]) :: [k] where
+  Intersection '[] ys = '[]
+  Intersection (x ': xs) ys =
+    If (Elem x ys)
+      (x ': Intersection xs ys)
+      (Intersection xs ys)
+
+type family Elem (t :: k) (ts :: [k]) :: Bool where
+  Elem t '[] = 'False
+  Elem t (t ': ts) = 'True
+  Elem t (t2 ': ts) = Elem t ts
+
+type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
+  '[] ++ ys = ys
+  (x ': xs) ++ ys = x ': xs ++ ys
+
+type family MapFst (ps :: [(a,b)]) :: [a] where
+  MapFst '[] = '[]
+  MapFst ( '(a,b) ': ps ) = a ': MapFst ps
+
+type family MapSecondConst (c :: b) (ps :: [(a,b)]) :: [(a,b)] where
+  MapSecondConst _ '[] = '[]
+  MapSecondConst c ( '(a,_) ': ps ) = '(a,c) ': MapSecondConst c ps
+
+type family Head (xs :: [a]) :: a where Head (a ': _) = a
+type family Tail (xs :: [a]) :: [a] where Tail (_ ': as) = as
+
+type family Fst (p :: (a,b)) :: a where Fst '(a,_) = a
+type family Snd (p :: (a,b)) :: b where Snd '(_,b) = b
+
+type family HalfLength (x :: [a]) :: Nat where
+  HalfLength (_ ': _ ': xs) = 1 + HalfLength xs
+  HalfLength _ = 0
+
+type family Take (n :: Nat) (xs :: [a]) :: [a] where
+  Take 0 _ = '[]
+  Take n (x ': xs) = x ': Take (n-1) xs
+
+type family Drop (n :: Nat) (xs :: [a]) :: [a] where
+  Drop 0 xs = xs
+  Drop n (_ ': xs) = Drop (n-1) xs
+
+type FirstHalf xs = Take (HalfLength xs) xs
+type SecondHalf xs = Drop (HalfLength xs) xs
+
+type family DifferenceByFst (xs :: [(k,v)]) (ys :: [k]) :: [(k,v)] where
+  DifferenceByFst '[] ys = '[]
+  DifferenceByFst (x ': xs) ys =
+    If (Elem (Fst x) ys)
+      (DifferenceByFst xs ys)
+      (x ': DifferenceByFst xs ys)
+
+-----
+
+-- | Merely a receptacle in which the user can syntactially use a
+-- record selector to avoid the @-Wunused-top-bind@ warning without
+-- having to export the record selector.
+--
+-- @
+--   {-\# OPTIONS_GHC -Werror -Wall #-}
+--
+--   module Foo (Bar(MkBar)) where
+--
+--   data Bar = MkBar {x,y :: Int}
+--
+--   instance 'NoWarnUnusedTopBind' Bar where 'noWarnUnusedTopBind' MkBar{x=_,y=_} = ()
+--   instance 'Data.Ruin.Has' "x" Bar
+--   instance 'Data.Ruin.Has' "y" Bar
+--   instance 'Data.Ruin.Build' Bar where
+--     {-\# INLINE 'Data.Ruin.rupEval' #-}
+--     'Data.Ruin.rupEval' = 'Data.Ruin.genericRupEval'
+-- @
+--
+-- @x@ and @y@ in that example are neither exported nor really used,
+-- but there will be no warnings.
+--
+-- An explicit instance of 'Control.DeepSeq.NFData', for example, will
+-- often use a similar record pattern that serves to use the
+-- selectors. On the other hand, most such instances are now quite
+-- conveient to implicitly derive, so this 'NoWarnUnusedTopBind' class
+-- may be the most obvious way to inconsequentially \"use\" a record
+-- selector so as to avoid the @-Wunused-top-bind@ warning.
+class NoWarnUnusedTopBind t where
+  noWarnUnusedTopBind :: Hoid t a => a -> ()
+
+-----
+
+-- | This is a \"tuple of one component\", so that it can have a data
+-- constructor like all the other tuples.
+--
+-- It is crucially not a newtype!
+data Tup1 a = MkTup1 a deriving Show
diff --git a/Data/Ruin/QQ.hs b/Data/Ruin/QQ.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/QQ.hs
@@ -0,0 +1,187 @@
+{-# Language ApplicativeDo #-}
+{-# Language LambdaCase #-}
+{-# Language MagicHash #-}
+{-# Language TemplateHaskell #-}
+{-# Language ViewPatterns #-}
+
+{-# OPTIONS_HADDOCK hide,not-home #-}
+
+module Data.Ruin.QQ (
+  expQQ,
+  expQQA,
+  pars,
+  patQQ,
+  rna,
+  rnaA,
+  rpat,
+  ) where
+
+import           Data.Maybe (catMaybes)
+import           GHC.Prim (Proxy#,proxy#)
+import qualified Language.Haskell.TH as TH
+import           Language.Haskell.TH.Quote (QuasiQuoter(..))
+import           Text.Parsec (parse)
+
+import Data.Ruin.All
+import Data.Ruin.Hoid
+import Data.Ruin.Internal
+import Data.Ruin.QQ.Parser
+
+pars :: (QQ -> TH.Q a) -> String -> TH.Q a
+pars k s = either (fail . show) k $ parse pQQ "rna quasiquote" s
+
+expQQ :: QQ -> TH.ExpQ
+expQQ (MkQQ typename binders) = case typename of
+  Nothing -> e
+  Just s -> [e| prto (proxy# :: Proxy# $(TH.conT (TH.mkName s))) $e |]
+  where
+  e = foldr TH.appE val (catMaybes seqs)
+  (seqs,vals) = unzip $ map mk binders
+  val = tupE vals
+
+  mk (strictness,var,field) =
+    ( if strictness then Just [e| seq $v |] else Nothing
+    , [e| dub (mkLabel :: Label $(TH.litT (TH.strTyLit field))) $v |]
+    )
+    where
+    v = TH.varE (TH.mkName var)
+
+expQQA :: QQ -> TH.ExpQ
+expQQA (MkQQ typename binders) =
+  foldl app [e| pure $fun |] binders
+  where
+  app f (_,var,_) = [e| $f <*> $(TH.varE (TH.mkName var)) |]
+
+  fun = do
+    (seqs,pats,vals) <- unzip3 <$> mapM mk binders
+    let e = tupE vals
+    let result = case typename of
+          Nothing -> e
+          Just s -> [e| prto (proxy# :: Proxy# $(TH.conT (TH.mkName s))) $e |]
+    TH.lamE pats $ foldr TH.appE result (catMaybes seqs)
+
+  mk (strictness,var,field) = do
+    n <- TH.newName (if "_" == var then "x" else var)
+    let v = TH.varE n
+    return (
+        if strictness then Just [e| seq $v |] else Nothing
+      ,
+        TH.varP n
+      ,
+        [e| dub (mkLabel :: Label $(TH.litT (TH.strTyLit field))) $v |]
+      )
+
+patQQ :: QQ -> TH.PatQ
+patQQ (MkQQ typename binders) = case typename of
+  Nothing -> tp
+  Just s -> [p| (rup . phoid (proxy# :: Proxy# $(TH.conT (TH.mkName s))) -> $tp) |]
+  where
+  tp = tupP $ map mk binders
+
+  mk (strictness,var,field) = bang p
+    where
+    bang = if strictness then TH.bangP else id
+    p = [p| (undub (mkLabel :: Label $(TH.litT (TH.strTyLit field))) -> $v) |]
+    v = if "_" == var then TH.wildP else TH.varP (TH.mkName var)
+
+tupE :: [TH.ExpQ] -> TH.ExpQ
+tupE [e] = [e| MkTup1 $e |]
+tupE es = TH.tupE es
+
+tupP :: [TH.PatQ] -> TH.PatQ
+tupP [p] = [p| MkTup1 $p |]
+tupP ps = TH.tupP ps
+
+-----
+
+-- | Named arguments for functions.
+--
+-- @
+--   (\\['rna'|x] -> x) :: 'Tup1' ("x" ':@' a) -> a
+--
+--   (\\['rna'|x y] -> (x,y)) :: ("x" ':@' a,"y" ':@' b) -> (a,b)
+--
+--   (\\['rna'|y x] -> (x,y)) :: ("y" ':@' b,"x" ':@' a) -> (a,b)
+-- @
+--
+-- And so on. The 'Has' and 'Build' classes support such tuples up to
+-- 8 components.
+--
+-- There are four pieces of special syntax, none of which can be
+-- escaped.
+--
+-- * A @\@@ allows a different variable name than the field name.
+--
+--     @
+--       (\\f ['rna'|l\@x|] ['rna'|r\@x|] -> f l r)
+--         :: (a -> b -> c) -> 'Tup1' ("x" ':@' a) -> 'Tup1' ("x" ':@' b) -> c
+--     @
+--
+-- * A name of @_@ is a wildcard pattern.
+--
+-- * A leading word of the form @(\<prefix>...\<suffix>)@ adds a
+-- prefix and/or suffix to all of the variable names. This affects
+-- even the names given with @\@@ syntax. It does not affect
+-- wildcards.
+--
+--     @
+--       (\\['rna'|(...L) x y|] ['rna'|(r_...') x y|] -> xL == r_x' && yL == r_y')
+--         :: (Eq a,Eq b) => ("x" ':@' a,"y" ':@' b) -> ("x" ':@' a,"y" ':@' b) -> Bool
+--     @
+--
+-- * A @!@ at the beginning of the pattern makes it strict.
+--
+--     @
+--       -- strict
+--       (\\['rna'|!x|] -> Just x) :: 'Tup1' ("x" ':@' a) -> Maybe a
+--
+--       -- strict
+--       (\\['rna'|!x\@foo|] -> Just x) :: 'Tup1' ("foo" ':@' a) -> Maybe a
+--
+--       -- strict
+--       (\\['rna'|!x\@!|] -> Just x) :: 'Tup1' ("!" ':@' a) -> Maybe a
+--
+--       -- not strict
+--       (\\['rna'|x\@!|] -> Just x) :: 'Tup1' ("!" ':@' a) -> Maybe a
+--     @
+--
+--     Note a @~@ pattern for binding would be redundant, since the
+--     bindings are ultimately variable bindings. Though it may be
+--     useful to apply a tilde pattern to the entire quasiquote.
+--
+-- * A leading word that is capitalized is interpreted as the name of
+-- a record type and is ascribed via 'rfrom'.
+--
+--    @
+--      data XY x y = MkXY {x :: x,y :: y}
+--
+--      (\\['rna'| XY x y|] -> (x,y)) :: XY t t1 -> (t, t1)
+--    @
+--
+--    When both are present, the type name must precede the prefix
+--    and/or suffix.
+--
+-- 'rna' also works as an expression. All of the sugar except
+-- wildcards is supported in the dual way.
+rna :: QuasiQuoter
+rna = QuasiQuoter (pars expQQ) (pars patQQ) nope nope
+  where
+  nope = fail "The `rna' quasiquoter only creates expressions or patterns."
+
+-- | 'rnaA' is like 'rna', but:
+--
+-- * it only works for expressions,
+--
+-- * it only works inside an 'Applicative'.
+rnaA :: QuasiQuoter
+rnaA = QuasiQuoter (pars expQQA) nope nope nope
+  where
+  nope = fail "The `rnaA' quasiquoter only creates expressions."
+
+-----
+
+-- | 'rpat' is like 'rna', but it only works for patterns.
+rpat :: QuasiQuoter
+rpat = QuasiQuoter nope (pars patQQ) nope nope
+  where
+  nope = fail "The `rpat' quasiquoter only creates patterns."
diff --git a/Data/Ruin/QQ/Parser.hs b/Data/Ruin/QQ/Parser.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/QQ/Parser.hs
@@ -0,0 +1,80 @@
+module Data.Ruin.QQ.Parser (
+  QQ(..),
+  pQQ,
+  ) where
+
+import           Data.Char (isSpace)
+import           Data.Functor (void)
+import           Data.Maybe (fromMaybe)
+
+import           Text.Parsec
+import           Text.Parsec.String (Parser)
+
+data QQ = MkQQ
+  (Maybe String)
+  [(Bool,String,String)]
+  deriving Show
+
+pQQ :: Parser QQ
+pQQ = do
+  optional gap
+  typename <- optionMaybe (pTypename <* gap)
+  affixes <- optionMaybe (pAffixes <* gap)
+  case affixes of
+    Just (Nothing,Nothing) -> fail "Refusing a degenerate affix specification: remove (...)."
+    _ -> return ()
+  binders <- go
+  eof
+  pure (MkQQ typename (map (interpretAffixes affixes) binders))
+
+  where
+
+  go = ((:) <$> pBinder <*> go1) <|> pure []
+  go1 = (gap *> go) <|> pure []
+
+interpretAffixes ::
+     Maybe (Maybe String,Maybe String)
+  -> (b,Maybe String,String) -> (b,String,String)
+interpretAffixes x (b,mvar,field) = (b,var,field)
+  where
+  var = case fromMaybe field mvar of
+    "_" -> "_"   -- do not apply affixes to _
+    o -> maybe id affix x o
+
+  affix (pre,suf) = maybe id (++) pre . maybe id (flip (++)) suf
+
+gap :: Parser ()
+gap = void $ many1 $ satisfy isSpace
+
+rest :: Parser Char
+rest = char '_' <|> char '\'' <|> alphaNum
+
+pTypename :: Parser String
+pTypename = (:) <$> upper <*> many rest <?> "type name"
+
+pAffixes :: Parser (Maybe String,Maybe String)
+pAffixes =
+    (<?> "affix spec")
+  $ between (char '(') (char ')')
+  $ (,) <$> optionMaybe pPrefix <* ellipsis <*> optionMaybe pSuffix
+
+ellipsis :: Parser ()
+ellipsis = () <$ string "..."
+
+pPrefix :: Parser String
+pPrefix = pVar
+
+pSuffix :: Parser String
+pSuffix = many1 $ char '_' <|> char '\'' <|> alphaNum
+
+pBinder :: Parser (Bool,Maybe String,String)
+pBinder = try (char '!' *> pAt True) <|> pAt False <?> "binder"
+
+pAt :: Bool -> Parser (Bool,Maybe String,String)
+pAt b = (,,) b <$> optionMaybe (try (pVar <* char '@')) <*> pField
+
+pVar :: Parser String
+pVar = (:) <$> (char '_' <|> lower) <*> many rest <?> "Haskell variable name"
+
+pField :: Parser String
+pField = (many1 $ satisfy $ not . isSpace) <?> "field name"
diff --git a/Data/Ruin/R.hs b/Data/Ruin/R.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/R.hs
@@ -0,0 +1,830 @@
+{-# Language AllowAmbiguousTypes #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language RoleAnnotations #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeInType #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+{-# Language UndecidableSuperClasses #-}
+
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
+-- | Anonymous records.
+
+module Data.Ruin.R (
+  -- * Data kind for fields declarations
+  FD,   -- opaque
+
+  -- ** Constructors
+  type (:::),
+  InsertFD,
+  NilFD,
+  MkFD,
+  PlusFD,
+
+  -- ** Operations
+  DeleteFD,
+  LookupFD,
+  LMergeFD,
+  HomogenizeFD,
+
+  -- ** Constraints
+  FDAbsent,
+  FDFoldable,
+  FDFoldable2,
+  FDHomogenous,
+  FDPure,
+  FDSplat,
+  FDSplatA,
+  fdIdentities,
+
+  -- * Anonymous records
+  R,   -- opaque
+  Rcrd,
+
+  -- ** Constructors
+  nilR,
+  oneR,
+  plusR,
+
+  -- ** Operations
+  addR,
+  adjustR,
+  deleteR,
+  extricate1R,
+  getR,
+  insertR,
+  lensR,
+  lmergeR,
+  setR,
+
+  -- ** Fieldwise operations
+  --
+  -- These only compose well if the field names of the involved
+  -- records are known. Otherwise the "Show/Read" Problem makes things
+  -- quite awkward.
+  FPure(..),
+  RCompare(..),
+  REq(..),
+  RShowField(..),
+  rfoldR,
+  rfoldMapR,
+  rfoldMap2R,
+  rlabelR,
+  rmapR,
+  rmapAR,
+  rmappendR,
+  rmemptyR,
+  rpureR,
+  rpolypureR,
+  rsappendR,
+  rsplatR,
+  rsplatAR,
+
+  -- ** Monomorphic specializations
+  monoadjustR,
+  lens'R,
+  rmonopureR,
+
+  -- * Field labels
+  Label,
+  mkLabel,
+  ) where
+
+import           Data.Functor.Compose (Compose(..))
+import           Data.Functor.Identity (Identity(..))
+import qualified Data.HashMap.Lazy as HML
+import           Data.Kind (type (*))
+import           Data.Monoid (All(..))
+import           Data.Semigroup (Semigroup,(<>))
+import           Data.Type.Equality
+import           GHC.Exts (Any,Constraint)
+import qualified GHC.Generics as G
+import           GHC.TypeLits hiding (type (*))
+import qualified Language.Haskell.TH as TH
+import           Language.Haskell.TH.Syntax (Lift(lift))
+import           Unsafe.Coerce (unsafeCoerce)
+
+import           Data.Ruin.All
+import           Data.Ruin.ClosedHas
+import           Data.Ruin.Eval
+import           Data.Ruin.Hoid (Hoid)
+import           Data.Ruin.Internal
+import           Data.Ruin.Fieldwise
+
+-- | An abstract data kind for the field declarations that determine
+-- an anonymous record type. The user can only build this type using
+-- the handful of type families exported by this module.
+--
+-- These families ensure that GHC's type equality relation @~@ ignores
+-- the order in which fields with different names are added to/removed
+-- from the declarations.
+newtype FD =
+  MkFD [(Symbol,*)]
+  -- ^ INVARIANT: strictly ascending by 'Symbol'
+
+type family NilFD :: FD where NilFD = 'MkFD '[]
+
+infix 0 :::
+-- | A field declaration.
+type s ::: ty = ( '(s,ty) :: (Symbol,*) )
+
+-- | Create a fields declaration from a list of individual field
+-- declarations. For example,@'MkFD' '["x" ::: Bool,"y" ::: Maybe
+-- Int]) :: 'FD'@.
+type family MkFD (ds :: [(Symbol,*)]) :: FD where
+  MkFD '[] = NilFD
+  MkFD (d ': ds) = InsertFD (Fst d) (Snd d) (MkFD ds)
+
+-----
+
+type family InsertFD (s :: Symbol) (ty :: *) (fd :: FD) :: FD where
+  InsertFD s ty ('MkFD ds) = 'MkFD (Insert1 s ty ds)
+
+type family Insert1
+  (s :: Symbol)
+  (ty :: *)
+  (ds :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  Insert1 s ty '[] = '[ '(s,ty) ]
+  Insert1 s ty (d ': ds) = Insert2 s ty (CmpSymbol s (Fst d)) d ds
+
+type family Insert2
+  (s :: Symbol)
+  (ty :: *)
+  (ord :: Ordering)
+  (d :: (Symbol,*))
+  (ds :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  Insert2 s ty 'LT d ds = '(s,ty) ': d ': ds
+  Insert2 s ty 'EQ d ds = '(s,ty) ': ds
+  Insert2 s ty 'GT d ds = d ': Insert1 s ty ds
+
+-----
+
+type family DeleteFD (s :: Symbol) (fd :: FD) :: FD where
+  DeleteFD s ('MkFD ds) = 'MkFD (Delete1 s ds)
+
+type family Delete1
+  (s :: Symbol)
+  (ds :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  Delete1 s '[] = '[]
+  Delete1 s (d ': ds) = Delete2 s (CmpSymbol s (Fst d)) d ds
+
+type family Delete2
+  (s :: Symbol)
+  (ord :: Ordering)
+  (d :: (Symbol,*))
+  (ds :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  Delete2 s 'LT d ds = d ': ds
+  Delete2 s 'EQ d ds = ds
+  Delete2 s 'GT d ds = d ': Delete1 s ds
+
+-----
+
+type family LookupFD (s :: Symbol) (fd :: FD) :: * where
+  LookupFD s ('MkFD ds) = FinalLookup s ('MkFD ds) (Lookup1 s ds)
+
+type family FinalLookup (s :: Symbol) (fd :: FD) (mty :: Maybe *) :: * where
+  FinalLookup s fd 'Nothing = TypeError
+    ('Text "Could not find `" ':<>: 'Text s ':<>: 'Text "' in " ':<>: 'ShowType fd)
+  FinalLookup _ _ ('Just ty) = ty
+
+type family Lookup1
+  (s :: Symbol)
+  (ds :: [(Symbol,*)])
+  :: Maybe * where
+  Lookup1 s '[] = 'Nothing
+  Lookup1 s (d ': ds) = Lookup2 s (CmpSymbol s (Fst d)) (Snd d) ds
+
+type family Lookup2
+  (s :: Symbol)
+  (ord :: Ordering)
+  (ty :: *)
+  (ds :: [(Symbol,*)])
+  :: Maybe * where
+  Lookup2 s 'LT _ _ = 'Nothing
+  Lookup2 s 'EQ ty _ = 'Just ty
+  Lookup2 s 'GT _ ds = Lookup1 s ds
+
+-----
+
+-- | A left-biased version of 'PlusFD'; instead of undefined types,
+-- shared fields will keep their type from the left declarations.
+type family LMergeFD (fd1 :: FD) (fd2 :: FD) :: FD where
+  LMergeFD ('MkFD ds1) ('MkFD ds2) = 'MkFD (LMerge1 ds1 ds2)
+
+type family LMerge1
+  (ds1 :: [(Symbol,*)])
+  (ds2 :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  LMerge1 '[] ds2 = ds2
+  LMerge1 ds1 '[] = ds1
+  LMerge1 (d1 ': ds1) (d2 ': ds2) = LMerge2 (CmpSymbol (Fst d1) (Fst d2)) d1 ds1 d2 ds2
+
+type family LMerge2
+  (ord :: Ordering)
+  (d1 :: (Symbol,*))
+  (ds1 :: [(Symbol,*)])
+  (d2 :: (Symbol,*))
+  (ds2 :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  LMerge2 'LT d1 ds1 d2 ds2 = d1 ': LMerge1 ds1 (d2 ': ds2)
+  LMerge2 'EQ d1 ds1 _  ds2 = d1 ': LMerge1 ds1 ds2
+  LMerge2 'GT d1 ds1 d2 ds2 = d2 ': LMerge1 (d1 ': ds1) ds2
+
+-----
+
+-- | Each field that is in both declaration lists will have an undefined type.
+--
+-- @
+--   *Data.Ruin.R> :t 'oneR' \#x () \``plusR`\` ('oneR' \#x () \``plusR`\` 'oneR' \#y ())
+--   'oneR' \#x () \``plusR`\` ('oneR' \#x () \``plusR`\` 'oneR' \#y ())
+--     :: 'R' ('MkFD '[ '("x", ('TypeError' ...)), '("y", ())) ])
+-- @
+type family PlusFD (fd1 :: FD) (fd2 :: FD) :: FD where
+  PlusFD ('MkFD ds1) ('MkFD ds2) = 'MkFD (Plus1 ('MkFD ds1) ('MkFD ds2) ds1 ds2)
+
+type family Plus1
+  (fd1 :: FD)
+  (fd2 :: FD)
+  (ds1 :: [(Symbol,*)])
+  (ds2 :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  Plus1 _ _ '[] ds2 = ds2
+  Plus1 _ _ ds1 '[] = ds1
+  Plus1 fd1 fd2 (d1 ': ds1) (d2 ': ds2) = Plus2 fd1 fd2 (CmpSymbol (Fst d1) (Fst d2)) d1 ds1 d2 ds2
+
+type family Plus2
+  (fd1 :: FD)
+  (fd2 :: FD)
+  (ord :: Ordering)
+  (d1 :: (Symbol,*))
+  (ds1 :: [(Symbol,*)])
+  (d2 :: (Symbol,*))
+  (ds2 :: [(Symbol,*)])
+  :: [(Symbol,*)] where
+  Plus2 fd1 fd2 'LT d1 ds1 d2 ds2 = d1 ': Plus1 fd1 fd2 ds1 (d2 ': ds2)
+  Plus2 fd1 fd2 'EQ d1 ds1 _ ds2 =
+    '(Fst d1,TypeError (PlusMsg fd1 fd2 (Fst d1))) ': Plus1 fd1 fd2 ds1 ds2
+  Plus2 fd1 fd2 'GT d1 ds1 d2 ds2 = d2 ': Plus1 fd1 fd2 (d1 ': ds1) ds2
+
+type PlusMsg fd1 fd2 s =
+  'Text "Field `" ':<>: 'Text s ':<>: 'Text "' occurs in both field declaration lists" ':$$: 'Text "    " ':<>: 'ShowType (FieldsFD fd1) ':$$: 'Text "  and" ':$$: 'Text "    " ':<>: 'ShowType (FieldsFD fd2)
+
+-----
+
+type family FDAbsent (s :: Symbol) (fd :: FD) :: Constraint where
+  FDAbsent s ('MkFD ds) = FDAbsent1 s ('MkFD ds) (Lookup1 s ds)
+
+type family FDAbsent1 (s :: Symbol) (fd :: FD) (mty :: Maybe *) :: Constraint where
+  FDAbsent1 _ _ 'Nothing = ()
+  FDAbsent1 s fd ('Just _) = TypeError
+    ('Text "`" ':<>: 'Text s ':<>: 'Text "' is already a field in " ':<>: 'ShowType fd)
+
+-----
+
+-- | This type equality provides a "proof by fiat" of some obvious
+-- identities involving the fields declarations combinators.
+--
+-- You typically won't need to use this.
+fdIdentities :: forall s fd a.
+     '(
+        LookupFD s (InsertFD s a fd)
+      ,
+        InsertFD s (LookupFD s fd) fd
+      ,
+        DeleteFD s (DeleteFD s fd)
+      ,
+        InsertFD s a (DeleteFD s fd)
+      ,
+        Lookup1 s (FieldsFD (DeleteFD s fd))
+      ,
+        'MkFD (FirstHalf (FieldsFD fd)) `PlusFD` 'MkFD (SecondHalf (FieldsFD fd))
+      )
+  :~:
+    '(
+       a
+     ,
+       fd
+     ,
+       DeleteFD s fd
+     ,
+       InsertFD s a fd
+     ,
+       'Nothing
+     ,
+       fd
+     )
+{-# INLINE fdIdentities #-}
+fdIdentities = unsafeCoerce (Refl :: () :~: ())
+
+-----
+
+-- | Every field in @fd@ has the same type, @a@.
+type family FDHomogenous (a :: *) (fd :: FD) :: Constraint where
+  FDHomogenous a fd = (FDHomogenous1 a (FieldsFD fd),Hoid 'MkFD fd)
+
+type family FDHomogenous1 (a :: *) (ds :: [(Symbol,*)]) :: Constraint where
+  FDHomogenous1 _ '[] = ()
+  FDHomogenous1 a (d ': ds) = (Snd d ~ a,FDHomogenous1 a ds)
+
+-----
+
+-- | A convenient alias.
+type Rcrd ds = R (MkFD ds)
+
+-- | A record with fields declarations @fd :: 'FD'@ is a product type
+-- with one factor per declared field.
+type role R nominal
+newtype R (fd :: FD) =
+  MkR (HML.HashMap String Any)
+  -- ^ INVARIANT: the keys in the map are exactly the fields declared in @fd@.
+
+type family RFD (r :: *) :: FD where RFD (R fd) = fd
+
+nilR :: R NilFD
+{-# INLINE nilR #-}
+nilR = MkR HML.empty
+
+oneR :: KnownSymbol s => Label s -> a -> R (InsertFD s a NilFD)
+{-# INLINE oneR #-}
+oneR lbl x = MkR $ HML.singleton (symbolVal lbl) (unsafeCoerce x)
+
+-- | Each field that is in both records will have an undefined type.
+plusR :: R fd1 -> R fd2 -> R (PlusFD fd1 fd2)
+{-# INLINE plusR #-}
+plusR (MkR m1) (MkR m2) = MkR $ HML.union m1 m2
+
+-----
+
+consR :: forall d ds. KnownSymbol (Fst d) => Snd d -> R ('MkFD ds) -> R ('MkFD (d ': ds))
+{-# INLINE consR #-}
+consR v (MkR m) = MkR $ HML.insert (symbolVal (mkLabel @(Fst d))) (unsafeCoerce v) m
+
+-----
+
+unsafeExtricate1R :: KnownSymbol s => Label s -> R fd -> Eval a
+{-# INLINE unsafeExtricate1R #-}
+unsafeExtricate1R lbl (MkR m) = case HML.lookup k m of
+  Nothing -> error $  "Panic! An ill-formed record is missing field `" ++ k ++ "'"
+  Just v -> pure (unsafeCoerce v)
+  where
+  k = symbolVal lbl
+
+-----
+
+instance FDFoldable RShowField ex1 fd [String] => Show (R fd) where
+  showsPrec d r = showParen (d > 10) $ let
+    fs = rfoldMapR @ex1 MkRShowField r
+    in showString "MkR " . showFields fs
+
+-- | For example:
+--
+-- @
+--   *Data.Ruin.R> mapM_ putStrLn $ 'rfoldMapR' 'MkRShowField' $ 'oneR' \#x "x" \``plusR`\` 'oneR' \#y ()
+--   x = "x"
+--   y = ()
+-- @
+data RShowField = MkRShowField
+
+instance (KnownSymbol s, Show a,b ~ (a -> [String])) => FPure RShowField s b where
+  fpure = \_ a -> [symbolVal (mkLabel @s) ++ " = " ++ show a]
+
+showFields :: [String] -> ShowS
+showFields [] = showString "{}"
+showFields (x:xs) = showChar '{' . showString x . go xs
+  where
+    go [] = showChar '}'
+    go (y:ys) = showChar ',' . showString y . go ys
+
+-----
+
+instance FDFoldable2 REq ex1 fd ex3 All => Eq (R fd) where
+  r1 == r2 = getAll $ rfoldMap2R @ex1 @fd @ex3 MkREq r1 r2
+
+data REq = MkREq
+
+instance (Eq a,b ~ (a -> a -> All)) => FPure REq s b where
+  fpure _ = \x y -> All (x == y)
+
+-----
+
+instance (Eq (R fd),FDFoldable2 RCompare ex1 fd ex3 Ordering) => Ord (R fd) where
+  compare r1 r2 = rfoldMap2R @ex1 @fd @ex3 MkRCompare r1 r2
+
+data RCompare = MkRCompare
+
+instance (Ord a,b ~ (a -> a -> Ordering)) => FPure RCompare s b where
+  fpure _ = compare
+
+-----
+
+-- | A version of 'insertR' that requires that the field is not
+-- already in the record. 'setR' is the opposite.
+addR :: (KnownSymbol s,FDAbsent s fd) => Label s -> a -> R fd -> R (InsertFD s a fd)
+{-# INLINE addR #-}
+addR = insertR
+
+adjustR ::
+  ( KnownSymbol s
+  , fd1 ~ InsertFD s a fd2
+  , fd2 ~ InsertFD s b fd1
+  )
+  => Label s
+  -> (a -> b)
+  -> R fd1
+  -> R fd2
+{-# INLINE adjustR #-}
+adjustR lbl f (MkR m) = MkR $ HML.adjust (unsafeCoerce f) (symbolVal lbl) m
+
+deleteR :: KnownSymbol s => Label s -> R fd -> R (DeleteFD s fd)
+{-# INLINE deleteR #-}
+deleteR lbl (MkR m) = MkR $ HML.delete (symbolVal lbl) m
+
+-- | When forced, this 'Eval' computation extricates the value of the
+-- field from the rest of the record without forcing the value of the
+-- field itself. See 'extricate1' for further motivation.
+extricate1R :: KnownSymbol s => Label s -> R fd -> Eval (LookupFD s fd)
+{-# INLINE extricate1R #-}
+extricate1R = unsafeExtricate1R
+
+getR :: KnownSymbol s => Label s -> R fd -> LookupFD s fd
+{-# INLINE getR #-}
+getR lbl = runEval . extricate1R lbl
+
+-- | Add a field to a record, or overwrite it if it's already
+-- present. See 'addR' and 'setR'.
+insertR :: KnownSymbol s => Label s -> a -> R fd -> R (InsertFD s a fd)
+{-# INLINE insertR #-}
+insertR lbl x (MkR m) = MkR $ HML.insert (symbolVal lbl) (unsafeCoerce x) m
+
+-- | Left-biased.
+lmergeR :: R fd1 -> R fd2 -> R (LMergeFD fd1 fd2)
+{-# INLINE lmergeR #-}
+lmergeR (MkR m1) (MkR m2) = MkR $ HML.union m1 m2
+
+-- | A version of 'insertR' that requires that the field is already in
+-- the record. 'addR' is the opposite.
+setR :: forall s fd. KnownSymbol s => Label s -> LookupFD s fd -> R fd -> R fd
+{-# INLINE setR #-}
+setR = case fdIdentities @s @fd @(LookupFD s fd) of Refl -> insertR
+
+-----
+
+-- | The @"lensR/adjustR" RULE@ rewrites 'lensR' to the more efficient
+-- 'adjustR' whenever the lens's functor is 'Identity'.
+--
+-- Most notably, @"Control.Lens".'Control.Lens.over'@ uses 'Identity'.
+lensR ::
+  ( KnownSymbol s
+  , fd1 ~ InsertFD s a fd2
+  , fd2 ~ InsertFD s b fd1
+  , Functor f
+  )
+  => Label s
+  -> (a -> f b)
+  -> R fd1
+  -> f (R fd2)
+{-# INLINE[1] lensR #-}
+lensR lbl = \f r -> flip (insertR lbl) r <$> f (runEval (unsafeExtricate1R lbl r))
+
+{-# RULES
+
+  "lensR/adjustR"
+
+    forall lbl f.
+
+        lensR lbl f
+      =
+        Identity . adjustR lbl (runIdentity . f)
+
+  #-}
+
+-----
+
+monoadjustR :: forall s fd. KnownSymbol s => Label s -> (LookupFD s fd -> LookupFD s fd) -> R fd -> R fd
+{-# INLINE monoadjustR #-}
+monoadjustR = case fdIdentities @s @fd @(LookupFD s fd) of Refl -> adjustR
+
+lens'R ::
+  forall s fd f.
+  ( KnownSymbol s
+  , Functor f
+  )
+  => Label s
+  -> (LookupFD s fd -> f (LookupFD s fd))
+  -> R fd
+  -> f (R fd)
+{-# INLINE lens'R #-}
+lens'R = case fdIdentities @s @fd @(LookupFD s fd) of Refl -> lensR
+
+-----
+
+instance KnownSymbol s => HasCase s (R fd) where
+  type FieldTypeCase s (R fd) = LookupFD s fd
+  {-# INLINE extricate1Case #-}
+  extricate1Case = unsafeExtricate1R
+
+instance ClosedHas s (R fd) => Has s (R fd) where
+  type FieldType s (R fd) = FieldTypeCase s (R fd)
+  {-# INLINE extricate1 #-}
+  extricate1 = closedExtricate1
+
+-----
+
+instance (KnownFD fd,Hoid 'MkFD fd) => Build (R fd) where
+  type Fields (R fd) = FieldsFD fd
+  type Shape (R fd) o = (Hoid R o,Hoid 'MkFD (RFD o),SameFields (FieldsFD fd) (FieldsFD (RFD o)))
+  build = buildR
+  buildNonStrict = runCEI . build
+
+type family FieldsFD (fd :: FD) :: [(Symbol,*)] where
+  FieldsFD ('MkFD ds) = ds
+
+type family SameFields (ds1 :: [(Symbol,*)]) (ds2 :: [(Symbol,*)]) :: Constraint where
+  SameFields '[] ds2 = ('[] ~ ds2)
+  SameFields (d ': ds1) ds2 =
+    ( (Head ds2 ': Tail ds2) ~ ds2
+    , '(Fst d,Snd (Head ds2)) ~ Head ds2
+    , SameFields ds1 (Tail ds2)
+    )
+
+class KnownFD (fd :: FD) where
+  buildR :: (Applicative i,GivesThese (Fields (R fd)) i rc) => rc -> Compose Eval i (R fd)
+
+instance KnownFD1 ds => KnownFD ('MkFD ds) where
+  buildR = buildR1
+
+class KnownFD1 (ds :: [(Symbol,*)]) where
+  buildR1 :: (Applicative i,GivesThese ds i rc) => rc -> Compose Eval i (R ('MkFD ds))
+
+instance KnownFD1 '[] where
+  {-# INLINE buildR1 #-}
+  buildR1 = const $ pure nilR
+
+instance (KnownSymbol (Fst d),KnownFD1 ds) => KnownFD1 (d ': ds) where
+  {-# INLINE buildR1 #-}
+  buildR1 rc = consR <$> get @(Fst d) rc <*> buildR1 rc
+
+-----
+
+-- | The type and value of @a@ determine the type and value of every
+-- field in @fd@.
+type family FDPure (a :: *) (fd :: FD) :: Constraint where
+  FDPure a fd = (FDPure0 a fd,Hoid 'MkFD fd)
+
+class FDPure0 (a :: *) (fd :: FD) where
+  rpureR0 :: a -> R fd
+
+instance FDPure1 a ds => FDPure0 a ('MkFD ds) where rpureR0 = rpureR1
+
+class FDPure1 (a :: *) (ds :: [(Symbol,*)]) where rpureR1 :: a -> R ('MkFD ds)
+
+instance FDPure1 a '[] where
+  {-# INLINE rpureR1 #-}
+  rpureR1 = const nilR
+
+instance (KnownSymbol (Fst d),FPure a (Fst d) (Snd d),FDPure1 a ds) => FDPure1 a (d ': ds) where
+  {-# INLINE rpureR1 #-}
+  rpureR1 a = consR (fpure @a @(Fst d) a) (rpureR1 a)
+
+-- | A specialized 'rpure' for 'R'.
+rpureR :: FDPure a fd => a -> R fd
+{-# INLINE rpureR #-}
+rpureR = rpureR0
+
+-- | A specialized 'rmonopure' for 'R'.
+rmonopureR :: FDPure (RMonoPure a) fd => a -> R fd
+{-# INLINE rmonopureR #-}
+rmonopureR = rpureR . MkRMonoPure
+
+-- | A specialized 'rpolypure' for 'R'.
+rpolypureR :: FDPure a fd => a -> R fd
+{-# INLINE rpolypureR #-}
+rpolypureR = rpureR
+
+-- | A specialized 'rmempty' for 'R'.
+rmemptyR :: FDPure RMEmpty fd => R fd
+{-# INLINE rmemptyR #-}
+rmemptyR = rpureR MkRMEmpty
+
+data RMAppendR = MkRMAppendR
+
+instance (Monoid m,b ~ (m -> m -> m)) => FPure RMAppendR s b where fpure _ = mappend
+
+-- | A specialized 'rmappend' for 'R'.
+rmappendR :: FDPure RMAppendR fd => R fd
+{-# INLINE rmappendR #-}
+rmappendR = rpureR MkRMAppendR
+
+data RSAppendR = MkRSAppendR
+
+instance (Semigroup g,b ~ (g -> g -> g)) => FPure RSAppendR s b where fpure _ = (<>)
+
+-- | A specialized 'rsappend' for 'R'.
+rsappendR :: FDPure RSAppendR fd => R fd
+{-# INLINE rsappendR #-}
+rsappendR = rpureR MkRSAppendR
+
+-- | A specialized 'rlabel' for 'R'.
+rlabelR :: FDPure RLabel fd => R fd
+{-# INLINE rlabelR #-}
+rlabelR = rpureR MkRLabel
+
+-----
+
+infixl 4 `rmapR`
+
+-- | A specialized 'rmap' for 'R'.
+rmapR ::
+  forall fd1 fd2 fd3 fun.
+  ( FDPure fun fd1
+  , FDSplat fd1 fd2 fd3
+  , UnifyShape (R fd1) (R fd2)
+  , UnifyShape (R fd2) (R fd3)
+  ) => fun -> R fd2 -> R fd3
+{-# INLINE rmapR #-}
+rmapR fun r = (rpureR fun :: R fd1) `rsplatR` r
+
+infixl 4 `rsplatR`
+
+-- | A specialized 'rsplat' for 'R'.
+rsplatR ::
+  ( FDSplat fd1 fd2 fd3
+  , UnifyShape (R fd1) (R fd2)
+  , UnifyShape (R fd2) (R fd3)
+  ) => R fd1 -> R fd2 -> R fd3
+{-# INLINE rsplatR #-}
+rsplatR (MkR m1) (MkR m2) = MkR $ HML.intersectionWith unsafeCoerce m1 m2
+
+-- | Each field in @fd1@ is a function from the same field in @fd2@ to
+-- the same field in @fd3@.
+type family FDSplat (fd1 :: FD) (fd2 :: FD) (fd3 :: FD) :: Constraint where
+  FDSplat ('MkFD ds1) ('MkFD ds2) ('MkFD ds3) = FDSplat1 ds1 ds2 ds3
+
+type family FDSplat1 (ds1 :: [(Symbol,*)]) (ds2 :: [(Symbol,*)]) (ds3 :: [(Symbol,*)]) :: Constraint where
+  FDSplat1 '[] '[] '[] = ()
+  FDSplat1 (f ': fs) (a ': as) (b ': bs) = (Snd f ~ (Snd a -> Snd b),FDSplat1 fs as bs)
+
+-----
+
+infixl 4 `rmapAR`
+
+-- | A specialized 'rmapA' for 'R'.
+rmapAR ::
+  forall fun fd1 fd2 fd3 i.
+  ( Applicative i
+  , FDPure fun fd1
+  , FDSplatA i fd1 fd2 fd3
+  , UnifyShape (R fd1) (R fd2)
+  , UnifyShape (R fd2) (R fd3)
+  ) => fun -> R fd2 -> i (R fd3)
+{-# INLINE rmapAR #-}
+rmapAR fun r = (rpureR fun :: R fd1) `rsplatAR` r
+
+infixl 4 `rsplatAR`
+
+-- | A specialized 'rsplatA' for 'R'.
+rsplatAR ::
+  ( Applicative i
+  , FDSplatA i fd1 fd2 fd3
+  , UnifyShape (R fd1) (R fd2)
+  , UnifyShape (R fd2) (R fd3)
+  ) => R fd1 -> R fd2 -> i (R fd3)
+{-# INLINE rsplatAR #-}
+rsplatAR (MkR m1) (MkR m2) = fmap MkR $ sequenceA $ HML.intersectionWith unsafeCoerce m1 m2
+
+-- | Each field in @fd1@ is a function from the same field in @fd2@ to
+-- an @i@-structure of the same field in @fd3@.
+type family FDSplatA (i :: * -> *) (fd1 :: FD) (fd2 :: FD) (fd3 :: FD) :: Constraint where
+  FDSplatA i ('MkFD ds1) ('MkFD ds2) ('MkFD ds3) = FDSplatA1 i ds1 ds2 ds3
+
+type family FDSplatA1 (i :: * -> *) (ds1 :: [(Symbol,*)]) (ds2 :: [(Symbol,*)]) (ds3 :: [(Symbol,*)]) :: Constraint where
+  FDSplatA1 _ '[] '[] '[] = ()
+  FDSplatA1 i (f ': fs) (a ': as) (b ': bs) = (Snd f ~ (Snd a -> i (Snd b)),FDSplatA1 i fs as bs)
+
+-----
+
+-- | Beware: the order in which the fields are combined is undefined,
+-- so the 'Monoid' ought to be commutative.
+rfoldR :: (Monoid m,FDHomogenous m fd) => R fd -> m
+{-# INLINE rfoldR #-}
+rfoldR (MkR m) = foldMap unsafeCoerce m
+
+type family HomogenizeFD (c :: *) (fd :: FD) :: FD where
+  HomogenizeFD c ('MkFD ds) = 'MkFD (MapSecondConst c ds)
+
+type family FDFoldable (fun :: *) (fd1 :: FD) (fd2 :: FD) (m :: *) where
+  FDFoldable fun fd1 fd2 m =
+    ( FDPure fun fd1
+    , FDSplat fd1 fd2 (HomogenizeFD m fd2)
+    , FDHomogenous m (HomogenizeFD m fd2)
+    , Monoid m
+    , UnifyShape (R fd1) (R fd2)
+    , UnifyShape (R fd2) (R (HomogenizeFD m fd2))
+    )
+
+rfoldMapR ::
+  forall fd1 fd2 fun m.
+     FDFoldable fun fd1 fd2 m
+  => fun -> R fd2 -> m
+{-# INLINE rfoldMapR #-}
+rfoldMapR fun r =
+  rfoldR ((rpureR fun :: R fd1) `rsplatR` r :: R (HomogenizeFD m fd2))
+
+type family FDFoldable2 (fun :: *) (fd1 :: FD) (fd2 :: FD) (fd3 :: FD) (m :: *) where
+  FDFoldable2 fun fd1 fd2 fd3 m =
+    ( FDPure fun fd1
+    , FDSplat fd1 fd2 fd3
+    , FDSplat fd3 fd2 (HomogenizeFD m fd2)
+    , FDHomogenous m (HomogenizeFD m fd2)
+    , Monoid m
+    , UnifyShape (R fd1) (R fd2)
+    , UnifyShape (R fd2) (R fd3)
+    , UnifyShape (R fd2) (R (HomogenizeFD m fd2))
+    )
+
+rfoldMap2R ::
+  forall fd1 fd2 fd3 fun m.
+     FDFoldable2 fun fd1 fd2 fd3 m
+  => fun -> R fd2 -> R fd2 -> m
+{-# INLINE rfoldMap2R #-}
+rfoldMap2R fun l r =
+  rfoldR
+   ((((rpureR fun :: R fd1)
+   `rsplatR` l :: R fd3)
+   `rsplatR` r :: R (HomogenizeFD m fd2)))
+
+-----
+
+-- | Beware: these conversions are inefficient and very unlikely to be
+-- simplified away.
+instance (Hoid 'MkFD fd,GenericDs (FieldsFD fd)) => G.Generic (R fd) where
+  type Rep (R fd) = RepDs (FieldsFD fd)
+  to = toDs
+  from = fromDs
+
+class GenericDs (ds :: [(Symbol,*)]) where
+  type RepDs ds :: * -> *
+  toDs :: RepDs ds x -> R ('MkFD ds)
+  fromDs :: R ('MkFD ds) -> RepDs ds x
+
+instance GenericDs '[] where
+  type RepDs '[] = G.U1
+  toDs _ = nilR
+  fromDs _ = G.U1
+
+instance (KnownSymbol (Fst d),Hoid '(,) d) => GenericDs '[d] where
+  type RepDs '[d] = G.S1 ('G.MetaSel ('Just (Fst d)) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy) (G.Rec0 (Snd d))
+  toDs (G.M1 (G.K1 x)) = oneR mkLabel x
+  fromDs r = G.M1 (G.K1 (getR (mkLabel @(Fst d)) r))
+
+instance
+     ( o ~ (d1 ': d2 ': ds)
+     , GenericDs (FirstHalf o)
+     , GenericDs (SecondHalf o)
+     , KnownFD1 (FirstHalf o)
+     , KnownFD1 (SecondHalf o)
+     , GivesThese (FirstHalf o) Identity (GiveAllItHas (R ('MkFD o)))
+     , GivesThese (SecondHalf o) Identity (GiveAllItHas (R ('MkFD o)))
+     )
+  => GenericDs (d1 ': d2 ': ds) where
+  type RepDs (d1 ': d2 ': ds) =
+          RepDs (FirstHalf (d1 ': d2 ': ds))
+    G.:*:
+          RepDs (SecondHalf (d1 ': d2 ': ds))
+  toDs (l G.:*: r) = case fdIdentities @"" @('MkFD o) @() of
+    Refl ->
+              (toDs l :: R ('MkFD (FirstHalf o)))
+      `plusR`
+              (toDs r :: R ('MkFD (SecondHalf o)))
+  fromDs = (\(l,r) -> fromDs l G.:*: fromDs r) . halves
+
+halves ::
+     ( KnownFD1 (FirstHalf ds)
+     , KnownFD1 (SecondHalf ds)
+     , GivesThese (FirstHalf ds) Identity (GiveAllItHas (R ('MkFD ds)))
+     , GivesThese (SecondHalf ds) Identity (GiveAllItHas (R ('MkFD ds)))
+     )
+  => R ('MkFD ds) -> (R ('MkFD (FirstHalf ds)),R ('MkFD (SecondHalf ds)))
+halves r = (rupNonStrict r,rupNonStrict r)
+
+-----
+
+instance FDFoldable RLiftField ex1 fd [TH.ExpQ] => Lift (R fd) where
+  lift = foldr TH.appE [| nilR |] . id @[TH.ExpQ] . rfoldMapR @ex1 MkRLiftField
+
+data RLiftField = MkRLiftField
+
+instance (KnownSymbol s,Lift a,b ~ (a -> [TH.ExpQ])) => FPure RLiftField s b where
+  fpure = \_ a -> [ [| insertR (mkLabel :: Label $s) a |] ]
+    where
+    s = TH.litT $ TH.strTyLit $ symbolVal (mkLabel @s)
diff --git a/Data/Ruin/TH.hs b/Data/Ruin/TH.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ruin/TH.hs
@@ -0,0 +1,140 @@
+{-# Language LambdaCase #-}
+{-# Language TemplateHaskell #-}
+{-# Language ViewPatterns #-}
+
+{-# OPTIONS_HADDOCK hide,not-home #-}
+
+module Data.Ruin.TH (makeRecords) where
+
+import Data.List (find)
+import Language.Haskell.TH
+
+import Data.Ruin.All
+import Data.Ruin.ClosedHas
+import Data.Ruin.Hoid (Hoid)
+import Data.Ruin.Internal
+
+-- | Declare the straight-forward 'Has' and 'Build' instances for a
+-- record type. A data type is a /record type/ if it has exactly one
+-- constructor and that constructor is declared using record syntax.
+--
+-- An instance of a data family can be a record type; refer to that
+-- type by the name of the instance's constructor.
+--
+-- The generated code relies on the "GHC.Generics" defaults in the
+-- same way a user would; it merely relieves you from enumerating the
+-- per-field instances.
+--
+-- Also, the splice will declare the instances in the style of
+-- "Data.Ruin.ClosedHas".
+makeRecords :: [Name] -> Q [Dec]
+makeRecords = fmap concat . mapM interpretName
+
+interpretName :: Name -> Q [Dec]
+interpretName n0 = start
+  where
+  abort :: Q a
+  abort = fail $ unwords [
+      "`makeRecords' cannot handle `" ++ show n0 ++ "' because the declared data type"
+    ,
+      "doesn't have exactly one constructor"
+    ,
+      "or it doesn't use record syntax."
+    ]
+
+  start :: Q [Dec]
+  start = do
+    (dn,t,fnames,mshape) <- reifyDataDecl n0 >>= maybe abort interpretDataDecl
+    fmap concat $ sequence $
+        [d| instance NoWarnUnusedTopBind $t where
+              noWarnUnusedTopBind $(recP dn [ (,) fname <$> wildP | fname <- fnames ]) = ()
+          |]
+      : maybe id addShape mshape
+        [d| instance Build $t where
+              {-# INLINE build #-}
+              build = genericBuild
+              {-# INLINE buildNonStrict #-}
+              buildNonStrict = genericBuildNonStrict
+          |]
+      : [d| instance ClosedHas s $t => Has s $t where
+              {-# INLINE extricate1 #-}
+              extricate1 = closedExtricate1
+          |]
+      : [ [d| instance HasCase $s $t |]
+        | s <- map (litT . strTyLit . nameBase) fnames
+        ]
+
+  addShape sh q = q >>= \case
+    [InstanceD mo c ihead@(AppT _ t) decs] -> do
+      o <- newName "o"
+      s <- sh o
+      let inst = TySynInstD ''Shape (TySynEqn [t,VarT o] s)
+      return [InstanceD mo c ihead (decs ++ [inst])]
+    _ -> fail "impossible! Quote of instance wasn't InstanceD"
+
+  -- | Map a record type declaration to its ctor name, its fully
+  -- applied type, its field names, and its shape.
+  interpretDataDecl :: Dec -> Q (Name,TypeQ,[Name],Maybe (Name -> TypeQ))
+  interpretDataDecl = \case
+    DataD _ n args _ [interpretCtor -> Just (dn,fnames)] _ -> return (dn,app n (map tvb args) Nothing,fnames,Nothing)
+    NewtypeD _ n args _ (interpretCtor -> Just (dn,fnames)) _ -> return (dn,app n (map tvb args) Nothing,fnames,Nothing)
+    DataInstD _ n args mk [interpretCtor -> Just (dn,fnames)] _ -> return (dn,app n args mk,fnames,Just $ dfShape n args)
+    NewtypeInstD _ n args mk (interpretCtor -> Just (dn,fnames)) _ -> return (dn,app n args mk,fnames,Just $ dfShape n args)
+    _ -> abort
+    where
+    tvb = \case
+      PlainTV n -> VarT n
+      KindedTV n _ -> VarT n
+
+    app :: Name -> [Type] -> Maybe Kind -> TypeQ
+    app n args mk =
+        return
+      $ maybe id (flip SigT) mk
+      $ foldl AppT (ConT n) args
+
+  -- | Map a constructor to its ctor name and field names.
+  interpretCtor :: Con -> Maybe (Name,[Name])
+  interpretCtor = \case
+    RecC dn vbts -> Just (dn,[ n | (n,_,_t) <- vbts ])
+    ForallC _ _ ctor -> interpretCtor ctor
+    RecGadtC (dn:_) vbts _ -> Just (dn,[ n | (n,_,_t) <- vbts ])
+    _ -> Nothing
+
+-- | If the name refers to a data type or a data constructor, return
+-- the declaration of the data type.
+--
+-- Only fails monadically if 'reify' fails.
+reifyDataDecl :: Name -> Q (Maybe Dec)
+reifyDataDecl n0 = reify n0 >>= \case
+  TyConI d -> return $ Just d
+  -- indirect through a constructor name to its parent's name
+  DataConI _ _ parent -> reify parent >>= \case
+    TyConI d -> return $ Just d
+    FamilyI DataFamilyD{} is -> return $ find sameCtorName is
+    _ -> return Nothing
+  _ -> return Nothing
+  where
+  sameCtorName :: Dec -> Bool
+  sameCtorName = \case
+    DataInstD _ _ _ _ [ctor] _ -> n0 == ctorName ctor
+    NewtypeInstD _ _ _ _ ctor _ -> n0 == ctorName ctor
+    _ -> False
+    where
+    ctorName :: Con -> Name
+    ctorName = \case
+      NormalC n _ -> n
+      RecC n _ -> n
+      InfixC _ n _ -> n
+      ForallC _ _ ctor -> ctorName ctor
+      GadtC (head -> n) _ _ -> n
+      RecGadtC (head -> n) _ _ -> n
+
+-- | Map a data family name and instance arguments to its 'Shape'.
+dfShape :: Name -> [Type] -> Name -> TypeQ
+dfShape dfname args (varT -> o) = reify dfname >>= \case
+  FamilyI (DataFamilyD _ (length -> nidx) _) _ -> do
+    let indices = take nidx args
+    let t = return $ foldl AppT (ConT dfname) indices
+    [t| Hoid $t $o |]
+    where
+  _ -> fail "impossible: DataInstD or NewtypeInstD does not name a DataFamilyD"
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+Copyright (c) 2016, Nicolas Frisby
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+contributors may be used to endorse or promote products derived from
+this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/ruin.cabal b/ruin.cabal
new file mode 100644
--- /dev/null
+++ b/ruin.cabal
@@ -0,0 +1,104 @@
+name: ruin
+version: 0.1.0.0
+cabal-version: >=1.10
+build-type: Simple
+license: BSD3
+license-file: LICENSE
+copyright: 2016 Nicolas Frisby
+maintainer: nicolas.frisby@gmail.com
+synopsis: Pliable records
+description:
+    @ruin@ is a DSL for working with record types. It focuses on
+    converting between conventionally-declared record types and
+    supporting named function arguments.
+    .
+    * Uses @-XOverloadedLabels@, so that @#x@ is a first-class label for
+    the field named @x@.
+    * Provides @GHC.Generics@ defaults.
+    * Named arguments: @\\[rna|x y z] -> (x,y,z)@ inhabits @("x" :\@ a,"y"
+    :\@ b,"z" :\@ c) -> (a,b,c)@.
+    * Relies on @-XDuplicateRecordFields@; the generic defaults only
+    work if record selector names do not have distinguishing prefices.
+    * Custom type errors, such as @ruin: Could not find the field \`x\'
+    in the type ...@
+    * "Data.Ruin.R" provides anonymous record types where the order of
+    fields is irrelevant.
+    .
+    See the "Data.Ruin" module for an overview.
+category: Data, Records
+author: Nicolas Frisby
+
+flag werror
+    description:
+        Enable -Werror
+    default: False
+    manual: True
+
+library
+    
+    if flag(werror)
+        ghc-options: -Werror
+    exposed-modules:
+        Data.Ruin
+        Data.Ruin.Ancillaries
+        Data.Ruin.ClosedHas
+        Data.Ruin.Core
+        Data.Ruin.Deep
+        Data.Ruin.Eval
+        Data.Ruin.R
+    build-depends:
+        base >=4.9 && <=5,
+        binary >=0.8.3.0 && <0.9,
+        cereal >=0.5.2.0 && <0.6,
+        deepseq >=1.4.2.0 && <1.5,
+        ghc-prim >=0.5.0.0 && <0.6,
+        parsec >=3.1.11 && <3.2,
+        template-haskell >=2.11.0.0 && <2.12,
+        unordered-containers >=0.2.7.1 && <0.3
+    default-language: Haskell2010
+    other-modules:
+        Data.Ruin.All
+        Data.Ruin.Fieldwise
+        Data.Ruin.Hide
+        Data.Ruin.Hoid
+        Data.Ruin.Internal
+        Data.Ruin.QQ
+        Data.Ruin.QQ.Parser
+        Data.Ruin.TH
+    ghc-options: -Wall
+
+test-suite test
+    
+    if flag(werror)
+        ghc-options: -Werror
+    type: exitcode-stdio-1.0
+    main-is: Test.hs
+    build-depends:
+        base >=4.9.0.0 && <4.10,
+        ruin >=0.1.0.0 && <0.2,
+        hspec >=2.2.3 && <2.3,
+        lens ==4.14.*,
+        mtl >=2.2.1 && <2.3,
+        optparse-applicative >=0.12.1.0 && <0.13,
+        should-not-typecheck >=2.1.0 && <2.2,
+        smallcheck >=1.1.1 && <1.2,
+        template-haskell >=2.11.0.0 && <2.12
+    default-language: Haskell2010
+    hs-source-dirs: test
+    other-modules:
+        MustCompile.ClosedHas
+        MustCompile.HRDatabase
+        MustCompile.Physics
+        MustCompile.PrintAndTime
+        MustCompile.RNA
+        MustCompile.RSplat
+        MustCompile.RSplit
+        MustCompile.TH
+        MustNotCompile
+        StrictCheck
+        Strictness
+        StrictnessTypes
+        Test.R
+        Test.RNA
+        XY
+    ghc-options: -Wall
diff --git a/test/MustCompile/ClosedHas.hs b/test/MustCompile/ClosedHas.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/ClosedHas.hs
@@ -0,0 +1,33 @@
+{-# Language DataKinds #-}
+{-# Language DeriveGeneric #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language UndecidableInstances #-}
+{-# Language ViewPatterns #-}
+
+module MustCompile.ClosedHas () where
+
+import GHC.Generics (Generic)
+
+import Data.Ruin
+import Data.Ruin.Ancillaries (genericBuild)
+import Data.Ruin.ClosedHas
+
+data XY x y = MkXY {x::x,y::y} deriving Generic
+
+instance NoWarnUnusedTopBind XY where
+   noWarnUnusedTopBind MkXY{x=_,y=_} = ()
+
+instance ClosedHas s (XY x y) => Has s (XY x y) where
+  {-# INLINE extricate1 #-}
+  extricate1 = closedExtricate1
+
+instance HasCase "x" (XY x y)
+instance HasCase "y" (XY x y)
+
+instance Build (XY x y) where
+  {-# INLINE build #-}
+  build = genericBuild
diff --git a/test/MustCompile/HRDatabase.hs b/test/MustCompile/HRDatabase.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/HRDatabase.hs
@@ -0,0 +1,43 @@
+{-# Language DataKinds #-}
+{-# Language DeriveGeneric #-}
+{-# Language DuplicateRecordFields #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language QuasiQuotes #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language UndecidableInstances #-}
+{-# Language ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+module MustCompile.HRDatabase () where
+
+import GHC.Generics (Generic)
+
+import Data.Ruin
+
+data Job = Baker | Carpenter | Coder | Artist
+  deriving Eq
+
+data Person = MkPerson {name :: String,age :: Int,job :: Job} deriving Generic
+data Opening = MkOpening {job :: Job,company :: String} deriving Generic
+data Match = MkMatch {job :: Job,company :: String,name :: String,age :: Int} deriving Generic
+
+$(makeRecords [''Person,''Opening,''Match])
+
+jobJoin :: [Person] -> [Opening] -> [Match]
+jobJoin ps os =
+  [ rto @Match (p <@ o)
+  | p <- ps, o <- os, j p == j o
+  ]
+  where
+  j (rup -> [rna|x@job|]) = x
+
+people :: [Person]
+people = [rnaA| Person (...I) name age job |]
+  where
+  nameI = ["Vin","Elend","Sazed"]
+  ageI = (+20) <$> [1..5]
+  jobI = [Baker,Carpenter]
diff --git a/test/MustCompile/Physics.hs b/test/MustCompile/Physics.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/Physics.hs
@@ -0,0 +1,45 @@
+{-# Language DataKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language OverloadedLabels #-}
+{-# Language PartialTypeSignatures #-}
+{-# Language QuasiQuotes #-}
+{-# Language TypeApplications #-}
+{-# Language ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+module MustCompile.Physics () where
+
+import Data.Ruin
+
+-- | The vacuum permittivity constant, in farads per meter.
+eps0 :: Fractional a => a
+eps0 = 8.854187817e-12
+
+-- | Capacitance of a conducting cylinder of radius @r@ and length @l@
+-- surrounded concentrically by conducting cylindrical shell of inner
+-- radius @r + gap@ and equal length where the gap has a dielectric
+-- constant of @kappa@.
+--
+-- From <http://www.phys.uri.edu/gerhard/PHY204/tsl105.pdf> and
+-- <http://physics.info/equations/> (\"cylindrical capacitor\").
+cylindricalCapacitance :: Floating a => _ -> a
+cylindricalCapacitance [rna|kappa l gap r|] =
+    2 * pi * kappa * eps0 * l
+  / log (b / a)
+  where
+  a = r
+  b = r + gap
+
+test :: Double
+test =
+  cylindricalCapacitance $ rsym (
+      dub #l 3
+    ,
+      dub #r 1.2
+    ,
+      dub #gap 1
+    ,
+      dub #kappa 2
+    )
diff --git a/test/MustCompile/PrintAndTime.hs b/test/MustCompile/PrintAndTime.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/PrintAndTime.hs
@@ -0,0 +1,27 @@
+{-# Language DataKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language ScopedTypeVariables #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+-- | This is the example from the Haddock on 'MapF'.
+
+module MustCompile.PrintAndTime () where
+
+import qualified System.CPUTime
+
+import Data.Ruin
+
+data PrintAndTime = MkPrintAndTime
+
+instance (Show a,f ~ (a -> IO (a,Integer))) => FPure PrintAndTime s f where
+  fpure = \_ x -> do
+    print x
+    (,) x <$> System.CPUTime.getCPUTime
+
+_printAndTime :: (Show x, Show y) => ("x" :@ x,"y" :@ y) -> IO ("x" :@ (x,Integer),"y" :@ (y,Integer))
+_printAndTime = rmapA MkPrintAndTime
diff --git a/test/MustCompile/RNA.hs b/test/MustCompile/RNA.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/RNA.hs
@@ -0,0 +1,44 @@
+{-# Language DataKinds #-}
+{-# Language QuasiQuotes #-}
+{-# Language TypeOperators #-}
+{-# Language ViewPatterns #-}
+
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+module MustCompile.RNA () where
+
+import Data.Ruin
+import Data.Ruin.Ancillaries (Tup1)
+
+import XY
+
+_p = (
+    (\[rna|(l...) x y|] -> [lx,ly]) :: ("x" :@ a,"y" :@ a) -> [a]
+  ,
+    (\[rna|(...R) x y|] -> [xR,yR]) :: ("x" :@ a,"y" :@ a) -> [a]
+  ,
+    \[rna||] -> ()
+  ,
+    (\[rna|c@C|] -> c) :: Tup1 ("C" :@ a) -> a
+  ,
+    (\[rna| !strict !bang@! |] -> [strict,bang]) :: ("strict" :@ a,"!" :@ a) -> [a]
+  ,
+    (\[rna|_ _@x|] -> ()) :: ("_" :@ a, "x" :@ x) -> ()
+  ,
+    (\[rna|XY (...R) a@x|] -> aR) :: XY x y -> x
+  )
+
+_e = (
+    [rna||] :: ()
+  ,
+    [rna|a|] :: Tup1 ("a" :@ ())
+  ,
+    [rna|a b|] :: ("a" :@ (),"b" :@ ())
+  ,
+    [rna|a b|] :: ("a" :@ (),"b" :@ ())
+  ,
+    [rna|XY a@x b@y|] :: XY () ()
+  )
+  where
+  a = ()
+  b = ()
diff --git a/test/MustCompile/RSplat.hs b/test/MustCompile/RSplat.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/RSplat.hs
@@ -0,0 +1,21 @@
+{-# Language DataKinds #-}
+{-# Language QuasiQuotes #-}
+{-# Language TypeApplications #-}
+
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+module MustCompile.RSplat () where
+
+import Data.Ruin
+
+import XY
+
+xy = [rna|XY x y|]
+  where
+  x = True
+  y = "Hello"
+
+_test = hoid @XY $ rsplat (rsym [rna|x y|]) xy
+  where
+  x = show
+  y = (++ ", World.")
diff --git a/test/MustCompile/RSplit.hs b/test/MustCompile/RSplit.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/RSplit.hs
@@ -0,0 +1,28 @@
+{-# Language DataKinds #-}
+{-# Language DeriveGeneric #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language QuasiQuotes #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+
+module MustCompile.RSplit () where
+
+import Control.Arrow ((***))
+import GHC.Generics (Generic)
+
+import Data.Ruin
+
+import XY
+
+data AB a b = MkAB {a::a,b::b} deriving (Generic,Show)
+$(makeRecords [''AB])
+
+-- _e ::
+--   (Monoid a3, Monoid a2, Monoid a1, Monoid a) =>
+--   t -> (XY a2 a3, AB a a1)
+_e _ = hoid @XY *** hoid @AB $ rsym [rna|mempty@a mempty@b mempty@x mempty@y|]
diff --git a/test/MustCompile/TH.hs b/test/MustCompile/TH.hs
new file mode 100644
--- /dev/null
+++ b/test/MustCompile/TH.hs
@@ -0,0 +1,40 @@
+{-# Language DataKinds #-}
+{-# Language DeriveGeneric #-}
+{-# Language DuplicateRecordFields #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language GADTs #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language OverloadedLabels #-}
+{-# Language PolyKinds #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language UndecidableInstances #-}
+
+module MustCompile.TH where
+
+import GHC.Generics (Generic)
+import Language.Haskell.TH.Syntax (Lift(lift))
+
+import Data.Ruin
+import Data.Ruin.R
+
+data family Family (t :: k) y
+
+data instance Family t Int where
+   MkFamily1 :: {x,y :: Int} -> Family t Int
+ deriving Generic
+
+$(makeRecords ['MkFamily1])
+
+newtype instance Family [] Char =
+   MkFamily2 {x :: Int}
+ deriving Generic
+
+$(makeRecords ['MkFamily2])
+
+-----
+
+r :: Rcrd '[ "a" ::: () , "b" ::: Bool ]
+r = $(lift (oneR #a () `plusR` oneR #b True))
diff --git a/test/MustNotCompile.hs b/test/MustNotCompile.hs
new file mode 100644
--- /dev/null
+++ b/test/MustNotCompile.hs
@@ -0,0 +1,56 @@
+{-# Language DataKinds #-}
+{-# Language OverloadedLabels #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language TypeOperators #-}
+
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# OPTIONS_GHC -Wno-deferred-type-errors #-}
+
+module MustNotCompile (test) where
+
+import Language.Haskell.TH.Syntax (Lift(lift))
+import Test.Hspec (Spec,describe,it)
+import Test.ShouldNotTypecheck (shouldNotTypecheck)
+
+import Data.Ruin
+import Data.Ruin.Ancillaries (rupNonStrict)
+
+x :: "x" :@ ()
+x = dub #x ()
+
+y :: "y" :@ ()
+y = dub #y ()
+
+test :: Spec
+test = do
+  describe "Missing fields prevent" $ do
+    it "`extricate1'" $ shouldNotTypecheck $
+      extricate1 #x y
+    it "`rup'" $ shouldNotTypecheck $
+      rup y `asTypeOf` x
+    it "`rupNonStrict'" $ shouldNotTypecheck $
+      rupNonStrict y `asTypeOf` x
+
+  describe "`lift'" $ do
+    it "preserves the field name for singleton records" $ shouldNotTypecheck $
+      $(lift (dub #x ())) `asTypeOf` dub #y ()
+
+{-
+  -- Test incorrectly fails, perhaps because of https://github.com/CRogers/should-not-typecheck/issues/5
+  describe "Extra fields prevent" $ do
+    it "`req'" $ shouldNotTypecheck $
+      req (x,y) `asTypeOf` y
+
+  -- Each of these causes a panic in GHC 8.0.1
+  data RecordDict :: * -> * where
+    MkRecordDict :: Record t => RecordDict t
+  describe "These are not instances of `Record'" $ do
+    it "Types with overlapping fields, e.g. (X,X)" $ shouldNotTypecheck $
+      MkRecordDict @(X,X)
+    it "Pair _ _" $ shouldNotTypecheck $
+      MkRecord @(Pair () ())
+  describe "A function" $ do
+    it "is not a record" $ shouldNotTypecheck $
+      MkRecord @(() -> ())
+-}
diff --git a/test/StrictCheck.hs b/test/StrictCheck.hs
new file mode 100644
--- /dev/null
+++ b/test/StrictCheck.hs
@@ -0,0 +1,94 @@
+{-# Language LambdaCase #-}
+{-# Language TypeOperators #-}
+{-# Language ViewPatterns #-}
+
+-- | This is a small wrapper around the generation capability of the
+-- @smallcheck@ library.
+--
+-- The key idea is that everywhere smallcheck would create a
+-- non-strict data constructor, it should also include the possibility
+-- that that position is an exception. In any given generated value,
+-- each such exception is unique. This means that if two functions
+-- applies to that same generated value always produce either the same
+-- value or the same exception, then those functions have the exact
+-- same strictness.
+
+module StrictCheck (
+  SSerial(..),
+  sameStrictness,
+  sdecDepth,
+  (<~>),
+  ) where
+
+import Control.Applicative ((<|>))
+import Control.Exception
+import Control.Monad (guard)
+import Control.Monad.State (State,evalState,get,modify)
+import Control.Monad.Trans (lift)
+import Test.SmallCheck.Series
+
+import Data.Ruin ((:@),dub)
+import Data.Ruin.Ancillaries (Pair(..),Tup1(..),mkLabel)
+
+data Landmine = MkLandmine {unLandmine :: Int} deriving (Eq,Show)
+
+instance Exception Landmine
+
+type SSeries = Series (State Int)
+
+-- | Use instead of 'decDepth'.
+sdecDepth :: SSeries a -> SSeries a
+sdecDepth m = do
+  do d <- getDepth
+     guard $ d > 0
+  localDepth (subtract 1) $ do
+    n <- lift get
+    lift $ modify (+1)
+    pure (throw (MkLandmine n)) <|> m
+
+-- | Use instead of 'Serial'.
+class SSerial a where sseries :: SSeries a
+
+instance SSerial () where sseries = sdecDepth $ pure ()
+
+instance SSerial a => SSerial (Tup1 a) where sseries = sdecDepth $ MkTup1 <$> sseries
+
+instance (SSerial a,SSerial b) => SSerial (a,b) where
+  sseries = sdecDepth $ (,) <$> sseries <~> sseries
+
+instance (SSerial a,SSerial b,SSerial c) => SSerial (a,b,c) where
+  sseries = sdecDepth $ (,,) <$> sseries <~> sseries <~> sseries
+
+instance (SSerial a,SSerial b,SSerial c,SSerial d) => SSerial (a,b,c,d) where
+  sseries = sdecDepth $ (,,,) <$> sseries <~> sseries <~> sseries <~> sseries
+
+instance SSerial a => SSerial (s :@ a) where
+  sseries = dub mkLabel <$> sseries   -- newtypes don't have depth
+
+instance (SSerial a,SSerial b) => SSerial (Pair a b) where
+  sseries = sdecDepth $ MkPair <$> sseries <~> sseries
+
+andM :: Monad m => [m Bool] -> m Bool
+andM = \case
+  [] -> return True
+  m:ms -> m >>= \case
+    True -> andM ms
+    False -> return False
+
+-- | Returns 'True' iff @f@ and @g@ force the same parts of @a@ for all
+-- possible inputs up to the given depth. Although, if @f@ or @g@
+-- throws some exception other than the 'Landmine's this library
+-- creates, this function returns 'False'.
+sameStrictness :: SSerial a => (a -> b) -> (a -> c) -> Int -> IO Bool
+sameStrictness f g depth = andM $ map test xs
+  where
+  xs = flip evalState 0 $ listM depth sseries
+  test x = do
+    fx <- try $ evaluate $ f x
+    gx <- try $ evaluate $ g x
+    case (fx,gx) of
+      (Right _,Right _) -> return True
+      (,)
+        (Left (fromException -> Just l))
+        (Left (fromException -> Just r)) -> return $ unLandmine l == unLandmine r
+      _ -> return False
diff --git a/test/Strictness.hs b/test/Strictness.hs
new file mode 100644
--- /dev/null
+++ b/test/Strictness.hs
@@ -0,0 +1,122 @@
+{-# Language BangPatterns #-}
+{-# Language DataKinds #-}
+{-# Language ExplicitForAll #-}
+{-# Language FlexibleContexts #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language OverloadedLabels #-}
+{-# Language PolyKinds #-}
+{-# Language QuasiQuotes #-}
+{-# Language TemplateHaskell #-}
+{-# Language TypeApplications #-}
+{-# Language TypeFamilies #-}
+{-# Language TypeOperators #-}
+{-# Language ViewPatterns #-}
+
+module Strictness (test) where
+
+import           Data.Functor.Compose
+import           Data.Functor.Identity
+import           Test.Hspec
+
+import           Data.Ruin
+import           Data.Ruin.Ancillaries (GiveAllItHas(..),Pair(..),genericBuild,genericBuildNonStrict,genericExtricate1,rupEval,rupNonStrict)
+import           Data.Ruin.Eval (Eval(Done),runEval)
+
+import qualified StrictCheck
+import           StrictnessTypes
+
+sameStrictness :: forall a b c. StrictCheck.SSerial a => (a -> b) -> (a -> c) -> IO ()
+sameStrictness f g = StrictCheck.sameStrictness f g d >>= (`shouldBe` True)
+  where
+  d = 1000   -- this depth is exhausive for our examples here
+
+nonstrict :: forall a b. StrictCheck.SSerial a => (a -> b) -> IO ()
+nonstrict f = sameStrictness f (const ())
+
+cei :: a -> Compose Eval Identity a
+cei = pure
+
+test :: Spec
+test = do
+  describe "Non-strict" $ do
+    it "`Done'" $ do
+      nonstrict @() Done
+
+    it "`extricate1' for singleton records" $ do
+      nonstrict @("s" :@ ()) (extricate1 #s)
+
+    it "`genericBuildNonStrict'" $ do
+      let eta t = ((genericBuildNonStrict . MkGiveAllItHas) `asTypeOf` id) t
+      nonstrict @L eta
+      nonstrict @XY eta
+
+    it "`rup' for ()'" $ do
+      let eta t = (rup `asTypeOf` id) t
+      nonstrict @() eta
+
+    it "`rupNonStrict' for tuples'" $ do
+      let eta t = (rupNonStrict `asTypeOf` id) t
+      nonstrict @() eta
+      nonstrict @(L,R) eta
+      nonstrict @XY eta
+
+    it "`genericBuild' for newtypes" $ do
+      nonstrict @NT ((genericBuild . MkGiveAllItHas) `asTypeOf` cei)
+
+    it "`rupEval' for singleton records'" $ do
+      nonstrict @("s" :@ ()) (rupEval `asTypeOf` pure)
+
+  describe "Only strict enough to ensure the necessary fields exist" $ do
+    it "`genericExtricate1'" $ do
+      sameStrictness (genericExtricate1 #l) $ \MkL{} -> ()
+      sameStrictness (genericExtricate1 #x) $ \MkXY{} -> ()
+      sameStrictness (genericExtricate1 #y) $ \MkXY{} -> ()
+      sameStrictness (genericExtricate1 #nt) $ \MkNT{} -> ()
+      nonstrict @NT (genericExtricate1 #nt)
+
+    describe "`extricate1' for" $ do
+      it "singleton records" $ do
+        nonstrict @("s" :@ ()) (extricate1 #s)
+
+      it "tuples" $ do
+        sameStrictness @(L,R) (extricate1 #l) $ \(MkL{},_) -> ()
+        sameStrictness @(L,R) (extricate1 #r) $ \(_,MkR{}) -> ()
+        sameStrictness @((XY,(L,R)),NT) (extricate1 #r) $ \((_,(_,MkR{})),_) -> ()
+        sameStrictness @(XY,L,R,NT) (extricate1 #r) $ \(_,_,MkR{},_) -> ()
+
+      it "`Pair'" $ do
+        sameStrictness @(Pair L R) (extricate1 #l) $ \(MkPair MkL{} _) -> ()
+        sameStrictness @(Pair L R) (extricate1 #r) $ \(MkPair _ MkR{}) -> ()
+        sameStrictness @(XY `Pair` (L `Pair` R) `Pair` (NT `Pair` R))
+          (extricate1 #r)
+          (\((_ `MkPair` (_ `MkPair` MkR{})) `MkPair` _) -> ())
+
+    it "`genericBuild'" $ do
+      let eta t = ((genericBuild . MkGiveAllItHas) `asTypeOf` cei) t
+      sameStrictness eta $ \MkL{} -> ()
+      sameStrictness eta $ \MkXY{} -> ()
+      sameStrictness eta $ \MkNT{} -> ()
+      nonstrict @NT eta
+
+    it "`rupEval' for non-() tuples" $ do
+      let eta t = (rupEval `asTypeOf` pure) t
+      nonstrict @() eta
+      sameStrictness eta $ \(MkL{},MkR{}) -> ()
+
+  describe "`rna' quasiquoter" $ do
+    it "always has a data constructor" $ do
+      nonstrict (\ ~[rna||] -> ())
+      nonstrict (\ ~[rna|x|] -> () `asTypeOf` x)
+      nonstrict (\ ~[rna|x y|] -> () `asTypeOf` x `asTypeOf` y)
+
+      sameStrictness (\[rna||] -> ()) id
+      sameStrictness (\[rna|x|] -> () `asTypeOf` x) id
+      sameStrictness (\[rna|x y|] -> () `asTypeOf` x `asTypeOf` y) id
+
+    it "is strict in a field if and only if it has a bang annotation" $ do
+      sameStrictness (\(rfrom @XY -> [rna| _@x _@y|]) -> ()) (extricate1 #x)
+      sameStrictness (\(rfrom @XY -> [rna|!_@x _@y|]) -> ()) (runEval . extricate1 #x)
+
+      nonstrict (\(rfrom @L -> ~[rna| _@l|]) -> ())
+      sameStrictness (\(rfrom @L -> [rna| _@l|]) -> ()) (extricate1 #l)
+      sameStrictness (\(rfrom @L -> [rna|!_@l|]) -> ()) (runEval . extricate1 #l)
diff --git a/test/StrictnessTypes.hs b/test/StrictnessTypes.hs
new file mode 100644
--- /dev/null
+++ b/test/StrictnessTypes.hs
@@ -0,0 +1,37 @@
+{-# Language DataKinds #-}
+{-# Language DeriveGeneric #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language TemplateHaskell #-}
+{-# Language UndecidableInstances #-}
+
+module StrictnessTypes (
+  -- everything but the fields
+  L(MkL),
+  R(MkR),
+  XY(MkXY),
+  NT(MkNT),
+  ) where
+
+import           GHC.Generics (Generic)
+import           StrictCheck
+
+import           Data.Ruin
+
+-- | It's crucial that 'L' and 'R' are box types. IE They have a single
+-- constructor that takes one argument and is non-strict. Such types
+-- exercise a corner case for 'genericExtricate' and 'genericBuild',
+-- since the isomorphism of "GHC.Generics" conflates them with
+-- newtypes.
+data L = MkL {l :: ()} deriving (Generic)
+data R = MkR {r :: ()} deriving (Generic)
+data XY = MkXY {x,y :: ()} deriving (Generic)
+newtype NT = MkNT {nt :: ()} deriving (Generic)
+
+instance SSerial L where sseries = sdecDepth $ MkL <$> sseries
+instance SSerial R where sseries = sdecDepth $ MkR <$> sseries
+instance SSerial XY where sseries = sdecDepth $ MkXY <$> sseries <~> sseries
+instance SSerial NT where sseries = MkNT <$> sseries
+
+$(makeRecords [''L,''R,''XY,''NT])
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -0,0 +1,24 @@
+module Main where
+
+import Test.Hspec (hspec)
+
+import MustCompile.ClosedHas ()
+import MustCompile.HRDatabase ()
+import MustCompile.Physics ()
+import MustCompile.PrintAndTime ()
+import MustCompile.RNA ()
+import MustCompile.RSplat ()
+import MustCompile.RSplit ()
+import MustCompile.TH ()
+
+import qualified MustNotCompile
+import qualified Strictness
+import qualified Test.RNA
+import qualified Test.R
+
+main :: IO ()
+main = hspec $ do
+  MustNotCompile.test
+  Strictness.test
+  Test.RNA.test
+  Test.R.test
diff --git a/test/Test/R.hs b/test/Test/R.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/R.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.R (test) where
+
+import GHC.Generics (to,from)
+import Test.Hspec
+
+import Data.Ruin.R
+
+test :: Spec
+test = do
+  describe "Generics" $ do
+    it "supports conversion" $ do
+      let gid = (to . from) `asTypeOf` id
+      let r = oneR #x False `plusR` oneR #y "y"
+      gid r `shouldBe` r
diff --git a/test/Test/RNA.hs b/test/Test/RNA.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/RNA.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.RNA (test) where
+
+import Control.Monad.Writer (Writer,tell)
+import Test.Hspec
+
+import Data.Ruin
+
+import XY
+
+data X = X deriving (Eq,Show)
+
+data Y = Y deriving (Eq,Show)
+
+test :: Spec
+test = do
+  describe "rnaA" $ do
+    it "uses given order for effects" $ do
+      let x =
+              hoid @(Writer String)
+            $ X <$ tell "x"
+      let y = Y <$ tell "y"
+
+      [rnaA|XY x y|] `shouldBe` (     MkXY <$> x <*> y)
+      [rnaA|XY y x|] `shouldBe` (flip MkXY <$> y <*> x)
diff --git a/test/XY.hs b/test/XY.hs
new file mode 100644
--- /dev/null
+++ b/test/XY.hs
@@ -0,0 +1,19 @@
+{-# Language DataKinds #-}
+{-# Language DeriveGeneric #-}
+{-# Language FlexibleContexts #-}
+{-# Language FlexibleInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language TemplateHaskell #-}
+{-# Language UndecidableInstances #-}
+
+module XY (XY(MkXY)) where
+
+import GHC.Generics (Generic)
+
+import Data.Ruin
+
+data XY x y = MkXY {x::x,y::y} deriving (Eq,Generic,Ord,Show)
+
+instance NoWarnUnusedTopBind XY where noWarnUnusedTopBind MkXY{x=_,y=_} = ()
+
+$(makeRecords [''XY])