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


-- | True Sums of Products
--   
--   Implementation of n-ary sums and n-ary products.
--   
--   The module <a>Data.SOP</a> is the main module of this library and
--   contains more detailed documentation.
--   
--   The main use case of this package is to serve as the core of
--   <tt><a>generics-sop</a></tt>.
--   
--   A detailed description of the ideas behind this library is provided by
--   the paper:
--   
--   <ul>
--   <li>Edsko de Vries and Andres Löh. <a>True Sums of Products</a>.
--   Workshop on Generic Programming (WGP) 2014.</li>
--   </ul>
@package sop-core
@version 0.5.0.2


-- | Basic functors.
--   
--   Definitions of the type-level equivalents of <a>const</a>, <a>id</a>,
--   and (<a>.</a>), and a definition of the lifted function space.
--   
--   These datatypes are generally useful, but in this library, they're
--   primarily used as parameters for the <tt>NP</tt>, <tt>NS</tt>,
--   <tt>POP</tt>, and <tt>SOP</tt> types.
--   
--   We define own variants of <a>Const</a>, <a>Identity</a> and
--   <a>Compose</a> for various reasons.
--   
--   <ul>
--   <li><a>Const</a> and <a>Compose</a> become kind polymorphic only in
--   <tt>base-4.9.0.0</tt> (<tt>transformers-0.5.0.0</tt>).</li>
--   <li>Shorter names are convenient, and pattern synonyms aren't (yet)
--   powerful enough, particularly exhaustiveness check doesn't work
--   properly. See
--   <a>https://ghc.haskell.org/trac/ghc/ticket/8779</a>.</li>
--   </ul>
module Data.SOP.BasicFunctors

-- | The constant type functor.
--   
--   Like <a>Constant</a>, but kind-polymorphic in its second argument and
--   with a shorter name.
newtype K (a :: Type) (b :: k)
K :: a -> K (a :: Type) (b :: k)

-- | Extract the contents of a <a>K</a> value.
unK :: K a b -> a

-- | The identity type functor.
--   
--   Like <a>Identity</a>, but with a shorter name.
newtype I (a :: Type)
I :: a -> I (a :: Type)

-- | Extract the contents of an <a>I</a> value.
unI :: I a -> a

-- | Composition of functors.
--   
--   Like <a>Compose</a>, but kind-polymorphic and with a shorter name.
newtype (:.:) (f :: l -> Type) (g :: k -> l) (p :: k)
Comp :: f (g p) -> (:.:) (f :: l -> Type) (g :: k -> l) (p :: k)
infixr 7 :.:

-- | Extract the contents of a <a>Comp</a> value.
unComp :: (f :.: g) p -> f (g p)

-- | Lift the given function.
mapII :: (a -> b) -> I a -> I b

-- | Lift the given function.
mapIK :: (a -> b) -> I a -> K b c

-- | Lift the given function.
mapKI :: (a -> b) -> K a c -> I b

-- | Lift the given function.
mapKK :: (a -> b) -> K a c -> K b d

-- | Lift the given function.
mapIII :: (a -> b -> c) -> I a -> I b -> I c

-- | Lift the given function.
mapIIK :: (a -> b -> c) -> I a -> I b -> K c d

-- | Lift the given function.
mapIKI :: (a -> b -> c) -> I a -> K b d -> I c

-- | Lift the given function.
mapIKK :: (a -> b -> c) -> I a -> K b d -> K c e

-- | Lift the given function.
mapKII :: (a -> b -> c) -> K a d -> I b -> I c

-- | Lift the given function.
mapKIK :: (a -> b -> c) -> K a d -> I b -> K c e

-- | Lift the given function.
mapKKI :: (a -> b -> c) -> K a d -> K b e -> I c

-- | Lift the given function.
mapKKK :: (a -> b -> c) -> K a d -> K b e -> K c f
instance forall a k (b :: k). GHC.Generics.Generic (Data.SOP.BasicFunctors.K a b)
instance Data.Traversable.Traversable (Data.SOP.BasicFunctors.K a)
instance Data.Foldable.Foldable (Data.SOP.BasicFunctors.K a)
instance GHC.Base.Functor (Data.SOP.BasicFunctors.K a)
instance GHC.Generics.Generic (Data.SOP.BasicFunctors.I a)
instance Data.Traversable.Traversable Data.SOP.BasicFunctors.I
instance Data.Foldable.Foldable Data.SOP.BasicFunctors.I
instance GHC.Base.Functor Data.SOP.BasicFunctors.I
instance forall l (f :: l -> *) k (g :: k -> l) (p :: k). GHC.Generics.Generic ((Data.SOP.BasicFunctors.:.:) f g p)
instance forall l k (f :: l -> *) (g :: k -> l) (x :: k). GHC.Base.Semigroup (f (g x)) => GHC.Base.Semigroup ((Data.SOP.BasicFunctors.:.:) f g x)
instance forall l k (f :: l -> *) (g :: k -> l) (x :: k). GHC.Base.Monoid (f (g x)) => GHC.Base.Monoid ((Data.SOP.BasicFunctors.:.:) f g x)
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (f Data.SOP.BasicFunctors.:.: g)
instance (GHC.Base.Applicative f, GHC.Base.Applicative g) => GHC.Base.Applicative (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Foldable.Foldable f, Data.Foldable.Foldable g) => Data.Foldable.Foldable (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Traversable.Traversable f, Data.Traversable.Traversable g) => Data.Traversable.Traversable (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Functor.Classes.Eq1 f, Data.Functor.Classes.Eq1 g) => Data.Functor.Classes.Eq1 (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Functor.Classes.Ord1 f, Data.Functor.Classes.Ord1 g) => Data.Functor.Classes.Ord1 (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Functor.Classes.Read1 f, Data.Functor.Classes.Read1 g) => Data.Functor.Classes.Read1 (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Functor.Classes.Show1 f, Data.Functor.Classes.Show1 g) => Data.Functor.Classes.Show1 (f Data.SOP.BasicFunctors.:.: g)
instance (Data.Functor.Classes.Eq1 f, Data.Functor.Classes.Eq1 g, GHC.Classes.Eq a) => GHC.Classes.Eq ((Data.SOP.BasicFunctors.:.:) f g a)
instance (Data.Functor.Classes.Ord1 f, Data.Functor.Classes.Ord1 g, GHC.Classes.Ord a) => GHC.Classes.Ord ((Data.SOP.BasicFunctors.:.:) f g a)
instance (Data.Functor.Classes.Read1 f, Data.Functor.Classes.Read1 g, GHC.Read.Read a) => GHC.Read.Read ((Data.SOP.BasicFunctors.:.:) f g a)
instance (Data.Functor.Classes.Show1 f, Data.Functor.Classes.Show1 g, GHC.Show.Show a) => GHC.Show.Show ((Data.SOP.BasicFunctors.:.:) f g a)
instance forall l k (f :: l -> *) (g :: k -> l) (a :: k). Control.DeepSeq.NFData (f (g a)) => Control.DeepSeq.NFData ((Data.SOP.BasicFunctors.:.:) f g a)
instance (Control.DeepSeq.NFData1 f, Control.DeepSeq.NFData1 g) => Control.DeepSeq.NFData1 (f Data.SOP.BasicFunctors.:.: g)
instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Data.SOP.BasicFunctors.I a)
instance GHC.Base.Monoid a => GHC.Base.Monoid (Data.SOP.BasicFunctors.I a)
instance GHC.Base.Applicative Data.SOP.BasicFunctors.I
instance GHC.Base.Monad Data.SOP.BasicFunctors.I
instance Data.Functor.Classes.Eq1 Data.SOP.BasicFunctors.I
instance Data.Functor.Classes.Ord1 Data.SOP.BasicFunctors.I
instance Data.Functor.Classes.Read1 Data.SOP.BasicFunctors.I
instance Data.Functor.Classes.Show1 Data.SOP.BasicFunctors.I
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.SOP.BasicFunctors.I a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.SOP.BasicFunctors.I a)
instance GHC.Read.Read a => GHC.Read.Read (Data.SOP.BasicFunctors.I a)
instance GHC.Show.Show a => GHC.Show.Show (Data.SOP.BasicFunctors.I a)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.SOP.BasicFunctors.I a)
instance Control.DeepSeq.NFData1 Data.SOP.BasicFunctors.I
instance Data.Functor.Classes.Eq2 Data.SOP.BasicFunctors.K
instance Data.Functor.Classes.Ord2 Data.SOP.BasicFunctors.K
instance Data.Functor.Classes.Read2 Data.SOP.BasicFunctors.K
instance Data.Functor.Classes.Show2 Data.SOP.BasicFunctors.K
instance GHC.Classes.Eq a => Data.Functor.Classes.Eq1 (Data.SOP.BasicFunctors.K a)
instance GHC.Classes.Ord a => Data.Functor.Classes.Ord1 (Data.SOP.BasicFunctors.K a)
instance GHC.Read.Read a => Data.Functor.Classes.Read1 (Data.SOP.BasicFunctors.K a)
instance GHC.Show.Show a => Data.Functor.Classes.Show1 (Data.SOP.BasicFunctors.K a)
instance forall k a (b :: k). GHC.Classes.Eq a => GHC.Classes.Eq (Data.SOP.BasicFunctors.K a b)
instance forall k a (b :: k). GHC.Classes.Ord a => GHC.Classes.Ord (Data.SOP.BasicFunctors.K a b)
instance forall k a (b :: k). GHC.Read.Read a => GHC.Read.Read (Data.SOP.BasicFunctors.K a b)
instance forall k a (b :: k). GHC.Show.Show a => GHC.Show.Show (Data.SOP.BasicFunctors.K a b)
instance forall k a (b :: k). GHC.Base.Semigroup a => GHC.Base.Semigroup (Data.SOP.BasicFunctors.K a b)
instance forall k a (b :: k). GHC.Base.Monoid a => GHC.Base.Monoid (Data.SOP.BasicFunctors.K a b)
instance GHC.Base.Monoid a => GHC.Base.Applicative (Data.SOP.BasicFunctors.K a)
instance forall k a (b :: k). Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.SOP.BasicFunctors.K a b)
instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData1 (Data.SOP.BasicFunctors.K a)
instance Control.DeepSeq.NFData2 Data.SOP.BasicFunctors.K


-- | Constraints for indexed datatypes.
--   
--   This module contains code that helps to specify that all elements of
--   an indexed structure must satisfy a particular constraint.
module Data.SOP.Constraint

-- | Require a constraint for every element of a list.
--   
--   If you have a datatype that is indexed over a type-level list, then
--   you can use <a>All</a> to indicate that all elements of that
--   type-level list must satisfy a given constraint.
--   
--   <i>Example:</i> The constraint
--   
--   <pre>
--   All Eq '[ Int, Bool, Char ]
--   </pre>
--   
--   is equivalent to the constraint
--   
--   <pre>
--   (Eq Int, Eq Bool, Eq Char)
--   </pre>
--   
--   <i>Example:</i> A type signature such as
--   
--   <pre>
--   f :: All Eq xs =&gt; NP I xs -&gt; ...
--   </pre>
--   
--   means that <tt>f</tt> can assume that all elements of the n-ary
--   product satisfy <a>Eq</a>.
--   
--   Note on superclasses: ghc cannot deduce superclasses from <a>All</a>
--   constraints. You might expect the following to compile
--   
--   <pre>
--   class (Eq a) =&gt; MyClass a
--   
--   foo :: (All Eq xs) =&gt; NP f xs -&gt; z
--   foo = [..]
--   
--   bar :: (All MyClass xs) =&gt; NP f xs -&gt; x
--   bar = foo
--   </pre>
--   
--   but it will fail with an error saying that it was unable to deduce the
--   class constraint <tt><a>AllF</a> <a>Eq</a> xs</tt> (or similar) in the
--   definition of <tt>bar</tt>. In cases like this you can use <a>Dict</a>
--   from <a>Data.SOP.Dict</a> to prove conversions between constraints.
--   See <a>this answer on SO for more details</a>.
class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k])

-- | Constrained paramorphism for a type-level list.
--   
--   The advantage of writing functions in terms of <a>cpara_SList</a> is
--   that they are then typically not recursive, and can be unfolded
--   statically if the type-level list is statically known.
cpara_SList :: All c xs => proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r ys -> r (y ': ys)) -> r xs

-- | Require a constraint for every element of a list of lists.
--   
--   If you have a datatype that is indexed over a type-level list of
--   lists, then you can use <a>All2</a> to indicate that all elements of
--   the inner lists must satisfy a given constraint.
--   
--   <i>Example:</i> The constraint
--   
--   <pre>
--   All2 Eq '[ '[ Int ], '[ Bool, Char ] ]
--   </pre>
--   
--   is equivalent to the constraint
--   
--   <pre>
--   (Eq Int, Eq Bool, Eq Char)
--   </pre>
--   
--   <i>Example:</i> A type signature such as
--   
--   <pre>
--   f :: All2 Eq xss =&gt; SOP I xs -&gt; ...
--   </pre>
--   
--   means that <tt>f</tt> can assume that all elements of the sum of
--   product satisfy <a>Eq</a>.
--   
--   Since 0.4.0.0, this is merely a synonym for 'All (All c)'.
type All2 c = All (All c)

-- | Require a constraint pointwise for every pair of elements from two
--   lists.
--   
--   <i>Example:</i> The constraint
--   
--   <pre>
--   AllZip (~) '[ Int, Bool, Char ] '[ a, b, c ]
--   </pre>
--   
--   is equivalent to the constraint
--   
--   <pre>
--   (Int ~ a, Bool ~ b, Char ~ c)
--   </pre>
class (SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])

-- | Require a constraint pointwise for every pair of elements from two
--   lists of lists.
class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss

-- | A generalization of <a>All</a> and <a>All2</a>.
--   
--   The family <a>AllN</a> expands to <a>All</a> or <a>All2</a> depending
--   on whether the argument is indexed by a list or a list of lists.
type family AllN (h :: (k -> Type) -> (l -> Type)) (c :: k -> Constraint) :: l -> Constraint

-- | A generalization of <a>AllZip</a> and <a>AllZip2</a>.
--   
--   The family <a>AllZipN</a> expands to <a>AllZip</a> or <a>AllZip2</a>
--   depending on whther the argument is indexed by a list or a list of
--   lists.
type family AllZipN (h :: (k -> Type) -> (l -> Type)) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint

-- | Composition of constraints.
--   
--   Note that the result of the composition must be a constraint, and
--   therefore, in <tt><a>Compose</a> f g</tt>, the kind of <tt>f</tt> is
--   <tt>k -&gt; <a>Constraint</a></tt>. The kind of <tt>g</tt>, however,
--   is <tt>l -&gt; k</tt> and can thus be a normal type constructor.
--   
--   A typical use case is in connection with <a>All</a> on an <a>NP</a> or
--   an <a>NS</a>. For example, in order to denote that all elements on an
--   <tt><a>NP</a> f xs</tt> satisfy <a>Show</a>, we can say <tt><a>All</a>
--   (<a>Compose</a> <a>Show</a> f) xs</tt>.
class (f (g x)) => ( f `Compose` g ) x
infixr 9 `Compose`

-- | Pairing of constraints.
class (f x, g x) => ( f `And` g ) x
infixl 7 `And`

-- | A constraint that can always be satisfied.
class Top x

-- | The constraint <tt><a>LiftedCoercible</a> f g x y</tt> is equivalent
--   to <tt><a>Coercible</a> (f x) (g y)</tt>.
class Coercible (f x) (g y) => LiftedCoercible f g x y

-- | Type family that forces a type-level list to be of the same shape as
--   the given type-level list.
--   
--   Since 0.5.0.0, this only tests the top-level structure of the list,
--   and is intended to be used in conjunction with a separate construct
--   (such as the <a>AllZip</a>, <a>AllZipF</a> combination to tie the
--   recursive knot). The reason is that making <a>SameShapeAs</a> directly
--   recursive leads to quadratic compile times.
--   
--   The main use of this constraint is to help type inference to learn
--   something about otherwise unknown type-level lists.
type family SameShapeAs (xs :: [a]) (ys :: [b]) :: Constraint

-- | Implicit singleton list.
--   
--   A singleton list can be used to reveal the structure of a type-level
--   list argument that the function is quantified over.
--   
--   Since 0.4.0.0, this is now defined in terms of <a>All</a>. A singleton
--   list provides a witness for a type-level list where the elements need
--   not satisfy any additional constraints.
type SListI = All Top

-- | Require a singleton for every inner list in a list of lists.
type SListI2 = All SListI

-- | Type family used to implement <a>All</a>.
type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint

-- | Type family used to implement <a>AllZip</a>.
type family AllZipF (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b]) :: Constraint

-- | Utility function to compute the head of a type-level list.
type family Head (xs :: [a]) :: a

-- | Utility function to compute the tail of a type-level list.
type family Tail (xs :: [a]) :: [a]

-- | A generalization of <a>SListI</a>.
--   
--   The family <a>SListIN</a> expands to <a>SListI</a> or <a>SListI2</a>
--   depending on whether the argument is indexed by a list or a list of
--   lists.
type family SListIN (h :: (k -> Type) -> (l -> Type)) :: l -> Constraint

-- | Constrained case distinction on a type-level list.
ccase_SList :: All c xs => proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r (y ': ys)) -> r xs
type Constraint = CONSTRAINT LiftedRep
instance forall a b (f :: a -> b -> GHC.Types.Constraint) (xss :: [[a]]) (yss :: [[b]]). (Data.SOP.Constraint.AllZipF (Data.SOP.Constraint.AllZip f) xss yss, Data.SOP.Constraint.SListI xss, Data.SOP.Constraint.SListI yss, Data.SOP.Constraint.SameShapeAs xss yss, Data.SOP.Constraint.SameShapeAs yss xss) => Data.SOP.Constraint.AllZip2 f xss yss
instance forall a b (xs :: [a]) (ys :: [b]) (c :: a -> b -> GHC.Types.Constraint). (Data.SOP.Constraint.SListI xs, Data.SOP.Constraint.SListI ys, Data.SOP.Constraint.SameShapeAs xs ys, Data.SOP.Constraint.SameShapeAs ys xs, Data.SOP.Constraint.AllZipF c xs ys) => Data.SOP.Constraint.AllZip c xs ys
instance forall k (c :: k -> GHC.Types.Constraint). Data.SOP.Constraint.All c '[]
instance forall a (c :: a -> GHC.Types.Constraint) (x :: a) (xs :: [a]). (c x, Data.SOP.Constraint.All c xs) => Data.SOP.Constraint.All c (x : xs)
instance forall k (x :: k). Data.SOP.Constraint.Top x
instance forall k (f :: k -> GHC.Types.Constraint) (x :: k) (g :: k -> GHC.Types.Constraint). (f x, g x) => Data.SOP.Constraint.And f g x
instance forall k1 k2 (f :: k1 -> GHC.Types.Constraint) (g :: k2 -> k1) (x :: k2). f (g x) => Data.SOP.Constraint.Compose f g x
instance forall k1 k2 k3 (f :: k1 -> k2) (x :: k1) (g :: k3 -> k2) (y :: k3). GHC.Types.Coercible (f x) (g y) => Data.SOP.Constraint.LiftedCoercible f g x y


-- | Classes for generalized combinators on SOP types.
--   
--   In the SOP approach to generic programming, we're predominantly
--   concerned with four structured datatypes:
--   
--   <pre>
--   <a>NP</a>  :: (k -&gt; <a>Type</a>) -&gt; ( [k]  -&gt; <a>Type</a>)   -- n-ary product
--   <a>NS</a>  :: (k -&gt; <a>Type</a>) -&gt; ( [k]  -&gt; <a>Type</a>)   -- n-ary sum
--   <a>POP</a> :: (k -&gt; <a>Type</a>) -&gt; ([[k]] -&gt; <a>Type</a>)   -- product of products
--   <a>SOP</a> :: (k -&gt; <a>Type</a>) -&gt; ([[k]] -&gt; <a>Type</a>)   -- sum of products
--   </pre>
--   
--   All of these have a kind that fits the following pattern:
--   
--   <pre>
--   (k -&gt; <a>Type</a>) -&gt; (l -&gt; <a>Type</a>)
--   </pre>
--   
--   These four types support similar interfaces. In order to allow reusing
--   the same combinator names for all of these types, we define various
--   classes in this module that allow the necessary generalization.
--   
--   The classes typically lift concepts that exist for kinds
--   <tt><a>Type</a></tt> or <tt><a>Type</a> -&gt; <a>Type</a></tt> to
--   datatypes of kind <tt>(k -&gt; <a>Type</a>) -&gt; (l -&gt;
--   <a>Type</a>)</tt>. This module also derives a number of derived
--   combinators.
--   
--   The actual instances are defined in <a>Data.SOP.NP</a> and
--   <a>Data.SOP.NS</a>.
module Data.SOP.Classes

-- | A generalization of <a>pure</a> or <a>return</a> to higher kinds.
class HPure (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>pure</a> directly.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hpure</a>, <a>pure_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a) -&gt; <a>NP</a>  f xs
--   <a>hpure</a>, <a>pure_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a) -&gt; <a>POP</a> f xss
--   </pre>
hpure :: (HPure h, SListIN h xs) => (forall a. f a) -> h f xs

-- | A variant of <a>hpure</a> that allows passing in a constrained
--   argument.
--   
--   Calling <tt><a>hcpure</a> f s</tt> where <tt>s :: h f xs</tt> causes
--   <tt>f</tt> to be applied at all the types that are contained in
--   <tt>xs</tt>. Therefore, the constraint <tt>c</tt> has to be satisfied
--   for all elements of <tt>xs</tt>, which is what <tt><a>AllN</a> h c
--   xs</tt> states.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcpure</a>, <a>cpure_NP</a>  :: (<a>All</a>  c xs ) =&gt; proxy c -&gt; (forall a. c a =&gt; f a) -&gt; <a>NP</a>  f xs
--   <a>hcpure</a>, <a>cpure_POP</a> :: (<a>All2</a> c xss) =&gt; proxy c -&gt; (forall a. c a =&gt; f a) -&gt; <a>POP</a> f xss
--   </pre>
hcpure :: (HPure h, AllN h c xs) => proxy c -> (forall a. c a => f a) -> h f xs

-- | Lifted functions.
newtype ( f -.-> g ) a
Fn :: (f a -> g a) -> (-.->) f g a
[apFn] :: (-.->) f g a -> f a -> g a
infixr 1 -.->

-- | Construct a lifted function.
--   
--   Same as <a>Fn</a>. Only available for uniformity with the higher-arity
--   versions.
fn :: (f a -> f' a) -> (f -.-> f') a

-- | Construct a binary lifted function.
fn_2 :: (f a -> f' a -> f'' a) -> (f -.-> (f' -.-> f'')) a

-- | Construct a ternary lifted function.
fn_3 :: (f a -> f' a -> f'' a -> f''' a) -> (f -.-> (f' -.-> (f'' -.-> f'''))) a

-- | Construct a quarternary lifted function.
fn_4 :: (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (f -.-> (f' -.-> (f'' -.-> (f''' -.-> f'''')))) a

-- | Maps a structure to the same structure.
type family Same (h :: (k1 -> Type) -> (l1 -> Type)) :: (k2 -> Type) -> (l2 -> Type)

-- | Maps a structure containing sums to the corresponding product
--   structure.
type family Prod (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)

-- | A generalization of <a>&lt;*&gt;</a>.
class (Prod (Prod h) ~ Prod h, HPure (Prod h)) => HAp (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>&lt;*&gt;</a>.
--   
--   For products (<a>NP</a>) as well as products of products (<a>POP</a>),
--   the correspondence is rather direct. We combine a structure containing
--   (lifted) functions and a compatible structure containing corresponding
--   arguments into a compatible structure containing results.
--   
--   The same combinator can also be used to combine a product structure of
--   functions with a sum structure of arguments, which then results in
--   another sum structure of results. The sum structure determines which
--   part of the product structure will be used.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hap</a>, <a>ap_NP</a>  :: <a>NP</a>  (f -.-&gt; g) xs  -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  g xs
--   <a>hap</a>, <a>ap_NS</a>  :: <a>NP</a>  (f -.-&gt; g) xs  -&gt; <a>NS</a>  f xs  -&gt; <a>NS</a>  g xs
--   <a>hap</a>, <a>ap_POP</a> :: <a>POP</a> (f -.-&gt; g) xss -&gt; <a>POP</a> f xss -&gt; <a>POP</a> g xss
--   <a>hap</a>, <a>ap_SOP</a> :: <a>POP</a> (f -.-&gt; g) xss -&gt; <a>SOP</a> f xss -&gt; <a>SOP</a> g xss
--   </pre>
hap :: HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs

-- | A generalized form of <a>liftA</a>, which in turn is a generalized
--   <a>map</a>.
--   
--   Takes a lifted function and applies it to every element of a structure
--   while preserving its shape.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hliftA</a> f xs = <a>hpure</a> (<a>fn</a> f) ` <a>hap</a> ` xs
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hliftA</a>, <a>liftA_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs
--   <a>hliftA</a>, <a>liftA_NS</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a) -&gt; <a>NS</a>  f xs  -&gt; <a>NS</a>  f' xs
--   <a>hliftA</a>, <a>liftA_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss
--   <a>hliftA</a>, <a>liftA_SOP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a) -&gt; <a>SOP</a> f xss -&gt; <a>SOP</a> f' xss
--   </pre>
hliftA :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs

-- | A generalized form of <a>liftA2</a>, which in turn is a generalized
--   <a>zipWith</a>.
--   
--   Takes a lifted binary function and uses it to combine two structures
--   of equal shape into a single structure.
--   
--   It either takes two product structures to a product structure, or one
--   product and one sum structure to a sum structure.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hliftA2</a> f xs ys = <a>hpure</a> (<a>fn_2</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hliftA2</a>, <a>liftA2_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs  -&gt; <a>NP</a>  f'' xs
--   <a>hliftA2</a>, <a>liftA2_NS</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NS</a>  f' xs  -&gt; <a>NS</a>  f'' xs
--   <a>hliftA2</a>, <a>liftA2_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss -&gt; <a>POP</a> f'' xss
--   <a>hliftA2</a>, <a>liftA2_SOP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>POP</a> f xss -&gt; <a>SOP</a> f' xss -&gt; <a>SOP</a> f'' xss
--   </pre>
hliftA2 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | A generalized form of <a>liftA3</a>, which in turn is a generalized
--   <a>zipWith3</a>.
--   
--   Takes a lifted ternary function and uses it to combine three
--   structures of equal shape into a single structure.
--   
--   It either takes three product structures to a product structure, or
--   two product structures and one sum structure to a sum structure.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hliftA3</a> f xs ys zs = <a>hpure</a> (<a>fn_3</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys ` <a>hap</a> ` zs
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hliftA3</a>, <a>liftA3_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs  -&gt; <a>NP</a>  f'' xs  -&gt; <a>NP</a>  f''' xs
--   <a>hliftA3</a>, <a>liftA3_NS</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs  -&gt; <a>NS</a>  f'' xs  -&gt; <a>NS</a>  f''' xs
--   <a>hliftA3</a>, <a>liftA3_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss -&gt; <a>POP</a> f'' xss -&gt; <a>POP</a> f''' xs
--   <a>hliftA3</a>, <a>liftA3_SOP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss -&gt; <a>SOP</a> f'' xss -&gt; <a>SOP</a> f''' xs
--   </pre>
hliftA3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Another name for <a>hliftA</a>.
hmap :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs

-- | Another name for <a>hliftA2</a>.
hzipWith :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | Another name for <a>hliftA3</a>.
hzipWith3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Variant of <a>hliftA</a> that takes a constrained function.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA</a> p f xs = <a>hcpure</a> p (<a>fn</a> f) ` <a>hap</a> ` xs
--   </pre>
hcliftA :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs

-- | Variant of <a>hliftA2</a> that takes a constrained function.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA2</a> p f xs ys = <a>hcpure</a> p (<a>fn_2</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys
--   </pre>
hcliftA2 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | Variant of <a>hliftA3</a> that takes a constrained function.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA3</a> p f xs ys zs = <a>hcpure</a> p (<a>fn_3</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys ` <a>hap</a> ` zs
--   </pre>
hcliftA3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Another name for <a>hcliftA</a>.
hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs

-- | Another name for <a>hcliftA2</a>.
hczipWith :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | Another name for <a>hcliftA3</a>.
hczipWith3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Maps products to lists, and sums to identities.
type family CollapseTo (h :: (k -> Type) -> (l -> Type)) (x :: Type) :: Type

-- | A class for collapsing a heterogeneous structure into a homogeneous
--   one.
class HCollapse (h :: (k -> Type) -> (l -> Type))

-- | Collapse a heterogeneous structure with homogeneous elements into a
--   homogeneous structure.
--   
--   If a heterogeneous structure is instantiated to the constant functor
--   <a>K</a>, then it is in fact homogeneous. This function maps such a
--   value to a simpler Haskell datatype reflecting that. An <tt><a>NS</a>
--   (<a>K</a> a)</tt> contains a single <tt>a</tt>, and an <tt><a>NP</a>
--   (<a>K</a> a)</tt> contains a list of <tt>a</tt>s.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcollapse</a>, <a>collapse_NP</a>  :: <a>NP</a>  (<a>K</a> a) xs  -&gt;  [a]
--   <a>hcollapse</a>, <a>collapse_NS</a>  :: <a>NS</a>  (<a>K</a> a) xs  -&gt;   a
--   <a>hcollapse</a>, <a>collapse_POP</a> :: <a>POP</a> (<a>K</a> a) xss -&gt; [[a]]
--   <a>hcollapse</a>, <a>collapse_SOP</a> :: <a>SOP</a> (<a>K</a> a) xss -&gt;  [a]
--   </pre>
hcollapse :: (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a

-- | A generalization of <a>traverse_</a> or <a>foldMap</a>.
class HTraverse_ (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>traverse_</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hctraverse_</a>, <a>ctraverse__NP</a>  :: (<a>All</a>  c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>NP</a>  f xs  -&gt; g ()
--   <a>hctraverse_</a>, <a>ctraverse__NS</a>  :: (<a>All2</a> c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>NS</a>  f xs  -&gt; g ()
--   <a>hctraverse_</a>, <a>ctraverse__POP</a> :: (<a>All</a>  c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>POP</a> f xss -&gt; g ()
--   <a>hctraverse_</a>, <a>ctraverse__SOP</a> :: (<a>All2</a> c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>SOP</a> f xss -&gt; g ()
--   </pre>
hctraverse_ :: (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> h f xs -> g ()

-- | Unconstrained version of <a>hctraverse_</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <tt>traverse_</tt>, <a>traverse__NP</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>NP</a>  f xs  -&gt; g ()
--   <tt>traverse_</tt>, <a>traverse__NS</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>NS</a>  f xs  -&gt; g ()
--   <tt>traverse_</tt>, <a>traverse__POP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>POP</a> f xss -&gt; g ()
--   <tt>traverse_</tt>, <a>traverse__SOP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>SOP</a> f xss -&gt; g ()
--   </pre>
htraverse_ :: (HTraverse_ h, SListIN h xs, Applicative g) => (forall a. f a -> g ()) -> h f xs -> g ()

-- | A generalization of <a>sequenceA</a>.
class HAp h => HSequence (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>sequenceA</a>.
--   
--   Lifts an applicative functor out of a structure.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hsequence'</a>, <a>sequence'_NP</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> f) =&gt; <a>NP</a>  (f <a>:.:</a> g) xs  -&gt; f (<a>NP</a>  g xs )
--   <a>hsequence'</a>, <a>sequence'_NS</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> f) =&gt; <a>NS</a>  (f <a>:.:</a> g) xs  -&gt; f (<a>NS</a>  g xs )
--   <a>hsequence'</a>, <a>sequence'_POP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> f) =&gt; <a>POP</a> (f <a>:.:</a> g) xss -&gt; f (<a>POP</a> g xss)
--   <a>hsequence'</a>, <a>sequence'_SOP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> f) =&gt; <a>SOP</a> (f <a>:.:</a> g) xss -&gt; f (<a>SOP</a> g xss)
--   </pre>
hsequence' :: (HSequence h, SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs)

-- | Corresponds to <a>traverse</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hctraverse'</a>, <a>ctraverse'_NP</a>  :: (<a>All</a>  c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NP</a>  f xs  -&gt; g (<a>NP</a>  f' xs )
--   <a>hctraverse'</a>, <a>ctraverse'_NS</a>  :: (<a>All2</a> c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NS</a>  f xs  -&gt; g (<a>NS</a>  f' xs )
--   <a>hctraverse'</a>, <a>ctraverse'_POP</a> :: (<a>All</a>  c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>POP</a> f xss -&gt; g (<a>POP</a> f' xss)
--   <a>hctraverse'</a>, <a>ctraverse'_SOP</a> :: (<a>All2</a> c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>SOP</a> f xss -&gt; g (<a>SOP</a> f' xss)
--   </pre>
hctraverse' :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> h f xs -> g (h f' xs)

-- | Unconstrained variant of <a>hctraverse'</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>htraverse'</a>, <a>traverse'_NP</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NP</a>  f xs  -&gt; g (<a>NP</a>  f' xs )
--   <a>htraverse'</a>, <a>traverse'_NS</a>  :: (<a>SListI2</a> xs , <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NS</a>  f xs  -&gt; g (<a>NS</a>  f' xs )
--   <a>htraverse'</a>, <a>traverse'_POP</a> :: (<a>SListI</a>  xss, <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>POP</a> f xss -&gt; g (<a>POP</a> f' xss)
--   <a>htraverse'</a>, <a>traverse'_SOP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>SOP</a> f xss -&gt; g (<a>SOP</a> f' xss)
--   </pre>
htraverse' :: (HSequence h, SListIN h xs, Applicative g) => (forall a. f a -> g (f' a)) -> h f xs -> g (h f' xs)

-- | Special case of <a>hctraverse_</a>.
hcfoldMap :: (HTraverse_ h, AllN h c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> h f xs -> m

-- | Flipped version of <a>hctraverse_</a>.
hcfor_ :: (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g ()) -> g ()

-- | Special case of <a>hsequence'</a> where <tt>g = <a>I</a></tt>.
hsequence :: (SListIN h xs, SListIN (Prod h) xs, HSequence h) => Applicative f => h f xs -> f (h I xs)

-- | Special case of <a>hsequence'</a> where <tt>g = <a>K</a> a</tt>.
hsequenceK :: (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) => h (K (f a)) xs -> f (h (K a) xs)

-- | Special case of <a>hctraverse'</a> where <tt>f' = <a>I</a></tt>.
hctraverse :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)

-- | Flipped version of <a>hctraverse</a>.
hcfor :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g a) -> g (h I xs)

-- | A class for determining which choice in a sum-like structure a value
--   represents.
class HIndex (h :: (k -> Type) -> (l -> Type))

-- | If <tt>h</tt> is a sum-like structure representing a choice between
--   <tt>n</tt> different options, and <tt>x</tt> is a value of type <tt>h
--   f xs</tt>, then <tt><a>hindex</a> x</tt> returns a number between
--   <tt>0</tt> and <tt>n - 1</tt> representing the index of the choice
--   made by <tt>x</tt>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hindex</a>, <a>index_NS</a>  :: <a>NS</a>  f xs -&gt; Int
--   <a>hindex</a>, <a>index_SOP</a> :: <a>SOP</a> f xs -&gt; Int
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hindex (S (S (Z (I False))))
--   2
--   
--   &gt;&gt;&gt; hindex (Z (K ()))
--   0
--   
--   &gt;&gt;&gt; hindex (SOP (S (Z (I True :* I 'x' :* Nil))))
--   1
--   </pre>
hindex :: HIndex h => h f xs -> Int

-- | Maps a structure containing products to the corresponding sum
--   structure.
type family UnProd (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)

-- | A class for applying all injections corresponding to a sum-like
--   structure to a table containing suitable arguments.
class (UnProd (Prod h) ~ h) => HApInjs (h :: (k -> Type) -> (l -> Type))

-- | For a given table (product-like structure), produce a list where each
--   element corresponds to the application of an injection function into
--   the corresponding sum-like structure.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hapInjs</a>, <a>apInjs_NP</a>  :: <a>SListI</a>  xs  =&gt; <a>NP</a>  f xs -&gt; [<a>NS</a>  f xs ]
--   <a>hapInjs</a>, <a>apInjs_SOP</a> :: <a>SListI2</a> xss =&gt; <a>POP</a> f xs -&gt; [<a>SOP</a> f xss]
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hapInjs (I 'x' :* I True :* I 2 :* Nil) :: [NS I '[Char, Bool, Int]]
--   [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; hapInjs (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil)) :: [SOP I '[ '[Char], '[Bool, Int]]]
--   [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]
--   </pre>
--   
--   Unfortunately the type-signatures are required in GHC-7.10 and older.
hapInjs :: (HApInjs h, SListIN h xs) => Prod h f xs -> [h f xs]

-- | A class for expanding sum structures into corresponding product
--   structures, filling in the slots not targeted by the sum with default
--   values.
class HExpand (h :: (k -> Type) -> (l -> Type))

-- | Expand a given sum structure into a corresponding product structure by
--   placing the value contained in the sum into the corresponding position
--   in the product, and using the given default value for all other
--   positions.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hexpand</a>, <a>expand_NS</a>  :: <a>SListI</a> xs   =&gt; (forall x . f x) -&gt; <a>NS</a>  f xs  -&gt; <a>NP</a>  f xs
--   <a>hexpand</a>, <a>expand_SOP</a> :: <a>SListI2</a> xss =&gt; (forall x . f x) -&gt; <a>SOP</a> f xss -&gt; <a>POP</a> f xss
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hexpand Nothing (S (Z (Just 3))) :: NP Maybe '[Char, Int, Bool]
--   Nothing :* Just 3 :* Nothing :* Nil
--   
--   &gt;&gt;&gt; hexpand [] (SOP (S (Z ([1,2] :* "xyz" :* Nil)))) :: POP [] '[ '[Bool], '[Int, Char] ]
--   POP (([] :* Nil) :* ([1,2] :* "xyz" :* Nil) :* Nil)
--   </pre>
hexpand :: (HExpand h, SListIN (Prod h) xs) => (forall x. f x) -> h f xs -> Prod h f xs

-- | Variant of <a>hexpand</a> that allows passing a constrained default.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcexpand</a>, <a>cexpand_NS</a>  :: <a>All</a>  c xs  =&gt; proxy c -&gt; (forall x . c x =&gt; f x) -&gt; <a>NS</a>  f xs  -&gt; <a>NP</a>  f xs
--   <a>hcexpand</a>, <a>cexpand_SOP</a> :: <a>All2</a> c xss =&gt; proxy c -&gt; (forall x . c x =&gt; f x) -&gt; <a>SOP</a> f xss -&gt; <a>POP</a> f xss
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hcexpand (Proxy :: Proxy Bounded) (I minBound) (S (Z (I 20))) :: NP I '[Bool, Int, Ordering]
--   I False :* I 20 :* I LT :* Nil
--   
--   &gt;&gt;&gt; hcexpand (Proxy :: Proxy Num) (I 0) (SOP (S (Z (I 1 :* I 2 :* Nil)))) :: POP I '[ '[Double], '[Int, Int] ]
--   POP ((I 0.0 :* Nil) :* (I 1 :* I 2 :* Nil) :* Nil)
--   </pre>
hcexpand :: (HExpand h, AllN (Prod h) c xs) => proxy c -> (forall x. c x => f x) -> h f xs -> Prod h f xs

-- | A class for transforming structures into related structures with a
--   different index list, as long as the index lists have the same shape
--   and the elements and interpretation functions are suitably related.
class (Same h1 ~ h2, Same h2 ~ h1) => HTrans (h1 :: (k1 -> Type) -> (l1 -> Type)) (h2 :: (k2 -> Type) -> (l2 -> Type))

-- | Transform a structure into a related structure given a conversion
--   function for the elements.
htrans :: (HTrans h1 h2, AllZipN (Prod h1) c xs ys) => proxy c -> (forall x y. c x y => f x -> g y) -> h1 f xs -> h2 g ys

-- | Safely coerce a structure into a representationally equal structure.
--   
--   This is a special case of <a>htrans</a>, but can be implemented more
--   efficiently; for example in terms of <a>unsafeCoerce</a>.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hcoerce (I (Just LT) :* I (Just 'x') :* I (Just True) :* Nil) :: NP Maybe '[Ordering, Char, Bool]
--   Just LT :* Just 'x' :* Just True :* Nil
--   
--   &gt;&gt;&gt; hcoerce (SOP (Z (K True :* K False :* Nil))) :: SOP I '[ '[Bool, Bool], '[Bool] ]
--   SOP (Z (I True :* I False :* Nil))
--   </pre>
hcoerce :: (HTrans h1 h2, AllZipN (Prod h1) (LiftedCoercible f g) xs ys) => h1 f xs -> h2 g ys

-- | Specialization of <a>hcoerce</a>.
hfromI :: (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) => h1 I xs -> h2 f ys

-- | Specialization of <a>hcoerce</a>.
htoI :: (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) => h1 f xs -> h2 I ys


-- | Singleton types corresponding to type-level data structures.
--   
--   The implementation is similar, but subtly different to that of the
--   <tt><a>singletons</a></tt> package. See the <a>"True Sums of
--   Products"</a> paper for details.
module Data.SOP.Sing

-- | Explicit singleton list.
--   
--   A singleton list can be used to reveal the structure of a type-level
--   list argument that the function is quantified over. For every
--   type-level list <tt>xs</tt>, there is one non-bottom value of type
--   <tt><a>SList</a> xs</tt>.
--   
--   Note that these singleton lists are polymorphic in the list elements;
--   we do not require a singleton representation for them.
data SList :: [k] -> Type
[SNil] :: SList '[]
[SCons] :: SListI xs => SList (x ': xs)

-- | Implicit singleton list.
--   
--   A singleton list can be used to reveal the structure of a type-level
--   list argument that the function is quantified over.
--   
--   Since 0.4.0.0, this is now defined in terms of <a>All</a>. A singleton
--   list provides a witness for a type-level list where the elements need
--   not satisfy any additional constraints.
type SListI = All Top

-- | Get hold of an explicit singleton (that one can then pattern match on)
--   for a type-level list
sList :: SListI xs => SList xs

-- | Paramorphism for a type-level list.
para_SList :: SListI xs => r '[] -> (forall y ys. SListI ys => r ys -> r (y ': ys)) -> r xs

-- | Case distinction on a type-level list.
case_SList :: SListI xs => r '[] -> (forall y ys. SListI ys => r (y ': ys)) -> r xs

-- | Occasionally it is useful to have an explicit, term-level,
--   representation of type-level lists (esp because of
--   <a>https://ghc.haskell.org/trac/ghc/ticket/9108</a> )
data Shape :: [k] -> Type
[ShapeNil] :: Shape '[]
[ShapeCons] :: SListI xs => Shape xs -> Shape (x ': xs)

-- | The shape of a type-level list.
shape :: forall k (xs :: [k]). SListI xs => Shape xs

-- | The length of a type-level list.
lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int
instance forall k (xs :: [k]). GHC.Show.Show (Data.SOP.Sing.SList xs)
instance forall k (xs :: [k]). GHC.Classes.Eq (Data.SOP.Sing.SList xs)
instance forall k (xs :: [k]). GHC.Classes.Ord (Data.SOP.Sing.SList xs)
instance forall k (xs :: [k]). GHC.Show.Show (Data.SOP.Sing.Shape xs)
instance forall k (xs :: [k]). GHC.Classes.Eq (Data.SOP.Sing.Shape xs)
instance forall k (xs :: [k]). GHC.Classes.Ord (Data.SOP.Sing.Shape xs)


-- | n-ary products (and products of products)
module Data.SOP.NP

-- | An n-ary product.
--   
--   The product is parameterized by a type constructor <tt>f</tt> and
--   indexed by a type-level list <tt>xs</tt>. The length of the list
--   determines the number of elements in the product, and if the
--   <tt>i</tt>-th element of the list is of type <tt>x</tt>, then the
--   <tt>i</tt>-th element of the product is of type <tt>f x</tt>.
--   
--   The constructor names are chosen to resemble the names of the list
--   constructors.
--   
--   Two common instantiations of <tt>f</tt> are the identity functor
--   <a>I</a> and the constant functor <a>K</a>. For <a>I</a>, the product
--   becomes a heterogeneous list, where the type-level list describes the
--   types of its components. For <tt><a>K</a> a</tt>, the product becomes
--   a homogeneous list, where the contents of the type-level list are
--   ignored, but its length still specifies the number of elements.
--   
--   In the context of the SOP approach to generic programming, an n-ary
--   product describes the structure of the arguments of a single data
--   constructor.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   I 'x'    :* I True  :* Nil  ::  NP I       '[ Char, Bool ]
--   K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
--   Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]
--   </pre>
data NP :: (k -> Type) -> [k] -> Type
[Nil] :: NP f '[]
[:*] :: f x -> NP f xs -> NP f (x ': xs)
infixr 5 :*

-- | A product of products.
--   
--   This is a 'newtype' for an <a>NP</a> of an <a>NP</a>. The elements of
--   the inner products are applications of the parameter <tt>f</tt>. The
--   type <a>POP</a> is indexed by the list of lists that determines the
--   lengths of both the outer and all the inner products, as well as the
--   types of all the elements of the inner products.
--   
--   A <a>POP</a> is reminiscent of a two-dimensional table (but the inner
--   lists can all be of different length). In the context of the SOP
--   approach to generic programming, a <a>POP</a> is useful to represent
--   information that is available for all arguments of all constructors of
--   a datatype.
newtype POP (f :: (k -> Type)) (xss :: [[k]])
POP :: NP (NP f) xss -> POP (f :: k -> Type) (xss :: [[k]])

-- | Unwrap a product of products.
unPOP :: POP f xss -> NP (NP f) xss

-- | Specialization of <a>hpure</a>.
--   
--   The call <tt><a>pure_NP</a> x</tt> generates a product that contains
--   <tt>x</tt> in every element position.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; pure_NP [] :: NP [] '[Char, Bool]
--   "" :* [] :* Nil
--   
--   &gt;&gt;&gt; pure_NP (K 0) :: NP (K Int) '[Double, Int, String]
--   K 0 :* K 0 :* K 0 :* Nil
--   </pre>
pure_NP :: forall f xs. SListI xs => (forall a. f a) -> NP f xs

-- | Specialization of <a>hpure</a>.
--   
--   The call <tt><a>pure_POP</a> x</tt> generates a product of products
--   that contains <tt>x</tt> in every element position.
pure_POP :: All SListI xss => (forall a. f a) -> POP f xss

-- | Specialization of <a>hcpure</a>.
--   
--   The call <tt><a>cpure_NP</a> p x</tt> generates a product that
--   contains <tt>x</tt> in every element position.
cpure_NP :: forall c xs proxy f. All c xs => proxy c -> (forall a. c a => f a) -> NP f xs

-- | Specialization of <a>hcpure</a>.
--   
--   The call <tt><a>cpure_NP</a> p x</tt> generates a product of products
--   that contains <tt>x</tt> in every element position.
cpure_POP :: forall c xss proxy f. All2 c xss => proxy c -> (forall a. c a => f a) -> POP f xss

-- | Construct a homogeneous n-ary product from a normal Haskell list.
--   
--   Returns <a>Nothing</a> if the length of the list does not exactly
--   match the expected size of the product.
fromList :: SListI xs => [a] -> Maybe (NP (K a) xs)

-- | Specialization of <a>hap</a>.
--   
--   Applies a product of (lifted) functions pointwise to a product of
--   suitable arguments.
ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs

-- | Specialization of <a>hap</a>.
--   
--   Applies a product of (lifted) functions pointwise to a product of
--   suitable arguments.
ap_POP :: POP (f -.-> g) xss -> POP f xss -> POP g xss

-- | Obtain the head of an n-ary product.
hd :: NP f (x ': xs) -> f x

-- | Obtain the tail of an n-ary product.
tl :: NP f (x ': xs) -> NP f xs

-- | The type of projections from an n-ary product.
--   
--   A projection is a function from the n-ary product to a single element.
type Projection (f :: k -> Type) (xs :: [k]) = K (NP f xs) -.-> f

-- | Compute all projections from an n-ary product.
--   
--   Each element of the resulting product contains one of the projections.
projections :: forall xs f. SListI xs => NP (Projection f xs) xs
shiftProjection :: Projection f xs a -> Projection f (x ': xs) a

-- | Specialization of <a>hliftA</a>.
liftA_NP :: SListI xs => (forall a. f a -> g a) -> NP f xs -> NP g xs

-- | Specialization of <a>hliftA</a>.
liftA_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss

-- | Specialization of <a>hliftA2</a>.
liftA2_NP :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

-- | Specialization of <a>hliftA2</a>.
liftA2_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

-- | Specialization of <a>hliftA3</a>.
liftA3_NP :: SListI xs => (forall a. f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs

-- | Specialization of <a>hliftA3</a>.
liftA3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

-- | Specialization of <a>hmap</a>, which is equivalent to <a>hliftA</a>.
map_NP :: SListI xs => (forall a. f a -> g a) -> NP f xs -> NP g xs

-- | Specialization of <a>hmap</a>, which is equivalent to <a>hliftA</a>.
map_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss

-- | Specialization of <a>hzipWith</a>, which is equivalent to
--   <a>hliftA2</a>.
zipWith_NP :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

-- | Specialization of <a>hzipWith</a>, which is equivalent to
--   <a>hliftA2</a>.
zipWith_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

-- | Specialization of <a>hzipWith3</a>, which is equivalent to
--   <a>hliftA3</a>.
zipWith3_NP :: SListI xs => (forall a. f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs

-- | Specialization of <a>hzipWith3</a>, which is equivalent to
--   <a>hliftA3</a>.
zipWith3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

-- | Specialization of <a>hcliftA</a>.
cliftA_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs

-- | Specialization of <a>hcliftA</a>.
cliftA_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP f xss -> POP g xss

-- | Specialization of <a>hcliftA2</a>.
cliftA2_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

-- | Specialization of <a>hcliftA2</a>.
cliftA2_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

-- | Specialization of <a>hcliftA3</a>.
cliftA3_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs

-- | Specialization of <a>hcliftA3</a>.
cliftA3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

-- | Specialization of <a>hcmap</a>, which is equivalent to <a>hcliftA</a>.
cmap_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> NP g xs

-- | Specialization of <a>hcmap</a>, which is equivalent to <a>hcliftA</a>.
cmap_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP f xss -> POP g xss

-- | Specialization of <a>hczipWith</a>, which is equivalent to
--   <a>hcliftA2</a>.
czipWith_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NP g xs -> NP h xs

-- | Specialization of <a>hczipWith</a>, which is equivalent to
--   <a>hcliftA2</a>.
czipWith_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

-- | Specialization of <a>hczipWith3</a>, which is equivalent to
--   <a>hcliftA3</a>.
czipWith3_NP :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP f xs -> NP g xs -> NP h xs -> NP i xs

-- | Specialization of <a>hczipWith3</a>, which is equivalent to
--   <a>hcliftA3</a>.
czipWith3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

-- | Lift a constrained function operating on a list-indexed structure to a
--   function on a list-of-list-indexed structure.
--   
--   This is a variant of <a>hcliftA</a>.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA'</a> p f xs = <a>hpure</a> (<a>fn_2</a> $ \ <tt>AllDictC</tt> -&gt; f) ` <a>hap</a> ` <tt>allDict_NP</tt> p ` <a>hap</a> ` xs
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcliftA'</a> :: <a>All2</a> c xss =&gt; proxy c -&gt; (forall xs. <a>All</a> c xs =&gt; f xs -&gt; f' xs) -&gt; <a>NP</a> f xss -&gt; <a>NP</a> f' xss
--   <a>hcliftA'</a> :: <a>All2</a> c xss =&gt; proxy c -&gt; (forall xs. <a>All</a> c xs =&gt; f xs -&gt; f' xs) -&gt; <a>NS</a> f xss -&gt; <a>NS</a> f' xss
--   </pre>

-- | <i>Deprecated: Use <a>hcliftA</a> or <a>hcmap</a> instead.</i>
hcliftA' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs) -> h f xss -> h f' xss

-- | Like <a>hcliftA'</a>, but for binary functions.

-- | <i>Deprecated: Use <a>hcliftA2</a> or <a>hczipWith</a> instead.</i>
hcliftA2' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs) -> Prod h f xss -> h f' xss -> h f'' xss

-- | Like <a>hcliftA'</a>, but for ternary functions.

-- | <i>Deprecated: Use <a>hcliftA3</a> or <a>hczipWith3</a> instead.</i>
hcliftA3' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss

-- | Specialization of <a>hcliftA2'</a>.

-- | <i>Deprecated: Use <a>cliftA2_NP</a> instead.</i>
cliftA2'_NP :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss

-- | Specialization of <a>hcollapse</a>.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; collapse_NP (K 1 :* K 2 :* K 3 :* Nil)
--   [1,2,3]
--   </pre>
collapse_NP :: NP (K a) xs -> [a]

-- | Specialization of <a>hcollapse</a>.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; collapse_POP (POP ((K 'a' :* Nil) :* (K 'b' :* K 'c' :* Nil) :* Nil) :: POP (K Char) '[ '[(a :: Type)], '[b, c] ])
--   ["a","bc"]
--   </pre>
--   
--   (The type signature is only necessary in this case to fix the kind of
--   the type variables.)
collapse_POP :: SListI xss => POP (K a) xss -> [[a]]

-- | Specialization of <a>hctraverse_</a>.
ctraverse__NP :: forall c proxy xs f g. (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g ()

-- | Specialization of <a>hctraverse_</a>.
ctraverse__POP :: forall c proxy xss f g. (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> POP f xss -> g ()

-- | Specialization of <a>htraverse_</a>.
traverse__NP :: forall xs f g. (SListI xs, Applicative g) => (forall a. f a -> g ()) -> NP f xs -> g ()

-- | Specialization of <a>htraverse_</a>.
traverse__POP :: forall xss f g. (SListI2 xss, Applicative g) => (forall a. f a -> g ()) -> POP f xss -> g ()

-- | Specialization of <a>hcfoldMap</a>.
cfoldMap_NP :: (All c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> NP f xs -> m

-- | Specialization of <a>hcfoldMap</a>.
cfoldMap_POP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> POP f xs -> m

-- | Specialization of <a>hsequence'</a>.
sequence'_NP :: Applicative f => NP (f :.: g) xs -> f (NP g xs)

-- | Specialization of <a>hsequence'</a>.
sequence'_POP :: (SListI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)

-- | Specialization of <a>hsequence</a>.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; sequence_NP (Just 1 :* Just 2 :* Nil)
--   Just (I 1 :* I 2 :* Nil)
--   </pre>
sequence_NP :: (SListI xs, Applicative f) => NP f xs -> f (NP I xs)

-- | Specialization of <a>hsequence</a>.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; sequence_POP (POP ((Just 1 :* Nil) :* (Just 2 :* Just 3 :* Nil) :* Nil))
--   Just (POP ((I 1 :* Nil) :* (I 2 :* I 3 :* Nil) :* Nil))
--   </pre>
sequence_POP :: (All SListI xss, Applicative f) => POP f xss -> f (POP I xss)

-- | Specialization of <a>hctraverse'</a>.
ctraverse'_NP :: forall c proxy xs f f' g. (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs -> g (NP f' xs)

-- | Specialization of <a>hctraverse'</a>.
ctraverse'_POP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> POP f xss -> g (POP f' xss)

-- | Specialization of <a>htraverse'</a>.
traverse'_NP :: forall xs f f' g. (SListI xs, Applicative g) => (forall a. f a -> g (f' a)) -> NP f xs -> g (NP f' xs)

-- | Specialization of <a>hctraverse'</a>.
traverse'_POP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> POP f xss -> g (POP f' xss)

-- | Specialization of <a>hctraverse</a>.
ctraverse_NP :: (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)

-- | Specialization of <a>hctraverse</a>.
ctraverse_POP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)

-- | Catamorphism for <a>NP</a>.
--   
--   This is a suitable generalization of <a>foldr</a>. It takes parameters
--   on what to do for <a>Nil</a> and <a>:*</a>. Since the input list is
--   heterogeneous, the result is also indexed by a type-level list.
cata_NP :: forall r f xs. r '[] -> (forall y ys. f y -> r ys -> r (y ': ys)) -> NP f xs -> r xs

-- | Constrained catamorphism for <a>NP</a>.
--   
--   The difference compared to <a>cata_NP</a> is that the function for the
--   cons-case can make use of the fact that the specified constraint holds
--   for all the types in the signature of the product.
ccata_NP :: forall c proxy r f xs. All c xs => proxy c -> r '[] -> (forall y ys. c y => f y -> r ys -> r (y ': ys)) -> NP f xs -> r xs

-- | Anamorphism for <a>NP</a>.
--   
--   In contrast to the anamorphism for normal lists, the generating
--   function does not return an <a>Either</a>, but simply an element and a
--   new seed value.
--   
--   This is because the decision on whether to generate a <a>Nil</a> or a
--   <a>:*</a> is determined by the types.
ana_NP :: forall s f xs. SListI xs => (forall y ys. s (y ': ys) -> (f y, s ys)) -> s xs -> NP f xs

-- | Constrained anamorphism for <a>NP</a>.
--   
--   Compared to <a>ana_NP</a>, the generating function can make use of the
--   specified constraint here for the elements that it generates.
cana_NP :: forall c proxy s f xs. All c xs => proxy c -> (forall y ys. c y => s (y ': ys) -> (f y, s ys)) -> s xs -> NP f xs

-- | Specialization of <a>htrans</a>.
trans_NP :: AllZip c xs ys => proxy c -> (forall x y. c x y => f x -> g y) -> NP f xs -> NP g ys

-- | Specialization of <a>htrans</a>.
trans_POP :: AllZip2 c xss yss => proxy c -> (forall x y. c x y => f x -> g y) -> POP f xss -> POP g yss

-- | Specialization of <a>hcoerce</a>.
coerce_NP :: forall f g xs ys. AllZip (LiftedCoercible f g) xs ys => NP f xs -> NP g ys

-- | Specialization of <a>hcoerce</a>.
coerce_POP :: forall f g xss yss. AllZip2 (LiftedCoercible f g) xss yss => POP f xss -> POP g yss

-- | Specialization of <a>hfromI</a>.
fromI_NP :: forall f xs ys. AllZip (LiftedCoercible I f) xs ys => NP I xs -> NP f ys

-- | Specialization of <a>hfromI</a>.
fromI_POP :: forall f xss yss. AllZip2 (LiftedCoercible I f) xss yss => POP I xss -> POP f yss

-- | Specialization of <a>htoI</a>.
toI_NP :: forall f xs ys. AllZip (LiftedCoercible f I) xs ys => NP f xs -> NP I ys

-- | Specialization of <a>htoI</a>.
toI_POP :: forall f xss yss. AllZip2 (LiftedCoercible f I) xss yss => POP f xss -> POP I yss
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Classes.Eq f) xs => GHC.Classes.Eq (Data.SOP.NP.NP f xs)
instance forall k (f :: k -> *) (xs :: [k]). (Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Classes.Eq f) xs, Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Classes.Ord f) xs) => GHC.Classes.Ord (Data.SOP.NP.NP f xs)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Show.Show (Data.SOP.NP.NP (Data.SOP.NP.NP f) xss) => GHC.Show.Show (Data.SOP.NP.POP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Classes.Eq (Data.SOP.NP.NP (Data.SOP.NP.NP f) xss) => GHC.Classes.Eq (Data.SOP.NP.POP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Classes.Ord (Data.SOP.NP.NP (Data.SOP.NP.NP f) xss) => GHC.Classes.Ord (Data.SOP.NP.POP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Base.Semigroup (Data.SOP.NP.NP (Data.SOP.NP.NP f) xss) => GHC.Base.Semigroup (Data.SOP.NP.POP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Base.Monoid (Data.SOP.NP.NP (Data.SOP.NP.NP f) xss) => GHC.Base.Monoid (Data.SOP.NP.POP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). Control.DeepSeq.NFData (Data.SOP.NP.NP (Data.SOP.NP.NP f) xss) => Control.DeepSeq.NFData (Data.SOP.NP.POP f xss)
instance Data.SOP.Classes.HPure Data.SOP.NP.POP
instance Data.SOP.Classes.HAp Data.SOP.NP.POP
instance Data.SOP.Classes.HCollapse Data.SOP.NP.POP
instance Data.SOP.Classes.HTraverse_ Data.SOP.NP.POP
instance Data.SOP.Classes.HSequence Data.SOP.NP.POP
instance Data.SOP.Classes.HTrans Data.SOP.NP.POP Data.SOP.NP.POP
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Show.Show f) xs => GHC.Show.Show (Data.SOP.NP.NP f xs)
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Base.Semigroup f) xs => GHC.Base.Semigroup (Data.SOP.NP.NP f xs)
instance forall k (f :: k -> *) (xs :: [k]). (Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Base.Monoid f) xs, Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Base.Semigroup f) xs) => GHC.Base.Monoid (Data.SOP.NP.NP f xs)
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose Control.DeepSeq.NFData f) xs => Control.DeepSeq.NFData (Data.SOP.NP.NP f xs)
instance Data.SOP.Classes.HPure Data.SOP.NP.NP
instance Data.SOP.Classes.HAp Data.SOP.NP.NP
instance Data.SOP.Classes.HCollapse Data.SOP.NP.NP
instance Data.SOP.Classes.HTraverse_ Data.SOP.NP.NP
instance Data.SOP.Classes.HSequence Data.SOP.NP.NP
instance Data.SOP.Classes.HTrans Data.SOP.NP.NP Data.SOP.NP.NP


-- | n-ary sums (and sums of products)
module Data.SOP.NS

-- | An n-ary sum.
--   
--   The sum is parameterized by a type constructor <tt>f</tt> and indexed
--   by a type-level list <tt>xs</tt>. The length of the list determines
--   the number of choices in the sum and if the <tt>i</tt>-th element of
--   the list is of type <tt>x</tt>, then the <tt>i</tt>-th choice of the
--   sum is of type <tt>f x</tt>.
--   
--   The constructor names are chosen to resemble Peano-style natural
--   numbers, i.e., <a>Z</a> is for "zero", and <a>S</a> is for
--   "successor". Chaining <a>S</a> and <a>Z</a> chooses the corresponding
--   component of the sum.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   Z         :: f x -&gt; NS f (x ': xs)
--   S . Z     :: f y -&gt; NS f (x ': y ': xs)
--   S . S . Z :: f z -&gt; NS f (x ': y ': z ': xs)
--   ...
--   </pre>
--   
--   Note that empty sums (indexed by an empty list) have no non-bottom
--   elements.
--   
--   Two common instantiations of <tt>f</tt> are the identity functor
--   <a>I</a> and the constant functor <a>K</a>. For <a>I</a>, the sum
--   becomes a direct generalization of the <a>Either</a> type to
--   arbitrarily many choices. For <tt><a>K</a> a</tt>, the result is a
--   homogeneous choice type, where the contents of the type-level list are
--   ignored, but its length specifies the number of options.
--   
--   In the context of the SOP approach to generic programming, an n-ary
--   sum describes the top-level structure of a datatype, which is a choice
--   between all of its constructors.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   Z (I 'x')      :: NS I       '[ Char, Bool ]
--   S (Z (I True)) :: NS I       '[ Char, Bool ]
--   S (Z (K 1))    :: NS (K Int) '[ Char, Bool ]
--   </pre>
data NS :: (k -> Type) -> [k] -> Type
[Z] :: f x -> NS f (x ': xs)
[S] :: NS f xs -> NS f (x ': xs)

-- | A sum of products.
--   
--   This is a 'newtype' for an <a>NS</a> of an <a>NP</a>. The elements of
--   the (inner) products are applications of the parameter <tt>f</tt>. The
--   type <a>SOP</a> is indexed by the list of lists that determines the
--   sizes of both the (outer) sum and all the (inner) products, as well as
--   the types of all the elements of the inner products.
--   
--   A <tt><a>SOP</a> <a>I</a></tt> reflects the structure of a normal
--   Haskell datatype. The sum structure represents the choice between the
--   different constructors, the product structure represents the arguments
--   of each constructor.
newtype SOP (f :: (k -> Type)) (xss :: [[k]])
SOP :: NS (NP f) xss -> SOP (f :: k -> Type) (xss :: [[k]])

-- | Unwrap a sum of products.
unSOP :: SOP f xss -> NS (NP f) xss

-- | The type of injections into an n-ary sum.
--   
--   If you expand the type synonyms and newtypes involved, you get
--   
--   <pre>
--   Injection f xs a = (f -.-&gt; K (NS f xs)) a ~= f a -&gt; K (NS f xs) a ~= f a -&gt; NS f xs
--   </pre>
--   
--   If we pick <tt>a</tt> to be an element of <tt>xs</tt>, this indeed
--   corresponds to an injection into the sum.
type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)

-- | Compute all injections into an n-ary sum.
--   
--   Each element of the resulting product contains one of the injections.
injections :: forall xs f. SListI xs => NP (Injection f xs) xs

-- | Shift an injection.
--   
--   Given an injection, return an injection into a sum that is one
--   component larger.

-- | <i>Deprecated: Use <a>shiftInjection</a> instead.</i>
shift :: Injection f xs a -> Injection f (x ': xs) a

-- | Shift an injection.
--   
--   Given an injection, return an injection into a sum that is one
--   component larger.
shiftInjection :: Injection f xs a -> Injection f (x ': xs) a

-- | Apply injections to a product.
--   
--   Given a product containing all possible choices, produce a list of
--   sums by applying each injection to the appropriate element.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; apInjs_NP (I 'x' :* I True :* I 2 :* Nil)
--   [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]
--   </pre>
apInjs_NP :: SListI xs => NP f xs -> [NS f xs]

-- | <a>apInjs_NP</a> without <a>hcollapse</a>.
--   
--   <pre>
--   &gt;&gt;&gt; apInjs'_NP (I 'x' :* I True :* I 2 :* Nil)
--   K (Z (I 'x')) :* K (S (Z (I True))) :* K (S (S (Z (I 2)))) :* Nil
--   </pre>
apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs

-- | Apply injections to a product of product.
--   
--   This operates on the outer product only. Given a product containing
--   all possible choices (that are products), produce a list of sums (of
--   products) by applying each injection to the appropriate element.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; apInjs_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))
--   [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]
--   </pre>
apInjs_POP :: SListI xss => POP f xss -> [SOP f xss]

-- | <a>apInjs_POP</a> without <a>hcollapse</a>.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; apInjs'_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))
--   K (SOP (Z (I 'x' :* Nil))) :* K (SOP (S (Z (I True :* I 2 :* Nil)))) :* Nil
--   </pre>
apInjs'_POP :: SListI xss => POP f xss -> NP (K (SOP f xss)) xss

-- | Extract the payload from a unary sum.
--   
--   For larger sums, this function would be partial, so it is only
--   provided with a rather restrictive type.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; unZ (Z (I 'x'))
--   I 'x'
--   </pre>
unZ :: NS f '[x] -> f x

-- | Obtain the index from an n-ary sum.
--   
--   An n-nary sum represents a choice between n different options. This
--   function returns an integer between 0 and n - 1 indicating the option
--   chosen by the given value.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; index_NS (S (S (Z (I False))))
--   2
--   
--   &gt;&gt;&gt; index_NS (Z (K ()))
--   0
--   </pre>
index_NS :: forall f xs. NS f xs -> Int

-- | Obtain the index from an n-ary sum of products.
--   
--   An n-nary sum represents a choice between n different options. This
--   function returns an integer between 0 and n - 1 indicating the option
--   chosen by the given value.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>index_SOP</a> = <a>index_NS</a> <a>.</a> <a>unSOP</a>
--   </pre>
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; index_SOP (SOP (S (Z (I True :* I 'x' :* Nil))))
--   1
--   </pre>
index_SOP :: SOP f xs -> Int

-- | The type of ejections from an n-ary sum.
--   
--   An ejection is the pattern matching function for one part of the n-ary
--   sum.
--   
--   It is the opposite of an <a>Injection</a>.
type Ejection (f :: k -> Type) (xs :: [k]) = K (NS f xs) -.-> Maybe :.: f

-- | Compute all ejections from an n-ary sum.
--   
--   Each element of the resulting product contains one of the ejections.
ejections :: forall xs f. SListI xs => NP (Ejection f xs) xs

shiftEjection :: forall f x xs a. Ejection f xs a -> Ejection f (x ': xs) a

-- | Specialization of <a>hap</a>.
ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs

-- | Specialization of <a>hap</a>.
ap_SOP :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss

-- | Specialization of <a>hliftA</a>.
liftA_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs

-- | Specialization of <a>hliftA</a>.
liftA_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss

-- | Specialization of <a>hliftA2</a>.
liftA2_NS :: SListI xs => (forall a. f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs

-- | Specialization of <a>hliftA2</a>.
liftA2_SOP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss

-- | Specialization of <a>hcliftA</a>.
cliftA_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs

-- | Specialization of <a>hcliftA</a>.
cliftA_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss

-- | Specialization of <a>hcliftA2</a>.
cliftA2_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP f xs -> NS g xs -> NS h xs

-- | Specialization of <a>hcliftA2</a>.
cliftA2_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP h xss

-- | Specialization of <a>hmap</a>, which is equivalent to <a>hliftA</a>.
map_NS :: SListI xs => (forall a. f a -> g a) -> NS f xs -> NS g xs

-- | Specialization of <a>hmap</a>, which is equivalent to <a>hliftA</a>.
map_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss

-- | Specialization of <a>hcmap</a>, which is equivalent to <a>hcliftA</a>.
cmap_NS :: All c xs => proxy c -> (forall a. c a => f a -> g a) -> NS f xs -> NS g xs

-- | Specialization of <a>hcmap</a>, which is equivalent to <a>hcliftA</a>.
cmap_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP f xss -> SOP g xss

-- | Specialization of <a>hcliftA2'</a>.

-- | <i>Deprecated: Use <a>cliftA2_NS</a> instead.</i>
cliftA2'_NS :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NS g xss -> NS h xss

-- | Compare two sums with respect to the choice they are making.
--   
--   A value that chooses the first option is considered smaller than one
--   that chooses the second option.
--   
--   If the choices are different, then either the first (if the first is
--   smaller than the second) or the third (if the first is larger than the
--   second) argument are called. If both choices are equal, then the
--   second argument is called, which has access to the elements contained
--   in the sums.
compare_NS :: forall r f g xs. r -> (forall x. f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r

-- | Constrained version of <a>compare_NS</a>.
ccompare_NS :: forall c proxy r f g xs. All c xs => proxy c -> r -> (forall x. c x => f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r

-- | Compare two sums of products with respect to the choice in the sum
--   they are making.
--   
--   Only the sum structure is used for comparison. This is a small wrapper
--   around <a>ccompare_NS</a> for a common special case.
compare_SOP :: forall r f g xss. r -> (forall xs. NP f xs -> NP g xs -> r) -> r -> SOP f xss -> SOP g xss -> r

-- | Constrained version of <a>compare_SOP</a>.
ccompare_SOP :: forall c proxy r f g xss. All2 c xss => proxy c -> r -> (forall xs. All c xs => NP f xs -> NP g xs -> r) -> r -> SOP f xss -> SOP g xss -> r

-- | Specialization of <a>hcollapse</a>.
collapse_NS :: NS (K a) xs -> a

-- | Specialization of <a>hcollapse</a>.
collapse_SOP :: SListI xss => SOP (K a) xss -> [a]

-- | Specialization of <a>hctraverse_</a>.
--   
--   <i>Note:</i> we don't need <a>Applicative</a> constraint.
ctraverse__NS :: forall c proxy xs f g. All c xs => proxy c -> (forall a. c a => f a -> g ()) -> NS f xs -> g ()

-- | Specialization of <a>hctraverse_</a>.
ctraverse__SOP :: forall c proxy xss f g. (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> SOP f xss -> g ()

-- | Specialization of <a>htraverse_</a>.
--   
--   <i>Note:</i> we don't need <a>Applicative</a> constraint.
traverse__NS :: forall xs f g. SListI xs => (forall a. f a -> g ()) -> NS f xs -> g ()

-- | Specialization of <a>htraverse_</a>.
traverse__SOP :: forall xss f g. (SListI2 xss, Applicative g) => (forall a. f a -> g ()) -> SOP f xss -> g ()

-- | Specialization of <a>hcfoldMap</a>.
--   
--   <i>Note:</i> We don't need <a>Monoid</a> instance.
cfoldMap_NS :: forall c proxy f xs m. All c xs => proxy c -> (forall a. c a => f a -> m) -> NS f xs -> m

-- | Specialization of <a>hcfoldMap</a>.
cfoldMap_SOP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> SOP f xs -> m

-- | Specialization of <a>hsequence'</a>.
sequence'_NS :: Applicative f => NS (f :.: g) xs -> f (NS g xs)

-- | Specialization of <a>hsequence'</a>.
sequence'_SOP :: (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss)

-- | Specialization of <a>hsequence</a>.
sequence_NS :: (SListI xs, Applicative f) => NS f xs -> f (NS I xs)

-- | Specialization of <a>hsequence</a>.
sequence_SOP :: (All SListI xss, Applicative f) => SOP f xss -> f (SOP I xss)

-- | Specialization of <a>hctraverse'</a>.
--   
--   <i>Note:</i> as <a>NS</a> has exactly one element, the <a>Functor</a>
--   constraint is enough.
ctraverse'_NS :: forall c proxy xs f f' g. (All c xs, Functor g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> NS f xs -> g (NS f' xs)

-- | Specialization of <a>hctraverse'</a>.
ctraverse'_SOP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)

-- | Specialization of <a>htraverse'</a>.
--   
--   <i>Note:</i> as <a>NS</a> has exactly one element, the <a>Functor</a>
--   constraint is enough.
traverse'_NS :: forall xs f f' g. (SListI xs, Functor g) => (forall a. f a -> g (f' a)) -> NS f xs -> g (NS f' xs)

-- | Specialization of <a>htraverse'</a>.
traverse'_SOP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)

-- | Specialization of <a>hctraverse</a>.
ctraverse_NS :: (All c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)

-- | Specialization of <a>hctraverse</a>.
ctraverse_SOP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)

-- | Catamorphism for <a>NS</a>.
--   
--   Takes arguments determining what to do for <a>Z</a> and what to do for
--   <a>S</a>. The result type is still indexed over the type-level lit.
cata_NS :: forall r f xs. (forall y ys. f y -> r (y ': ys)) -> (forall y ys. r ys -> r (y ': ys)) -> NS f xs -> r xs

-- | Constrained catamorphism for <a>NS</a>.
ccata_NS :: forall c proxy r f xs. All c xs => proxy c -> (forall y ys. c y => f y -> r (y ': ys)) -> (forall y ys. c y => r ys -> r (y ': ys)) -> NS f xs -> r xs

-- | Anamorphism for <a>NS</a>.
ana_NS :: forall s f xs. SListI xs => (forall r. s '[] -> r) -> (forall y ys. s (y ': ys) -> Either (f y) (s ys)) -> s xs -> NS f xs

-- | Constrained anamorphism for <a>NS</a>.
cana_NS :: forall c proxy s f xs. All c xs => proxy c -> (forall r. s '[] -> r) -> (forall y ys. c y => s (y ': ys) -> Either (f y) (s ys)) -> s xs -> NS f xs

-- | Specialization of <a>hexpand</a>.
expand_NS :: forall f xs. SListI xs => (forall x. f x) -> NS f xs -> NP f xs

-- | Specialization of <a>hcexpand</a>.
cexpand_NS :: forall c proxy f xs. All c xs => proxy c -> (forall x. c x => f x) -> NS f xs -> NP f xs

-- | Specialization of <a>hexpand</a>.
expand_SOP :: forall f xss. All SListI xss => (forall x. f x) -> SOP f xss -> POP f xss

-- | Specialization of <a>hcexpand</a>.
cexpand_SOP :: forall c proxy f xss. All2 c xss => proxy c -> (forall x. c x => f x) -> SOP f xss -> POP f xss

-- | Specialization of <a>htrans</a>.
trans_NS :: AllZip c xs ys => proxy c -> (forall x y. c x y => f x -> g y) -> NS f xs -> NS g ys

-- | Specialization of <a>htrans</a>.
trans_SOP :: AllZip2 c xss yss => proxy c -> (forall x y. c x y => f x -> g y) -> SOP f xss -> SOP g yss

-- | Specialization of <a>hcoerce</a>.
coerce_NS :: forall f g xs ys. AllZip (LiftedCoercible f g) xs ys => NS f xs -> NS g ys

-- | Specialization of <a>hcoerce</a>.
coerce_SOP :: forall f g xss yss. AllZip2 (LiftedCoercible f g) xss yss => SOP f xss -> SOP g yss

-- | Specialization of <a>hfromI</a>.
fromI_NS :: forall f xs ys. AllZip (LiftedCoercible I f) xs ys => NS I xs -> NS f ys

-- | Specialization of <a>hfromI</a>.
fromI_SOP :: forall f xss yss. AllZip2 (LiftedCoercible I f) xss yss => SOP I xss -> SOP f yss

-- | Specialization of <a>htoI</a>.
toI_NS :: forall f xs ys. AllZip (LiftedCoercible f I) xs ys => NS f xs -> NS I ys

-- | Specialization of <a>htoI</a>.
toI_SOP :: forall f xss yss. AllZip2 (LiftedCoercible f I) xss yss => SOP f xss -> SOP I yss
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Show.Show f) xs => GHC.Show.Show (Data.SOP.NS.NS f xs)
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Classes.Eq f) xs => GHC.Classes.Eq (Data.SOP.NS.NS f xs)
instance forall k (f :: k -> *) (xs :: [k]). (Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Classes.Eq f) xs, Data.SOP.Constraint.All (Data.SOP.Constraint.Compose GHC.Classes.Ord f) xs) => GHC.Classes.Ord (Data.SOP.NS.NS f xs)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Show.Show (Data.SOP.NS.NS (Data.SOP.NP.NP f) xss) => GHC.Show.Show (Data.SOP.NS.SOP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Classes.Eq (Data.SOP.NS.NS (Data.SOP.NP.NP f) xss) => GHC.Classes.Eq (Data.SOP.NS.SOP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). GHC.Classes.Ord (Data.SOP.NS.NS (Data.SOP.NP.NP f) xss) => GHC.Classes.Ord (Data.SOP.NS.SOP f xss)
instance forall k (f :: k -> *) (xss :: [[k]]). Control.DeepSeq.NFData (Data.SOP.NS.NS (Data.SOP.NP.NP f) xss) => Control.DeepSeq.NFData (Data.SOP.NS.SOP f xss)
instance Data.SOP.Classes.HIndex Data.SOP.NS.SOP
instance Data.SOP.Classes.HApInjs Data.SOP.NS.SOP
instance Data.SOP.Classes.HAp Data.SOP.NS.SOP
instance Data.SOP.Classes.HCollapse Data.SOP.NS.SOP
instance Data.SOP.Classes.HTraverse_ Data.SOP.NS.SOP
instance Data.SOP.Classes.HSequence Data.SOP.NS.SOP
instance Data.SOP.Classes.HExpand Data.SOP.NS.SOP
instance Data.SOP.Classes.HTrans Data.SOP.NS.SOP Data.SOP.NS.SOP
instance forall k (f :: k -> *) (xs :: [k]). Data.SOP.Constraint.All (Data.SOP.Constraint.Compose Control.DeepSeq.NFData f) xs => Control.DeepSeq.NFData (Data.SOP.NS.NS f xs)
instance Data.SOP.Classes.HIndex Data.SOP.NS.NS
instance Data.SOP.Classes.HApInjs Data.SOP.NS.NS
instance Data.SOP.Classes.HAp Data.SOP.NS.NS
instance Data.SOP.Classes.HCollapse Data.SOP.NS.NS
instance Data.SOP.Classes.HTraverse_ Data.SOP.NS.NS
instance Data.SOP.Classes.HSequence Data.SOP.NS.NS
instance Data.SOP.Classes.HExpand Data.SOP.NS.NS
instance Data.SOP.Classes.HTrans Data.SOP.NS.NS Data.SOP.NS.NS


-- | Explicit dictionaries.
--   
--   When working with compound constraints such as constructed using
--   <a>All</a> or <a>All2</a>, GHC cannot always prove automatically what
--   one would expect to hold.
--   
--   This module provides a way of explicitly proving conversions between
--   such constraints to GHC. Such conversions still have to be manually
--   applied.
--   
--   This module remains somewhat experimental. It is therefore not
--   exported via the main module and has to be imported explicitly.
module Data.SOP.Dict

-- | An explicit dictionary carrying evidence of a class constraint.
--   
--   The constraint parameter is separated into a second argument so that
--   <tt><a>Dict</a> c</tt> is of the correct kind to be used directly as a
--   parameter to e.g. <a>NP</a>.
data Dict (c :: k -> Constraint) (a :: k)
[Dict] :: c a => Dict c a

-- | A proof that the trivial constraint holds over all type-level lists.
pureAll :: SListI xs => Dict (All Top) xs

-- | A proof that the trivial constraint holds over all type-level lists of
--   lists.
pureAll2 :: All SListI xss => Dict (All2 Top) xss

-- | Lifts a dictionary conversion over a type-level list.
mapAll :: forall c d xs. (forall a. Dict c a -> Dict d a) -> Dict (All c) xs -> Dict (All d) xs

-- | Lifts a dictionary conversion over a type-level list of lists.
mapAll2 :: forall c d xss. (forall a. Dict c a -> Dict d a) -> Dict (All2 c) xss -> Dict (All2 d) xss

-- | If two constraints <tt>c</tt> and <tt>d</tt> hold over a type-level
--   list <tt>xs</tt>, then the combination of both constraints holds over
--   that list.
zipAll :: Dict (All c) xs -> Dict (All d) xs -> Dict (All (c `And` d)) xs

-- | If two constraints <tt>c</tt> and <tt>d</tt> hold over a type-level
--   list of lists <tt>xss</tt>, then the combination of both constraints
--   holds over that list of lists.
zipAll2 :: All SListI xss => Dict (All2 c) xss -> Dict (All2 d) xss -> Dict (All2 (c `And` d)) xss

-- | If we have a constraint <tt>c</tt> that holds over a type-level list
--   <tt>xs</tt>, we can create a product containing proofs that each
--   individual list element satisfies <tt>c</tt>.
unAll_NP :: forall c xs. Dict (All c) xs -> NP (Dict c) xs

-- | If we have a constraint <tt>c</tt> that holds over a type-level list
--   of lists <tt>xss</tt>, we can create a product of products containing
--   proofs that all the inner elements satisfy <tt>c</tt>.
unAll_POP :: forall c xss. Dict (All2 c) xss -> POP (Dict c) xss

-- | If we have a product containing proofs that each element of
--   <tt>xs</tt> satisfies <tt>c</tt>, then <tt><a>All</a> c</tt> holds for
--   <tt>xs</tt>.
all_NP :: NP (Dict c) xs -> Dict (All c) xs

-- | If we have a product of products containing proofs that each inner
--   element of <tt>xss</tt> satisfies <tt>c</tt>, then <tt><a>All2</a>
--   c</tt> holds for <tt>xss</tt>.
all_POP :: SListI xss => POP (Dict c) xss -> Dict (All2 c) xss

-- | The constraint <tt><a>All2</a> c</tt> is convertible to <tt><a>All</a>
--   (<a>All</a> c)</tt>.

-- | <i>Deprecated: 'All2 c' is now a synonym of 'All (All c)'</i>
unAll2 :: Dict (All2 c) xss -> Dict (All (All c)) xss

-- | The constraint <tt><a>All</a> (<a>All</a> c)</tt> is convertible to
--   <tt><a>All2</a> c</tt>.

-- | <i>Deprecated: 'All2 c' is now a synonym of 'All (All c)'</i>
all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss

-- | If we have an explicit dictionary, we can unwrap it and pass a
--   function that makes use of it.
withDict :: Dict c a -> (c a => r) -> r

-- | A structure of dictionaries.
hdicts :: forall h c xs. (AllN h c xs, HPure h) => h (Dict c) xs
instance forall k (c :: k -> GHC.Types.Constraint) (a :: k). GHC.Show.Show (Data.SOP.Dict.Dict c a)


-- | Main module of <tt>sop-core</tt>
module Data.SOP

-- | An n-ary product.
--   
--   The product is parameterized by a type constructor <tt>f</tt> and
--   indexed by a type-level list <tt>xs</tt>. The length of the list
--   determines the number of elements in the product, and if the
--   <tt>i</tt>-th element of the list is of type <tt>x</tt>, then the
--   <tt>i</tt>-th element of the product is of type <tt>f x</tt>.
--   
--   The constructor names are chosen to resemble the names of the list
--   constructors.
--   
--   Two common instantiations of <tt>f</tt> are the identity functor
--   <a>I</a> and the constant functor <a>K</a>. For <a>I</a>, the product
--   becomes a heterogeneous list, where the type-level list describes the
--   types of its components. For <tt><a>K</a> a</tt>, the product becomes
--   a homogeneous list, where the contents of the type-level list are
--   ignored, but its length still specifies the number of elements.
--   
--   In the context of the SOP approach to generic programming, an n-ary
--   product describes the structure of the arguments of a single data
--   constructor.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   I 'x'    :* I True  :* Nil  ::  NP I       '[ Char, Bool ]
--   K 0      :* K 1     :* Nil  ::  NP (K Int) '[ Char, Bool ]
--   Just 'x' :* Nothing :* Nil  ::  NP Maybe   '[ Char, Bool ]
--   </pre>
data NP :: (k -> Type) -> [k] -> Type
[Nil] :: NP f '[]
[:*] :: f x -> NP f xs -> NP f (x ': xs)
infixr 5 :*

-- | An n-ary sum.
--   
--   The sum is parameterized by a type constructor <tt>f</tt> and indexed
--   by a type-level list <tt>xs</tt>. The length of the list determines
--   the number of choices in the sum and if the <tt>i</tt>-th element of
--   the list is of type <tt>x</tt>, then the <tt>i</tt>-th choice of the
--   sum is of type <tt>f x</tt>.
--   
--   The constructor names are chosen to resemble Peano-style natural
--   numbers, i.e., <a>Z</a> is for "zero", and <a>S</a> is for
--   "successor". Chaining <a>S</a> and <a>Z</a> chooses the corresponding
--   component of the sum.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   Z         :: f x -&gt; NS f (x ': xs)
--   S . Z     :: f y -&gt; NS f (x ': y ': xs)
--   S . S . Z :: f z -&gt; NS f (x ': y ': z ': xs)
--   ...
--   </pre>
--   
--   Note that empty sums (indexed by an empty list) have no non-bottom
--   elements.
--   
--   Two common instantiations of <tt>f</tt> are the identity functor
--   <a>I</a> and the constant functor <a>K</a>. For <a>I</a>, the sum
--   becomes a direct generalization of the <a>Either</a> type to
--   arbitrarily many choices. For <tt><a>K</a> a</tt>, the result is a
--   homogeneous choice type, where the contents of the type-level list are
--   ignored, but its length specifies the number of options.
--   
--   In the context of the SOP approach to generic programming, an n-ary
--   sum describes the top-level structure of a datatype, which is a choice
--   between all of its constructors.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   Z (I 'x')      :: NS I       '[ Char, Bool ]
--   S (Z (I True)) :: NS I       '[ Char, Bool ]
--   S (Z (K 1))    :: NS (K Int) '[ Char, Bool ]
--   </pre>
data NS :: (k -> Type) -> [k] -> Type
[Z] :: f x -> NS f (x ': xs)
[S] :: NS f xs -> NS f (x ': xs)

-- | A sum of products.
--   
--   This is a 'newtype' for an <a>NS</a> of an <a>NP</a>. The elements of
--   the (inner) products are applications of the parameter <tt>f</tt>. The
--   type <a>SOP</a> is indexed by the list of lists that determines the
--   sizes of both the (outer) sum and all the (inner) products, as well as
--   the types of all the elements of the inner products.
--   
--   A <tt><a>SOP</a> <a>I</a></tt> reflects the structure of a normal
--   Haskell datatype. The sum structure represents the choice between the
--   different constructors, the product structure represents the arguments
--   of each constructor.
newtype SOP (f :: (k -> Type)) (xss :: [[k]])
SOP :: NS (NP f) xss -> SOP (f :: k -> Type) (xss :: [[k]])

-- | Unwrap a sum of products.
unSOP :: SOP f xss -> NS (NP f) xss

-- | A product of products.
--   
--   This is a 'newtype' for an <a>NP</a> of an <a>NP</a>. The elements of
--   the inner products are applications of the parameter <tt>f</tt>. The
--   type <a>POP</a> is indexed by the list of lists that determines the
--   lengths of both the outer and all the inner products, as well as the
--   types of all the elements of the inner products.
--   
--   A <a>POP</a> is reminiscent of a two-dimensional table (but the inner
--   lists can all be of different length). In the context of the SOP
--   approach to generic programming, a <a>POP</a> is useful to represent
--   information that is available for all arguments of all constructors of
--   a datatype.
newtype POP (f :: (k -> Type)) (xss :: [[k]])
POP :: NP (NP f) xss -> POP (f :: k -> Type) (xss :: [[k]])

-- | Unwrap a product of products.
unPOP :: POP f xss -> NP (NP f) xss

-- | A generalization of <a>pure</a> or <a>return</a> to higher kinds.
class HPure (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>pure</a> directly.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hpure</a>, <a>pure_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a) -&gt; <a>NP</a>  f xs
--   <a>hpure</a>, <a>pure_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a) -&gt; <a>POP</a> f xss
--   </pre>
hpure :: (HPure h, SListIN h xs) => (forall a. f a) -> h f xs

-- | A variant of <a>hpure</a> that allows passing in a constrained
--   argument.
--   
--   Calling <tt><a>hcpure</a> f s</tt> where <tt>s :: h f xs</tt> causes
--   <tt>f</tt> to be applied at all the types that are contained in
--   <tt>xs</tt>. Therefore, the constraint <tt>c</tt> has to be satisfied
--   for all elements of <tt>xs</tt>, which is what <tt><a>AllN</a> h c
--   xs</tt> states.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcpure</a>, <a>cpure_NP</a>  :: (<a>All</a>  c xs ) =&gt; proxy c -&gt; (forall a. c a =&gt; f a) -&gt; <a>NP</a>  f xs
--   <a>hcpure</a>, <a>cpure_POP</a> :: (<a>All2</a> c xss) =&gt; proxy c -&gt; (forall a. c a =&gt; f a) -&gt; <a>POP</a> f xss
--   </pre>
hcpure :: (HPure h, AllN h c xs) => proxy c -> (forall a. c a => f a) -> h f xs

-- | Obtain the head of an n-ary product.
hd :: NP f (x ': xs) -> f x

-- | Obtain the tail of an n-ary product.
tl :: NP f (x ': xs) -> NP f xs

-- | The type of projections from an n-ary product.
--   
--   A projection is a function from the n-ary product to a single element.
type Projection (f :: k -> Type) (xs :: [k]) = K (NP f xs) -.-> f

-- | Compute all projections from an n-ary product.
--   
--   Each element of the resulting product contains one of the projections.
projections :: forall xs f. SListI xs => NP (Projection f xs) xs
shiftProjection :: Projection f xs a -> Projection f (x ': xs) a

-- | Lifted functions.
newtype ( f -.-> g ) a
Fn :: (f a -> g a) -> (-.->) f g a
[apFn] :: (-.->) f g a -> f a -> g a
infixr 1 -.->

-- | Construct a lifted function.
--   
--   Same as <a>Fn</a>. Only available for uniformity with the higher-arity
--   versions.
fn :: (f a -> f' a) -> (f -.-> f') a

-- | Construct a binary lifted function.
fn_2 :: (f a -> f' a -> f'' a) -> (f -.-> (f' -.-> f'')) a

-- | Construct a ternary lifted function.
fn_3 :: (f a -> f' a -> f'' a -> f''' a) -> (f -.-> (f' -.-> (f'' -.-> f'''))) a

-- | Construct a quarternary lifted function.
fn_4 :: (f a -> f' a -> f'' a -> f''' a -> f'''' a) -> (f -.-> (f' -.-> (f'' -.-> (f''' -.-> f'''')))) a

-- | Maps a structure containing sums to the corresponding product
--   structure.
type family Prod (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)

-- | A generalization of <a>&lt;*&gt;</a>.
class (Prod (Prod h) ~ Prod h, HPure (Prod h)) => HAp (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>&lt;*&gt;</a>.
--   
--   For products (<a>NP</a>) as well as products of products (<a>POP</a>),
--   the correspondence is rather direct. We combine a structure containing
--   (lifted) functions and a compatible structure containing corresponding
--   arguments into a compatible structure containing results.
--   
--   The same combinator can also be used to combine a product structure of
--   functions with a sum structure of arguments, which then results in
--   another sum structure of results. The sum structure determines which
--   part of the product structure will be used.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hap</a>, <a>ap_NP</a>  :: <a>NP</a>  (f -.-&gt; g) xs  -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  g xs
--   <a>hap</a>, <a>ap_NS</a>  :: <a>NP</a>  (f -.-&gt; g) xs  -&gt; <a>NS</a>  f xs  -&gt; <a>NS</a>  g xs
--   <a>hap</a>, <a>ap_POP</a> :: <a>POP</a> (f -.-&gt; g) xss -&gt; <a>POP</a> f xss -&gt; <a>POP</a> g xss
--   <a>hap</a>, <a>ap_SOP</a> :: <a>POP</a> (f -.-&gt; g) xss -&gt; <a>SOP</a> f xss -&gt; <a>SOP</a> g xss
--   </pre>
hap :: HAp h => Prod h (f -.-> g) xs -> h f xs -> h g xs

-- | A generalized form of <a>liftA</a>, which in turn is a generalized
--   <a>map</a>.
--   
--   Takes a lifted function and applies it to every element of a structure
--   while preserving its shape.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hliftA</a> f xs = <a>hpure</a> (<a>fn</a> f) ` <a>hap</a> ` xs
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hliftA</a>, <a>liftA_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs
--   <a>hliftA</a>, <a>liftA_NS</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a) -&gt; <a>NS</a>  f xs  -&gt; <a>NS</a>  f' xs
--   <a>hliftA</a>, <a>liftA_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss
--   <a>hliftA</a>, <a>liftA_SOP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a) -&gt; <a>SOP</a> f xss -&gt; <a>SOP</a> f' xss
--   </pre>
hliftA :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs

-- | A generalized form of <a>liftA2</a>, which in turn is a generalized
--   <a>zipWith</a>.
--   
--   Takes a lifted binary function and uses it to combine two structures
--   of equal shape into a single structure.
--   
--   It either takes two product structures to a product structure, or one
--   product and one sum structure to a sum structure.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hliftA2</a> f xs ys = <a>hpure</a> (<a>fn_2</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hliftA2</a>, <a>liftA2_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs  -&gt; <a>NP</a>  f'' xs
--   <a>hliftA2</a>, <a>liftA2_NS</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NS</a>  f' xs  -&gt; <a>NS</a>  f'' xs
--   <a>hliftA2</a>, <a>liftA2_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss -&gt; <a>POP</a> f'' xss
--   <a>hliftA2</a>, <a>liftA2_SOP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a) -&gt; <a>POP</a> f xss -&gt; <a>SOP</a> f' xss -&gt; <a>SOP</a> f'' xss
--   </pre>
hliftA2 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | A generalized form of <a>liftA3</a>, which in turn is a generalized
--   <a>zipWith3</a>.
--   
--   Takes a lifted ternary function and uses it to combine three
--   structures of equal shape into a single structure.
--   
--   It either takes three product structures to a product structure, or
--   two product structures and one sum structure to a sum structure.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hliftA3</a> f xs ys zs = <a>hpure</a> (<a>fn_3</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys ` <a>hap</a> ` zs
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hliftA3</a>, <a>liftA3_NP</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs  -&gt; <a>NP</a>  f'' xs  -&gt; <a>NP</a>  f''' xs
--   <a>hliftA3</a>, <a>liftA3_NS</a>  :: <a>SListI</a>  xs  =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>NP</a>  f xs  -&gt; <a>NP</a>  f' xs  -&gt; <a>NS</a>  f'' xs  -&gt; <a>NS</a>  f''' xs
--   <a>hliftA3</a>, <a>liftA3_POP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss -&gt; <a>POP</a> f'' xss -&gt; <a>POP</a> f''' xs
--   <a>hliftA3</a>, <a>liftA3_SOP</a> :: <a>SListI2</a> xss =&gt; (forall a. f a -&gt; f' a -&gt; f'' a -&gt; f''' a) -&gt; <a>POP</a> f xss -&gt; <a>POP</a> f' xss -&gt; <a>SOP</a> f'' xss -&gt; <a>SOP</a> f''' xs
--   </pre>
hliftA3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Variant of <a>hliftA</a> that takes a constrained function.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA</a> p f xs = <a>hcpure</a> p (<a>fn</a> f) ` <a>hap</a> ` xs
--   </pre>
hcliftA :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs

-- | Variant of <a>hliftA2</a> that takes a constrained function.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA2</a> p f xs ys = <a>hcpure</a> p (<a>fn_2</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys
--   </pre>
hcliftA2 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | Variant of <a>hliftA3</a> that takes a constrained function.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA3</a> p f xs ys zs = <a>hcpure</a> p (<a>fn_3</a> f) ` <a>hap</a> ` xs ` <a>hap</a> ` ys ` <a>hap</a> ` zs
--   </pre>
hcliftA3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Another name for <a>hliftA</a>.
hmap :: (SListIN (Prod h) xs, HAp h) => (forall a. f a -> f' a) -> h f xs -> h f' xs

-- | Another name for <a>hliftA2</a>.
hzipWith :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | Another name for <a>hliftA3</a>.
hzipWith3 :: (SListIN (Prod h) xs, HAp h, HAp (Prod h)) => (forall a. f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | Another name for <a>hcliftA</a>.
hcmap :: (AllN (Prod h) c xs, HAp h) => proxy c -> (forall a. c a => f a -> f' a) -> h f xs -> h f' xs

-- | Another name for <a>hcliftA2</a>.
hczipWith :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a) -> Prod h f xs -> h f' xs -> h f'' xs

-- | Another name for <a>hcliftA3</a>.
hczipWith3 :: (AllN (Prod h) c xs, HAp h, HAp (Prod h)) => proxy c -> (forall a. c a => f a -> f' a -> f'' a -> f''' a) -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs

-- | The type of injections into an n-ary sum.
--   
--   If you expand the type synonyms and newtypes involved, you get
--   
--   <pre>
--   Injection f xs a = (f -.-&gt; K (NS f xs)) a ~= f a -&gt; K (NS f xs) a ~= f a -&gt; NS f xs
--   </pre>
--   
--   If we pick <tt>a</tt> to be an element of <tt>xs</tt>, this indeed
--   corresponds to an injection into the sum.
type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)

-- | Compute all injections into an n-ary sum.
--   
--   Each element of the resulting product contains one of the injections.
injections :: forall xs f. SListI xs => NP (Injection f xs) xs

-- | Shift an injection.
--   
--   Given an injection, return an injection into a sum that is one
--   component larger.

-- | <i>Deprecated: Use <a>shiftInjection</a> instead.</i>
shift :: Injection f xs a -> Injection f (x ': xs) a

-- | Shift an injection.
--   
--   Given an injection, return an injection into a sum that is one
--   component larger.
shiftInjection :: Injection f xs a -> Injection f (x ': xs) a

-- | Maps a structure containing products to the corresponding sum
--   structure.
type family UnProd (h :: (k -> Type) -> (l -> Type)) :: (k -> Type) -> (l -> Type)

-- | A class for applying all injections corresponding to a sum-like
--   structure to a table containing suitable arguments.
class (UnProd (Prod h) ~ h) => HApInjs (h :: (k -> Type) -> (l -> Type))

-- | For a given table (product-like structure), produce a list where each
--   element corresponds to the application of an injection function into
--   the corresponding sum-like structure.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hapInjs</a>, <a>apInjs_NP</a>  :: <a>SListI</a>  xs  =&gt; <a>NP</a>  f xs -&gt; [<a>NS</a>  f xs ]
--   <a>hapInjs</a>, <a>apInjs_SOP</a> :: <a>SListI2</a> xss =&gt; <a>POP</a> f xs -&gt; [<a>SOP</a> f xss]
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hapInjs (I 'x' :* I True :* I 2 :* Nil) :: [NS I '[Char, Bool, Int]]
--   [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; hapInjs (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil)) :: [SOP I '[ '[Char], '[Bool, Int]]]
--   [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]
--   </pre>
--   
--   Unfortunately the type-signatures are required in GHC-7.10 and older.
hapInjs :: (HApInjs h, SListIN h xs) => Prod h f xs -> [h f xs]

-- | Apply injections to a product.
--   
--   Given a product containing all possible choices, produce a list of
--   sums by applying each injection to the appropriate element.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; apInjs_NP (I 'x' :* I True :* I 2 :* Nil)
--   [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]
--   </pre>
apInjs_NP :: SListI xs => NP f xs -> [NS f xs]

-- | Apply injections to a product of product.
--   
--   This operates on the outer product only. Given a product containing
--   all possible choices (that are products), produce a list of sums (of
--   products) by applying each injection to the appropriate element.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; apInjs_POP (POP ((I 'x' :* Nil) :* (I True :* I 2 :* Nil) :* Nil))
--   [SOP (Z (I 'x' :* Nil)),SOP (S (Z (I True :* I 2 :* Nil)))]
--   </pre>
apInjs_POP :: SListI xss => POP f xss -> [SOP f xss]

-- | Extract the payload from a unary sum.
--   
--   For larger sums, this function would be partial, so it is only
--   provided with a rather restrictive type.
--   
--   <i>Example:</i>
--   
--   <pre>
--   &gt;&gt;&gt; unZ (Z (I 'x'))
--   I 'x'
--   </pre>
unZ :: NS f '[x] -> f x

-- | A class for determining which choice in a sum-like structure a value
--   represents.
class HIndex (h :: (k -> Type) -> (l -> Type))

-- | If <tt>h</tt> is a sum-like structure representing a choice between
--   <tt>n</tt> different options, and <tt>x</tt> is a value of type <tt>h
--   f xs</tt>, then <tt><a>hindex</a> x</tt> returns a number between
--   <tt>0</tt> and <tt>n - 1</tt> representing the index of the choice
--   made by <tt>x</tt>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hindex</a>, <a>index_NS</a>  :: <a>NS</a>  f xs -&gt; Int
--   <a>hindex</a>, <a>index_SOP</a> :: <a>SOP</a> f xs -&gt; Int
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hindex (S (S (Z (I False))))
--   2
--   
--   &gt;&gt;&gt; hindex (Z (K ()))
--   0
--   
--   &gt;&gt;&gt; hindex (SOP (S (Z (I True :* I 'x' :* Nil))))
--   1
--   </pre>
hindex :: HIndex h => h f xs -> Int

-- | Lift a constrained function operating on a list-indexed structure to a
--   function on a list-of-list-indexed structure.
--   
--   This is a variant of <a>hcliftA</a>.
--   
--   <i>Specification:</i>
--   
--   <pre>
--   <a>hcliftA'</a> p f xs = <a>hpure</a> (<a>fn_2</a> $ \ <tt>AllDictC</tt> -&gt; f) ` <a>hap</a> ` <tt>allDict_NP</tt> p ` <a>hap</a> ` xs
--   </pre>
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcliftA'</a> :: <a>All2</a> c xss =&gt; proxy c -&gt; (forall xs. <a>All</a> c xs =&gt; f xs -&gt; f' xs) -&gt; <a>NP</a> f xss -&gt; <a>NP</a> f' xss
--   <a>hcliftA'</a> :: <a>All2</a> c xss =&gt; proxy c -&gt; (forall xs. <a>All</a> c xs =&gt; f xs -&gt; f' xs) -&gt; <a>NS</a> f xss -&gt; <a>NS</a> f' xss
--   </pre>

-- | <i>Deprecated: Use <a>hcliftA</a> or <a>hcmap</a> instead.</i>
hcliftA' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs) -> h f xss -> h f' xss

-- | Like <a>hcliftA'</a>, but for binary functions.

-- | <i>Deprecated: Use <a>hcliftA2</a> or <a>hczipWith</a> instead.</i>
hcliftA2' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs) -> Prod h f xss -> h f' xss -> h f'' xss

-- | Like <a>hcliftA'</a>, but for ternary functions.

-- | <i>Deprecated: Use <a>hcliftA3</a> or <a>hczipWith3</a> instead.</i>
hcliftA3' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss

-- | Compare two sums with respect to the choice they are making.
--   
--   A value that chooses the first option is considered smaller than one
--   that chooses the second option.
--   
--   If the choices are different, then either the first (if the first is
--   smaller than the second) or the third (if the first is larger than the
--   second) argument are called. If both choices are equal, then the
--   second argument is called, which has access to the elements contained
--   in the sums.
compare_NS :: forall r f g xs. r -> (forall x. f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r

-- | Constrained version of <a>compare_NS</a>.
ccompare_NS :: forall c proxy r f g xs. All c xs => proxy c -> r -> (forall x. c x => f x -> g x -> r) -> r -> NS f xs -> NS g xs -> r

-- | Compare two sums of products with respect to the choice in the sum
--   they are making.
--   
--   Only the sum structure is used for comparison. This is a small wrapper
--   around <a>ccompare_NS</a> for a common special case.
compare_SOP :: forall r f g xss. r -> (forall xs. NP f xs -> NP g xs -> r) -> r -> SOP f xss -> SOP g xss -> r

-- | Constrained version of <a>compare_SOP</a>.
ccompare_SOP :: forall c proxy r f g xss. All2 c xss => proxy c -> r -> (forall xs. All c xs => NP f xs -> NP g xs -> r) -> r -> SOP f xss -> SOP g xss -> r

-- | Maps products to lists, and sums to identities.
type family CollapseTo (h :: (k -> Type) -> (l -> Type)) (x :: Type) :: Type

-- | A class for collapsing a heterogeneous structure into a homogeneous
--   one.
class HCollapse (h :: (k -> Type) -> (l -> Type))

-- | Collapse a heterogeneous structure with homogeneous elements into a
--   homogeneous structure.
--   
--   If a heterogeneous structure is instantiated to the constant functor
--   <a>K</a>, then it is in fact homogeneous. This function maps such a
--   value to a simpler Haskell datatype reflecting that. An <tt><a>NS</a>
--   (<a>K</a> a)</tt> contains a single <tt>a</tt>, and an <tt><a>NP</a>
--   (<a>K</a> a)</tt> contains a list of <tt>a</tt>s.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcollapse</a>, <a>collapse_NP</a>  :: <a>NP</a>  (<a>K</a> a) xs  -&gt;  [a]
--   <a>hcollapse</a>, <a>collapse_NS</a>  :: <a>NS</a>  (<a>K</a> a) xs  -&gt;   a
--   <a>hcollapse</a>, <a>collapse_POP</a> :: <a>POP</a> (<a>K</a> a) xss -&gt; [[a]]
--   <a>hcollapse</a>, <a>collapse_SOP</a> :: <a>SOP</a> (<a>K</a> a) xss -&gt;  [a]
--   </pre>
hcollapse :: (HCollapse h, SListIN h xs) => h (K a) xs -> CollapseTo h a

-- | A generalization of <a>traverse_</a> or <a>foldMap</a>.
class HTraverse_ (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>traverse_</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hctraverse_</a>, <a>ctraverse__NP</a>  :: (<a>All</a>  c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>NP</a>  f xs  -&gt; g ()
--   <a>hctraverse_</a>, <a>ctraverse__NS</a>  :: (<a>All2</a> c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>NS</a>  f xs  -&gt; g ()
--   <a>hctraverse_</a>, <a>ctraverse__POP</a> :: (<a>All</a>  c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>POP</a> f xss -&gt; g ()
--   <a>hctraverse_</a>, <a>ctraverse__SOP</a> :: (<a>All2</a> c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g ()) -&gt; <a>SOP</a> f xss -&gt; g ()
--   </pre>
hctraverse_ :: (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g ()) -> h f xs -> g ()

-- | Unconstrained version of <a>hctraverse_</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <tt>traverse_</tt>, <a>traverse__NP</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>NP</a>  f xs  -&gt; g ()
--   <tt>traverse_</tt>, <a>traverse__NS</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>NS</a>  f xs  -&gt; g ()
--   <tt>traverse_</tt>, <a>traverse__POP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>POP</a> f xss -&gt; g ()
--   <tt>traverse_</tt>, <a>traverse__SOP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> g) =&gt; (forall a. f a -&gt; g ()) -&gt; <a>SOP</a> f xss -&gt; g ()
--   </pre>
htraverse_ :: (HTraverse_ h, SListIN h xs, Applicative g) => (forall a. f a -> g ()) -> h f xs -> g ()

-- | Special case of <a>hctraverse_</a>.
hcfoldMap :: (HTraverse_ h, AllN h c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> h f xs -> m

-- | Flipped version of <a>hctraverse_</a>.
hcfor_ :: (HTraverse_ h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g ()) -> g ()

-- | A generalization of <a>sequenceA</a>.
class HAp h => HSequence (h :: (k -> Type) -> (l -> Type))

-- | Corresponds to <a>sequenceA</a>.
--   
--   Lifts an applicative functor out of a structure.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hsequence'</a>, <a>sequence'_NP</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> f) =&gt; <a>NP</a>  (f <a>:.:</a> g) xs  -&gt; f (<a>NP</a>  g xs )
--   <a>hsequence'</a>, <a>sequence'_NS</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> f) =&gt; <a>NS</a>  (f <a>:.:</a> g) xs  -&gt; f (<a>NS</a>  g xs )
--   <a>hsequence'</a>, <a>sequence'_POP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> f) =&gt; <a>POP</a> (f <a>:.:</a> g) xss -&gt; f (<a>POP</a> g xss)
--   <a>hsequence'</a>, <a>sequence'_SOP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> f) =&gt; <a>SOP</a> (f <a>:.:</a> g) xss -&gt; f (<a>SOP</a> g xss)
--   </pre>
hsequence' :: (HSequence h, SListIN h xs, Applicative f) => h (f :.: g) xs -> f (h g xs)

-- | Corresponds to <a>traverse</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hctraverse'</a>, <a>ctraverse'_NP</a>  :: (<a>All</a>  c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NP</a>  f xs  -&gt; g (<a>NP</a>  f' xs )
--   <a>hctraverse'</a>, <a>ctraverse'_NS</a>  :: (<a>All2</a> c xs , <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NS</a>  f xs  -&gt; g (<a>NS</a>  f' xs )
--   <a>hctraverse'</a>, <a>ctraverse'_POP</a> :: (<a>All</a>  c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>POP</a> f xss -&gt; g (<a>POP</a> f' xss)
--   <a>hctraverse'</a>, <a>ctraverse'_SOP</a> :: (<a>All2</a> c xss, <a>Applicative</a> g) =&gt; proxy c -&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>SOP</a> f xss -&gt; g (<a>SOP</a> f' xss)
--   </pre>
hctraverse' :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> h f xs -> g (h f' xs)

-- | Unconstrained variant of <a>hctraverse'</a>.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>htraverse'</a>, <a>traverse'_NP</a>  :: (<a>SListI</a>  xs , <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NP</a>  f xs  -&gt; g (<a>NP</a>  f' xs )
--   <a>htraverse'</a>, <a>traverse'_NS</a>  :: (<a>SListI2</a> xs , <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>NS</a>  f xs  -&gt; g (<a>NS</a>  f' xs )
--   <a>htraverse'</a>, <a>traverse'_POP</a> :: (<a>SListI</a>  xss, <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>POP</a> f xss -&gt; g (<a>POP</a> f' xss)
--   <a>htraverse'</a>, <a>traverse'_SOP</a> :: (<a>SListI2</a> xss, <a>Applicative</a> g) =&gt; (forall a. c a =&gt; f a -&gt; g (f' a)) -&gt; <a>SOP</a> f xss -&gt; g (<a>SOP</a> f' xss)
--   </pre>
htraverse' :: (HSequence h, SListIN h xs, Applicative g) => (forall a. f a -> g (f' a)) -> h f xs -> g (h f' xs)

-- | Special case of <a>hsequence'</a> where <tt>g = <a>I</a></tt>.
hsequence :: (SListIN h xs, SListIN (Prod h) xs, HSequence h) => Applicative f => h f xs -> f (h I xs)

-- | Special case of <a>hsequence'</a> where <tt>g = <a>K</a> a</tt>.
hsequenceK :: (SListIN h xs, SListIN (Prod h) xs, Applicative f, HSequence h) => h (K (f a)) xs -> f (h (K a) xs)

-- | Special case of <a>hctraverse'</a> where <tt>f' = <a>I</a></tt>.
hctraverse :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> h f xs -> g (h I xs)

-- | Flipped version of <a>hctraverse</a>.
hcfor :: (HSequence h, AllN h c xs, Applicative g) => proxy c -> h f xs -> (forall a. c a => f a -> g a) -> g (h I xs)

-- | A class for expanding sum structures into corresponding product
--   structures, filling in the slots not targeted by the sum with default
--   values.
class HExpand (h :: (k -> Type) -> (l -> Type))

-- | Expand a given sum structure into a corresponding product structure by
--   placing the value contained in the sum into the corresponding position
--   in the product, and using the given default value for all other
--   positions.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hexpand</a>, <a>expand_NS</a>  :: <a>SListI</a> xs   =&gt; (forall x . f x) -&gt; <a>NS</a>  f xs  -&gt; <a>NP</a>  f xs
--   <a>hexpand</a>, <a>expand_SOP</a> :: <a>SListI2</a> xss =&gt; (forall x . f x) -&gt; <a>SOP</a> f xss -&gt; <a>POP</a> f xss
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hexpand Nothing (S (Z (Just 3))) :: NP Maybe '[Char, Int, Bool]
--   Nothing :* Just 3 :* Nothing :* Nil
--   
--   &gt;&gt;&gt; hexpand [] (SOP (S (Z ([1,2] :* "xyz" :* Nil)))) :: POP [] '[ '[Bool], '[Int, Char] ]
--   POP (([] :* Nil) :* ([1,2] :* "xyz" :* Nil) :* Nil)
--   </pre>
hexpand :: (HExpand h, SListIN (Prod h) xs) => (forall x. f x) -> h f xs -> Prod h f xs

-- | Variant of <a>hexpand</a> that allows passing a constrained default.
--   
--   <i>Instances:</i>
--   
--   <pre>
--   <a>hcexpand</a>, <a>cexpand_NS</a>  :: <a>All</a>  c xs  =&gt; proxy c -&gt; (forall x . c x =&gt; f x) -&gt; <a>NS</a>  f xs  -&gt; <a>NP</a>  f xs
--   <a>hcexpand</a>, <a>cexpand_SOP</a> :: <a>All2</a> c xss =&gt; proxy c -&gt; (forall x . c x =&gt; f x) -&gt; <a>SOP</a> f xss -&gt; <a>POP</a> f xss
--   </pre>
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hcexpand (Proxy :: Proxy Bounded) (I minBound) (S (Z (I 20))) :: NP I '[Bool, Int, Ordering]
--   I False :* I 20 :* I LT :* Nil
--   
--   &gt;&gt;&gt; hcexpand (Proxy :: Proxy Num) (I 0) (SOP (S (Z (I 1 :* I 2 :* Nil)))) :: POP I '[ '[Double], '[Int, Int] ]
--   POP ((I 0.0 :* Nil) :* (I 1 :* I 2 :* Nil) :* Nil)
--   </pre>
hcexpand :: (HExpand h, AllN (Prod h) c xs) => proxy c -> (forall x. c x => f x) -> h f xs -> Prod h f xs

-- | A class for transforming structures into related structures with a
--   different index list, as long as the index lists have the same shape
--   and the elements and interpretation functions are suitably related.
class (Same h1 ~ h2, Same h2 ~ h1) => HTrans (h1 :: (k1 -> Type) -> (l1 -> Type)) (h2 :: (k2 -> Type) -> (l2 -> Type))

-- | Transform a structure into a related structure given a conversion
--   function for the elements.
htrans :: (HTrans h1 h2, AllZipN (Prod h1) c xs ys) => proxy c -> (forall x y. c x y => f x -> g y) -> h1 f xs -> h2 g ys

-- | Safely coerce a structure into a representationally equal structure.
--   
--   This is a special case of <a>htrans</a>, but can be implemented more
--   efficiently; for example in terms of <a>unsafeCoerce</a>.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; hcoerce (I (Just LT) :* I (Just 'x') :* I (Just True) :* Nil) :: NP Maybe '[Ordering, Char, Bool]
--   Just LT :* Just 'x' :* Just True :* Nil
--   
--   &gt;&gt;&gt; hcoerce (SOP (Z (K True :* K False :* Nil))) :: SOP I '[ '[Bool, Bool], '[Bool] ]
--   SOP (Z (I True :* I False :* Nil))
--   </pre>
hcoerce :: (HTrans h1 h2, AllZipN (Prod h1) (LiftedCoercible f g) xs ys) => h1 f xs -> h2 g ys

-- | Specialization of <a>hcoerce</a>.
hfromI :: (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) => h1 I xs -> h2 f ys

-- | Specialization of <a>hcoerce</a>.
htoI :: (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) => h1 f xs -> h2 I ys

-- | Construct a homogeneous n-ary product from a normal Haskell list.
--   
--   Returns <a>Nothing</a> if the length of the list does not exactly
--   match the expected size of the product.
fromList :: SListI xs => [a] -> Maybe (NP (K a) xs)

-- | The constant type functor.
--   
--   Like <a>Constant</a>, but kind-polymorphic in its second argument and
--   with a shorter name.
newtype K (a :: Type) (b :: k)
K :: a -> K (a :: Type) (b :: k)

-- | Extract the contents of a <a>K</a> value.
unK :: K a b -> a

-- | The identity type functor.
--   
--   Like <a>Identity</a>, but with a shorter name.
newtype I (a :: Type)
I :: a -> I (a :: Type)

-- | Extract the contents of an <a>I</a> value.
unI :: I a -> a

-- | Composition of functors.
--   
--   Like <a>Compose</a>, but kind-polymorphic and with a shorter name.
newtype (:.:) (f :: l -> Type) (g :: k -> l) (p :: k)
Comp :: f (g p) -> (:.:) (f :: l -> Type) (g :: k -> l) (p :: k)
infixr 7 :.:

-- | Extract the contents of a <a>Comp</a> value.
unComp :: (f :.: g) p -> f (g p)

-- | Lift the given function.
mapII :: (a -> b) -> I a -> I b

-- | Lift the given function.
mapIK :: (a -> b) -> I a -> K b c

-- | Lift the given function.
mapKI :: (a -> b) -> K a c -> I b

-- | Lift the given function.
mapKK :: (a -> b) -> K a c -> K b d

-- | Lift the given function.
mapIII :: (a -> b -> c) -> I a -> I b -> I c

-- | Lift the given function.
mapIIK :: (a -> b -> c) -> I a -> I b -> K c d

-- | Lift the given function.
mapIKI :: (a -> b -> c) -> I a -> K b d -> I c

-- | Lift the given function.
mapIKK :: (a -> b -> c) -> I a -> K b d -> K c e

-- | Lift the given function.
mapKII :: (a -> b -> c) -> K a d -> I b -> I c

-- | Lift the given function.
mapKIK :: (a -> b -> c) -> K a d -> I b -> K c e

-- | Lift the given function.
mapKKI :: (a -> b -> c) -> K a d -> K b e -> I c

-- | Lift the given function.
mapKKK :: (a -> b -> c) -> K a d -> K b e -> K c f

-- | Require a constraint for every element of a list.
--   
--   If you have a datatype that is indexed over a type-level list, then
--   you can use <a>All</a> to indicate that all elements of that
--   type-level list must satisfy a given constraint.
--   
--   <i>Example:</i> The constraint
--   
--   <pre>
--   All Eq '[ Int, Bool, Char ]
--   </pre>
--   
--   is equivalent to the constraint
--   
--   <pre>
--   (Eq Int, Eq Bool, Eq Char)
--   </pre>
--   
--   <i>Example:</i> A type signature such as
--   
--   <pre>
--   f :: All Eq xs =&gt; NP I xs -&gt; ...
--   </pre>
--   
--   means that <tt>f</tt> can assume that all elements of the n-ary
--   product satisfy <a>Eq</a>.
--   
--   Note on superclasses: ghc cannot deduce superclasses from <a>All</a>
--   constraints. You might expect the following to compile
--   
--   <pre>
--   class (Eq a) =&gt; MyClass a
--   
--   foo :: (All Eq xs) =&gt; NP f xs -&gt; z
--   foo = [..]
--   
--   bar :: (All MyClass xs) =&gt; NP f xs -&gt; x
--   bar = foo
--   </pre>
--   
--   but it will fail with an error saying that it was unable to deduce the
--   class constraint <tt><a>AllF</a> <a>Eq</a> xs</tt> (or similar) in the
--   definition of <tt>bar</tt>. In cases like this you can use <a>Dict</a>
--   from <a>Data.SOP.Dict</a> to prove conversions between constraints.
--   See <a>this answer on SO for more details</a>.
class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k])

-- | Require a constraint for every element of a list of lists.
--   
--   If you have a datatype that is indexed over a type-level list of
--   lists, then you can use <a>All2</a> to indicate that all elements of
--   the inner lists must satisfy a given constraint.
--   
--   <i>Example:</i> The constraint
--   
--   <pre>
--   All2 Eq '[ '[ Int ], '[ Bool, Char ] ]
--   </pre>
--   
--   is equivalent to the constraint
--   
--   <pre>
--   (Eq Int, Eq Bool, Eq Char)
--   </pre>
--   
--   <i>Example:</i> A type signature such as
--   
--   <pre>
--   f :: All2 Eq xss =&gt; SOP I xs -&gt; ...
--   </pre>
--   
--   means that <tt>f</tt> can assume that all elements of the sum of
--   product satisfy <a>Eq</a>.
--   
--   Since 0.4.0.0, this is merely a synonym for 'All (All c)'.
type All2 c = All (All c)

-- | Constrained paramorphism for a type-level list.
--   
--   The advantage of writing functions in terms of <a>cpara_SList</a> is
--   that they are then typically not recursive, and can be unfolded
--   statically if the type-level list is statically known.
cpara_SList :: All c xs => proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r ys -> r (y ': ys)) -> r xs

-- | Constrained case distinction on a type-level list.
ccase_SList :: All c xs => proxy c -> r '[] -> (forall y ys. (c y, All c ys) => r (y ': ys)) -> r xs

-- | Require a constraint pointwise for every pair of elements from two
--   lists.
--   
--   <i>Example:</i> The constraint
--   
--   <pre>
--   AllZip (~) '[ Int, Bool, Char ] '[ a, b, c ]
--   </pre>
--   
--   is equivalent to the constraint
--   
--   <pre>
--   (Int ~ a, Bool ~ b, Char ~ c)
--   </pre>
class (SListI xs, SListI ys, SameShapeAs xs ys, SameShapeAs ys xs, AllZipF c xs ys) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])

-- | Require a constraint pointwise for every pair of elements from two
--   lists of lists.
class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss

-- | A generalization of <a>All</a> and <a>All2</a>.
--   
--   The family <a>AllN</a> expands to <a>All</a> or <a>All2</a> depending
--   on whether the argument is indexed by a list or a list of lists.
type family AllN (h :: (k -> Type) -> (l -> Type)) (c :: k -> Constraint) :: l -> Constraint

-- | A generalization of <a>AllZip</a> and <a>AllZip2</a>.
--   
--   The family <a>AllZipN</a> expands to <a>AllZip</a> or <a>AllZip2</a>
--   depending on whther the argument is indexed by a list or a list of
--   lists.
type family AllZipN (h :: (k -> Type) -> (l -> Type)) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint

-- | Composition of constraints.
--   
--   Note that the result of the composition must be a constraint, and
--   therefore, in <tt><a>Compose</a> f g</tt>, the kind of <tt>f</tt> is
--   <tt>k -&gt; <a>Constraint</a></tt>. The kind of <tt>g</tt>, however,
--   is <tt>l -&gt; k</tt> and can thus be a normal type constructor.
--   
--   A typical use case is in connection with <a>All</a> on an <a>NP</a> or
--   an <a>NS</a>. For example, in order to denote that all elements on an
--   <tt><a>NP</a> f xs</tt> satisfy <a>Show</a>, we can say <tt><a>All</a>
--   (<a>Compose</a> <a>Show</a> f) xs</tt>.
class (f (g x)) => ( f `Compose` g ) x
infixr 9 `Compose`

-- | Pairing of constraints.
class (f x, g x) => ( f `And` g ) x
infixl 7 `And`

-- | A constraint that can always be satisfied.
class Top x

-- | The constraint <tt><a>LiftedCoercible</a> f g x y</tt> is equivalent
--   to <tt><a>Coercible</a> (f x) (g y)</tt>.
class Coercible (f x) (g y) => LiftedCoercible f g x y

-- | Type family that forces a type-level list to be of the same shape as
--   the given type-level list.
--   
--   Since 0.5.0.0, this only tests the top-level structure of the list,
--   and is intended to be used in conjunction with a separate construct
--   (such as the <a>AllZip</a>, <a>AllZipF</a> combination to tie the
--   recursive knot). The reason is that making <a>SameShapeAs</a> directly
--   recursive leads to quadratic compile times.
--   
--   The main use of this constraint is to help type inference to learn
--   something about otherwise unknown type-level lists.
type family SameShapeAs (xs :: [a]) (ys :: [b]) :: Constraint

-- | Explicit singleton list.
--   
--   A singleton list can be used to reveal the structure of a type-level
--   list argument that the function is quantified over. For every
--   type-level list <tt>xs</tt>, there is one non-bottom value of type
--   <tt><a>SList</a> xs</tt>.
--   
--   Note that these singleton lists are polymorphic in the list elements;
--   we do not require a singleton representation for them.
data SList :: [k] -> Type
[SNil] :: SList '[]
[SCons] :: SListI xs => SList (x ': xs)

-- | Implicit singleton list.
--   
--   A singleton list can be used to reveal the structure of a type-level
--   list argument that the function is quantified over.
--   
--   Since 0.4.0.0, this is now defined in terms of <a>All</a>. A singleton
--   list provides a witness for a type-level list where the elements need
--   not satisfy any additional constraints.
type SListI = All Top

-- | Require a singleton for every inner list in a list of lists.
type SListI2 = All SListI

-- | Get hold of an explicit singleton (that one can then pattern match on)
--   for a type-level list
sList :: SListI xs => SList xs

-- | Paramorphism for a type-level list.
para_SList :: SListI xs => r '[] -> (forall y ys. SListI ys => r ys -> r (y ': ys)) -> r xs

-- | Case distinction on a type-level list.
case_SList :: SListI xs => r '[] -> (forall y ys. SListI ys => r (y ': ys)) -> r xs

-- | Occasionally it is useful to have an explicit, term-level,
--   representation of type-level lists (esp because of
--   <a>https://ghc.haskell.org/trac/ghc/ticket/9108</a> )
data Shape :: [k] -> Type
[ShapeNil] :: Shape '[]
[ShapeCons] :: SListI xs => Shape xs -> Shape (x ': xs)

-- | The shape of a type-level list.
shape :: forall k (xs :: [k]). SListI xs => Shape xs

-- | The length of a type-level list.
lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int
data () => Proxy (t :: k)
Proxy :: Proxy (t :: k)
