row-types 0.4.0.0 → 1.0.0.0

raw patch · 17 files changed

+2665/−2043 lines, 17 filesdep +gaugedep −criteriondep ~constraintsPVP ok

version bump matches the API change (PVP)

Dependencies added: gauge

Dependencies removed: criterion

Dependency ranges changed: constraints

API changes (from Hackage documentation)

Files

• CHANGELOG.md +17/−1
• Data/Row.hs +0/−56
• Data/Row/Internal.hs +0/−573
• Data/Row/Records.hs +0/−706
• Data/Row/Switch.hs +0/−45
• Data/Row/Variants.hs +0/−565
• benchmarks/perf/Main.hs +44/−44
• examples/Examples.lhs +18/−13
• row-types.cabal +30/−40
• src/Data/Row.hs +60/−0
• src/Data/Row/Dictionaries.hs +186/−0
• src/Data/Row/Internal.hs +518/−0
• src/Data/Row/Records.hs +837/−0
• src/Data/Row/Switch.hs +65/−0
• src/Data/Row/Variants.hs +761/−0
• src/aeson/Data/Row/Aeson.hs +52/−0
• src/barbies/Data/Row/Barbies.hs +77/−0

@@ -1,3 +1,19 @@+## 1.0.0.0 [2020-09-12]
+This release has many breaking changes, specifically to `metamorph` and some functions related to `Variant`, hence the major version bump to `1.0`.  However, users that only use basic features of records may not notice a difference.
+
+- Removed `metamorph'` and `biMetamorph'` in favor of generalizing `metamorph` over choice of bifunctor.
+- Removed "unsafe" functions (`unsafeRemove` and `unsafeInjectFront` from `Records` and `unsafeMarkVar` and `unsafeInjectFront` from `Variants`).
+- Removed `Switch` class, reimplementing the `switch` function using `BiForall`.
+- Swap the order of the result of calling `trial`, `multiTrial`, and `split`.
+- Added new functions to `Records`: `lazyRemove`, `curryRec`, `(.$)`, `zipTransform`, `zipTransform'`, `traverse`, `traverseMap`, `distribute`, and `coerceRec`.
+- Added new functions to `Variants`: `fromLabelsMap`, `traverse`, `traverseMap`, and `coerceVar`.
+- Added `Dictionaries` module, full of axioms that are helpful for using `metamorph`.  Moved axioms from `Internal` to `Dictionaries` (in some cases, the type variable order has changed).
+- Added `ApSingle` type family as well as `eraseSingle`, `mapSingle`, and `eraseZipSingle` (thanks Jordan Woehr!).
+- Improved error messages.
+
+Note: GHC 8.4 and earlier are no longer officially supported in row-types 1.0.0.0.
+
+
 ## 0.4.0.0 [2020-05-20]
 - Renamed `toNative` to `toNativeGeneral` and `toNativeExact` to `toNative` for records and likewise for `fromNative` for variants.
 - Added a type family `NativeRow` which, when given any generic type that can go through `fromNative`, is equal to the row-type of the resulting record/variant.  Note that `NativeRow` is defined separately (and differently!) for records vs variants, so it is exported at the `Data.Row.Records`/`Variants` level but not at `Data.Row`.
@@ -5,7 +21,7 @@ - Exposed `BiForall` in `Data.Row`, `Data.Row.Records`, and `Data.Row.Variants`
 - (Internal) Rewrote internal `Generic` code to use an associated type family instead of a standalone one.
 
-Note: GHC 8.2 and earlier are no longer supported in row-types 0.4.0.0.
+Note: GHC 8.2 and earlier are no longer officially supported in row-types 0.4.0.0.
 
 ## 0.3.1.0 [2020-01-29]
 - Added "native" classes as exports for `Records` and `Variants` (e.g., `ToNative`, `FromNative`)

@@ -1,56 +0,0 @@------------------------------------------------------------------------------
--- |
--- Module      :  Data.Row
---
--- This module includes a set of common functions for Records and Variants.
--- It includes:
---
--- * Common constructors, destructors, and querying functions
---
--- It specifically excludes:
---
--- * Functions that have the same name for Records and Variants (e.g. 'focus',
---   'update', 'fromLabels', etc.)
---
--- * Common clashes with the standard Prelude or other modules (e.g. 'map',
---   'sequence', 'zip', 'Map', etc.)
---
--- If these particular functions are needed, they should be brought in qualified
--- from one of the Data.Row.*** modules directly.
---
------------------------------------------------------------------------------
-
-
-module Data.Row
-  (
-  -- * Types and constraints
-    Label(..)
-  , KnownSymbol, AllUniqueLabels, WellBehaved
-  , Var, Rec, Row, Empty, type (≈)
-  , HasType, Lacks, type (.\), type (.+)
-  , type (.\/), type (.\\), type (.//)
-  , BiForall, Forall, Switch(..)
-  -- * Record Construction
-  , empty
-  , type (.==), (.==), pattern (:==)
-  -- ** Restriction
-  , type (.-), (.-)
-  -- ** Query
-  , type (.!), (.!)
-  -- ** Union
-  , (.+), Disjoint, pattern (:+)
-  , (.//)
-  -- * Variant construction
-  , pattern IsJust
-  -- ** Expansion
-  , diversify
-  -- ** Destruction
-  , impossible, trial, trial', multiTrial
-  -- * Labels
-  , labels
-  )
-where
-
-import Data.Row.Variants
-import Data.Row.Records
-import Data.Row.Switch

@@ -1,573 +0,0 @@-{-# LANGUAGE CPP #-}
-{-# LANGUAGE UndecidableSuperClasses #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Row.Internal
---
--- This module implements the internals of open records and variants.
---
------------------------------------------------------------------------------
-
-
-module Data.Row.Internal
-  (
-  -- * Rows
-    Row(..)
-  , Label(..)
-  , KnownSymbol
-  , LT(..)
-  , Empty
-  , HideType(..)
-  -- * Row Operations
-  , Extend, Modify, Rename
-  , type (.==), type (.!), type (.-), type (.\\)
-  -- $merges
-  , type (.+), type (.\/), type (.//)
-  -- * Row Constraints
-  , Lacks, type (.\), HasType
-  , Forall(..)
-  , BiForall(..)
-  , BiConstraint
-  , Unconstrained1
-  , Unconstrained2
-  , WellBehaved, AllUniqueLabels
-  , Ap, Zip, Map, Subset, Disjoint
-  -- * Helper functions
-  , Labels, labels, labels'
-  , show'
-  , toKey
-  , type (≈)
-
-  , mapForall
-  , freeForall
-  , uniqueMap
-  , mapHas
-  , IsA(..)
-  , As(..)
-  )
-where
-
-import Data.Constraint
-import Data.Functor.Const
-import Data.Proxy
-import Data.String (IsString (fromString))
-import Data.Text (Text)
-import qualified Data.Text as Text
-import Data.Type.Equality (type (==))
-
-import qualified Unsafe.Coerce as UNSAFE
-
-import GHC.OverloadedLabels
-import GHC.TypeLits
-import qualified GHC.TypeLits as TL
-
-
-
-
-{--------------------------------------------------------------------
-  Rows
---------------------------------------------------------------------}
--- | The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us
---   which symbols are associated with which types.
-newtype Row a = R [LT a]
-  -- ^ A row is a list of symbol-to-type pairs that should always be sorted
-  -- lexically by the symbol.
-  -- The constructor is exported here (because this is an internal module) but
-  -- should not be exported elsewhere.
-
--- | The kind of elements of rows.  Each element is a label and its associated type.
-data LT a = Symbol :-> a
-
-
--- | A label
-data Label (s :: Symbol) = Label
-  deriving (Eq)
-
-instance KnownSymbol s => Show (Label s) where
-  show = symbolVal
-
-instance x ≈ y => IsLabel x (Label y) where
-#if __GLASGOW_HASKELL__ >= 802
-  fromLabel = Label
-#else
-  fromLabel _ = Label
-#endif
-
--- | A helper function for showing labels
-show' :: (IsString s, Show a) => a -> s
-show' = fromString . show
-
--- | A helper function to turn a Label directly into 'Text'.
-toKey :: forall s. KnownSymbol s => Label s -> Text
-toKey = Text.pack . symbolVal
-
--- | Type level version of 'empty'
-type Empty = R '[]
-
--- | Elements stored in a Row type are usually hidden.
-data HideType where
-  HideType :: a -> HideType
-
-
-
-{--------------------------------------------------------------------
-  Row operations
---------------------------------------------------------------------}
-
-infixl 4 .\ {- This comment needed to appease CPP -}
--- | Does the row lack (i.e. it does not have) the specified label?
-type family (r :: Row k) .\ (l :: Symbol) :: Constraint where
-  R r .\ l = LacksR l r r
-
--- | Type level Row extension
-type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k where
-  Extend l a (R x) = R (Inject (l :-> a) x)
-
--- | Type level Row modification
-type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k where
-  Modify l a (R ρ) = R (ModifyR l a ρ)
-
--- | Type level row renaming
-type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k where
-  Rename l l' r = Extend  l' (r .! l) (r .- l)
-
-infixl 5 .!
--- | Type level label fetching
-type family (r :: Row k) .! (t :: Symbol) :: k where
-  R r .! l = Get l r
-
-infixl 6 .-
--- | Type level Row element removal
-type family (r :: Row k) .- (s :: Symbol) :: Row k where
-  R r .- l = R (Remove l r)
-
-infixl 6 .\\ {- This comment needed to appease CPP -}
--- | Type level Row difference.  That is, @l '.\\' r@ is the row remaining after
--- removing any matching elements of @r@ from @l@.
-type family (l :: Row k) .\\ (r :: Row k) :: Row k where
-  R l .\\ R r = R (Diff l r)
-
--- $merges
--- == Various row-type merges
--- The difference between '.+' (read "append"), '.\/' (read "min-join"), and
--- '.\\' (read "const-union") comes down to how duplicates are handled.
--- In '.+', the two given row-types must be entirely unique.  Even the same
--- entry in both row-types is forbidden.  In '.\/', this final restriction is
--- relaxed, allowing two row-types that have no conflicts to be merged in the
--- logical way.  The '.\\' operator is the most liberal, allowing any two row-types
--- to be merged together, and whenever there is a conflict, favoring the left argument.
---
--- As examples of use:
---
--- - '.+' is used when appending two records, assuring that those two records are
---   entirely disjoint.
---
--- - '.\/' is used when diversifying a variant, allowing some extension to the
---   row-type so long as no original types have changed.
---
--- - './/' is used when doing record overwrite, allowing data in a record to
--- totally overwrite what was previously there.
-
-infixl 6 .+
--- | Type level Row append
-type family (l :: Row k) .+ (r :: Row k) :: Row k where
-  R l .+ R r = R (Merge l r)
-
-infixl 6 .\/
--- | The minimum join of the two rows.
-type family (l :: Row k) .\/ (r :: Row k) where
-  R l .\/ R r = R (MinJoinR l r)
-
-infixl 6 .//
--- | The overwriting union, where the left row overwrites the types of the right
--- row where the labels overlap.
-type family (l :: Row k) .// (r :: Row k) where
-  R l .// R r = R (ConstUnionR l r)
-
-
-{--------------------------------------------------------------------
-  Syntactic sugar for record operations
---------------------------------------------------------------------}
--- | Alias for '.\'. It is a class rather than an alias, so that
--- it can be partially applied.
-class Lacks (l :: Symbol) (r :: Row *)
-instance (r .\ l) => Lacks l r
-
-
--- | Alias for @(r .! l) ≈ a@. It is a class rather than an alias, so that
--- it can be partially applied.
-class (r .! l ≈ a) => HasType l a r
-instance (r .! l ≈ a) => HasType l a r
-
--- | A type level way to create a singleton Row.
-infix 7 .==
-type (l :: Symbol) .== (a :: k) = Extend l a Empty
-
-
-{--------------------------------------------------------------------
-  Constrained record operations
---------------------------------------------------------------------}
-
--- | Any structure over a row in which every element is similarly constrained can
---   be metamorphized into another structure over the same row.
-class Forall (r :: Row k) (c :: k -> Constraint) where
-  -- | A metamorphism is an unfold followed by a fold.  This one is for
-  -- product-like row-types (e.g. Rec).
-  metamorph :: forall (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
-               Proxy h
-            -> (f Empty -> g Empty)
-               -- ^ The way to transform the empty element
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> (h τ, f ('R ρ)))
-               -- ^ The unfold
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> h τ -> g ('R ρ) -> g ('R (ℓ :-> τ ': ρ)))
-               -- ^ The fold
-            -> f r  -- ^ The input structure
-            -> g r
-
-  -- | A metamorphism is an unfold followed by a fold.  This one is for
-  -- sum-like row-types (e.g. Var).
-  metamorph' :: forall (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
-               Proxy h
-            -> (f Empty -> g Empty)
-               -- ^ The way to transform the empty element
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> Either (h τ) (f ('R ρ)))
-               -- ^ The unfold
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> Either (h τ) (g ('R ρ)) -> g ('R (ℓ :-> τ ': ρ)))
-               -- ^ The fold
-            -> f r  -- ^ The input structure
-            -> g r
-
--- | This data type is used to for its ability to existentially bind a type
--- variable.  Particularly, it says that for the type 'a', there exists a 't'
--- such that 'a ~ f t' and 'c t' holds.
-data As c f a where
-  As :: forall c f a t. (a ~ f t, c t) => As c f a
-
--- | A class to capture the idea of 'As' so that it can be partially applied in
--- a context.
-class IsA c f a where
-  as :: As c f a
-
-instance c a => IsA c f (f a) where
-  as = As
-
--- | An internal type used by the 'metamorph' in 'mapForall'.
-newtype MapForall c f (r :: Row k) = MapForall { unMapForall :: Dict (Forall (Map f r) (IsA c f)) }
-
--- | This allows us to derive a `Forall (Map f r) ..` from a `Forall r ..`.
-mapForall :: forall f c ρ. Forall ρ c :- Forall (Map f ρ) (IsA c f)
-mapForall = Sub $ unMapForall $ metamorph @_ @ρ @c @(Const ()) @(MapForall c f) @(Const ()) Proxy empty uncons cons $ Const ()
-  where empty :: Const () Empty -> MapForall c f Empty
-        empty _ = MapForall Dict
-
-        uncons :: forall l t r. (KnownSymbol l, c t)
-               => Label l -> Const () ('R (l :-> t ': r)) -> (Const () t, Const () ('R r))
-        uncons _ _ = (Const (), Const ())
-
-        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-             => Label ℓ -> Const () τ -> MapForall c f ('R ρ)
-             -> MapForall c f ('R (ℓ :-> τ ': ρ))
-        cons _ _ (MapForall Dict) = MapForall Dict
-
--- | Map preserves uniqueness of labels.
-uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)
-uniqueMap = Sub $ UNSAFE.unsafeCoerce @(Dict Unconstrained) Dict
-
--- | Allow any 'Forall` over a row-type, be usable for 'Unconstrained1'.
-freeForall :: forall r c. Forall r c :- Forall r Unconstrained1
-freeForall = Sub $ UNSAFE.unsafeCoerce @(Dict (Forall r c)) Dict
-
--- | This allows us to derive `Map f r .! l ≈ f t` from `r .! l ≈ t`
-mapHas :: forall f r l t. (r .! l ≈ t) :- (Map f r .! l ≈ f t)
-mapHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(r .! l ≈ t)
-
-instance Forall (R '[]) c where
-  {-# INLINE metamorph #-}
-  metamorph _ empty _ _ = empty
-  {-# INLINE metamorph' #-}
-  metamorph' _ empty _ _ = empty
-
-instance (KnownSymbol ℓ, c τ, Forall ('R ρ) c) => Forall ('R (ℓ :-> τ ': ρ) :: Row k) c where
-  metamorph :: forall (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
-               Proxy h
-            -> (f Empty -> g Empty)
-               -- ^ The way to transform the empty element
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> (h τ, f ('R ρ)))
-               -- ^ The unfold
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> h τ -> g ('R ρ) -> g ('R (ℓ :-> τ ': ρ)))
-               -- ^ The fold
-            -> f ('R (ℓ :-> τ ': ρ))  -- ^ The input structure
-            -> g ('R (ℓ :-> τ ': ρ))
-  {-# INLINE metamorph #-}
-  metamorph _ empty uncons cons r = cons Label t $ metamorph @_ @('R ρ) @c @_ @_ @h Proxy empty uncons cons r'
-    where (t, r') = uncons Label r
-  metamorph' :: forall (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
-               Proxy h
-            -> (f Empty -> g Empty)
-               -- ^ The way to transform the empty element
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ('R (ℓ :-> τ ': ρ)) -> Either (h τ) (f ('R ρ)))
-               -- ^ The unfold
-            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> Either (h τ) (g ('R ρ)) -> g ('R (ℓ :-> τ ': ρ)))
-               -- ^ The fold
-            -> f ('R (ℓ :-> τ ': ρ))  -- ^ The input structure
-            -> g ('R (ℓ :-> τ ': ρ))
-  {-# INLINE metamorph' #-}
-  metamorph' _ empty uncons cons r = cons Label $ metamorph' @_ @('R ρ) @c @_ @_ @h Proxy empty uncons cons <$> uncons Label r
-
--- | Any structure over two rows in which the elements of each row satisfy some
---   constraints can be metamorphized into another structure over both of the
---   rows.
-class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) where
-  -- | A metamorphism is a fold followed by an unfold.  This one is for
-  -- product-like row-types.
-  biMetamorph :: forall (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
-                        (h :: k1 -> k2 -> *).
-                 Proxy h
-              -> (f Empty Empty -> g Empty Empty)
-              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)
-                  => Label ℓ
-                  -> f ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))
-                  -> (h τ1 τ2, f ('R ρ1) ('R ρ2)))
-              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)
-                  => Label ℓ -> h τ1 τ2 -> g ('R ρ1) ('R ρ2) -> g ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)))
-              -> f r1 r2 -> g r1 r2
-
-  -- | A metamorphism is a fold followed by an unfold.  This one is for
-  -- sum-like row-types.
-  biMetamorph' :: forall (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
-                         (h :: k1 -> k2 -> *).
-                  Proxy h
-               -> (f Empty Empty -> g Empty Empty)
-               -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)
-                   => Label ℓ
-                   -> f ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))
-                   -> Either (h τ1 τ2) (f ('R ρ1) ('R ρ2)))
-               -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)
-                   => Label ℓ -> Either (h τ1 τ2) (g ('R ρ1) ('R ρ2)) -> g ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)))
-               -> f r1 r2 -> g r1 r2
-
-instance BiForall (R '[]) (R '[]) c1 where
-  {-# INLINE biMetamorph #-}
-  biMetamorph _ empty _ _ = empty
-  biMetamorph' _ empty _ _ = empty
-
-instance (KnownSymbol ℓ, c τ1 τ2, BiForall ('R ρ1) ('R ρ2) c)
-      => BiForall ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)) c where
-  {-# INLINE biMetamorph #-}
-  biMetamorph h empty uncons cons r = cons (Label @ℓ) t $ biMetamorph @_ @_ @('R ρ1) @('R ρ2) @c h empty uncons cons r'
-    where (t, r') = uncons (Label @ℓ) r
-  {-# INLINE biMetamorph' #-}
-  biMetamorph' h empty uncons cons r =
-    cons (Label @ℓ) $ biMetamorph' @_ @_ @('R ρ1) @('R ρ2) @c h empty uncons cons <$> uncons (Label @ℓ) r
-
--- | A null constraint
-class Unconstrained
-instance Unconstrained
-
--- | A null constraint of one argument
-class Unconstrained1 a
-instance Unconstrained1 a
-
--- | A null constraint of two arguments
-class Unconstrained2 a b
-instance Unconstrained2 a b
-
--- | A pair of constraints
-class (c1 x, c2 y) => BiConstraint c1 c2 x y
-instance (c1 x, c2 y) => BiConstraint c1 c2 x y
-
--- | The labels in a Row.
-type family Labels (r :: Row a) where
-  Labels (R '[]) = '[]
-  Labels (R (l :-> a ': xs)) = l ': Labels (R xs)
-
--- | Return a list of the labels in a row type.
-labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]
-labels = getConst $ metamorph @_ @ρ @c @(Const ()) @(Const [s]) @(Const ()) Proxy (const $ Const []) doUncons doCons (Const ())
-  where doUncons _ _ = (Const (), Const ())
-        doCons l _ (Const c) = Const $ show' l : c
-
--- | Return a list of the labels in a row type and is specialized to the 'Unconstrained1' constraint.
-labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]
-labels' = labels @ρ @Unconstrained1
-
-
-{--------------------------------------------------------------------
-  Convenient type families and classes
---------------------------------------------------------------------}
-
--- | A convenient way to provide common, easy constraints
-type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)
-
--- | Are all of the labels in this Row unique?
-type family AllUniqueLabels (r :: Row k) :: Constraint where
-  AllUniqueLabels (R r) = AllUniqueLabelsR r
-
-type family AllUniqueLabelsR (r :: [LT k]) :: Constraint where
-  AllUniqueLabelsR '[] = Unconstrained
-  AllUniqueLabelsR '[l :-> a] = Unconstrained
-  AllUniqueLabelsR (l :-> a ': l :-> b ': _) = TypeError
-    (TL.Text "The label " :<>: ShowType l :<>: TL.Text " is not unique."
-    :$$: TL.Text "It is assigned to both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b)
-  AllUniqueLabelsR (l :-> a ': l' :-> b ': r) = AllUniqueLabelsR (l' :-> b ': r)
-
--- | Is the first row a subset of the second?
-type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint where
-  Subset (R r1) (R r2) = SubsetR r1 r2
-
-type family SubsetR (r1 :: [LT k]) (r2 :: [LT k]) :: Constraint where
-  SubsetR '[] _ = Unconstrained
-  SubsetR x '[] = TypeError (TL.Text "One row-type is not a subset of the other."
-        :$$: TL.Text "The first contains the bindings " :<>: ShowType x
-        :<>: TL.Text " while the second does not.")
-  SubsetR (l :-> a ': x) (l :-> a ': y) = SubsetR x y
-  SubsetR (l :-> a ': x) (l :-> b ': y) =
-    TypeError (TL.Text "One row-type is not a subset of the other."
-          :$$: TL.Text "The first assigns the label " :<>: ShowType l :<>: TL.Text " to "
-          :<>: ShowType a :<>: TL.Text " while the second assigns it to " :<>: ShowType b)
-  SubsetR (hl :-> al ': tl) (hr :-> ar ': tr) =
-      Ifte (hl <=.? hr)
-      (TypeError (TL.Text "One row-type is not a subset of the other."
-             :$$: TL.Text "The first assigns the label " :<>: ShowType hl :<>: TL.Text " to "
-             :<>: ShowType al :<>: TL.Text " while the second has no assignment for it."))
-      (SubsetR (hl :-> al ': tl) tr)
-
--- | A type synonym for disjointness.
-type Disjoint l r = ( WellBehaved l
-                    , WellBehaved r
-                    , Subset l (l .+ r)
-                    , Subset r (l .+ r)
-                    , l .+ r .\\ l ≈ r
-                    , l .+ r .\\ r ≈ l)
-
--- | Map a type level function over a Row.
-type family Map (f :: a -> b) (r :: Row a) :: Row b where
-  Map f (R r) = R (MapR f r)
-
-type family MapR (f :: a -> b) (r :: [LT a]) :: [LT b] where
-  MapR f '[] = '[]
-  MapR f (l :-> v ': t) = l :-> f v ': MapR f t
-
--- | Take two rows with the same labels, and apply the type operator from the
--- first row to the type of the second.
-type family Ap (fs :: Row (a -> b)) (r :: Row a) :: Row b where
-  Ap (R fs) (R r) = R (ApR fs r)
-
-type family ApR (fs :: [LT (a -> b)]) (r :: [LT a]) :: [LT b] where
-  ApR '[] '[] = '[]
-  ApR (l :-> f ': tf) (l :-> v ': tv) = l :-> f v ': ApR tf tv
-  ApR _ _ = TypeError (TL.Text "Row types with different label sets cannot be App'd together.")
-
--- | Zips two rows together to create a Row of the pairs.
---   The two rows must have the same set of labels.
-type family Zip (r1 :: Row *) (r2 :: Row *) where
-  Zip (R r1) (R r2) = R (ZipR r1 r2)
-
-type family ZipR (r1 :: [LT *]) (r2 :: [LT *]) where
-  ZipR '[] '[] = '[]
-  ZipR (l :-> t1 ': r1) (l :-> t2 ': r2) =
-    l :-> (t1, t2) ': ZipR r1 r2
-  ZipR (l :-> t1 ': r1) _ = TypeError (TL.Text "Row types with different label sets cannot be zipped"
-                                  :$$: TL.Text "For one, the label " :<>: ShowType l :<>: TL.Text " is not in both lists.")
-  ZipR '[] (l :-> t ': r) = TypeError (TL.Text "Row types with different label sets cannot be zipped"
-                                  :$$: TL.Text "For one, the label " :<>: ShowType l :<>: TL.Text " is not in both lists.")
-
-type family Inject (l :: LT k) (r :: [LT k]) where
-  Inject (l :-> t) '[] = (l :-> t ': '[])
-  Inject (l :-> t) (l :-> t' ': x) = TypeError (TL.Text "Cannot inject a label into a row type that already has that label"
-                                  :$$: TL.Text "The label " :<>: ShowType l :<>: TL.Text " was already assigned the type "
-                                  :<>: ShowType t' :<>: TL.Text " and is now trying to be assigned the type "
-                                  :<>: ShowType t :<>: TL.Text ".")
-  Inject (l :-> t) (l' :-> t' ': x) =
-      Ifte (l <=.? l')
-      (l :-> t   ': l' :-> t' ': x)
-      (l' :-> t' ': Inject (l :-> t)  x)
-
--- | Type level Row modification helper
-type family ModifyR (l :: Symbol) (a :: k) (ρ :: [LT k]) :: [LT k] where
-  ModifyR l a (l :-> a' ': ρ) = l :-> a ': ρ
-  ModifyR l a (l' :-> a' ': ρ) = l' :-> a' ': ModifyR l a ρ
-  ModifyR l a '[] = TypeError (TL.Text "Tried to modify the label " :<>: ShowType l
-                          :<>: TL.Text ", but it does not appear in the row-type.")
-
-type family Ifte (c :: Bool) (t :: k) (f :: k)   where
-  Ifte True  t f = t
-  Ifte False t f = f
-
-type family Get (l :: Symbol) (r :: [LT k]) where
-  Get l '[] = TypeError (TL.Text "No such field: " :<>: ShowType l)
-  Get l (l :-> t ': x) = t
-  Get l (l' :-> t ': x) = Get l x
-
-type family Remove (l :: Symbol) (r :: [LT k]) where
-  Remove l r = RemoveT l r r
-
-type family RemoveT (l :: Symbol) (r :: [LT k]) (r_orig :: [LT k]) where
-  RemoveT l (l :-> t ': x) _ = x
-  RemoveT l (l' :-> t ': x) r = l' :-> t ': RemoveT l x r
-  RemoveT l '[] r = TypeError (TL.Text "Cannot remove a label that does not occur in the row type."
-                          :$$: TL.Text "The label " :<>: ShowType l :<>: TL.Text " is not in "
-                          :<>: ShowType r)
-
-type family LacksR (l :: Symbol) (r :: [LT k]) (r_orig :: [LT k]) :: Constraint where
-  LacksR l '[] _ = Unconstrained
-  LacksR l (l :-> t ': x) r = TypeError (TL.Text "The label " :<>: ShowType l
-                                    :<>: TL.Text " already exists in " :<>: ShowType r)
-  LacksR l (l' :-> _ ': x) r = Ifte (l <=.? l') Unconstrained (LacksR l x r)
-
-
-type family Merge (l :: [LT k]) (r :: [LT k]) where
-  Merge '[] r = r
-  Merge l '[] = l
-  Merge (h :-> a ': tl)   (h :-> a ': tr) =
-    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " (of type "
-          :$$: ShowType a :<>: TL.Text ") has duplicate assignments.")
-  Merge (h :-> a ': tl)   (h :-> b ': tr) =
-    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."
-          :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")
-  Merge (hl :-> al ': tl) (hr :-> ar ': tr) =
-      Ifte (hl <=.? hr)
-      (hl :-> al ': Merge tl (hr :-> ar ': tr))
-      (hr :-> ar ': Merge (hl :-> al ': tl) tr)
-
-type family MinJoinR (l :: [LT k]) (r :: [LT k]) where
-  MinJoinR '[] r = r
-  MinJoinR l '[] = l
-  MinJoinR (h :-> a ': tl)   (h :-> a ': tr) =
-      (h :-> a ': MinJoinR tl tr)
-  MinJoinR (h :-> a ': tl)   (h :-> b ': tr) =
-    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."
-          :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")
-  MinJoinR (hl :-> al ': tl) (hr :-> ar ': tr) =
-      Ifte (CmpSymbol hl hr == 'LT)
-      (hl :-> al ': MinJoinR tl (hr :-> ar ': tr))
-      (hr :-> ar ': MinJoinR (hl :-> al ': tl) tr)
-
-type family ConstUnionR (l :: [LT k]) (r :: [LT k]) where
-  ConstUnionR '[] r = r
-  ConstUnionR l '[] = l
-  ConstUnionR (h :-> a ': tl)   (h :-> b ': tr) =
-      (h :-> a ': ConstUnionR tl tr)
-  ConstUnionR (hl :-> al ': tl) (hr :-> ar ': tr) =
-      Ifte (CmpSymbol hl hr == 'LT)
-      (hl :-> al ': ConstUnionR tl (hr :-> ar ': tr))
-      (hr :-> ar ': ConstUnionR (hl :-> al ': tl) tr)
-
-
--- | Returns the left list with all of the elements from the right list removed.
-type family Diff (l :: [LT k]) (r :: [LT k]) where
-  Diff '[] r = '[]
-  Diff l '[] = l
-  Diff (l :-> al ': tl) (l :-> al ': tr) = Diff tl tr
-  Diff (hl :-> al ': tl) (hr :-> ar ': tr) =
-    Ifte (hl <=.? hr)
-    (hl :-> al ': Diff tl (hr :-> ar ': tr))
-    (Diff (hl :-> al ': tl) tr)
-
--- | There doesn't seem to be a (<=.?) :: Symbol -> Symbol -> Bool,
--- so here it is in terms of other ghc-7.8 type functions
-type a <=.? b = (CmpSymbol a b == 'LT)
-
--- | A lower fixity operator for type equality
-infix 4 ≈
-type a ≈ b = a ~ b

@@ -1,706 +0,0 @@------------------------------------------------------------------------------
--- |
--- Module      :  Data.Row.Records
---
--- This module implements extensible records using closed type famillies.
---
--- See Examples.lhs for examples.
---
--- Lists of (label,type) pairs are kept sorted thereby ensuring
--- that { x = 0, y = 0 } and { y = 0, x = 0 } have the same type.
---
--- In this way we can implement standard type classes such as Show, Eq, Ord and Bounded
--- for open records, given that all the elements of the open record satify the constraint.
---
------------------------------------------------------------------------------
-
-
-module Data.Row.Records
-  (
-  -- * Types and constraints
-    Label(..)
-  , KnownSymbol, AllUniqueLabels, WellBehaved
-  , Rec, Row, Empty, type (≈)
-  -- * Construction
-  , empty
-  , type (.==), (.==), pattern (:==), unSingleton
-  , default', defaultA
-  , fromLabels, fromLabelsA, fromLabelsMapA
-  -- ** Extension
-  , extend, Extend, Lacks, type (.\)
-  -- ** Restriction
-  , type (.-), (.-)
-  , restrict, split
-  -- ** Modification
-  , update, focus, multifocus, Modify, rename, Rename
-  -- * Query
-  , HasType, type (.!), (.!)
-  -- * Combine
-  -- ** Disjoint union
-  , type (.+), (.+), Disjoint, pattern (:+)
-  -- ** Overwrite
-  , type (.//), (.//)
-  -- * Native Conversion
-  -- $native
-  , fromNative, toNative, toNativeGeneral
-  , FromNative, ToNative, ToNativeGeneral
-  , NativeRow
-  -- * Dynamic Conversion
-  , toDynamicMap, fromDynamicMap
-  -- * Row operations
-  -- ** Map
-  , Map, map, map', mapF
-  , transform, transform'
-  -- ** Fold
-  , BiForall, Forall, erase, eraseWithLabels, eraseZip, eraseToHashMap
-  -- ** Zip
-  , Zip, zip
-  -- ** Sequence
-  , sequence, sequence'
-  -- ** Compose
-  -- $compose
-  , compose, uncompose
-  , compose', uncompose'
-  -- ** Labels
-  , labels, labels'
-  -- ** Coerce
-  , coerceRec
-  -- ** UNSAFE operations
-  , unsafeRemove, unsafeInjectFront
-  )
-where
-
-import Prelude hiding (map, sequence, zip)
-
-import Control.DeepSeq (NFData(..), deepseq)
-
-import           Data.Coerce
-import           Data.Constraint              ((\\))
-import           Data.Dynamic
-import           Data.Functor.Compose
-import           Data.Functor.Const
-import           Data.Functor.Identity
-import           Data.Functor.Product
-import           Data.Generics.Product.Fields (HasField(..), HasField'(..))
-import           Data.Hashable
-import           Data.HashMap.Lazy            (HashMap)
-import qualified Data.HashMap.Lazy            as M
-import qualified Data.List                    as L
-import           Data.Monoid                  (Endo(..), appEndo)
-import           Data.Proxy
-import           Data.String                  (IsString)
-import           Data.Text                    (Text)
-
-import qualified GHC.Generics as G
-import           GHC.TypeLits
-
-import Unsafe.Coerce
-
-import Data.Row.Internal
-
-
-{--------------------------------------------------------------------
-  Open records
---------------------------------------------------------------------}
--- | A record with row r.
-newtype Rec (r :: Row *) where
-  OR :: HashMap Text HideType -> Rec r
-
-instance Forall r Show => Show (Rec r) where
-  showsPrec p r =
-    case eraseWithLabels @Show (showsPrec 7) r of
-      [] ->
-        showString "empty"
-      xs ->
-        showParen
-          (p > 6)
-          (appEndo $ foldMap Endo (L.intersperse (showString " .+ ") (L.map binds xs)))
-    where
-      binds (label, value) =
-        showChar '#' .
-        showString label .
-        showString " .== " .
-        value
-
-instance Forall r Eq => Eq (Rec r) where
-  r == r' = and $ eraseZip @Eq (==) r r'
-
-instance (Forall r Eq, Forall r Ord) => Ord (Rec r) where
-  compare m m' = cmp $ eraseZip @Ord compare m m'
-      where cmp l | [] <- l' = EQ
-                  | a : _ <- l' = a
-                  where l' = dropWhile (== EQ) l
-
-instance (Forall r Bounded, AllUniqueLabels r) => Bounded (Rec r) where
-  minBound = default' @Bounded minBound
-  maxBound = default' @Bounded maxBound
-
-instance Forall r NFData => NFData (Rec r) where
-  rnf r = getConst $ metamorph @_ @r @NFData @Rec @(Const ()) @Identity Proxy empty doUncons doCons r
-    where empty = const $ Const ()
-          doUncons l r = (Identity $ r .! l, unsafeRemove l r)
-          doCons _ x r = deepseq x $ deepseq r $ Const ()
-
--- | The empty record
-empty :: Rec Empty
-empty = OR M.empty
-
--- | The singleton record
-infix 7 .==
-(.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a)
-l .== a = extend l a empty
-
--- | A pattern for the singleton record; can be used to both destruct a record
--- when in a pattern position or construct one in an expression position.
-{-# COMPLETE (:==) #-}
-infix 7 :==
-pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a)
-pattern l :== a <- (unSingleton @l @a -> (l, a)) where
-        (:==) l a = l .== a
-
--- | Turns a singleton record into a pair of the label and value.
-unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a)
-unSingleton r = (l, r .! l) where l = Label @l
-
-{--------------------------------------------------------------------
-  Basic record operations
---------------------------------------------------------------------}
-
-
--- | Record extension. The row may already contain the label,
---   in which case the origin value can be obtained after restriction ('.-') with
---   the label.
-extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)
-extend (toKey -> l) a (OR m) = OR $ M.insert l (HideType a) m
-
--- | Update the value associated with the label.
-update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Rec r -> Rec r
-update (toKey -> l) a (OR m) = OR $ M.adjust f l m where f = const (HideType a)
-
--- | Focus on the value associated with the label.
-focus ::
-  ( KnownSymbol l
-  , r' .! l ≈ b
-  , r  .! l ≈ a
-  , r' ~ Modify l b r
-  , r  ~ Modify l a r'
-  , Functor f)
-  => Label l -> (a -> f b) -> Rec r -> f (Rec r')
-focus (toKey -> l) f (OR m) = case m M.! l of
-  HideType x -> OR . flip (M.insert l) m . HideType <$> f (unsafeCoerce x)
-
--- | Focus on a sub-record
-multifocus :: forall u v r f.
-  ( Functor f
-  , Disjoint u r
-  , Disjoint v r)
-  => (Rec u -> f (Rec v)) -> Rec (u .+ r) -> f (Rec (v .+ r))
-multifocus f (u :+ r) = (.+ r) <$> f u
-
--- | Rename a label.
-rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
-rename (toKey -> l) (toKey -> l') (OR m) = OR $ M.insert l' (m M.! l) $ M.delete l m
-
--- | Record selection
-(.!) :: KnownSymbol l => Rec r -> Label l -> r .! l
-OR m .! (toKey -> a) = case m M.! a of
-  HideType x -> unsafeCoerce x
-
-infixl 6 .-
--- | Record restriction. Remove the label l from the record.
-(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l)
--- OR m .- _ = OR m
-OR m .- (toKey -> a) = OR $ M.delete a m
-
--- | Record disjoint union (commutative)
-infixl 6 .+
-(.+) :: Rec l -> Rec r -> Rec (l .+ r)
-OR l .+ OR r = OR $ M.unionWith (error "Impossible") l r
-
--- | Record overwrite.
---
--- The operation @r .// r'@ creates a new record such that:
---
--- - Any label that is in both @r@ and @r'@ is in the resulting record with the
---   type and value given by the fields in @r@,
---
--- - Any label that is only found in @r@ is in the resulting record.
---
--- - Any label that is only found in @r'@ is in the resulting record.
---
--- This can be thought of as @r@ "overwriting" @r'@.
-(.//) :: Rec r -> Rec r' -> Rec (r .// r')
-OR l .// OR r = OR $ M.union l r
-
--- | A pattern version of record union, for use in pattern matching.
-{-# COMPLETE (:+) #-}
-infixl 6 :+
-pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r)
-pattern l :+ r <- (split @l -> (l, r)) where
-        (:+) l r = l .+ r
-
--- | Split a record into two sub-records.
-split :: forall s r. (Forall s Unconstrained1, Subset s r)
-         => Rec r -> (Rec s, Rec (r .\\ s))
-split (OR m) = (OR $ M.intersection m labelMap, OR $ M.difference m labelMap)
-  where labelMap = M.fromList $ L.zip (labels @s @Unconstrained1) (repeat ())
-
--- | Arbitrary record restriction.  Turn a record into a subset of itself.
-restrict :: forall r r'. (Forall r Unconstrained1, Subset r r') => Rec r' -> Rec r
-restrict = fst . split
-
--- | Removes a label from the record but does not remove the underlying value.
---
--- This is faster than regular record removal ('.-') but should only be used when
--- either: the record will never be merged with another record again, or a new
--- value will soon be placed into the record at this label (as in, an 'update'
--- that is split over two commands).
---
--- If the resulting record is then merged (with '.+') with another record that
--- contains a value at that label, an "impossible" error will occur.
-unsafeRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l)
-unsafeRemove _ (OR m) = OR m
-
-
-{--------------------------------------------------------------------
-  Folds and maps
---------------------------------------------------------------------}
--- An easier type synonym for a pair where both elements are the same type.
-type IPair = Product Identity Identity
-
--- Construct an IPair.
-iPair :: τ -> τ -> IPair τ
-iPair = (. Identity) . Pair . Identity
-
--- Destruct an IPair.  Easily used with ViewPatterns.
-unIPair :: IPair τ -> (τ, τ)
-unIPair (Pair (Identity x) (Identity y)) = (x,y)
-
-
--- | A standard fold
-erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b]
-erase f = fmap (snd @String) . eraseWithLabels @c f
-
--- | A fold with labels
-eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s,b)]
-eraseWithLabels f = getConst . metamorph @_ @ρ @c @Rec @(Const [(s,b)]) @Identity Proxy doNil doUncons doCons
-  where doNil _ = Const []
-        doUncons l r = (Identity $ r .! l, unsafeRemove l r)
-        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-               => Label ℓ -> Identity τ -> Const [(s,b)] ('R ρ) -> Const [(s,b)] ('R (ℓ :-> τ ': ρ))
-        doCons l (Identity x) (Const c) = Const $ (show' l, f x) : c
-
--- | A fold over two row type structures at once
-eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
-eraseZip f x y = getConst $ metamorph @_ @ρ @c @(Product Rec Rec) @(Const [b]) @IPair Proxy (const $ Const []) doUncons doCons (Pair x y)
-  where doUncons l (Pair r1 r2) = (iPair a b, Pair r1' r2')
-          where (a, r1') = (r1 .! l, unsafeRemove l r1)
-                (b, r2') = (r2 .! l, unsafeRemove l r2)
-        doCons :: forall ℓ τ ρ. c τ
-               => Label ℓ -> IPair τ -> Const [b] ('R ρ) -> Const [b] ('R (ℓ :-> τ ': ρ))
-        doCons _ (unIPair -> x) (Const c) = Const $ uncurry f x : c
-
--- | Turns a record into a 'HashMap' from values representing the labels to
---   the values of the record.
-eraseToHashMap :: forall c r s b. (IsString s, Eq s, Hashable s, Forall r c) =>
-                  (forall a . c a => a -> b) -> Rec r -> HashMap s b
-eraseToHashMap f r = M.fromList $ eraseWithLabels @c f r
-
--- | RMap is used internally as a type level lambda for defining record maps.
-newtype RMap (f :: * -> *) (ρ :: Row *) = RMap { unRMap :: Rec (Map f ρ) }
-newtype RMap2 (f :: * -> *) (g :: * -> *) (ρ :: Row *) = RMap2 { unRMap2 :: Rec (Map f (Map g ρ)) }
-
--- | A function to map over a record given a constraint.
-map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
-map f = unRMap . metamorph @_ @r @c @Rec @(RMap f) @Identity Proxy doNil doUncons doCons
-  where
-    doNil _ = RMap empty
-    doUncons l r = (Identity $ r .! l, unsafeRemove l r)
-    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-           => Label ℓ -> Identity τ -> RMap f ('R ρ) -> RMap f ('R (ℓ :-> τ ': ρ))
-    doCons l (Identity v) (RMap r) = RMap (unsafeInjectFront l (f v) r)
-
-newtype RFMap (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1) = RFMap { unRFMap :: Rec (Ap ϕ (Map g ρ)) }
-newtype RecAp (ϕ :: Row (k -> *)) (ρ :: Row k) = RecAp (Rec (Ap ϕ ρ))
-newtype App (f :: k -> *) (a :: k) = App (f a)
-
--- | A function to map over a Ap record given constraints.
-mapF :: forall k c g (ϕ :: Row (k -> *)) (ρ :: Row k). BiForall ϕ ρ c
-     => (forall f a. (c f a) => f a -> f (g a))
-     -> Rec (Ap ϕ ρ)
-     -> Rec (Ap ϕ (Map g ρ))
-mapF f = unRFMap . biMetamorph @_ @_ @ϕ @ρ @c @RecAp @(RFMap g) @App Proxy doNil doUncons doCons . RecAp
-  where
-    doNil _ = RFMap empty
-    doUncons l (RecAp r) = (App $ r .! l, RecAp $ unsafeRemove l r)
-    doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2)
-           => Label ℓ -> App τ1 τ2 -> RFMap g ('R ρ1) ('R ρ2) -> RFMap g ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))
-    doCons l (App v) (RFMap r) = RFMap (unsafeInjectFront l (f @τ1 @τ2 v) r)
-
--- | A function to map over a record given no constraint.
-map' :: forall f r. Forall r Unconstrained1 => (forall a. a -> f a) -> Rec r -> Rec (Map f r)
-map' = map @Unconstrained1
-
--- | Lifts a natural transformation over a record.  In other words, it acts as a
--- record transformer to convert a record of @f a@ values to a record of @g a@
--- values.  If no constraint is needed, instantiate the first type argument with
--- 'Unconstrained1' or use 'transform''.
-transform :: forall c r (f :: * -> *) (g :: * -> *). Forall r c => (forall a. c a => f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
-transform f = unRMap . metamorph @_ @r @c @(RMap f) @(RMap g) @f Proxy doNil doUncons doCons . RMap
-  where
-    doNil _ = RMap empty
-    doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)
-    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-           => Label ℓ -> f τ -> RMap g ('R ρ) -> RMap g ('R (ℓ :-> τ ': ρ))
-    doCons l v (RMap r) = RMap (unsafeInjectFront l (f v) r)
-
--- | A version of 'transform' for when there is no constraint.
-transform' :: forall r (f :: * -> *) (g :: * -> *). Forall r Unconstrained1 => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
-transform' = transform @Unconstrained1 @r
-
--- | A version of 'sequence' in which the constraint for 'Forall' can be chosen.
-sequence' :: forall f r c. (Forall r c, Applicative f)
-          => Rec (Map f r) -> f (Rec r)
-sequence' = getCompose . metamorph @_ @r @c @(RMap f) @(Compose f Rec) @f Proxy doNil doUncons doCons . RMap
-  where
-    doNil _ = Compose (pure empty)
-    doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)
-    doCons l fv (Compose fr) = Compose $ unsafeInjectFront l <$> fv <*> fr
-
--- | Applicative sequencing over a record.
-sequence :: forall f r. (Forall r Unconstrained1, Applicative f)
-         => Rec (Map f r) -> f (Rec r)
-sequence = sequence' @_ @_ @Unconstrained1
-
--- $compose
--- We can easily convert between mapping two functors over the types of a row
--- and mapping the composition of the two functors.  The following two functions
--- perform this composition with the gaurantee that:
---
--- >>> compose . uncompose = id
---
--- >>> uncompose . compose = id
-
--- | A version of 'compose' in which the constraint for 'Forall' can be chosen.
-compose' :: forall c (f :: * -> *) (g :: * -> *) (r :: Row *) . Forall r c
-        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
-compose' = unRMap . metamorph @_ @r @c @(RMap2 f g) @(RMap (Compose f g)) @(Compose f g) Proxy doNil doUncons doCons . RMap2
-  where
-    doNil _ = RMap empty
-    doUncons l (RMap2 r) = (Compose $ r .! l, RMap2 $ unsafeRemove l r)
-    doCons l v (RMap r) = RMap $ unsafeInjectFront l v r
-
--- | Convert from a record where two functors have been mapped over the types to
--- one where the composition of the two functors is mapped over the types.
-compose :: forall (f :: * -> *) (g :: * -> *) r . Forall r Unconstrained1
-        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
-compose = compose' @Unconstrained1 @f @g @r
-
--- | A version of 'uncompose' in which the constraint for 'Forall' can be chosen.
-uncompose' :: forall c (f :: * -> *) (g :: * -> *) r . Forall r c
-           => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
-uncompose' = unRMap2 . metamorph @_ @r @c @(RMap (Compose f g)) @(RMap2 f g) @(Compose f g) Proxy doNil doUncons doCons . RMap
-  where
-    doNil _ = RMap2 empty
-    doUncons l (RMap r) = (r .! l, RMap $ unsafeRemove l r)
-    doCons l (Compose v) (RMap2 r) = RMap2 $ unsafeInjectFront l v r
-
--- | Convert from a record where the composition of two functors have been mapped
--- over the types to one where the two functors are mapped individually one at a
--- time over the types.
-uncompose :: forall (f :: * -> *) (g :: * -> *) r . Forall r Unconstrained1
-          => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
-uncompose = uncompose' @Unconstrained1 @f @g @r
-
-
--- | Coerce a record to a coercible representation.  The 'BiForall' in the context
--- indicates that the type of every field in @r1@ can be coerced to the type of
--- the corresponding fields in @r2@.
---
--- Internally, this is implemented just with `unsafeCoerce`, but we provide the
--- following implementation as a proof:
---
--- > newtype ConstR a b = ConstR (Rec a)
--- > newtype FlipConstR a b = FlipConstR { unFlipConstR :: Rec b }
--- > coerceRec = unFlipConstR . biMetamorph @_ @_ @r1 @r2 @Coercible @ConstR @FlipConstR @Const Proxy doNil doUncons doCons . ConstR
--- >   where
--- >     doNil _ = FlipConstR empty
--- >     doUncons l (ConstR r) = (Const (r .! l), ConstR (unsafeRemove l r))
--- >     doCons l (Const v) (FlipConstR r) = FlipConstR $ unsafeInjectFront l (coerce v) r
-coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2
-coerceRec = unsafeCoerce
-
-
--- | RZipPair is used internally as a type level lambda for zipping records.
-newtype RecPair  (ρ1 :: Row *) (ρ2 :: Row *) = RecPair  (Rec ρ1, Rec ρ2)
-newtype RZipPair (ρ1 :: Row *) (ρ2 :: Row *) = RZipPair { unRZipPair :: Rec (Zip ρ1 ρ2) }
-
--- | Zips together two records that have the same set of labels.
-zip :: forall r1 r2. BiForall r1 r2 Unconstrained2 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)
-zip r1 r2 = unRZipPair $ biMetamorph @_ @_ @r1 @r2 @Unconstrained2 @RecPair @RZipPair @(,) Proxy doNil doUncons doCons $ RecPair (r1, r2)
-  where
-    doNil _ = RZipPair empty
-    doUncons l (RecPair (r1, r2)) = ((r1 .! l, r2 .! l), RecPair (unsafeRemove l r1, unsafeRemove l r2))
-    doCons l (v1, v2) (RZipPair r) = RZipPair $ unsafeInjectFront l (v1, v2) r
-
--- | A helper function for unsafely adding an element to the front of a record.
--- This can cause the resulting record to be malformed, for instance, if the record
--- already contains labels that are lexicographically before the given label.
--- Realistically, this function should only be used when writing calls to 'metamorph'.
-unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R (l :-> a ': r))
-unsafeInjectFront (toKey -> a) b (OR m) = OR $ M.insert a (HideType b) m
-{-# INLINE unsafeInjectFront #-}
-
-
-{--------------------------------------------------------------------
-  Record initialization
---------------------------------------------------------------------}
-
--- | Initialize a record with a default value at each label.
-default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ
-default' v = runIdentity $ defaultA @c $ pure v
-
--- | Initialize a record with a default value at each label; works over an 'Applicative'.
-defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
-         => (forall a. c a => f a) -> f (Rec ρ)
-defaultA v = fromLabelsA @c $ pure v
-
--- | Initialize a record, where each value is determined by the given function over
--- the label at that value.
-fromLabels :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ)
-           => (forall l a. (KnownSymbol l, c a) => Label l -> a) -> Rec ρ
-fromLabels f = runIdentity $ fromLabelsA @c $ (pure .) f
-
--- | Initialize a record, where each value is determined by the given function over
--- the label at that value.  This function works over an 'Applicative'.
-fromLabelsA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
-            => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Rec ρ)
-fromLabelsA mk = getCompose $ metamorph @_ @ρ @c @(Const ()) @(Compose f Rec) @(Const ()) Proxy doNil doUncons doCons (Const ())
-  where doNil _ = Compose $ pure empty
-        doUncons _ _ = (Const (), Const ())
-        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-               => Label ℓ -> Const () τ -> Compose f Rec ('R ρ) -> Compose f Rec ('R (ℓ :-> τ ': ρ))
-        doCons l _ (Compose r) = Compose $ unsafeInjectFront l <$> mk l <*> r
-
--- | Initialize a record that is produced by a `Map`.
-fromLabelsMapA :: forall c f g ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
-               => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Rec (Map g ρ))
-fromLabelsMapA f = fromLabelsA @(IsA c g) @f @(Map g ρ) inner
-                \\ mapForall @g @c @ρ
-                \\ uniqueMap @g @ρ
-   where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a
-         inner l = case as @c @g @a of As -> f l
-
-
-{--------------------------------------------------------------------
-  Dynamic compatibility
---------------------------------------------------------------------}
-
--- | Converts a 'Rec' into a 'HashMap' of 'Dynamic's.
-toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic
-toDynamicMap = eraseToHashMap @Typeable @_ @Text @Dynamic toDyn
-
--- | Produces a 'Rec' from a 'HashMap' of 'Dynamic's.
-fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable)
-               => HashMap Text Dynamic -> Maybe (Rec r)
-fromDynamicMap m = fromLabelsA @Typeable
-  $ \ (toKey -> k) -> M.lookup k m >>= fromDynamic
-
-
-{--------------------------------------------------------------------
-  Generic instance
---------------------------------------------------------------------}
-
--- The generic structure we want Recs to have is not the hidden internal one,
--- but rather one that appears as a Haskell record.  Thus, we can't derive
--- Generic automatically.
---
--- The following Generic instance creates a representation of a Rec that is
--- very similar to a native Haskell record except that the tree of pairs (':*:')
--- that it produces will be extremely unbalanced.  I don't think this is a problem.
--- Furthermore, because we don't want Recs to always have a trailing unit on
--- the end, we must have a special case for singleton Recs, which means that
--- we can't use metamorph.
-
-instance GenericRec r => G.Generic (Rec r) where
-  type Rep (Rec r) =
-    G.D1 ('G.MetaData "Rec" "Data.Row.Records" "row-types" 'False)
-      (G.C1 ('G.MetaCons "Rec" 'G.PrefixI 'True)
-        (RepRec r))
-  from = G.M1 . G.M1 . fromRec
-  to = toRec . G.unM1 . G.unM1
-
-class GenericRec r where
-  type RepRec (r :: Row *) :: * -> *
-  fromRec :: Rec r -> RepRec r x
-  toRec   :: RepRec r x -> Rec r
-
-instance GenericRec Empty where
-  type RepRec (R '[]) = G.U1
-  fromRec _ = G.U1
-  toRec _ = empty
-
-instance KnownSymbol name => GenericRec (R '[name :-> t]) where
-  type RepRec (R (name :-> t ': '[])) = G.S1
-    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
-    (G.Rec0 t)
-  fromRec (_ :== a) = G.M1 (G.K1 a)
-  toRec (G.M1 (G.K1 a)) = (Label @name) :== a
-
-instance
-    ( GenericRec (R (name' :-> t' ': r'))
-    , KnownSymbol name
-    ) => GenericRec (R (name :-> t ': (name' :-> t' ': r'))) where
-  type RepRec (R (name :-> t ': (name' :-> t' ': r')))   = (G.S1
-    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
-    (G.Rec0 t)) G.:*: RepRec (R (name' :-> t' ': r'))
-  fromRec r = G.M1 (G.K1 (r .! Label @name)) G.:*: fromRec (unsafeRemove @name Label r)
-  toRec (G.M1 (G.K1 a) G.:*: r) = unsafeInjectFront (Label @name) a (toRec r)
-
-{--------------------------------------------------------------------
-  Native data type compatibility
---------------------------------------------------------------------}
--- ToNative is shamelessly copied from
---   https://www.athiemann.net/2017/07/02/superrecord.html
-
--- $native
--- The 'toNative' and 'fromNative' functions allow one to convert between
--- 'Rec's and regular Haskell data types ("native" types) that have a single constructor and any
--- number of named fields with the same names and types as the 'Rec'.  As expected,
--- they compose to form the identity.  Alternatively, one may use 'toNativeGeneral',
--- which allows fields to be dropped when a record has excess fields compared
--- to the native type.  Because of this, 'toNativeGeneral' requires a type
--- application (although 'fromNative' does not).  The only requirement is that
--- the native Haskell data type be an instance of 'Generic'.
---
--- For example, consider the following simple data type:
---
--- >>> data Person = Person { name :: String, age :: Int} deriving (Generic, Show)
---
--- Then, we have the following:
---
--- >>> toNative @Person $ #name .== "Alice" .+ #age .== 7 .+ #hasDog .== True
--- Person {name = "Alice", age = 7}
--- >>> fromNative $ Person "Bob" 9
--- { age=9, name="Bob" }
-
-type family NativeRow t where
-  NativeRow t = NativeRowG (G.Rep t)
-
-type family NativeRowG t where
-  NativeRowG (G.M1 G.D m cs) = NativeRowG cs
-  NativeRowG (G.M1 G.C m cs) = NativeRowG cs
-  NativeRowG G.U1 = Empty
-  NativeRowG (l G.:*: r) = NativeRowG l .+ NativeRowG r
-  NativeRowG (G.M1 G.S ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) = name .== t
-
-
--- | Conversion helper to turn a Haskell record into a row-types extensible
--- record. Note that the native Haskell type must be an instance of 'Generic'.
-class FromNativeG a where
-  fromNative' :: a x -> Rec (NativeRowG a)
-
-instance FromNativeG cs => FromNativeG (G.D1 m cs) where
-  fromNative' (G.M1 xs) = fromNative' xs
-
-instance FromNativeG cs => FromNativeG (G.C1 m cs) where
-  fromNative' (G.M1 xs) = fromNative' xs
-
-instance FromNativeG G.U1 where
-  fromNative' G.U1 = empty
-
-instance KnownSymbol name => FromNativeG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) where
-  fromNative' (G.M1 (G.K1 x)) =  (Label @name) .== x
-
-instance (FromNativeG l, FromNativeG r) => FromNativeG (l G.:*: r) where
-  fromNative' (x G.:*: y) = fromNative' @l x .+ fromNative' @r y
-
-type FromNative t = (G.Generic t, FromNativeG (G.Rep t))
-
--- | Convert a Haskell record to a row-types Rec.
-fromNative :: FromNative t => t -> Rec (NativeRow t)
-fromNative = fromNative' . G.from
-
-
--- | Conversion helper to bring a record back into a Haskell type. Note that the
--- native Haskell type must be an instance of 'Generic'.
-class ToNativeG a where
-  toNative' :: Rec (NativeRowG a) -> a x
-
-instance ToNativeG cs => ToNativeG (G.D1 m cs) where
-  toNative' xs = G.M1 $ toNative' xs
-
-instance ToNativeG cs => ToNativeG (G.C1 m cs) where
-  toNative' xs = G.M1 $ toNative' xs
-
-instance ToNativeG G.U1 where
-  toNative' _ = G.U1
-
-instance (KnownSymbol name) => ToNativeG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) where
-  toNative' r = G.M1 $ G.K1 $ r .! (Label @name)
-
-instance (ToNativeG l, ToNativeG r, Disjoint (NativeRowG l) (NativeRowG r))
-    => ToNativeG (l G.:*: r) where
-  toNative' r = toNative' r1 G.:*: toNative' r2
-    where
-      (r1 :: Rec (NativeRowG l)) :+ (r2 :: Rec (NativeRowG r)) = r
-
-type ToNative t = (G.Generic t, ToNativeG (G.Rep t))
-
--- | Convert a record to an exactly matching native Haskell type.
-toNative :: ToNative t => Rec (NativeRow t) -> t
-toNative = G.to . toNative'
-
-
-
--- | Conversion helper to bring a record back into a Haskell type. Note that the
--- native Haskell type must be an instance of 'Generic'.
-class ToNativeGeneralG a ρ where
-  toNativeGeneral' :: Rec ρ -> a x
-
-instance ToNativeGeneralG cs ρ => ToNativeGeneralG (G.D1 m cs) ρ where
-  toNativeGeneral' xs = G.M1 $ toNativeGeneral' xs
-
-instance ToNativeGeneralG cs ρ => ToNativeGeneralG (G.C1 m cs) ρ where
-  toNativeGeneral' xs = G.M1 $ toNativeGeneral' xs
-
-instance ToNativeGeneralG G.U1 ρ where
-  toNativeGeneral' _ = G.U1
-
-instance (KnownSymbol name, ρ .! name ≈ t)
-    => ToNativeGeneralG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where
-  toNativeGeneral' r = G.M1 $ G.K1 $ r .! (Label @name)
-
-instance (ToNativeGeneralG l ρ, ToNativeGeneralG r ρ)
-    => ToNativeGeneralG (l G.:*: r) ρ where
-  toNativeGeneral' r = toNativeGeneral' r G.:*: toNativeGeneral' r
-
-type ToNativeGeneral t ρ = (G.Generic t, ToNativeGeneralG (G.Rep t) ρ)
-
--- | Convert a record to a native Haskell type.
-toNativeGeneral :: ToNativeGeneral t ρ => Rec ρ -> t
-toNativeGeneral = G.to . toNativeGeneral'
-
-
-{--------------------------------------------------------------------
-  Generic-lens compatibility
---------------------------------------------------------------------}
-
--- | Every field in a row-types based record has a 'HasField' instance.
-instance {-# OVERLAPPING #-}
-  ( KnownSymbol name
-  , r' .! name ≈ b
-  , r  .! name ≈ a
-  , r' ~ Modify name b r
-  , r  ~ Modify name a r')
-  => HasField name (Rec r) (Rec r') a b where
-  field = focus (Label @name)
-  {-# INLINE field #-}
-
-instance {-# OVERLAPPING #-}
-  ( KnownSymbol name
-  , r .! name ≈ a
-  , r ~ Modify name a r)
-  => HasField' name (Rec r) a where
-  field' = focus (Label @name)
-  {-# INLINE field' #-}

@@ -1,45 +0,0 @@-{-# LANGUAGE FunctionalDependencies #-}
------------------------------------------------------------------------------
--- |
--- Module: Data.Row.Switch
---
--- This module provides the ability to discharge a polymorphic variant using
--- a record that has matching fields.
---
------------------------------------------------------------------------------
-
-
-module Data.Row.Switch
-  (
-    Switch(..)
-  )
-where
-
-import Data.Row.Internal
-import Data.Row.Records
-import Data.Row.Variants
-
-
-
--- | A 'Var' and a 'Rec' can combine if their rows line up properly.
-class Switch (v :: Row *) (r :: Row *) x | v x -> r, r x -> v where
-  {-# MINIMAL switch | caseon #-}
-  -- | Given a Variant and a Record of functions from each possible value
-  -- of the variant to a single output type, apply the correct
-  -- function to the value in the variant.
-  switch :: Var v -> Rec r -> x
-  switch = flip caseon
-  -- | The same as @switch@ but with the argument order reversed
-  caseon :: Rec r -> Var v -> x
-  caseon = flip switch
-
-
-instance Switch (R '[]) (R '[]) x where
-  switch = const . impossible
-
-instance (KnownSymbol l, Switch (R v) (R r) b)
-      => Switch (R (l :-> a ': v)) (R (l :-> (a -> b) ': r)) b where
-  switch v r = case trial v l of
-    Left x  -> (r .! l) x
-    Right v -> switch v (unsafeRemove l r)
-    where l = Label @l

@@ -1,565 +0,0 @@------------------------------------------------------------------------------
--- |
--- Module      :  Data.Row.Variants
---
--- This module implements extensible variants using closed type families.
---
------------------------------------------------------------------------------
-
-
-module Data.Row.Variants
-  (
-  -- * Types and constraints
-    Label(..)
-  , KnownSymbol, AllUniqueLabels, WellBehaved
-  , Var, Row, Empty, type (≈)
-  -- * Construction
-  , HasType, pattern IsJust, singleton, unSingleton
-  , fromLabels
-  -- ** Extension
-  , type (.\), Lacks, type (.\/), diversify, type (.+)
-  -- ** Modification
-  , update, focus, Modify, rename, Rename
-  -- * Destruction
-  , impossible, trial, trial', multiTrial, view
-  , restrict, split
-  -- ** Types for destruction
-  , type (.!), type (.-), type (.\\), type (.==)
-  -- * Native Conversion
-  -- $native
-  , toNative, fromNative, fromNativeGeneral
-  , ToNative, FromNative, FromNativeGeneral
-  , NativeRow
-  -- * Row operations
-  -- ** Map
-  , Map, map, map', transform, transform'
-  -- ** Fold
-  , Forall, erase, eraseWithLabels, eraseZip
-  -- ** Sequence
-  , sequence
-  -- ** Compose
-  -- $compose
-  , compose, uncompose
-  -- ** labels
-  , labels
-  -- ** Coerce
-  , coerceVar
-  -- ** UNSAFE operations
-  , unsafeMakeVar, unsafeInjectFront
-  )
-where
-
-import Prelude hiding (map, sequence, zip)
-
-import Control.Applicative
-import Control.Arrow       ((+++), left, right)
-import Control.DeepSeq     (NFData(..), deepseq)
-
-import Data.Coerce
-import Data.Functor.Compose
-import Data.Functor.Identity
-import Data.Functor.Product
-import Data.Generics.Sum.Constructors (AsConstructor(..), AsConstructor'(..))
-import Data.Maybe                     (fromMaybe)
-import Data.Profunctor                (Choice(..), Profunctor(..))
-import Data.Proxy
-import Data.String                    (IsString)
-import Data.Text                      (Text)
-
-import qualified GHC.Generics as G
-import           GHC.TypeLits
-
-import Unsafe.Coerce
-
-import Data.Row.Internal
-
-{--------------------------------------------------------------------
-  Polymorphic Variants
---------------------------------------------------------------------}
-
--- | The variant type.
-data Var (r :: Row *) where
-  OneOf :: Text -> HideType -> Var r
-
-instance Forall r Show => Show (Var r) where
-  show v = (\ (x, y) -> "{" ++ x ++ "=" ++ y ++ "}") $ eraseWithLabels @Show show v
-
-instance Forall r Eq => Eq (Var r) where
-  r == r' = fromMaybe False $ eraseZip @Eq (==) r r'
-
-instance (Forall r Eq, Forall r Ord) => Ord (Var r) where
-  compare :: Var r -> Var r -> Ordering
-  compare x y = getConst $ metamorph' @_ @r @Ord @(Product Var Var) @(Const Ordering) @(Const Ordering) Proxy doNil doUncons doCons (Pair x y)
-    where doNil (Pair x _) = impossible x
-          doUncons l (Pair r1 r2) = case (trial r1 l, trial r2 l) of
-            (Left a,  Left b)  -> Left $ Const $ compare a b
-            (Left _,  Right _) -> Left $ Const LT
-            (Right _, Left _)  -> Left $ Const GT
-            (Right x, Right y) -> Right $ Pair x y
-          doCons _ (Left (Const c)) = Const c
-          doCons _ (Right (Const c)) = Const c
-
-instance Forall r NFData => NFData (Var r) where
-  rnf r = getConst $ metamorph' @_ @r @NFData @Var @(Const ()) @Identity Proxy empty doUncons doCons r
-    where empty = const $ Const ()
-          doUncons l = left Identity . flip trial l
-          doCons _ x = deepseq x $ Const ()
-
-
-{--------------------------------------------------------------------
-  Basic Operations
---------------------------------------------------------------------}
-
--- | An unsafe way to make a Variant.  This function does not guarantee that
--- the labels are all unique.
-unsafeMakeVar :: forall r l. KnownSymbol l => Label l -> r .! l -> Var r
-unsafeMakeVar (toKey -> l) = OneOf l . HideType
-
--- | A Variant with no options is uninhabited.
-impossible :: Var Empty -> a
-impossible _ = error "Impossible! Somehow, a variant of nothing was produced."
-
--- | A quick constructor to create a singleton variant.
-singleton :: KnownSymbol l => Label l -> a -> Var (l .== a)
-singleton = IsJust
-
--- | A quick destructor for singleton variants.
-unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a)
-unSingleton (OneOf _ (HideType x)) = (l, unsafeCoerce x) where l = Label @l
-
--- | A pattern for variants; can be used to both destruct a variant
--- when in a pattern position or construct one in an expression position.
-pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> r .! l -> Var r
-pattern IsJust l a <- (isJustHelper @l -> (l, Just a)) where
-        IsJust l a = unsafeMakeVar l a
-
-isJustHelper :: forall l r. KnownSymbol l => Var r -> (Label l, Maybe (r .! l))
-isJustHelper v = (l, view l v) where l = Label @l
-
--- | Make the variant arbitrarily more diverse.
-diversify :: forall r' r. Var r -> Var (r .\/ r')
-diversify = unsafeCoerce -- (OneOf l x) = OneOf l x
-
--- | If the variant exists at the given label, update it to the given value.
--- Otherwise, do nothing.
-update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Var r -> Var r
-update (toKey -> l') a (OneOf l x) = OneOf l $ if l == l' then HideType a else x
-
--- | If the variant exists at the given label, focus on the value associated with it.
--- Otherwise, do nothing.
-focus :: forall l r r' a b p f.
-  ( AllUniqueLabels r
-  , AllUniqueLabels r'
-  , KnownSymbol l
-  , r  .! l ≈ a
-  , r' .! l ≈ b
-  , r' ≈ (r .- l) .\/ (l .== b)
-  , Applicative f
-  , Choice p
-  ) => Label l -> p a (f b) -> p (Var r) (f (Var r'))
-focus (toKey -> l) =
-  dimap unwrap rewrap . left'
-  where
-    unwrap :: Var r -> Either a (Var r')
-    unwrap (OneOf l' (HideType x))
-      | l == l'   = Left (unsafeCoerce x)
-      | otherwise = Right (OneOf l' (HideType x))
-    rewrap :: Either (f b) (Var r') -> f (Var r')
-    rewrap = either (fmap $ OneOf l . HideType) pure
-
--- | Rename the given label.
-rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r)
-rename (toKey -> l1) (toKey -> l2) (OneOf l x) = OneOf (if l == l1 then l2 else l) x
-
--- | Convert a variant into either the value at the given label or a variant without
--- that label.  This is the basic variant destructor.
-trial :: KnownSymbol l => Var r -> Label l -> Either (r .! l) (Var (r .- l))
-trial (OneOf l (HideType x)) (toKey -> l') = if l == l' then Left (unsafeCoerce x) else Right (OneOf l (HideType x))
-
--- | A version of 'trial' that ignores the leftover variant.
-trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l)
-trial' = (either Just (const Nothing) .) . trial
-
--- | A trial over multiple types
-multiTrial :: forall x y. (AllUniqueLabels x, Forall (y .\\ x) Unconstrained1) => Var y -> Either (Var x) (Var (y .\\ x))
-multiTrial (OneOf l x) = if l `elem` labels @(y .\\ x) @Unconstrained1 then Right (OneOf l x) else Left (OneOf l x)
-
--- | A convenient function for using view patterns when dispatching variants.
---   For example:
---
--- @
--- myShow :: Var ("y" '::= String :| "x" '::= Int :| Empty) -> String
--- myShow (view x -> Just n) = "Int of "++show n
--- myShow (view y -> Just s) = "String of "++s @
-view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)
-view = flip trial'
-
--- | Split a variant into two sub-variants.
-split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var s) (Var (r .\\ s))
-split (OneOf l a) | l `elem` labels @s @Unconstrained1 = Left  $ OneOf l a
-                  | otherwise                          = Right $ OneOf l a
-
--- | Arbitrary variant restriction.  Turn a variant into a subset of itself.
-restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r)
-restrict = either Just (pure Nothing) . split
-
-
-{--------------------------------------------------------------------
-  Folds and maps
---------------------------------------------------------------------}
-
--- | A standard fold
-erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b
-erase f = snd @String . eraseWithLabels @c f
-
--- | A fold with labels
-eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s,b)
-eraseWithLabels f = getConst . metamorph' @_ @ρ @c @Var @(Const (s,b)) @Identity Proxy impossible doUncons doCons
-  where doUncons l = left Identity . flip trial l
-        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-               => Label ℓ -> Either (Identity τ) (Const (s,b) ('R ρ)) -> Const (s,b) ('R (ℓ :-> τ ': ρ))
-        doCons l (Left (Identity x)) = Const (show' l, f x)
-        doCons _ (Right (Const c)) = Const c
-
--- | A fold over two row type structures at once
-eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b
-eraseZip f x y = getConst $ metamorph' @_ @ρ @c @(Product Var Var) @(Const (Maybe b)) @(Const (Maybe b)) Proxy doNil doUncons doCons (Pair x y)
-  where doNil _ = Const Nothing
-        doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-                 => Label ℓ -> Product Var Var ('R (ℓ :-> τ ': ρ)) -> Either (Const (Maybe b) τ) (Product Var Var ('R ρ))
-        doUncons l (Pair r1 r2) = case (trial r1 l, trial r2 l) of
-          (Left a,  Left b)  -> Left $ Const $ Just $ f a b
-          (Right x, Right y) -> Right $ Pair x y
-          _ -> Left $ Const Nothing
-        doCons _ (Left  (Const c)) = Const c
-        doCons _ (Right (Const c)) = Const c
-
-
--- | VMap is used internally as a type level lambda for defining variant maps.
-newtype VMap (f :: * -> *) (ρ :: Row *) = VMap { unVMap :: Var (Map f ρ) }
-newtype VMap2 (f :: * -> *) (g :: * -> *) (ρ :: Row *) = VMap2 { unVMap2 :: Var (Map f (Map g ρ)) }
-
--- | A function to map over a variant given a constraint.
-map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Var r -> Var (Map f r)
-map f = unVMap . metamorph' @_ @r @c @Var @(VMap f) @Identity Proxy doNil doUncons doCons
-  where
-    doNil = impossible
-    doUncons l = left Identity . flip trial l
-    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-           => Label ℓ -> Either (Identity τ) (VMap f ('R ρ)) -> VMap f ('R (ℓ :-> τ ': ρ))
-    doCons l (Left (Identity x)) = VMap $ unsafeMakeVar l $ f x
-    doCons _ (Right (VMap v)) = VMap $ unsafeInjectFront v
-
--- | A function to map over a variant given no constraint.
-map' :: forall f r. Forall r Unconstrained1 => (forall a. a -> f a) -> Var r -> Var (Map f r)
-map' = map @Unconstrained1
-
--- | Lifts a natrual transformation over a variant.  In other words, it acts as a
--- variant transformer to convert a variant of @f a@ values to a variant of @g a@
--- values.  If no constraint is needed, instantiate the first type argument with
--- 'Unconstrained1'.
-transform :: forall r c (f :: * -> *) (g :: * -> *). Forall r c => (forall a. c a => f a -> g a) -> Var (Map f r) -> Var (Map g r)
-transform f = unVMap . metamorph' @_ @r @c @(VMap f) @(VMap g) @f Proxy doNil doUncons doCons . VMap
-  where
-    doNil = impossible . unVMap
-    doUncons l = right VMap . flip trial l . unVMap
-    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-           => Label ℓ -> Either (f τ) (VMap g ('R ρ)) -> VMap g ('R (ℓ :-> τ ': ρ))
-    doCons l (Left x) = VMap $ unsafeMakeVar l $ f x
-    doCons _ (Right (VMap v)) = VMap $ unsafeInjectFront v
-
--- | A form of @transformC@ that doesn't have a constraint on @a@
-transform' :: forall r (f :: * -> *) (g :: * -> *) . Forall r Unconstrained1 => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r)
-transform' = transform @r @Unconstrained1
-
--- | Applicative sequencing over a variant
-sequence :: forall f r. (Forall r Unconstrained1, Applicative f) => Var (Map f r) -> f (Var r)
-sequence = getCompose . metamorph' @_ @r @Unconstrained1 @(VMap f) @(Compose f Var) @f Proxy doNil doUncons doCons . VMap
-  where
-    doNil = impossible . unVMap
-    doUncons l = right VMap . flip trial l . unVMap
-    doCons l (Left fx) = Compose $ unsafeMakeVar l <$> fx
-    doCons _ (Right (Compose v)) = Compose $ unsafeInjectFront <$> v
-
--- $compose
--- We can easily convert between mapping two functors over the types of a row
--- and mapping the composition of the two functors.  The following two functions
--- perform this composition with the gaurantee that:
---
--- >>> compose . uncompose = id
---
--- >>> uncompose . compose = id
-
--- | Convert from a variant where two functors have been mapped over the types to
--- one where the composition of the two functors is mapped over the types.
-compose :: forall (f :: * -> *) (g :: * -> *) r . Forall r Unconstrained1 => Var (Map f (Map g r)) -> Var (Map (Compose f g) r)
-compose = unVMap . metamorph' @_ @r @Unconstrained1 @(VMap2 f g) @(VMap (Compose f g)) Proxy doNil doUncons doCons . VMap2
-  where
-    doNil = impossible . unVMap2
-    doUncons l = (Compose +++ VMap2) . flip trial l . unVMap2
-    doCons l (Left x) = VMap $ unsafeMakeVar l x
-    doCons _ (Right (VMap v)) = VMap $ unsafeInjectFront v
-
--- | Convert from a variant where the composition of two functors have been mapped
--- over the types to one where the two functors are mapped individually one at a
--- time over the types.
-uncompose :: forall (f :: * -> *) (g :: * -> *) r . Forall r Unconstrained1 => Var (Map (Compose f g) r) -> Var (Map f (Map g r))
-uncompose = unVMap2 . metamorph' @_ @r @Unconstrained1 @(VMap (Compose f g)) @(VMap2 f g) Proxy doNil doUncons doCons . VMap
-  where
-    doNil = impossible . unVMap
-    doUncons l = right VMap . flip trial l . unVMap
-    doCons l (Left (Compose x)) = VMap2 $ unsafeMakeVar l x
-    doCons _ (Right (VMap2 v)) = VMap2 $ unsafeInjectFront v
-
-
--- | Coerce a variant to a coercible representation.  The 'BiForall' in the context
--- indicates that the type of any option in @r1@ can be coerced to the type of
--- the corresponding option in @r2@.
---
--- Internally, this is implemented just with `unsafeCoerce`, but we provide the
--- following implementation as a proof:
---
--- > newtype ConstR a b = ConstR { unConstR :: Var a }
--- > newtype FlipConstR a b = FlipConstR { unFlipConstR :: Var b }
--- > coerceVar = unFlipConstR . biMetamorph' @_ @_ @r1 @r2 @Coercible @ConstR @FlipConstR @Const Proxy doNil doUncons doCons . ConstR
--- >   where
--- >     doNil = impossible . unConstR
--- >     doUncons l = (Const +++ ConstR) . flip trial l . unConstR
--- >     doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2)
--- >            => Label ℓ -> Either (Const τ1 τ2) (FlipConstR ('R ρ1) ('R ρ2))
--- >            -> FlipConstR ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2))
--- >     doCons l (Left (Const x)) = FlipConstR $ unsafeMakeVar l (coerce @τ1 @τ2 x)
--- >     doCons _ (Right (FlipConstR v)) = FlipConstR $ unsafeInjectFront v
-coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
-coerceVar = unsafeCoerce
-
-{--------------------------------------------------------------------
-  Variant initialization
---------------------------------------------------------------------}
-
--- | A helper function for unsafely adding an element to the front of a variant.
--- This can cause the type of the resulting variant to be malformed, for instance,
--- if the variant already contains labels that are lexicographically before the
--- given label.  Realistically, this function should only be used when writing
--- calls to 'metamorph'.
-unsafeInjectFront :: forall l a r. KnownSymbol l => Var (R r) -> Var (R (l :-> a ': r))
-unsafeInjectFront = unsafeCoerce
-
--- | Initialize a variant from a producer function that accepts labels.  If this
--- function returns more than one possibility, then one is chosen arbitrarily to
--- be the value in the variant.
-fromLabels :: forall c ρ f. (Alternative f, Forall ρ c, AllUniqueLabels ρ)
-           => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Var ρ)
-fromLabels mk = getCompose $ metamorph' @_ @ρ @c @(Const ()) @(Compose f Var) @(Const ())
-                                        Proxy doNil doUncons doCons (Const ())
-  where doNil _ = Compose $ empty
-        doUncons _ _ = Right $ Const ()
-        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
-               => Label ℓ -> Either (Const () τ) (Compose f Var ('R ρ)) -> Compose f Var ('R (ℓ :-> τ ': ρ))
-        doCons l (Left _) = Compose $ unsafeMakeVar l <$> mk l --This case should be impossible
-        doCons l (Right (Compose v)) = Compose $
-          unsafeMakeVar l <$> mk l <|> unsafeInjectFront <$> v
-
-{--------------------------------------------------------------------
-  Generic instance
---------------------------------------------------------------------}
-
--- The generic structure we want Vars to have is not the hidden internal one,
--- but rather one that appears as a Haskell sum type.  Thus, we can't derive
--- Generic automatically.
---
--- The following Generic instance creates a representation of a Var that is
--- very similar to a native Haskell sum type except that the tree of possibilities (':+:')
--- that it produces will be extremely unbalanced.  I don't think this is a problem.
--- Furthermore, because we don't want Vars to always have a trailing void option on
--- the end, we must have a special case for singleton Vars, which means that
--- we can't use metamorph.
-
-instance GenericVar r => G.Generic (Var r) where
-  type Rep (Var r) =
-    G.D1 ('G.MetaData "Var" "Data.Row.Variants" "row-types" 'False) (RepVar r)
-  from = G.M1 . fromVar
-  to = toVar . G.unM1
-
-class GenericVar r where
-  type RepVar (r :: Row *) :: * -> *
-  fromVar :: Var r -> RepVar r x
-  toVar   :: RepVar r x -> Var r
-
-instance GenericVar Empty where
-  type RepVar Empty = G.V1
-  fromVar = impossible
-  toVar = \case
-
-instance KnownSymbol name => GenericVar (R '[name :-> t]) where
-  type RepVar (R (name :-> t ': '[])) = G.C1
-    ('G.MetaCons name 'G.PrefixI 'False)
-    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
-          (G.Rec0 t))
-  fromVar (unSingleton -> (_, a)) = G.M1 (G.M1 (G.K1 a))
-  toVar (G.M1 (G.M1 (G.K1 a))) = IsJust (Label @name) a
-
-instance
-    ( GenericVar (R (name' :-> t' ': r'))
-    , KnownSymbol name
-    , AllUniqueLabels (R (name :-> t ': (name' :-> t' ': r')))
-    ) => GenericVar (R (name :-> t ': (name' :-> t' ': r'))) where
-  type RepVar (R (name :-> t ': (name' :-> t' ': r'))) = (G.C1
-    ('G.MetaCons name 'G.PrefixI 'False)
-    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
-          (G.Rec0 t)))  G.:+: RepVar (R (name' :-> t' ': r'))
-  fromVar v = case trial @name v Label of
-    Left a   -> G.L1 (G.M1 (G.M1 (G.K1 a)))
-    Right v' -> G.R1 (fromVar v')
-  toVar (G.L1 (G.M1 (G.M1 (G.K1 a)))) = IsJust (Label @name) a
-  toVar (G.R1 g) = unsafeInjectFront $ toVar g
-
-{--------------------------------------------------------------------
-  Native data type compatibility
---------------------------------------------------------------------}
-
--- $native
--- The 'toNative' and 'fromNative' functions allow one to convert between
--- 'Var's and regular Haskell data types ("native" types) that have the same
--- number of constructors such that each constructor has one field and the same
--- name as one of the options of the 'Var', which has the same type as that field.
--- As expected, they compose to form the identity.  Alternatively, one may use
--- 'fromNativeGeneral', which allows a variant with excess options to  still be
--- transformed to a native type.  Because of this, 'fromNativeGeneral' requires a type
--- application (although 'fromNative' does not).  The only requirement is that
--- the native Haskell data type be an instance of 'Generic'.
---
--- For example, consider the following simple data type:
---
--- >>> data Pet = Dog {age :: Int} | Cat {age :: Int} deriving (Generic, Show)
---
--- Then, we have the following:
---
--- >>> toNative $ IsJust (Label @"Dog") 3 :: Pet
--- Dog {age = 3}
--- >>> V.fromNative $ Dog 3 :: Var ("Dog" .== Int .+ "Cat" .== Int)
--- {Dog=3}
-
-type family NativeRow t where
-  NativeRow t = NativeRowG (G.Rep t)
-
-type family NativeRowG t where
-  NativeRowG (G.M1 G.D m cs) = NativeRowG cs
-  NativeRowG G.V1 = Empty
-  NativeRowG (l G.:+: r) = NativeRowG l .+ NativeRowG r
-  NativeRowG (G.C1 ('G.MetaCons name fixity sels) (G.S1 m (G.Rec0 t))) = name .== t
-
-
--- | Conversion helper to bring a variant back into a Haskell type. Note that the
--- native Haskell type must be an instance of 'Generic'.
-class ToNativeG a where
-  toNative' :: Var (NativeRowG a) -> a x
-
-instance ToNativeG cs => ToNativeG (G.D1 m cs) where
-  toNative' = G.M1 . toNative'
-
-instance ToNativeG G.V1 where
-  toNative' = impossible
-
-instance (KnownSymbol name)
-    => ToNativeG (G.C1 ('G.MetaCons name fixity sels)
-                (G.S1 m (G.Rec0 t))) where
-  toNative' = G.M1 . G.M1 . G.K1 . snd . unSingleton
-
-instance ( ToNativeG l, ToNativeG r, (NativeRowG l .+ NativeRowG r) .\\ NativeRowG l ≈ NativeRowG r
-         , AllUniqueLabels (NativeRowG l), Forall (NativeRowG r) Unconstrained1)
-    => ToNativeG (l G.:+: r) where
-  toNative' v = case multiTrial @(NativeRowG l) @(NativeRowG (l G.:+: r)) v of
-    Left  v' -> G.L1 $ toNative' v'
-    Right v' -> G.R1 $ toNative' v'
-
-type ToNative t = (G.Generic t, ToNativeG (G.Rep t))
-
--- | Convert a variant to a native Haskell type.
-toNative :: ToNative t => Var (NativeRow t) -> t
-toNative = G.to . toNative'
-
-
--- | Conversion helper to turn a Haskell variant into a row-types extensible
--- variant. Note that the native Haskell type must be an instance of 'Generic'.
-class FromNativeG a where
-  fromNative' :: a x -> Var (NativeRowG a)
-
-instance FromNativeG cs => FromNativeG (G.D1 m cs) where
-  fromNative' (G.M1 v) = fromNative' v
-
-instance FromNativeG G.V1 where
-  fromNative' = \ case
-
-instance KnownSymbol name
-    => FromNativeG (G.C1 ('G.MetaCons name fixity sels)
-                       (G.S1 m (G.Rec0 t))) where
-  fromNative' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x
-
-instance (FromNativeG l, FromNativeG r) => FromNativeG (l G.:+: r) where
-  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it
-  -- makes the constraints really hairy.
-  fromNative' (G.L1 x) = unsafeCoerce $ fromNative' @l x
-  fromNative' (G.R1 y) = unsafeCoerce $ fromNative' @r y
-
-type FromNative t = (G.Generic t, FromNativeG (G.Rep t))
-
--- | Convert a Haskell record to a row-types Var.
-fromNative :: FromNative t => t -> Var (NativeRow t)
-fromNative = fromNative' . G.from
-
-
--- | Conversion helper to turn a Haskell variant into a row-types extensible
--- variant. Note that the native Haskell type must be an instance of 'Generic'.
-class FromNativeGeneralG a ρ where
-  fromNativeGeneral' :: a x -> Var ρ
-
-instance FromNativeGeneralG cs ρ => FromNativeGeneralG (G.D1 m cs) ρ where
-  fromNativeGeneral' (G.M1 v) = fromNativeGeneral' v
-
-instance FromNativeGeneralG G.V1 ρ where
-  fromNativeGeneral' = \ case
-
-instance (KnownSymbol name, ρ .! name ≈ t, AllUniqueLabels ρ)
-    => FromNativeGeneralG (G.C1 ('G.MetaCons name fixity sels)
-                  (G.S1 m (G.Rec0 t))) ρ where
-  fromNativeGeneral' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x
-
-instance (FromNativeGeneralG l ρ, FromNativeGeneralG r ρ)
-    => FromNativeGeneralG (l G.:+: r) ρ where
-  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it
-  -- makes the constraints really hairy.
-  fromNativeGeneral' (G.L1 x) = unsafeCoerce $ fromNativeGeneral' @l @ρ x
-  fromNativeGeneral' (G.R1 y) = unsafeCoerce $ fromNativeGeneral' @r @ρ y
-
-type FromNativeGeneral t ρ = (G.Generic t, FromNativeGeneralG (G.Rep t) ρ)
-
--- | Convert a Haskell record to a row-types Var.
-fromNativeGeneral :: FromNativeGeneral t ρ => t -> Var ρ
-fromNativeGeneral = fromNativeGeneral' . G.from
-
-
-{--------------------------------------------------------------------
-  Generic-lens compatibility
---------------------------------------------------------------------}
-
--- | Every possibility of a row-types based variant has an 'AsConstructor' instance.
-instance {-# OVERLAPPING #-}
-  ( AllUniqueLabels r
-  , AllUniqueLabels r'
-  , KnownSymbol name
-  , r  .! name ≈ a
-  , r' .! name ≈ b
-  , r' ≈ (r .- name) .\/ (name .== b))
-  => AsConstructor name (Var r) (Var r') a b where
-  _Ctor = focus (Label @name)
-  {-# INLINE _Ctor #-}
-
-instance {-# OVERLAPPING #-}
-  ( AllUniqueLabels r
-  , KnownSymbol name
-  , r  .! name ≈ a
-  , r ≈ (r .- name) .\/ (name .== a))
-  => AsConstructor' name (Var r) a where
-  _Ctor' = focus (Label @name)
-  {-# INLINE _Ctor' #-}

@@ -1,6 +1,6 @@ module Main (main) where
 
-import Criterion.Main
+import Gauge.Main
 
 import Data.String
 
@@ -20,42 +20,42 @@   .+ "i20" .== a  .+ "i21" .== a  .+ "i22" .== a  .+ "i23"  .== a
   .+ "i30" .== a  .+ "i31" .== a  .+ "i32" .== a  .+ "i33"  .== a
 
-type SixtyFourRecord a =
-     "i0"   .== a .+ "i1"   .== a .+ "i2"   .== a .+ "i3"   .== a
-  .+ "i10"  .== a .+ "i11"  .== a .+ "i12"  .== a .+ "i13"  .== a
-  .+ "i20"  .== a .+ "i21"  .== a .+ "i22"  .== a .+ "i23"  .== a
-  .+ "i30"  .== a .+ "i31"  .== a .+ "i32"  .== a .+ "i33"  .== a
-  .+ "i100" .== a .+ "i101" .== a .+ "i102" .== a .+ "i103" .== a
-  .+ "i110" .== a .+ "i111" .== a .+ "i112" .== a .+ "i113" .== a
-  .+ "i120" .== a .+ "i121" .== a .+ "i122" .== a .+ "i123" .== a
-  .+ "i130" .== a .+ "i131" .== a .+ "i132" .== a .+ "i133" .== a
-  .+ "i200" .== a .+ "i201" .== a .+ "i202" .== a .+ "i203" .== a
-  .+ "i210" .== a .+ "i211" .== a .+ "i212" .== a .+ "i213" .== a
-  .+ "i220" .== a .+ "i221" .== a .+ "i222" .== a .+ "i223" .== a
-  .+ "i230" .== a .+ "i231" .== a .+ "i232" .== a .+ "i233" .== a
-  .+ "i300" .== a .+ "i301" .== a .+ "i302" .== a .+ "i303" .== a
-  .+ "i310" .== a .+ "i311" .== a .+ "i312" .== a .+ "i313" .== a
-  .+ "i320" .== a .+ "i321" .== a .+ "i322" .== a .+ "i323" .== a
-  .+ "i330" .== a .+ "i331" .== a .+ "i332" .== a .+ "i333" .== a
+-- type SixtyFourRecord a =
+--      "i0"   .== a .+ "i1"   .== a .+ "i2"   .== a .+ "i3"   .== a
+--   .+ "i10"  .== a .+ "i11"  .== a .+ "i12"  .== a .+ "i13"  .== a
+--   .+ "i20"  .== a .+ "i21"  .== a .+ "i22"  .== a .+ "i23"  .== a
+--   .+ "i30"  .== a .+ "i31"  .== a .+ "i32"  .== a .+ "i33"  .== a
+--   .+ "i100" .== a .+ "i101" .== a .+ "i102" .== a .+ "i103" .== a
+--   .+ "i110" .== a .+ "i111" .== a .+ "i112" .== a .+ "i113" .== a
+--   .+ "i120" .== a .+ "i121" .== a .+ "i122" .== a .+ "i123" .== a
+--   .+ "i130" .== a .+ "i131" .== a .+ "i132" .== a .+ "i133" .== a
+--   .+ "i200" .== a .+ "i201" .== a .+ "i202" .== a .+ "i203" .== a
+--   .+ "i210" .== a .+ "i211" .== a .+ "i212" .== a .+ "i213" .== a
+--   .+ "i220" .== a .+ "i221" .== a .+ "i222" .== a .+ "i223" .== a
+--   .+ "i230" .== a .+ "i231" .== a .+ "i232" .== a .+ "i233" .== a
+--   .+ "i300" .== a .+ "i301" .== a .+ "i302" .== a .+ "i303" .== a
+--   .+ "i310" .== a .+ "i311" .== a .+ "i312" .== a .+ "i313" .== a
+--   .+ "i320" .== a .+ "i321" .== a .+ "i322" .== a .+ "i323" .== a
+--   .+ "i330" .== a .+ "i331" .== a .+ "i332" .== a .+ "i333" .== a
 
-my64Record :: Rec (SixtyFourRecord Double)
-my64Record =
-     #i0   .== 0 .+ #i1   .== 0 .+ #i2   .== 0 .+ #i3   .== 0
-  .+ #i10  .== 0 .+ #i11  .== 0 .+ #i12  .== 0 .+ #i13  .== 0
-  .+ #i20  .== 0 .+ #i21  .== 0 .+ #i22  .== 0 .+ #i23  .== 0
-  .+ #i30  .== 0 .+ #i31  .== 0 .+ #i32  .== 0 .+ #i33  .== 0
-  .+ #i100 .== 0 .+ #i101 .== 0 .+ #i102 .== 0 .+ #i103 .== 0
-  .+ #i110 .== 0 .+ #i111 .== 0 .+ #i112 .== 0 .+ #i113 .== 0
-  .+ #i120 .== 0 .+ #i121 .== 0 .+ #i122 .== 0 .+ #i123 .== 0
-  .+ #i130 .== 0 .+ #i131 .== 0 .+ #i132 .== 0 .+ #i133 .== 0
-  .+ #i200 .== 0 .+ #i201 .== 0 .+ #i202 .== 0 .+ #i203 .== 0
-  .+ #i210 .== 0 .+ #i211 .== 0 .+ #i212 .== 0 .+ #i213 .== 0
-  .+ #i220 .== 0 .+ #i221 .== 0 .+ #i222 .== 0 .+ #i223 .== 0
-  .+ #i230 .== 0 .+ #i231 .== 0 .+ #i232 .== 0 .+ #i233 .== 0
-  .+ #i300 .== 0 .+ #i301 .== 0 .+ #i302 .== 0 .+ #i303 .== 0
-  .+ #i310 .== 0 .+ #i311 .== 0 .+ #i312 .== 0 .+ #i313 .== 0
-  .+ #i320 .== 0 .+ #i321 .== 0 .+ #i322 .== 0 .+ #i323 .== 0
-  .+ #i330 .== 0 .+ #i331 .== 0 .+ #i332 .== 0 .+ #i333 .== 0
+-- my64Record :: Rec (SixtyFourRecord Double)
+-- my64Record =
+--      #i0   .== 0 .+ #i1   .== 0 .+ #i2   .== 0 .+ #i3   .== 0
+--   .+ #i10  .== 0 .+ #i11  .== 0 .+ #i12  .== 0 .+ #i13  .== 0
+--   .+ #i20  .== 0 .+ #i21  .== 0 .+ #i22  .== 0 .+ #i23  .== 0
+--   .+ #i30  .== 0 .+ #i31  .== 0 .+ #i32  .== 0 .+ #i33  .== 0
+--   .+ #i100 .== 0 .+ #i101 .== 0 .+ #i102 .== 0 .+ #i103 .== 0
+--   .+ #i110 .== 0 .+ #i111 .== 0 .+ #i112 .== 0 .+ #i113 .== 0
+--   .+ #i120 .== 0 .+ #i121 .== 0 .+ #i122 .== 0 .+ #i123 .== 0
+--   .+ #i130 .== 0 .+ #i131 .== 0 .+ #i132 .== 0 .+ #i133 .== 0
+--   .+ #i200 .== 0 .+ #i201 .== 0 .+ #i202 .== 0 .+ #i203 .== 0
+--   .+ #i210 .== 0 .+ #i211 .== 0 .+ #i212 .== 0 .+ #i213 .== 0
+--   .+ #i220 .== 0 .+ #i221 .== 0 .+ #i222 .== 0 .+ #i223 .== 0
+--   .+ #i230 .== 0 .+ #i231 .== 0 .+ #i232 .== 0 .+ #i233 .== 0
+--   .+ #i300 .== 0 .+ #i301 .== 0 .+ #i302 .== 0 .+ #i303 .== 0
+--   .+ #i310 .== 0 .+ #i311 .== 0 .+ #i312 .== 0 .+ #i313 .== 0
+--   .+ #i320 .== 0 .+ #i321 .== 0 .+ #i322 .== 0 .+ #i323 .== 0
+--   .+ #i330 .== 0 .+ #i331 .== 0 .+ #i332 .== 0 .+ #i333 .== 0
 
 main :: IO ()
 main =
@@ -70,9 +70,9 @@         , bench "recordFromLabels 11" $ nf id $ fromLabels @IsString @(ElevenRecord String) (fromString . show)
         , bench "default 16" $ nf id $ default' @Num @(SixteenRecord Double) 0
         , bench "recordFromLabels 16" $ nf id $ fromLabels @IsString @(SixteenRecord String) (fromString . show)
-        , bench "simple 64" $ nf id $ my64Record
-        , bench "default 64" $ nf id $ default' @Num @(SixtyFourRecord Double) 0
-        , bench "recordFromLabels 64" $ nf id $ fromLabels @IsString @(SixtyFourRecord String) (fromString . show)
+        -- , bench "simple 64" $ nf id $ my64Record
+        -- , bench "default 64" $ nf id $ default' @Num @(SixtyFourRecord Double) 0
+        -- , bench "recordFromLabels 64" $ nf id $ fromLabels @IsString @(SixtyFourRecord String) (fromString . show)
         ]
     , bgroup "Record Append"
         [ bench "append 3 3" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== (),   #d .== () .+ #e .== () .+ #f .== ())
@@ -81,15 +81,15 @@         ]
     , bgroup "Record Access"
         [ bench "get 2 of 4" $ nf (.! #i1)     $ default' @Num @(FourRecord Double) 0
-        [ bench "get 7 of 11" $ nf (.! #i1)    $ default' @Num @(ElevenRecord Double) 0
+        , bench "get 7 of 11" $ nf (.! #i1)    $ default' @Num @(ElevenRecord Double) 0
         , bench "get 4 of 16" $ nf (.! #i10)   $ default' @Num @(SixteenRecord Double) 0
         , bench "get 16 of 16" $ nf (.! #i33)  $ default' @Num @(SixteenRecord Double) 0
-        , bench "get 4 of 64" $ nf (.! #i10)   $ default' @Num @(SixtyFourRecord Double) 1
-        , bench "get 45 of 64" $ nf (.! #i230) $ default' @Num @(SixtyFourRecord Double) 2
-        , bench "get 63 of 64" $ nf (.! #i332) $ default' @Num @(SixtyFourRecord Double) 3
+        -- , bench "get 4 of 64" $ nf (.! #i10)   $ default' @Num @(SixtyFourRecord Double) 1
+        -- , bench "get 45 of 64" $ nf (.! #i230) $ default' @Num @(SixtyFourRecord Double) 2
+        -- , bench "get 63 of 64" $ nf (.! #i332) $ default' @Num @(SixtyFourRecord Double) 3
         ]
     , bgroup "Record Metamorphosis"
         [ bench "erase 4"  $ nf (erase @Show show) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()
-        , bench "erase 64" $ nf (erase @Show show) $ my64Record
+        -- , bench "erase 64" $ nf (erase @Show show) $ my64Record
         ]
     ]

@@ -1,6 +1,12 @@-> {-# LANGUAGE OverloadedLabels #-}
+> {-# LANGUAGE AllowAmbiguousTypes #-}
+> {-# LANGUAGE DataKinds #-}
 > {-# LANGUAGE DeriveGeneric #-}
+> {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE OverloadedLabels #-}
 > {-# LANGUAGE PartialTypeSignatures #-}
+> {-# LANGUAGE ScopedTypeVariables #-}
+> {-# LANGUAGE TypeOperators #-}
+> {-# LANGUAGE ViewPatterns #-}
 > module Examples where
 >
 > import Data.Row
@@ -153,8 +159,7 @@ λ> distance (move (named "2D" origin3D) 5 12)
 13.0
 
-Note that if we were using row-types-lens and the lens library, we could write
-move as:
+Or, with lenses, we could write move as:
 
 > moveLensy p dx dy = p & #x %~ (+ dx) & #y %~ (+ dy)
 
@@ -304,16 +309,16 @@ out, and to do that, you must trial it:
 
 λ> trial v #x
-Left 1
+Right 1
 λ> trial v #y
-Right {x=1}
+Left {x=1}
 λ> trial v' #x
-Right {y="Foo"}
+Left {y="Foo"}
 λ> trial v' #y
-Left "Foo"
+Right "Foo"
 
-If trialing at a label l succeeds, then it provides a Left value of the value at l.
-If not, it provides a Right value of the variant with this label removed---since the
+If trialing at a label l succeeds, then it provides a Right value of the value at l.
+If not, it provides a Left value of the variant with this label removed---since the
 trial failed, we now can be sure that the value is not from l.
 
 --------------------------------------------------------------------------------
@@ -409,18 +414,18 @@ λ> :t multiTrial @("x" .== Double .+ "y" .== String) v
 multiTrial @("x" .== Double .+ "y" .== String) v
   :: Either
-       (Var ('R '["x" ':-> Double, "y" ':-> String]))
        (Var ('R '["x" ':-> Integer]))
+       (Var ('R '["x" ':-> Double, "y" ':-> String]))
 λ> multiTrial @("x" .== Double .+ "y" .== String) v
-Right {x=1}
+Left {x=1}
 
 λ> :t multiTrial @("x" .== Double .+ "y" .== String) v'
 multiTrial @("x" .== Double .+ "y" .== String) v'
   :: Either
-       (Var ('R '["x" ':-> Double, "y" ':-> String]))
        (Var ('R '["x" ':-> Integer]))
+       (Var ('R '["x" ':-> Double, "y" ':-> String]))
 λ> multiTrial @("x" .== Double .+ "y" .== String) v'
-Left {y="Foo"}
+Right {y="Foo"}
 
 Thus, multiTrial can be used not only to arbitrarily split apart a variant, but
 also to change unused label associations (in this case, we changed the variant

@@ -1,5 +1,5 @@ Name:                row-types
-Version:             0.4.0.0
+Version:             1.0.0.0
 License:             MIT
 License-file:        LICENSE
 Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck
@@ -7,7 +7,7 @@ homepage:            https://github.com/target/row-types
 Build-Type:          Simple
 Cabal-Version:       >=1.10
-Tested-With:         GHC == 8.4, GHC == 8.6, GHC == 8.8
+Tested-With:         GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.1
 Category:            Data, Data Structures
 Synopsis:	           Open Records and Variants
 Description:
@@ -21,51 +21,41 @@ 
 extra-source-files:
   examples/Examples.lhs
+  src/aeson/Data/Row/Aeson.hs
+  src/barbies/Data/Row/Barbies.hs
   README.md
   CHANGELOG.md
   LICENSE
   NOTICE
 
 Library
-  Build-Depends: base >= 2 && < 5,
-                 constraints,
-                 deepseq >= 1.4,
-                 hashable >= 1.2,
-                 unordered-containers >= 0.2,
-                 generic-lens >= 1.0.0.0,
-                 profunctors >= 5.0,
-                 text
-  Exposed-modules: Data.Row
-                 , Data.Row.Internal
-                 , Data.Row.Records
-                 , Data.Row.Variants
-                 , Data.Row.Switch
+  Build-Depends:
+    base >= 2 && < 5,
+    constraints >= 0.11,
+    deepseq >= 1.4,
+    hashable >= 1.2,
+    unordered-containers >= 0.2,
+    generic-lens >= 1.0.0.0,
+    profunctors >= 5.0,
+    text
+  Exposed-modules:
+      Data.Row
+    , Data.Row.Internal
+    , Data.Row.Dictionaries
+    , Data.Row.Records
+    , Data.Row.Variants
+    , Data.Row.Switch
+  hs-source-dirs:
+    src
   ghc-options: -W
   default-language: Haskell2010
-  default-extensions: AllowAmbiguousTypes,
-              ConstraintKinds,
-              DataKinds,
-              EmptyCase,
-              EmptyDataDecls,
-              FlexibleContexts,
-              FlexibleInstances,
-              GADTs,
-              InstanceSigs,
-              KindSignatures,
-              LambdaCase,
-              MultiParamTypeClasses,
-              OverloadedLabels,
-              PatternGuards,
-              PatternSynonyms,
-              PolyKinds,
-              RankNTypes,
-              ScopedTypeVariables,
-              TypeApplications,
-              TypeFamilies,
-              TypeOperators,
-              TupleSections,
-              ViewPatterns,
-              UndecidableInstances
+  default-extensions:
+      DataKinds
+    , ExplicitForAll
+    , GADTs
+    , OverloadedLabels
+    , TypeApplications
+    , TypeOperators
 
 benchmark perf
   type: exitcode-stdio-1.0
@@ -76,7 +66,7 @@   build-depends: base >= 2 && < 6
                , row-types
                , deepseq >= 1.4
-               , criterion >= 1.1
+               , gauge >= 0.2.0
   default-language: Haskell2010
   default-extensions: AllowAmbiguousTypes,
               DataKinds,

@@ -0,0 +1,60 @@+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeOperators #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row
+--
+-- This module includes a set of common functions for Records and Variants.
+-- It includes:
+--
+-- * Common constructors, destructors, and querying functions
+--
+-- It specifically excludes:
+--
+-- * Functions that have the same name for Records and Variants (e.g. 'focus',
+--   'update', 'fromLabels', etc.)
+--
+-- * Common clashes with the standard Prelude or other modules (e.g. 'map',
+--   'sequence', 'zip', 'Map', etc.)
+--
+-- If these particular functions are needed, they should be brought in qualified
+-- from one of the Data.Row.*** modules directly.
+--
+-----------------------------------------------------------------------------
+
+
+module Data.Row
+  (
+  -- * Types and constraints
+    Label(..)
+  , KnownSymbol, AllUniqueLabels, WellBehaved
+  , Var, Rec, Row, Empty, type (≈)
+  , HasType, Lacks, type (.\), type (.+)
+  , type (.\/), type (.\\), type (.//)
+  , BiForall, Forall, FreeForall, FreeBiForall
+  , switch, caseon
+  -- * Record Construction
+  , empty
+  , type (.==), (.==), pattern (:==)
+  -- ** Restriction
+  , type (.-), (.-)
+  -- ** Query
+  , type (.!), (.!)
+  -- ** Union
+  , (.+), Disjoint, pattern (:+)
+  , (.//)
+  -- * Variant construction
+  , pattern IsJust
+  -- ** Expansion
+  , diversify
+  -- ** Destruction
+  , impossible, trial, trial', multiTrial
+  -- * Labels
+  , labels
+  )
+where
+
+import Data.Row.Dictionaries
+import Data.Row.Variants
+import Data.Row.Records
+import Data.Row.Switch

@@ -0,0 +1,186 @@+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row.Dictionaries
+--
+-- This module exports various dictionaries that help the type-checker when
+-- dealing with row-types.
+--
+-- For the various axioms, type variables are consistently in the following order:
+--
+--  * Any types that do not belong later.
+--
+--  * Labels
+--
+--  * Row-types
+--
+--      * If applicable, the type in the row-type at the given label goes after
+--      each row-type
+--
+--  * Constraints
+-----------------------------------------------------------------------------
+
+
+module Data.Row.Dictionaries
+  ( -- * Axioms
+    uniqueMap, uniqueAp, uniqueApSingle, uniqueZip
+  , extendHas, mapHas, apHas, apSingleHas
+  , mapExtendSwap, apExtendSwap, apSingleExtendSwap, zipExtendSwap
+  , FreeForall
+  , FreeBiForall
+  , freeForall
+  , mapForall
+  , apSingleForall
+  -- ** Helper Types
+  , IsA(..)
+  , As(..)
+  , ActsOn(..)
+  , As'(..)
+  -- * Re-exports
+  , Dict(..), (:-)(..), HasDict(..), (\\), withDict
+  , Unconstrained, Unconstrained1, Unconstrained2
+
+  )
+where
+
+import Data.Constraint
+import Data.Functor.Const
+import Data.Proxy
+import qualified Unsafe.Coerce as UNSAFE
+import GHC.TypeLits
+
+import Data.Row.Internal
+
+
+
+-- | This data type is used to for its ability to existentially bind a type
+-- variable.  Particularly, it says that for the type 'a', there exists a 't'
+-- such that @a ~ f t@ and @c t@ holds.
+data As c f a where
+  As :: forall c f a t. (a ~ f t, c t) => As c f a
+
+-- | A class to capture the idea of 'As' so that it can be partially applied in
+-- a context.
+class IsA c f a where
+  as :: As c f a
+
+instance c a => IsA c f (f a) where
+  as = As
+
+-- | Like 'As', but here we know the underlying value is some 'f' applied to the
+-- given type 'a'.
+data As' c t a where
+  As' :: forall c f a t. (a ~ f t, c f) => As' c t a
+
+-- | A class to capture the idea of 'As'' so that it can be partially applied in
+-- a context.
+class ActsOn c t a where
+  actsOn :: As' c t a
+
+instance c f => ActsOn c t (f t) where
+  actsOn = As'
+
+-- | An internal type used by the 'metamorph' in 'mapForall'.
+newtype MapForall c f (r :: Row k) = MapForall { unMapForall :: Dict (Forall (Map f r) (IsA c f)) }
+
+-- | An internal type used by the 'metamorph' in 'apSingleForall'.
+newtype ApSingleForall c a (fs :: Row (k -> k')) = ApSingleForall
+  { unApSingleForall :: Dict (Forall (ApSingle fs a) (ActsOn c a)) }
+
+-- | This allows us to derive a @Forall (Map f r) ..@ from a @Forall r ..@.
+mapForall :: forall f ρ c. Forall ρ c :- Forall (Map f ρ) (IsA c f)
+mapForall = Sub $ unMapForall $ metamorph @_ @ρ @c @Const @Proxy @(MapForall c f) @Proxy Proxy empty uncons cons $ Proxy
+  where empty _ = MapForall Dict
+        uncons _ _ = Const Proxy
+        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
+             => Label ℓ -> Const (MapForall c f ρ) (Proxy τ)
+             -> MapForall c f (Extend ℓ τ ρ)
+        cons _ (Const (MapForall Dict)) = case frontExtendsDict @ℓ @τ @ρ of
+          FrontExtendsDict Dict -> MapForall Dict
+            \\ mapExtendSwap @f @ℓ @τ @ρ
+            \\ uniqueMap @f @(Extend ℓ τ ρ)
+
+-- | This allows us to derive a @Forall (ApSingle f r) ..@ from a @Forall f ..@.
+apSingleForall :: forall a fs c. Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
+apSingleForall = Sub $ unApSingleForall $ metamorph @_ @fs @c @Const @Proxy @(ApSingleForall c a) @Proxy Proxy empty uncons cons $ Proxy
+  where empty _ = ApSingleForall Dict
+        uncons _ _ = Const Proxy
+        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
+             => Label ℓ -> Const (ApSingleForall c a ρ) (Proxy τ)
+             -> ApSingleForall c a (Extend ℓ τ ρ)
+        cons _ (Const (ApSingleForall Dict)) = case frontExtendsDict @ℓ @τ @ρ of
+          FrontExtendsDict Dict -> ApSingleForall Dict
+            \\ apSingleExtendSwap @a @ℓ @τ @ρ
+            \\ uniqueApSingle @a @(Extend ℓ τ ρ)
+
+-- | Allow any 'Forall' over a row-type, be usable for 'Unconstrained1'.
+freeForall :: forall r c. Forall r c :- Forall r Unconstrained1
+freeForall = Sub $ UNSAFE.unsafeCoerce @(Dict (Forall r c)) Dict
+
+-- | `FreeForall` can be used when a `Forall` constraint is necessary but there
+-- is no particular constraint we care about.
+type FreeForall r = Forall r Unconstrained1
+
+-- | `FreeForall` can be used when a `BiForall` constraint is necessary but
+-- there is no particular constraint we care about.
+type FreeBiForall r1 r2 = BiForall r1 r2 Unconstrained2
+
+-- | If we know that 'r' has been extended with @l .== t@, then we know that this
+-- extension at the label 'l' must be 't'.
+extendHas :: forall l t r. Dict (Extend l t r .! l ≈ t)
+extendHas = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | This allows us to derive @Map f r .! l ≈ f t@ from @r .! l ≈ t@
+mapHas :: forall f l t r. (r .! l ≈ t) :- (Map f r .! l ≈ f t, Map f r .- l ≈ Map f (r .- l))
+mapHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(r .! l ≈ t)
+
+-- | This allows us to derive @Ap ϕ ρ .! l ≈ f t@ from @ϕ .! l ≈ f@ and @ρ .! l ≈ t@
+apHas :: forall l f ϕ t ρ. (ϕ .! l ≈ f, ρ .! l ≈ t) :- (Ap ϕ ρ .! l ≈ f t, Ap ϕ ρ .- l ≈ Ap (ϕ .- l) (ρ .- l))
+apHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(ϕ .! l ≈ f, ρ .! l ≈ t)
+
+-- | This allows us to derive @ApSingle r x .! l ≈ f x@ from @r .! l ≈ f@
+apSingleHas :: forall x l f r. (r .! l ≈ f) :- (ApSingle r x .! l ≈ f x, ApSingle r x .- l ≈ ApSingle (r .- l) x)
+apSingleHas = Sub $ UNSAFE.unsafeCoerce $ Dict @(r .! l ≈ f)
+
+-- | Proof that the 'Map' type family preserves labels and their ordering.
+mapExtendSwap :: forall f ℓ τ r. Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
+mapExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | Proof that the 'Ap' type family preserves labels and their ordering.
+apExtendSwap :: forall ℓ f fs τ r. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
+apExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | Proof that the 'ApSingle' type family preserves labels and their ordering.
+apSingleExtendSwap :: forall τ ℓ f r. Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
+apSingleExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | Proof that the 'Ap' type family preserves labels and their ordering.
+zipExtendSwap :: forall ℓ τ1 r1 τ2 r2. Dict (Extend ℓ (τ1, τ2) (Zip r1 r2) ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
+zipExtendSwap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | Map preserves uniqueness of labels.
+uniqueMap :: forall f r. Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
+uniqueMap = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | Ap preserves uniqueness of labels.
+uniqueAp :: forall fs r. Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
+uniqueAp = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | ApSingle preserves uniqueness of labels.
+uniqueApSingle :: forall x r. Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
+uniqueApSingle = UNSAFE.unsafeCoerce $ Dict @Unconstrained
+
+-- | Zip preserves uniqueness of labels.
+uniqueZip :: forall r1 r2. Dict (AllUniqueLabels (Zip r1 r2) ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
+uniqueZip = UNSAFE.unsafeCoerce $ Dict @Unconstrained

@@ -0,0 +1,518 @@+{-# LANGUAGE CPP #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row.Internal
+--
+-- This module implements the internals of open records and variants.
+--
+-----------------------------------------------------------------------------
+
+
+module Data.Row.Internal
+  (
+  -- * Rows
+    Row(..)
+  , Label(..)
+  , KnownSymbol
+  , LT(..)
+  , Empty
+  , HideType(..)
+  -- * Row Operations
+  , Extend, Modify, Rename
+  , type (.==), type (.!), type (.-), type (.\\)
+  -- $merges
+  , type (.+), type (.\/), type (.//)
+  -- * Row Constraints
+  , Lacks, type (.\), HasType
+  , Forall(..)
+  , BiForall(..)
+  , BiConstraint
+  , Unconstrained
+  , Unconstrained1
+  , Unconstrained2
+  , FrontExtends(..)
+  , FrontExtendsDict(..)
+  , WellBehaved, AllUniqueLabels
+  , Ap, ApSingle, Zip, Map, Subset, Disjoint
+  -- * Helper functions
+  , Labels, labels, labels'
+  , show'
+  , toKey
+  , type (≈)
+  )
+where
+
+import Data.Bifunctor (Bifunctor(..))
+import Data.Constraint
+import Data.Functor.Const
+import Data.Proxy
+import Data.String (IsString (fromString))
+import Data.Text (Text)
+import qualified Data.Text as Text
+import Data.Type.Equality (type (==))
+
+import GHC.OverloadedLabels
+import GHC.TypeLits
+import qualified GHC.TypeLits as TL
+
+
+
+
+{--------------------------------------------------------------------
+  Rows
+--------------------------------------------------------------------}
+-- | The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us
+--   which symbols are associated with which types.
+newtype Row a = R [LT a]
+  -- ^ A row is a list of symbol-to-type pairs that should always be sorted
+  -- lexically by the symbol.
+  -- The constructor is exported here (because this is an internal module) but
+  -- should not be exported elsewhere.
+
+-- | The kind of elements of rows.  Each element is a label and its associated type.
+data LT a = Symbol :-> a
+
+
+-- | A label
+data Label (s :: Symbol) = Label
+  deriving (Eq)
+
+instance KnownSymbol s => Show (Label s) where
+  show = symbolVal
+
+instance x ≈ y => IsLabel x (Label y) where
+#if __GLASGOW_HASKELL__ >= 802
+  fromLabel = Label
+#else
+  fromLabel _ = Label
+#endif
+
+-- | A helper function for showing labels
+show' :: (IsString s, Show a) => a -> s
+show' = fromString . show
+
+-- | A helper function to turn a Label directly into 'Text'.
+toKey :: forall s. KnownSymbol s => Label s -> Text
+toKey = Text.pack . symbolVal
+
+-- | Type level version of 'empty'
+type Empty = R '[]
+
+-- | Elements stored in a Row type are usually hidden.
+data HideType where
+  HideType :: a -> HideType
+
+
+
+{--------------------------------------------------------------------
+  Row operations
+--------------------------------------------------------------------}
+
+infixl 4 .\ {- This comment needed to appease CPP -}
+-- | Does the row lack (i.e. it does not have) the specified label?
+type family (r :: Row k) .\ (l :: Symbol) :: Constraint where
+  R r .\ l = LacksR l r r
+
+-- | Type level Row extension
+type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k where
+  Extend l a (R x) = R (Inject (l :-> a) x)
+
+-- | Type level Row modification
+type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k where
+  Modify l a (R ρ) = R (ModifyR l a ρ)
+
+-- | Type level row renaming
+type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k where
+  Rename l l' r = Extend  l' (r .! l) (r .- l)
+
+infixl 5 .!
+-- | Type level label fetching
+type family (r :: Row k) .! (t :: Symbol) :: k where
+  R r .! l = Get l r
+
+infixl 6 .-
+-- | Type level Row element removal
+type family (r :: Row k) .- (s :: Symbol) :: Row k where
+  R r .- l = R (Remove l r)
+
+infixl 6 .\\ {- This comment needed to appease CPP -}
+-- | Type level Row difference.  That is, @l '.\\' r@ is the row remaining after
+-- removing any matching elements of @r@ from @l@.
+type family (l :: Row k) .\\ (r :: Row k) :: Row k where
+  R l .\\ R r = R (Diff l r)
+
+-- $merges
+-- == Various row-type merges
+-- The difference between '.+' (read "append"), '.\/' (read "min-join"), and
+-- '.\\' (read "const-union") comes down to how duplicates are handled.
+-- In '.+', the two given row-types must be entirely unique.  Even the same
+-- entry in both row-types is forbidden.  In '.\/', this final restriction is
+-- relaxed, allowing two row-types that have no conflicts to be merged in the
+-- logical way.  The '.\\' operator is the most liberal, allowing any two row-types
+-- to be merged together, and whenever there is a conflict, favoring the left argument.
+--
+-- As examples of use:
+--
+-- - '.+' is used when appending two records, assuring that those two records are
+--   entirely disjoint.
+--
+-- - '.\/' is used when diversifying a variant, allowing some extension to the
+--   row-type so long as no original types have changed.
+--
+-- - './/' is used when doing record overwrite, allowing data in a record to
+-- totally overwrite what was previously there.
+
+infixl 6 .+
+-- | Type level Row append
+type family (l :: Row k) .+ (r :: Row k) :: Row k where
+  R l .+ R r = R (Merge l r)
+
+infixl 6 .\/
+-- | The minimum join of the two rows.
+type family (l :: Row k) .\/ (r :: Row k) where
+  R l .\/ R r = R (MinJoinR l r)
+
+infixl 6 .//
+-- | The overwriting union, where the left row overwrites the types of the right
+-- row where the labels overlap.
+type family (l :: Row k) .// (r :: Row k) where
+  R l .// R r = R (ConstUnionR l r)
+
+
+{--------------------------------------------------------------------
+  Syntactic sugar for record operations
+--------------------------------------------------------------------}
+-- | Alias for '.\'. It is a class rather than an alias, so that
+-- it can be partially applied.
+class Lacks (l :: Symbol) (r :: Row *)
+instance (r .\ l) => Lacks l r
+
+
+-- | Alias for @(r .! l) ≈ a@. It is a class rather than an alias, so that
+-- it can be partially applied.
+class (r .! l ≈ a) => HasType l a r
+instance (r .! l ≈ a) => HasType l a r
+
+-- | A type level way to create a singleton Row.
+infix 7 .==
+type (l :: Symbol) .== (a :: k) = Extend l a Empty
+
+
+{--------------------------------------------------------------------
+  Constrained record operations
+--------------------------------------------------------------------}
+
+-- | A dictionary of information that proves that extending a row-type @r@ with
+-- a label @l@ will necessarily put it to the front of the underlying row-type
+-- list.  This is quite internal and should not generally be necessary.
+data FrontExtendsDict l t r = forall ρ. FrontExtendsDict (Dict (r ~ R ρ, R (l :-> t ': ρ) ≈ Extend l t (R ρ), AllUniqueLabelsR (l :-> t ': ρ)))
+
+-- | A class wrapper for 'FrontExtendsDict'.
+class FrontExtends l t r where
+  frontExtendsDict :: FrontExtendsDict l t r
+
+instance (r ~ R ρ, R (l :-> t ': ρ) ≈ Extend l t (R ρ), AllUniqueLabelsR (l :-> t ': ρ)) => FrontExtends l t r where
+  frontExtendsDict = FrontExtendsDict Dict
+
+
+-- | Any structure over a row in which every element is similarly constrained can
+-- be metamorphized into another structure over the same row.
+class Forall (r :: Row k) (c :: k -> Constraint) where
+  -- | A metamorphism is an anamorphism (an unfold) followed by a catamorphism (a fold).
+  -- The parameter 'p' describes the output of the unfold and the input of the fold.
+  -- For records, @p = (,)@, because every entry in the row will unfold to a value paired
+  -- with the rest of the record.
+  -- For variants, @p = Either@, because there will either be a value or future types to
+  -- explore.
+  -- 'Const' can be useful when the types in the row are unnecessary.
+  metamorph :: forall (p :: * -> * -> *) (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *). Bifunctor p
+            => Proxy (Proxy h, Proxy p)
+            -> (f Empty -> g Empty)
+               -- ^ The way to transform the empty element
+            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+               => Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
+               -- ^ The unfold
+            -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
+               => Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
+               -- ^ The fold
+            -> f r  -- ^ The input structure
+            -> g r
+
+instance Forall (R '[]) c where
+  {-# INLINE metamorph #-}
+  metamorph _ empty _ _ = empty
+
+instance (KnownSymbol ℓ, c τ, Forall ('R ρ) c, FrontExtends ℓ τ ('R ρ), AllUniqueLabels (Extend ℓ τ ('R ρ))) => Forall ('R (ℓ :-> τ ': ρ) :: Row k) c where
+  {-# INLINE metamorph #-}
+  metamorph h empty uncons cons = case frontExtendsDict @ℓ @τ @('R ρ) of
+    FrontExtendsDict Dict ->
+      cons (Label @ℓ) . first (metamorph @_ @('R ρ) @c h empty uncons cons) . uncons (Label @ℓ)
+
+
+-- | Any structure over two rows in which the elements of each row satisfy some
+--   constraints can be metamorphized into another structure over both of the
+--   rows.
+class BiForall (r1 :: Row k1) (r2 :: Row k2) (c :: k1 -> k2 -> Constraint) where
+  -- | A metamorphism is an anamorphism (an unfold) followed by a catamorphism (a fold).
+  biMetamorph :: forall (p :: * -> * -> *) (f :: Row k1 -> Row k2 -> *) (g :: Row k1 -> Row k2 -> *)
+                        (h :: k1 -> k2 -> *). Bifunctor p
+              => Proxy (Proxy h, Proxy p)
+              -> (f Empty Empty -> g Empty Empty)
+              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2, HasType ℓ τ1 ρ1, HasType ℓ τ2 ρ2)
+                  => Label ℓ -> f ρ1 ρ2 -> p (f (ρ1 .- ℓ) (ρ2 .- ℓ)) (h τ1 τ2))
+              -> (forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, c τ1 τ2, FrontExtends ℓ τ1 ρ1, FrontExtends ℓ τ2 ρ2, AllUniqueLabels (Extend ℓ τ1 ρ1), AllUniqueLabels (Extend ℓ τ2 ρ2))
+                  => Label ℓ -> p (g ρ1 ρ2) (h τ1 τ2) -> g (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2))
+              -> f r1 r2 -> g r1 r2
+
+
+instance BiForall (R '[]) (R '[]) c1 where
+  {-# INLINE biMetamorph #-}
+  biMetamorph _ empty _ _ = empty
+
+instance (KnownSymbol ℓ, c τ1 τ2, BiForall ('R ρ1) ('R ρ2) c, FrontExtends ℓ τ1 ('R ρ1), FrontExtends ℓ τ2 ('R ρ2), AllUniqueLabels (Extend ℓ τ1 ('R ρ1)), AllUniqueLabels (Extend ℓ τ2 ('R ρ2)))
+      => BiForall ('R (ℓ :-> τ1 ': ρ1)) ('R (ℓ :-> τ2 ': ρ2)) c where
+  {-# INLINE biMetamorph #-}
+  biMetamorph h empty uncons cons = case (frontExtendsDict @ℓ @τ1 @('R ρ1), frontExtendsDict @ℓ @τ2 @('R ρ2)) of
+    (FrontExtendsDict Dict, FrontExtendsDict Dict) ->
+      cons (Label @ℓ) . first (biMetamorph @_ @_ @('R ρ1) @('R ρ2) @c h empty uncons cons) . uncons (Label @ℓ)
+
+
+-- | A null constraint
+class Unconstrained
+instance Unconstrained
+
+-- | A null constraint of one argument
+class Unconstrained1 a
+instance Unconstrained1 a
+
+-- | A null constraint of two arguments
+class Unconstrained2 a b
+instance Unconstrained2 a b
+
+-- | A pair of constraints
+class (c1 x, c2 y) => BiConstraint c1 c2 x y
+instance (c1 x, c2 y) => BiConstraint c1 c2 x y
+
+-- | The labels in a Row.
+type family Labels (r :: Row a) where
+  Labels (R '[]) = '[]
+  Labels (R (l :-> a ': xs)) = l ': Labels (R xs)
+
+-- | Return a list of the labels in a row type.
+labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]
+labels = getConst $ metamorph @_ @ρ @c @Const @(Const ()) @(Const [s]) @Proxy Proxy (const $ Const []) doUncons doCons (Const ())
+  where doUncons _ _ = Const $ Const ()
+        doCons l (Const (Const c)) = Const $ show' l : c
+
+-- | Return a list of the labels in a row type and is specialized to the 'Unconstrained1' constraint.
+labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]
+labels' = labels @ρ @Unconstrained1
+
+
+{--------------------------------------------------------------------
+  Convenient type families and classes
+--------------------------------------------------------------------}
+
+-- | A convenient way to provide common, easy constraints
+type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)
+
+-- | Are all of the labels in this Row unique?
+type family AllUniqueLabels (r :: Row k) :: Constraint where
+  AllUniqueLabels (R r) = AllUniqueLabelsR r
+
+type family AllUniqueLabelsR (r :: [LT k]) :: Constraint where
+  AllUniqueLabelsR '[] = Unconstrained
+  AllUniqueLabelsR '[l :-> a] = Unconstrained
+  AllUniqueLabelsR (l :-> a ': l :-> b ': _) = TypeError
+    (TL.Text "The label " :<>: ShowType l :<>: TL.Text " is not unique."
+    :$$: TL.Text "It is assigned to both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b)
+  AllUniqueLabelsR (l :-> a ': l' :-> b ': r) = AllUniqueLabelsR (l' :-> b ': r)
+
+-- | Is the first row a subset of the second?
+type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint where
+  Subset (R r1) (R r2) = SubsetR r1 r2
+
+type family SubsetR (r1 :: [LT k]) (r2 :: [LT k]) :: Constraint where
+  SubsetR '[] _ = Unconstrained
+  SubsetR x '[] = TypeError (TL.Text "One row-type is not a subset of the other."
+        :$$: TL.Text "The first contains the bindings " :<>: ShowRowType x
+        :<>: TL.Text " while the second does not.")
+  SubsetR (l :-> a ': x) (l :-> a ': y) = SubsetR x y
+  SubsetR (l :-> a ': x) (l :-> b ': y) =
+    TypeError (TL.Text "One row-type is not a subset of the other."
+          :$$: TL.Text "The first assigns the label " :<>: ShowType l :<>: TL.Text " to "
+          :<>: ShowType a :<>: TL.Text " while the second assigns it to " :<>: ShowType b)
+  SubsetR (hl :-> al ': tl) (hr :-> ar ': tr) =
+      Ifte (hl <=.? hr)
+      (TypeError (TL.Text "One row-type is not a subset of the other."
+             :$$: TL.Text "The first assigns the label " :<>: ShowType hl :<>: TL.Text " to "
+             :<>: ShowType al :<>: TL.Text " while the second has no assignment for it."))
+      (SubsetR (hl :-> al ': tl) tr)
+
+-- | A type synonym for disjointness.
+type Disjoint l r = ( WellBehaved l
+                    , WellBehaved r
+                    , Subset l (l .+ r)
+                    , Subset r (l .+ r)
+                    , l .+ r .\\ l ≈ r
+                    , l .+ r .\\ r ≈ l)
+
+-- | Map a type level function over a Row.
+type family Map (f :: a -> b) (r :: Row a) :: Row b where
+  Map f (R r) = R (MapR f r)
+
+type family MapR (f :: a -> b) (r :: [LT a]) :: [LT b] where
+  MapR f '[] = '[]
+  MapR f (l :-> v ': t) = l :-> f v ': MapR f t
+
+-- | Take two rows with the same labels, and apply the type operator from the
+-- first row to the type of the second.
+type family Ap (fs :: Row (a -> b)) (r :: Row a) :: Row b where
+  Ap (R fs) (R r) = R (ApR fs r)
+
+type family ApR (fs :: [LT (a -> b)]) (r :: [LT a]) :: [LT b] where
+  ApR '[] '[] = '[]
+  ApR (l :-> f ': tf) (l :-> v ': tv) = l :-> f v ': ApR tf tv
+  ApR _ _ = TypeError (TL.Text "Row types with different label sets cannot be App'd together.")
+
+-- | Take a row of type operators and apply each to the second argument.
+type family ApSingle (fs :: Row (a -> b)) (x :: a) :: Row b where
+  ApSingle (R fs) x = R (ApSingleR fs x)
+
+type family ApSingleR (fs :: [LT (a -> b)]) (x :: a) :: [LT b] where
+  ApSingleR '[] _ = '[]
+  ApSingleR (l ':-> f ': fs) x = l ':-> f x ': ApSingleR fs x
+
+-- | Zips two rows together to create a Row of the pairs.
+--   The two rows must have the same set of labels.
+type family Zip (r1 :: Row *) (r2 :: Row *) where
+  Zip (R r1) (R r2) = R (ZipR r1 r2)
+
+type family ZipR (r1 :: [LT *]) (r2 :: [LT *]) where
+  ZipR '[] '[] = '[]
+  ZipR (l :-> t1 ': r1) (l :-> t2 ': r2) =
+    l :-> (t1, t2) ': ZipR r1 r2
+  ZipR (l :-> t1 ': r1) _ = TypeError (TL.Text "Row types with different label sets cannot be zipped"
+                                  :$$: TL.Text "For one, the label " :<>: ShowType l :<>: TL.Text " is not in both lists.")
+  ZipR '[] (l :-> t ': r) = TypeError (TL.Text "Row types with different label sets cannot be zipped"
+                                  :$$: TL.Text "For one, the label " :<>: ShowType l :<>: TL.Text " is not in both lists.")
+
+type family Inject (l :: LT k) (r :: [LT k]) where
+  Inject (l :-> t) '[] = (l :-> t ': '[])
+  Inject (l :-> t) (l :-> t' ': x) = TypeError (TL.Text "Cannot inject a label into a row type that already has that label"
+                                  :$$: TL.Text "The label " :<>: ShowType l :<>: TL.Text " was already assigned the type "
+                                  :<>: ShowType t' :<>: TL.Text " and is now trying to be assigned the type "
+                                  :<>: ShowType t :<>: TL.Text ".")
+  Inject (l :-> t) (l' :-> t' ': x) =
+      Ifte (l <=.? l')
+      (l :-> t   ': l' :-> t' ': x)
+      (l' :-> t' ': Inject (l :-> t)  x)
+
+-- | Type level Row modification helper
+type family ModifyR (l :: Symbol) (a :: k) (ρ :: [LT k]) :: [LT k] where
+  ModifyR l a (l :-> a' ': ρ) = l :-> a ': ρ
+  ModifyR l a (l' :-> a' ': ρ) = l' :-> a' ': ModifyR l a ρ
+  ModifyR l a '[] = TypeError (TL.Text "Tried to modify the label " :<>: ShowType l
+                          :<>: TL.Text ", but it does not appear in the row-type.")
+
+type family Ifte (c :: Bool) (t :: k) (f :: k)   where
+  Ifte True  t f = t
+  Ifte False t f = f
+
+type family Get (l :: Symbol) (r :: [LT k]) where
+  Get l '[] = TypeError (TL.Text "No such field: " :<>: ShowType l)
+  Get l (l :-> t ': x) = t
+  Get l (l' :-> t ': x) = Get l x
+
+type family Remove (l :: Symbol) (r :: [LT k]) where
+  Remove l r = RemoveT l r r
+
+type family RemoveT (l :: Symbol) (r :: [LT k]) (r_orig :: [LT k]) where
+  RemoveT l (l :-> t ': x) _ = x
+  RemoveT l (l' :-> t ': x) r = l' :-> t ': RemoveT l x r
+  RemoveT l '[] r = TypeError (TL.Text "Cannot remove a label that does not occur in the row type."
+                          :$$: TL.Text "The label " :<>: ShowType l :<>: TL.Text " is not in "
+                          :<>: ShowRowType r)
+
+type family LacksR (l :: Symbol) (r :: [LT k]) (r_orig :: [LT k]) :: Constraint where
+  LacksR l '[] _ = Unconstrained
+  LacksR l (l :-> t ': x) r = TypeError (TL.Text "The label " :<>: ShowType l
+                                    :<>: TL.Text " already exists in " :<>: ShowRowType r)
+  LacksR l (l' :-> _ ': x) r = Ifte (l <=.? l') Unconstrained (LacksR l x r)
+
+
+type family Merge (l :: [LT k]) (r :: [LT k]) where
+  Merge '[] r = r
+  Merge l '[] = l
+  Merge (h :-> a ': tl)   (h :-> a ': tr) =
+    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " (of type "
+          :$$: ShowType a :<>: TL.Text ") has duplicate assignments.")
+  Merge (h :-> a ': tl)   (h :-> b ': tr) =
+    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."
+          :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")
+  Merge (hl :-> al ': tl) (hr :-> ar ': tr) =
+      Ifte (hl <=.? hr)
+      (hl :-> al ': Merge tl (hr :-> ar ': tr))
+      (hr :-> ar ': Merge (hl :-> al ': tl) tr)
+
+type family MinJoinR (l :: [LT k]) (r :: [LT k]) where
+  MinJoinR '[] r = r
+  MinJoinR l '[] = l
+  MinJoinR (h :-> a ': tl)   (h :-> a ': tr) =
+      (h :-> a ': MinJoinR tl tr)
+  MinJoinR (h :-> a ': tl)   (h :-> b ': tr) =
+    TypeError (TL.Text "The label " :<>: ShowType h :<>: TL.Text " has conflicting assignments."
+          :$$: TL.Text "Its type is both " :<>: ShowType a :<>: TL.Text " and " :<>: ShowType b :<>: TL.Text ".")
+  MinJoinR (hl :-> al ': tl) (hr :-> ar ': tr) =
+      Ifte (CmpSymbol hl hr == 'LT)
+      (hl :-> al ': MinJoinR tl (hr :-> ar ': tr))
+      (hr :-> ar ': MinJoinR (hl :-> al ': tl) tr)
+
+type family ConstUnionR (l :: [LT k]) (r :: [LT k]) where
+  ConstUnionR '[] r = r
+  ConstUnionR l '[] = l
+  ConstUnionR (h :-> a ': tl)   (h :-> b ': tr) =
+      (h :-> a ': ConstUnionR tl tr)
+  ConstUnionR (hl :-> al ': tl) (hr :-> ar ': tr) =
+      Ifte (CmpSymbol hl hr == 'LT)
+      (hl :-> al ': ConstUnionR tl (hr :-> ar ': tr))
+      (hr :-> ar ': ConstUnionR (hl :-> al ': tl) tr)
+
+
+-- | Returns the left list with all of the elements from the right list removed.
+type family Diff (l :: [LT k]) (r :: [LT k]) where
+  Diff '[] r = '[]
+  Diff l '[] = l
+  Diff (l :-> al ': tl) (l :-> al ': tr) = Diff tl tr
+  Diff (hl :-> al ': tl) (hr :-> ar ': tr) =
+    Ifte (hl <=.? hr)
+    (hl :-> al ': Diff tl (hr :-> ar ': tr))
+    (Diff (hl :-> al ': tl) tr)
+
+type family ShowRowType (r :: [LT k]) :: ErrorMessage where
+  ShowRowType '[] = TL.Text "Empty"
+  ShowRowType '[l ':-> t] = TL.ShowType l TL.:<>: TL.Text " .== " TL.:<>: TL.ShowType t
+  ShowRowType ((l ':-> t) ': r) = TL.ShowType l TL.:<>: TL.Text " .== " TL.:<>: TL.ShowType t TL.:<>: TL.Text " .+ " TL.:<>: ShowRowType r
+
+-- | There doesn't seem to be a (<=.?) :: Symbol -> Symbol -> Bool,
+-- so here it is in terms of other ghc-7.8 type functions
+type a <=.? b = (CmpSymbol a b == 'LT)
+
+-- | A lower fixity operator for type equality
+infix 4 ≈
+type a ≈ b = a ~ b

@@ -0,0 +1,837 @@+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row.Records
+--
+-- This module implements extensible records using closed type famillies.
+--
+-- See Examples.lhs for examples.
+--
+-- Lists of (label,type) pairs are kept sorted thereby ensuring
+-- that { x = 0, y = 0 } and { y = 0, x = 0 } have the same type.
+--
+-- In this way we can implement standard type classes such as Show, Eq, Ord and Bounded
+-- for open records, given that all the elements of the open record satify the constraint.
+--
+-----------------------------------------------------------------------------
+
+
+module Data.Row.Records
+  (
+  -- * Types and constraints
+    Label(..)
+  , KnownSymbol, AllUniqueLabels, WellBehaved
+  , Rec, Row, Empty, type (≈)
+  -- * Construction
+  , empty
+  , type (.==), (.==), pattern (:==), unSingleton
+  , default', defaultA
+  , fromLabels, fromLabelsA, fromLabelsMapA
+  -- ** Extension
+  , extend, Extend, Lacks, type (.\)
+  -- ** Restriction
+  , type (.-), (.-)
+  , lazyRemove
+  , restrict, split
+  -- ** Modification
+  , update, focus, multifocus, Modify, rename, Rename
+  -- * Query
+  , HasType, type (.!), (.!)
+  -- * Combine
+  -- ** Disjoint union
+  , type (.+), (.+), Disjoint, pattern (:+)
+  -- ** Overwrite
+  , type (.//), (.//)
+  -- * Application with functions
+  , curryRec
+  , (.$)
+  -- * Native Conversion
+  -- $native
+  , fromNative, toNative, toNativeGeneral
+  , FromNative, ToNative, ToNativeGeneral
+  , NativeRow
+  -- * Dynamic Conversion
+  , toDynamicMap, fromDynamicMap
+  -- * Row operations
+  -- ** Map
+  , Map, map, map', mapF
+  , transform, transform'
+  , zipTransform, zipTransform'
+  -- ** Fold
+  , BiForall, Forall, erase, eraseWithLabels, eraseZip, eraseToHashMap
+  -- ** Zip
+  , Zip, zip
+  -- ** Applicative-like functions
+  , traverse, traverseMap
+  , sequence, sequence'
+  , distribute
+  -- ** Compose
+  -- $compose
+  , compose, uncompose
+  , compose', uncompose'
+  -- ** Labels
+  , labels, labels'
+  -- ** Coerce
+  , coerceRec
+  )
+where
+
+import Prelude hiding (map, sequence, traverse, zip)
+
+import Control.DeepSeq (NFData(..), deepseq)
+
+import           Data.Bifunctor               (Bifunctor(..))
+import           Data.Coerce
+import           Data.Dynamic
+import           Data.Functor.Compose
+import           Data.Functor.Const
+import           Data.Functor.Identity
+import           Data.Functor.Product
+import           Data.Generics.Product.Fields (HasField(..), HasField'(..))
+import           Data.Hashable
+import           Data.HashMap.Lazy            (HashMap)
+import qualified Data.HashMap.Lazy            as M
+import qualified Data.List                    as L
+import           Data.Monoid                  (Endo(..), appEndo)
+import           Data.Proxy
+import           Data.String                  (IsString)
+import           Data.Text                    (Text)
+
+import qualified GHC.Generics as G
+import           GHC.TypeLits
+import Unsafe.Coerce
+
+import Data.Row.Dictionaries
+import Data.Row.Internal
+
+
+{--------------------------------------------------------------------
+  Open records
+--------------------------------------------------------------------}
+-- | A record with row r.
+newtype Rec (r :: Row *) where
+  OR :: HashMap Text HideType -> Rec r
+
+instance Forall r Show => Show (Rec r) where
+  showsPrec p r =
+    case eraseWithLabels @Show (showsPrec 7) r of
+      [] ->
+        showString "empty"
+      xs ->
+        showParen
+          (p > 6)
+          (appEndo $ foldMap Endo (L.intersperse (showString " .+ ") (L.map binds xs)))
+    where
+      binds (label, value) =
+        showChar '#' .
+        showString label .
+        showString " .== " .
+        value
+
+instance Forall r Eq => Eq (Rec r) where
+  r == r' = and $ eraseZip @Eq (==) r r'
+
+instance (Forall r Eq, Forall r Ord) => Ord (Rec r) where
+  compare m m' = cmp $ eraseZip @Ord compare m m'
+      where cmp l | [] <- l' = EQ
+                  | a : _ <- l' = a
+                  where l' = dropWhile (== EQ) l
+
+instance (Forall r Bounded, AllUniqueLabels r) => Bounded (Rec r) where
+  minBound = default' @Bounded minBound
+  maxBound = default' @Bounded maxBound
+
+instance Forall r NFData => NFData (Rec r) where
+  rnf r = getConst $ metamorph @_ @r @NFData @(,) @Rec @(Const ()) @Identity Proxy empty doUncons doCons r
+    where empty = const $ Const ()
+          doUncons l = second Identity . lazyUncons l
+          doCons _ (r, x) = deepseq x $ deepseq r $ Const ()
+
+-- | The empty record
+empty :: Rec Empty
+empty = OR M.empty
+
+-- | The singleton record
+infix 7 .==
+(.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a)
+l .== a = extend l a empty
+
+-- | A pattern for the singleton record; can be used to both destruct a record
+-- when in a pattern position or construct one in an expression position.
+{-# COMPLETE (:==) #-}
+infix 7 :==
+pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a)
+pattern l :== a <- (unSingleton @l @a -> (l, a)) where
+        (:==) l a = l .== a
+
+-- | Turns a singleton record into a pair of the label and value.
+unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a)
+unSingleton r = (l, r .! l) where l = Label @l
+
+{--------------------------------------------------------------------
+  Basic record operations
+--------------------------------------------------------------------}
+
+
+-- | Record extension. The row may already contain the label,
+--   in which case the origin value can be obtained after restriction ('.-') with
+--   the label.
+extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)
+extend (toKey -> l) a (OR m) = OR $ M.insert l (HideType a) m
+
+-- | Update the value associated with the label.
+update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Rec r -> Rec r
+update (toKey -> l) a (OR m) = OR $ M.adjust f l m where f = const (HideType a)
+
+-- | Focus on the value associated with the label.
+focus ::
+  ( KnownSymbol l
+  , r' .! l ≈ b
+  , r  .! l ≈ a
+  , r' ~ Modify l b r
+  , r  ~ Modify l a r'
+  , Functor f)
+  => Label l -> (a -> f b) -> Rec r -> f (Rec r')
+focus (toKey -> l) f (OR m) = case m M.! l of
+  HideType x -> OR . flip (M.insert l) m . HideType <$> f (unsafeCoerce x)
+
+-- | Focus on a sub-record
+multifocus :: forall u v r f.
+  ( Functor f
+  , Disjoint u r
+  , Disjoint v r)
+  => (Rec u -> f (Rec v)) -> Rec (u .+ r) -> f (Rec (v .+ r))
+multifocus f (u :+ r) = (.+ r) <$> f u
+
+-- | Rename a label.
+rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)
+rename (toKey -> l) (toKey -> l') (OR m) = OR $ M.insert l' (m M.! l) $ M.delete l m
+
+-- | Record selection
+(.!) :: KnownSymbol l => Rec r -> Label l -> r .! l
+OR m .! (toKey -> a) = case m M.! a of
+  HideType x -> unsafeCoerce x
+
+infixl 6 .-
+-- | Record restriction. Remove the label l from the record.
+(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l)
+-- OR m .- _ = OR m
+OR m .- (toKey -> a) = OR $ M.delete a m
+
+-- | Record disjoint union (commutative)
+infixl 6 .+
+(.+) :: forall l r. FreeForall l => Rec l -> Rec r -> Rec (l .+ r)
+OR l .+ OR r = OR $ M.unionWithKey choose l r
+  where
+    choose k lv rv = if k `elem` labels' @l @Text then lv else rv
+
+-- | Record overwrite.
+--
+-- The operation @r .// r'@ creates a new record such that:
+--
+-- - Any label that is in both @r@ and @r'@ is in the resulting record with the
+--   type and value given by the fields in @r@,
+--
+-- - Any label that is only found in @r@ is in the resulting record.
+--
+-- - Any label that is only found in @r'@ is in the resulting record.
+--
+-- This can be thought of as @r@ "overwriting" @r'@.
+(.//) :: Rec r -> Rec r' -> Rec (r .// r')
+OR l .// OR r = OR $ M.union l r
+
+-- | A pattern version of record union, for use in pattern matching.
+{-# COMPLETE (:+) #-}
+infixl 6 :+
+pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r)
+pattern l :+ r <- (split @l -> (l, r)) where
+        (:+) l r = l .+ r
+
+-- | Split a record into two sub-records.
+split :: forall s r. (Subset s r, FreeForall s)
+         => Rec r -> (Rec s, Rec (r .\\ s))
+split (OR m) = (OR $ M.intersection m labelMap, OR $ M.difference m labelMap)
+  where
+    labelMap = M.fromList $ L.zip (labels' @s) (repeat ())
+
+-- | Arbitrary record restriction.  Turn a record into a subset of itself.
+restrict :: forall r r'. (FreeForall r, Subset r r') => Rec r' -> Rec r
+restrict = fst . split
+
+-- | Removes a label from the record but does not remove the underlying value.
+--
+-- This is faster than regular record removal ('.-'), but it has two downsides:
+--
+-- 1. It may incur a performance penalty during a future merge operation ('.+'), and
+--
+-- 2. It will keep the reference to the value alive, meaning that it will not get garbage collected.
+--
+-- Thus, it's great when one knows ahead of time that no future merges will happen
+-- and that the whole record will be GC'd soon, for instance, during the catamorphism
+-- function of 'metamorph'.
+lazyRemove :: KnownSymbol l => Label l -> Rec r -> Rec (r .- l)
+lazyRemove _ (OR m) = OR m
+
+-- | This is the same as @(lazyRemove l r, r .! l)@.
+lazyUncons :: KnownSymbol l => Label l -> Rec r -> (Rec (r .- l), r .! l)
+lazyUncons l r = (lazyRemove l r, r .! l)
+
+-- | Kind of like 'curry' for functions over records.
+curryRec :: forall l t r x. KnownSymbol l => Label l -> (Rec (l .== t .+ r) -> x) -> t -> Rec r -> x
+curryRec l f t r = f $ (l .== t) .+ r
+
+infixl 2 .$
+-- | This function allows one to do partial application on a function of a record.
+-- Note that this also means that arguments can be supplied in arbitrary order.
+-- For instance, if one had a function like
+--
+-- > xtheny r = (r .! #x) <> (r .! #y)
+--
+-- and a record like
+--
+-- > greeting = #x .== "hello " .+ #y .== "world!"
+--
+-- Then all of the following would be possible:
+--
+-- >>> xtheny greeting
+-- "hello world!"
+--
+-- >>> xtheny .$ (#x, greeting) .$ (#y, greeting) $ empty
+-- "hello world!"
+--
+-- >>> xtheny .$ (#y, greeting) .$ (#x, greeting) $ empty
+-- "hello world!"
+--
+-- >>> xtheny .$ (#y, greeting) .$ (#x, #x .== "Goodbye ") $ empty
+-- "Goodbye world!"
+(.$) :: (KnownSymbol l, r' .! l ≈ t) => (Rec (l .== t .+ r) -> x) -> (Label l, Rec r') -> Rec r -> x
+(.$) f (l, r') r = curryRec l f (r' .! l) r
+
+{--------------------------------------------------------------------
+  Folds and maps
+--------------------------------------------------------------------}
+-- An easy type synonym for a pair where both elements are the same type.
+newtype Pair' a = Pair' { unPair' :: (a,a) }
+
+-- | A standard fold
+erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b]
+erase f = fmap (snd @String) . eraseWithLabels @c f
+
+-- | A fold with labels
+eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s,b)]
+eraseWithLabels f = getConst . metamorph @_ @ρ @c @(,) @Rec @(Const [(s,b)]) @Identity Proxy doNil doUncons doCons
+  where doNil _ = Const []
+        doUncons l = second Identity . lazyUncons l
+        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+               => Label ℓ -> (Const [(s,b)] ρ, Identity τ) -> Const [(s,b)] (Extend ℓ τ ρ)
+        doCons l (Const c, Identity x) = Const $ (show' l, f x) : c
+
+-- | A fold over two row type structures at once
+eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Rec ρ -> Rec ρ -> [b]
+eraseZip f x y = getConst $ metamorph @_ @ρ @c @(,) @(Product Rec Rec) @(Const [b]) @Pair' Proxy (const $ Const []) doUncons doCons (Pair x y)
+  where doUncons l (Pair r1 r2) = (Pair r1' r2', Pair' (a, b))
+          where (r1', a) = lazyUncons l r1
+                (r2', b) = lazyUncons l r2
+        doCons :: forall ℓ τ ρ. c τ
+               => Label ℓ -> (Const [b] ρ, Pair' τ) -> Const [b] (Extend ℓ τ ρ)
+        doCons _ (Const c, unPair' -> x) = Const $ uncurry f x : c
+
+-- | Turns a record into a 'HashMap' from values representing the labels to
+--   the values of the record.
+eraseToHashMap :: forall c r s b. (IsString s, Eq s, Hashable s, Forall r c) =>
+                  (forall a . c a => a -> b) -> Rec r -> HashMap s b
+eraseToHashMap f r = M.fromList $ eraseWithLabels @c f r
+
+-- | RMap is used internally as a type level lambda for defining record maps.
+newtype RMap (f :: * -> *) (ρ :: Row *) = RMap { unRMap :: Rec (Map f ρ) }
+newtype RMap2 (f :: * -> *) (g :: * -> *) (ρ :: Row *) = RMap2 { unRMap2 :: Rec (Map f (Map g ρ)) }
+
+-- | A function to map over a record given a constraint.
+map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Rec r -> Rec (Map f r)
+map f = unRMap . metamorph @_ @r @c @(,) @Rec @(RMap f) @f Proxy doNil doUncons doCons
+  where
+    doNil _ = RMap empty
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> Rec ρ -> (Rec (ρ .- ℓ), f τ)
+    doUncons l = second f . lazyUncons l
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+           => Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
+    doCons l (RMap r, v) = RMap (extend l v r)
+      \\ mapExtendSwap @f @ℓ @τ @ρ
+
+newtype RFMap (g :: k1 -> k2) (ϕ :: Row (k2 -> *)) (ρ :: Row k1) = RFMap { unRFMap :: Rec (Ap ϕ (Map g ρ)) }
+newtype RecAp (ϕ :: Row (k -> *)) (ρ :: Row k) = RecAp (Rec (Ap ϕ ρ))
+newtype App (f :: k -> *) (a :: k) = App (f a)
+
+-- | A function to map over a Ap record given constraints.
+mapF :: forall k c g (ϕ :: Row (k -> *)) (ρ :: Row k). BiForall ϕ ρ c
+     => (forall h a. (c h a) => h a -> h (g a))
+     -> Rec (Ap ϕ ρ)
+     -> Rec (Ap ϕ (Map g ρ))
+mapF f = unRFMap . biMetamorph @_ @_ @ϕ @ρ @c @(,) @RecAp @(RFMap g) @App Proxy doNil doUncons doCons . RecAp
+  where
+    doNil _ = RFMap empty
+    doUncons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, c f τ, HasType ℓ f ϕ, HasType ℓ τ ρ)
+             => Label ℓ -> RecAp ϕ ρ -> (RecAp (ϕ .- ℓ) (ρ .- ℓ), App f τ)
+    doUncons l (RecAp r) = bimap RecAp App $ lazyUncons l r
+      \\ apHas @ℓ @f @ϕ @τ @ρ
+    doCons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, c f τ)
+           => Label ℓ -> (RFMap g ϕ ρ, App f τ) -> RFMap g (Extend ℓ f ϕ) (Extend ℓ τ ρ)
+    doCons l (RFMap r, App v) = RFMap (extend l (f @f @τ v) r)
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+      \\ apExtendSwap @ℓ @f @ϕ @(g τ) @(Map g ρ)
+
+-- | A function to map over a record given no constraint.
+map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Rec r -> Rec (Map f r)
+map' = map @Unconstrained1
+
+-- | Lifts a natural transformation over a record.  In other words, it acts as a
+-- record transformer to convert a record of @f a@ values to a record of @g a@
+-- values.  If no constraint is needed, instantiate the first type argument with
+-- 'Unconstrained1' or use 'transform''.
+transform :: forall c r (f :: * -> *) (g :: * -> *). Forall r c => (forall a. c a => f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
+transform f = unRMap . metamorph @_ @r @c @(,) @(RMap f) @(RMap g) @f Proxy doNil doUncons doCons . RMap
+  where
+    doNil _ = RMap empty
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
+    doUncons l (RMap r) = first RMap $ lazyUncons l r
+      \\ mapHas @f @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+           => Label ℓ -> (RMap g ρ, f τ) -> RMap g (Extend ℓ τ ρ)
+    doCons l (RMap r, v) = RMap (extend l (f v) r)
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+
+-- | A version of 'transform' for when there is no constraint.
+transform' :: forall r (f :: * -> *) (g :: * -> *). FreeForall r => (forall a. f a -> g a) -> Rec (Map f r) -> Rec (Map g r)
+transform' = transform @Unconstrained1 @r
+
+
+data RecMapPair (f :: * -> *) (g :: * -> *) (ρ :: Row *) = RecMapPair (Rec (Map f ρ)) (Rec (Map g ρ))
+
+-- | Zip together two records that are the same up to the type being mapped over them,
+-- combining their constituent fields with the given function.
+zipTransform :: forall c r (f :: * -> *) (g :: * -> *) (h :: * -> *) .
+  Forall r c => (forall a. c a => f a -> g a -> h a) -> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
+zipTransform f x y = unRMap $ metamorph @_ @r @c @(,) @(RecMapPair f g) @(RMap h) @h Proxy doNil doUncons doCons $ RecMapPair x y
+  where
+    doNil _ = RMap empty
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> RecMapPair f g ρ -> (RecMapPair f g (ρ .- ℓ), h τ)
+    doUncons l (RecMapPair x y) = (RecMapPair (lazyRemove l x) (lazyRemove l y), f (x .! l) (y .! l))
+      \\ mapHas @f @ℓ @τ @ρ
+      \\ mapHas @g @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+           => Label ℓ -> (RMap h ρ, h τ) -> RMap h (Extend ℓ τ ρ)
+    doCons l (RMap r, h) = RMap (extend l h r)
+      \\ mapExtendSwap @h @ℓ @τ @ρ
+
+-- | A version of 'zipTransform' for when there is no constraint.
+zipTransform' :: forall r (f :: * -> *) (g :: * -> *) (h :: * -> *) .
+  FreeForall r => (forall a. f a -> g a -> h a) -> Rec (Map f r) -> Rec (Map g r) -> Rec (Map h r)
+zipTransform' = zipTransform @Unconstrained1 @r
+
+-- | Traverse a function over a record.  Note that the fields of the record will
+-- be accessed in lexicographic order by the labels.
+traverse :: forall c f r. (Forall r c, Applicative f) => (forall a. c a => a -> f a) -> Rec r -> f (Rec r)
+traverse f = sequence' @f @r @c . map @c @f @r f
+
+-- | Traverse a function over a Mapped record.  Note that the fields of the record will
+-- be accessed in lexicographic order by the labels.
+traverseMap :: forall c (f :: * -> *) (g :: * -> *) (h :: * -> *) r.
+  (Forall r c, Applicative f) => (forall a. c a => g a -> f (h a)) -> Rec (Map g r) -> f (Rec (Map h r))
+traverseMap f =
+  sequence' @f @(Map h r) @(IsA c h) .
+  uncompose' @c @f @h @r .
+  transform @c @r @g @(Compose f h) (Compose . f)
+  \\ mapForall @h @r @c
+
+-- | A version of 'sequence' in which the constraint for 'Forall' can be chosen.
+sequence' :: forall f r c. (Forall r c, Applicative f)
+          => Rec (Map f r) -> f (Rec r)
+sequence' = getCompose . metamorph @_ @r @c @(,) @(RMap f) @(Compose f Rec) @f Proxy doNil doUncons doCons . RMap
+  where
+    doNil _ = Compose (pure empty)
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> RMap f ρ -> (RMap f (ρ .- ℓ), f τ)
+    doUncons l (RMap r) = first RMap $ lazyUncons l r
+      \\ mapHas @f @ℓ @τ @ρ
+    doCons l (Compose fr, fv) = Compose $ extend l <$> fv <*> fr
+
+-- | Applicative sequencing over a record.
+sequence :: forall f r. (Applicative f, FreeForall r)
+         => Rec (Map f r) -> f (Rec r)
+sequence = sequence' @_ @_ @Unconstrained1
+
+-- | This function acts as the inversion of `sequence`, allowing one to move a
+-- functor level into a record.
+distribute :: forall f r. (FreeForall r, Functor f) => f (Rec r) -> Rec (Map f r)
+distribute  = unRMap . metamorph @_ @r @Unconstrained1 @(,) @(Compose f Rec) @(RMap f) @f Proxy doNil doUncons doCons . Compose
+  where
+    doNil _ = RMap empty
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
+             => Label ℓ -> Compose f Rec ρ -> (Compose f Rec (ρ .- ℓ), f τ)
+    doUncons l (Compose fr) = (Compose $ lazyRemove l <$> fr, (.! l) <$> fr)
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ)
+           => Label ℓ -> (RMap f ρ, f τ) -> RMap f (Extend ℓ τ ρ)
+    doCons l (RMap r, fv) = RMap (extend l fv r)
+      \\ mapExtendSwap @f @ℓ @τ @ρ
+
+
+-- $compose
+-- We can easily convert between mapping two functors over the types of a row
+-- and mapping the composition of the two functors.  The following two functions
+-- perform this composition with the gaurantee that:
+--
+-- >>> compose . uncompose = id
+--
+-- >>> uncompose . compose = id
+
+-- | A version of 'compose' in which the constraint for 'Forall' can be chosen.
+compose' :: forall c (f :: * -> *) (g :: * -> *) (r :: Row *) . Forall r c
+        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
+compose' = unRMap . metamorph @_ @r @c @(,) @(RMap2 f g) @(RMap (Compose f g)) @(Compose f g) Proxy doNil doUncons doCons . RMap2
+  where
+    doNil _ = RMap empty
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> RMap2 f g ρ -> (RMap2 f g (ρ .- ℓ), Compose f g τ)
+    doUncons l (RMap2 r) = bimap RMap2 Compose $ lazyUncons l r
+      \\ mapHas @f @ℓ @(g τ) @(Map g ρ)
+      \\ mapHas @g @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+           => Label ℓ -> (RMap (Compose f g) ρ, Compose f g τ) -> RMap (Compose f g) (Extend ℓ τ ρ)
+    doCons l (RMap r, v) = RMap $ extend l v r
+      \\ mapExtendSwap @(Compose f g) @ℓ @τ @ρ
+
+-- | Convert from a record where two functors have been mapped over the types to
+-- one where the composition of the two functors is mapped over the types.
+compose :: forall (f :: * -> *) (g :: * -> *) r . FreeForall r
+        => Rec (Map f (Map g r)) -> Rec (Map (Compose f g) r)
+compose = compose' @Unconstrained1 @f @g @r
+
+-- | A version of 'uncompose' in which the constraint for 'Forall' can be chosen.
+uncompose' :: forall c (f :: * -> *) (g :: * -> *) r . Forall r c
+           => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
+uncompose' = unRMap2 . metamorph @_ @r @c @(,) @(RMap (Compose f g)) @(RMap2 f g) @(Compose f g) Proxy doNil doUncons doCons . RMap
+  where
+    doNil _ = RMap2 empty
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> RMap (Compose f g) ρ -> (RMap (Compose f g) (ρ .- ℓ), Compose f g τ)
+    doUncons l (RMap r) = first RMap $ lazyUncons l r
+      \\ mapHas @(Compose f g) @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+           => Label ℓ -> (RMap2 f g ρ, Compose f g τ) -> RMap2 f g (Extend ℓ τ ρ)
+    doCons l (RMap2 r, Compose v) = RMap2 $ extend l v r
+      \\ mapExtendSwap @f @ℓ @(g τ) @(Map g ρ)
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+
+-- | Convert from a record where the composition of two functors have been mapped
+-- over the types to one where the two functors are mapped individually one at a
+-- time over the types.
+uncompose :: forall (f :: * -> *) (g :: * -> *) r . FreeForall r
+          => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))
+uncompose = uncompose' @Unconstrained1 @f @g @r
+
+
+-- | Coerce a record to a coercible representation.  The 'BiForall' in the context
+-- indicates that the type of every field in @r1@ can be coerced to the type of
+-- the corresponding fields in @r2@.
+--
+-- Internally, this is implemented just with `unsafeCoerce`, but we provide the
+-- following implementation as a proof:
+--
+-- > newtype ConstR a b = ConstR (Rec a)
+-- > newtype FlipConstR a b = FlipConstR { unFlipConstR :: Rec b }
+-- > coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2
+-- > coerceRec = unFlipConstR . biMetamorph @_ @_ @r1 @r2 @Coercible @(,) @ConstR @FlipConstR @Const Proxy doNil doUncons doCons . ConstR
+-- >   where
+-- >     doNil _ = FlipConstR empty
+-- >     doUncons l (ConstR r) = bimap ConstR Const $ lazyUncons l r
+-- >     doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2)
+-- >            => Label ℓ -> (FlipConstR ρ1 ρ2, Const τ1 τ2) -> FlipConstR (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
+-- >     doCons l (FlipConstR r, Const v) = FlipConstR $ extend l (coerce @τ1 @τ2 v) r
+coerceRec :: forall r1 r2. BiForall r1 r2 Coercible => Rec r1 -> Rec r2
+coerceRec = unsafeCoerce
+
+
+-- | RZipPair is used internally as a type level lambda for zipping records.
+newtype RecPair  (ρ1 :: Row *) (ρ2 :: Row *) = RecPair  (Rec ρ1, Rec ρ2)
+newtype RZipPair (ρ1 :: Row *) (ρ2 :: Row *) = RZipPair { unRZipPair :: Rec (Zip ρ1 ρ2) }
+
+-- | Zips together two records that have the same set of labels.
+zip :: forall r1 r2. FreeBiForall r1 r2 => Rec r1 -> Rec r2 -> Rec (Zip r1 r2)
+zip r1 r2 = unRZipPair $ biMetamorph @_ @_ @r1 @r2 @Unconstrained2 @(,) @RecPair @RZipPair @(,) Proxy doNil doUncons doCons $ RecPair (r1, r2)
+  where
+    doNil _ = RZipPair empty
+    doUncons l (RecPair (r1, r2)) = (RecPair (lazyRemove l r1, lazyRemove l r2), (r1 .! l, r2 .! l))
+    doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ)
+           => Label ℓ -> (RZipPair ρ1 ρ2, (τ1, τ2)) -> RZipPair (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
+    doCons l (RZipPair r, vs) = RZipPair $ extend l vs r
+      \\ zipExtendSwap @ℓ @τ1 @ρ1 @τ2 @ρ2
+
+{--------------------------------------------------------------------
+  Record initialization
+--------------------------------------------------------------------}
+
+-- | Initialize a record with a default value at each label.
+default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ
+default' v = runIdentity $ defaultA @c $ pure v
+
+-- | Initialize a record with a default value at each label; works over an 'Applicative'.
+defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
+         => (forall a. c a => f a) -> f (Rec ρ)
+defaultA v = fromLabelsA @c $ pure v
+
+-- | Initialize a record, where each value is determined by the given function over
+-- the label at that value.
+fromLabels :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ)
+           => (forall l a. (KnownSymbol l, c a) => Label l -> a) -> Rec ρ
+fromLabels f = runIdentity $ fromLabelsA @c $ (pure .) f
+
+-- | Initialize a record, where each value is determined by the given function over
+-- the label at that value.  This function works over an 'Applicative'.
+fromLabelsA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
+            => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Rec ρ)
+fromLabelsA mk = getCompose $ metamorph @_ @ρ @c @Const @(Const ()) @(Compose f Rec) @Proxy Proxy doNil doUncons doCons (Const ())
+  where doNil _ = Compose $ pure empty
+        doUncons _ _ = Const $ Const ()
+        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+               => Label ℓ -> Const (Compose f Rec ρ) (Proxy τ) -> Compose f Rec (Extend ℓ τ ρ)
+        doCons l (Const (Compose r)) = Compose $ extend l <$> mk @ℓ @τ l <*> r
+
+-- | Initialize a record over a `Map`.
+fromLabelsMapA :: forall c f g ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ)
+               => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Rec (Map g ρ))
+fromLabelsMapA f = fromLabelsA @(IsA c g) @f @(Map g ρ) inner
+                \\ mapForall @g @ρ @c
+                \\ uniqueMap @g @ρ
+   where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a
+         inner l = case as @c @g @a of As -> f l
+
+
+{--------------------------------------------------------------------
+  Dynamic compatibility
+--------------------------------------------------------------------}
+
+-- | Converts a 'Rec' into a 'HashMap' of 'Dynamic's.
+toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic
+toDynamicMap = eraseToHashMap @Typeable @_ @Text @Dynamic toDyn
+
+-- | Produces a 'Rec' from a 'HashMap' of 'Dynamic's.
+fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable)
+               => HashMap Text Dynamic -> Maybe (Rec r)
+fromDynamicMap m = fromLabelsA @Typeable
+  $ \ (toKey -> k) -> M.lookup k m >>= fromDynamic
+
+
+{--------------------------------------------------------------------
+  Generic instance
+--------------------------------------------------------------------}
+
+-- The generic structure we want Recs to have is not the hidden internal one,
+-- but rather one that appears as a Haskell record.  Thus, we can't derive
+-- Generic automatically.
+--
+-- The following Generic instance creates a representation of a Rec that is
+-- very similar to a native Haskell record except that the tree of pairs (':*:')
+-- that it produces will be extremely unbalanced.  I don't think this is a problem.
+-- Furthermore, because we don't want Recs to always have a trailing unit on
+-- the end, we must have a special case for singleton Recs, which means that
+-- we can't use metamorph.
+
+instance GenericRec r => G.Generic (Rec r) where
+  type Rep (Rec r) =
+    G.D1 ('G.MetaData "Rec" "Data.Row.Records" "row-types" 'False)
+      (G.C1 ('G.MetaCons "Rec" 'G.PrefixI 'True)
+        (RepRec r))
+  from = G.M1 . G.M1 . fromRec
+  to = toRec . G.unM1 . G.unM1
+
+class GenericRec r where
+  type RepRec (r :: Row *) :: * -> *
+  fromRec :: Rec r -> RepRec r x
+  toRec   :: RepRec r x -> Rec r
+
+instance GenericRec Empty where
+  type RepRec (R '[]) = G.U1
+  fromRec _ = G.U1
+  toRec _ = empty
+
+instance KnownSymbol name => GenericRec (R '[name :-> t]) where
+  type RepRec (R (name :-> t ': '[])) = G.S1
+    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
+    (G.Rec0 t)
+  fromRec (_ :== a) = G.M1 (G.K1 a)
+  toRec (G.M1 (G.K1 a)) = (Label @name) :== a
+
+instance
+    ( r ~ (name' :-> t' ': r'), GenericRec (R r)
+    , KnownSymbol name, Extend name t ('R r) ≈ 'R (name :-> t ': r)
+    ) => GenericRec (R (name :-> t ': (name' :-> t' ': r'))) where
+  type RepRec (R (name :-> t ': (name' :-> t' ': r'))) = (G.S1
+    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
+    (G.Rec0 t)) G.:*: RepRec (R (name' :-> t' ': r'))
+  fromRec r = G.M1 (G.K1 (r .! Label @name)) G.:*: fromRec (lazyRemove @name Label r)
+  toRec (G.M1 (G.K1 a) G.:*: r) = extend @_ @name @('R (name' :-> t' ': r')) Label a (toRec r)
+
+{--------------------------------------------------------------------
+  Native data type compatibility
+--------------------------------------------------------------------}
+-- ToNative is shamelessly copied from
+--   https://www.athiemann.net/2017/07/02/superrecord.html
+
+-- $native
+-- The 'toNative' and 'fromNative' functions allow one to convert between
+-- 'Rec's and regular Haskell data types ("native" types) that have a single constructor and any
+-- number of named fields with the same names and types as the 'Rec'.  As expected,
+-- they compose to form the identity.  Alternatively, one may use 'toNativeGeneral',
+-- which allows fields to be dropped when a record has excess fields compared
+-- to the native type.  Because of this, 'toNativeGeneral' requires a type
+-- application (although 'fromNative' does not).  The only requirement is that
+-- the native Haskell data type be an instance of 'Generic'.
+--
+-- For example, consider the following simple data type:
+--
+-- >>> data Person = Person { name :: String, age :: Int} deriving (Generic, Show)
+--
+-- Then, we have the following:
+--
+-- >>> toNative @Person $ #name .== "Alice" .+ #age .== 7 .+ #hasDog .== True
+-- Person {name = "Alice", age = 7}
+-- >>> fromNative $ Person "Bob" 9
+-- { age=9, name="Bob" }
+
+type family NativeRow t where
+  NativeRow t = NativeRowG (G.Rep t)
+
+type family NativeRowG t where
+  NativeRowG (G.M1 G.D m cs) = NativeRowG cs
+  NativeRowG (G.M1 G.C m cs) = NativeRowG cs
+  NativeRowG G.U1 = Empty
+  NativeRowG (l G.:*: r) = NativeRowG l .+ NativeRowG r
+  NativeRowG (G.M1 G.S ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) = name .== t
+
+
+-- | Conversion helper to turn a Haskell record into a row-types extensible
+-- record. Note that the native Haskell type must be an instance of 'Generic'.
+class FromNativeG a where
+  fromNative' :: a x -> Rec (NativeRowG a)
+
+instance FromNativeG cs => FromNativeG (G.D1 m cs) where
+  fromNative' (G.M1 xs) = fromNative' xs
+
+instance FromNativeG cs => FromNativeG (G.C1 m cs) where
+  fromNative' (G.M1 xs) = fromNative' xs
+
+instance FromNativeG G.U1 where
+  fromNative' G.U1 = empty
+
+instance KnownSymbol name => FromNativeG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) where
+  fromNative' (G.M1 (G.K1 x)) =  (Label @name) .== x
+
+instance (FromNativeG l, FromNativeG r, FreeForall (NativeRowG l)) => FromNativeG (l G.:*: r) where
+  fromNative' (x G.:*: y) = fromNative' @l x .+ fromNative' @r y
+
+type FromNative t = (G.Generic t, FromNativeG (G.Rep t))
+
+-- | Convert a Haskell record to a row-types Rec.
+fromNative :: FromNative t => t -> Rec (NativeRow t)
+fromNative = fromNative' . G.from
+
+
+-- | Conversion helper to bring a record back into a Haskell type. Note that the
+-- native Haskell type must be an instance of 'Generic'.
+class ToNativeG a where
+  toNative' :: Rec (NativeRowG a) -> a x
+
+instance ToNativeG cs => ToNativeG (G.D1 m cs) where
+  toNative' xs = G.M1 $ toNative' xs
+
+instance ToNativeG cs => ToNativeG (G.C1 m cs) where
+  toNative' xs = G.M1 $ toNative' xs
+
+instance ToNativeG G.U1 where
+  toNative' _ = G.U1
+
+instance (KnownSymbol name) => ToNativeG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) where
+  toNative' r = G.M1 $ G.K1 $ r .! (Label @name)
+
+instance (ToNativeG l, ToNativeG r, Disjoint (NativeRowG l) (NativeRowG r))
+    => ToNativeG (l G.:*: r) where
+  toNative' r = toNative' r1 G.:*: toNative' r2
+    where
+      (r1 :: Rec (NativeRowG l)) :+ (r2 :: Rec (NativeRowG r)) = r
+
+type ToNative t = (G.Generic t, ToNativeG (G.Rep t))
+
+-- | Convert a record to an exactly matching native Haskell type.
+toNative :: ToNative t => Rec (NativeRow t) -> t
+toNative = G.to . toNative'
+
+
+
+-- | Conversion helper to bring a record back into a Haskell type. Note that the
+-- native Haskell type must be an instance of 'Generic'.
+class ToNativeGeneralG a ρ where
+  toNativeGeneral' :: Rec ρ -> a x
+
+instance ToNativeGeneralG cs ρ => ToNativeGeneralG (G.D1 m cs) ρ where
+  toNativeGeneral' xs = G.M1 $ toNativeGeneral' xs
+
+instance ToNativeGeneralG cs ρ => ToNativeGeneralG (G.C1 m cs) ρ where
+  toNativeGeneral' xs = G.M1 $ toNativeGeneral' xs
+
+instance ToNativeGeneralG G.U1 ρ where
+  toNativeGeneral' _ = G.U1
+
+instance (KnownSymbol name, ρ .! name ≈ t)
+    => ToNativeGeneralG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where
+  toNativeGeneral' r = G.M1 $ G.K1 $ r .! (Label @name)
+
+instance (ToNativeGeneralG l ρ, ToNativeGeneralG r ρ)
+    => ToNativeGeneralG (l G.:*: r) ρ where
+  toNativeGeneral' r = toNativeGeneral' r G.:*: toNativeGeneral' r
+
+type ToNativeGeneral t ρ = (G.Generic t, ToNativeGeneralG (G.Rep t) ρ)
+
+-- | Convert a record to a native Haskell type.
+toNativeGeneral :: ToNativeGeneral t ρ => Rec ρ -> t
+toNativeGeneral = G.to . toNativeGeneral'
+
+
+{--------------------------------------------------------------------
+  Generic-lens compatibility
+--------------------------------------------------------------------}
+
+-- | Every field in a row-types based record has a 'HasField' instance.
+instance {-# OVERLAPPING #-}
+  ( KnownSymbol name
+  , r' .! name ≈ b
+  , r  .! name ≈ a
+  , r' ~ Modify name b r
+  , r  ~ Modify name a r')
+  => HasField name (Rec r) (Rec r') a b where
+  field = focus (Label @name)
+  {-# INLINE field #-}
+
+instance {-# OVERLAPPING #-}
+  ( KnownSymbol name
+  , r .! name ≈ a
+  , r ~ Modify name a r)
+  => HasField' name (Rec r) a where
+  field' = focus (Label @name)
+  {-# INLINE field' #-}

@@ -0,0 +1,65 @@+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module: Data.Row.Switch
+--
+-- This module provides the ability to discharge a polymorphic variant using
+-- a record that has matching fields.
+--
+-----------------------------------------------------------------------------
+
+
+module Data.Row.Switch
+  ( AppliesTo(..)
+  , switch
+  , caseon
+  )
+where
+
+import Data.Proxy
+
+import Data.Bifunctor (Bifunctor(..))
+import Data.Row.Internal
+import Data.Row.Records
+import Data.Row.Variants
+
+-- | A simple class that we use to provide a constraint for function application.
+class AppliesTo r f x | r x -> f, f r -> x where
+  applyTo :: f -> x -> r
+instance AppliesTo r (x -> r) x where
+  applyTo = ($)
+
+-- | A pair of a record and a variant.
+data SwitchData r v = SwitchData (Rec r) (Var v)
+
+-- | Like 'Const' but for two ignored type arguments.
+newtype Const2 x y z = Const2 { getConst2 :: x }
+
+-- | A 'Var' and a 'Rec' can combine if their rows line up properly.
+-- Given a Variant along with a Record of functions from each possible value
+-- of the variant to a single output type, apply the correct
+-- function to the value in the variant.
+switch :: forall v r x. BiForall r v (AppliesTo x) => Var v -> Rec r -> x
+switch v r = getConst2 $ biMetamorph @_ @_ @r @v @(AppliesTo x) @Either @SwitchData @(Const2 x) @(Const2 x)
+  Proxy doNil doUncons doCons $ SwitchData r v
+  where
+    doNil (SwitchData _ v) = impossible v
+    doUncons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, AppliesTo x f τ, HasType ℓ f ϕ, HasType ℓ τ ρ)
+             => Label ℓ -> SwitchData ϕ ρ -> Either (SwitchData (ϕ .- ℓ) (ρ .- ℓ)) (Const2 x f τ)
+    doUncons l (SwitchData r v) = bimap (SwitchData $ lazyRemove l r) (Const2 . applyTo (r .! l)) $ trial v l
+    -- doCons :: forall ℓ f τ ϕ ρ. (KnownSymbol ℓ, AppliesTo x f τ)
+    --        => Label ℓ -> Either (Const2 x f τ) (Const2 x ϕ ρ) -> Const2 x (Extend ℓ f ϕ) (Extend ℓ τ ρ)
+    doCons _ (Left  (Const2 x)) = Const2 x
+    doCons _ (Right (Const2 x)) = Const2 x
+
+-- | The same as 'switch' but with the argument order reversed
+caseon :: forall v r x. BiForall r v (AppliesTo x) => Rec r -> Var v -> x
+caseon = flip switch

@@ -0,0 +1,761 @@+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row.Variants
+--
+-- This module implements extensible variants using closed type families.
+--
+-----------------------------------------------------------------------------
+
+
+module Data.Row.Variants
+  (
+  -- * Types and constraints
+    Label(..)
+  , KnownSymbol, AllUniqueLabels, WellBehaved
+  , Var, Row, Empty, type (≈)
+  -- * Construction
+  , HasType, pattern IsJust, singleton, unSingleton
+  , fromLabels, fromLabelsMap
+  -- ** Extension
+  , type (.\), Lacks, type (.\/), diversify, extend, type (.+)
+  -- ** Modification
+  , update, focus, Modify, rename, Rename
+  -- * Destruction
+  , impossible, trial, trial', multiTrial, view
+  , restrict, split
+  -- ** Types for destruction
+  , type (.!), type (.-), type (.\\), type (.==)
+  -- * Native Conversion
+  -- $native
+  , toNative, fromNative, fromNativeGeneral
+  , ToNative, FromNative, FromNativeGeneral
+  , NativeRow
+  -- * Row operations
+  -- ** Map
+  , Map, map, map', transform, transform'
+  -- ** Fold
+  , Forall, erase, eraseWithLabels, eraseZipGeneral, eraseZip
+  -- ** Applicative-like functions
+  , traverse, traverseMap
+  , sequence
+  -- ** Compose
+  -- $compose
+  , compose, uncompose
+  -- ** labels
+  , labels
+  -- ** ApSingle functions
+  , eraseSingle, mapSingle, eraseZipSingle
+  -- ** Coerce
+  , coerceVar
+  )
+where
+
+import Prelude hiding (map, sequence, traverse, zip)
+
+import Control.Applicative
+import Control.DeepSeq     (NFData(..), deepseq)
+
+import Data.Bifunctor (Bifunctor(..))
+import Data.Coerce
+import Data.Constraint                (Constraint)
+import Data.Functor.Compose
+import Data.Functor.Identity
+import Data.Functor.Product
+import Data.Generics.Sum.Constructors (AsConstructor(..), AsConstructor'(..))
+import Data.Maybe                     (fromMaybe)
+import Data.Profunctor                (Choice(..), Profunctor(..))
+import Data.Proxy
+import Data.String                    (IsString)
+import Data.Text                      (Text)
+
+import qualified GHC.Generics as G
+import           GHC.TypeLits
+
+import Unsafe.Coerce
+
+import Data.Row.Dictionaries
+import Data.Row.Internal
+
+{--------------------------------------------------------------------
+  Polymorphic Variants
+--------------------------------------------------------------------}
+
+-- | The variant type.
+data Var (r :: Row *) where
+  OneOf :: Text -> HideType -> Var r
+
+instance Forall r Show => Show (Var r) where
+  show v = (\ (x, y) -> "{" ++ x ++ "=" ++ y ++ "}") $ eraseWithLabels @Show show v
+
+instance Forall r Eq => Eq (Var r) where
+  r == r' = fromMaybe False $ eraseZip @Eq (==) r r'
+
+instance (Forall r Eq, Forall r Ord) => Ord (Var r) where
+  compare :: Var r -> Var r -> Ordering
+  compare = eraseZipGeneral @Ord @r @Ordering @Text $ \case
+    (Left (_, x, y))           -> compare x y
+    (Right ((s1, _), (s2, _))) -> compare s1 s2
+
+instance Forall r NFData => NFData (Var r) where
+  rnf r = getConst $ metamorph @_ @r @NFData @Either @Var @(Const ()) @Identity Proxy empty doUncons doCons r
+    where empty = const $ Const ()
+          doUncons l = second Identity . flip trial l
+          doCons _ x = deepseq x $ Const ()
+
+
+{--------------------------------------------------------------------
+  Basic Operations
+--------------------------------------------------------------------}
+
+-- | A Variant with no options is uninhabited.
+impossible :: Var Empty -> a
+impossible _ = error "Impossible! Somehow, a variant of nothing was produced."
+
+-- | A quick constructor to create a singleton variant.
+singleton :: KnownSymbol l => Label l -> a -> Var (l .== a)
+singleton = IsJust
+
+-- | A quick destructor for singleton variants.
+unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a)
+unSingleton (OneOf _ (HideType x)) = (l, unsafeCoerce x) where l = Label @l
+
+-- | A pattern for variants; can be used to both destruct a variant
+-- when in a pattern position or construct one in an expression position.
+pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> r .! l -> Var r
+pattern IsJust l a <- (isJustHelper @l -> (l, Just a)) where
+        IsJust (toKey -> l) = OneOf l . HideType
+
+isJustHelper :: forall l r. KnownSymbol l => Var r -> (Label l, Maybe (r .! l))
+isJustHelper v = (l, view l v) where l = Label @l
+
+-- | Make the variant arbitrarily more diverse.
+diversify :: forall r' r. Var r -> Var (r .\/ r')
+diversify = unsafeCoerce -- (OneOf l x) = OneOf l x
+
+-- | A weaker version of 'diversify', but it's helpful for 'metamorph' as it explicitly
+-- uses 'Extend'.
+extend :: forall a l r. KnownSymbol l => Label l -> Var r -> Var (Extend l a r)
+extend _ = unsafeCoerce
+
+-- | If the variant exists at the given label, update it to the given value.
+-- Otherwise, do nothing.
+update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Var r -> Var r
+update (toKey -> l') a (OneOf l x) = OneOf l $ if l == l' then HideType a else x
+
+-- | If the variant exists at the given label, focus on the value associated with it.
+-- Otherwise, do nothing.
+focus :: forall l r r' a b p f.
+  ( AllUniqueLabels r
+  , AllUniqueLabels r'
+  , KnownSymbol l
+  , r  .! l ≈ a
+  , r' .! l ≈ b
+  , r' ≈ (r .- l) .\/ (l .== b)
+  , Applicative f
+  , Choice p
+  ) => Label l -> p a (f b) -> p (Var r) (f (Var r'))
+focus (toKey -> l) =
+  dimap unwrap rewrap . left'
+  where
+    unwrap :: Var r -> Either a (Var r')
+    unwrap (OneOf l' (HideType x))
+      | l == l'   = Left (unsafeCoerce x)
+      | otherwise = Right (OneOf l' (HideType x))
+    rewrap :: Either (f b) (Var r') -> f (Var r')
+    rewrap = either (fmap $ OneOf l . HideType) pure
+
+-- | Rename the given label.
+rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r)
+rename (toKey -> l1) (toKey -> l2) (OneOf l x) = OneOf (if l == l1 then l2 else l) x
+
+-- | Convert a variant into either the value at the given label or a variant without
+-- that label.  This is the basic variant destructor.
+trial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l)
+trial (OneOf l (HideType x)) (toKey -> l') = if l == l' then Right (unsafeCoerce x) else Left (OneOf l (HideType x))
+
+-- | A version of 'trial' that ignores the leftover variant.
+trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l)
+trial' = (either (const Nothing) Just .) . trial
+
+-- | A trial over multiple types
+multiTrial :: forall x y. (AllUniqueLabels x, Forall (y .\\ x) Unconstrained1) => Var y -> Either (Var (y .\\ x)) (Var x)
+multiTrial (OneOf l x) = if l `elem` labels @(y .\\ x) @Unconstrained1 then Left (OneOf l x) else Right (OneOf l x)
+
+-- | A convenient function for using view patterns when dispatching variants.
+--   For example:
+--
+-- @
+-- myShow :: Var ("y" '::= String :| "x" '::= Int :| Empty) -> String
+-- myShow (view x -> Just n) = "Int of "++show n
+-- myShow (view y -> Just s) = "String of "++s @
+view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)
+view = flip trial'
+
+-- | Split a variant into two sub-variants.
+split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var (r .\\ s)) (Var s)
+split (OneOf l a) | l `elem` labels @s @Unconstrained1 = Right $ OneOf l a
+                  | otherwise                          = Left  $ OneOf l a
+
+-- | Arbitrary variant restriction.  Turn a variant into a subset of itself.
+restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r)
+restrict = either (pure Nothing) Just . split
+
+
+{--------------------------------------------------------------------
+  Folds and maps
+--------------------------------------------------------------------}
+
+-- | A standard fold
+erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b
+erase f = snd @String . eraseWithLabels @c f
+
+-- | A fold with labels
+eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s,b)
+eraseWithLabels f = getConst . metamorph @_ @ρ @c @Either @Var @(Const (s,b)) @Identity Proxy impossible doUncons doCons
+  where doUncons l = second Identity . flip trial l
+        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
+               => Label ℓ -> Either (Const (s,b) ρ) (Identity τ) -> Const (s,b) (Extend ℓ τ ρ)
+        doCons _ (Left  (Const c)) = Const c
+        doCons l (Right (Identity x)) = Const (show' l, f x)
+
+
+data ErasedVal c s = forall y. c y => ErasedVal (s, y)
+data ErasePair c s ρ = ErasePair (Either (ErasedVal c s) (Var ρ)) (Either (ErasedVal c s) (Var ρ))
+
+-- | A fold over two variants at once.  A call @eraseZipGeneral f x y@ will return
+-- @f (Left (show l, a, b))@ when 'x' and 'y' both have values at the same label 'l'
+-- and will return @f (Right ((show l1, a), (show l2, b)))@ when they have values
+-- at different labels 'l1' and 'l2' respectively.
+eraseZipGeneral
+  :: forall c ρ b s. (Forall ρ c, IsString s)
+  => (forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b)
+  -> Var ρ -> Var ρ -> b
+eraseZipGeneral f x y = getConst $ metamorph @_ @ρ @c @Either @(ErasePair c s) @(Const b) @(Const b) Proxy doNil doUncons doCons (ErasePair (Right x) (Right y))
+  where
+    doNil (ErasePair (Left (ErasedVal a)) (Left (ErasedVal b))) =
+      Const $ f $ Right (a, b)
+    doNil (ErasePair (Right x) _) = impossible x
+    doNil (ErasePair _ (Right y)) = impossible y
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> ErasePair c s ρ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
+    doUncons _ (ErasePair (Left (ErasedVal a)) (Left (ErasedVal b))) =
+      Right $ Const $ f $ Right (a, b)
+    doUncons l (ErasePair (Right x) (Left eb)) = case (trial x l, eb) of
+      (Right a, ErasedVal b) -> Right $ Const $ f $ Right ((show' l, a), b)
+      (Left x', _)           -> Left $ ErasePair (Right x') (Left eb)
+    doUncons l (ErasePair (Left ea) (Right y)) = case (ea, trial y l) of
+      (ErasedVal a, Right b) -> Right $ Const $ f $ Right (a, (show' l, b))
+      (_, Left x')           -> Left $ ErasePair (Left ea) (Right x')
+    doUncons l (ErasePair (Right x) (Right y)) = case (trial x l, trial y l) of
+      (Right (a :: x), Right b) -> Right $ Const $ f @x @x $ Left (show' l, a, b)
+      (Right a,        Left y') -> Left $ ErasePair (Left $ ErasedVal (show' l, a)) (Right y')
+      (Left x', Right b)        -> Left $ ErasePair (Right x') (Left $ ErasedVal (show' l, b))
+      (Left x', Left y')        -> Left $ ErasePair (Right x') (Right y')
+    doCons _ (Left  (Const b)) = Const b
+    doCons _ (Right (Const b)) = Const b
+
+
+-- | A simpler fold over two variants at once
+eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b
+eraseZip f = eraseZipGeneral @c @ρ @(Maybe b) @Text $ \case
+    Left (_,x,y) -> Just (f x y)
+    _            -> Nothing
+
+
+-- | VMap is used internally as a type level lambda for defining variant maps.
+newtype VMap (f :: * -> *) (ρ :: Row *) = VMap { unVMap :: Var (Map f ρ) }
+newtype VMap2 (f :: * -> *) (g :: * -> *) (ρ :: Row *) = VMap2 { unVMap2 :: Var (Map f (Map g ρ)) }
+
+-- | A function to map over a variant given a constraint.
+map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Var r -> Var (Map f r)
+map f = unVMap . metamorph @_ @r @c @Either @Var @(VMap f) @Identity Proxy impossible doUncons doCons
+  where
+    doUncons l = second Identity . flip trial l
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ))
+           => Label ℓ -> Either (VMap f ρ) (Identity τ) -> VMap f (Extend ℓ τ ρ)
+    doCons l (Left (VMap v)) = VMap $ extend @(f τ) l v
+      \\ mapExtendSwap @f @ℓ @τ @ρ
+    doCons l (Right (Identity x)) = VMap $ IsJust l (f x)
+      \\ mapExtendSwap @f @ℓ @τ @ρ
+      \\ extendHas @ℓ @(f τ) @(Map f ρ)
+      \\ uniqueMap @f @(Extend ℓ τ ρ)
+
+-- | A function to map over a variant given no constraint.
+map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Var r -> Var (Map f r)
+map' = map @Unconstrained1
+
+-- | Lifts a natrual transformation over a variant.  In other words, it acts as a
+-- variant transformer to convert a variant of @f a@ values to a variant of @g a@
+-- values.  If no constraint is needed, instantiate the first type argument with
+-- 'Unconstrained1'.
+transform :: forall c r (f :: * -> *) (g :: * -> *). Forall r c => (forall a. c a => f a -> g a) -> Var (Map f r) -> Var (Map g r)
+transform f = unVMap . metamorph @_ @r @c @Either @(VMap f) @(VMap g) @f Proxy doNil doUncons doCons . VMap
+  where
+    doNil = impossible . unVMap
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
+             => Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
+    doUncons l = first VMap . flip trial l . unVMap
+      \\ mapHas @f @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ))
+           => Label ℓ -> Either (VMap g ρ) (f τ) -> VMap g (Extend ℓ τ ρ)
+    doCons l (Left (VMap v)) = VMap $ extend @(g τ) l v
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+    doCons l (Right x) = VMap $ IsJust l (f x)
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+      \\ extendHas @ℓ @(g τ) @(Map g ρ)
+      \\ uniqueMap @g @(Extend ℓ τ ρ)
+
+-- | A form of @transformC@ that doesn't have a constraint on @a@
+transform' :: forall r (f :: * -> *) (g :: * -> *) . FreeForall r => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r)
+transform' = transform @Unconstrained1 @r
+
+-- | Traverse a function over a variant.
+traverse :: forall c f r. (Forall r c, Applicative f) => (forall a. c a => a -> f a) -> Var r -> f (Var r)
+traverse f = sequence' @f @r @c . map @c @f @r f
+
+-- | Traverse a function over a Mapped variant.
+traverseMap :: forall c (f :: * -> *) (g :: * -> *) (h :: * -> *) r.
+  (Forall r c, Applicative f) => (forall a. c a => g a -> f (h a)) -> Var (Map g r) -> f (Var (Map h r))
+traverseMap f =
+  sequence' @f @(Map h r) @(IsA c h) .
+  uncompose' @c @f @h @r .
+  transform @c @r @g @(Compose f h) (Compose . f)
+  \\ mapForall @h @r @c
+
+-- | Applicative sequencing over a variant with arbitrary constraint.
+sequence' :: forall f r c. (Forall r c, Applicative f) => Var (Map f r) -> f (Var r)
+sequence' = getCompose . metamorph @_ @r @c @Either @(VMap f) @(Compose f Var) @f Proxy doNil doUncons doCons . VMap
+  where
+    doNil = impossible . unVMap
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
+             => Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
+    doUncons l = first VMap . flip trial l . unVMap
+      \\ mapHas @f @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ))
+           => Label ℓ -> Either (Compose f Var ρ) (f τ) -> Compose f Var (Extend ℓ τ ρ)
+    doCons l (Left (Compose v)) = Compose $ extend @τ l <$> v
+    doCons l (Right fx) = Compose $ IsJust l <$> fx
+      \\ extendHas @ℓ @τ @ρ
+
+
+-- | Applicative sequencing over a variant
+sequence :: forall f r. (FreeForall r, Applicative f) => Var (Map f r) -> f (Var r)
+sequence = sequence' @f @r @Unconstrained1
+
+-- $compose
+-- We can easily convert between mapping two functors over the types of a row
+-- and mapping the composition of the two functors.  The following two functions
+-- perform this composition with the gaurantee that:
+--
+-- >>> compose . uncompose = id
+--
+-- >>> uncompose . compose = id
+
+-- | Convert from a variant where two functors have been mapped over the types to
+-- one where the composition of the two functors is mapped over the types.
+compose :: forall (f :: * -> *) (g :: * -> *) r . FreeForall r => Var (Map f (Map g r)) -> Var (Map (Compose f g) r)
+compose = unVMap . metamorph @_ @r @Unconstrained1 @Either @(VMap2 f g) @(VMap (Compose f g)) @(Compose f g) Proxy doNil doUncons doCons . VMap2
+  where
+    doNil = impossible . unVMap2
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
+             => Label ℓ -> VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
+    doUncons l = bimap VMap2 Compose . flip trial l . unVMap2
+      \\ mapHas @f @ℓ @(g τ) @(Map g ρ)
+      \\ mapHas @g @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ))
+           => Label ℓ -> Either (VMap (Compose f g) ρ) (Compose f g τ) -> VMap (Compose f g) (Extend ℓ τ ρ)
+    doCons l (Left (VMap v)) = VMap $ extend @(Compose f g τ) l v
+      \\ mapExtendSwap @(Compose f g) @ℓ @τ @ρ
+    doCons l (Right x) = VMap $ IsJust l x
+      \\ mapExtendSwap @(Compose f g) @ℓ @τ @ρ
+      \\ extendHas @ℓ @((Compose f g) τ) @(Map (Compose f g) ρ)
+      \\ uniqueMap @(Compose f g) @(Extend ℓ τ ρ)
+
+-- | A version of 'uncompose' that allows an arbitrary constraint.
+uncompose' :: forall c (f :: * -> *) (g :: * -> *) r . Forall r c => Var (Map (Compose f g) r) -> Var (Map f (Map g r))
+uncompose' = unVMap2 . metamorph @_ @r @c @Either @(VMap (Compose f g)) @(VMap2 f g) @(Compose f g) Proxy doNil doUncons doCons . VMap
+  where
+    doNil = impossible . unVMap
+    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
+             => Label ℓ -> VMap (Compose f g) ρ -> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
+    doUncons l = first VMap . flip trial l . unVMap
+      \\ mapHas @(Compose f g) @ℓ @τ @ρ
+    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ))
+           => Label ℓ -> Either (VMap2 f g ρ) (Compose f g τ) -> VMap2 f g (Extend ℓ τ ρ)
+    doCons l (Left (VMap2 v)) = VMap2 $ extend @(f (g τ)) l v
+      \\ mapExtendSwap @f @ℓ @(g τ) @(Map g ρ)
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+    doCons l (Right (Compose x)) = VMap2 $ IsJust l x
+      \\ mapExtendSwap @f @ℓ @(g τ) @(Map g ρ)
+      \\ mapExtendSwap @g @ℓ @τ @ρ
+      \\ extendHas @ℓ @(f (g τ)) @(Map f (Map g ρ))
+      \\ uniqueMap @f @(Extend ℓ (g τ) (Map g ρ))
+      \\ uniqueMap @g @(Extend ℓ τ ρ)
+
+-- | Convert from a variant where the composition of two functors have been mapped
+-- over the types to one where the two functors are mapped individually one at a
+-- time over the types.
+uncompose :: forall (f :: * -> *) (g :: * -> *) r . FreeForall r => Var (Map (Compose f g) r) -> Var (Map f (Map g r))
+uncompose = uncompose' @Unconstrained1 @f @g @r
+
+-- | Coerce a variant to a coercible representation.  The 'BiForall' in the context
+-- indicates that the type of any option in @r1@ can be coerced to the type of
+-- the corresponding option in @r2@.
+--
+-- Internally, this is implemented just with `unsafeCoerce`, but we provide the
+-- following implementation as a proof:
+--
+-- > newtype ConstV a b = ConstV { unConstV :: Var a }
+-- > newtype ConstV a b = FlipConstV { unFlipConstV :: Var b }
+-- > coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
+-- > coerceVar = unFlipConstV . biMetamorph @_ @_ @r1 @r2 @Coercible @Either @ConstV @FlipConstV @Const Proxy doNil doUncons doCons . ConstV
+-- >   where
+-- >     doNil = impossible . unConstV
+-- >     doUncons l = bimap ConstV Const . flip trial l . unConstV
+-- >     doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2, AllUniqueLabels (Extend ℓ τ2 ρ2))
+-- >            => Label ℓ -> Either (FlipConstV ρ1 ρ2) (Const τ1 τ2)
+-- >            -> FlipConstV (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
+-- >     doCons l (Left (FlipConstV v)) = FlipConstV $ extend @τ2 l v
+-- >     doCons l (Right (Const x)) = FlipConstV $ IsJust l (coerce @τ1 @τ2 x)
+-- >       \\ extendHas @ρ2 @ℓ @τ2
+coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
+coerceVar = unsafeCoerce
+
+{--------------------------------------------------------------------
+  Variant initialization
+--------------------------------------------------------------------}
+
+-- | Initialize a variant from a producer function that accepts labels.  If this
+-- function returns more than one possibility, then one is chosen arbitrarily to
+-- be the value in the variant.
+fromLabels :: forall c ρ f. (Alternative f, Forall ρ c, AllUniqueLabels ρ)
+           => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Var ρ)
+fromLabels mk = getCompose $ metamorph @_ @ρ @c @Const @(Const ()) @(Compose f Var) @Proxy
+                                        Proxy doNil doUncons doCons (Const ())
+  where doNil _ = Compose $ empty
+        doUncons _ _ = Const $ Const ()
+        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ))
+               => Label ℓ -> Const (Compose f Var ρ) (Proxy τ) -> Compose f Var (Extend ℓ τ ρ)
+        doCons l (Const (Compose v)) = Compose $ IsJust l <$> mk l <|> extend @τ l <$> v
+          \\ extendHas @ℓ @τ @ρ
+
+-- | Initialize a variant over a `Map`.
+fromLabelsMap :: forall c f g ρ. (Alternative f, Forall ρ c, AllUniqueLabels ρ)
+              => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Var (Map g ρ))
+fromLabelsMap f = fromLabels @(IsA c g) @(Map g ρ) @f inner
+               \\ mapForall @g @ρ @c
+               \\ uniqueMap @g @ρ
+   where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a
+         inner l = case as @c @g @a of As -> f l
+
+{--------------------------------------------------------------------
+  Functions for variants of ApSingle
+--------------------------------------------------------------------}
+
+newtype VApS x (fs :: Row (* -> *)) = VApS { unVApS :: Var (ApSingle fs x) }
+newtype FlipApp (x :: *) (f :: * -> *) = FlipApp (f x)
+
+-- | A version of 'erase' that works even when the row-type of the variant argument
+-- is of the form @ApSingle fs x@.
+eraseSingle
+  :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *)
+   . Forall fs c
+  => (forall f . (c f) => f x -> y)
+  -> Var (ApSingle fs x)
+  -> y
+eraseSingle f = erase @(ActsOn c x) @(ApSingle fs x) @y g
+  \\ apSingleForall @x @fs @c
+  where
+    g :: forall a. ActsOn c x a => a -> y
+    g a = case actsOn @c @x @a of As' -> f a
+
+-- | Performs a functorial-like map over an 'ApSingle' variant.
+-- In other words, it acts as a variant transformer to convert a variant of
+-- @f x@ values to a variant of @f y@ values.  If no constraint is needed,
+-- instantiate the first type argument with 'Unconstrained1'.
+mapSingle
+  :: forall (c :: (* -> *) -> Constraint) (fs :: Row (* -> *)) (x :: *) (y :: *)
+   . (Forall fs c)
+  => (forall f . (c f) => f x -> f y)
+  -> Var (ApSingle fs x)
+  -> Var (ApSingle fs y)
+mapSingle f = unVApS . metamorph @_ @fs @c @Either @(VApS x) @(VApS y) @(FlipApp x)
+             Proxy doNil doUncons doCons . VApS
+ where
+  doNil = impossible . unVApS
+
+  doUncons :: forall l f fs
+           .  ( c f, fs .! l ≈ f, KnownSymbol l)
+           => Label l -> VApS x fs -> Either (VApS x (fs .- l)) (FlipApp x f)
+  doUncons l = bimap VApS FlipApp
+             . flip (trial \\ apSingleHas @x @l @f @fs) l
+             . unVApS
+
+  doCons :: forall l f fs. (KnownSymbol l, c f, AllUniqueLabels (Extend l f fs))
+         => Label l
+         -> Either (VApS y fs) (FlipApp x f)
+         -> VApS y (Extend l f fs)
+  doCons l (Right (FlipApp x)) = VApS $ IsJust l (f x)
+    \\ apSingleExtendSwap @y @l @f @fs
+    \\ extendHas @l @(f y) @(ApSingle fs y)
+    \\ uniqueApSingle @y @(Extend l f fs)
+  doCons l (Left (VApS v)) = VApS $ extend @(f y) l v
+    \\ apSingleExtendSwap @y @l @f @fs
+
+-- | A version of 'eraseZip' that works even when the row-types of the variant
+-- arguments are of the form @ApSingle fs x@.
+eraseZipSingle :: forall c fs (x :: *) (y :: *) z
+                . (Forall fs c)
+               => (forall f. c f => f x -> f y -> z)
+               -> Var (ApSingle fs x) -> Var (ApSingle fs y) -> Maybe z
+eraseZipSingle f x y = getConst $ metamorph @_ @fs @c @Either
+    @(Product (VApS x) (VApS y)) @(Const (Maybe z)) @(Const (Maybe z))
+    Proxy doNil doUncons doCons (Pair (VApS x) (VApS y))
+
+  where doNil :: Product (VApS x) (VApS y) Empty
+              -> Const (Maybe z) (Empty :: Row (* -> *))
+        doNil (Pair (VApS z) _) = Const (impossible z)
+
+        doUncons :: forall l f ρ
+                  . (KnownSymbol l, c f, ρ .! l ≈ f)
+                 => Label l
+                 -> Product (VApS x) (VApS y) ρ
+                 -> Either (Product (VApS x) (VApS y) (ρ .- l))
+                           (Const (Maybe z) f)
+        doUncons l (Pair (VApS r1) (VApS r2)) =
+          case (
+            trial r1 l \\ apSingleHas @x @l @f @ρ,
+            trial r2 l \\ apSingleHas @y @l @f @ρ
+          ) of
+            (Right u, Right v) -> Right $ Const $ Just $ f @f u v
+            (Left us, Left vs) -> Left (Pair (VApS us) (VApS vs))
+            _                  -> Right $ Const Nothing
+
+        doCons :: forall l (τ :: * -> *) ρ
+                . Label l
+               -> Either (Const (Maybe z) ρ) (Const (Maybe z) τ)
+               -> Const (Maybe z) (Extend l τ ρ)
+        doCons _ (Left (Const w))  = Const w
+        doCons _ (Right (Const w)) = Const w
+
+{--------------------------------------------------------------------
+  Generic instance
+--------------------------------------------------------------------}
+
+-- The generic structure we want Vars to have is not the hidden internal one,
+-- but rather one that appears as a Haskell sum type.  Thus, we can't derive
+-- Generic automatically.
+--
+-- The following Generic instance creates a representation of a Var that is
+-- very similar to a native Haskell sum type except that the tree of possibilities (':+:')
+-- that it produces will be extremely unbalanced.  I don't think this is a problem.
+-- Furthermore, because we don't want Vars to always have a trailing void option on
+-- the end, we must have a special case for singleton Vars, which means that
+-- we can't use metamorph.
+
+instance GenericVar r => G.Generic (Var r) where
+  type Rep (Var r) =
+    G.D1 ('G.MetaData "Var" "Data.Row.Variants" "row-types" 'False) (RepVar r)
+  from = G.M1 . fromVar
+  to = toVar . G.unM1
+
+class GenericVar r where
+  type RepVar (r :: Row *) :: * -> *
+  fromVar :: Var r -> RepVar r x
+  toVar   :: RepVar r x -> Var r
+
+instance GenericVar Empty where
+  type RepVar Empty = G.V1
+  fromVar = impossible
+  toVar = \case
+
+instance KnownSymbol name => GenericVar (R '[name :-> t]) where
+  type RepVar (R (name :-> t ': '[])) = G.C1
+    ('G.MetaCons name 'G.PrefixI 'False)
+    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
+          (G.Rec0 t))
+  fromVar (unSingleton -> (_, a)) = G.M1 (G.M1 (G.K1 a))
+  toVar (G.M1 (G.M1 (G.K1 a))) = IsJust (Label @name) a
+
+instance
+    ( GenericVar (R (name' :-> t' ': r'))
+    , KnownSymbol name, Extend name t ('R (name' :-> t' ': r')) ≈ 'R (name :-> t ': (name' :-> t' ': r'))
+    , AllUniqueLabels (R (name :-> t ': (name' :-> t' ': r')))
+    ) => GenericVar (R (name :-> t ': (name' :-> t' ': r'))) where
+  type RepVar (R (name :-> t ': (name' :-> t' ': r'))) = (G.C1
+    ('G.MetaCons name 'G.PrefixI 'False)
+    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
+          (G.Rec0 t)))  G.:+: RepVar (R (name' :-> t' ': r'))
+  fromVar v = case trial @name v Label of
+    Left v' -> G.R1 (fromVar v')
+    Right a -> G.L1 (G.M1 (G.M1 (G.K1 a)))
+  toVar (G.L1 (G.M1 (G.M1 (G.K1 a)))) = IsJust (Label @name) a
+  toVar (G.R1 g) = extend @t @name @('R (name' :-> t' ': r')) Label $ toVar g
+
+{--------------------------------------------------------------------
+  Native data type compatibility
+--------------------------------------------------------------------}
+
+-- $native
+-- The 'toNative' and 'fromNative' functions allow one to convert between
+-- 'Var's and regular Haskell data types ("native" types) that have the same
+-- number of constructors such that each constructor has one field and the same
+-- name as one of the options of the 'Var', which has the same type as that field.
+-- As expected, they compose to form the identity.  Alternatively, one may use
+-- 'fromNativeGeneral', which allows a variant with excess options to  still be
+-- transformed to a native type.  Because of this, 'fromNativeGeneral' requires a type
+-- application (although 'fromNative' does not).  The only requirement is that
+-- the native Haskell data type be an instance of 'Generic'.
+--
+-- For example, consider the following simple data type:
+--
+-- >>> data Pet = Dog {age :: Int} | Cat {age :: Int} deriving (Generic, Show)
+--
+-- Then, we have the following:
+--
+-- >>> toNative $ IsJust (Label @"Dog") 3 :: Pet
+-- Dog {age = 3}
+-- >>> V.fromNative $ Dog 3 :: Var ("Dog" .== Int .+ "Cat" .== Int)
+-- {Dog=3}
+
+type family NativeRow t where
+  NativeRow t = NativeRowG (G.Rep t)
+
+type family NativeRowG t where
+  NativeRowG (G.M1 G.D m cs) = NativeRowG cs
+  NativeRowG G.V1 = Empty
+  NativeRowG (l G.:+: r) = NativeRowG l .+ NativeRowG r
+  NativeRowG (G.C1 ('G.MetaCons name fixity sels) (G.S1 m (G.Rec0 t))) = name .== t
+
+
+-- | Conversion helper to bring a variant back into a Haskell type. Note that the
+-- native Haskell type must be an instance of 'Generic'.
+class ToNativeG a where
+  toNative' :: Var (NativeRowG a) -> a x
+
+instance ToNativeG cs => ToNativeG (G.D1 m cs) where
+  toNative' = G.M1 . toNative'
+
+instance ToNativeG G.V1 where
+  toNative' = impossible
+
+instance (KnownSymbol name)
+    => ToNativeG (G.C1 ('G.MetaCons name fixity sels)
+                (G.S1 m (G.Rec0 t))) where
+  toNative' = G.M1 . G.M1 . G.K1 . snd . unSingleton
+
+instance ( ToNativeG l, ToNativeG r, (NativeRowG l .+ NativeRowG r) .\\ NativeRowG r ≈ NativeRowG l
+         , AllUniqueLabels (NativeRowG r), Forall (NativeRowG l) Unconstrained1)
+    => ToNativeG (l G.:+: r) where
+  toNative' v = case multiTrial @(NativeRowG r) @(NativeRowG (l G.:+: r)) v of
+    Left  v' -> G.L1 $ toNative' v'
+    Right v' -> G.R1 $ toNative' v'
+
+type ToNative t = (G.Generic t, ToNativeG (G.Rep t))
+
+-- | Convert a variant to a native Haskell type.
+toNative :: ToNative t => Var (NativeRow t) -> t
+toNative = G.to . toNative'
+
+
+-- | Conversion helper to turn a Haskell variant into a row-types extensible
+-- variant. Note that the native Haskell type must be an instance of 'Generic'.
+class FromNativeG a where
+  fromNative' :: a x -> Var (NativeRowG a)
+
+instance FromNativeG cs => FromNativeG (G.D1 m cs) where
+  fromNative' (G.M1 v) = fromNative' v
+
+instance FromNativeG G.V1 where
+  fromNative' = \ case
+
+instance KnownSymbol name
+    => FromNativeG (G.C1 ('G.MetaCons name fixity sels)
+                       (G.S1 m (G.Rec0 t))) where
+  fromNative' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x
+
+instance (FromNativeG l, FromNativeG r) => FromNativeG (l G.:+: r) where
+  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it
+  -- makes the constraints really hairy.
+  fromNative' (G.L1 x) = unsafeCoerce $ fromNative' @l x
+  fromNative' (G.R1 y) = unsafeCoerce $ fromNative' @r y
+
+type FromNative t = (G.Generic t, FromNativeG (G.Rep t))
+
+-- | Convert a Haskell variant to a row-types Var.
+fromNative :: FromNative t => t -> Var (NativeRow t)
+fromNative = fromNative' . G.from
+
+
+-- | Conversion helper to turn a Haskell variant into a row-types extensible
+-- variant. Note that the native Haskell type must be an instance of 'Generic'.
+class FromNativeGeneralG a ρ where
+  fromNativeGeneral' :: a x -> Var ρ
+
+instance FromNativeGeneralG cs ρ => FromNativeGeneralG (G.D1 m cs) ρ where
+  fromNativeGeneral' (G.M1 v) = fromNativeGeneral' v
+
+instance FromNativeGeneralG G.V1 ρ where
+  fromNativeGeneral' = \ case
+
+instance (KnownSymbol name, ρ .! name ≈ t, AllUniqueLabels ρ)
+    => FromNativeGeneralG (G.C1 ('G.MetaCons name fixity sels)
+                  (G.S1 m (G.Rec0 t))) ρ where
+  fromNativeGeneral' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x
+
+instance (FromNativeGeneralG l ρ, FromNativeGeneralG r ρ)
+    => FromNativeGeneralG (l G.:+: r) ρ where
+  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it
+  -- makes the constraints really hairy.
+  fromNativeGeneral' (G.L1 x) = unsafeCoerce $ fromNativeGeneral' @l @ρ x
+  fromNativeGeneral' (G.R1 y) = unsafeCoerce $ fromNativeGeneral' @r @ρ y
+
+type FromNativeGeneral t ρ = (G.Generic t, FromNativeGeneralG (G.Rep t) ρ)
+
+-- | Convert a Haskell variant to a row-types Var.
+fromNativeGeneral :: FromNativeGeneral t ρ => t -> Var ρ
+fromNativeGeneral = fromNativeGeneral' . G.from
+
+
+{--------------------------------------------------------------------
+  Generic-lens compatibility
+--------------------------------------------------------------------}
+
+-- | Every possibility of a row-types based variant has an 'AsConstructor' instance.
+instance {-# OVERLAPPING #-}
+  ( AllUniqueLabels r
+  , AllUniqueLabels r'
+  , KnownSymbol name
+  , r  .! name ≈ a
+  , r' .! name ≈ b
+  , r' ≈ (r .- name) .\/ (name .== b))
+  => AsConstructor name (Var r) (Var r') a b where
+  _Ctor = focus (Label @name)
+  {-# INLINE _Ctor #-}
+
+instance {-# OVERLAPPING #-}
+  ( AllUniqueLabels r
+  , KnownSymbol name
+  , r  .! name ≈ a
+  , r ≈ (r .- name) .\/ (name .== a))
+  => AsConstructor' name (Var r) a where
+  _Ctor' = focus (Label @name)
+  {-# INLINE _Ctor' #-}

@@ -0,0 +1,52 @@+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row.Aeson
+--
+-- This module adds orphan Aeson instances for 'Rec' and 'Var'.
+--
+-----------------------------------------------------------------------------
+
+module Data.Row.Aeson () where
+
+import           Data.Aeson
+import           Data.Aeson.Encoding (pairStr)
+import           Data.Aeson.Types    (typeMismatch)
+import           Data.List           (intercalate)
+import           Data.Text           (Text)
+import qualified Data.Text           as Text (pack)
+
+import           Data.Row
+import qualified Data.Row.Records  as Rec
+import qualified Data.Row.Variants as Var
+
+instance Forall r ToJSON => ToJSON (Rec r) where
+  toJSON = Object . Rec.eraseToHashMap @ToJSON toJSON
+
+  toEncoding =
+    pairs . foldMap (uncurry pairStr) . Rec.eraseWithLabels @ToJSON toEncoding
+
+instance (AllUniqueLabels r, Forall r FromJSON) => FromJSON (Rec r) where
+  parseJSON (Object o) = do
+    r <- Rec.fromLabelsA @FromJSON $ \ l -> do x <- o .: (show' l)
+                                               x `seq` pure x
+    r `seq` pure r
+
+  parseJSON v = typeMismatch msg v
+    where msg = "REC: {" ++ intercalate "," (labels @r @FromJSON) ++ "}"
+
+instance Forall r ToJSON => ToJSON (Var r) where
+  toJSON v = object [foo l]
+    where (l, foo) = Var.eraseWithLabels @ToJSON (\v l -> l .= v) v
+
+instance (AllUniqueLabels r, Forall r FromJSON) => FromJSON (Var r) where
+  parseJSON (Object o) = Var.fromLabels @FromJSON $ \ l -> o .: (show' l)
+  parseJSON v = typeMismatch msg v
+    where msg = "VAR: {" ++ intercalate "," (labels @r @FromJSON) ++ "}"
+
+show' :: Show a => a -> Text
+show' = Text.pack . show

@@ -0,0 +1,77 @@+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Row.Barbie
+--
+-- This module adds Barbie instances for 'Rec' and 'Var'.
+--
+-----------------------------------------------------------------------------
+
+
+module Data.Row.Barbies () where
+
+import           Data.Functor.Compose
+import           Data.Functor.Identity
+import           Data.Functor.Product
+import           Data.Row
+import           Data.Row.Dictionaries
+import qualified Data.Row.Records      as Rec
+import qualified Data.Row.Variants     as Var
+
+import           Data.Functor.Barbie (FunctorB(..), TraversableB(..), DistributiveB(..), ApplicativeB(..), ConstraintsB(..))
+import qualified Barbies.Constraints as B
+
+-- | Barbies requires that the functor be the final argument of the type.  So,
+-- even though the real type is @Rec (Map f ρ)@, we must wrap it in a newtype
+-- wrapper so that 'f' is at the end.
+newtype BarbieRec (ρ :: Row *) (f :: * -> *) = BarbieRec { unBarbieRec :: Rec (Rec.Map f ρ) }
+newtype BarbieVar (ρ :: Row *) (f :: * -> *) = BarbieVar { unBarbieVar :: Var (Var.Map f ρ) }
+
+instance FreeForall r => FunctorB (BarbieRec r) where
+  bmap f = BarbieRec . Rec.transform' @r f . unBarbieRec
+
+instance FreeForall r => TraversableB (BarbieRec r) where
+  btraverse :: forall e f g. Applicative e => (forall a. f a -> e (g a)) -> BarbieRec r f -> e (BarbieRec r g)
+  btraverse f  = fmap BarbieRec . Rec.traverseMap @Unconstrained1 @e @f @g @r f . unBarbieRec
+
+instance FreeForall r => DistributiveB (BarbieRec r) where
+  bdistribute :: forall f g. Functor f => f (BarbieRec r g) -> BarbieRec r (Compose f g)
+  bdistribute = BarbieRec . Rec.compose @f @g @r . Rec.distribute @f @(Rec.Map g r) . fmap unBarbieRec
+    \\ freeForall @(Rec.Map g r) @(IsA Unconstrained1 g) \\ mapForall @g @r @Unconstrained1
+
+instance (AllUniqueLabels r, FreeForall r) => ApplicativeB (BarbieRec r) where
+  bpure :: forall f. (forall a. f a) -> BarbieRec r f
+  bpure fa = BarbieRec $ runIdentity $ Rec.fromLabelsMapA @Unconstrained1 @Identity @f @r (const $ Identity fa)
+
+  bprod :: forall f g. BarbieRec r f -> BarbieRec r g -> BarbieRec r (f `Product` g)
+  bprod (BarbieRec r1) (BarbieRec r2) = BarbieRec $ Rec.zipTransform @Unconstrained1 @r @f @g @(Product f g) Pair r1 r2
+
+instance FreeForall r => ConstraintsB (BarbieRec r) where
+  type AllB c (BarbieRec r) = Forall r c
+  baddDicts :: forall c f. Forall r c => BarbieRec r f -> BarbieRec r (B.Dict c `Product` f)
+  baddDicts = BarbieRec . Rec.transform @c @r @f @(B.Dict c `Product` f) (Pair (B.Dict @c)) . unBarbieRec
+
+
+
+instance FreeForall r => FunctorB (BarbieVar r) where
+  bmap f = BarbieVar . Var.transform' @r f . unBarbieVar
+
+instance FreeForall r => TraversableB (BarbieVar r) where
+  btraverse :: forall e f g. Applicative e => (forall a. f a -> e (g a)) -> BarbieVar r f -> e (BarbieVar r g)
+  btraverse f  = fmap BarbieVar . Var.traverseMap @Unconstrained1 @e @f @g @r f . unBarbieVar
+
+instance FreeForall r => ConstraintsB (BarbieVar r) where
+  type AllB c (BarbieVar r) = Forall r c
+  baddDicts :: forall c f. Forall r c => BarbieVar r f -> BarbieVar r (B.Dict c `Product` f)
+  baddDicts = BarbieVar . Var.transform @c @r @f @(B.Dict c `Product` f) (Pair (B.Dict @c)) . unBarbieVar