row-types 0.3.1.0 → 0.4.0.0

raw patch · 14 files changed

+2693/−2631 lines, 14 filessetup-changed

Files

• CHANGELOG.md +46/−37
• Data/Row.hs +56/−56
• Data/Row/Internal.hs +573/−573
• Data/Row/Records.hs +706/−685
• Data/Row/Switch.hs +45/−45
• Data/Row/Variants.hs +565/−538
• LICENSE +7/−7
• NOTICE +15/−15
• README.md +21/−21
• Setup.hs +2/−2
• benchmarks/perf/Main.hs +95/−95
• examples/Examples.lhs +441/−441
• row-types.cabal +115/−110
• tests/Main.hs +6/−6

@@ -1,37 +1,46 @@-## 0.3.1.0 [2020-01-29]-- Added "native" classes as exports for `Records` and `Variants` (e.g., `ToNative`, `FromNative`)-- Added more example hs files.--## 0.3.0.0 [2019-05-28]-- Added `HasField` and `AsConstructor` instances (from generic-lens) for `Rec` and `Var` respectively.-- Added record-overwrite function `.//`.-- Added `Generic` instances for Rec and Var.-- Added mapHas entailment connecting `Map f r .! l` to `r .! l`.-- Changed `Forall2` to `BiForall`.-  - Added `BiConstraint` type class for use  with `BiForall`.-- Added `Ap` type family that functions as `ap` over rows using zipping.-  - Added `mapF` to map a function over a record with an `Ap` row.-- Added `toDynamicMap` and `fromDynamicMap` as functions to convert between `Rec`s and  `HashMap Text Dynamic`s.-- Added `toNativeExact` to convert a `Rec` to a native Haskell type without losing any fields.-- Added `toNative`, `fromNative`, and `fromNativeExact` for `Var`s.-- Added `unSingleton` for `Var`s.-  - Removed `unSingleton` from `Data.Row` export list.-- Tightened the type signatures of `focus` (for both `Rec` and `Var`) to improve type inference when using `focus` in lens-like situations.--## 0.2.3.1 [2018-07-11]-- Fix a bug in the `Show` instance for `Rec`.--## 0.2.3.0 [2018-07-02]-- Update the `Show` instance for `Rec` to render valid code.-- Add `toNative` and `fromNative` functions for records to easily convert between Haskell records and row-types records.-- Make type families in `Data.Row.Internal` polykinded (thanks James Yu!)--## 0.2.1.0 [2018-03-20]-- Bug Fix: The type of `update` for both `Rec` and `Var` now enforce the newly inserted type is correct.-- New: Add `restrict` and `split` for `Var`s.  -  - Removed `restrict` from `Data.Row` export list.-- New: Added support for universally quantified rows: `mapForall` and `uniqueMap`.-- Added very simple test suite.--## 0.2.0.0 [2018-02-12]-- Initial Release+## 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`.
+- Added `coerceRec` and `coerceVar` to coerce the row-types of records and variants respectively.
+- 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.
+
+## 0.3.1.0 [2020-01-29]
+- Added "native" classes as exports for `Records` and `Variants` (e.g., `ToNative`, `FromNative`)
+- Added more example hs files.
+
+## 0.3.0.0 [2019-05-28]
+- Added `HasField` and `AsConstructor` instances (from generic-lens) for `Rec` and `Var` respectively.
+- Added record-overwrite function `.//`.
+- Added `Generic` instances for Rec and Var.
+- Added mapHas entailment connecting `Map f r .! l` to `r .! l`.
+- Changed `Forall2` to `BiForall`.
+  - Added `BiConstraint` type class for use  with `BiForall`.
+- Added `Ap` type family that functions as `ap` over rows using zipping.
+  - Added `mapF` to map a function over a record with an `Ap` row.
+- Added `toDynamicMap` and `fromDynamicMap` as functions to convert between `Rec`s and  `HashMap Text Dynamic`s.
+- Added `toNativeExact` to convert a `Rec` to a native Haskell type without losing any fields.
+- Added `toNative`, `fromNative`, and `fromNativeExact` for `Var`s.
+- Added `unSingleton` for `Var`s.
+  - Removed `unSingleton` from `Data.Row` export list.
+- Tightened the type signatures of `focus` (for both `Rec` and `Var`) to improve type inference when using `focus` in lens-like situations.
+
+## 0.2.3.1 [2018-07-11]
+- Fix a bug in the `Show` instance for `Rec`.
+
+## 0.2.3.0 [2018-07-02]
+- Update the `Show` instance for `Rec` to render valid code.
+- Add `toNative` and `fromNative` functions for records to easily convert between Haskell records and row-types records.
+- Make type families in `Data.Row.Internal` polykinded (thanks James Yu!)
+
+## 0.2.1.0 [2018-03-20]
+- Bug Fix: The type of `update` for both `Rec` and `Var` now enforce the newly inserted type is correct.
+- New: Add `restrict` and `split` for `Var`s.  
+  - Removed `restrict` from `Data.Row` export list.
+- New: Added support for universally quantified rows: `mapForall` and `uniqueMap`.
+- Added very simple test suite.
+
+## 0.2.0.0 [2018-02-12]
+- Initial Release

@@ -1,56 +1,56 @@--------------------------------------------------------------------------------- |--- 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 (.//)-  , 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+-----------------------------------------------------------------------------
+-- |
+-- 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 +1,573 @@-{-# 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+{-# 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,685 +1,706 @@--------------------------------------------------------------------------------- |--- 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-  , toNative, toNativeExact, fromNative-  , ToNative, ToNativeExact, FromNative-  -- * Dynamic Conversion-  , toDynamicMap, fromDynamicMap-  -- * Row operations-  -- ** Map-  , Map, map, map', mapF-  , transform, transform'-  -- ** Fold-  , Forall, erase, eraseWithLabels, eraseZip, eraseToHashMap-  -- ** Zip-  , Zip, zip-  -- ** Sequence-  , sequence, sequence'-  -- ** Compose-  -- $compose-  , compose, uncompose-  , compose', uncompose'-  -- ** Labels-  , labels, labels'-  -- ** UNSAFE operations-  , unsafeRemove, unsafeInjectFront-  )-where--import Prelude hiding (map, sequence, zip)--import Control.DeepSeq (NFData(..), deepseq)--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 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----- | 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.  This means that--- we can't use metamorph and that we must use an overlappable instance for--- larger records.--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--type family RepRec (r :: Row *) :: * -> * where-  RepRec (R '[])                 = G.U1-  RepRec (R (name :-> t ': '[])) = G.S1-    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)-    (G.Rec0 t)-  RepRec (R (name :-> t ': r))   = (G.S1-    ('G.MetaSel ('Just name) 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)-    (G.Rec0 t)) G.:*: RepRec (R r)--class GenericRec r where-  fromRec :: Rec r -> RepRec r x-  toRec   :: RepRec r x -> Rec r--instance GenericRec Empty where-  fromRec _ = G.U1-  toRec _ = empty--instance KnownSymbol name => GenericRec (R '[name :-> t]) where-  fromRec (_ :== a) = G.M1 (G.K1 a)-  toRec (G.M1 (G.K1 a)) = (Label @name) :== a--instance {-# OVERLAPPABLE #-}-    ( GenericRec (R r)-    , KnownSymbol name-    , r ~ (name' :-> t' ': r') -- r is not Empty-    ) => GenericRec (R (name :-> t ': r)) where-  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'.  That--- said, they do not compose to form the identity because 'toNative' allows--- fields to be dropped: a record with excess fields can still be transformed--- to a native type, but when the native type is converted to a record, the--- fields are exactly transformed.  Because of this, 'toNative' 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" }------ The 'toNativeExact' function is a more restricted version of 'toNative' that--- does not allow fields to be dropped; in other words, the fields in the record--- must exactly match the fields in the data type.  Because of this, 'toNativeExact'--- and 'fromNative' compose to form the identity function.----- | 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 ρ -> 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, ρ .! name ≈ t)-    => 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 ρ)-    => ToNativeG (l G.:*: r) ρ where-  toNative' r = toNative' r G.:*: toNative' r--type ToNative t ρ = (G.Generic t, ToNativeG (G.Rep t) ρ)---- | Convert a record to a native Haskell type.-toNative :: ToNative t ρ => Rec ρ -> 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 ToNativeExactG a ρ where-  toNativeExact' :: Rec ρ -> a x--instance ToNativeExactG cs ρ => ToNativeExactG (G.D1 m cs) ρ where-  toNativeExact' xs = G.M1 $ toNativeExact' xs--instance ToNativeExactG cs ρ => ToNativeExactG (G.C1 m cs) ρ where-  toNativeExact' xs = G.M1 $ toNativeExact' xs--instance ToNativeExactG G.U1 Empty where-  toNativeExact' _ = G.U1--instance (KnownSymbol name, ρ ≈ name .== t)-    => ToNativeExactG (G.S1 ('G.MetaSel ('Just name) p s l) (G.Rec0 t)) ρ where-  toNativeExact' r = G.M1 $ G.K1 $ r .! (Label @name)--instance (ToNativeExactG l ρ₁, ToNativeExactG r ρ₂, ρ ≈ ρ₁ .+ ρ₂, Disjoint ρ₁ ρ₂)-    => ToNativeExactG (l G.:*: r) ρ where-  toNativeExact' r = toNativeExact' r1 G.:*: toNativeExact' r2-    where-      (r1 :: Rec ρ₁) :+ (r2 :: Rec ρ₂) = r--type ToNativeExact t ρ = (G.Generic t, ToNativeExactG (G.Rep t) ρ)---- | Convert a record to an exactly matching native Haskell type.-toNativeExact :: ToNativeExact t ρ => Rec ρ -> t-toNativeExact = G.to . toNativeExact'----- | 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 ρ--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 Empty where-  fromNative' G.U1 = empty--instance (KnownSymbol name, ρ ≈ name .== t)-    => 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 ρ-fromNative = fromNative' . G.from---{---------------------------------------------------------------------  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' #-}+-----------------------------------------------------------------------------
+-- |
+-- 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 +1,45 @@-{-# 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+{-# 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,538 +1,565 @@--------------------------------------------------------------------------------- |--- 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, fromNativeExact-  , ToNative, FromNative, FromNativeExact-  -- * Row operations-  -- ** Map-  , Map, map, map', transform, transform'-  -- ** Fold-  , Forall, erase, eraseWithLabels, eraseZip-  -- ** Sequence-  , sequence-  -- ** Compose-  -- $compose-  , compose, uncompose-  -- ** labels-  , labels-  -- ** 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.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 (VMap x) = impossible x-    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 (VMap2 x) = impossible x-    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 (VMap x) = impossible x-    doUncons l = right VMap . flip trial l . unVMap-    doCons l (Left (Compose x)) = VMap2 $ unsafeMakeVar l x-    doCons _ (Right (VMap2 v)) = VMap2 $ unsafeInjectFront v---{---------------------------------------------------------------------  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.  This means that--- we can't use metamorph and that we must use an overlappable instance for--- larger variants.--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--type family RepVar (r :: Row *) :: * -> * where-  RepVar (R '[])                 = G.V1-  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))-  RepVar (R (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 r)--class GenericVar r where-  fromVar :: Var r -> RepVar r x-  toVar   :: RepVar r x -> Var r--instance GenericVar Empty where-  fromVar = impossible-  toVar = \case--instance KnownSymbol name => GenericVar (R '[name :-> t]) where-  fromVar (unSingleton -> (_, a)) = G.M1 (G.M1 (G.K1 a))-  toVar (G.M1 (G.M1 (G.K1 a))) = IsJust (Label @name) a--instance {-# OVERLAPPABLE #-}-    ( GenericVar (R r)-    , KnownSymbol name-    , r ~ (name' :-> t' ': r') -- r is not Empty-    , AllUniqueLabels (R (name :-> t ': r))-    ) => GenericVar (R (name :-> t ': r)) where-  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.--- That said, they do not compose to form the identity because 'fromNative' allows--- constructors to be added: a variant with excess options can still be transformed--- to a native type, but when the native type is converted to a variant, the--- options are exactly transformed.  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}------ The 'fromNativeExact' function is a more restricted version of 'fromNative' that--- does not allow options to be added; in other words, the options in the variant--- must exactly match the constructors in the data type.  Because of this,--- 'fromNativeExact' and 'toNative' compose to form the identity function.----- | 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 ρ -> a x--instance ToNativeG cs ρ => ToNativeG (G.D1 m cs) ρ where-  toNative' = G.M1 . toNative'--instance ToNativeG G.V1 Empty where-  toNative' = impossible--instance (KnownSymbol name, ρ ≈ name .== t)-    => 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 ρ₂, ρ₂ ≈ ρ .\\ ρ₁, ρ ≈ ρ₁ .+ ρ₂-         , AllUniqueLabels ρ₁, Forall ρ₂ Unconstrained1)-    => ToNativeG (l G.:+: r) ρ where-  toNative' v = case multiTrial @ρ₁ @ρ 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 ρ -> 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 ρ--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, ρ .! name ≈ t, AllUniqueLabels ρ)-    => 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 ρ-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 FromNativeExactG a ρ where-  fromNativeExact' :: a x -> Var ρ--instance FromNativeExactG cs ρ => FromNativeExactG (G.D1 m cs) ρ where-  fromNativeExact' (G.M1 v) = fromNativeExact' v--instance FromNativeExactG G.V1 Empty where-  fromNativeExact' = \ case--instance (KnownSymbol name, ρ ≈ name .== t)-    => FromNativeExactG (G.C1 ('G.MetaCons name fixity sels)-                       (G.S1 m (G.Rec0 t))) ρ where-  fromNativeExact' (G.M1 (G.M1 (G.K1 x))) = IsJust (Label @name) x--instance (FromNativeExactG l ρ₁, FromNativeExactG r ρ₂, ρ ≈ ρ₁ .+ ρ₂)-    => FromNativeExactG (l G.:+: r) ρ where-  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it-  -- makes the constraints really hairy.-  fromNativeExact' (G.L1 x) = unsafeCoerce $ fromNativeExact' @l @ρ₁ x-  fromNativeExact' (G.R1 y) = unsafeCoerce $ fromNativeExact' @r @ρ₂ y--type FromNativeExact t ρ = (G.Generic t, FromNativeExactG (G.Rep t) ρ)---- | Convert a Haskell record to a row-types Var.-fromNativeExact :: FromNativeExact t ρ => t -> Var ρ-fromNativeExact = fromNativeExact' . 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' #-}+-----------------------------------------------------------------------------
+-- |
+-- 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,7 +1,7 @@-Copyright (c) 2017 Target Brands, Inc.--Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:--The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.--THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.+Copyright (c) 2017 Target Brands, Inc.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -1,15 +1,15 @@-This software package includes open source components, each of which is subject to its respective license as listed below:----------------------------------------------------------------------------------- CTRex (commit 5cf771e3c6650351b2aad08d5bd8e94a87ec326d) https://github.com/atzeus/CTRex/blob/master/LICENSE--Copyright (c) 2015, Atze van der Ploeg-All rights reserved.--Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:--1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.--2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.--3. Neither the name of the Atze van der Ploeg nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.+This software package includes open source components, each of which is subject to its respective license as listed below:
+
+-------------------------------------------------------------------------------
+- CTRex (commit 5cf771e3c6650351b2aad08d5bd8e94a87ec326d) https://github.com/atzeus/CTRex/blob/master/LICENSE
+
+Copyright (c) 2015, Atze van der Ploeg
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the Atze van der Ploeg nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

@@ -1,21 +1,21 @@-Row-Types-=======--[![Build Status](https://api.travis-ci.org/target/row-types.svg?branch=master)](https://travis-ci.org/target/row-types/branches)-[![Hackage](https://img.shields.io/hackage/v/row-types.svg)](https://hackage.haskell.org/package/row-types)--Row-types is a library of open records and variants for Haskell using closed-type families and type literals (among other things...).-See [examples/Examples.lhs](https://raw.githubusercontent.com/target/row-types/master/examples/Examples.lhs)-for a literate Haskell file that functions as an overview of how this library can be used,-and check out [the website](https://target.github.io/row-types/) for further examples.--Available on [Hackage](https://hackage.haskell.org/package/row-types).--This work is a branch from CTRex [1,2] with other inspiration from data-diverse [3].-My thanks to the authors and contributors of those libraries!---[1] https://wiki.haskell.org/CTRex \-[2] https://hackage.haskell.org/package/CTRex/docs/Data-OpenRecords.html \-[3] https://hackage.haskell.org/package/data-diverse+Row-Types
+=======
+
+[![Build Status](https://api.travis-ci.org/target/row-types.svg?branch=master)](https://travis-ci.org/target/row-types/branches)
+[![Hackage](https://img.shields.io/hackage/v/row-types.svg)](https://hackage.haskell.org/package/row-types)
+
+Row-types is a library of open records and variants for Haskell using closed
+type families and type literals (among other things...).
+See [examples/Examples.lhs](https://raw.githubusercontent.com/target/row-types/master/examples/Examples.lhs)
+for a literate Haskell file that functions as an overview of how this library can be used,
+and check out [the website](https://target.github.io/row-types/) for further examples.
+
+Available on [Hackage](https://hackage.haskell.org/package/row-types).
+
+This work is a branch from CTRex [1,2] with other inspiration from data-diverse [3].
+My thanks to the authors and contributors of those libraries!
+
+
+[1] https://wiki.haskell.org/CTRex \
+[2] https://hackage.haskell.org/package/CTRex/docs/Data-OpenRecords.html \
+[3] https://hackage.haskell.org/package/data-diverse

@@ -1,2 +1,2 @@-import Distribution.Simple-main = defaultMain+import Distribution.Simple
+main = defaultMain

@@ -1,95 +1,95 @@-module Main (main) where--import Criterion.Main--import Data.String--import Data.Row.Records--type FourRecord a =-     "i0" .== a   .+ "i1" .== a   .+ "i2" .== a   .+ "i3"   .== a--type ElevenRecord a =-     "i0"  .== a  .+ "i1"  .== a  .+ "i2"  .== a  .+ "i3"   .== a-  .+ "i10" .== a  .+ "i11" .== a  .+ "i12" .== a  .+ "i13"  .== a-  .+ "i20" .== a  .+ "i21" .== a  .+ "i22" .== a--type SixteenRecord 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--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--main :: IO ()-main =-  defaultMain-    [ bgroup "Record Construction"-        [ bench "simple 1"  $ nf (#a .==) ()-        , bench "simple 4"  $ nf id $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()-        , bench "reverse 4" $ nf id $ #d .== () .+ #c .== () .+ #b .== () .+ #a .== ()-        , bench "default 4" $ nf id $ default' @Num @(FourRecord Double) 0-        , bench "recordFromLabels 4" $ nf id $ fromLabels @IsString @(FourRecord String) (fromString . show)-        , bench "default 11" $ nf id $ default' @Num @(ElevenRecord Double) 0-        , 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)-        ]-    , bgroup "Record Append"-        [ bench "append 3 3" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== (),   #d .== () .+ #e .== () .+ #f .== ())-        , bench "append 5 1" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== (),   #f .== ())-        , bench "append 1 5" $ nf (uncurry (.+)) (#a .== (),   #b .== () .+ #c .== () .+ #d .== () .+ #e .== () .+ #f .== ())-        ]-    , 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 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-        ]-    , bgroup "Record Metamorphosis"-        [ bench "erase 4"  $ nf (erase @Show show) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()-        , bench "erase 64" $ nf (erase @Show show) $ my64Record-        ]-    ]+module Main (main) where
+
+import Criterion.Main
+
+import Data.String
+
+import Data.Row.Records
+
+type FourRecord a =
+     "i0" .== a   .+ "i1" .== a   .+ "i2" .== a   .+ "i3"   .== a
+
+type ElevenRecord a =
+     "i0"  .== a  .+ "i1"  .== a  .+ "i2"  .== a  .+ "i3"   .== a
+  .+ "i10" .== a  .+ "i11" .== a  .+ "i12" .== a  .+ "i13"  .== a
+  .+ "i20" .== a  .+ "i21" .== a  .+ "i22" .== a
+
+type SixteenRecord 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
+
+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
+
+main :: IO ()
+main =
+  defaultMain
+    [ bgroup "Record Construction"
+        [ bench "simple 1"  $ nf (#a .==) ()
+        , bench "simple 4"  $ nf id $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()
+        , bench "reverse 4" $ nf id $ #d .== () .+ #c .== () .+ #b .== () .+ #a .== ()
+        , bench "default 4" $ nf id $ default' @Num @(FourRecord Double) 0
+        , bench "recordFromLabels 4" $ nf id $ fromLabels @IsString @(FourRecord String) (fromString . show)
+        , bench "default 11" $ nf id $ default' @Num @(ElevenRecord Double) 0
+        , 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)
+        ]
+    , bgroup "Record Append"
+        [ bench "append 3 3" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== (),   #d .== () .+ #e .== () .+ #f .== ())
+        , bench "append 5 1" $ nf (uncurry (.+)) (#a .== () .+ #b .== () .+ #c .== () .+ #d .== () .+ #e .== (),   #f .== ())
+        , bench "append 1 5" $ nf (uncurry (.+)) (#a .== (),   #b .== () .+ #c .== () .+ #d .== () .+ #e .== () .+ #f .== ())
+        ]
+    , 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 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
+        ]
+    , bgroup "Record Metamorphosis"
+        [ bench "erase 4"  $ nf (erase @Show show) $ #a .== () .+ #b .== () .+ #c .== () .+ #d .== ()
+        , bench "erase 64" $ nf (erase @Show show) $ my64Record
+        ]
+    ]

@@ -1,441 +1,441 @@-> {-# LANGUAGE OverloadedLabels #-}-> {-# LANGUAGE DeriveGeneric #-}-> {-# LANGUAGE PartialTypeSignatures #-}-> module Examples where->-> import Data.Row-> import qualified Data.Row.Records as Rec-> import qualified Data.Row.Variants as Var--In this example file, we will explore how to create and use records and variants.-----------------------------------------------------------------------------------  LABELS-----------------------------------------------------------------------------------To begin, we will briefly discuss creating labels -- their use will follow.--The most basic way to create a label is through construction with a type signature:-- x = Label :: Label "x"--With the above definition, x is a label for the field x.  Using type applications,-this can be shortened to:-- x = Label @"x"--And with OverloadedLabels, one can just write:-- #x--We will use the OverloadedLabels notation in these examples.-----------------------------------------------------------------------------------  LENS-----------------------------------------------------------------------------------Records and variants play nicely with the lens library if we additionally import-Data.Generics.Labels from the generic-lens library.  Each overloaded-label is also a Lens for a record and a prism for variants.  Thus, .! can be-replaced with ^. and trial' can be made infix with ^?.  Additionally, update-can be made infix:--update #x v r === r & #x .~ v--And because of the power of lens, it's easy to make modifications rather than-just update:--update #x (f (r .! #x)) r === r & #x %~ f--Lens is not included with row-types by default, but using it can make row-types-much friendlier.  For this example module, we'll include a couple of handy lens-operations:--> import Data.Generics.Labels ()-> import Data.Generics.Internal.VL.Lens->-> infixl 6 &-> (&) :: a -> (a -> b) -> b-> (&) = flip ($)-> (%~) = over-----------------------------------------------------------------------------------  RECORDS-----------------------------------------------------------------------------------With some labels defined, let's begin with records.  To start, let's create a-record representing the Cartesian coordinates of the origin.  To do this,-we use the .== operator to initialize values in a record, and we separate each-initialized value with the .+ operator.Notice that the value level code uses the-same operators as the type level code.--> origin :: Rec ("x" .== Double .+ "y" .== Double )-> origin = #x .== 0 .+ #y .== 0--Note that, although we wrote the type explicitly, GHC has no problem inferring-it exactly.--If we show this at the repl, we see:-λ> origin- #x .== 0.0 .+ #y .== 0.0--Of course, as an extensible record, the order that we build it shouldn't matter,-and indeed, it doesn't.  Consider the following variation:--> origin' :: Rec ("y" .== Double .+ "x" .== Double)-> origin' = #y .== 0 .+ #x .== 0--If we show this at the repl, we see:--λ> origin'- #x .== 0.0 .+ #y .== 0.0--Indeed, the two values are indistinguishable:--λ> origin == origin'-True--Now, let's expand upon our record.  Why stop at two dimensions when we can make-a record in three dimensions.--> origin3D = #z .== 0.0 .+ origin--Once again, the type is inferred for us, and the record is exactly as expected.--In fact, we can do this generally.  The following function takes a name and a-record and adds the "name" field to that record with the given name.--> named :: a -> Rec r -> Rec ("name" .== a .+ r)-> named s r = #name .== s .+ r--Note that we require that the record we are naming must not have a "name" field-already.  Overlapping labels within a single record/variant is strictly forbidden.--Let's say we want to get the values out of the record.  Simple selection is achieved-with the .! operator, like so:--λ> origin .! #x-0.0--and we can use this to write whatever we want.  Here is a function for calculating-Euclidean distance from the origin to a point:--> distance :: (Floating t, r .! "y" ≈ t, r .! "x" ≈ t) => Rec r -> t-> distance p = sqrt $ p .! #x * p .! #x + p .! #y * p .! #y--Once again, the type of distance is entirely inferrable, but we write it here for-convenience.  This works exactly as expected:--λ> distance origin-0.0-λ> distance origin3D-0.0-λ> distance (named "2D" origin)-0.0--Of course, that wasn't very interesting when our only points are at the origin-already.  We could make new records representing new points, but instead, let's-write a function to move the points we have:--> move :: (Num (r .! "x"), Num (r .! "y"))->      => Rec r -> r .! "x" -> r .! "y" -> Rec r-> move p dx dy = Rec.update #x (p .! #x + dx) $->                Rec.update #y (p .! #y + dy) p--Here, we're using the Rec.update operator to update the value at the label x by-adding dx to it, and then we do the same for y.-We can see it work in practice:--λ> move origin 3 4- #x .== 3.0 .+ #y .== 4.0-λ> distance (move origin 3 4)-5.0-λ> 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:--> moveLensy p dx dy = p & #x %~ (+ dx) & #y %~ (+ dy)--So far, we created an origin point in 2d and then one in 3d, but what if we are-adventurous mathematicians who want to have points in a space with some arbitrary-number of dimensions.  We could write out each of the 0s necessary, but there's-an easier way to initialize a record:--> origin4 :: Rec ("x" .== Double .+ "y" .== Double .+ "z" .== Double .+ "w" .== Double)-> origin4 = Rec.default' @Num 0--Finally, we have come to a case where GHC cannot infer the type signature, and how-could it!  The type is providing crucial information about the shape of the record.-Regardless, with the type provided, it works exactly as expected:--λ> origin4- #w .== 0.0 .+ #x .== 0.0 .+ #y .== 0.0 .+ #z .== 0.0--While we have added names or further fields, we can also choose to forget-information in a record.  To remove a particular label, one can use the .--operator, like so:--> unName :: HasType "name" a r => Rec r -> Rec (r .- "name")-> unName r = r .- #name--For larger changes, it is easier to use the restrict function.  The following-function will take a record that contains both an x and y coordinate and remove-the rest of the fields from it.--> get2D :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)->       => Rec (r .+ rest)->       -> Rec r-> get2D r = Rec.restrict r--GHC is a little finicky about the type operators and constraints -- indeed, some-slight modifications to the signature can easily cause type checking to fail.-However, a type signature is not necessary when-using type applications, and the function can instead be written as:--> get2D' r = Rec.restrict @("x" .== Double .+ "y" .== Double) r--with no trouble.  Yet another altnerative is to match directly on the values desired-using the :== and :+ record patterns:--> get2D'' :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)->         => Rec (r .+ rest)->         -> Rec r-> get2D'' ((Label :: Label "x") :== n1 :+ (Label :: Label "y") :== n2 :+ _)->           = #x .== n1 .+ #y .== n2--(Note that overloaded labels cannot be used in the patterns, so the notation is-unfortunately bloated by types.  Also, the type operators are left associated,-so the "_" must go on the right, and the type signature is unforunately necessary.)--All three of the get2D functions behave the same.-----------------------------------------------------------------------------------  VARIANTS----------------------------------------------------------------------------------Let's move on from records to variants.  In many ways, variants are quite similar,-as might be expected given that variants are dual to records.  The types look-almost the same, and some of the operators are shared as well.  However,-construction and destruction are obviously different.--Creating a variant can be done with IsJust:--> v,v' :: Var ("y" .== String .+ "x" .== Integer)-> v  = IsJust #x 1-> v' = IsJust #y "Foo"--Here, the type is necessary to specify what concrete type the variant is (when-using AllowAmbiguousTypes, the type is not always needed, but it would be needed-to e.g. show the variant).  In the simple case of a variant of just one type,-the simpler singleton function can be used:--> v2 = Var.singleton #x 1--Now, the type can be easily derived by GHC.  We can show variants as easily as-records:--λ> v-{x=1}-λ> v'-{y="Foo"}-λ> v2-{x=1}--Once created, a variant can be expanded by using type applications and the-diversify function.--> v3 = diversify @("y" .== String) v2-> v4 = diversify @("y" .== String .+ "z" .== Double) v2--λ> :t v4-v4 :: Var ('R '["x" ':-> Integer, "y" ':-> String, "z" ':-> Double])-λ> v == v3-True--The diversify function makes use of the .\/ type class, pronounced min-join.-The min-join of two row-types is the minimum row-type that contains all the-bindings of the two constituent ones.  This allows use to write a function to-join two lists of variants:--> joinVarLists :: forall x y. (WellBehaved (x .\/ y), x .\/ y ≈ y .\/ x)->              => [Var x] -> [Var y] -> [Var (x .\/ y)]-> joinVarLists xs ys = map (diversify @y) xs ++ map (diversify @x) ys--Unfortunately, GHC cannot deduce that the min-join of x and y is the same as the-min-join of y and x, so  we must add that to the constraints.  However, any concrete-types x and y that we construct will have this property, so it is easy to dispatch-when we go to use this function.--Taking a step back, it's worth looking closer at the equality tests we did earlier-on variants.  Indeed, one may ask how equality works on variants at all.-For instance, v2 and v3 both look the same when you show them, and they-both have the same value inside, but can we test them for equality?  Indeed, we can't,-precisely because their types are different: it is a type error to even try to-check whether they're equal:--λ> v2 == v3-error:-    • Couldn't match type ‘'["y" ':-> [Char]]’ with ‘'[]’-      Expected type: Var ('R '["x" ':-> Integer])-        Actual type: Var ('R '["x" ':-> Integer] .+ ("y" .== String))-    • In the second argument of ‘(==)’, namely ‘v3’-      In the expression: v2 == v3-      In an equation for ‘it’: it = v2 == v3--This may look a little scary, but it's actually a pretty useful message.  Essentially,-it's expecting a variant that can only be an Integer at label "x", but it found one-that could also be a String at label "y".  So, comparing v2 and v3 is not allowed,-but since v3 now has the same labels as v1, that comparison is fine:--λ> v == v3-True-λ> v == IsJust #x 3-False-λ> v == v'-False-λ> v == IsJust #y "fail"-False--(Also note here that using IsJust without a type signature is fine because the correct-type can be easily inferred due to v's type.)--What can you do with a variant?  The only way to really use one is to get the value-out, and to do that, you must trial it:--λ> trial v #x-Left 1-λ> trial v #y-Right {x=1}-λ> trial v' #x-Right {y="Foo"}-λ> trial v' #y-Left "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-trial failed, we now can be sure that the value is not from l.-----------------------------------------------------------------------------------Note on lenses:-The generic-lens library distinguishes labels that are meant to be lens from labels-meant to be prisms by whether the front of the label is an underscore followed by-an uppercase letter.  This makes a lot of sense for data constructors, which is what-generic-lens's prisms were designed for, but it's a little restrictive for variants.-The result is that we can only use the lensy notation if the labels in our variants-are uppercase.  Consider the following:--> vUpper :: Var ("Y" .== String .+ "X" .== Integer)-> vUpper = IsJust (Label @"X") 1--λ> v ^? #_X-Left 1--The row-types library does not generally assert that variants need labels that-start with uppercase letters while records need labels that start with lowercase-letters---in fact, the `switch` function described below will only work if the-labels in a record and variant are exactly the same---but GHC is limited in that-the # syntax only works for lowercase labels.  Therefore, to make uppercase labels-like in the `vUpper` example above, one must use the syntax `Label @"X"` instead-of simply `#X`.  See the proposal in https://github.com/ghc-proposals/ghc-proposals/pull/170-for more information.-----------------------------------------------------------------------------------For ease of use in view patterns, Variants also exposes the view function.-(If using lens, this can be replaced with preview.)  With it, we can write a-function like this:--> myShow :: (r .! "y" ≈ String, Show (r .! "x")) => Var r -> String-> myShow (Var.view #x -> Just n) = "Showable of "++show n-> myShow (Var.view #y -> Just s) = "String of "++s-> myShow _ = "Unknown"--λ> myShow v-"Showable of 1"-λ> myShow v'-"String of Foo"-λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))-"Unknown"--This can also be achieved with the IsJust pattern synonym in much the same way:--> myShow' :: (WellBehaved r, r .! "y" ≈ String, Show (r .! "x")) => Var r -> String-> myShow' (IsJust (Label :: Label "x") n) = "Showable of "++show n-> myShow' (IsJust (Label :: Label "y") s) = "String of "++s-> myShow' _ = "Unknown"--In either case, the type signature is once again totally derivable.--There are three minor annoyances with this.  First, it's annoying to have to write-out the Label types in the pattern.  This is actually a requested issue on GHC-(see https://gitlab.haskell.org/ghc/ghc/issues/13116 and-https://github.com/ghc-proposals/ghc-proposals/pull/80 for more information).-Second, it's fairly common to want to define-a function like myShow to be exhaustive in the variant's cases, but to do this,-you must manually provide a type signature:--> myShowRestricted :: Var ("y" .== String .+ "x" .== Integer) -> String-> myShowRestricted (Var.view #x -> Just n) = "Integer of "++show n-> myShowRestricted (Var.view #y -> Just s) = "String of "++s-> myShowRestricted _ = error "Unreachable"--The final blemish can be seen in this restricted version of myShow.  Even though-we know from the type that we've covered all the posibilities of the variant, GHC-will generate a "non-exhaustive pattern match" warning without the final line.-(This is true for the pattern synonym version too.)--One way to avoid this problem is to use switch.  The switch operator takes a variant-and a record such that for each label that the variant has, the record has a function-at that label that consumes the value the variant has and produces a value in a-common type.  Essentially, switch "applies" the variant to the record to produce-an output value.--> --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String-> myShowRestricted' v = switch v $->      #x .== (\n -> "Integer of "++show n)->   .+ #y .== (\s -> "String of "++s)--This version of myShow needs neither a type signature (it is inferred exactly) nor-a default "unreachable" case.  However, we no longer have the benefit of Haskell's-standard pattern matching.---A more powerful version of trial is multiTrial, which tests for multiple labels-at once.  With this, you can wholesale change the type of the variant to any (valid)-variant type you would like.  Of course, there needs to be a recourse if the variant-you provide is not expressible in the type you want, so multiTrial returns an Either-of the type you want or a Variant of the leftovers.  Consider the examples:--λ> :t multiTrial @("x" .== Double .+ "y" .== String) v-multiTrial @("x" .== Double .+ "y" .== String) v-  :: Either-       (Var ('R '["x" ':-> Double, "y" ':-> String]))-       (Var ('R '["x" ':-> Integer]))-λ> multiTrial @("x" .== Double .+ "y" .== String) v-Right {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]))-λ> multiTrial @("x" .== Double .+ "y" .== String) v'-Left {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-from one where "x" is an Integer to one where it's a Double).  We can even use-it to combine dispatching of two different variants at once:--> also :: Disjoint xs ys->      => (Var xs -> a)->      -> (Var ys -> a)->      -> Var (xs .+ ys) -> a-> also f1 f2 e = case multiTrial e of->   Left  e' -> f1 e'->   Right e' -> f2 e'--The above also function takes two functions f1 and f2 that can each independently-be used on variants with rows xs and ys respectively.  Using multiTrial, we can-split the input variant (which is the join of xs and ys) and easily apply f1 or-f2 as appropriate.+> {-# LANGUAGE OverloadedLabels #-}
+> {-# LANGUAGE DeriveGeneric #-}
+> {-# LANGUAGE PartialTypeSignatures #-}
+> module Examples where
+>
+> import Data.Row
+> import qualified Data.Row.Records as Rec
+> import qualified Data.Row.Variants as Var
+
+In this example file, we will explore how to create and use records and variants.
+
+--------------------------------------------------------------------------------
+  LABELS
+--------------------------------------------------------------------------------
+
+To begin, we will briefly discuss creating labels -- their use will follow.
+
+The most basic way to create a label is through construction with a type signature:
+
+ x = Label :: Label "x"
+
+With the above definition, x is a label for the field x.  Using type applications,
+this can be shortened to:
+
+ x = Label @"x"
+
+And with OverloadedLabels, one can just write:
+
+ #x
+
+We will use the OverloadedLabels notation in these examples.
+
+--------------------------------------------------------------------------------
+  LENS
+--------------------------------------------------------------------------------
+
+Records and variants play nicely with the lens library if we additionally import
+Data.Generics.Labels from the generic-lens library.  Each overloaded
+label is also a Lens for a record and a prism for variants.  Thus, .! can be
+replaced with ^. and trial' can be made infix with ^?.  Additionally, update
+can be made infix:
+
+update #x v r === r & #x .~ v
+
+And because of the power of lens, it's easy to make modifications rather than
+just update:
+
+update #x (f (r .! #x)) r === r & #x %~ f
+
+Lens is not included with row-types by default, but using it can make row-types
+much friendlier.  For this example module, we'll include a couple of handy lens
+operations:
+
+> import Data.Generics.Labels ()
+> import Data.Generics.Internal.VL.Lens
+>
+> infixl 6 &
+> (&) :: a -> (a -> b) -> b
+> (&) = flip ($)
+> (%~) = over
+
+--------------------------------------------------------------------------------
+  RECORDS
+--------------------------------------------------------------------------------
+
+With some labels defined, let's begin with records.  To start, let's create a
+record representing the Cartesian coordinates of the origin.  To do this,
+we use the .== operator to initialize values in a record, and we separate each
+initialized value with the .+ operator.Notice that the value level code uses the
+same operators as the type level code.
+
+> origin :: Rec ("x" .== Double .+ "y" .== Double )
+> origin = #x .== 0 .+ #y .== 0
+
+Note that, although we wrote the type explicitly, GHC has no problem inferring
+it exactly.
+
+If we show this at the repl, we see:
+λ> origin
+ #x .== 0.0 .+ #y .== 0.0
+
+Of course, as an extensible record, the order that we build it shouldn't matter,
+and indeed, it doesn't.  Consider the following variation:
+
+> origin' :: Rec ("y" .== Double .+ "x" .== Double)
+> origin' = #y .== 0 .+ #x .== 0
+
+If we show this at the repl, we see:
+
+λ> origin'
+ #x .== 0.0 .+ #y .== 0.0
+
+Indeed, the two values are indistinguishable:
+
+λ> origin == origin'
+True
+
+Now, let's expand upon our record.  Why stop at two dimensions when we can make
+a record in three dimensions.
+
+> origin3D = #z .== 0.0 .+ origin
+
+Once again, the type is inferred for us, and the record is exactly as expected.
+
+In fact, we can do this generally.  The following function takes a name and a
+record and adds the "name" field to that record with the given name.
+
+> named :: a -> Rec r -> Rec ("name" .== a .+ r)
+> named s r = #name .== s .+ r
+
+Note that we require that the record we are naming must not have a "name" field
+already.  Overlapping labels within a single record/variant is strictly forbidden.
+
+Let's say we want to get the values out of the record.  Simple selection is achieved
+with the .! operator, like so:
+
+λ> origin .! #x
+0.0
+
+and we can use this to write whatever we want.  Here is a function for calculating
+Euclidean distance from the origin to a point:
+
+> distance :: (Floating t, r .! "y" ≈ t, r .! "x" ≈ t) => Rec r -> t
+> distance p = sqrt $ p .! #x * p .! #x + p .! #y * p .! #y
+
+Once again, the type of distance is entirely inferrable, but we write it here for
+convenience.  This works exactly as expected:
+
+λ> distance origin
+0.0
+λ> distance origin3D
+0.0
+λ> distance (named "2D" origin)
+0.0
+
+Of course, that wasn't very interesting when our only points are at the origin
+already.  We could make new records representing new points, but instead, let's
+write a function to move the points we have:
+
+> move :: (Num (r .! "x"), Num (r .! "y"))
+>      => Rec r -> r .! "x" -> r .! "y" -> Rec r
+> move p dx dy = Rec.update #x (p .! #x + dx) $
+>                Rec.update #y (p .! #y + dy) p
+
+Here, we're using the Rec.update operator to update the value at the label x by
+adding dx to it, and then we do the same for y.
+We can see it work in practice:
+
+λ> move origin 3 4
+ #x .== 3.0 .+ #y .== 4.0
+λ> distance (move origin 3 4)
+5.0
+λ> 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:
+
+> moveLensy p dx dy = p & #x %~ (+ dx) & #y %~ (+ dy)
+
+So far, we created an origin point in 2d and then one in 3d, but what if we are
+adventurous mathematicians who want to have points in a space with some arbitrary
+number of dimensions.  We could write out each of the 0s necessary, but there's
+an easier way to initialize a record:
+
+> origin4 :: Rec ("x" .== Double .+ "y" .== Double .+ "z" .== Double .+ "w" .== Double)
+> origin4 = Rec.default' @Num 0
+
+Finally, we have come to a case where GHC cannot infer the type signature, and how
+could it!  The type is providing crucial information about the shape of the record.
+Regardless, with the type provided, it works exactly as expected:
+
+λ> origin4
+ #w .== 0.0 .+ #x .== 0.0 .+ #y .== 0.0 .+ #z .== 0.0
+
+While we have added names or further fields, we can also choose to forget
+information in a record.  To remove a particular label, one can use the .-
+operator, like so:
+
+> unName :: HasType "name" a r => Rec r -> Rec (r .- "name")
+> unName r = r .- #name
+
+For larger changes, it is easier to use the restrict function.  The following
+function will take a record that contains both an x and y coordinate and remove
+the rest of the fields from it.
+
+> get2D :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)
+>       => Rec (r .+ rest)
+>       -> Rec r
+> get2D r = Rec.restrict r
+
+GHC is a little finicky about the type operators and constraints -- indeed, some
+slight modifications to the signature can easily cause type checking to fail.
+However, a type signature is not necessary when
+using type applications, and the function can instead be written as:
+
+> get2D' r = Rec.restrict @("x" .== Double .+ "y" .== Double) r
+
+with no trouble.  Yet another altnerative is to match directly on the values desired
+using the :== and :+ record patterns:
+
+> get2D'' :: (r ≈ "x" .== Double .+ "y" .== Double, Disjoint r rest)
+>         => Rec (r .+ rest)
+>         -> Rec r
+> get2D'' ((Label :: Label "x") :== n1 :+ (Label :: Label "y") :== n2 :+ _)
+>           = #x .== n1 .+ #y .== n2
+
+(Note that overloaded labels cannot be used in the patterns, so the notation is
+unfortunately bloated by types.  Also, the type operators are left associated,
+so the "_" must go on the right, and the type signature is unforunately necessary.)
+
+All three of the get2D functions behave the same.
+
+--------------------------------------------------------------------------------
+  VARIANTS
+--------------------------------------------------------------------------------
+Let's move on from records to variants.  In many ways, variants are quite similar,
+as might be expected given that variants are dual to records.  The types look
+almost the same, and some of the operators are shared as well.  However,
+construction and destruction are obviously different.
+
+Creating a variant can be done with IsJust:
+
+> v,v' :: Var ("y" .== String .+ "x" .== Integer)
+> v  = IsJust #x 1
+> v' = IsJust #y "Foo"
+
+Here, the type is necessary to specify what concrete type the variant is (when
+using AllowAmbiguousTypes, the type is not always needed, but it would be needed
+to e.g. show the variant).  In the simple case of a variant of just one type,
+the simpler singleton function can be used:
+
+> v2 = Var.singleton #x 1
+
+Now, the type can be easily derived by GHC.  We can show variants as easily as
+records:
+
+λ> v
+{x=1}
+λ> v'
+{y="Foo"}
+λ> v2
+{x=1}
+
+Once created, a variant can be expanded by using type applications and the
+diversify function.
+
+> v3 = diversify @("y" .== String) v2
+> v4 = diversify @("y" .== String .+ "z" .== Double) v2
+
+λ> :t v4
+v4 :: Var ('R '["x" ':-> Integer, "y" ':-> String, "z" ':-> Double])
+λ> v == v3
+True
+
+The diversify function makes use of the .\/ type class, pronounced min-join.
+The min-join of two row-types is the minimum row-type that contains all the
+bindings of the two constituent ones.  This allows use to write a function to
+join two lists of variants:
+
+> joinVarLists :: forall x y. (WellBehaved (x .\/ y), x .\/ y ≈ y .\/ x)
+>              => [Var x] -> [Var y] -> [Var (x .\/ y)]
+> joinVarLists xs ys = map (diversify @y) xs ++ map (diversify @x) ys
+
+Unfortunately, GHC cannot deduce that the min-join of x and y is the same as the
+min-join of y and x, so  we must add that to the constraints.  However, any concrete
+types x and y that we construct will have this property, so it is easy to dispatch
+when we go to use this function.
+
+Taking a step back, it's worth looking closer at the equality tests we did earlier
+on variants.  Indeed, one may ask how equality works on variants at all.
+For instance, v2 and v3 both look the same when you show them, and they
+both have the same value inside, but can we test them for equality?  Indeed, we can't,
+precisely because their types are different: it is a type error to even try to
+check whether they're equal:
+
+λ> v2 == v3
+error:
+    • Couldn't match type ‘'["y" ':-> [Char]]’ with ‘'[]’
+      Expected type: Var ('R '["x" ':-> Integer])
+        Actual type: Var ('R '["x" ':-> Integer] .+ ("y" .== String))
+    • In the second argument of ‘(==)’, namely ‘v3’
+      In the expression: v2 == v3
+      In an equation for ‘it’: it = v2 == v3
+
+This may look a little scary, but it's actually a pretty useful message.  Essentially,
+it's expecting a variant that can only be an Integer at label "x", but it found one
+that could also be a String at label "y".  So, comparing v2 and v3 is not allowed,
+but since v3 now has the same labels as v1, that comparison is fine:
+
+λ> v == v3
+True
+λ> v == IsJust #x 3
+False
+λ> v == v'
+False
+λ> v == IsJust #y "fail"
+False
+
+(Also note here that using IsJust without a type signature is fine because the correct
+type can be easily inferred due to v's type.)
+
+What can you do with a variant?  The only way to really use one is to get the value
+out, and to do that, you must trial it:
+
+λ> trial v #x
+Left 1
+λ> trial v #y
+Right {x=1}
+λ> trial v' #x
+Right {y="Foo"}
+λ> trial v' #y
+Left "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
+trial failed, we now can be sure that the value is not from l.
+
+--------------------------------------------------------------------------------
+Note on lenses:
+The generic-lens library distinguishes labels that are meant to be lens from labels
+meant to be prisms by whether the front of the label is an underscore followed by
+an uppercase letter.  This makes a lot of sense for data constructors, which is what
+generic-lens's prisms were designed for, but it's a little restrictive for variants.
+The result is that we can only use the lensy notation if the labels in our variants
+are uppercase.  Consider the following:
+
+> vUpper :: Var ("Y" .== String .+ "X" .== Integer)
+> vUpper = IsJust (Label @"X") 1
+
+λ> v ^? #_X
+Left 1
+
+The row-types library does not generally assert that variants need labels that
+start with uppercase letters while records need labels that start with lowercase
+letters---in fact, the `switch` function described below will only work if the
+labels in a record and variant are exactly the same---but GHC is limited in that
+the # syntax only works for lowercase labels.  Therefore, to make uppercase labels
+like in the `vUpper` example above, one must use the syntax `Label @"X"` instead
+of simply `#X`.  See the proposal in https://github.com/ghc-proposals/ghc-proposals/pull/170
+for more information.
+--------------------------------------------------------------------------------
+
+For ease of use in view patterns, Variants also exposes the view function.
+(If using lens, this can be replaced with preview.)  With it, we can write a
+function like this:
+
+> myShow :: (r .! "y" ≈ String, Show (r .! "x")) => Var r -> String
+> myShow (Var.view #x -> Just n) = "Showable of "++show n
+> myShow (Var.view #y -> Just s) = "String of "++s
+> myShow _ = "Unknown"
+
+λ> myShow v
+"Showable of 1"
+λ> myShow v'
+"String of Foo"
+λ> myShow (just #z 3 :: Var ("y" .== String .+ "x" .== Integer .+ "z" .== Double))
+"Unknown"
+
+This can also be achieved with the IsJust pattern synonym in much the same way:
+
+> myShow' :: (WellBehaved r, r .! "y" ≈ String, Show (r .! "x")) => Var r -> String
+> myShow' (IsJust (Label :: Label "x") n) = "Showable of "++show n
+> myShow' (IsJust (Label :: Label "y") s) = "String of "++s
+> myShow' _ = "Unknown"
+
+In either case, the type signature is once again totally derivable.
+
+There are three minor annoyances with this.  First, it's annoying to have to write
+out the Label types in the pattern.  This is actually a requested issue on GHC
+(see https://gitlab.haskell.org/ghc/ghc/issues/13116 and
+https://github.com/ghc-proposals/ghc-proposals/pull/80 for more information).
+Second, it's fairly common to want to define
+a function like myShow to be exhaustive in the variant's cases, but to do this,
+you must manually provide a type signature:
+
+> myShowRestricted :: Var ("y" .== String .+ "x" .== Integer) -> String
+> myShowRestricted (Var.view #x -> Just n) = "Integer of "++show n
+> myShowRestricted (Var.view #y -> Just s) = "String of "++s
+> myShowRestricted _ = error "Unreachable"
+
+The final blemish can be seen in this restricted version of myShow.  Even though
+we know from the type that we've covered all the posibilities of the variant, GHC
+will generate a "non-exhaustive pattern match" warning without the final line.
+(This is true for the pattern synonym version too.)
+
+One way to avoid this problem is to use switch.  The switch operator takes a variant
+and a record such that for each label that the variant has, the record has a function
+at that label that consumes the value the variant has and produces a value in a
+common type.  Essentially, switch "applies" the variant to the record to produce
+an output value.
+
+> --myShowRestricted' :: Var ("y" .== String .+ "x" .== Integer) -> String
+> myShowRestricted' v = switch v $
+>      #x .== (\n -> "Integer of "++show n)
+>   .+ #y .== (\s -> "String of "++s)
+
+This version of myShow needs neither a type signature (it is inferred exactly) nor
+a default "unreachable" case.  However, we no longer have the benefit of Haskell's
+standard pattern matching.
+
+
+A more powerful version of trial is multiTrial, which tests for multiple labels
+at once.  With this, you can wholesale change the type of the variant to any (valid)
+variant type you would like.  Of course, there needs to be a recourse if the variant
+you provide is not expressible in the type you want, so multiTrial returns an Either
+of the type you want or a Variant of the leftovers.  Consider the examples:
+
+λ> :t multiTrial @("x" .== Double .+ "y" .== String) v
+multiTrial @("x" .== Double .+ "y" .== String) v
+  :: Either
+       (Var ('R '["x" ':-> Double, "y" ':-> String]))
+       (Var ('R '["x" ':-> Integer]))
+λ> multiTrial @("x" .== Double .+ "y" .== String) v
+Right {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]))
+λ> multiTrial @("x" .== Double .+ "y" .== String) v'
+Left {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
+from one where "x" is an Integer to one where it's a Double).  We can even use
+it to combine dispatching of two different variants at once:
+
+> also :: Disjoint xs ys
+>      => (Var xs -> a)
+>      -> (Var ys -> a)
+>      -> Var (xs .+ ys) -> a
+> also f1 f2 e = case multiTrial e of
+>   Left  e' -> f1 e'
+>   Right e' -> f2 e'
+
+The above also function takes two functions f1 and f2 that can each independently
+be used on variants with rows xs and ys respectively.  Using multiTrial, we can
+split the input variant (which is the join of xs and ys) and easily apply f1 or
+f2 as appropriate.

@@ -1,110 +1,115 @@-Name:                row-types-Version:             0.3.1.0-License:             MIT-License-file:        LICENSE-Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck-Maintainer:          daniel.winograd-cort@target.com, matthew.farkas-dyck@target.com-Build-Type:          Simple-Cabal-Version:       >=1.8-Category:            Data, Data Structures-Synopsis:	           Open Records and Variants-Description:-  This package uses closed type families and type literals to implement open-  records and variants.-  The core is based off of the <https://hackage.haskell.org/package/CTRex CTRex>-  package, but it additionally includes polymorphic variants and a number of-  additional functions.  That said, it is not a proper superset of CTRex as it-  specifically forbids records from having more than one element of the same-  label.--extra-source-files:-  examples/Examples.lhs-  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-  ghc-options: -W-  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--benchmark perf-  type: exitcode-stdio-1.0-  main-is: Main.hs-  hs-source-dirs:-      benchmarks/perf-  ghc-options: -W-  build-depends: base >= 2 && < 6-               , row-types-               , deepseq >= 1.4-               , criterion >= 1.1-  Extensions: AllowAmbiguousTypes,-              DataKinds,-              OverloadedLabels,-              RankNTypes,-              ScopedTypeVariables,-              TypeApplications,-              TypeFamilies,-              TypeOperators--test-suite test-  type: exitcode-stdio-1.0-  main-is: Main.hs-  hs-source-dirs: tests, examples-  ghc-options: -W-  other-modules: Examples-  build-depends: base >= 2 && < 6-               , generic-lens >= 1.1.0.0-               , row-types-  Extensions: AllowAmbiguousTypes,-              DataKinds,-              FlexibleContexts,-              OverloadedLabels,-              PatternSynonyms,-              RankNTypes,-              ScopedTypeVariables,-              TypeApplications,-              TypeFamilies,-              TypeOperators,-              ViewPatterns---source-repository head-    type:     git-    location: https://github.com/target/row-types/+Name:                row-types
+Version:             0.4.0.0
+License:             MIT
+License-file:        LICENSE
+Author:              Daniel Winograd-Cort, Matthew Farkas-Dyck
+Maintainer:          dwincort@gmail.com
+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
+Category:            Data, Data Structures
+Synopsis:	           Open Records and Variants
+Description:
+  This package uses closed type families and type literals to implement open
+  records and variants.
+  The core is based off of the <https://hackage.haskell.org/package/CTRex CTRex>
+  package, but it also includes polymorphic variants and a number of
+  additional functions.  That said, it is not a proper superset of CTRex as it
+  specifically forbids records from having more than one element of the same
+  label.
+
+extra-source-files:
+  examples/Examples.lhs
+  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
+  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
+
+benchmark perf
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs:
+      benchmarks/perf
+  ghc-options: -W
+  build-depends: base >= 2 && < 6
+               , row-types
+               , deepseq >= 1.4
+               , criterion >= 1.1
+  default-language: Haskell2010
+  default-extensions: AllowAmbiguousTypes,
+              DataKinds,
+              OverloadedLabels,
+              RankNTypes,
+              ScopedTypeVariables,
+              TypeApplications,
+              TypeFamilies,
+              TypeOperators
+
+test-suite test
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs: tests, examples
+  ghc-options: -W
+  other-modules: Examples
+  build-depends: base >= 2 && < 6
+               , generic-lens >= 1.1.0.0
+               , row-types
+  default-language: Haskell2010
+  default-extensions: AllowAmbiguousTypes,
+              DataKinds,
+              FlexibleContexts,
+              OverloadedLabels,
+              PatternSynonyms,
+              RankNTypes,
+              ScopedTypeVariables,
+              TypeApplications,
+              TypeFamilies,
+              TypeOperators,
+              ViewPatterns
+
+
+source-repository head
+    type:     git
+    location: https://github.com/target/row-types/

@@ -1,6 +1,6 @@--module Main where--import Examples ()--main = putStrLn "Test passes if Examples.lhs type-checks."+
+module Main where
+
+import Examples ()
+
+main = putStrLn "Test passes if Examples.lhs type-checks."