    {-# LANGUAGE PolyKinds    #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# OPTIONS_GHC -Wno-orphans #-}
    module Barbies.Internal.ApplicativeB
      ( ApplicativeB(bpure, bprod)
      , bzip, bunzip, bzipWith, bzipWith3, bzipWith4

      , CanDeriveApplicativeB
      , gbprodDefault, gbpureDefault
      )

    where

    import Barbies.Generics.Applicative(GApplicative(..))
    import Barbies.Internal.FunctorB (FunctorB (..))

    import Data.Functor.Const   (Const (..))
    import Data.Functor.Constant(Constant (..))
    import Data.Functor.Product (Product (..))
    import Data.Kind            (Type)
    import Data.Proxy           (Proxy (..))

    import Data.Generics.GenericN

    -- | A 'FunctorB' with application, providing operations to:
    --
    --     * embed an "empty" value ('bpure')
    --
    --     * align and combine values ('bprod')
    --
    --  It should satisfy the following laws:
    --
    --  [Naturality of 'bprod']
    --
    -- @
    -- 'bmap' (\('Pair' a b) -> 'Pair' (f a) (g b)) (u `'bprod'` v) = 'bmap' f u `'bprod'` 'bmap' g v
    -- @
    --
    --
    --  [Left and right identity]
    --
    -- @
    -- 'bmap' (\('Pair' _ b) -> b) ('bpure' e `'bprod'` v) = v
    -- 'bmap' (\('Pair' a _) -> a) (u `'bprod'` 'bpure' e) = u
    -- @
    --
    -- [Associativity]
    --
    -- @
    -- 'bmap' (\('Pair' a ('Pair' b c)) -> 'Pair' ('Pair' a b) c) (u `'bprod'` (v `'bprod'` w)) = (u `'bprod'` v) `'bprod'` w
    -- @
    --
    --  It is to 'FunctorB' in the same way as 'Applicative'
    --  relates to 'Functor'. For a presentation of 'Applicative' as
    --  a monoidal functor, see Section 7 of
    --  <http://www.soi.city.ac.uk/~ross/papers/Applicative.html Applicative Programming with Effects>.
    --
    -- There is a default implementation of 'bprod' and 'bpure' based on 'Generic'.
    -- Intuitively, it works on types where the value of `bpure` is uniquely defined.
    -- This corresponds rougly to record types (in the presence of sums, there would
    -- be several candidates for `bpure`), where every field is either a 'Monoid' or
    -- covered by the argument @f@.
    class FunctorB b => ApplicativeB (b :: (k -> Type) -> Type) where
      bpure
        :: (forall a . f a)
        -> b f

      bprod
        :: b f
        -> b g
        -> b (f `Product` g)

      default bpure
        :: CanDeriveApplicativeB b f f
        => (forall a . f a)
        -> b f
      bpure = (forall (a :: k). f a) -> b f
    forall {k} (b :: (k -> *) -> *) (f :: k -> *).
    CanDeriveApplicativeB b f f =>
    (forall (a :: k). f a) -> b f
    gbpureDefault

      default bprod
        :: CanDeriveApplicativeB b f g
        => b f
        -> b
        g -> b (f `Product` g)
      bprod = b f -> b g -> b (Product f g)
    forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    CanDeriveApplicativeB b f g =>
    b f -> b g -> b (Product f g)
    gbprodDefault

    -- | An alias of 'bprod', since this is like a 'zip'.
    bzip
      :: ApplicativeB b
      => b f
      -> b g
      -> b (f `Product` g)
    bzip :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    bzip = b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod

    -- | An equivalent of 'unzip'.
    bunzip
      :: ApplicativeB b
      => b (f `Product` g)
      -> (b f, b g)
    bunzip :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b (Product f g) -> (b f, b g)
    bunzip b (Product f g)
    bfg
      = ((forall (a :: k). Product f g a -> f a) -> b (Product f g) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap (\(Pair f a
    a g a
    _) -> f a
    a) b (Product f g)
    bfg, (forall (a :: k). Product f g a -> g a) -> b (Product f g) -> b g
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap (\(Pair f a
    _ g a
    b) -> g a
    b) b (Product f g)
    bfg)

    -- | An equivalent of 'Data.List.zipWith'.
    bzipWith
      :: ApplicativeB b
      => (forall a. f a -> g a -> h a)
      -> b f
      -> b g
      -> b h
    bzipWith :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a -> g a -> h a) -> b f -> b g -> b h
    bzipWith forall (a :: k). f a -> g a -> h a
    f b f
    bf b g
    bg
      = (forall (a :: k). Product f g a -> h a) -> b (Product f g) -> b h
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap (\(Pair f a
    fa g a
    ga) -> f a -> g a -> h a
    forall (a :: k). f a -> g a -> h a
    f f a
    fa g a
    ga) (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg)

    -- | An equivalent of 'Data.List.zipWith3'.
    bzipWith3
      :: ApplicativeB b
      => (forall a. f a -> g a -> h a -> i a)
      -> b f
      -> b g
      -> b h
      -> b i
    bzipWith3 :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *) (i :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> b f -> b g -> b h -> b i
    bzipWith3 forall (a :: k). f a -> g a -> h a -> i a
    f b f
    bf b g
    bg b h
    bh
      = (forall (a :: k). Product (Product f g) h a -> i a)
    -> b (Product (Product f g) h) -> b i
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap (\(Pair (Pair f a
    fa g a
    ga) h a
    ha) -> f a -> g a -> h a -> i a
    forall (a :: k). f a -> g a -> h a -> i a
    f f a
    fa g a
    ga h a
    ha)
             (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg b (Product f g) -> b h -> b (Product (Product f g) h)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b h
    bh)

    -- | An equivalent of 'Data.List.zipWith4'.
    bzipWith4
      :: ApplicativeB b
      => (forall a. f a -> g a -> h a -> i a -> j a)
      -> b f
      -> b g
      -> b h
      -> b
      i -> b j
    bzipWith4 :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *)
           (h :: k -> *) (i :: k -> *) (j :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a -> g a -> h a -> i a -> j a)
    -> b f -> b g -> b h -> b i -> b j
    bzipWith4 forall (a :: k). f a -> g a -> h a -> i a -> j a
    f b f
    bf b g
    bg b h
    bh b i
    bi
      = (forall (a :: k). Product (Product (Product f g) h) i a -> j a)
    -> b (Product (Product (Product f g) h) i) -> b j
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap (\(Pair (Pair (Pair f a
    fa g a
    ga) h a
    ha) i a
    ia) -> f a -> g a -> h a -> i a -> j a
    forall (a :: k). f a -> g a -> h a -> i a -> j a
    f f a
    fa g a
    ga h a
    ha i a
    ia)
             (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg b (Product f g) -> b h -> b (Product (Product f g) h)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b h
    bh b (Product (Product f g) h)
    -> b i -> b (Product (Product (Product f g) h) i)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b i
    bi)

    -- | @'CanDeriveApplicativeB' B f g@ is in practice a predicate about @B@ only.
    --   Intuitively, it says that the following holds, for any arbitrary @f@:
    --
    --     * There is an instance of @'Generic' (B f)@.
    --
    --     * @B@ has only one constructor (that is, it is not a sum-type).
    --
    --     * Every field of @B f@ is either a monoid, or of the form @f a@, for
    --       some type @a@.
    type CanDeriveApplicativeB b f g
      = ( GenericP 0 (b f)
        , GenericP 0 (b g)
        , GenericP 0 (b (f `Product` g))
        , GApplicative 0 f g (RepP 0 (b f)) (RepP 0 (b g)) (RepP 0 (b (f `Product` g)))
        )

    -- ======================================
    -- Generic derivation of instances
    -- ======================================

    -- | Default implementation of 'bprod' based on 'Generic'.
    gbprodDefault
      :: forall b f g
      .  CanDeriveApplicativeB b f g
      => b f
      -> b g
      -> b (f `Product` g)
    gbprodDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    CanDeriveApplicativeB b f g =>
    b f -> b g -> b (Product f g)
    gbprodDefault b f
    l b g
    r
      = Proxy 0 -> RepP 0 (b (Product f g)) (ZonkAny 1) -> b (Product f g)
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> RepP n a x -> a
    forall x. Proxy 0 -> RepP 0 (b (Product f g)) x -> b (Product f g)
    toP Proxy 0
    p0 (RepP 0 (b (Product f g)) (ZonkAny 1) -> b (Product f g))
    -> RepP 0 (b (Product f g)) (ZonkAny 1) -> b (Product f g)
    forall a b. (a -> b) -> a -> b
    $ Proxy 0
    -> Proxy f
    -> Proxy g
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f)))
         (Rep (b f))
         (ZonkAny 1)
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 g)))
         (Rep (b g))
         (ZonkAny 1)
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 (Product f g))))
         (Rep (b (Product f g)))
         (ZonkAny 1)
    forall x.
    Proxy 0
    -> Proxy f
    -> Proxy g
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f))) (Rep (b f)) x
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 g))) (Rep (b g)) x
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 (Product f g))))
         (Rep (b (Product f g)))
         x
    forall {k} {k1} k2 (n :: k) (f :: k2 -> *) (g :: k2 -> *)
           (repbf :: k1 -> *) (repbg :: k1 -> *) (repbfg :: k1 -> *)
           (x :: k1).
    GApplicative n f g repbf repbg repbfg =>
    Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gprod Proxy 0
    p0 (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @f) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @g) (Proxy 0 -> b f -> RepP 0 (b f) (ZonkAny 1)
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> a -> RepP n a x
    forall x. Proxy 0 -> b f -> RepP 0 (b f) x
    fromP Proxy 0
    p0 b f
    l) (Proxy 0 -> b g -> RepP 0 (b g) (ZonkAny 1)
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> a -> RepP n a x
    forall x. Proxy 0 -> b g -> RepP 0 (b g) x
    fromP Proxy 0
    p0 b g
    r)
      where
        p0 :: Proxy 0
    p0 = forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0
    {-# INLINE gbprodDefault #-}

    gbpureDefault
      :: forall b f
      .  CanDeriveApplicativeB b f f
      => (forall a . f a)
      -> b f
    gbpureDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *).
    CanDeriveApplicativeB b f f =>
    (forall (a :: k). f a) -> b f
    gbpureDefault forall (a :: k). f a
    fa
      = Proxy 0 -> RepP 0 (b f) (ZonkAny 0) -> b f
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> RepP n a x -> a
    forall x. Proxy 0 -> RepP 0 (b f) x -> b f
    toP (forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0) (RepP 0 (b f) (ZonkAny 0) -> b f)
    -> RepP 0 (b f) (ZonkAny 0) -> b f
    forall a b. (a -> b) -> a -> b
    $ Proxy 0
    -> Proxy f
    -> Proxy
         (Zip (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f))) (Rep (b f)))
    -> Proxy
         (Zip
            (Rep (FilterIndex 0 (Indexed b 1) (Param 0 (Product f f))))
            (Rep (b (Product f f))))
    -> (forall (a :: k). f a)
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f)))
         (Rep (b f))
         (ZonkAny 0)
    forall x.
    (f ~ f,
     Zip (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f))) (Rep (b f))
     ~ Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f))) (Rep (b f))) =>
    Proxy 0
    -> Proxy f
    -> Proxy
         (Zip (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f))) (Rep (b f)))
    -> Proxy
         (Zip
            (Rep (FilterIndex 0 (Indexed b 1) (Param 0 (Product f f))))
            (Rep (b (Product f f))))
    -> (forall (a :: k). f a)
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 1) (Param 0 f))) (Rep (b f)) x
    forall {k} {k1} k2 (n :: k) (f :: k2 -> *) (g :: k2 -> *)
           (repbf :: k1 -> *) (repbg :: k1 -> *) (repbfg :: k1 -> *)
           (x :: k1).
    (GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy n
    -> Proxy f
    -> Proxy repbf
    -> Proxy repbfg
    -> (forall (a :: k2). f a)
    -> repbf x
    gpure
          (forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0)
          (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @f)
          (forall {k} (t :: k). Proxy t
    forall (t :: * -> *). Proxy t
    Proxy @(RepP 0 (b f)))
          (forall {k} (t :: k). Proxy t
    forall (t :: * -> *). Proxy t
    Proxy @(RepP 0 (b (f `Product` f))))
          f a
    forall (a :: k). f a
    fa
    {-# INLINE gbpureDefault #-}

    -- ------------------------------------------------------------
    -- Generic derivation: Special cases for ApplicativeB
    -- -------------------------------------------------------------

    type P = Param

    instance
      (  ApplicativeB b
      ) => GApplicative 0 f g (Rec (b (P 0 f)) (b f))
                              (Rec (b (P 0 g)) (b g))
                              (Rec (b (P 0 (f `Product` g))) (b (f `Product` g)))
      where
      gpure :: forall (x :: k1).
    (f ~ g, Rec (b (P 0 f)) (b f) ~ Rec (b (P 0 g)) (b g)) =>
    Proxy 0
    -> Proxy f
    -> Proxy (Rec (b (P 0 f)) (b f))
    -> Proxy (Rec (b (P 0 (Product f g))) (b (Product f g)))
    -> (forall (a :: k). f a)
    -> Rec (b (P 0 f)) (b f) x
    gpure Proxy 0
    _ Proxy f
    _ Proxy (Rec (b (P 0 f)) (b f))
    _ Proxy (Rec (b (P 0 (Product f g))) (b (Product f g)))
    _ forall (a :: k). f a
    fa
        = K1 R (b f) x -> Rec (b (P 0 f)) (b f) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (b f -> K1 R (b f) x
    forall k i c (p :: k). c -> K1 i c p
    K1 ((forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    bpure f a
    forall (a :: k). f a
    fa))
      {-# INLINE gpure #-}

      gprod :: forall (x :: k1).
    Proxy 0
    -> Proxy f
    -> Proxy g
    -> Rec (b (P 0 f)) (b f) x
    -> Rec (b (P 0 g)) (b g) x
    -> Rec (b (P 0 (Product f g))) (b (Product f g)) x
    gprod Proxy 0
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 b f
    bf)) (Rec (K1 b g
    bg))
        = K1 R (b (Product f g)) x
    -> Rec (b (P 0 (Product f g))) (b (Product f g)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (b (Product f g) -> K1 R (b (Product f g)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg))
      {-# INLINE gprod #-}

    instance
      ( Applicative h
      , ApplicativeB b
      ) => GApplicative 0 f g (Rec (h (b (P 0 f))) (h (b f)))
                              (Rec (h (b (P 0 g))) (h (b g)))
                              (Rec (h (b (P 0 (f `Product` g)))) (h (b (f `Product` g))))
      where
      gpure :: forall (x :: k1).
    (f ~ g,
     Rec (h (b (P 0 f))) (h (b f)) ~ Rec (h (b (P 0 g))) (h (b g))) =>
    Proxy 0
    -> Proxy f
    -> Proxy (Rec (h (b (P 0 f))) (h (b f)))
    -> Proxy (Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))))
    -> (forall (a :: k). f a)
    -> Rec (h (b (P 0 f))) (h (b f)) x
    gpure Proxy 0
    _ Proxy f
    _ Proxy (Rec (h (b (P 0 f))) (h (b f)))
    _ Proxy (Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))))
    _ forall (a :: k). f a
    fa
        = K1 R (h (b f)) x -> Rec (h (b (P 0 f))) (h (b f)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (h (b f) -> K1 R (h (b f)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b f -> h (b f)
    forall a. a -> h a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (b f -> h (b f)) -> b f -> h (b f)
    forall a b. (a -> b) -> a -> b
    $ (forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    bpure f a
    forall (a :: k). f a
    fa))
      {-# INLINE gpure #-}

      gprod :: forall (x :: k1).
    Proxy 0
    -> Proxy f
    -> Proxy g
    -> Rec (h (b (P 0 f))) (h (b f)) x
    -> Rec (h (b (P 0 g))) (h (b g)) x
    -> Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))) x
    gprod Proxy 0
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 h (b f)
    hbf)) (Rec (K1 h (b g)
    hbg))
        = K1 R (h (b (Product f g))) x
    -> Rec (h (b (P 0 (Product f g)))) (h (b (Product f g))) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (h (b (Product f g)) -> K1 R (h (b (Product f g))) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod (b f -> b g -> b (Product f g))
    -> h (b f) -> h (b g -> b (Product f g))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> h (b f)
    hbf h (b g -> b (Product f g)) -> h (b g) -> h (b (Product f g))
    forall a b. h (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> h (b g)
    hbg))
      {-# INLINE gprod #-}

    -- This is the same as the previous instance, but for nested Applicatives.
    instance
      ( Applicative h
      , Applicative m
      , ApplicativeB b
      ) => GApplicative 0 f g (Rec (m (h (b (P 0 f)))) (m (h (b f))))
                              (Rec (m (h (b (P 0 g)))) (m (h (b g))))
                              (Rec (m (h (b (P 0 (f `Product` g))))) (m (h (b (f `Product` g)))))
      where
      gpure :: forall (x :: k1).
    (f ~ g,
     Rec (m (h (b (P 0 f)))) (m (h (b f)))
     ~ Rec (m (h (b (P 0 g)))) (m (h (b g)))) =>
    Proxy 0
    -> Proxy f
    -> Proxy (Rec (m (h (b (P 0 f)))) (m (h (b f))))
    -> Proxy
         (Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))))
    -> (forall (a :: k). f a)
    -> Rec (m (h (b (P 0 f)))) (m (h (b f))) x
    gpure Proxy 0
    _ Proxy f
    _ Proxy (Rec (m (h (b (P 0 f)))) (m (h (b f))))
    _ Proxy
      (Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))))
    _ forall (a :: k). f a
    x
        = K1 R (m (h (b f))) x -> Rec (m (h (b (P 0 f)))) (m (h (b f))) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (m (h (b f)) -> K1 R (m (h (b f))) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (h (b f) -> m (h (b f))
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (h (b f) -> m (h (b f))) -> (b f -> h (b f)) -> b f -> m (h (b f))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b f -> h (b f)
    forall a. a -> h a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (b f -> m (h (b f))) -> b f -> m (h (b f))
    forall a b. (a -> b) -> a -> b
    $ (forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    bpure f a
    forall (a :: k). f a
    x))
      {-# INLINE gpure #-}

      gprod :: forall (x :: k1).
    Proxy 0
    -> Proxy f
    -> Proxy g
    -> Rec (m (h (b (P 0 f)))) (m (h (b f))) x
    -> Rec (m (h (b (P 0 g)))) (m (h (b g))) x
    -> Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))) x
    gprod Proxy 0
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 m (h (b f))
    hbf)) (Rec (K1 m (h (b g))
    hbg))
        = K1 R (m (h (b (Product f g)))) x
    -> Rec (m (h (b (P 0 (Product f g))))) (m (h (b (Product f g)))) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (m (h (b (Product f g))) -> K1 R (m (h (b (Product f g)))) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (h (b f) -> h (b g) -> h (b (Product f g))
    forall {k} {f :: * -> *} {b :: (k -> *) -> *} {f :: k -> *}
           {g :: k -> *}.
    (Applicative f, ApplicativeB b) =>
    f (b f) -> f (b g) -> f (b (Product f g))
    go (h (b f) -> h (b g) -> h (b (Product f g)))
    -> m (h (b f)) -> m (h (b g) -> h (b (Product f g)))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (h (b f))
    hbf m (h (b g) -> h (b (Product f g)))
    -> m (h (b g)) -> m (h (b (Product f g)))
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> m (h (b g))
    hbg))
        where
          go :: f (b f) -> f (b g) -> f (b (Product f g))
    go f (b f)
    a f (b g)
    b = b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod (b f -> b g -> b (Product f g))
    -> f (b f) -> f (b g -> b (Product f g))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (b f)
    a f (b g -> b (Product f g)) -> f (b g) -> f (b (Product f g))
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f (b g)
    b
      {-# INLINE gprod #-}

    -- --------------------------------
    -- Instances for base types
    -- --------------------------------

    instance ApplicativeB Proxy where
      bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Proxy f
    bpure forall (a :: k). f a
    _ = Proxy f
    forall {k} (t :: k). Proxy t
    Proxy
      {-# INLINE bpure #-}

      bprod :: forall (f :: k -> *) (g :: k -> *).
    Proxy f -> Proxy g -> Proxy (Product f g)
    bprod Proxy f
    _ Proxy g
    _ = Proxy (Product f g)
    forall {k} (t :: k). Proxy t
    Proxy
      {-# INLINE bprod #-}

    instance Monoid a => ApplicativeB (Const a) where
      bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Const a f
    bpure forall (a :: k). f a
    _
        = a -> Const a f
    forall {k} a (b :: k). a -> Const a b
    Const a
    forall a. Monoid a => a
    mempty
      {-# INLINE bpure #-}

      bprod :: forall (f :: k -> *) (g :: k -> *).
    Const a f -> Const a g -> Const a (Product f g)
    bprod (Const a
    l) (Const a
    r)
        = a -> Const a (Product f g)
    forall {k} a (b :: k). a -> Const a b
    Const (a
    l a -> a -> a
    forall a. Monoid a => a -> a -> a
    `mappend` a
    r)
      {-# INLINE bprod #-}

    instance (ApplicativeB a, ApplicativeB b) => ApplicativeB (Product a b) where
      bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Product a b f
    bpure forall (a :: k). f a
    x
        = a f -> b f -> Product a b f
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair ((forall (a :: k). f a) -> a f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> a f
    bpure f a
    forall (a :: k). f a
    x) ((forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    bpure f a
    forall (a :: k). f a
    x)
      {-# INLINE bpure #-}

      bprod :: forall (f :: k -> *) (g :: k -> *).
    Product a b f -> Product a b g -> Product a b (Product f g)
    bprod (Pair a f
    ll b f
    lr) (Pair a g
    rl b g
    rr)
        = a (Product f g) -> b (Product f g) -> Product a b (Product f g)
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (a f -> a g -> a (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). a f -> a g -> a (Product f g)
    bprod a f
    ll a g
    rl) (b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod b f
    lr b g
    rr)
      {-# INLINE bprod #-}

    -- --------------------------------
    -- Instances for base types
    -- --------------------------------

    instance Monoid a => ApplicativeB (Constant a) where
      bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> Constant a f
    bpure forall (a :: k). f a
    _
        = a -> Constant a f
    forall {k} a (b :: k). a -> Constant a b
    Constant a
    forall a. Monoid a => a
    mempty
      {-# INLINE bpure #-}

      bprod :: forall (f :: k -> *) (g :: k -> *).
    Constant a f -> Constant a g -> Constant a (Product f g)
    bprod (Constant a
    l) (Constant a
    r)
        = a -> Constant a (Product f g)
    forall {k} a (b :: k). a -> Constant a b
    Constant (a
    l a -> a -> a
    forall a. Monoid a => a -> a -> a
    `mappend` a
    r)
      {-# INLINE bprod #-}