-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Open Records and Variants
--   
--   This package uses closed type families and type literals to implement
--   open records and variants. The core is based off of the <a>CTRex</a>
--   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.
@package row-types
@version 0.3.0.0


-- | This module implements the internals of open records and variants.
module Data.Row.Internal

-- | 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

-- | 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.
R :: [LT a] -> Row a

-- | A label
data Label (s :: Symbol)
Label :: Label

-- | This class gives the string associated with a type-level symbol. There
--   are instances of the class for every concrete literal: "hello", etc.
class KnownSymbol (n :: Symbol)

-- | The kind of elements of rows. Each element is a label and its
--   associated type.
data LT a
(:->) :: Symbol -> a -> LT a

-- | Type level version of <tt>empty</tt>
type Empty = R '[]

-- | Elements stored in a Row type are usually hidden.
data HideType
[HideType] :: a -> HideType

-- | Type level Row extension
type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k

-- | Type level Row modification
type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k

-- | Type level row renaming
type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k

-- | A type level way to create a singleton Row.
type (l :: Symbol) .== (a :: k) = Extend l a Empty
infix 7 .==

-- | Type level label fetching
type family (r :: Row k) .! (t :: Symbol) :: k
infixl 5 .!

-- | Type level Row element removal
type family (r :: Row k) .- (s :: Symbol) :: Row k
infixl 6 .-

-- | Type level Row difference. That is, <tt>l <a>.\\</a> r</tt> is the row
--   remaining after removing any matching elements of <tt>r</tt> from
--   <tt>l</tt>.
type family (l :: Row k) .\\ (r :: Row k) :: Row k
infixl 6 .\\

-- | Type level Row append
type family (l :: Row k) .+ (r :: Row k) :: Row k
infixl 6 .+

-- | The minimum join of the two rows.
type family (l :: Row k) .\/ (r :: Row k)
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)
infixl 6 .//

-- | Alias for <a>.\</a>. It is a class rather than an alias, so that it
--   can be partially applied.
class Lacks (l :: Symbol) (r :: Row *)

-- | Does the row lack (i.e. it does not have) the specified label?
type family (r :: Row k) .\ (l :: Symbol) :: Constraint
infixl 4 .\

-- | Alias for <tt>(r .! l) ≈ a</tt>. It is a class rather than an alias,
--   so that it can be partially applied.
class (r .! l ≈ a) => HasType l a r

-- | 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)

-- | 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 -> *). Forall r c => Proxy h -> (f Empty -> g Empty) -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ( 'R ((ℓ :-> τ) : ρ)) -> (h τ, f ( 'R ρ))) -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> h τ -> g ( 'R ρ) -> g ( 'R ((ℓ :-> τ) : ρ))) -> f r -> 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 -> *). Forall r c => Proxy h -> (f Empty -> g Empty) -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> f ( 'R ((ℓ :-> τ) : ρ)) -> Either (h τ) (f ( 'R ρ))) -> (forall ℓ τ ρ. (KnownSymbol ℓ, c τ) => Label ℓ -> Either (h τ) (g ( 'R ρ)) -> g ( 'R ((ℓ :-> τ) : ρ))) -> f r -> g 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)

-- | 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 -> *). BiForall r1 r2 c => 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 -> *). BiForall r1 r2 c => 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

-- | A pair of constraints
class (c1 x, c2 y) => BiConstraint c1 c2 x y

-- | A null constraint of one argument
class Unconstrained1 a

-- | A null constraint of two arguments
class Unconstrained2 a b

-- | 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

-- | 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

-- | 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 *)

-- | Map a type level function over a Row.
type family Map (f :: a -> b) (r :: Row a) :: Row b

-- | Is the first row a subset of the second?
type family Subset (r1 :: Row k) (r2 :: Row k) :: Constraint

-- | 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)

-- | The labels in a Row.
type family Labels (r :: Row a)

-- | Return a list of the labels in a row type.
labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]

-- | Return a list of the labels in a row type and is specialized to the
--   <a>Unconstrained1</a> constraint.
labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]

-- | A helper function for showing labels
show' :: (IsString s, Show a) => a -> s

-- | A helper function to turn a Label directly into <a>Text</a>.
toKey :: forall s. KnownSymbol s => Label s -> Text

-- | A lower fixity operator for type equality
type a ≈ b = a ~ b
infix 4 ≈

-- | 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)

-- | Allow any <a>Forall</a> over a row-type, be usable for
--   <a>Unconstrained1</a>.
freeForall :: forall r c. Forall r c :- Forall r Unconstrained1

-- | Map preserves uniqueness of labels.
uniqueMap :: forall f ρ. AllUniqueLabels ρ :- AllUniqueLabels (Map f ρ)

-- | 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)

-- | A class to capture the idea of <a>As</a> so that it can be partially
--   applied in a context.
class IsA c f a
as :: IsA c f a => As c f a

-- | This data type is used to for its ability to existentially bind a type
--   variable. Particularly, it says that for the type <tt>a</tt>, there
--   exists a <tt>t</tt> such that 'a ~ f t' and 'c t' holds.
data As c f a
[As] :: forall c f a t. (a ~ f t, c t) => As c f a
instance GHC.Classes.Eq (Data.Row.Internal.Label s)
instance forall k (r :: Data.Row.Internal.Row k) (l :: GHC.Types.Symbol) (a :: k). ((r Data.Row.Internal..! l) Data.Row.Internal.≈ a) => Data.Row.Internal.HasType l a r
instance (x Data.Row.Internal.≈ y) => GHC.OverloadedLabels.IsLabel x (Data.Row.Internal.Label y)
instance (r Data.Row.Internal..\ l) => Data.Row.Internal.Lacks l r
instance forall k1 k2 (c1 :: k2 -> GHC.Types.Constraint) (x :: k2) (c2 :: k1 -> GHC.Types.Constraint) (y :: k1). (c1 x, c2 y) => Data.Row.Internal.BiConstraint c1 c2 x y
instance forall k1 k2 (a :: k2) (b :: k1). Data.Row.Internal.Unconstrained2 a b
instance forall k (a :: k). Data.Row.Internal.Unconstrained1 a
instance Data.Row.Internal.Unconstrained
instance forall k1 k2 (c1 :: k1 -> k2 -> GHC.Types.Constraint). Data.Row.Internal.BiForall ('Data.Row.Internal.R '[]) ('Data.Row.Internal.R '[]) c1
instance forall k1 k2 (ℓ :: GHC.Types.Symbol) (c :: k1 -> k2 -> GHC.Types.Constraint) (τ1 :: k1) (τ2 :: k2) (ρ1 :: [Data.Row.Internal.LT k1]) (ρ2 :: [Data.Row.Internal.LT k2]). (GHC.TypeLits.KnownSymbol ℓ, c τ1 τ2, Data.Row.Internal.BiForall ('Data.Row.Internal.R ρ1) ('Data.Row.Internal.R ρ2) c) => Data.Row.Internal.BiForall ('Data.Row.Internal.R ((ℓ 'Data.Row.Internal.:-> τ1) : ρ1)) ('Data.Row.Internal.R ((ℓ 'Data.Row.Internal.:-> τ2) : ρ2)) c
instance forall k1 k2 (c :: k2 -> GHC.Types.Constraint) (a :: k2) (f :: k2 -> k1). c a => Data.Row.Internal.IsA c f (f a)
instance forall k (c :: k -> GHC.Types.Constraint). Data.Row.Internal.Forall ('Data.Row.Internal.R '[]) c
instance forall k (ℓ :: GHC.Types.Symbol) (c :: k -> GHC.Types.Constraint) (τ :: k) (ρ :: [Data.Row.Internal.LT k]). (GHC.TypeLits.KnownSymbol ℓ, c τ, Data.Row.Internal.Forall ('Data.Row.Internal.R ρ) c) => Data.Row.Internal.Forall ('Data.Row.Internal.R ((ℓ 'Data.Row.Internal.:-> τ) : ρ)) c
instance GHC.TypeLits.KnownSymbol s => GHC.Show.Show (Data.Row.Internal.Label s)


-- | This module implements extensible records using closed type famillies.
--   
--   See Examples.hs 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

-- | A label
data Label (s :: Symbol)
Label :: Label

-- | This class gives the string associated with a type-level symbol. There
--   are instances of the class for every concrete literal: "hello", etc.
class KnownSymbol (n :: Symbol)

-- | Are all of the labels in this Row unique?
type family AllUniqueLabels (r :: Row k) :: Constraint

-- | A convenient way to provide common, easy constraints
type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)

-- | A record with row r.
data Rec (r :: Row *)

-- | 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.
data Row a

-- | Type level version of <tt>empty</tt>
type Empty = R '[]

-- | A lower fixity operator for type equality
type a ≈ b = a ~ b
infix 4 ≈

-- | The empty record
empty :: Rec Empty

-- | A type level way to create a singleton Row.
type (l :: Symbol) .== (a :: k) = Extend l a Empty
infix 7 .==

-- | The singleton record
(.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a)
infix 7 .==

-- | 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.
pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a)
infix 7 :==

-- | Turns a singleton record into a pair of the label and value.
unSingleton :: forall l a. KnownSymbol l => Rec (l .== a) -> (Label l, a)

-- | Initialize a record with a default value at each label.
default' :: forall c ρ. (Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => a) -> Rec ρ

-- | Initialize a record with a default value at each label; works over an
--   <a>Applicative</a>.
defaultA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall a. c a => f a) -> f (Rec ρ)

-- | 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 ρ

-- | Initialize a record, where each value is determined by the given
--   function over the label at that value. This function works over an
--   <a>Applicative</a>.
fromLabelsA :: forall c f ρ. (Applicative f, Forall ρ c, AllUniqueLabels ρ) => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Rec ρ)

-- | Initialize a record that is produced by a <a>Map</a>.
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 ρ))

-- | Record extension. The row may already contain the label, in which case
--   the origin value can be obtained after restriction (<a>.-</a>) with
--   the label.
extend :: forall a l r. KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)

-- | Type level Row extension
type family Extend (l :: Symbol) (a :: k) (r :: Row k) :: Row k

-- | Alias for <a>.\</a>. It is a class rather than an alias, so that it
--   can be partially applied.
class Lacks (l :: Symbol) (r :: Row *)

-- | Does the row lack (i.e. it does not have) the specified label?
type family (r :: Row k) .\ (l :: Symbol) :: Constraint
infixl 4 .\

-- | Type level Row element removal
type family (r :: Row k) .- (s :: Symbol) :: Row k
infixl 6 .-

-- | Record restriction. Remove the label l from the record.
(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l)
infixl 6 .-

-- | 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

-- | Split a record into two sub-records.
split :: forall s r. (Forall s Unconstrained1, Subset s r) => Rec r -> (Rec s, Rec (r .\\ s))

-- | Update the value associated with the label.
update :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Rec r -> Rec r

-- | 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 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))

-- | Type level Row modification
type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k

-- | Rename a label.
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)

-- | Type level row renaming
type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k

-- | Alias for <tt>(r .! l) ≈ a</tt>. It is a class rather than an alias,
--   so that it can be partially applied.
class (r .! l ≈ a) => HasType l a r

-- | Type level label fetching
type family (r :: Row k) .! (t :: Symbol) :: k
infixl 5 .!

-- | Record selection
(.!) :: KnownSymbol l => Rec r -> Label l -> r .! l

-- | Type level Row append
type family (l :: Row k) .+ (r :: Row k) :: Row k
infixl 6 .+

-- | Record disjoint union (commutative)
(.+) :: Rec l -> Rec r -> Rec (l .+ r)
infixl 6 .+

-- | 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)

-- | A pattern version of record union, for use in pattern matching.
pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (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)
infixl 6 .//

-- | Record overwrite.
--   
--   The operation <tt>r .// r'</tt> creates a new record such that:
--   
--   <ul>
--   <li>Any label that is in both <tt>r</tt> and <tt>r'</tt> is in the
--   resulting record with the type and value given by the fields in
--   <tt>r</tt>,</li>
--   <li>Any label that is only found in <tt>r</tt> is in the resulting
--   record.</li>
--   <li>Any label that is only found in <tt>r'</tt> is in the resulting
--   record.</li>
--   </ul>
--   
--   This can be thought of as <tt>r</tt> "overwriting" <tt>r'</tt>.
(.//) :: Rec r -> Rec r' -> Rec (r .// r')

-- | Convert a record to a native Haskell type.
toNative :: forall t ρ. (Generic t, ToNative (Rep t) ρ) => Rec ρ -> t

-- | Convert a record to an exactly matching native Haskell type.
toNativeExact :: forall t ρ. (Generic t, ToNativeExact (Rep t) ρ) => Rec ρ -> t

-- | Convert a Haskell record to a row-types Rec.
fromNative :: forall t ρ. (Generic t, FromNative (Rep t) ρ) => t -> Rec ρ

-- | Converts a <a>Rec</a> into a <a>HashMap</a> of <a>Dynamic</a>s.
toDynamicMap :: Forall r Typeable => Rec r -> HashMap Text Dynamic

-- | Produces a <a>Rec</a> from a <a>HashMap</a> of <a>Dynamic</a>s.
fromDynamicMap :: (AllUniqueLabels r, Forall r Typeable) => HashMap Text Dynamic -> Maybe (Rec r)

-- | Map a type level function over a Row.
type family Map (f :: a -> b) (r :: Row a) :: Row b

-- | 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)

-- | 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)

-- | 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 ρ))

-- | Lifts a natural transformation over a record. In other words, it acts
--   as a record transformer to convert a record of <tt>f a</tt> values to
--   a record of <tt>g a</tt> values. If no constraint is needed,
--   instantiate the first type argument with <a>Unconstrained1</a> or use
--   <a>transform'</a>.
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)

-- | A version of <a>transform</a> 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)

-- | 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)

-- | A standard fold
erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Rec ρ -> [b]

-- | A fold with labels
eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Rec ρ -> [(s, b)]

-- | 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]

-- | Turns a record into a <a>HashMap</a> 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

-- | 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 *)

-- | 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)

-- | Applicative sequencing over a record.
sequence :: forall f r. (Forall r Unconstrained1, Applicative f) => Rec (Map f r) -> f (Rec r)

-- | A version of <a>sequence</a> in which the constraint for <a>Forall</a>
--   can be chosen.
sequence' :: forall f r c. (Forall r c, Applicative f) => Rec (Map f r) -> f (Rec 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)

-- | 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))

-- | A version of <a>compose</a> in which the constraint for <a>Forall</a>
--   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)

-- | A version of <a>uncompose</a> in which the constraint for
--   <a>Forall</a> can be chosen.
uncompose' :: forall c (f :: * -> *) (g :: * -> *) r. Forall r c => Rec (Map (Compose f g) r) -> Rec (Map f (Map g r))

-- | Return a list of the labels in a row type.
labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]

-- | Return a list of the labels in a row type and is specialized to the
--   <a>Unconstrained1</a> constraint.
labels' :: forall ρ s. (IsString s, Forall ρ Unconstrained1) => [s]

-- | Removes a label from the record but does not remove the underlying
--   value.
--   
--   This is faster than regular record removal (<a>.-</a>) 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 <a>update</a> that is split over two commands).
--   
--   If the resulting record is then merged (with <a>.+</a>) 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)

-- | 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 <a>metamorph</a>.
unsafeInjectFront :: KnownSymbol l => Label l -> a -> Rec (R r) -> Rec (R ((l :-> a) : r))
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.FromNative cs ρ => Data.Row.Records.FromNative (GHC.Generics.D1 m cs) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.FromNative cs ρ => Data.Row.Records.FromNative (GHC.Generics.C1 m cs) ρ
instance Data.Row.Records.FromNative GHC.Generics.U1 Data.Row.Internal.Empty
instance (GHC.TypeLits.KnownSymbol name, ρ Data.Row.Internal.≈ (name Data.Row.Internal..== t)) => Data.Row.Records.FromNative (GHC.Generics.S1 ('GHC.Generics.MetaSel ('GHC.Maybe.Just name) p s l) (GHC.Generics.Rec0 t)) ρ
instance forall k (l :: k -> *) (ρ₁ :: Data.Row.Internal.Row *) (r :: k -> *) (ρ₂ :: Data.Row.Internal.Row *) (ρ :: Data.Row.Internal.Row *). (Data.Row.Records.FromNative l ρ₁, Data.Row.Records.FromNative r ρ₂, ρ Data.Row.Internal.≈ (ρ₁ Data.Row.Internal..+ ρ₂)) => Data.Row.Records.FromNative (l GHC.Generics.:*: r) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNativeExact cs ρ => Data.Row.Records.ToNativeExact (GHC.Generics.D1 m cs) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNativeExact cs ρ => Data.Row.Records.ToNativeExact (GHC.Generics.C1 m cs) ρ
instance Data.Row.Records.ToNativeExact GHC.Generics.U1 Data.Row.Internal.Empty
instance (GHC.TypeLits.KnownSymbol name, ρ Data.Row.Internal.≈ (name Data.Row.Internal..== t)) => Data.Row.Records.ToNativeExact (GHC.Generics.S1 ('GHC.Generics.MetaSel ('GHC.Maybe.Just name) p s l) (GHC.Generics.Rec0 t)) ρ
instance forall k (l :: k -> *) (ρ₁ :: Data.Row.Internal.Row *) (r :: k -> *) (ρ₂ :: Data.Row.Internal.Row *) (ρ :: Data.Row.Internal.Row *). (Data.Row.Records.ToNativeExact l ρ₁, Data.Row.Records.ToNativeExact r ρ₂, ρ Data.Row.Internal.≈ (ρ₁ Data.Row.Internal..+ ρ₂), Data.Row.Internal.Disjoint ρ₁ ρ₂) => Data.Row.Records.ToNativeExact (l GHC.Generics.:*: r) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNative cs ρ => Data.Row.Records.ToNative (GHC.Generics.D1 m cs) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Records.ToNative cs ρ => Data.Row.Records.ToNative (GHC.Generics.C1 m cs) ρ
instance Data.Row.Records.ToNative GHC.Generics.U1 ρ
instance (GHC.TypeLits.KnownSymbol name, (ρ Data.Row.Internal..! name) Data.Row.Internal.≈ t) => Data.Row.Records.ToNative (GHC.Generics.S1 ('GHC.Generics.MetaSel ('GHC.Maybe.Just name) p s l) (GHC.Generics.Rec0 t)) ρ
instance forall k (l :: k -> *) (ρ :: Data.Row.Internal.Row *) (r :: k -> *). (Data.Row.Records.ToNative l ρ, Data.Row.Records.ToNative r ρ) => Data.Row.Records.ToNative (l GHC.Generics.:*: r) ρ
instance Data.Row.Records.GenericRec r => GHC.Generics.Generic (Data.Row.Records.Rec r)
instance Data.Row.Records.GenericRec Data.Row.Internal.Empty
instance GHC.TypeLits.KnownSymbol name => Data.Row.Records.GenericRec ('Data.Row.Internal.R '[ name 'Data.Row.Internal.:-> t])
instance (Data.Row.Records.GenericRec ('Data.Row.Internal.R r), GHC.TypeLits.KnownSymbol name, r Data.Type.Equality.~ ((name' 'Data.Row.Internal.:-> t') : r')) => Data.Row.Records.GenericRec ('Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : r))
instance Data.Row.Internal.Forall r GHC.Show.Show => GHC.Show.Show (Data.Row.Records.Rec r)
instance Data.Row.Internal.Forall r GHC.Classes.Eq => GHC.Classes.Eq (Data.Row.Records.Rec r)
instance (Data.Row.Internal.Forall r GHC.Classes.Eq, Data.Row.Internal.Forall r GHC.Classes.Ord) => GHC.Classes.Ord (Data.Row.Records.Rec r)
instance (Data.Row.Internal.Forall r GHC.Enum.Bounded, Data.Row.Internal.AllUniqueLabels r) => GHC.Enum.Bounded (Data.Row.Records.Rec r)
instance Data.Row.Internal.Forall r Control.DeepSeq.NFData => Control.DeepSeq.NFData (Data.Row.Records.Rec r)
instance (GHC.TypeLits.KnownSymbol name, (r' Data.Row.Internal..! name) Data.Row.Internal.≈ b, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, r' Data.Type.Equality.~ Data.Row.Internal.Modify name b r, r Data.Type.Equality.~ Data.Row.Internal.Modify name a r') => Data.Generics.Product.Fields.HasField name (Data.Row.Records.Rec r) (Data.Row.Records.Rec r') a b
instance (GHC.TypeLits.KnownSymbol name, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, r Data.Type.Equality.~ Data.Row.Internal.Modify name a r) => Data.Generics.Product.Fields.HasField' name (Data.Row.Records.Rec r) a


-- | This module implements extensible variants using closed type families.
module Data.Row.Variants

-- | A label
data Label (s :: Symbol)
Label :: Label

-- | This class gives the string associated with a type-level symbol. There
--   are instances of the class for every concrete literal: "hello", etc.
class KnownSymbol (n :: Symbol)

-- | Are all of the labels in this Row unique?
type family AllUniqueLabels (r :: Row k) :: Constraint

-- | A convenient way to provide common, easy constraints
type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)

-- | The variant type.
data Var (r :: Row *)

-- | 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.
data Row a

-- | Type level version of <tt>empty</tt>
type Empty = R '[]

-- | A lower fixity operator for type equality
type a ≈ b = a ~ b
infix 4 ≈

-- | Alias for <tt>(r .! l) ≈ a</tt>. It is a class rather than an alias,
--   so that it can be partially applied.
class (r .! l ≈ a) => HasType l a r

-- | 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

-- | A quick constructor to create a singleton variant.
singleton :: KnownSymbol l => Label l -> a -> Var (l .== a)

-- | A quick destructor for singleton variants.
unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a)

-- | 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 ρ)

-- | Does the row lack (i.e. it does not have) the specified label?
type family (r :: Row k) .\ (l :: Symbol) :: Constraint
infixl 4 .\

-- | Alias for <a>.\</a>. It is a class rather than an alias, so that it
--   can be partially applied.
class Lacks (l :: Symbol) (r :: Row *)

-- | The minimum join of the two rows.
type family (l :: Row k) .\/ (r :: Row k)
infixl 6 .\/

-- | Make the variant arbitrarily more diverse.
diversify :: forall r' r. Var r -> Var (r .\/ r')

-- | Type level Row append
type family (l :: Row k) .+ (r :: Row k) :: Row k
infixl 6 .+

-- | 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

-- | 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'))

-- | Type level Row modification
type family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k

-- | Rename the given label.
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r)

-- | Type level row renaming
type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row k) :: Row k

-- | A Variant with no options is uninhabited.
impossible :: Var Empty -> a

-- | 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))

-- | A version of <a>trial</a> that ignores the leftover variant.
trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l)

-- | A trial over multiple types
multiTrial :: forall x y. (AllUniqueLabels x, Forall (y .\\ x) Unconstrained1) => Var y -> Either (Var x) (Var (y .\\ x))

-- | A convenient function for using view patterns when dispatching
--   variants. For example:
--   
--   <pre>
--   myShow :: Var ("y" '::= String :| "x" '::= Int :| Empty) -&gt; String
--   myShow (view x -&gt; Just n) = "Int of "++show n
--   myShow (view y -&gt; Just s) = "String of "++s
--   </pre>
view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)

-- | 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)

-- | Split a variant into two sub-variants.
split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var s) (Var (r .\\ s))

-- | Type level label fetching
type family (r :: Row k) .! (t :: Symbol) :: k
infixl 5 .!

-- | Type level Row element removal
type family (r :: Row k) .- (s :: Symbol) :: Row k
infixl 6 .-

-- | Type level Row difference. That is, <tt>l <a>.\\</a> r</tt> is the row
--   remaining after removing any matching elements of <tt>r</tt> from
--   <tt>l</tt>.
type family (l :: Row k) .\\ (r :: Row k) :: Row k
infixl 6 .\\

-- | A type level way to create a singleton Row.
type (l :: Symbol) .== (a :: k) = Extend l a Empty
infix 7 .==

-- | Convert a variant to a native Haskell type.
toNative :: forall t ρ. (Generic t, ToNative (Rep t) ρ) => Var ρ -> t

-- | Convert a Haskell record to a row-types Var.
fromNative :: forall t ρ. (Generic t, FromNative (Rep t) ρ) => t -> Var ρ

-- | Convert a Haskell record to a row-types Var.
fromNativeExact :: forall t ρ. (Generic t, FromNativeExact (Rep t) ρ) => t -> Var ρ

-- | Map a type level function over a Row.
type family Map (f :: a -> b) (r :: Row a) :: Row b

-- | 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)

-- | 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)

-- | Lifts a natrual transformation over a variant. In other words, it acts
--   as a variant transformer to convert a variant of <tt>f a</tt> values
--   to a variant of <tt>g a</tt> values. If no constraint is needed,
--   instantiate the first type argument with <a>Unconstrained1</a>.
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)

-- | A form of <tt>transformC</tt> that doesn't have a constraint on
--   <tt>a</tt>
transform' :: forall r (f :: * -> *) (g :: * -> *). Forall r Unconstrained1 => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r)

-- | 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)

-- | A standard fold
erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b

-- | A fold with labels
eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s, b)

-- | 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

-- | Applicative sequencing over a variant
sequence :: forall f r. (Forall r Unconstrained1, Applicative f) => Var (Map f r) -> f (Var r)

-- | 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)

-- | 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))

-- | Return a list of the labels in a row type.
labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]

-- | 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

-- | 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 <a>metamorph</a>.
unsafeInjectFront :: forall l a r. KnownSymbol l => Var (R r) -> Var (R ((l :-> a) : r))
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Variants.FromNativeExact cs ρ => Data.Row.Variants.FromNativeExact (GHC.Generics.D1 m cs) ρ
instance Data.Row.Variants.FromNativeExact GHC.Generics.V1 Data.Row.Internal.Empty
instance (GHC.TypeLits.KnownSymbol name, ρ Data.Row.Internal.≈ (name Data.Row.Internal..== t)) => Data.Row.Variants.FromNativeExact (GHC.Generics.C1 ('GHC.Generics.MetaCons name fixity sels) (GHC.Generics.S1 m (GHC.Generics.Rec0 t))) ρ
instance forall k (l :: k -> *) (ρ₁ :: Data.Row.Internal.Row *) (r :: k -> *) (ρ₂ :: Data.Row.Internal.Row *) (ρ :: Data.Row.Internal.Row *). (Data.Row.Variants.FromNativeExact l ρ₁, Data.Row.Variants.FromNativeExact r ρ₂, ρ Data.Row.Internal.≈ (ρ₁ Data.Row.Internal..+ ρ₂)) => Data.Row.Variants.FromNativeExact (l GHC.Generics.:+: r) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Variants.FromNative cs ρ => Data.Row.Variants.FromNative (GHC.Generics.D1 m cs) ρ
instance Data.Row.Variants.FromNative GHC.Generics.V1 ρ
instance (GHC.TypeLits.KnownSymbol name, (ρ Data.Row.Internal..! name) Data.Row.Internal.≈ t, Data.Row.Internal.AllUniqueLabels ρ) => Data.Row.Variants.FromNative (GHC.Generics.C1 ('GHC.Generics.MetaCons name fixity sels) (GHC.Generics.S1 m (GHC.Generics.Rec0 t))) ρ
instance forall k (l :: k -> *) (ρ :: Data.Row.Internal.Row *) (r :: k -> *). (Data.Row.Variants.FromNative l ρ, Data.Row.Variants.FromNative r ρ) => Data.Row.Variants.FromNative (l GHC.Generics.:+: r) ρ
instance forall k (cs :: k -> *) (ρ :: Data.Row.Internal.Row *) (m :: GHC.Generics.Meta). Data.Row.Variants.ToNative cs ρ => Data.Row.Variants.ToNative (GHC.Generics.D1 m cs) ρ
instance Data.Row.Variants.ToNative GHC.Generics.V1 Data.Row.Internal.Empty
instance (GHC.TypeLits.KnownSymbol name, ρ Data.Row.Internal.≈ (name Data.Row.Internal..== t)) => Data.Row.Variants.ToNative (GHC.Generics.C1 ('GHC.Generics.MetaCons name fixity sels) (GHC.Generics.S1 m (GHC.Generics.Rec0 t))) ρ
instance forall k (l :: k -> *) (ρ₁ :: Data.Row.Internal.Row *) (r :: k -> *) (ρ₂ :: Data.Row.Internal.Row *) (ρ :: Data.Row.Internal.Row *). (Data.Row.Variants.ToNative l ρ₁, Data.Row.Variants.ToNative r ρ₂, ρ₂ Data.Row.Internal.≈ (ρ Data.Row.Internal..\\ ρ₁), ρ Data.Row.Internal.≈ (ρ₁ Data.Row.Internal..+ ρ₂), Data.Row.Internal.AllUniqueLabels ρ₁, Data.Row.Internal.Forall ρ₂ Data.Row.Internal.Unconstrained1) => Data.Row.Variants.ToNative (l GHC.Generics.:+: r) ρ
instance Data.Row.Variants.GenericVar r => GHC.Generics.Generic (Data.Row.Variants.Var r)
instance Data.Row.Variants.GenericVar Data.Row.Internal.Empty
instance GHC.TypeLits.KnownSymbol name => Data.Row.Variants.GenericVar ('Data.Row.Internal.R '[ name 'Data.Row.Internal.:-> t])
instance (Data.Row.Variants.GenericVar ('Data.Row.Internal.R r), GHC.TypeLits.KnownSymbol name, r Data.Type.Equality.~ ((name' 'Data.Row.Internal.:-> t') : r'), Data.Row.Internal.AllUniqueLabels ('Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : r))) => Data.Row.Variants.GenericVar ('Data.Row.Internal.R ((name 'Data.Row.Internal.:-> t) : r))
instance Data.Row.Internal.Forall r GHC.Show.Show => GHC.Show.Show (Data.Row.Variants.Var r)
instance Data.Row.Internal.Forall r GHC.Classes.Eq => GHC.Classes.Eq (Data.Row.Variants.Var r)
instance (Data.Row.Internal.Forall r GHC.Classes.Eq, Data.Row.Internal.Forall r GHC.Classes.Ord) => GHC.Classes.Ord (Data.Row.Variants.Var r)
instance Data.Row.Internal.Forall r Control.DeepSeq.NFData => Control.DeepSeq.NFData (Data.Row.Variants.Var r)
instance (Data.Row.Internal.AllUniqueLabels r, Data.Row.Internal.AllUniqueLabels r', GHC.TypeLits.KnownSymbol name, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, (r' Data.Row.Internal..! name) Data.Row.Internal.≈ b, r' Data.Row.Internal.≈ ((r Data.Row.Internal..- name) Data.Row.Internal..\/ (name Data.Row.Internal..== b))) => Data.Generics.Sum.Constructors.AsConstructor name (Data.Row.Variants.Var r) (Data.Row.Variants.Var r') a b
instance (Data.Row.Internal.AllUniqueLabels r, GHC.TypeLits.KnownSymbol name, (r Data.Row.Internal..! name) Data.Row.Internal.≈ a, r Data.Row.Internal.≈ ((r Data.Row.Internal..- name) Data.Row.Internal..\/ (name Data.Row.Internal..== a))) => Data.Generics.Sum.Constructors.AsConstructor' name (Data.Row.Variants.Var r) a


-- | This module provides the ability to discharge a polymorphic variant
--   using a record that has matching fields.
module Data.Row.Switch

-- | A <a>Var</a> and a <a>Rec</a> can combine if their rows line up
--   properly.
class Switch (v :: Row *) (r :: Row *) x | v x -> r, r x -> v

-- | 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 :: Switch v r x => Var v -> Rec r -> x

-- | The same as <tt>switch</tt> but with the argument order reversed
caseon :: Switch v r x => Rec r -> Var v -> x
instance Data.Row.Switch.Switch ('Data.Row.Internal.R '[]) ('Data.Row.Internal.R '[]) x
instance (GHC.TypeLits.KnownSymbol l, Data.Row.Switch.Switch ('Data.Row.Internal.R v) ('Data.Row.Internal.R r) b) => Data.Row.Switch.Switch ('Data.Row.Internal.R ((l 'Data.Row.Internal.:-> a) : v)) ('Data.Row.Internal.R ((l 'Data.Row.Internal.:-> (a -> b)) : r)) b


-- | This module includes a set of common functions for Records and
--   Variants. It includes:
--   
--   <ul>
--   <li>Common constructors, destructors, and querying functions</li>
--   </ul>
--   
--   It specifically excludes:
--   
--   <ul>
--   <li>Functions that have the same name for Records and Variants (e.g.
--   <a>focus</a>, <a>update</a>, <a>fromLabels</a>, etc.)</li>
--   <li>Common clashes with the standard Prelude or other modules (e.g.
--   <a>map</a>, <a>sequence</a>, <a>zip</a>, <a>Map</a>, etc.)</li>
--   </ul>
--   
--   If these particular functions are needed, they should be brought in
--   qualified from one of the Data.Row.*** modules directly.
module Data.Row

-- | A label
data Label (s :: Symbol)
Label :: Label

-- | This class gives the string associated with a type-level symbol. There
--   are instances of the class for every concrete literal: "hello", etc.
class KnownSymbol (n :: Symbol)

-- | Are all of the labels in this Row unique?
type family AllUniqueLabels (r :: Row k) :: Constraint

-- | A convenient way to provide common, easy constraints
type WellBehaved ρ = (Forall ρ Unconstrained1, AllUniqueLabels ρ)

-- | The variant type.
data Var (r :: Row *)

-- | A record with row r.
data Rec (r :: Row *)

-- | 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.
data Row a

-- | Type level version of <tt>empty</tt>
type Empty = R '[]

-- | A lower fixity operator for type equality
type a ≈ b = a ~ b
infix 4 ≈

-- | Alias for <tt>(r .! l) ≈ a</tt>. It is a class rather than an alias,
--   so that it can be partially applied.
class (r .! l ≈ a) => HasType l a r

-- | Alias for <a>.\</a>. It is a class rather than an alias, so that it
--   can be partially applied.
class Lacks (l :: Symbol) (r :: Row *)

-- | Does the row lack (i.e. it does not have) the specified label?
type family (r :: Row k) .\ (l :: Symbol) :: Constraint
infixl 4 .\

-- | Type level Row append
type family (l :: Row k) .+ (r :: Row k) :: Row k
infixl 6 .+

-- | The minimum join of the two rows.
type family (l :: Row k) .\/ (r :: Row k)
infixl 6 .\/

-- | Type level Row difference. That is, <tt>l <a>.\\</a> r</tt> is the row
--   remaining after removing any matching elements of <tt>r</tt> from
--   <tt>l</tt>.
type family (l :: Row k) .\\ (r :: Row k) :: Row k
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)
infixl 6 .//

-- | 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)

-- | A <a>Var</a> and a <a>Rec</a> can combine if their rows line up
--   properly.
class Switch (v :: Row *) (r :: Row *) x | v x -> r, r x -> v

-- | 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 :: Switch v r x => Var v -> Rec r -> x

-- | The same as <tt>switch</tt> but with the argument order reversed
caseon :: Switch v r x => Rec r -> Var v -> x

-- | The empty record
empty :: Rec Empty

-- | A type level way to create a singleton Row.
type (l :: Symbol) .== (a :: k) = Extend l a Empty
infix 7 .==

-- | The singleton record
(.==) :: KnownSymbol l => Label l -> a -> Rec (l .== a)
infix 7 .==

-- | 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.
pattern (:==) :: forall l a. KnownSymbol l => Label l -> a -> Rec (l .== a)
infix 7 :==

-- | Type level Row element removal
type family (r :: Row k) .- (s :: Symbol) :: Row k
infixl 6 .-

-- | Record restriction. Remove the label l from the record.
(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r .- l)
infixl 6 .-

-- | Type level label fetching
type family (r :: Row k) .! (t :: Symbol) :: k
infixl 5 .!

-- | Record selection
(.!) :: KnownSymbol l => Rec r -> Label l -> r .! l

-- | Record disjoint union (commutative)
(.+) :: Rec l -> Rec r -> Rec (l .+ r)
infixl 6 .+

-- | 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)

-- | A pattern version of record union, for use in pattern matching.
pattern (:+) :: forall l r. Disjoint l r => Rec l -> Rec r -> Rec (l .+ r)
infixl 6 :+

-- | Record overwrite.
--   
--   The operation <tt>r .// r'</tt> creates a new record such that:
--   
--   <ul>
--   <li>Any label that is in both <tt>r</tt> and <tt>r'</tt> is in the
--   resulting record with the type and value given by the fields in
--   <tt>r</tt>,</li>
--   <li>Any label that is only found in <tt>r</tt> is in the resulting
--   record.</li>
--   <li>Any label that is only found in <tt>r'</tt> is in the resulting
--   record.</li>
--   </ul>
--   
--   This can be thought of as <tt>r</tt> "overwriting" <tt>r'</tt>.
(.//) :: Rec r -> Rec r' -> Rec (r .// r')

-- | 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

-- | Make the variant arbitrarily more diverse.
diversify :: forall r' r. Var r -> Var (r .\/ r')

-- | A Variant with no options is uninhabited.
impossible :: Var Empty -> a

-- | 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))

-- | A version of <a>trial</a> that ignores the leftover variant.
trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l)

-- | A trial over multiple types
multiTrial :: forall x y. (AllUniqueLabels x, Forall (y .\\ x) Unconstrained1) => Var y -> Either (Var x) (Var (y .\\ x))

-- | Return a list of the labels in a row type.
labels :: forall ρ c s. (IsString s, Forall ρ c) => [s]