    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE EmptyCase #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# OPTIONS_GHC -fno-warn-deprecations #-}
    -- | n-ary sums (and sums of products)
    module Data.SOP.NS
      ( -- * Datatypes
        NS(..)
      , SOP(..)
      , unSOP
        -- * Constructing sums
      , Injection
      , injections
      , shift
      , shiftInjection
      , apInjs_NP
      , apInjs'_NP
      , apInjs_POP
      , apInjs'_POP
        -- * Destructing sums
      , unZ
      , index_NS
      , index_SOP
      , Ejection
      , ejections
      , shiftEjection
        -- * Application
      , ap_NS
      , ap_SOP
        -- * Lifting / mapping
      , liftA_NS
      , liftA_SOP
      , liftA2_NS
      , liftA2_SOP
      , cliftA_NS
      , cliftA_SOP
      , cliftA2_NS
      , cliftA2_SOP
      , map_NS
      , map_SOP
      , cmap_NS
      , cmap_SOP
        -- * Dealing with @'All' c@
      , cliftA2'_NS
        -- * Comparison
      , compare_NS
      , ccompare_NS
      , compare_SOP
      , ccompare_SOP
        -- * Collapsing
      , collapse_NS
      , collapse_SOP
        -- * Folding and sequencing
      , ctraverse__NS
      , ctraverse__SOP
      , traverse__NS
      , traverse__SOP
      , cfoldMap_NS
      , cfoldMap_SOP
      , sequence'_NS
      , sequence'_SOP
      , sequence_NS
      , sequence_SOP
      , ctraverse'_NS
      , ctraverse'_SOP
      , traverse'_NS
      , traverse'_SOP
      , ctraverse_NS
      , ctraverse_SOP
        -- * Catamorphism and anamorphism
      , cata_NS
      , ccata_NS
      , ana_NS
      , cana_NS
        -- * Expanding sums to products
      , expand_NS
      , cexpand_NS
      , expand_SOP
      , cexpand_SOP
        -- * Transformation of index lists and coercions
      , trans_NS
      , trans_SOP
      , coerce_NS
      , coerce_SOP
      , fromI_NS
      , fromI_SOP
      , toI_NS
      , toI_SOP
      ) where

    import Data.Coerce
    import Data.Kind (Type)
    import Data.Proxy (Proxy (..))
    import Unsafe.Coerce

    import Control.DeepSeq (NFData(..))

    import Data.SOP.BasicFunctors
    import Data.SOP.Classes
    import Data.SOP.Constraint
    import Data.SOP.NP
    import Data.SOP.Sing

    -- * Datatypes

    -- | An n-ary sum.
    --
    -- The sum is parameterized by a type constructor @f@ and
    -- indexed by a type-level list @xs@. The length of the list
    -- determines the number of choices in the sum and if the
    -- @i@-th element of the list is of type @x@, then the @i@-th
    -- choice of the sum is of type @f x@.
    --
    -- The constructor names are chosen to resemble Peano-style
    -- natural numbers, i.e., 'Z' is for "zero", and 'S' is for
    -- "successor". Chaining 'S' and 'Z' chooses the corresponding
    -- component of the sum.
    --
    -- /Examples:/
    --
    -- > Z         :: f x -> NS f (x ': xs)
    -- > S . Z     :: f y -> NS f (x ': y ': xs)
    -- > S . S . Z :: f z -> NS f (x ': y ': z ': xs)
    -- > ...
    --
    -- Note that empty sums (indexed by an empty list) have no
    -- non-bottom elements.
    --
    -- Two common instantiations of @f@ are the identity functor 'I'
    -- and the constant functor 'K'. For 'I', the sum becomes a
    -- direct generalization of the 'Either' type to arbitrarily many
    -- choices. For @'K' a@, 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.
    --
    -- /Examples:/
    --
    -- > Z (I 'x')      :: NS I       '[ Char, Bool ]
    -- > S (Z (I True)) :: NS I       '[ Char, Bool ]
    -- > S (Z (K 1))    :: NS (K Int) '[ Char, Bool ]
    --
    data NS :: (k -> Type) -> [k] -> Type where
      Z :: f x -> NS f (x ': xs)
      S :: NS f xs -> NS f (x ': xs)

    deriving instance All (Show `Compose` f) xs => Show (NS f xs)
    deriving instance All (Eq   `Compose` f) xs => Eq   (NS f xs)
    deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)

    -- | @since 0.2.5.0
    instance All (NFData `Compose` f) xs => NFData (NS f xs) where
        rnf :: NS f xs -> ()
    rnf (Z f x
    x)  = f x -> ()
    forall a. NFData a => a -> ()
    rnf f x
    x
        rnf (S NS f xs
    xs) = NS f xs -> ()
    forall a. NFData a => a -> ()
    rnf NS f xs
    xs

    -- | 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 'Injection'.
    --
    -- @since 0.5.0.0
    --
    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.
    --
    -- @since 0.5.0.0
    --
    ejections :: forall xs f . SListI xs => NP (Ejection f xs) xs
    ejections :: forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Ejection f xs) xs
    ejections = case SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList :: SList xs of
      SList xs
    SNil  -> NP (Ejection f xs) xs
    NP (Ejection f xs) '[]
    forall {k} (a :: k -> *). NP a '[]
    Nil
      SList xs
    SCons ->
        (K (NS f xs) x -> (:.:) Maybe f x)
    -> (-.->) (K (NS f xs)) (Maybe :.: f) x
    forall {k} (f :: k -> *) (a :: k) (f' :: k -> *).
    (f a -> f' a) -> (-.->) f f' a
    fn (Maybe (f x) -> (:.:) Maybe f x
    forall l k (f :: l -> *) (g :: k -> l) (p :: k).
    f (g p) -> (:.:) f g p
    Comp (Maybe (f x) -> (:.:) Maybe f x)
    -> (K (NS f xs) x -> Maybe (f x))
    -> K (NS f xs) x
    -> (:.:) Maybe f x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\NS f xs
    ns -> case NS f xs
    ns of Z f x
    fx -> f x -> Maybe (f x)
    forall a. a -> Maybe a
    Just f x
    f x
    fx; S NS f xs
    _ -> Maybe (f x)
    forall a. Maybe a
    Nothing) (NS f xs -> Maybe (f x))
    -> (K (NS f xs) x -> NS f xs) -> K (NS f xs) x -> Maybe (f x)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K (NS f xs) x -> NS f xs
    forall {k} a (b :: k). K a b -> a
    unK) (-.->) (K (NS f xs)) (Maybe :.: f) x
    -> NP (Ejection f xs) xs -> NP (Ejection f xs) (x : xs)
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
    a x -> NP a xs -> NP a (x : xs)
    :*
        (forall (a :: k). Ejection f xs a -> Ejection f xs a)
    -> NP (Ejection f xs) xs -> NP (Ejection f xs) xs
    forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
    liftA_NP (-.->) (K (NS f xs)) (Maybe :.: f) a
    -> (-.->) (K (NS f xs)) (Maybe :.: f) a
    (-.->) (K (NS f xs)) (Maybe :.: f) a -> Ejection f (x : xs) a
    forall (a :: k). Ejection f xs a -> Ejection f xs a
    forall {a} (f :: a -> *) (x :: a) (xs :: [a]) (a :: a).
    Ejection f xs a -> Ejection f (x : xs) a
    shiftEjection NP (Ejection f xs) xs
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Ejection f xs) xs
    ejections

    -- |
    -- @since 0.5.0.0
    --
    shiftEjection :: forall f x xs a . Ejection f xs a -> Ejection f (x ': xs) a
    shiftEjection :: forall {a} (f :: a -> *) (x :: a) (xs :: [a]) (a :: a).
    Ejection f xs a -> Ejection f (x : xs) a
    shiftEjection (Fn K (NS f xs) a -> (:.:) Maybe f a
    f) = (K (NS f (x : xs)) a -> (:.:) Maybe f a)
    -> (-.->) (K (NS f (x : xs))) (Maybe :.: f) a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    (f a -> g a) -> (-.->) f g a
    Fn ((K (NS f (x : xs)) a -> (:.:) Maybe f a)
     -> (-.->) (K (NS f (x : xs))) (Maybe :.: f) a)
    -> (K (NS f (x : xs)) a -> (:.:) Maybe f a)
    -> (-.->) (K (NS f (x : xs))) (Maybe :.: f) a
    forall a b. (a -> b) -> a -> b
    $ (\NS f (x : xs)
    ns -> case NS f (x : xs)
    ns of Z f x
    _ -> Maybe (f a) -> (:.:) Maybe f a
    forall l k (f :: l -> *) (g :: k -> l) (p :: k).
    f (g p) -> (:.:) f g p
    Comp Maybe (f a)
    forall a. Maybe a
    Nothing; S NS f xs
    s -> K (NS f xs) a -> (:.:) Maybe f a
    f (NS f xs -> K (NS f xs) a
    forall k a (b :: k). a -> K a b
    K NS f xs
    NS f xs
    s)) (NS f (x : xs) -> (:.:) Maybe f a)
    -> (K (NS f (x : xs)) a -> NS f (x : xs))
    -> K (NS f (x : xs)) a
    -> (:.:) Maybe f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K (NS f (x : xs)) a -> NS f (x : xs)
    forall {k} a (b :: k). K a b -> a
    unK

    -- | 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.
    --
    -- /Example:/
    --
    -- >>> unZ (Z (I 'x'))
    -- I 'x'
    --
    -- @since 0.2.2.0
    --
    unZ :: NS f '[x] -> f x
    unZ :: forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
    unZ (Z f x
    x) = f x
    f x
    x
    unZ (S NS f xs
    x) = case NS f xs
    x of {}

    -- | 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.
    --
    -- /Examples:/
    --
    -- >>> index_NS (S (S (Z (I False))))
    -- 2
    -- >>> index_NS (Z (K ()))
    -- 0
    --
    -- @since 0.2.4.0
    --
    index_NS :: forall f xs . NS f xs -> Int
    index_NS :: forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Int
    index_NS = Int -> NS f xs -> Int
    forall (ys :: [k]). Int -> NS f ys -> Int
    go Int
    0
      where
        go :: forall ys . Int -> NS f ys -> Int
        go :: forall (ys :: [k]). Int -> NS f ys -> Int
    go !Int
    acc (Z f x
    _) = Int
    acc
        go !Int
    acc (S NS f xs
    x) = Int -> NS f xs -> Int
    forall (ys :: [k]). Int -> NS f ys -> Int
    go (Int
    acc Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) NS f xs
    x

    instance HIndex NS where
      hindex :: forall (f :: k -> *) (xs :: [k]). NS f xs -> Int
    hindex = NS f xs -> Int
    forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Int
    index_NS

    -- | A sum of products.
    --
    -- This is a 'newtype' for an 'NS' of an 'NP'. The elements of the
    -- (inner) products are applications of the parameter @f@. The type
    -- 'SOP' 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 @'SOP' 'I'@ 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)

    deriving instance (Show (NS (NP f) xss)) => Show (SOP f xss)
    deriving instance (Eq   (NS (NP f) xss)) => Eq   (SOP f xss)
    deriving instance (Ord  (NS (NP f) xss)) => Ord  (SOP f xss)

    -- | @since 0.2.5.0
    instance (NFData (NS (NP f) xss)) => NFData (SOP f xss) where
        rnf :: SOP f xss -> ()
    rnf (SOP NS (NP f) xss
    xss) = NS (NP f) xss -> ()
    forall a. NFData a => a -> ()
    rnf NS (NP f) xss
    xss

    -- | Unwrap a sum of products.
    unSOP :: SOP f xss -> NS (NP f) xss
    unSOP :: forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP (SOP NS (NP f) xss
    xss) = NS (NP f) xss
    xss

    type instance AllN NS  c = All  c
    type instance AllN SOP c = All2 c

    -- | 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.
    --
    -- /Specification:/
    --
    -- @
    -- 'index_SOP' = 'index_NS' '.' 'unSOP'
    -- @
    --
    -- /Example:/
    --
    -- >>> index_SOP (SOP (S (Z (I True :* I 'x' :* Nil))))
    -- 1
    --
    -- @since 0.2.4.0
    --
    index_SOP :: SOP f xs -> Int
    index_SOP :: forall {k} (f :: k -> *) (xs :: [[k]]). SOP f xs -> Int
    index_SOP = NS (NP f) xs -> Int
    forall {k} (f :: k -> *) (xs :: [k]). NS f xs -> Int
    index_NS (NS (NP f) xs -> Int)
    -> (SOP f xs -> NS (NP f) xs) -> SOP f xs -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP f xs -> NS (NP f) xs
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    instance HIndex SOP where
      hindex :: forall (f :: k -> *) (xs :: [[k]]). SOP f xs -> Int
    hindex = SOP f xs -> Int
    forall {k} (f :: k -> *) (xs :: [[k]]). SOP f xs -> Int
    index_SOP

    -- * Constructing sums

    -- | The type of injections into an n-ary sum.
    --
    -- If you expand the type synonyms and newtypes involved, you get
    --
    -- > Injection f xs a = (f -.-> K (NS f xs)) a ~= f a -> K (NS f xs) a ~= f a -> NS f xs
    --
    -- If we pick @a@ to be an element of @xs@, 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
    injections :: forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Injection f xs) xs
    injections = case SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList :: SList xs of
      SList xs
    SNil   -> NP (Injection f xs) xs
    NP (Injection f xs) '[]
    forall {k} (a :: k -> *). NP a '[]
    Nil
      SList xs
    SCons  -> (f x -> K (NS f xs) x) -> (-.->) f (K (NS f xs)) x
    forall {k} (f :: k -> *) (a :: k) (f' :: k -> *).
    (f a -> f' a) -> (-.->) f f' a
    fn (NS f xs -> K (NS f xs) x
    forall k a (b :: k). a -> K a b
    K (NS f xs -> K (NS f xs) x)
    -> (f x -> NS f xs) -> f x -> K (NS f xs) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f x -> NS f xs
    f x -> NS f (x : xs)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z) (-.->) f (K (NS f xs)) x
    -> NP (Injection f xs) xs -> NP (Injection f xs) (x : xs)
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
    a x -> NP a xs -> NP a (x : xs)
    :* (forall (a :: k). Injection f xs a -> Injection f xs a)
    -> NP (Injection f xs) xs -> NP (Injection f xs) xs
    forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
    liftA_NP (-.->) f (K (NS f xs)) a -> (-.->) f (K (NS f xs)) a
    (-.->) f (K (NS f xs)) a -> Injection f (x : xs) a
    forall (a :: k). Injection f xs a -> Injection f xs a
    forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
    Injection f xs a -> Injection f (x : xs) a
    shiftInjection NP (Injection f xs) xs
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Injection f xs) xs
    injections

    -- | 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
    shiftInjection :: forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
    Injection f xs a -> Injection f (x : xs) a
    shiftInjection (Fn f a -> K (NS f xs) a
    f) = (f a -> K (NS f (x : xs)) a) -> (-.->) f (K (NS f (x : xs))) a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    (f a -> g a) -> (-.->) f g a
    Fn ((f a -> K (NS f (x : xs)) a) -> (-.->) f (K (NS f (x : xs))) a)
    -> (f a -> K (NS f (x : xs)) a) -> (-.->) f (K (NS f (x : xs))) a
    forall a b. (a -> b) -> a -> b
    $ NS f (x : xs) -> K (NS f (x : xs)) a
    forall k a (b :: k). a -> K a b
    K (NS f (x : xs) -> K (NS f (x : xs)) a)
    -> (f a -> NS f (x : xs)) -> f a -> K (NS f (x : xs)) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS f xs -> NS f (x : xs)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (NS f xs -> NS f (x : xs))
    -> (f a -> NS f xs) -> f a -> NS f (x : xs)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K (NS f xs) a -> NS f xs
    forall {k} a (b :: k). K a b -> a
    unK (K (NS f xs) a -> NS f xs)
    -> (f a -> K (NS f xs) a) -> f a -> NS f xs
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f a -> K (NS f xs) a
    f

    {-# DEPRECATED shift "Use 'shiftInjection' instead." #-}
    -- | Shift an injection.
    --
    -- Given an injection, return an injection into a sum that is one component larger.
    --
    shift :: Injection f xs a -> Injection f (x ': xs) a
    shift :: forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
    Injection f xs a -> Injection f (x : xs) a
    shift = Injection f xs a -> Injection f (x : xs) a
    forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
    Injection f xs a -> Injection f (x : xs) a
    shiftInjection

    -- | 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.
    --
    -- /Example:/
    --
    -- >>> apInjs_NP (I 'x' :* I True :* I 2 :* Nil)
    -- [Z (I 'x'),S (Z (I True)),S (S (Z (I 2)))]
    --
    apInjs_NP  :: SListI xs  => NP  f xs  -> [NS  f xs]
    apInjs_NP :: forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP f xs -> [NS f xs]
    apInjs_NP  = NP (K (NS f xs)) xs -> [NS f xs]
    NP (K (NS f xs)) xs -> CollapseTo NP (NS f xs)
    forall (xs :: [k]) a.
    SListIN NP xs =>
    NP (K a) xs -> CollapseTo NP a
    forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
    (HCollapse h, SListIN h xs) =>
    h (K a) xs -> CollapseTo h a
    hcollapse (NP (K (NS f xs)) xs -> [NS f xs])
    -> (NP f xs -> NP (K (NS f xs)) xs) -> NP f xs -> [NS f xs]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP f xs -> NP (K (NS f xs)) xs
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP f xs -> NP (K (NS f xs)) xs
    apInjs'_NP

    -- | `apInjs_NP` without `hcollapse`.
    --
    -- >>> 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
    --
    -- @since 0.2.5.0
    --
    apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs
    apInjs'_NP :: forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP f xs -> NP (K (NS f xs)) xs
    apInjs'_NP = Prod NP (f -.-> K (NS f xs)) xs -> NP f xs -> NP (K (NS f xs)) xs
    forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
           (xs :: l).
    HAp h =>
    Prod h (f -.-> g) xs -> h f xs -> h g xs
    forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
    Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
    hap Prod NP (f -.-> K (NS f xs)) xs
    NP (f -.-> K (NS f xs)) xs
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Injection f xs) xs
    injections

    -- | 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.
    --
    -- /Example:/
    --
    -- >>> 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)))]
    --
    apInjs_POP :: SListI xss => POP f xss -> [SOP f xss]
    apInjs_POP :: forall {k} (xss :: [[k]]) (f :: k -> *).
    SListI xss =>
    POP f xss -> [SOP f xss]
    apInjs_POP = (NS (NP f) xss -> SOP f xss) -> [NS (NP f) xss] -> [SOP f xss]
    forall a b. (a -> b) -> [a] -> [b]
    map NS (NP f) xss -> SOP f xss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP ([NS (NP f) xss] -> [SOP f xss])
    -> (POP f xss -> [NS (NP f) xss]) -> POP f xss -> [SOP f xss]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP (NP f) xss -> [NS (NP f) xss]
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP f xs -> [NS f xs]
    apInjs_NP (NP (NP f) xss -> [NS (NP f) xss])
    -> (POP f xss -> NP (NP f) xss) -> POP f xss -> [NS (NP f) xss]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . POP f xss -> NP (NP f) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
    unPOP

    -- | `apInjs_POP` without `hcollapse`.
    --
    -- /Example:/
    --
    -- >>> 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
    --
    -- @since 0.2.5.0
    --
    apInjs'_POP :: SListI xss => POP f xss -> NP (K (SOP f xss)) xss
    apInjs'_POP :: forall {k} (xss :: [[k]]) (f :: k -> *).
    SListI xss =>
    POP f xss -> NP (K (SOP f xss)) xss
    apInjs'_POP = (forall (a :: [k]). K (NS (NP f) xss) a -> K (SOP f xss) a)
    -> NP (K (NS (NP f) xss)) xss -> NP (K (SOP f xss)) xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hmap (SOP f xss -> K (SOP f xss) a
    forall k a (b :: k). a -> K a b
    K (SOP f xss -> K (SOP f xss) a)
    -> (K (NS (NP f) xss) a -> SOP f xss)
    -> K (NS (NP f) xss) a
    -> K (SOP f xss) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS (NP f) xss -> SOP f xss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (NS (NP f) xss -> SOP f xss)
    -> (K (NS (NP f) xss) a -> NS (NP f) xss)
    -> K (NS (NP f) xss) a
    -> SOP f xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K (NS (NP f) xss) a -> NS (NP f) xss
    forall {k} a (b :: k). K a b -> a
    unK) (NP (K (NS (NP f) xss)) xss -> NP (K (SOP f xss)) xss)
    -> (POP f xss -> NP (K (NS (NP f) xss)) xss)
    -> POP f xss
    -> NP (K (SOP f xss)) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Prod NP (NP f -.-> K (NS (NP f) xss)) xss
    -> NP (NP f) xss -> NP (K (NS (NP f) xss)) xss
    forall k l (h :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *)
           (xs :: l).
    HAp h =>
    Prod h (f -.-> g) xs -> h f xs -> h g xs
    forall (f :: [k] -> *) (g :: [k] -> *) (xs :: [[k]]).
    Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
    hap Prod NP (NP f -.-> K (NS (NP f) xss)) xss
    NP (NP f -.-> K (NS (NP f) xss)) xss
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Injection f xs) xs
    injections (NP (NP f) xss -> NP (K (NS (NP f) xss)) xss)
    -> (POP f xss -> NP (NP f) xss)
    -> POP f xss
    -> NP (K (NS (NP f) xss)) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . POP f xss -> NP (NP f) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
    unPOP

    type instance UnProd NP  = NS
    type instance UnProd POP = SOP

    instance HApInjs NS where
      hapInjs :: forall (xs :: [k]) (f :: k -> *).
    SListIN NS xs =>
    Prod NS f xs -> [NS f xs]
    hapInjs = Prod NS f xs -> [NS f xs]
    NP f xs -> [NS f xs]
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP f xs -> [NS f xs]
    apInjs_NP

    instance HApInjs SOP where
      hapInjs :: forall (xs :: [[k]]) (f :: k -> *).
    SListIN SOP xs =>
    Prod SOP f xs -> [SOP f xs]
    hapInjs = Prod SOP f xs -> [SOP f xs]
    POP f xs -> [SOP f xs]
    forall {k} (xss :: [[k]]) (f :: k -> *).
    SListI xss =>
    POP f xss -> [SOP f xss]
    apInjs_POP

    -- * Application

    -- | Specialization of 'hap'.
    ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs
    ap_NS :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NS f xs -> NS g xs
    ap_NS (Fn f x -> g x
    f  :* NP (f -.-> g) xs
    _)   (Z f x
    x)   = g x -> NS g (x : xs)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z (f x -> g x
    f f x
    f x
    x)
    ap_NS ((-.->) f g x
    _     :* NP (f -.-> g) xs
    fs)  (S NS f xs
    xs)  = NS g xs -> NS g (x : xs)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (NP (f -.-> g) xs -> NS f xs -> NS g xs
    forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NS f xs -> NS g xs
    ap_NS NP (f -.-> g) xs
    fs NS f xs
    NS f xs
    xs)
    ap_NS NP (f -.-> g) xs
    Nil            NS f xs
    x       = case NS f xs
    x of {}

    -- | Specialization of 'hap'.
    ap_SOP  :: POP (f -.-> g) xss -> SOP f xss -> SOP g xss
    ap_SOP :: forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    POP (f -.-> g) xss -> SOP f xss -> SOP g xss
    ap_SOP (POP NP (NP (f -.-> g)) xss
    fss') (SOP NS (NP f) xss
    xss') = NS (NP g) xss -> SOP g xss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
    forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
    go NP (NP (f -.-> g)) xss
    fss' NS (NP f) xss
    xss')
      where
        go :: NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
        go :: forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
    go (NP (f -.-> g) x
    fs :* NP (NP (f -.-> g)) xs
    _  ) (Z NP f x
    xs ) = NP g x -> NS (NP g) (x : xs)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z (NP (f -.-> g) x -> NP f x -> NP g x
    forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NP f xs -> NP g xs
    ap_NP NP (f -.-> g) x
    fs  NP f x
    NP f x
    xs )
        go (NP (f -.-> g) x
    _  :* NP (NP (f -.-> g)) xs
    fss) (S NS (NP f) xs
    xss) = NS (NP g) xs -> NS (NP g) (x : xs)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (NP (NP (f -.-> g)) xs -> NS (NP f) xs -> NS (NP g) xs
    forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    NP (NP (f -.-> g)) xss -> NS (NP f) xss -> NS (NP g) xss
    go    NP (NP (f -.-> g)) xs
    fss NS (NP f) xs
    NS (NP f) xs
    xss)
        go NP (NP (f -.-> g)) xss
    Nil         NS (NP f) xss
    x       = case NS (NP f) xss
    x of {}

    -- The definition of 'ap_SOP' is a more direct variant of
    -- '_ap_SOP_spec'. The direct definition has the advantage
    -- that it avoids the 'SListI' constraint.
    _ap_SOP_spec :: SListI xss => POP (t -.-> f) xss -> SOP t xss -> SOP f xss
    _ap_SOP_spec :: forall {k} (xss :: [[k]]) (t :: k -> *) (f :: k -> *).
    SListI xss =>
    POP (t -.-> f) xss -> SOP t xss -> SOP f xss
    _ap_SOP_spec (POP NP (NP (t -.-> f)) xss
    fs) (SOP NS (NP t) xss
    xs) = NS (NP f) xss -> SOP f xss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP ((forall (a :: [k]). NP (t -.-> f) a -> NP t a -> NP f a)
    -> NP (NP (t -.-> f)) xss -> NS (NP t) xss -> NS (NP f) xss
    forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NS g xs -> NS h xs
    liftA2_NS NP (t -.-> f) a -> NP t a -> NP f a
    forall (a :: [k]). NP (t -.-> f) a -> NP t a -> NP f a
    forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NP f xs -> NP g xs
    ap_NP NP (NP (t -.-> f)) xss
    fs NS (NP t) xss
    xs)

    type instance Same NS  = NS
    type instance Same SOP = SOP

    type instance Prod NS  = NP
    type instance Prod SOP = POP

    type instance SListIN NS  = SListI
    type instance SListIN SOP = SListI2

    instance HAp NS  where hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [k]).
    Prod NS (f -.-> g) xs -> NS f xs -> NS g xs
    hap = Prod NS (f -.-> g) xs -> NS f xs -> NS g xs
    NP (f -.-> g) xs -> NS f xs -> NS g xs
    forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NS f xs -> NS g xs
    ap_NS
    instance HAp SOP where hap :: forall (f :: k -> *) (g :: k -> *) (xs :: [[k]]).
    Prod SOP (f -.-> g) xs -> SOP f xs -> SOP g xs
    hap = Prod SOP (f -.-> g) xs -> SOP f xs -> SOP g xs
    POP (f -.-> g) xs -> SOP f xs -> SOP g xs
    forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    POP (f -.-> g) xss -> SOP f xss -> SOP g xss
    ap_SOP

    -- * Lifting / mapping

    -- | Specialization of 'hliftA'.
    liftA_NS  :: SListI     xs  => (forall a. f a -> g a) -> NS  f xs  -> NS  g xs
    -- | Specialization of 'hliftA'.
    liftA_SOP :: All SListI xss => (forall a. f a -> g a) -> SOP f xss -> SOP g xss

    liftA_NS :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs
    liftA_NS  = (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hliftA
    liftA_SOP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a) -> SOP f xss -> SOP g xss
    liftA_SOP = (forall (a :: k). f a -> g a) -> SOP f xss -> SOP g xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hliftA

    -- | Specialization of 'hliftA2'.
    liftA2_NS  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NS  g xs  -> NS   h xs
    -- | Specialization of 'hliftA2'.
    liftA2_SOP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> SOP g xss -> SOP  h xss

    liftA2_NS :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NS g xs -> NS h xs
    liftA2_NS  = (forall (a :: k). f a -> g a -> h a)
    -> Prod NS f xs -> NS g xs -> NS h xs
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NS g xs -> NS h xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *).
    (SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
    (forall (a :: k). f a -> f' a -> f'' a)
    -> Prod h f xs -> h f' xs -> h f'' xs
    hliftA2
    liftA2_SOP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *)
           (h :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a -> h a)
    -> POP f xss -> SOP g xss -> SOP h xss
    liftA2_SOP = (forall (a :: k). f a -> g a -> h a)
    -> Prod SOP f xss -> SOP g xss -> SOP h xss
    (forall (a :: k). f a -> g a -> h a)
    -> POP f xss -> SOP g xss -> SOP h xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *).
    (SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
    (forall (a :: k). f a -> f' a -> f'' a)
    -> Prod h f xs -> h f' xs -> h f'' xs
    hliftA2

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

    map_NS :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs
    map_NS  = (forall (a :: k). f a -> g a) -> NS f xs -> NS g xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hmap
    map_SOP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a) -> SOP f xss -> SOP g xss
    map_SOP = (forall (a :: k). f a -> g a) -> SOP f xss -> SOP g xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hmap

    -- | Specialization of 'hcliftA'.
    cliftA_NS  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NS   f xs  -> NS  g xs
    -- | Specialization of 'hcliftA'.
    cliftA_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP  f xss -> SOP g xss

    cliftA_NS :: forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    All c xs =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs
    cliftA_NS  = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (f' :: k -> *).
    (AllN (Prod h) c xs, HAp h) =>
    proxy c
    -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
    hcliftA
    cliftA_SOP :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    All2 c xss =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP g xss
    cliftA_SOP = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP g xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (f' :: k -> *).
    (AllN (Prod h) c xs, HAp h) =>
    proxy c
    -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
    hcliftA

    -- | Specialization of 'hcliftA2'.
    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 'hcliftA2'.
    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

    cliftA2_NS :: forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *).
    All c xs =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> NP f xs
    -> NS g xs
    -> NS h xs
    cliftA2_NS  = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> Prod NS f xs
    -> NS g xs
    -> NS h xs
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> NP f xs
    -> NS g xs
    -> NS h xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *).
    (AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
    proxy c
    -> (forall (a :: k). c a => f a -> f' a -> f'' a)
    -> Prod h f xs
    -> h f' xs
    -> h f'' xs
    hcliftA2
    cliftA2_SOP :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *).
    All2 c xss =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> POP f xss
    -> SOP g xss
    -> SOP h xss
    cliftA2_SOP = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> Prod SOP f xss
    -> SOP g xss
    -> SOP h xss
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> POP f xss
    -> SOP g xss
    -> SOP h xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *).
    (AllN (Prod h) c xs, HAp h, HAp (Prod h)) =>
    proxy c
    -> (forall (a :: k). c a => f a -> f' a -> f'' a)
    -> Prod h f xs
    -> h f' xs
    -> h f'' xs
    hcliftA2

    -- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
    cmap_NS  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NS   f xs  -> NS  g xs
    -- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
    cmap_SOP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> SOP  f xss -> SOP g xss

    cmap_NS :: forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    All c xs =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs
    cmap_NS  = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NS f xs -> NS g xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (f' :: k -> *).
    (AllN (Prod h) c xs, HAp h) =>
    proxy c
    -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
    hcmap
    cmap_SOP :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    All2 c xss =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP g xss
    cmap_SOP = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> SOP f xss -> SOP g xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (f' :: k -> *).
    (AllN (Prod h) c xs, HAp h) =>
    proxy c
    -> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
    hcmap

    -- * Dealing with @'All' c@

    -- | Specialization of 'hcliftA2''.
    {-# DEPRECATED cliftA2'_NS "Use 'cliftA2_NS' instead." #-}
    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

    cliftA2'_NS :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: [k] -> *) (g :: [k] -> *)
           (h :: [k] -> *).
    All2 c xss =>
    proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
    -> NP f xss
    -> NS g xss
    -> NS h xss
    cliftA2'_NS = proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
    -> Prod NS f xss
    -> NS g xss
    -> NS h xss
    proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
    -> NP f xss
    -> NS g xss
    -> NS h xss
    forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (h :: ([k] -> *) -> [[k]] -> *) (proxy :: (k -> Constraint) -> *)
           (f :: [k] -> *) (f' :: [k] -> *) (f'' :: [k] -> *).
    (All2 c xss, Prod h ~ NP, HAp h) =>
    proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> f' xs -> f'' xs)
    -> Prod h f xss
    -> h f' xss
    -> h f'' xss
    hcliftA2'

    -- * Comparison

    -- | 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.
    --
    -- @since 0.3.2.0
    --
    compare_NS ::
         forall r f g xs .
         r                             -- ^ what to do if first is smaller
      -> (forall x . f x -> g x -> r)  -- ^ what to do if both are equal
      -> r                             -- ^ what to do if first is larger
      -> NS f xs -> NS g xs
      -> r
    compare_NS :: forall {k} r (f :: k -> *) (g :: k -> *) (xs :: [k]).
    r
    -> (forall (x :: k). f x -> g x -> r)
    -> r
    -> NS f xs
    -> NS g xs
    -> r
    compare_NS r
    lt forall (x :: k). f x -> g x -> r
    eq r
    gt = NS f xs -> NS g xs -> r
    forall (ys :: [k]). NS f ys -> NS g ys -> r
    go
      where
        go :: forall ys . NS f ys -> NS g ys -> r
        go :: forall (ys :: [k]). NS f ys -> NS g ys -> r
    go (Z f x
    x)  (Z g x
    y)  = f x -> g x -> r
    forall (x :: k). f x -> g x -> r
    eq f x
    x g x
    g x
    y
        go (Z f x
    _)  (S NS g xs
    _)  = r
    lt
        go (S NS f xs
    _)  (Z g x
    _)  = r
    gt
        go (S NS f xs
    xs) (S NS g xs
    ys) = NS f xs -> NS g xs -> r
    forall (ys :: [k]). NS f ys -> NS g ys -> r
    go NS f xs
    xs NS g xs
    NS g xs
    ys
    --
    -- NOTE: The above could be written in terms of
    -- ccompare_NS, but the direct definition avoids the
    -- SListI constraint. We may change this in the future.

    -- | Constrained version of 'compare_NS'.
    --
    -- @since 0.3.2.0
    --
    ccompare_NS ::
         forall c proxy r f g xs .
         (All c xs)
      => proxy c
      -> r                                    -- ^ what to do if first is smaller
      -> (forall x . c x => f x -> g x -> r)  -- ^ what to do if both are equal
      -> r                                    -- ^ what to do if first is larger
      -> NS f xs -> NS g xs
      -> r
    ccompare_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           r (f :: k -> *) (g :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> r
    -> (forall (x :: k). c x => f x -> g x -> r)
    -> r
    -> NS f xs
    -> NS g xs
    -> r
    ccompare_NS proxy c
    _ r
    lt forall (x :: k). c x => f x -> g x -> r
    eq r
    gt = NS f xs -> NS g xs -> r
    forall (ys :: [k]). All c ys => NS f ys -> NS g ys -> r
    go
      where
        go :: forall ys . (All c ys) => NS f ys -> NS g ys -> r
        go :: forall (ys :: [k]). All c ys => NS f ys -> NS g ys -> r
    go (Z f x
    x)  (Z g x
    y)  = f x -> g x -> r
    forall (x :: k). c x => f x -> g x -> r
    eq f x
    x g x
    g x
    y
        go (Z f x
    _)  (S NS g xs
    _)  = r
    lt
        go (S NS f xs
    _)  (Z g x
    _)  = r
    gt
        go (S NS f xs
    xs) (S NS g xs
    ys) = NS f xs -> NS g xs -> r
    forall (ys :: [k]). All c ys => NS f ys -> NS g ys -> r
    go NS f xs
    xs NS g xs
    NS g xs
    ys

    -- | 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 'ccompare_NS' for
    -- a common special case.
    --
    -- @since 0.3.2.0
    --
    compare_SOP ::
         forall r f g xss .
         r                                      -- ^ what to do if first is smaller
      -> (forall xs . NP f xs -> NP g xs -> r)  -- ^ what to do if both are equal
      -> r                                      -- ^ what to do if first is larger
      -> SOP f xss -> SOP g xss
      -> r
    compare_SOP :: forall {k} r (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    r
    -> (forall (xs :: [k]). NP f xs -> NP g xs -> r)
    -> r
    -> SOP f xss
    -> SOP g xss
    -> r
    compare_SOP r
    lt forall (xs :: [k]). NP f xs -> NP g xs -> r
    eq r
    gt (SOP NS (NP f) xss
    xs) (SOP NS (NP g) xss
    ys) =
      r
    -> (forall (xs :: [k]). NP f xs -> NP g xs -> r)
    -> r
    -> NS (NP f) xss
    -> NS (NP g) xss
    -> r
    forall {k} r (f :: k -> *) (g :: k -> *) (xs :: [k]).
    r
    -> (forall (x :: k). f x -> g x -> r)
    -> r
    -> NS f xs
    -> NS g xs
    -> r
    compare_NS r
    lt NP f x -> NP g x -> r
    forall (xs :: [k]). NP f xs -> NP g xs -> r
    eq r
    gt NS (NP f) xss
    xs NS (NP g) xss
    ys

    -- | Constrained version of 'compare_SOP'.
    --
    -- @since 0.3.2.0
    --
    ccompare_SOP ::
         forall c proxy r f g xss .
         (All2 c xss)
      => proxy c
      -> r                                                  -- ^ what to do if first is smaller
      -> (forall xs . All c xs => NP f xs -> NP g xs -> r)  -- ^ what to do if both are equal
      -> r                                                  -- ^ what to do if first is larger
      -> SOP f xss -> SOP g xss
      -> r
    ccompare_SOP :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           r (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    All2 c xss =>
    proxy c
    -> r
    -> (forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r)
    -> r
    -> SOP f xss
    -> SOP g xss
    -> r
    ccompare_SOP proxy c
    p r
    lt forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r
    eq r
    gt (SOP NS (NP f) xss
    xs) (SOP NS (NP g) xss
    ys) =
      Proxy (All c)
    -> r
    -> (forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r)
    -> r
    -> NS (NP f) xss
    -> NS (NP g) xss
    -> r
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           r (f :: k -> *) (g :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> r
    -> (forall (x :: k). c x => f x -> g x -> r)
    -> r
    -> NS f xs
    -> NS g xs
    -> r
    ccompare_NS (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p) r
    lt NP f x -> NP g x -> r
    forall (xs :: [k]). All c xs => NP f xs -> NP g xs -> r
    eq r
    gt NS (NP f) xss
    xs NS (NP g) xss
    ys

    -- * Collapsing

    -- | Specialization of 'hcollapse'.
    collapse_NS  ::               NS  (K a) xs  ->   a
    -- | Specialization of 'hcollapse'.
    collapse_SOP :: SListI xss => SOP (K a) xss ->  [a]

    collapse_NS :: forall {k} a (xs :: [k]). NS (K a) xs -> a
    collapse_NS (Z (K a
    x)) = a
    x
    collapse_NS (S NS (K a) xs
    xs)    = NS (K a) xs -> a
    forall {k} a (xs :: [k]). NS (K a) xs -> a
    collapse_NS NS (K a) xs
    xs

    collapse_SOP :: forall {k} (xss :: [[k]]) a. SListI xss => SOP (K a) xss -> [a]
    collapse_SOP = NS (K [a]) xss -> [a]
    forall {k} a (xs :: [k]). NS (K a) xs -> a
    collapse_NS (NS (K [a]) xss -> [a])
    -> (SOP (K a) xss -> NS (K [a]) xss) -> SOP (K a) xss -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (a :: [k]). NP (K a) a -> K [a] a)
    -> NS (NP (K a)) xss -> NS (K [a]) xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hliftA ([a] -> K [a] a
    forall k a (b :: k). a -> K a b
    K ([a] -> K [a] a) -> (NP (K a) a -> [a]) -> NP (K a) a -> K [a] a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP (K a) a -> [a]
    forall {k} a (xs :: [k]). NP (K a) xs -> [a]
    collapse_NP) (NS (NP (K a)) xss -> NS (K [a]) xss)
    -> (SOP (K a) xss -> NS (NP (K a)) xss)
    -> SOP (K a) xss
    -> NS (K [a]) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP (K a) xss -> NS (NP (K a)) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    type instance CollapseTo NS  a =  a
    type instance CollapseTo SOP a = [a]

    instance HCollapse NS  where hcollapse :: forall (xs :: [k]) a.
    SListIN NS xs =>
    NS (K a) xs -> CollapseTo NS a
    hcollapse = NS (K a) xs -> a
    NS (K a) xs -> CollapseTo NS a
    forall {k} a (xs :: [k]). NS (K a) xs -> a
    collapse_NS
    instance HCollapse SOP where hcollapse :: forall (xs :: [[k]]) a.
    SListIN SOP xs =>
    SOP (K a) xs -> CollapseTo SOP a
    hcollapse = SOP (K a) xs -> [a]
    SOP (K a) xs -> CollapseTo SOP a
    forall {k} (xss :: [[k]]) a. SListI xss => SOP (K a) xss -> [a]
    collapse_SOP

    -- * Folding

    -- | Specialization of 'hctraverse_'.
    --
    -- /Note:/ we don't need 'Applicative' constraint.
    --
    -- @since 0.3.2.0
    --
    ctraverse__NS ::
         forall c proxy xs f g. (All c xs)
      => proxy c -> (forall a. c a => f a -> g ()) -> NS f xs -> g ()
    ctraverse__NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (g :: * -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g ()
    ctraverse__NS proxy c
    _ forall (a :: k). c a => f a -> g ()
    f = NS f xs -> g ()
    forall (ys :: [k]). All c ys => NS f ys -> g ()
    go
      where
        go :: All c ys => NS f ys -> g ()
        go :: forall (ys :: [k]). All c ys => NS f ys -> g ()
    go (Z f x
    x)  = f x -> g ()
    forall (a :: k). c a => f a -> g ()
    f f x
    x
        go (S NS f xs
    xs) = NS f xs -> g ()
    forall (ys :: [k]). All c ys => NS f ys -> g ()
    go NS f xs
    xs

    -- | Specialization of 'htraverse_'.
    --
    -- /Note:/ we don't need 'Applicative' constraint.
    --
    -- @since 0.3.2.0
    --
    traverse__NS ::
         forall xs f g. (SListI xs)
      => (forall a. f a -> g ()) -> NS f xs -> g ()
    traverse__NS :: forall {k} (xs :: [k]) (f :: k -> *) (g :: * -> *).
    SListI xs =>
    (forall (a :: k). f a -> g ()) -> NS f xs -> g ()
    traverse__NS forall (a :: k). f a -> g ()
    f = NS f xs -> g ()
    forall (ys :: [k]). NS f ys -> g ()
    go
      where
        go :: NS f ys -> g ()
        go :: forall (ys :: [k]). NS f ys -> g ()
    go (Z f x
    x)  = f x -> g ()
    forall (a :: k). f a -> g ()
    f f x
    x
        go (S NS f xs
    xs) = NS f xs -> g ()
    forall (ys :: [k]). NS f ys -> g ()
    go NS f xs
    xs

    -- | Specialization of 'hctraverse_'.
    --
    -- @since 0.3.2.0
    --
    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 ()
    ctraverse__SOP :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (All2 c xss, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> SOP f xss -> g ()
    ctraverse__SOP proxy c
    p forall (a :: k). c a => f a -> g ()
    f = Proxy (All c)
    -> (forall (a :: [k]). All c a => NP f a -> g ())
    -> NS (NP f) xss
    -> g ()
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (g :: * -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g ()
    ctraverse__NS (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p) (proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f a -> g ()
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (g :: * -> *).
    (All c xs, Applicative g) =>
    proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
    ctraverse__NP proxy c
    p f a -> g ()
    forall (a :: k). c a => f a -> g ()
    f) (NS (NP f) xss -> g ())
    -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> g ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP f xss -> NS (NP f) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    -- | Specialization of 'htraverse_'.
    --
    -- @since 0.3.2.0
    --
    traverse__SOP ::
         forall xss f g. (SListI2 xss, Applicative g)
      => (forall a. f a -> g ()) -> SOP f xss -> g ()
    traverse__SOP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> SOP f xss -> g ()
    traverse__SOP forall (a :: k). f a -> g ()
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g ()) -> SOP f xss -> g ()
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (All2 c xss, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> SOP f xss -> g ()
    ctraverse__SOP Proxy Top
    forall {k}. Proxy Top
    topP f a -> g ()
    forall (a :: k). f a -> g ()
    forall (a :: k). Top a => f a -> g ()
    f
    {-# INLINE traverse__SOP #-}

    topP :: Proxy Top
    topP :: forall {k}. Proxy Top
    topP = Proxy Top
    forall {k} (t :: k). Proxy t
    Proxy

    instance HTraverse_ NS  where
      hctraverse_ :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (AllN NS c xs, Applicative g) =>
    proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g ()
    hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g ()
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (g :: * -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a -> g ()) -> NS f xs -> g ()
    ctraverse__NS
      htraverse_ :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *).
    (SListIN NS xs, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> NS f xs -> g ()
    htraverse_  = (forall (a :: k). f a -> g ()) -> NS f xs -> g ()
    forall {k} (xs :: [k]) (f :: k -> *) (g :: * -> *).
    SListI xs =>
    (forall (a :: k). f a -> g ()) -> NS f xs -> g ()
    traverse__NS

    instance HTraverse_ SOP where
      hctraverse_ :: forall (c :: k -> Constraint) (xs :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (AllN SOP c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> SOP f xs -> g ()
    hctraverse_ = proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> SOP f xs -> g ()
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (All2 c xss, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> SOP f xss -> g ()
    ctraverse__SOP
      htraverse_ :: forall (xs :: [[k]]) (g :: * -> *) (f :: k -> *).
    (SListIN SOP xs, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> SOP f xs -> g ()
    htraverse_  = (forall (a :: k). f a -> g ()) -> SOP f xs -> g ()
    forall {k} (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> SOP f xss -> g ()
    traverse__SOP

    -- | Specialization of 'hcfoldMap'.
    --
    -- /Note:/ We don't need 'Monoid' instance.
    --
    -- @since 0.3.2.0
    --
    cfoldMap_NS ::
         forall c proxy f xs m. (All c xs)
      => proxy c -> (forall a. c a => f a -> m) -> NS f xs -> m
    cfoldMap_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xs :: [k]) m.
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a -> m) -> NS f xs -> m
    cfoldMap_NS proxy c
    _ forall (a :: k). c a => f a -> m
    f = NS f xs -> m
    forall (ys :: [k]). All c ys => NS f ys -> m
    go
      where
        go :: All c ys => NS f ys -> m
        go :: forall (ys :: [k]). All c ys => NS f ys -> m
    go (Z f x
    x)  = f x -> m
    forall (a :: k). c a => f a -> m
    f f x
    x
        go (S NS f xs
    xs) = NS f xs -> m
    forall (ys :: [k]). All c ys => NS f ys -> m
    go NS f xs
    xs

    -- | Specialization of 'hcfoldMap'.
    --
    -- @since 0.3.2.0
    --
    cfoldMap_SOP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> SOP f xs -> m
    cfoldMap_SOP :: forall {k} (c :: k -> Constraint) (xs :: [[k]]) m
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (All2 c xs, Monoid m) =>
    proxy c -> (forall (a :: k). c a => f a -> m) -> SOP f xs -> m
    cfoldMap_SOP = proxy c -> (forall (a :: k). c a => f a -> m) -> SOP f xs -> m
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) m (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (HTraverse_ h, AllN h c xs, Monoid m) =>
    proxy c -> (forall (a :: k). c a => f a -> m) -> h f xs -> m
    hcfoldMap

    -- * Sequencing

    -- | Specialization of 'hsequence''.
    sequence'_NS  ::              Applicative f  => NS  (f :.: g) xs  -> f (NS  g xs)
    sequence'_NS :: forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NS (f :.: g) xs -> f (NS g xs)
    sequence'_NS (Z (:.:) f g x
    mx)  = g x -> NS g xs
    g x -> NS g (x : xs)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z (g x -> NS g xs) -> f (g x) -> f (NS g xs)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (:.:) f g x -> f (g x)
    forall {l} {k} (f :: l -> *) (g :: k -> l) (p :: k).
    (:.:) f g p -> f (g p)
    unComp (:.:) f g x
    mx
    sequence'_NS (S NS (f :.: g) xs
    mxs) = NS g xs -> NS g xs
    NS g xs -> NS g (x : xs)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (NS g xs -> NS g xs) -> f (NS g xs) -> f (NS g xs)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NS (f :.: g) xs -> f (NS g xs)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NS (f :.: g) xs -> f (NS g xs)
    sequence'_NS NS (f :.: g) xs
    mxs

    -- | Specialization of 'hsequence''.
    sequence'_SOP :: (SListI xss, Applicative f) => SOP (f :.: g) xss -> f (SOP g xss)
    sequence'_SOP :: forall {k} (xss :: [[k]]) (f :: * -> *) (g :: k -> *).
    (SListI xss, Applicative f) =>
    SOP (f :.: g) xss -> f (SOP g xss)
    sequence'_SOP = (NS (NP g) xss -> SOP g xss) -> f (NS (NP g) xss) -> f (SOP g xss)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NS (NP g) xss -> SOP g xss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (f (NS (NP g) xss) -> f (SOP g xss))
    -> (SOP (f :.: g) xss -> f (NS (NP g) xss))
    -> SOP (f :.: g) xss
    -> f (SOP g xss)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NS (f :.: NP g) xss -> f (NS (NP g) xss)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NS (f :.: g) xs -> f (NS g xs)
    sequence'_NS (NS (f :.: NP g) xss -> f (NS (NP g) xss))
    -> (SOP (f :.: g) xss -> NS (f :.: NP g) xss)
    -> SOP (f :.: g) xss
    -> f (NS (NP g) xss)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (a :: [k]). NP (f :.: g) a -> (:.:) f (NP g) a)
    -> NS (NP (f :.: g)) xss -> NS (f :.: NP g) xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *).
    (SListIN (Prod h) xs, HAp h) =>
    (forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
    hliftA (f (NP g a) -> (:.:) f (NP g) a
    forall l k (f :: l -> *) (g :: k -> l) (p :: k).
    f (g p) -> (:.:) f g p
    Comp (f (NP g a) -> (:.:) f (NP g) a)
    -> (NP (f :.: g) a -> f (NP g a))
    -> NP (f :.: g) a
    -> (:.:) f (NP g) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP (f :.: g) a -> f (NP g a)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NP (f :.: g) xs -> f (NP g xs)
    sequence'_NP) (NS (NP (f :.: g)) xss -> NS (f :.: NP g) xss)
    -> (SOP (f :.: g) xss -> NS (NP (f :.: g)) xss)
    -> SOP (f :.: g) xss
    -> NS (f :.: NP g) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP (f :.: g) xss -> NS (NP (f :.: g)) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    -- | Specialization of 'hctraverse''.
    --
    -- /Note:/ as 'NS' has exactly one element, the 'Functor' constraint is enough.
    --
    -- @since 0.3.2.0
    --
    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)
    ctraverse'_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (All c xs, Functor g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    ctraverse'_NS proxy c
    _ forall (a :: k). c a => f a -> g (f' a)
    f = NS f xs -> g (NS f' xs)
    forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
    go where
      go :: All c ys => NS f ys -> g (NS f' ys)
      go :: forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
    go (Z f x
    x)  = f' x -> NS f' ys
    f' x -> NS f' (x : xs)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z (f' x -> NS f' ys) -> g (f' x) -> g (NS f' ys)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f x -> g (f' x)
    forall (a :: k). c a => f a -> g (f' a)
    f f x
    x
      go (S NS f xs
    xs) = NS f' xs -> NS f' ys
    NS f' xs -> NS f' (x : xs)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (NS f' xs -> NS f' ys) -> g (NS f' xs) -> g (NS f' ys)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NS f xs -> g (NS f' xs)
    forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
    go NS f xs
    xs

    -- | Specialization of 'htraverse''.
    --
    -- /Note:/ as 'NS' has exactly one element, the 'Functor' constraint is enough.
    --
    -- @since 0.3.2.0
    --
    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)
    traverse'_NS :: forall {k} (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (SListI xs, Functor g) =>
    (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
    traverse'_NS forall (a :: k). f a -> g (f' a)
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (All c xs, Functor g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    ctraverse'_NS Proxy Top
    forall {k}. Proxy Top
    topP f a -> g (f' a)
    forall (a :: k). f a -> g (f' a)
    forall (a :: k). Top a => f a -> g (f' a)
    f
    {-# INLINE traverse'_NS #-}

    -- | Specialization of 'hctraverse''.
    --
    -- @since 0.3.2.0
    --
    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)
    ctraverse'_SOP :: forall {k} (c :: k -> Constraint) (xss :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (All2 c xss, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> SOP f xss
    -> g (SOP f' xss)
    ctraverse'_SOP proxy c
    p forall (a :: k). c a => f a -> g (f' a)
    f = (NS (NP f') xss -> SOP f' xss)
    -> g (NS (NP f') xss) -> g (SOP f' xss)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NS (NP f') xss -> SOP f' xss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (g (NS (NP f') xss) -> g (SOP f' xss))
    -> (SOP f xss -> g (NS (NP f') xss)) -> SOP f xss -> g (SOP f' xss)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy (All c)
    -> (forall (a :: [k]). All c a => NP f a -> g (NP f' a))
    -> NS (NP f) xss
    -> g (NS (NP f') xss)
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (All c xs, Functor g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    ctraverse'_NS (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p) (proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NP f a
    -> g (NP f' a)
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (All c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NP f xs
    -> g (NP f' xs)
    ctraverse'_NP proxy c
    p f a -> g (f' a)
    forall (a :: k). c a => f a -> g (f' a)
    f) (NS (NP f) xss -> g (NS (NP f') xss))
    -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> g (NS (NP f') xss)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP f xss -> NS (NP f) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    -- | Specialization of 'htraverse''.
    --
    -- @since 0.3.2.0
    --
    traverse'_SOP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)
    traverse'_SOP :: forall {k} (xss :: [[k]]) (g :: * -> *) (f :: k -> *)
           (f' :: k -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)
    traverse'_SOP forall (a :: k). f a -> g (f' a)
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g (f' a))
    -> SOP f xss
    -> g (SOP f' xss)
    forall {k} (c :: k -> Constraint) (xss :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (All2 c xss, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> SOP f xss
    -> g (SOP f' xss)
    ctraverse'_SOP Proxy Top
    forall {k}. Proxy Top
    topP f a -> g (f' a)
    forall (a :: k). f a -> g (f' a)
    forall (a :: k). Top a => f a -> g (f' a)
    f
    {-# INLINE traverse'_SOP #-}

    instance HSequence NS  where
      hsequence' :: forall (xs :: [k]) (f :: * -> *) (g :: k -> *).
    (SListIN NS xs, Applicative f) =>
    NS (f :.: g) xs -> f (NS g xs)
    hsequence'  = NS (f :.: g) xs -> f (NS g xs)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NS (f :.: g) xs -> f (NS g xs)
    sequence'_NS
      hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (AllN NS c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    hctraverse' = proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (All c xs, Functor g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NS f xs
    -> g (NS f' xs)
    ctraverse'_NS
      htraverse' :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
    (SListIN NS xs, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
    htraverse'  = (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
    forall {k} (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (SListI xs, Functor g) =>
    (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
    traverse'_NS

    instance HSequence SOP where
      hsequence' :: forall (xs :: [[k]]) (f :: * -> *) (g :: k -> *).
    (SListIN SOP xs, Applicative f) =>
    SOP (f :.: g) xs -> f (SOP g xs)
    hsequence'  = SOP (f :.: g) xs -> f (SOP g xs)
    forall {k} (xss :: [[k]]) (f :: * -> *) (g :: k -> *).
    (SListI xss, Applicative f) =>
    SOP (f :.: g) xss -> f (SOP g xss)
    sequence'_SOP
      hctraverse' :: forall (c :: k -> Constraint) (xs :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (AllN SOP c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> SOP f xs
    -> g (SOP f' xs)
    hctraverse' = proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> SOP f xs
    -> g (SOP f' xs)
    forall {k} (c :: k -> Constraint) (xss :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (All2 c xss, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> SOP f xss
    -> g (SOP f' xss)
    ctraverse'_SOP
      htraverse' :: forall (xs :: [[k]]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
    (SListIN SOP xs, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs)
    htraverse'  = (forall (a :: k). f a -> g (f' a)) -> SOP f xs -> g (SOP f' xs)
    forall {k} (xss :: [[k]]) (g :: * -> *) (f :: k -> *)
           (f' :: k -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> SOP f xss -> g (SOP f' xss)
    traverse'_SOP

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

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

    sequence_NS :: forall (xs :: [*]) (f :: * -> *).
    (SListI xs, Applicative f) =>
    NS f xs -> f (NS I xs)
    sequence_NS   = NS f xs -> f (NS I xs)
    forall {l} (h :: (* -> *) -> l -> *) (xs :: l) (f :: * -> *).
    (SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) =>
    h f xs -> f (h I xs)
    hsequence
    sequence_SOP :: forall (xss :: [[*]]) (f :: * -> *).
    (All SListI xss, Applicative f) =>
    SOP f xss -> f (SOP I xss)
    sequence_SOP  = SOP f xss -> f (SOP I xss)
    forall {l} (h :: (* -> *) -> l -> *) (xs :: l) (f :: * -> *).
    (SListIN h xs, SListIN (Prod h) xs, HSequence h, Applicative f) =>
    h f xs -> f (h I xs)
    hsequence

    -- | Specialization of 'hctraverse'.
    --
    -- @since 0.3.2.0
    --
    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 'hctraverse'.
    --
    -- @since 0.3.2.0
    --
    ctraverse_SOP :: (All2 c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)

    ctraverse_NS :: forall (c :: * -> Constraint) (xs :: [*]) (g :: * -> *)
           (proxy :: (* -> Constraint) -> *) (f :: * -> *).
    (All c xs, Applicative g) =>
    proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)
    ctraverse_NS = proxy c -> (forall a. c a => f a -> g a) -> NP f xs -> g (NP I xs)
    forall {l} (h :: (* -> *) -> l -> *) (c :: * -> Constraint)
           (xs :: l) (g :: * -> *) (proxy :: (* -> Constraint) -> *)
           (f :: * -> *).
    (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)
    hctraverse
    ctraverse_SOP :: forall (c :: * -> Constraint) (xs :: [[*]]) (g :: * -> *)
           (proxy :: (* -> Constraint) -> *) (f :: * -> *).
    (All2 c xs, Applicative g) =>
    proxy c
    -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)
    ctraverse_SOP = proxy c
    -> (forall a. c a => f a -> g a) -> POP f xs -> g (POP I xs)
    forall {l} (h :: (* -> *) -> l -> *) (c :: * -> Constraint)
           (xs :: l) (g :: * -> *) (proxy :: (* -> Constraint) -> *)
           (f :: * -> *).
    (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)
    hctraverse

    -- * Catamorphism and anamorphism

    -- | Catamorphism for 'NS'.
    --
    -- Takes arguments determining what to do for 'Z'
    -- and what to do for 'S'. The result type is still
    -- indexed over the type-level lit.
    --
    -- @since 0.2.3.0
    --
    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
    cata_NS :: forall {k} (r :: [k] -> *) (f :: k -> *) (xs :: [k]).
    (forall (y :: k) (ys :: [k]). f y -> r (y : ys))
    -> (forall (y :: k) (ys :: [k]). r ys -> r (y : ys))
    -> NS f xs
    -> r xs
    cata_NS forall (y :: k) (ys :: [k]). f y -> r (y : ys)
    z forall (y :: k) (ys :: [k]). r ys -> r (y : ys)
    s = NS f xs -> r xs
    forall (ys :: [k]). NS f ys -> r ys
    go
      where
        go :: forall ys . NS f ys -> r ys
        go :: forall (ys :: [k]). NS f ys -> r ys
    go (Z f x
    x) = f x -> r (x : xs)
    forall (y :: k) (ys :: [k]). f y -> r (y : ys)
    z f x
    x
        go (S NS f xs
    i) = r xs -> r (x : xs)
    forall (y :: k) (ys :: [k]). r ys -> r (y : ys)
    s (NS f xs -> r xs
    forall (ys :: [k]). NS f ys -> r ys
    go NS f xs
    i)

    -- | Constrained catamorphism for 'NS'.
    --
    -- @since 0.2.3.0
    --
    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
    ccata_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (r :: [k] -> *) (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> (forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys))
    -> (forall (y :: k) (ys :: [k]). c y => r ys -> r (y : ys))
    -> NS f xs
    -> r xs
    ccata_NS proxy c
    _ forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys)
    z forall (y :: k) (ys :: [k]). c y => r ys -> r (y : ys)
    s = NS f xs -> r xs
    forall (ys :: [k]). All c ys => NS f ys -> r ys
    go
      where
        go :: forall ys . (All c ys) => NS f ys -> r ys
        go :: forall (ys :: [k]). All c ys => NS f ys -> r ys
    go (Z f x
    x) = f x -> r (x : xs)
    forall (y :: k) (ys :: [k]). c y => f y -> r (y : ys)
    z f x
    x
        go (S NS f xs
    i) = r xs -> r (x : xs)
    forall (y :: k) (ys :: [k]). c y => r ys -> r (y : ys)
    s (NS f xs -> r xs
    forall (ys :: [k]). All c ys => NS f ys -> r ys
    go NS f xs
    i)

    -- | Anamorphism for 'NS'.
    --
    -- @since 0.2.3.0
    --
    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
    ana_NS :: forall {k} (s :: [k] -> *) (f :: k -> *) (xs :: [k]).
    SListI xs =>
    (forall r. s '[] -> r)
    -> (forall (y :: k) (ys :: [k]). s (y : ys) -> Either (f y) (s ys))
    -> s xs
    -> NS f xs
    ana_NS forall r. s '[] -> r
    refute forall (y :: k) (ys :: [k]). s (y : ys) -> Either (f y) (s ys)
    decide =
      Proxy Top
    -> (forall r. s '[] -> r)
    -> (forall (y :: k) (ys :: [k]).
        Top y =>
        s (y : ys) -> Either (f y) (s ys))
    -> s xs
    -> NS f xs
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (s :: [k] -> *) (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> (forall r. s '[] -> r)
    -> (forall (y :: k) (ys :: [k]).
        c y =>
        s (y : ys) -> Either (f y) (s ys))
    -> s xs
    -> NS f xs
    cana_NS Proxy Top
    forall {k}. Proxy Top
    topP s '[] -> r
    forall r. s '[] -> r
    refute s (y : ys) -> Either (f y) (s ys)
    forall (y :: k) (ys :: [k]). s (y : ys) -> Either (f y) (s ys)
    forall (y :: k) (ys :: [k]).
    Top y =>
    s (y : ys) -> Either (f y) (s ys)
    decide
    {-# INLINE ana_NS #-}

    -- | Constrained anamorphism for 'NS'.
    --
    -- @since 0.2.3.0
    --
    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
    cana_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (s :: [k] -> *) (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> (forall r. s '[] -> r)
    -> (forall (y :: k) (ys :: [k]).
        c y =>
        s (y : ys) -> Either (f y) (s ys))
    -> s xs
    -> NS f xs
    cana_NS proxy c
    _ forall r. s '[] -> r
    refute forall (y :: k) (ys :: [k]).
    c y =>
    s (y : ys) -> Either (f y) (s ys)
    decide = SList xs -> s xs -> NS f xs
    forall (ys :: [k]). All c ys => SList ys -> s ys -> NS f ys
    go SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList
      where
        go :: forall ys . (All c ys) => SList ys -> s ys -> NS f ys
        go :: forall (ys :: [k]). All c ys => SList ys -> s ys -> NS f ys
    go SList ys
    SNil  s ys
    s = s '[] -> NS f ys
    forall r. s '[] -> r
    refute s ys
    s '[]
    s
        go SList ys
    SCons s ys
    s = case s (x : xs) -> Either (f x) (s xs)
    forall (y :: k) (ys :: [k]).
    c y =>
    s (y : ys) -> Either (f y) (s ys)
    decide s ys
    s (x : xs)
    s of
          Left f x
    x   -> f x -> NS f (x : xs)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z f x
    x
          Right s xs
    s' -> NS f xs -> NS f (x : xs)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (SList xs -> s xs -> NS f xs
    forall (ys :: [k]). All c ys => SList ys -> s ys -> NS f ys
    go SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList s xs
    s')

    -- * Expanding sums to products

    -- | Specialization of 'hexpand'.
    --
    -- @since 0.2.5.0
    --
    expand_NS :: forall f xs .
         (SListI xs)
      => (forall x . f x)
      -> NS f xs -> NP f xs
    expand_NS :: forall {k} (f :: k -> *) (xs :: [k]).
    SListI xs =>
    (forall (x :: k). f x) -> NS f xs -> NP f xs
    expand_NS forall (x :: k). f x
    d =
      Proxy Top -> (forall (x :: k). Top x => f x) -> NS f xs -> NP f xs
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
    cexpand_NS Proxy Top
    forall {k}. Proxy Top
    topP f x
    forall (x :: k). f x
    forall (x :: k). Top x => f x
    d
    {-# INLINE expand_NS #-}

    -- | Specialization of 'hcexpand'.
    --
    -- @since 0.2.5.0
    --
    cexpand_NS :: forall c proxy f xs .
         (All c xs)
      => proxy c -> (forall x . c x => f x)
      -> NS f xs -> NP f xs
    cexpand_NS :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
    cexpand_NS proxy c
    p forall (x :: k). c x => f x
    d = NS f xs -> NP f xs
    forall (ys :: [k]). All c ys => NS f ys -> NP f ys
    go
      where
        go :: forall ys . All c ys => NS f ys -> NP f ys
        go :: forall (ys :: [k]). All c ys => NS f ys -> NP f ys
    go (Z f x
    x) = f x
    x f x -> NP f xs -> NP f (x : xs)
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
    a x -> NP a xs -> NP a (x : xs)
    :* proxy c -> (forall (x :: k). c x => f x) -> NP f xs
    forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (HPure h, AllN h c xs) =>
    proxy c -> (forall (a :: k). c a => f a) -> h f xs
    forall (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    AllN NP c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    hcpure proxy c
    p f a
    forall (x :: k). c x => f x
    d
        go (S NS f xs
    i) = f x
    forall (x :: k). c x => f x
    d f x -> NP f xs -> NP f (x : xs)
    forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
    a x -> NP a xs -> NP a (x : xs)
    :* NS f xs -> NP f xs
    forall (ys :: [k]). All c ys => NS f ys -> NP f ys
    go NS f xs
    i

    -- | Specialization of 'hexpand'.
    --
    -- @since 0.2.5.0
    --
    expand_SOP :: forall f xss .
         (All SListI xss)
      => (forall x . f x)
      -> SOP f xss -> POP f xss
    expand_SOP :: forall {k} (f :: k -> *) (xss :: [[k]]).
    All SListI xss =>
    (forall (x :: k). f x) -> SOP f xss -> POP f xss
    expand_SOP forall (x :: k). f x
    d =
      Proxy Top
    -> (forall (x :: k). Top x => f x) -> SOP f xss -> POP f xss
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xss :: [[k]]).
    All2 c xss =>
    proxy c -> (forall (x :: k). c x => f x) -> SOP f xss -> POP f xss
    cexpand_SOP Proxy Top
    forall {k}. Proxy Top
    topP f x
    forall (x :: k). f x
    forall (x :: k). Top x => f x
    d
    {-# INLINE cexpand_SOP #-}

    -- | Specialization of 'hcexpand'.
    --
    -- @since 0.2.5.0
    --
    cexpand_SOP :: forall c proxy f xss .
         (All2 c xss)
      => proxy c -> (forall x . c x => f x)
      -> SOP f xss -> POP f xss
    cexpand_SOP :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xss :: [[k]]).
    All2 c xss =>
    proxy c -> (forall (x :: k). c x => f x) -> SOP f xss -> POP f xss
    cexpand_SOP proxy c
    p forall (x :: k). c x => f x
    d =
      NP (NP f) xss -> POP f xss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP (NP (NP f) xss -> POP f xss)
    -> (SOP f xss -> NP (NP f) xss) -> SOP f xss -> POP f xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy (All c)
    -> (forall (x :: [k]). All c x => NP f x)
    -> NS (NP f) xss
    -> NP (NP f) xss
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
    cexpand_NS (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p) (proxy c -> (forall (x :: k). c x => f x) -> NP f x
    forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (HPure h, AllN h c xs) =>
    proxy c -> (forall (a :: k). c a => f a) -> h f xs
    forall (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    AllN NP c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    hcpure proxy c
    p f a
    forall (x :: k). c x => f x
    d) (NS (NP f) xss -> NP (NP f) xss)
    -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> NP (NP f) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP f xss -> NS (NP f) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    allP :: proxy c -> Proxy (All c)
    allP :: forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    _ = Proxy (All c)
    forall {k} (t :: k). Proxy t
    Proxy

    instance HExpand NS where
      hexpand :: forall (xs :: [k]) (f :: k -> *).
    SListIN (Prod NS) xs =>
    (forall (x :: k). f x) -> NS f xs -> Prod NS f xs
    hexpand  = (forall (x :: k). f x) -> NS f xs -> Prod NS f xs
    (forall (x :: k). f x) -> NS f xs -> NP f xs
    forall {k} (f :: k -> *) (xs :: [k]).
    SListI xs =>
    (forall (x :: k). f x) -> NS f xs -> NP f xs
    expand_NS
      hcexpand :: forall (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    AllN (Prod NS) c xs =>
    proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs
    hcexpand = proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs
    proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
    cexpand_NS

    instance HExpand SOP where
      hexpand :: forall (xs :: [[k]]) (f :: k -> *).
    SListIN (Prod SOP) xs =>
    (forall (x :: k). f x) -> SOP f xs -> Prod SOP f xs
    hexpand  = (forall (x :: k). f x) -> SOP f xs -> Prod SOP f xs
    (forall (x :: k). f x) -> SOP f xs -> POP f xs
    forall {k} (f :: k -> *) (xss :: [[k]]).
    All SListI xss =>
    (forall (x :: k). f x) -> SOP f xss -> POP f xss
    expand_SOP
      hcexpand :: forall (c :: k -> Constraint) (xs :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    AllN (Prod SOP) c xs =>
    proxy c
    -> (forall (x :: k). c x => f x) -> SOP f xs -> Prod SOP f xs
    hcexpand = proxy c
    -> (forall (x :: k). c x => f x) -> SOP f xs -> Prod SOP f xs
    proxy c -> (forall (x :: k). c x => f x) -> SOP f xs -> POP f xs
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (f :: k -> *) (xss :: [[k]]).
    All2 c xss =>
    proxy c -> (forall (x :: k). c x => f x) -> SOP f xss -> POP f xss
    cexpand_SOP

    -- | Specialization of 'htrans'.
    --
    -- @since 0.3.1.0
    --
    trans_NS ::
         AllZip c xs ys
      => proxy c
      -> (forall x y . c x y => f x -> g y)
      -> NS f xs -> NS g ys
    trans_NS :: forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
           (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    AllZip c xs ys =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    trans_NS proxy c
    _ forall (x :: k) (y :: k). c x y => f x -> g y
    t (Z f x
    x)      = g (Head ys) -> NS g (Head ys : Tail ys)
    forall {k} (f :: k -> *) (xs :: k) (x :: [k]).
    f xs -> NS f (xs : x)
    Z (f x -> g (Head ys)
    forall (x :: k) (y :: k). c x y => f x -> g y
    t f x
    x)
    trans_NS proxy c
    p forall (x :: k) (y :: k). c x y => f x -> g y
    t (S NS f xs
    x)      = NS g (Tail ys) -> NS g (Head ys : Tail ys)
    forall {k} (f :: k -> *) (xs :: [k]) (x :: k).
    NS f xs -> NS f (x : xs)
    S (proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NS f xs
    -> NS g (Tail ys)
    forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
           (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    AllZip c xs ys =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    trans_NS proxy c
    p f x -> g y
    forall (x :: k) (y :: k). c x y => f x -> g y
    t NS f xs
    x)

    -- | Specialization of 'htrans'.
    --
    -- @since 0.3.1.0
    --
    trans_SOP ::
         AllZip2 c xss yss
      => proxy c
      -> (forall x y . c x y => f x -> g y)
      -> SOP f xss -> SOP g yss
    trans_SOP :: forall {k} {k} (c :: k -> k -> Constraint) (xss :: [[k]])
           (yss :: [[k]]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *)
           (g :: k -> *).
    AllZip2 c xss yss =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> SOP f xss
    -> SOP g yss
    trans_SOP proxy c
    p forall (x :: k) (y :: k). c x y => f x -> g y
    t =
      NS (NP g) yss -> SOP g yss
    forall k (f :: k -> *) (xss :: [[k]]). NS (NP f) xss -> SOP f xss
    SOP (NS (NP g) yss -> SOP g yss)
    -> (SOP f xss -> NS (NP g) yss) -> SOP f xss -> SOP g yss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy (AllZip c)
    -> (forall (x :: [k]) (y :: [k]). AllZip c x y => NP f x -> NP g y)
    -> NS (NP f) xss
    -> NS (NP g) yss
    forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
           (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    AllZip c xs ys =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    trans_NS (proxy c -> Proxy (AllZip c)
    forall {a} {b} (proxy :: (a -> b -> Constraint) -> *)
           (c :: a -> b -> Constraint).
    proxy c -> Proxy (AllZip c)
    allZipP proxy c
    p) (proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NP f x
    -> NP g y
    forall {k1} {k2} (c :: k1 -> k2 -> Constraint) (xs :: [k1])
           (ys :: [k2]) (proxy :: (k1 -> k2 -> Constraint) -> *)
           (f :: k1 -> *) (g :: k2 -> *).
    AllZip c xs ys =>
    proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> NP f xs
    -> NP g ys
    trans_NP proxy c
    p f x -> g y
    forall (x :: k) (y :: k). c x y => f x -> g y
    t) (NS (NP f) xss -> NS (NP g) yss)
    -> (SOP f xss -> NS (NP f) xss) -> SOP f xss -> NS (NP g) yss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SOP f xss -> NS (NP f) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). SOP f xss -> NS (NP f) xss
    unSOP

    allZipP :: proxy c -> Proxy (AllZip c)
    allZipP :: forall {a} {b} (proxy :: (a -> b -> Constraint) -> *)
           (c :: a -> b -> Constraint).
    proxy c -> Proxy (AllZip c)
    allZipP proxy c
    _ = Proxy (AllZip c)
    forall {k} (t :: k). Proxy t
    Proxy

    -- | Specialization of 'hcoerce'.
    --
    -- @since 0.3.1.0
    --
    coerce_NS ::
         forall f g xs ys .
         AllZip (LiftedCoercible f g) xs ys
      => NS f xs -> NS g ys
    coerce_NS :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
    AllZip (LiftedCoercible f g) xs ys =>
    NS f xs -> NS g ys
    coerce_NS =
      NS f xs -> NS g ys
    forall a b. a -> b
    unsafeCoerce

    -- | Safe version of 'coerce_NS'.
    --
    -- For documentation purposes only; not exported.
    --
    _safe_coerce_NS ::
         forall f g xs ys .
         AllZip (LiftedCoercible f g) xs ys
      => NS f xs -> NS g ys
    _safe_coerce_NS :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
    AllZip (LiftedCoercible f g) xs ys =>
    NS f xs -> NS g ys
    _safe_coerce_NS =
      Proxy (LiftedCoercible f g)
    -> (forall (x :: k) (y :: k).
        LiftedCoercible f g x y =>
        f x -> g y)
    -> NS f xs
    -> NS g ys
    forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
           (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    AllZip c xs ys =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    trans_NS (Proxy (LiftedCoercible f g)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (LiftedCoercible f g)) f x -> g y
    forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
    forall a b. Coercible a b => a -> b
    coerce

    -- | Specialization of 'hcoerce'.
    --
    -- @since 0.3.1.0
    --
    coerce_SOP ::
         forall f g xss yss .
         AllZip2 (LiftedCoercible f g) xss yss
      => SOP f xss -> SOP g yss
    coerce_SOP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]])
           (yss :: [[k]]).
    AllZip2 (LiftedCoercible f g) xss yss =>
    SOP f xss -> SOP g yss
    coerce_SOP =
      SOP f xss -> SOP g yss
    forall a b. a -> b
    unsafeCoerce

    -- | Safe version of 'coerce_SOP'.
    --
    -- For documentation purposes only; not exported.
    --
    _safe_coerce_SOP ::
         forall f g xss yss .
         AllZip2 (LiftedCoercible f g) xss yss
      => SOP f xss -> SOP g yss
    _safe_coerce_SOP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]])
           (yss :: [[k]]).
    AllZip2 (LiftedCoercible f g) xss yss =>
    SOP f xss -> SOP g yss
    _safe_coerce_SOP =
      Proxy (LiftedCoercible f g)
    -> (forall (x :: k) (y :: k).
        LiftedCoercible f g x y =>
        f x -> g y)
    -> SOP f xss
    -> SOP g yss
    forall {k} {k} (c :: k -> k -> Constraint) (xss :: [[k]])
           (yss :: [[k]]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *)
           (g :: k -> *).
    AllZip2 c xss yss =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> SOP f xss
    -> SOP g yss
    trans_SOP (Proxy (LiftedCoercible f g)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (LiftedCoercible f g)) f x -> g y
    forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
    forall a b. Coercible a b => a -> b
    coerce

    -- | Specialization of 'hfromI'.
    --
    -- @since 0.3.1.0
    --
    fromI_NS ::
         forall f xs ys .
         AllZip (LiftedCoercible I f) xs ys
      => NS I xs -> NS f ys
    fromI_NS :: forall {k} (f :: k -> *) (xs :: [*]) (ys :: [k]).
    AllZip (LiftedCoercible I f) xs ys =>
    NS I xs -> NS f ys
    fromI_NS = NS I xs -> NS f ys
    forall {l1} {k2} {l2} (h1 :: (* -> *) -> l1 -> *) (f :: k2 -> *)
           (xs :: l1) (ys :: l2) (h2 :: (k2 -> *) -> l2 -> *).
    (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) =>
    h1 I xs -> h2 f ys
    hfromI

    -- | Specialization of 'htoI'.
    --
    -- @since 0.3.1.0
    --
    toI_NS ::
         forall f xs ys .
         AllZip (LiftedCoercible f I) xs ys
      => NS f xs -> NS I ys
    toI_NS :: forall {k} (f :: k -> *) (xs :: [k]) (ys :: [*]).
    AllZip (LiftedCoercible f I) xs ys =>
    NS f xs -> NS I ys
    toI_NS = NS f xs -> NS I ys
    forall {k1} {l1} {l2} (h1 :: (k1 -> *) -> l1 -> *) (f :: k1 -> *)
           (xs :: l1) (ys :: l2) (h2 :: (* -> *) -> l2 -> *).
    (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) =>
    h1 f xs -> h2 I ys
    htoI

    -- | Specialization of 'hfromI'.
    --
    -- @since 0.3.1.0
    --
    fromI_SOP ::
         forall f xss yss .
         AllZip2 (LiftedCoercible I f) xss yss
      => SOP I xss -> SOP f yss
    fromI_SOP :: forall {k} (f :: k -> *) (xss :: [[*]]) (yss :: [[k]]).
    AllZip2 (LiftedCoercible I f) xss yss =>
    SOP I xss -> SOP f yss
    fromI_SOP = SOP I xss -> SOP f yss
    forall {l1} {k2} {l2} (h1 :: (* -> *) -> l1 -> *) (f :: k2 -> *)
           (xs :: l1) (ys :: l2) (h2 :: (k2 -> *) -> l2 -> *).
    (AllZipN (Prod h1) (LiftedCoercible I f) xs ys, HTrans h1 h2) =>
    h1 I xs -> h2 f ys
    hfromI

    -- | Specialization of 'htoI'.
    --
    -- @since 0.3.1.0
    --
    toI_SOP ::
         forall f xss yss .
         AllZip2 (LiftedCoercible f I) xss yss
      => SOP f xss -> SOP I yss
    toI_SOP :: forall {k} (f :: k -> *) (xss :: [[k]]) (yss :: [[*]]).
    AllZip2 (LiftedCoercible f I) xss yss =>
    SOP f xss -> SOP I yss
    toI_SOP = SOP f xss -> SOP I yss
    forall {k1} {l1} {l2} (h1 :: (k1 -> *) -> l1 -> *) (f :: k1 -> *)
           (xs :: l1) (ys :: l2) (h2 :: (* -> *) -> l2 -> *).
    (AllZipN (Prod h1) (LiftedCoercible f I) xs ys, HTrans h1 h2) =>
    h1 f xs -> h2 I ys
    htoI

    instance HTrans NS NS where
      htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2])
           (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *)
           (g :: k2 -> *).
    AllZipN (Prod NS) c xs ys =>
    proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    htrans  = proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    forall {k} {k} (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
           (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
    AllZip c xs ys =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NS f xs
    -> NS g ys
    trans_NS
      hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [k1]) (ys :: [k2]).
    AllZipN (Prod NS) (LiftedCoercible f g) xs ys =>
    NS f xs -> NS g ys
    hcoerce = NS f xs -> NS g ys
    forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
    AllZip (LiftedCoercible f g) xs ys =>
    NS f xs -> NS g ys
    coerce_NS

    instance HTrans SOP SOP where
      htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [[k1]]) (ys :: [[k2]])
           (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *)
           (g :: k2 -> *).
    AllZipN (Prod SOP) c xs ys =>
    proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> SOP f xs
    -> SOP g ys
    htrans  = proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> SOP f xs
    -> SOP g ys
    forall {k} {k} (c :: k -> k -> Constraint) (xss :: [[k]])
           (yss :: [[k]]) (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *)
           (g :: k -> *).
    AllZip2 c xss yss =>
    proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> SOP f xss
    -> SOP g yss
    trans_SOP
      hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [[k1]]) (ys :: [[k2]]).
    AllZipN (Prod SOP) (LiftedCoercible f g) xs ys =>
    SOP f xs -> SOP g ys
    hcoerce = SOP f xs -> SOP g ys
    forall {k} {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]])
           (yss :: [[k]]).
    AllZip2 (LiftedCoercible f g) xss yss =>
    SOP f xss -> SOP g yss
    coerce_SOP