    {-# LANGUAGE PolyKinds, StandaloneDeriving, UndecidableInstances #-}
    -- | n-ary products (and products of products)
    module Data.SOP.NP
      ( -- * Datatypes
        NP(..)
      , POP(..)
      , unPOP
        -- * Constructing products
      , pure_NP
      , pure_POP
      , cpure_NP
      , cpure_POP
        -- ** Construction from a list
      , fromList
        -- * Application
      , ap_NP
      , ap_POP
        -- * Destructing products
      , hd
      , tl
      , Projection
      , projections
      , shiftProjection
        -- * Lifting / mapping
      , liftA_NP
      , liftA_POP
      , liftA2_NP
      , liftA2_POP
      , liftA3_NP
      , liftA3_POP
      , map_NP
      , map_POP
      , zipWith_NP
      , zipWith_POP
      , zipWith3_NP
      , zipWith3_POP
      , cliftA_NP
      , cliftA_POP
      , cliftA2_NP
      , cliftA2_POP
      , cliftA3_NP
      , cliftA3_POP
      , cmap_NP
      , cmap_POP
      , czipWith_NP
      , czipWith_POP
      , czipWith3_NP
      , czipWith3_POP
        -- * Dealing with @'All' c@
      , hcliftA'
      , hcliftA2'
      , hcliftA3'
      , cliftA2'_NP
        -- * Collapsing
      , collapse_NP
      , collapse_POP
        -- * Folding and sequencing
      , ctraverse__NP
      , ctraverse__POP
      , traverse__NP
      , traverse__POP
      , cfoldMap_NP
      , cfoldMap_POP
      , sequence'_NP
      , sequence'_POP
      , sequence_NP
      , sequence_POP
      , ctraverse'_NP
      , ctraverse'_POP
      , traverse'_NP
      , traverse'_POP
      , ctraverse_NP
      , ctraverse_POP
        -- * Catamorphism and anamorphism
      , cata_NP
      , ccata_NP
      , ana_NP
      , cana_NP
        -- * Transformation of index lists and coercions
      , trans_NP
      , trans_POP
      , coerce_NP
      , coerce_POP
      , fromI_NP
      , fromI_POP
      , toI_NP
      , toI_POP
      ) where

    import Data.Coerce
    import Data.Kind (Type)
    import Data.Proxy (Proxy(..))
    import Unsafe.Coerce
    #if !MIN_VERSION_base(4,11,0)
    import Data.Semigroup (Semigroup (..))
    #endif

    import Control.DeepSeq (NFData(..))

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

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

    infixr 5 :*

    -- This is written manually,
    -- because built-in deriving doesn't use associativity information!
    instance All (Show `Compose` f) xs => Show (NP f xs) where
      showsPrec :: Int -> NP f xs -> ShowS
    showsPrec Int
    _ NP f xs
    Nil       = String -> ShowS
    showString String
    "Nil"
      showsPrec Int
    d (f x
    f :* NP f xs
    fs) = Bool -> ShowS -> ShowS
    showParen (Int
    d Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    5)
        (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ Int -> f x -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec (Int
    5 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) f x
    f
        ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString String
    " :* "
        ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> NP f xs -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    5 NP f xs
    fs

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

    -- | @since 0.4.0.0
    instance All (Semigroup `Compose` f) xs => Semigroup (NP f xs) where
      <> :: NP f xs -> NP f xs -> NP f xs
    (<>) = Proxy (Compose Semigroup f)
    -> (forall (a :: k). Compose Semigroup f a => f a -> f a -> f a)
    -> NP f xs
    -> NP f xs
    -> NP f xs
    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
    -> NP g xs
    -> NP h xs
    czipWith_NP (Proxy (Compose Semigroup f)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (Semigroup `Compose` f)) f a -> f a -> f a
    forall (a :: k). Compose Semigroup f a => f a -> f a -> f a
    forall a. Semigroup a => a -> a -> a
    (<>)

    -- | @since 0.4.0.0
    instance (All (Monoid `Compose` f) xs
    #if MIN_VERSION_base(4,11,0)
      , All (Semigroup `Compose` f) xs  -- GHC isn't smart enough to figure this out
    #endif
      ) => Monoid (NP f xs) where
      mempty :: NP f xs
    mempty  = Proxy (Compose Monoid f)
    -> (forall (a :: k). Compose Monoid f a => f a) -> NP f xs
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP (Proxy (Compose Monoid f)
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy (Monoid `Compose` f)) f a
    forall (a :: k). Compose Monoid f a => f a
    forall a. Monoid a => a
    mempty
    #if !MIN_VERSION_base(4,11,0)
      mappend = czipWith_NP (Proxy :: Proxy (Monoid `Compose` f)) mappend
    #endif

    -- | @since 0.2.5.0
    instance All (NFData `Compose` f) xs => NFData (NP f xs) where
        rnf :: NP f xs -> ()
    rnf NP f xs
    Nil       = ()
        rnf (f x
    x :* NP f xs
    xs) = f x -> ()
    forall a. NFData a => a -> ()
    rnf f x
    x () -> () -> ()
    forall a b. a -> b -> b
    `seq` NP f xs -> ()
    forall a. NFData a => a -> ()
    rnf NP f xs
    xs

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

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

    -- | @since 0.4.0.0
    instance (Semigroup (NP (NP f) xss)) => Semigroup (POP f xss) where
      POP NP (NP f) xss
    xss <> :: POP f xss -> POP f xss -> POP f xss
    <> POP NP (NP f) xss
    yss = 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
    xss NP (NP f) xss -> NP (NP f) xss -> NP (NP f) xss
    forall a. Semigroup a => a -> a -> a
    <> NP (NP f) xss
    yss)

    -- | @since 0.4.0.0
    instance (Monoid (NP (NP f) xss)) => Monoid (POP f xss) where
      mempty :: POP f xss
    mempty                      = 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
    forall a. Monoid a => a
    mempty
    #if !MIN_VERSION_base(4,11,0)
      mappend (POP xss) (POP yss) = POP (mappend xss yss)
    #endif

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

    -- | Unwrap a product of products.
    unPOP :: POP f xss -> NP (NP f) xss
    unPOP :: forall {k} (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
    unPOP (POP NP (NP f) xss
    xss) = NP (NP f) xss
    xss

    type instance AllN NP  c = All  c
    type instance AllN POP c = All2 c

    type instance AllZipN NP  c = AllZip  c
    type instance AllZipN POP c = AllZip2 c

    type instance SListIN NP  = SListI
    type instance SListIN POP = SListI2

    -- * Constructing products

    -- | Specialization of 'hpure'.
    --
    -- The call @'pure_NP' x@ generates a product that contains 'x' in every
    -- element position.
    --
    -- /Example:/
    --
    -- >>> pure_NP [] :: NP [] '[Char, Bool]
    -- "" :* [] :* Nil
    -- >>> pure_NP (K 0) :: NP (K Int) '[Double, Int, String]
    -- K 0 :* K 0 :* K 0 :* Nil
    --
    pure_NP :: forall f xs. SListI xs => (forall a. f a) -> NP f xs
    pure_NP :: forall {k} (f :: k -> *) (xs :: [k]).
    SListI xs =>
    (forall (a :: k). f a) -> NP f xs
    pure_NP forall (a :: k). f a
    f = Proxy Top -> (forall (a :: k). Top a => f a) -> NP f xs
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP Proxy Top
    forall {k}. Proxy Top
    topP f a
    forall (a :: k). f a
    forall (a :: k). Top a => f a
    f
    {-# INLINE pure_NP #-}

    -- | Specialization of 'hpure'.
    --
    -- The call @'pure_POP' x@ generates a product of products that contains 'x'
    -- in every element position.
    --
    pure_POP :: All SListI xss => (forall a. f a) -> POP f xss
    pure_POP :: forall {k} (xss :: [[k]]) (f :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a) -> POP f xss
    pure_POP forall (a :: k). f a
    f = Proxy Top -> (forall (a :: k). Top a => f a) -> POP f xss
    forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All2 c xss =>
    proxy c -> (forall (a :: k). c a => f a) -> POP f xss
    cpure_POP Proxy Top
    forall {k}. Proxy Top
    topP f a
    forall (a :: k). f a
    forall (a :: k). Top a => f a
    f
    {-# INLINE pure_POP #-}

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

    -- | Specialization of 'hcpure'.
    --
    -- The call @'cpure_NP' p x@ generates a product that contains 'x' in every
    -- element position.
    --
    cpure_NP :: forall c xs proxy f. All c xs
             => proxy c -> (forall a. c a => f a) -> NP f xs
    cpure_NP :: forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP proxy c
    p forall (a :: k). c a => f a
    f = case SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList :: SList xs of
      SList xs
    SNil   -> NP f xs
    NP f '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
      SList xs
    SCons  -> f x
    forall (a :: k). c a => f a
    f f x -> NP f xs -> NP f (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    :* proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP proxy c
    p f a
    forall (a :: k). c a => f a
    f

    -- | Specialization of 'hcpure'.
    --
    -- The call @'cpure_NP' p x@ generates a product of products that contains 'x'
    -- in every element position.
    --
    cpure_POP :: forall c xss proxy f. All2 c xss
              => proxy c -> (forall a. c a => f a) -> POP f xss
    cpure_POP :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All2 c xss =>
    proxy c -> (forall (a :: k). c a => f a) -> POP f xss
    cpure_POP proxy c
    p forall (a :: k). c a => f a
    f = NP (NP f) xss -> POP f xss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP (Proxy (All c)
    -> (forall (a :: [k]). All c a => NP f a) -> NP (NP f) xss
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP (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) -> NP f a
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP proxy c
    p f a
    forall (a :: k). c a => f a
    f))

    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 HPure NP where
      hpure :: forall (xs :: [k]) (f :: k -> *).
    SListIN NP xs =>
    (forall (a :: k). f a) -> NP f xs
    hpure  = (forall (a :: k). f a) -> NP f xs
    forall {k} (f :: k -> *) (xs :: [k]).
    SListI xs =>
    (forall (a :: k). f a) -> NP f xs
    pure_NP
      hcpure :: 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 -> (forall (a :: k). c a => f a) -> NP f xs
    forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> NP f xs
    cpure_NP

    instance HPure POP where
      hpure :: forall (xs :: [[k]]) (f :: k -> *).
    SListIN POP xs =>
    (forall (a :: k). f a) -> POP f xs
    hpure  = (forall (a :: k). f a) -> POP f xs
    forall {k} (xss :: [[k]]) (f :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a) -> POP f xss
    pure_POP
      hcpure :: forall (c :: k -> Constraint) (xs :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    AllN POP c xs =>
    proxy c -> (forall (a :: k). c a => f a) -> POP f xs
    hcpure = proxy c -> (forall (a :: k). c a => f a) -> POP f xs
    forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    All2 c xss =>
    proxy c -> (forall (a :: k). c a => f a) -> POP f xss
    cpure_POP

    -- ** Construction from a list

    -- | Construct a homogeneous n-ary product from a normal Haskell list.
    --
    -- Returns 'Nothing' if the length of the list does not exactly match the
    -- expected size of the product.
    --
    fromList :: SListI xs => [a] -> Maybe (NP (K a) xs)
    fromList :: forall {k} (xs :: [k]) a. SListI xs => [a] -> Maybe (NP (K a) xs)
    fromList = SList xs -> [a] -> Maybe (NP (K a) xs)
    forall {k} (xs :: [k]) a. SList xs -> [a] -> Maybe (NP (K a) xs)
    go SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList
      where
        go :: SList xs -> [a] -> Maybe (NP (K a) xs)
        go :: forall {k} (xs :: [k]) a. SList xs -> [a] -> Maybe (NP (K a) xs)
    go SList xs
    SNil  []     = NP (K a) xs -> Maybe (NP (K a) xs)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return NP (K a) xs
    NP (K a) '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
        go SList xs
    SCons (a
    x:[a]
    xs) = do ys <- SList xs -> [a] -> Maybe (NP (K a) xs)
    forall {k} (xs :: [k]) a. SList xs -> [a] -> Maybe (NP (K a) xs)
    go SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList [a]
    xs ; return (K x :* ys)
        go SList xs
    _     [a]
    _      = Maybe (NP (K a) xs)
    forall a. Maybe a
    Nothing

    -- * Application

    -- | Specialization of 'hap'.
    --
    -- Applies a product of (lifted) functions pointwise to a product of
    -- suitable arguments.
    --
    ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
    ap_NP :: forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NP f xs -> NP g xs
    ap_NP NP (f -.-> g) xs
    Nil           NP f xs
    Nil        = NP g xs
    NP g '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
    ap_NP (Fn f x -> g x
    f :* NP (f -.-> g) xs
    fs)  (f x
    x :* NP f xs
    xs)  = f x -> g x
    f f x
    f x
    x g x -> NP g xs -> NP g (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    :* NP (f -.-> g) xs -> NP f xs -> NP g xs
    forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NP f xs -> NP g xs
    ap_NP NP (f -.-> g) xs
    fs NP f xs
    NP f xs
    xs

    -- | Specialization of 'hap'.
    --
    -- Applies a product of (lifted) functions pointwise to a product of
    -- suitable arguments.
    --
    ap_POP :: POP (f -.-> g) xss -> POP f xss -> POP g xss
    ap_POP :: forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    POP (f -.-> g) xss -> POP f xss -> POP g xss
    ap_POP (POP NP (NP (f -.-> g)) xss
    fss') (POP NP (NP f) xss
    xss') = NP (NP g) xss -> POP g xss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP (NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
    forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
    go NP (NP (f -.-> g)) xss
    fss' NP (NP f) xss
    xss')
      where
        go :: NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
        go :: forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
    go NP (NP (f -.-> g)) xss
    Nil         NP (NP f) xss
    Nil         = NP (NP g) xss
    NP (NP g) '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
        go (NP (f -.-> g) x
    fs :* NP (NP (f -.-> g)) xs
    fss) (NP f x
    xs :* NP (NP f) xs
    xss) = 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 NP g x -> NP (NP g) xs -> NP (NP g) (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    :* NP (NP (f -.-> g)) xs -> NP (NP f) xs -> NP (NP g) xs
    forall {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]]).
    NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) xss
    go NP (NP (f -.-> g)) xs
    fss NP (NP f) xs
    NP (NP f) xs
    xss

    -- The definition of 'ap_POP' is a more direct variant of
    -- '_ap_POP_spec'. The direct definition has the advantage
    -- that it avoids the 'SListI' constraint.
    _ap_POP_spec :: SListI xss => POP (f -.-> g) xss -> POP  f xss -> POP  g xss
    _ap_POP_spec :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *).
    SListI xss =>
    POP (f -.-> g) xss -> POP f xss -> POP g xss
    _ap_POP_spec (POP NP (NP (f -.-> g)) xss
    fs) (POP NP (NP f) xss
    xs) = NP (NP g) xss -> POP g xss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP ((forall (a :: [k]). NP (f -.-> g) a -> NP f a -> NP g a)
    -> NP (NP (f -.-> g)) xss -> NP (NP f) xss -> NP (NP g) 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 -> NP g xs -> NP h xs
    liftA2_NP NP (f -.-> g) a -> NP f a -> NP g a
    forall (a :: [k]). NP (f -.-> g) a -> NP f a -> NP g a
    forall {k} (f :: k -> *) (g :: k -> *) (xs :: [k]).
    NP (f -.-> g) xs -> NP f xs -> NP g xs
    ap_NP NP (NP (f -.-> g)) xss
    fs NP (NP f) xss
    xs)

    type instance Same NP  = NP
    type instance Same POP = POP

    type instance Prod NP  = NP
    type instance Prod POP = POP

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

    -- * Destructing products

    -- | Obtain the head of an n-ary product.
    --
    -- @since 0.2.1.0
    --
    hd :: NP f (x ': xs) -> f x
    hd :: forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
    hd (f x
    x :* NP f xs
    _xs) = f x
    f x
    x

    -- | Obtain the tail of an n-ary product.
    --
    -- @since 0.2.1.0
    --
    tl :: NP f (x ': xs) -> NP f xs
    tl :: forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    NP f (x : xs) -> NP f xs
    tl (f x
    _x :* NP f xs
    xs) = NP f xs
    NP f xs
    xs

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

    -- | Compute all projections from an n-ary product.
    --
    -- Each element of the resulting product contains one of the projections.
    --
    projections :: forall xs f . SListI xs => NP (Projection f xs) xs
    projections :: forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Projection f xs) xs
    projections = case SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList :: SList xs of
      SList xs
    SNil  -> NP (Projection f xs) xs
    NP (Projection f xs) '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
      SList xs
    SCons -> (K (NP f xs) x -> f x) -> (-.->) (K (NP f xs)) f x
    forall {k} (f :: k -> *) (a :: k) (f' :: k -> *).
    (f a -> f' a) -> (-.->) f f' a
    fn (NP f (x : xs) -> f x
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
    hd (NP f (x : xs) -> f x)
    -> (K (NP f xs) x -> NP f (x : xs)) -> K (NP f xs) x -> f x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K (NP f xs) x -> NP f xs
    K (NP f xs) x -> NP f (x : xs)
    forall {k} a (b :: k). K a b -> a
    unK) (-.->) (K (NP f xs)) f x
    -> NP (Projection f xs) xs -> NP (Projection f xs) (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    :* (forall (a :: k). Projection f xs a -> Projection f xs a)
    -> NP (Projection f xs) xs -> NP (Projection 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 (NP f xs)) f a -> (-.->) (K (NP f xs)) f a
    (-.->) (K (NP f xs)) f a -> Projection f (x : xs) a
    forall (a :: k). Projection f xs a -> Projection f xs a
    forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
    Projection f xs a -> Projection f (x : xs) a
    shiftProjection NP (Projection f xs) xs
    forall {k} (xs :: [k]) (f :: k -> *).
    SListI xs =>
    NP (Projection f xs) xs
    projections

    shiftProjection :: Projection f xs a -> Projection f (x ': xs) a
    shiftProjection :: forall {a} (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
    Projection f xs a -> Projection f (x : xs) a
    shiftProjection (Fn K (NP f xs) a -> f a
    f) = (K (NP f (x : xs)) a -> f a) -> (-.->) (K (NP f (x : xs))) f a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    (f a -> g a) -> (-.->) f g a
    Fn ((K (NP f (x : xs)) a -> f a) -> (-.->) (K (NP f (x : xs))) f a)
    -> (K (NP f (x : xs)) a -> f a) -> (-.->) (K (NP f (x : xs))) f a
    forall a b. (a -> b) -> a -> b
    $ K (NP f xs) a -> f a
    f (K (NP f xs) a -> f a)
    -> (K (NP f (x : xs)) a -> K (NP f xs) a)
    -> K (NP f (x : xs)) a
    -> f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP f xs -> K (NP f xs) a
    forall k a (b :: k). a -> K a b
    K (NP f xs -> K (NP f xs) a)
    -> (K (NP f (x : xs)) a -> NP f xs)
    -> K (NP f (x : xs)) a
    -> K (NP f xs) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP f (x : xs) -> NP f xs
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    NP f (x : xs) -> NP f xs
    tl (NP f (x : xs) -> NP f xs)
    -> (K (NP f (x : xs)) a -> NP f (x : xs))
    -> K (NP f (x : xs)) a
    -> NP f xs
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K (NP f (x : xs)) a -> NP f (x : xs)
    forall {k} a (b :: k). K a b -> a
    unK

    -- * Lifting / mapping

    -- | Specialization of 'hliftA'.
    liftA_NP  :: SListI     xs  => (forall a. f a -> g a) -> NP  f xs  -> NP  g xs
    -- | Specialization of 'hliftA'.
    liftA_POP :: All SListI xss => (forall a. f a -> g a) -> POP f xss -> POP g xss

    liftA_NP :: 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  = (forall (a :: k). f a -> g a) -> NP f xs -> NP 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_POP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss
    liftA_POP = (forall (a :: k). f a -> g a) -> POP f xss -> POP 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_NP  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
    -- | Specialization of 'hliftA2'.
    liftA2_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss

    liftA2_NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NP g xs -> NP h xs
    liftA2_NP  = (forall (a :: k). f a -> g a -> h a)
    -> Prod NP f xs -> NP g xs -> NP h xs
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NP g xs -> NP 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_POP :: 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 -> POP g xss -> POP h xss
    liftA2_POP = (forall (a :: k). f a -> g a -> h a)
    -> Prod POP f xss -> POP g xss -> POP h xss
    (forall (a :: k). f a -> g a -> h a)
    -> POP f xss -> POP g xss -> POP 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 'hliftA3'.
    liftA3_NP  :: SListI     xs  => (forall a. f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
    -- | Specialization of 'hliftA3'.
    liftA3_POP :: All SListI xss => (forall a. f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

    liftA3_NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (i :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> NP f xs -> NP g xs -> NP h xs -> NP i xs
    liftA3_NP  = (forall (a :: k). f a -> g a -> h a -> i a)
    -> Prod NP f xs -> Prod NP g xs -> NP h xs -> NP i xs
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> NP f xs -> NP g xs -> NP h xs -> NP i xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
    (SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
    (forall (a :: k). f a -> f' a -> f'' a -> f''' a)
    -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
    hliftA3
    liftA3_POP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (i :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> POP f xss -> POP g xss -> POP h xss -> POP i xss
    liftA3_POP = (forall (a :: k). f a -> g a -> h a -> i a)
    -> Prod POP f xss -> Prod POP g xss -> POP h xss -> POP i xss
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> POP f xss -> POP g xss -> POP h xss -> POP i xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
    (SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
    (forall (a :: k). f a -> f' a -> f'' a -> f''' a)
    -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
    hliftA3

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

    map_NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a) -> NP f xs -> NP g xs
    map_NP  = (forall (a :: k). f a -> g a) -> NP f xs -> NP 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_POP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a) -> POP f xss -> POP g xss
    map_POP = (forall (a :: k). f a -> g a) -> POP f xss -> POP 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 'hzipWith', which is equivalent to 'hliftA2'.
    zipWith_NP  :: SListI     xs  => (forall a. f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP   h xs
    -- | Specialization of 'hzipWith', which is equivalent to 'hliftA2'.
    zipWith_POP :: All SListI xss => (forall a. f a -> g a -> h a) -> POP f xss -> POP g xss -> POP  h xss

    zipWith_NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NP g xs -> NP h xs
    zipWith_NP  = (forall (a :: k). f a -> g a -> h a)
    -> Prod NP f xs -> NP g xs -> NP h xs
    (forall (a :: k). f a -> g a -> h a)
    -> NP f xs -> NP g xs -> NP 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
    hzipWith
    zipWith_POP :: 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 -> POP g xss -> POP h xss
    zipWith_POP = (forall (a :: k). f a -> g a -> h a)
    -> Prod POP f xss -> POP g xss -> POP h xss
    (forall (a :: k). f a -> g a -> h a)
    -> POP f xss -> POP g xss -> POP 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
    hzipWith

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

    zipWith3_NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (i :: k -> *).
    SListI xs =>
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> NP f xs -> NP g xs -> NP h xs -> NP i xs
    zipWith3_NP  = (forall (a :: k). f a -> g a -> h a -> i a)
    -> Prod NP f xs -> Prod NP g xs -> NP h xs -> NP i xs
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> NP f xs -> NP g xs -> NP h xs -> NP i xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
    (SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
    (forall (a :: k). f a -> f' a -> f'' a -> f''' a)
    -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
    hzipWith3
    zipWith3_POP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: k -> *) (h :: k -> *)
           (i :: k -> *).
    All SListI xss =>
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> POP f xss -> POP g xss -> POP h xss -> POP i xss
    zipWith3_POP = (forall (a :: k). f a -> g a -> h a -> i a)
    -> Prod POP f xss -> Prod POP g xss -> POP h xss -> POP i xss
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> POP f xss -> POP g xss -> POP h xss -> POP i xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
           (f' :: k -> *) (f'' :: k -> *) (f''' :: k -> *).
    (SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
    (forall (a :: k). f a -> f' a -> f'' a -> f''' a)
    -> Prod h f xs -> Prod h f' xs -> h f'' xs -> h f''' xs
    hzipWith3

    -- | Specialization of 'hcliftA'.
    cliftA_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
    -- | Specialization of 'hcliftA'.
    cliftA_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss

    cliftA_NP :: 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) -> NP f xs -> NP g xs
    cliftA_NP  = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP 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_POP :: 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) -> POP f xss -> POP g xss
    cliftA_POP = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP 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_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a) -> NP  f xs  -> NP  g xs  -> NP  h xs
    -- | Specialization of 'hcliftA2'.
    cliftA2_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a) -> POP f xss -> POP g xss -> POP h xss

    cliftA2_NP :: 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
    -> NP g xs
    -> NP h xs
    cliftA2_NP  = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> Prod NP f xs
    -> NP g xs
    -> NP h xs
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> NP f xs
    -> NP g xs
    -> NP 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_POP :: 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
    -> POP g xss
    -> POP h xss
    cliftA2_POP = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> Prod POP f xss
    -> POP g xss
    -> POP h xss
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> POP f xss
    -> POP g xss
    -> POP 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 'hcliftA3'.
    cliftA3_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> NP  f xs  -> NP  g xs  -> NP  h xs  -> NP  i xs
    -- | Specialization of 'hcliftA3'.
    cliftA3_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a -> h a -> i a) -> POP f xss -> POP g xss -> POP h xss -> POP i xss

    cliftA3_NP :: forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *) (i :: k -> *).
    All c xs =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> NP f xs
    -> NP g xs
    -> NP h xs
    -> NP i xs
    cliftA3_NP  = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> Prod NP f xs
    -> Prod NP g xs
    -> NP h xs
    -> NP i xs
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> NP f xs
    -> NP g xs
    -> NP h xs
    -> NP i xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (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 -> f''' a)
    -> Prod h f xs
    -> Prod h f' xs
    -> h f'' xs
    -> h f''' xs
    hcliftA3
    cliftA3_POP :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *) (i :: k -> *).
    All2 c xss =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> POP f xss
    -> POP g xss
    -> POP h xss
    -> POP i xss
    cliftA3_POP = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> Prod POP f xss
    -> Prod POP g xss
    -> POP h xss
    -> POP i xss
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> POP f xss
    -> POP g xss
    -> POP h xss
    -> POP i xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (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 -> f''' a)
    -> Prod h f xs
    -> Prod h f' xs
    -> h f'' xs
    -> h f''' xs
    hcliftA3

    -- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
    cmap_NP  :: All  c xs  => proxy c -> (forall a. c a => f a -> g a) -> NP   f xs  -> NP  g xs
    -- | Specialization of 'hcmap', which is equivalent to 'hcliftA'.
    cmap_POP :: All2 c xss => proxy c -> (forall a. c a => f a -> g a) -> POP  f xss -> POP g xss

    cmap_NP :: 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) -> NP f xs -> NP g xs
    cmap_NP  = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> NP f xs -> NP 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_POP :: 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) -> POP f xss -> POP g xss
    cmap_POP = proxy c
    -> (forall (a :: k). c a => f a -> g a) -> POP f xss -> POP 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

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

    czipWith_NP :: 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
    -> NP g xs
    -> NP h xs
    czipWith_NP  = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> Prod NP f xs
    -> NP g xs
    -> NP h xs
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> NP f xs
    -> NP g xs
    -> NP 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
    hczipWith
    czipWith_POP :: 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
    -> POP g xss
    -> POP h xss
    czipWith_POP = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> Prod POP f xss
    -> POP g xss
    -> POP h xss
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a)
    -> POP f xss
    -> POP g xss
    -> POP 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
    hczipWith

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

    czipWith3_NP :: forall {k} (c :: k -> Constraint) (xs :: [k])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *) (i :: k -> *).
    All c xs =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> NP f xs
    -> NP g xs
    -> NP h xs
    -> NP i xs
    czipWith3_NP  = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> Prod NP f xs
    -> Prod NP g xs
    -> NP h xs
    -> NP i xs
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> NP f xs
    -> NP g xs
    -> NP h xs
    -> NP i xs
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (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 -> f''' a)
    -> Prod h f xs
    -> Prod h f' xs
    -> h f'' xs
    -> h f''' xs
    hczipWith3
    czipWith3_POP :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *) (i :: k -> *).
    All2 c xss =>
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> POP f xss
    -> POP g xss
    -> POP h xss
    -> POP i xss
    czipWith3_POP = proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> Prod POP f xss
    -> Prod POP g xss
    -> POP h xss
    -> POP i xss
    proxy c
    -> (forall (a :: k). c a => f a -> g a -> h a -> i a)
    -> POP f xss
    -> POP g xss
    -> POP h xss
    -> POP i xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (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 -> f''' a)
    -> Prod h f xs
    -> Prod h f' xs
    -> h f'' xs
    -> h f''' xs
    hczipWith3

    -- * Dealing with @'All' c@

    -- | Lift a constrained function operating on a list-indexed structure
    -- to a function on a list-of-list-indexed structure.
    --
    -- This is a variant of 'hcliftA'.
    --
    -- /Specification:/
    --
    -- @
    -- 'hcliftA'' p f xs = 'hpure' ('fn_2' $ \\ 'AllDictC' -> f) \` 'hap' \` 'allDict_NP' p \` 'hap' \` xs
    -- @
    --
    -- /Instances:/
    --
    -- @
    -- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'NP' f xss -> 'NP' f' xss
    -- 'hcliftA'' :: 'All2' c xss => proxy c -> (forall xs. 'All' c xs => f xs -> f' xs) -> 'Data.SOP.NS.NS' f xss -> 'Data.SOP.NS.NS' f' xss
    -- @
    --
    {-# DEPRECATED hcliftA' "Use 'hcliftA' or 'hcmap' instead." #-}
    hcliftA'  :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs)                                                       -> h f   xss -> h f'   xss

    -- | Like 'hcliftA'', but for binary functions.
    {-# DEPRECATED hcliftA2' "Use 'hcliftA2' or 'hczipWith' instead." #-}
    hcliftA2' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs)            -> Prod h f xss                  -> h f'  xss -> h f''  xss

    -- | Like 'hcliftA'', but for ternary functions.
    {-# DEPRECATED hcliftA3' "Use 'hcliftA3' or 'hczipWith3' instead." #-}
    hcliftA3' :: (All2 c xss, Prod h ~ NP, HAp h) => proxy c -> (forall xs. All c xs => f xs -> f' xs -> f'' xs -> f''' xs) -> Prod h f xss -> Prod h f' xss -> h f'' xss -> h f''' xss

    hcliftA' :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (h :: ([k] -> *) -> [[k]] -> *) (proxy :: (k -> Constraint) -> *)
           (f :: [k] -> *) (f' :: [k] -> *).
    (All2 c xss, Prod h ~ NP, HAp h) =>
    proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> f' xs)
    -> h f xss
    -> h f' xss
    hcliftA'  proxy c
    p = Proxy (All c)
    -> (forall (xs :: [k]). All c xs => f xs -> f' xs)
    -> h f xss
    -> h f' 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  (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p)
    hcliftA2' :: 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' proxy c
    p = Proxy (All c)
    -> (forall (xs :: [k]). All c xs => f xs -> f' xs -> f'' xs)
    -> Prod h f xss
    -> h f' xss
    -> h f'' 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 (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p)
    hcliftA3' :: forall {k} (c :: k -> Constraint) (xss :: [[k]])
           (h :: ([k] -> *) -> [[k]] -> *) (proxy :: (k -> Constraint) -> *)
           (f :: [k] -> *) (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 -> f''' xs)
    -> Prod h f xss
    -> Prod h f' xss
    -> h f'' xss
    -> h f''' xss
    hcliftA3' proxy c
    p = Proxy (All c)
    -> (forall (xs :: [k]).
        All c xs =>
        f xs -> f' xs -> f'' xs -> f''' xs)
    -> Prod h f xss
    -> Prod h f' xss
    -> h f'' xss
    -> h f''' xss
    forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
           (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
           (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 -> f''' a)
    -> Prod h f xs
    -> Prod h f' xs
    -> h f'' xs
    -> h f''' xs
    hcliftA3 (proxy c -> Proxy (All c)
    forall {k} (proxy :: (k -> Constraint) -> *)
           (c :: k -> Constraint).
    proxy c -> Proxy (All c)
    allP proxy c
    p)

    -- | Specialization of 'hcliftA2''.
    {-# DEPRECATED cliftA2'_NP "Use 'cliftA2_NP'  instead." #-}
    cliftA2'_NP :: All2 c xss => proxy c -> (forall xs. All c xs => f xs -> g xs -> h xs) -> NP f xss -> NP g xss -> NP h xss

    cliftA2'_NP :: 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
    -> NP g xss
    -> NP h xss
    cliftA2'_NP = proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
    -> Prod NP f xss
    -> NP g xss
    -> NP h xss
    proxy c
    -> (forall (xs :: [k]). All c xs => f xs -> g xs -> h xs)
    -> NP f xss
    -> NP g xss
    -> NP 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'

    -- * Collapsing

    -- | Specialization of 'hcollapse'.
    --
    -- /Example:/
    --
    -- >>> collapse_NP (K 1 :* K 2 :* K 3 :* Nil)
    -- [1,2,3]
    --
    collapse_NP  ::              NP  (K a) xs  ->  [a]

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

    collapse_NP :: forall {k} a (xs :: [k]). NP (K a) xs -> [a]
    collapse_NP NP (K a) xs
    Nil         = []
    collapse_NP (K a
    x :* NP (K a) xs
    xs) = a
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : NP (K a) xs -> [a]
    forall {k} a (xs :: [k]). NP (K a) xs -> [a]
    collapse_NP NP (K a) xs
    xs

    collapse_POP :: forall {k} (xss :: [[k]]) a. SListI xss => POP (K a) xss -> [[a]]
    collapse_POP = NP (K [a]) xss -> [[a]]
    forall {k} a (xs :: [k]). NP (K a) xs -> [a]
    collapse_NP (NP (K [a]) xss -> [[a]])
    -> (POP (K a) xss -> NP (K [a]) xss) -> POP (K a) xss -> [[a]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (a :: [k]). NP (K a) a -> K [a] a)
    -> NP (NP (K a)) xss -> NP (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) (NP (NP (K a)) xss -> NP (K [a]) xss)
    -> (POP (K a) xss -> NP (NP (K a)) xss)
    -> POP (K a) xss
    -> NP (K [a]) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . POP (K a) xss -> NP (NP (K a)) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
    unPOP

    type instance CollapseTo NP  a = [a]
    type instance CollapseTo POP a = [[a]]

    instance HCollapse NP  where hcollapse :: forall (xs :: [k]) a.
    SListIN NP xs =>
    NP (K a) xs -> CollapseTo NP a
    hcollapse = NP (K a) xs -> [a]
    NP (K a) xs -> CollapseTo NP a
    forall {k} a (xs :: [k]). NP (K a) xs -> [a]
    collapse_NP
    instance HCollapse POP where hcollapse :: forall (xs :: [[k]]) a.
    SListIN POP xs =>
    POP (K a) xs -> CollapseTo POP a
    hcollapse = POP (K a) xs -> [[a]]
    POP (K a) xs -> CollapseTo POP a
    forall {k} (xss :: [[k]]) a. SListI xss => POP (K a) xss -> [[a]]
    collapse_POP

    -- * Folding

    -- | Specialization of 'hctraverse_'.
    --
    -- @since 0.3.2.0
    --
    ctraverse__NP ::
         forall c proxy xs f g. (All c xs, Applicative g)
      => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g ()
    ctraverse__NP :: 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
    _ forall (a :: k). c a => f a -> g ()
    f = NP f xs -> g ()
    forall (ys :: [k]). All c ys => NP f ys -> g ()
    go
      where
        go :: All c ys => NP f ys -> g ()
        go :: forall (ys :: [k]). All c ys => NP f ys -> g ()
    go NP f ys
    Nil       = () -> g ()
    forall a. a -> g a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        go (f x
    x :* NP f xs
    xs) = f x -> g ()
    forall (a :: k). c a => f a -> g ()
    f f x
    x g () -> g () -> g ()
    forall a b. g a -> g b -> g b
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> NP f xs -> g ()
    forall (ys :: [k]). All c ys => NP f ys -> g ()
    go NP f xs
    xs

    -- | Specialization of 'htraverse_'.
    --
    -- @since 0.3.2.0
    --
    traverse__NP ::
         forall xs f g. (SListI xs, Applicative g)
      => (forall a. f a -> g ()) -> NP f xs -> g ()
    traverse__NP :: forall {k} (xs :: [k]) (f :: k -> *) (g :: * -> *).
    (SListI xs, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
    traverse__NP forall (a :: k). f a -> g ()
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g ()) -> NP f xs -> 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 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__NP #-}

    -- | Specialization of 'hctraverse_'.
    --
    -- @since 0.3.2.0
    --
    ctraverse__POP ::
         forall c proxy xss f g. (All2 c xss, Applicative g)
      => proxy c -> (forall a. c a => f a -> g ()) -> POP f xss -> g ()
    ctraverse__POP :: 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 ()) -> POP f xss -> g ()
    ctraverse__POP 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 ())
    -> NP (NP f) xss
    -> 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 -> 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) (NP (NP f) xss -> g ())
    -> (POP f xss -> NP (NP f) xss) -> POP f xss -> g ()
    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

    -- | Specialization of 'htraverse_'.
    --
    -- @since 0.3.2.0
    --
    traverse__POP ::
         forall xss f g. (SListI2 xss, Applicative g)
      => (forall a. f a -> g ()) -> POP f xss -> g ()
    traverse__POP :: forall {k} (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> POP f xss -> g ()
    traverse__POP forall (a :: k). f a -> g ()
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g ()) -> POP 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 ()) -> POP f xss -> g ()
    ctraverse__POP 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__POP #-}

    instance HTraverse_ NP  where
      hctraverse_ :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (AllN NP c xs, Applicative g) =>
    proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
    hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> 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
      htraverse_ :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *).
    (SListIN NP xs, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
    htraverse_  = (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
    forall {k} (xs :: [k]) (f :: k -> *) (g :: * -> *).
    (SListI xs, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
    traverse__NP

    instance HTraverse_ POP where
      hctraverse_ :: forall (c :: k -> Constraint) (xs :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (AllN POP c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> POP f xs -> g ()
    hctraverse_ = proxy c
    -> (forall (a :: k). c a => f a -> g ()) -> POP 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 ()) -> POP f xss -> g ()
    ctraverse__POP
      htraverse_ :: forall (xs :: [[k]]) (g :: * -> *) (f :: k -> *).
    (SListIN POP xs, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> POP f xs -> g ()
    htraverse_  = (forall (a :: k). f a -> g ()) -> POP f xs -> g ()
    forall {k} (xss :: [[k]]) (f :: k -> *) (g :: * -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g ()) -> POP f xss -> g ()
    traverse__POP

    -- | Specialization of 'hcfoldMap'.
    --
    -- @since 0.3.2.0
    --
    cfoldMap_NP :: (All c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> NP f xs -> m
    cfoldMap_NP :: forall {k} (c :: k -> Constraint) (xs :: [k]) m
           (proxy :: (k -> Constraint) -> *) (f :: k -> *).
    (All c xs, Monoid m) =>
    proxy c -> (forall (a :: k). c a => f a -> m) -> NP f xs -> m
    cfoldMap_NP  = proxy c -> (forall (a :: k). c a => f a -> m) -> NP 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

    -- | Specialization of 'hcfoldMap'.
    --
    -- @since 0.3.2.0
    --
    cfoldMap_POP :: (All2 c xs, Monoid m) => proxy c -> (forall a. c a => f a -> m) -> POP f xs -> m
    cfoldMap_POP :: 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) -> POP f xs -> m
    cfoldMap_POP = proxy c -> (forall (a :: k). c a => f a -> m) -> POP 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'_NP  ::              Applicative f  => NP  (f :.: g) xs  -> f (NP  g xs)
    sequence'_NP :: forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NP (f :.: g) xs -> f (NP g xs)
    sequence'_NP NP (f :.: g) xs
    Nil         = NP g xs -> f (NP g xs)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure NP g xs
    NP g '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
    sequence'_NP ((:.:) f g x
    mx :* NP (f :.: g) xs
    mxs) = g x -> NP g xs -> NP g xs
    g x -> NP g xs -> NP g (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    (:*) (g x -> NP g xs -> NP g xs) -> f (g x) -> f (NP g xs -> NP 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 f (NP g xs -> NP g xs) -> f (NP g xs) -> f (NP g xs)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NP (f :.: g) xs -> f (NP g xs)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NP (f :.: g) xs -> f (NP g xs)
    sequence'_NP NP (f :.: g) xs
    mxs

    -- | Specialization of 'hsequence''.
    sequence'_POP :: (SListI xss, Applicative f) => POP (f :.: g) xss -> f (POP g xss)
    sequence'_POP :: forall {k} (xss :: [[k]]) (f :: * -> *) (g :: k -> *).
    (SListI xss, Applicative f) =>
    POP (f :.: g) xss -> f (POP g xss)
    sequence'_POP = (NP (NP g) xss -> POP g xss) -> f (NP (NP g) xss) -> f (POP g xss)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NP (NP g) xss -> POP g xss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP (f (NP (NP g) xss) -> f (POP g xss))
    -> (POP (f :.: g) xss -> f (NP (NP g) xss))
    -> POP (f :.: g) xss
    -> f (POP g xss)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NP (f :.: NP g) xss -> f (NP (NP g) xss)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NP (f :.: g) xs -> f (NP g xs)
    sequence'_NP (NP (f :.: NP g) xss -> f (NP (NP g) xss))
    -> (POP (f :.: g) xss -> NP (f :.: NP g) xss)
    -> POP (f :.: g) xss
    -> f (NP (NP g) xss)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall (a :: [k]). NP (f :.: g) a -> (:.:) f (NP g) a)
    -> NP (NP (f :.: g)) xss -> NP (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) (NP (NP (f :.: g)) xss -> NP (f :.: NP g) xss)
    -> (POP (f :.: g) xss -> NP (NP (f :.: g)) xss)
    -> POP (f :.: g) xss
    -> NP (f :.: NP g) xss
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . POP (f :.: g) xss -> NP (NP (f :.: g)) xss
    forall {k} (f :: k -> *) (xss :: [[k]]). POP f xss -> NP (NP f) xss
    unPOP

    -- | Specialization of 'hctraverse''.
    --
    -- @since 0.3.2.0
    --
    ctraverse'_NP  ::
         forall c proxy xs f f' g. (All c xs,  Applicative g)
      => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs  -> g (NP f' xs)
    ctraverse'_NP :: 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
    _ forall (a :: k). c a => f a -> g (f' a)
    f = NP f xs -> g (NP f' xs)
    forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
    go where
      go :: All c ys => NP f ys -> g (NP f' ys)
      go :: forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
    go NP f ys
    Nil       = NP f' ys -> g (NP f' ys)
    forall a. a -> g a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure NP f' ys
    NP f' '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
      go (f x
    x :* NP f xs
    xs) = f' x -> NP f' xs -> NP f' ys
    f' x -> NP f' xs -> NP f' (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    (:*) (f' x -> NP f' xs -> NP f' ys)
    -> g (f' x) -> g (NP f' xs -> NP 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 g (NP f' xs -> NP f' ys) -> g (NP f' xs) -> g (NP f' ys)
    forall a b. g (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NP f xs -> g (NP f' xs)
    forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
    go NP f xs
    xs

    -- | Specialization of 'htraverse''.
    --
    -- @since 0.3.2.0
    --
    traverse'_NP  ::
         forall xs f f' g. (SListI xs,  Applicative g)
      => (forall a. f a -> g (f' a)) -> NP f xs  -> g (NP f' xs)
    traverse'_NP :: forall {k} (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (SListI xs, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
    traverse'_NP forall (a :: k). f a -> g (f' a)
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g (f' a))
    -> NP f xs
    -> g (NP f' xs)
    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 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'_NP #-}

    -- | Specialization of 'hctraverse''.
    --
    -- @since 0.3.2.0
    --
    ctraverse'_POP :: (All2 c xss, Applicative g) => proxy c -> (forall a. c a => f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
    ctraverse'_POP :: 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))
    -> POP f xss
    -> g (POP f' xss)
    ctraverse'_POP proxy c
    p forall (a :: k). c a => f a -> g (f' a)
    f = (NP (NP f') xss -> POP f' xss)
    -> g (NP (NP f') xss) -> g (POP f' xss)
    forall a b. (a -> b) -> g a -> g b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap NP (NP f') xss -> POP f' xss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP (g (NP (NP f') xss) -> g (POP f' xss))
    -> (POP f xss -> g (NP (NP f') xss)) -> POP f xss -> g (POP 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))
    -> NP (NP f) xss
    -> g (NP (NP f') xss)
    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 -> 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) (NP (NP f) xss -> g (NP (NP f') xss))
    -> (POP f xss -> NP (NP f) xss) -> POP f xss -> g (NP (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

    -- | Specialization of 'hctraverse''.
    --
    -- @since 0.3.2.0
    --
    traverse'_POP :: (SListI2 xss, Applicative g) => (forall a. f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
    traverse'_POP :: forall {k} (xss :: [[k]]) (g :: * -> *) (f :: k -> *)
           (f' :: k -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
    traverse'_POP forall (a :: k). f a -> g (f' a)
    f =
      Proxy Top
    -> (forall (a :: k). Top a => f a -> g (f' a))
    -> POP f xss
    -> g (POP 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))
    -> POP f xss
    -> g (POP f' xss)
    ctraverse'_POP 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'_POP #-}

    instance HSequence NP  where
      hsequence' :: forall (xs :: [k]) (f :: * -> *) (g :: k -> *).
    (SListIN NP xs, Applicative f) =>
    NP (f :.: g) xs -> f (NP g xs)
    hsequence'  = NP (f :.: g) xs -> f (NP g xs)
    forall {k} (f :: * -> *) (g :: k -> *) (xs :: [k]).
    Applicative f =>
    NP (f :.: g) xs -> f (NP g xs)
    sequence'_NP
      hctraverse' :: forall (c :: k -> Constraint) (xs :: [k]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (AllN NP c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NP f xs
    -> g (NP f' xs)
    hctraverse' = proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> NP f xs
    -> g (NP f' xs)
    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
      htraverse' :: forall (xs :: [k]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
    (SListIN NP xs, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
    htraverse'  = (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
    forall {k} (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
    (SListI xs, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
    traverse'_NP

    instance HSequence POP where
      hsequence' :: forall (xs :: [[k]]) (f :: * -> *) (g :: k -> *).
    (SListIN POP xs, Applicative f) =>
    POP (f :.: g) xs -> f (POP g xs)
    hsequence'  = POP (f :.: g) xs -> f (POP g xs)
    forall {k} (xss :: [[k]]) (f :: * -> *) (g :: k -> *).
    (SListI xss, Applicative f) =>
    POP (f :.: g) xss -> f (POP g xss)
    sequence'_POP
      hctraverse' :: forall (c :: k -> Constraint) (xs :: [[k]]) (g :: * -> *)
           (proxy :: (k -> Constraint) -> *) (f :: k -> *) (f' :: k -> *).
    (AllN POP c xs, Applicative g) =>
    proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> POP f xs
    -> g (POP f' xs)
    hctraverse' = proxy c
    -> (forall (a :: k). c a => f a -> g (f' a))
    -> POP f xs
    -> g (POP 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))
    -> POP f xss
    -> g (POP f' xss)
    ctraverse'_POP
      htraverse' :: forall (xs :: [[k]]) (g :: * -> *) (f :: k -> *) (f' :: k -> *).
    (SListIN POP xs, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> POP f xs -> g (POP f' xs)
    htraverse'  = (forall (a :: k). f a -> g (f' a)) -> POP f xs -> g (POP f' xs)
    forall {k} (xss :: [[k]]) (g :: * -> *) (f :: k -> *)
           (f' :: k -> *).
    (SListI2 xss, Applicative g) =>
    (forall (a :: k). f a -> g (f' a)) -> POP f xss -> g (POP f' xss)
    traverse'_POP

    -- | Specialization of 'hsequence'.
    --
    -- /Example:/
    --
    -- >>> sequence_NP (Just 1 :* Just 2 :* Nil)
    -- Just (I 1 :* I 2 :* Nil)
    --
    sequence_NP  :: (SListI xs,  Applicative f) => NP  f xs  -> f (NP  I xs)

    -- | Specialization of 'hsequence'.
    --
    -- /Example:/
    --
    -- >>> sequence_POP (POP ((Just 1 :* Nil) :* (Just 2 :* Just 3 :* Nil) :* Nil))
    -- Just (POP ((I 1 :* Nil) :* (I 2 :* I 3 :* Nil) :* Nil))
    --
    sequence_POP :: (All SListI xss, Applicative f) => POP f xss -> f (POP I xss)

    sequence_NP :: forall (xs :: [*]) (f :: * -> *).
    (SListI xs, Applicative f) =>
    NP f xs -> f (NP I xs)
    sequence_NP   = NP f xs -> f (NP 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_POP :: forall (xss :: [[*]]) (f :: * -> *).
    (All SListI xss, Applicative f) =>
    POP f xss -> f (POP I xss)
    sequence_POP  = POP f xss -> f (POP 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_NP  :: (All  c xs, Applicative g) => proxy c -> (forall a. c a => f a -> g a) -> NP  f xs -> g (NP  I xs)

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

    ctraverse_NP :: 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_NP  = 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_POP :: 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_POP = 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 'NP'.
    --
    -- This is a suitable generalization of 'foldr'. It takes
    -- parameters on what to do for 'Nil' and ':*'. Since the
    -- input list is heterogeneous, the result is also indexed
    -- by a type-level list.
    --
    -- @since 0.2.3.0
    --
    cata_NP ::
         forall r f xs .
         r '[]
      -> (forall y ys . f y -> r ys -> r (y ': ys))
      -> NP f xs
      -> r xs
    cata_NP :: forall {a} (r :: [a] -> *) (f :: a -> *) (xs :: [a]).
    r '[]
    -> (forall (y :: a) (ys :: [a]). f y -> r ys -> r (y : ys))
    -> NP f xs
    -> r xs
    cata_NP r '[]
    nil forall (y :: a) (ys :: [a]). f y -> r ys -> r (y : ys)
    cons = NP f xs -> r xs
    forall (ys :: [a]). NP f ys -> r ys
    go
      where
        go :: forall ys . NP f ys -> r ys
        go :: forall (ys :: [a]). NP f ys -> r ys
    go NP f ys
    Nil       = r ys
    r '[]
    nil
        go (f x
    x :* NP f xs
    xs) = f x -> r xs -> r (x : xs)
    forall (y :: a) (ys :: [a]). f y -> r ys -> r (y : ys)
    cons f x
    x (NP f xs -> r xs
    forall (ys :: [a]). NP f ys -> r ys
    go NP f xs
    xs)

    -- | Constrained catamorphism for 'NP'.
    --
    -- The difference compared to 'cata_NP' is that the function
    -- for the cons-case can make use of the fact that the specified
    -- constraint holds for all the types in the signature of the
    -- product.
    --
    -- @since 0.2.3.0
    --
    ccata_NP ::
         forall c proxy r f xs . (All c xs)
      => proxy c
      -> r '[]
      -> (forall y ys . c y => f y -> r ys -> r (y ': ys))
      -> NP f xs
      -> r xs
    ccata_NP :: forall {a} (c :: a -> Constraint) (proxy :: (a -> Constraint) -> *)
           (r :: [a] -> *) (f :: a -> *) (xs :: [a]).
    All c xs =>
    proxy c
    -> r '[]
    -> (forall (y :: a) (ys :: [a]). c y => f y -> r ys -> r (y : ys))
    -> NP f xs
    -> r xs
    ccata_NP proxy c
    _ r '[]
    nil forall (y :: a) (ys :: [a]). c y => f y -> r ys -> r (y : ys)
    cons = NP f xs -> r xs
    forall (ys :: [a]). All c ys => NP f ys -> r ys
    go
      where
        go :: forall ys . (All c ys) => NP f ys -> r ys
        go :: forall (ys :: [a]). All c ys => NP f ys -> r ys
    go NP f ys
    Nil       = r ys
    r '[]
    nil
        go (f x
    x :* NP f xs
    xs) = f x -> r xs -> r (x : xs)
    forall (y :: a) (ys :: [a]). c y => f y -> r ys -> r (y : ys)
    cons f x
    x (NP f xs -> r xs
    forall (ys :: [a]). All c ys => NP f ys -> r ys
    go NP f xs
    xs)

    -- | Anamorphism for 'NP'.
    --
    -- In contrast to the anamorphism for normal lists, the
    -- generating function does not return an 'Either', but
    -- simply an element and a new seed value.
    --
    -- This is because the decision on whether to generate a
    -- 'Nil' or a ':*' is determined by the types.
    --
    -- @since 0.2.3.0
    --
    ana_NP ::
         forall s f xs .
         SListI xs
      => (forall y ys . s (y ': ys) -> (f y, s ys))
      -> s xs
      -> NP f xs
    ana_NP :: forall {k} (s :: [k] -> *) (f :: k -> *) (xs :: [k]).
    SListI xs =>
    (forall (y :: k) (ys :: [k]). s (y : ys) -> (f y, s ys))
    -> s xs -> NP f xs
    ana_NP forall (y :: k) (ys :: [k]). s (y : ys) -> (f y, s ys)
    uncons =
      Proxy Top
    -> (forall (y :: k) (ys :: [k]).
        Top y =>
        s (y : ys) -> (f y, s ys))
    -> s xs
    -> NP f xs
    forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (s :: [k] -> *) (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> (forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys))
    -> s xs
    -> NP f xs
    cana_NP Proxy Top
    forall {k}. Proxy Top
    topP s (y : ys) -> (f y, s ys)
    forall (y :: k) (ys :: [k]). s (y : ys) -> (f y, s ys)
    forall (y :: k) (ys :: [k]). Top y => s (y : ys) -> (f y, s ys)
    uncons
    {-# INLINE ana_NP #-}

    -- | Constrained anamorphism for 'NP'.
    --
    -- Compared to 'ana_NP', the generating function can
    -- make use of the specified constraint here for the
    -- elements that it generates.
    --
    -- @since 0.2.3.0
    --
    cana_NP ::
         forall c proxy s f xs . (All c xs)
      => proxy c
      -> (forall y ys . c y => s (y ': ys) -> (f y, s ys))
      -> s xs
      -> NP f xs
    cana_NP :: forall {k} (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
           (s :: [k] -> *) (f :: k -> *) (xs :: [k]).
    All c xs =>
    proxy c
    -> (forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys))
    -> s xs
    -> NP f xs
    cana_NP proxy c
    _ forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys)
    uncons = SList xs -> s xs -> NP f xs
    forall (ys :: [k]). All c ys => SList ys -> s ys -> NP 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 -> NP f ys
        go :: forall (ys :: [k]). All c ys => SList ys -> s ys -> NP f ys
    go SList ys
    SNil  s ys
    _ = NP f ys
    NP f '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
        go SList ys
    SCons s ys
    s = case s (x : xs) -> (f x, s xs)
    forall (y :: k) (ys :: [k]). c y => s (y : ys) -> (f y, s ys)
    uncons s ys
    s (x : xs)
    s of
          (f x
    x, s xs
    s') -> f x
    x f x -> NP f xs -> NP f (x : xs)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    :* SList xs -> s xs -> NP f xs
    forall (ys :: [k]). All c ys => SList ys -> s ys -> NP f ys
    go SList xs
    forall {k} (xs :: [k]). SListI xs => SList xs
    sList s xs
    s'

    -- | Specialization of 'htrans'.
    --
    -- @since 0.3.1.0
    --
    trans_NP ::
         AllZip c xs ys
      => proxy c
      -> (forall x y . c x y => f x -> g y)
      -> NP f xs -> NP g ys
    trans_NP :: 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)
    -> NP f xs
    -> NP g ys
    trans_NP proxy c
    _ forall (x :: k) (y :: k). c x y => f x -> g y
    _t NP f xs
    Nil       = NP g ys
    NP g '[]
    forall {k} (f :: k -> *). NP f '[]
    Nil
    trans_NP proxy c
    p  forall (x :: k) (y :: k). c x y => f x -> g y
    t (f x
    x :* NP f xs
    xs) = f x -> g (Head ys)
    forall (x :: k) (y :: k). c x y => f x -> g y
    t f x
    x g (Head ys) -> NP g (Tail ys) -> NP g (Head ys : Tail ys)
    forall {k} (f :: k -> *) (x :: k) (xs :: [k]).
    f x -> NP f xs -> NP f (x : xs)
    :* proxy c
    -> (forall (x :: k) (y :: k). c x y => f x -> g y)
    -> NP f xs
    -> NP 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)
    -> 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 NP f xs
    xs

    -- | Specialization of 'htrans'.
    --
    -- @since 0.3.1.0
    --
    trans_POP ::
         AllZip2 c xss yss
      => proxy c
      -> (forall x y . c x y => f x -> g y)
      -> POP f xss -> POP g yss
    trans_POP :: 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)
    -> POP f xss
    -> POP g yss
    trans_POP proxy c
    p forall (x :: k) (y :: k). c x y => f x -> g y
    t =
      NP (NP g) yss -> POP g yss
    forall k (f :: k -> *) (xss :: [[k]]). NP (NP f) xss -> POP f xss
    POP (NP (NP g) yss -> POP g yss)
    -> (POP f xss -> NP (NP g) yss) -> POP f xss -> POP 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)
    -> NP (NP f) xss
    -> NP (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)
    -> NP f xs
    -> NP g ys
    trans_NP (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 {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)
    -> 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) (NP (NP f) xss -> NP (NP g) yss)
    -> (POP f xss -> NP (NP f) xss) -> POP f xss -> NP (NP g) yss
    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

    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_NP ::
         forall f g xs ys .
         AllZip (LiftedCoercible f g) xs ys
      => NP f xs -> NP g ys
    coerce_NP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
    AllZip (LiftedCoercible f g) xs ys =>
    NP f xs -> NP g ys
    coerce_NP =
      NP f xs -> NP g ys
    forall a b. a -> b
    unsafeCoerce

    -- | Safe version of 'coerce_NP'.
    --
    -- For documentation purposes only; not exported.
    --
    _safe_coerce_NP ::
         forall f g xs ys .
         AllZip (LiftedCoercible f g) xs ys
      => NP f xs -> NP g ys
    _safe_coerce_NP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
    AllZip (LiftedCoercible f g) xs ys =>
    NP f xs -> NP g ys
    _safe_coerce_NP =
      Proxy (LiftedCoercible f g)
    -> (forall (x :: k) (y :: k).
        LiftedCoercible f g x y =>
        f x -> g y)
    -> NP f xs
    -> NP 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)
    -> NP f xs
    -> NP g ys
    trans_NP (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_POP ::
         forall f g xss yss .
         AllZip2 (LiftedCoercible f g) xss yss
      => POP f xss -> POP g yss
    coerce_POP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]])
           (yss :: [[k]]).
    AllZip2 (LiftedCoercible f g) xss yss =>
    POP f xss -> POP g yss
    coerce_POP =
      POP f xss -> POP g yss
    forall a b. a -> b
    unsafeCoerce

    -- | Safe version of 'coerce_POP'.
    --
    -- For documentation purposes only; not exported.
    --
    _safe_coerce_POP ::
         forall f g xss yss .
         AllZip2 (LiftedCoercible f g) xss yss
      => POP f xss -> POP g yss
    _safe_coerce_POP :: forall {k} {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]])
           (yss :: [[k]]).
    AllZip2 (LiftedCoercible f g) xss yss =>
    POP f xss -> POP g yss
    _safe_coerce_POP =
      Proxy (LiftedCoercible f g)
    -> (forall (x :: k) (y :: k).
        LiftedCoercible f g x y =>
        f x -> g y)
    -> POP f xss
    -> POP 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)
    -> POP f xss
    -> POP g yss
    trans_POP (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_NP ::
         forall f xs ys .
         AllZip (LiftedCoercible I f) xs ys
      => NP I xs -> NP f ys
    fromI_NP :: forall {k} (f :: k -> *) (xs :: [*]) (ys :: [k]).
    AllZip (LiftedCoercible I f) xs ys =>
    NP I xs -> NP f ys
    fromI_NP = NP I xs -> NP 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_NP ::
         forall f xs ys .
         AllZip (LiftedCoercible f I) xs ys
      => NP f xs -> NP I ys
    toI_NP :: forall {k} (f :: k -> *) (xs :: [k]) (ys :: [*]).
    AllZip (LiftedCoercible f I) xs ys =>
    NP f xs -> NP I ys
    toI_NP = NP f xs -> NP 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_POP ::
         forall f xss yss .
         AllZip2 (LiftedCoercible I f) xss yss
      => POP I xss -> POP f yss
    fromI_POP :: forall {k} (f :: k -> *) (xss :: [[*]]) (yss :: [[k]]).
    AllZip2 (LiftedCoercible I f) xss yss =>
    POP I xss -> POP f yss
    fromI_POP = POP I xss -> POP 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_POP ::
         forall f xss yss .
         AllZip2 (LiftedCoercible f I) xss yss
      => POP f xss -> POP I yss
    toI_POP :: forall {k} (f :: k -> *) (xss :: [[k]]) (yss :: [[*]]).
    AllZip2 (LiftedCoercible f I) xss yss =>
    POP f xss -> POP I yss
    toI_POP = POP f xss -> POP 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 NP NP where
      htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [k1]) (ys :: [k2])
           (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *)
           (g :: k2 -> *).
    AllZipN (Prod NP) c xs ys =>
    proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> NP f xs
    -> NP g ys
    htrans  = proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> NP f xs
    -> NP 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)
    -> NP f xs
    -> NP g ys
    trans_NP
      hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [k1]) (ys :: [k2]).
    AllZipN (Prod NP) (LiftedCoercible f g) xs ys =>
    NP f xs -> NP g ys
    hcoerce = NP f xs -> NP g ys
    forall {k} {k} (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
    AllZip (LiftedCoercible f g) xs ys =>
    NP f xs -> NP g ys
    coerce_NP
    instance HTrans POP POP where
      htrans :: forall (c :: k1 -> k2 -> Constraint) (xs :: [[k1]]) (ys :: [[k2]])
           (proxy :: (k1 -> k2 -> Constraint) -> *) (f :: k1 -> *)
           (g :: k2 -> *).
    AllZipN (Prod POP) c xs ys =>
    proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> POP f xs
    -> POP g ys
    htrans  = proxy c
    -> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
    -> POP f xs
    -> POP 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)
    -> POP f xss
    -> POP g yss
    trans_POP
      hcoerce :: forall (f :: k1 -> *) (g :: k2 -> *) (xs :: [[k1]]) (ys :: [[k2]]).
    AllZipN (Prod POP) (LiftedCoercible f g) xs ys =>
    POP f xs -> POP g ys
    hcoerce = POP f xs -> POP g ys
    forall {k} {k} (f :: k -> *) (g :: k -> *) (xss :: [[k]])
           (yss :: [[k]]).
    AllZip2 (LiftedCoercible f g) xss yss =>
    POP f xss -> POP g yss
    coerce_POP