    {-# LANGUAGE CPP #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE UndecidableInstances #-}

    #if __GLASGOW_HASKELL__ >= 806

    {-# LANGUAGE QuantifiedConstraints #-}

    #endif

    {-# OPTIONS_GHC -Wno-orphans #-}
    module Barbies.Internal.ApplicativeT
      ( ApplicativeT(tpure, tprod)
      , tzip, tunzip, tzipWith, tzipWith3, tzipWith4

      , CanDeriveApplicativeT
      , gtprodDefault, gtpureDefault
      )

    where

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

    import Control.Applicative (Alternative(..))
    import Data.Functor.Compose (Compose (..))
    import Data.Functor.Product (Product (..))
    import Data.Functor.Reverse (Reverse (..))
    import Data.Functor.Sum (Sum (..))
    import Data.Kind (Type)
    import Data.Proxy (Proxy (..))

    import Data.Generics.GenericN

    -- | A 'FunctorT' with application, providing operations to:
    --
    --     * embed an "empty" value ('tpure')
    --
    --     * align and combine values ('tprod')
    --
    --  It should satisfy the following laws:
    --
    --  [Naturality of 'tprod']
    --
    -- @
    -- 'tmap' (\('Pair' a b) -> 'Pair' (f a) (g b)) (u `'tprod'` v) = 'tmap' f u `'tprod'` 'tmap' g v
    -- @
    --
    --  [Left and right identity]
    --
    -- @
    -- 'tmap' (\('Pair' _ b) -> b) ('tpure' e `'tprod'` v) = v
    -- 'tmap' (\('Pair' a _) -> a) (u `'tprod'` 'tpure' e) = u
    -- @
    --
    -- [Associativity]
    --
    -- @
    -- 'tmap' (\('Pair' a ('Pair' b c)) -> 'Pair' ('Pair' a b) c) (u `'tprod'` (v `'tprod'` w)) = (u `'tprod'` v) `'tprod'` w
    -- @
    --
    --  It is to 'FunctorT' in the same way is '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 'tprod' and 'tpure' based on 'Generic'.
    -- Intuitively, it works on types where the value of `tpure` is uniquely defined.
    -- This corresponds rougly to record types (in the presence of sums, there would
    -- be several candidates for `tpure`), where every field is either a 'Monoid' or
    -- covered by the argument @f@.
    class FunctorT t => ApplicativeT (t :: (k -> Type) -> (k' -> Type)) where
      tpure
        :: (forall a . f a)
        -> t f x

      tprod
        :: t f x
        -> t g x
        -> t (f `Product` g) x

      default tpure
        :: CanDeriveApplicativeT t f f x
        => (forall a . f a)
        -> t f x
      tpure = (forall (a :: k). f a) -> t f x
    forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *) (x :: k).
    CanDeriveApplicativeT t f f x =>
    (forall (a :: k). f a) -> t f x
    gtpureDefault

      default tprod
        :: CanDeriveApplicativeT t f g x
        => t f x
        -> t g x
        -> t (f `Product` g) x
      tprod = t f x -> t g x -> t (Product f g) x
    forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *)
           (g :: k -> *) (x :: k).
    CanDeriveApplicativeT t f g x =>
    t f x -> t g x -> t (Product f g) x
    gtprodDefault

    -- | An alias of 'tprod'.
    tzip
      :: ApplicativeT t
      => t f x
      -> t g x
      -> t (f `Product` g) x
    tzip :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    tzip = t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    tprod

    -- | An equivalent of 'unzip'.
    tunzip
      :: ApplicativeT t
      => t (f `Product` g) x
      -> (t f x, t g x)
    tunzip :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
           (g :: k -> *) (x :: k').
    ApplicativeT t =>
    t (Product f g) x -> (t f x, t g x)
    tunzip t (Product f g) x
    tfg
      = ((forall (a :: k). Product f g a -> f a)
    -> t (Product f g) x -> t f x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
           (x :: k').
    FunctorT t =>
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    forall (f :: k -> *) (g :: k -> *) (x :: k').
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    tmap (\(Pair f a
    a g a
    _) -> f a
    a) t (Product f g) x
    tfg, (forall (a :: k). Product f g a -> g a)
    -> t (Product f g) x -> t g x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
           (x :: k').
    FunctorT t =>
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    forall (f :: k -> *) (g :: k -> *) (x :: k').
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    tmap (\(Pair f a
    _ g a
    b) -> g a
    b) t (Product f g) x
    tfg)

    -- | An equivalent of 'Data.List.zipWith'.
    tzipWith
      :: ApplicativeT t
      => (forall a. f a -> g a -> h a)
      -> t f x
      -> t g x
      -> t h x
    tzipWith :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
           (g :: k -> *) (h :: k -> *) (x :: k').
    ApplicativeT t =>
    (forall (a :: k). f a -> g a -> h a) -> t f x -> t g x -> t h x
    tzipWith forall (a :: k). f a -> g a -> h a
    f t f x
    tf t g x
    tg
      = (forall (a :: k). Product f g a -> h a)
    -> t (Product f g) x -> t h x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
           (x :: k').
    FunctorT t =>
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    forall (f :: k -> *) (g :: k -> *) (x :: k').
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    tmap (\(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) (t f x
    tf t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t g x
    tg)

    -- | An equivalent of 'Data.List.zipWith3'.
    tzipWith3
      :: ApplicativeT t
      => (forall a. f a -> g a -> h a -> i a)
      -> t f x
      -> t g x
      -> t h x
      -> t i x
    tzipWith3 :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
           (g :: k -> *) (h :: k -> *) (i :: k -> *) (x :: k').
    ApplicativeT t =>
    (forall (a :: k). f a -> g a -> h a -> i a)
    -> t f x -> t g x -> t h x -> t i x
    tzipWith3 forall (a :: k). f a -> g a -> h a -> i a
    f t f x
    tf t g x
    tg t h x
    th
      = (forall (a :: k). Product (Product f g) h a -> i a)
    -> t (Product (Product f g) h) x -> t i x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
           (x :: k').
    FunctorT t =>
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    forall (f :: k -> *) (g :: k -> *) (x :: k').
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    tmap (\(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)
             (t f x
    tf t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t g x
    tg t (Product f g) x -> t h x -> t (Product (Product f g) h) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t h x
    th)

    -- | An equivalent of 'Data.List.zipWith4'.
    tzipWith4
      :: ApplicativeT t
      => (forall a. f a -> g a -> h a -> i a -> j a)
      -> t f x
      -> t g x
      -> t h x
      -> t i x
      -> t j x
    tzipWith4 :: forall {k} {k'} (t :: (k -> *) -> k' -> *) (f :: k -> *)
           (g :: k -> *) (h :: k -> *) (i :: k -> *) (j :: k -> *) (x :: k').
    ApplicativeT t =>
    (forall (a :: k). f a -> g a -> h a -> i a -> j a)
    -> t f x -> t g x -> t h x -> t i x -> t j x
    tzipWith4 forall (a :: k). f a -> g a -> h a -> i a -> j a
    f t f x
    tf t g x
    tg t h x
    th t i x
    ti
      = (forall (a :: k). Product (Product (Product f g) h) i a -> j a)
    -> t (Product (Product (Product f g) h) i) x -> t j x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
           (x :: k').
    FunctorT t =>
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    forall (f :: k -> *) (g :: k -> *) (x :: k').
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    tmap (\(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)
             (t f x
    tf t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t g x
    tg t (Product f g) x -> t h x -> t (Product (Product f g) h) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t h x
    th t (Product (Product f g) h) x
    -> t i x -> t (Product (Product (Product f g) h) i) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t i x
    ti)

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

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

    -- | Default implementation of 'tprod' based on 'Generic'.
    gtprodDefault
      :: forall t f g x
      .  CanDeriveApplicativeT t f g x
      => t f x
      -> t g x
      -> t (f `Product` g) x
    gtprodDefault :: forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *)
           (g :: k -> *) (x :: k).
    CanDeriveApplicativeT t f g x =>
    t f x -> t g x -> t (Product f g) x
    gtprodDefault t f x
    l t g x
    r
      = Proxy 1
    -> RepP 1 (t (Product f g) x) (ZonkAny 1) -> t (Product f g) x
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> RepP n a x -> a
    forall x.
    Proxy 1 -> RepP 1 (t (Product f g) x) x -> t (Product f g) x
    toP Proxy 1
    p1 (RepP 1 (t (Product f g) x) (ZonkAny 1) -> t (Product f g) x)
    -> RepP 1 (t (Product f g) x) (ZonkAny 1) -> t (Product f g) x
    forall a b. (a -> b) -> a -> b
    $ Proxy 1
    -> Proxy f
    -> Proxy g
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x))
         (Rep (t f x))
         (ZonkAny 1)
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 g) x))
         (Rep (t g x))
         (ZonkAny 1)
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 (Product f g)) x))
         (Rep (t (Product f g) x))
         (ZonkAny 1)
    forall x.
    Proxy 1
    -> Proxy f
    -> Proxy g
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x)) (Rep (t f x)) x
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 g) x)) (Rep (t g x)) x
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 (Product f g)) x))
         (Rep (t (Product f g) x))
         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 1
    p1 (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 1 -> t f x -> RepP 1 (t f x) (ZonkAny 1)
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> a -> RepP n a x
    forall x. Proxy 1 -> t f x -> RepP 1 (t f x) x
    fromP Proxy 1
    p1 t f x
    l) (Proxy 1 -> t g x -> RepP 1 (t g x) (ZonkAny 1)
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> a -> RepP n a x
    forall x. Proxy 1 -> t g x -> RepP 1 (t g x) x
    fromP Proxy 1
    p1 t g x
    r)
      where
          p1 :: Proxy 1
    p1 = forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @1
    {-# INLINE gtprodDefault #-}

    gtpureDefault
      :: forall t f x
      .  CanDeriveApplicativeT t f f x
      => (forall a . f a)
      -> t f x
    gtpureDefault :: forall {k} {k} (t :: (k -> *) -> k -> *) (f :: k -> *) (x :: k).
    CanDeriveApplicativeT t f f x =>
    (forall (a :: k). f a) -> t f x
    gtpureDefault forall (a :: k). f a
    fa
      = Proxy 1 -> RepP 1 (t f x) (ZonkAny 0) -> t f x
    forall (n :: Natural) a x.
    GenericP n a =>
    Proxy n -> RepP n a x -> a
    forall x. Proxy 1 -> RepP 1 (t f x) x -> t f x
    toP (forall (t :: Natural). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @1) (RepP 1 (t f x) (ZonkAny 0) -> t f x)
    -> RepP 1 (t f x) (ZonkAny 0) -> t f x
    forall a b. (a -> b) -> a -> b
    $ Proxy 1
    -> Proxy f
    -> Proxy
         (Zip
            (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x)) (Rep (t f x)))
    -> Proxy
         (Zip
            (Rep (FilterIndex 1 (Indexed t 2) (Param 1 (Product f f)) x))
            (Rep (t (Product f f) x)))
    -> (forall (a :: k). f a)
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x))
         (Rep (t f x))
         (ZonkAny 0)
    forall x.
    (f ~ f,
     Zip (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x)) (Rep (t f x))
     ~ Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x)) (Rep (t f x))) =>
    Proxy 1
    -> Proxy f
    -> Proxy
         (Zip
            (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x)) (Rep (t f x)))
    -> Proxy
         (Zip
            (Rep (FilterIndex 1 (Indexed t 2) (Param 1 (Product f f)) x))
            (Rep (t (Product f f) x)))
    -> (forall (a :: k). f a)
    -> Zip
         (Rep (FilterIndex 1 (Indexed t 2) (Param 1 f) x)) (Rep (t f x)) 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 @1)
          (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 1 (t f x)))
          (forall {k} (t :: k). Proxy t
    forall (t :: * -> *). Proxy t
    Proxy @(RepP 1 (t (f `Product` f) x)))
          f a
    forall (a :: k). f a
    fa
    {-# INLINE gtpureDefault #-}

    -- ------------------------------------------------------------
    -- Generic derivation: Special cases for ApplicativeT
    -- -------------------------------------------------------------

    type P = Param

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

      gprod :: forall (x :: k1).
    Proxy 1
    -> Proxy f
    -> Proxy g
    -> Rec (t (P 1 f) x) (t f x) x
    -> Rec (t (P 1 g) x) (t g x) x
    -> Rec (t (P 1 (Product f g)) x) (t (Product f g) x) x
    gprod Proxy 1
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 t f x
    tf)) (Rec (K1 t g x
    tg))
        = K1 R (t (Product f g) x) x
    -> Rec (t (P 1 (Product f g)) x) (t (Product f g) x) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (t (Product f g) x -> K1 R (t (Product f g) x) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (t f x
    tf t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    `tprod` t g x
    tg))
      {-# INLINE gprod #-}

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

      gprod :: forall (x :: k1).
    Proxy 1
    -> Proxy f
    -> Proxy g
    -> Rec (h (t (P 1 f) x)) (h (t f x)) x
    -> Rec (h (t (P 1 g) x)) (h (t g x)) x
    -> Rec (h (t (P 1 (Product f g)) x)) (h (t (Product f g) x)) x
    gprod Proxy 1
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 h (t f x)
    htf)) (Rec (K1 h (t g x)
    htg))
        = K1 R (h (t (Product f g) x)) x
    -> Rec (h (t (P 1 (Product f g)) x)) (h (t (Product f g) x)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (h (t (Product f g) x) -> K1 R (h (t (Product f g) x)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    tprod (t f x -> t g x -> t (Product f g) x)
    -> h (t f x) -> h (t g x -> t (Product f g) x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> h (t f x)
    htf h (t g x -> t (Product f g) x)
    -> h (t g x) -> h (t (Product f g) x)
    forall a b. h (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> h (t g x)
    htg))
      {-# INLINE gprod #-}

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

      gprod :: forall (x :: k1).
    Proxy 1
    -> Proxy f
    -> Proxy g
    -> Rec (m (h (t (P 1 f) x))) (m (h (t f x))) x
    -> Rec (m (h (t (P 1 g) x))) (m (h (t g x))) x
    -> Rec
         (m (h (t (P 1 (Product f g)) x))) (m (h (t (Product f g) x))) x
    gprod Proxy 1
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 m (h (t f x))
    htfx)) (Rec (K1 m (h (t g x))
    htgx))
        = K1 R (m (h (t (Product f g) x))) x
    -> Rec
         (m (h (t (P 1 (Product f g)) x))) (m (h (t (Product f g) x))) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (m (h (t (Product f g) x)) -> K1 R (m (h (t (Product f g) x))) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (h (t f x) -> h (t g x) -> h (t (Product f g) x)
    forall {k} {k'} {f :: * -> *} {t :: (k -> *) -> k' -> *}
           {f :: k -> *} {x :: k'} {g :: k -> *}.
    (Applicative f, ApplicativeT t) =>
    f (t f x) -> f (t g x) -> f (t (Product f g) x)
    go (h (t f x) -> h (t g x) -> h (t (Product f g) x))
    -> m (h (t f x)) -> m (h (t g x) -> h (t (Product f g) x))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (h (t f x))
    htfx m (h (t g x) -> h (t (Product f g) x))
    -> m (h (t g x)) -> m (h (t (Product f g) x))
    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 (t g x))
    htgx))
        where
          go :: f (t f x) -> f (t g x) -> f (t (Product f g) x)
    go f (t f x)
    a f (t g x)
    b = t f x -> t g x -> t (Product f g) x
    forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
           (g :: k -> *).
    ApplicativeT t =>
    t f x -> t g x -> t (Product f g) x
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    t f x -> t g x -> t (Product f g) x
    tprod (t f x -> t g x -> t (Product f g) x)
    -> f (t f x) -> f (t g x -> t (Product f g) x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (t f x)
    a f (t g x -> t (Product f g) x)
    -> f (t g x) -> f (t (Product f g) x)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f (t g x)
    b
      {-# INLINE gprod #-}

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

    instance Applicative f => ApplicativeT (Compose f) where
      tpure :: forall (f :: k' -> *) (x :: k').
    (forall (a :: k'). f a) -> Compose f f x
    tpure forall (a :: k'). f a
    fa
        = f (f x) -> Compose f f x
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f x -> f (f x)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure f x
    forall (a :: k'). f a
    fa)
      {-# INLINE tpure #-}

      tprod :: forall (f :: k' -> *) (x :: k') (g :: k' -> *).
    Compose f f x -> Compose f g x -> Compose f (Product f g) x
    tprod (Compose f (f x)
    fga) (Compose f (g x)
    fha)
        = f (Product f g x) -> Compose f (Product f g) x
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f x -> g x -> Product f g x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (f x -> g x -> Product f g x)
    -> f (f x) -> f (g x -> Product f g x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (f x)
    fga f (g x -> Product f g x) -> f (g x) -> f (Product f g x)
    forall a b. f (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> f (g x)
    fha)
      {-# INLINE tprod #-}

    instance ApplicativeT Reverse where
      tpure :: forall (f :: k' -> *) (x :: k').
    (forall (a :: k'). f a) -> Reverse f x
    tpure forall (a :: k'). f a
    fa
        = f x -> Reverse f x
    forall {k} (f :: k -> *) (a :: k). f a -> Reverse f a
    Reverse f x
    forall (a :: k'). f a
    fa
      {-# INLINE tpure #-}

      tprod :: forall (f :: k' -> *) (x :: k') (g :: k' -> *).
    Reverse f x -> Reverse g x -> Reverse (Product f g) x
    tprod (Reverse f x
    fa) (Reverse g x
    ga)
        = Product f g x -> Reverse (Product f g) x
    forall {k} (f :: k -> *) (a :: k). f a -> Reverse f a
    Reverse (f x -> g x -> Product f g x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f x
    fa g x
    ga)
      {-# INLINE tprod #-}

    instance Alternative f => ApplicativeT (Product f) where
      tpure :: forall (f :: * -> *) x. (forall a. f a) -> Product f f x
    tpure forall a. f a
    fa
        = f x -> f x -> Product f f x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f x
    forall a. f a
    forall (f :: * -> *) a. Alternative f => f a
    empty f x
    forall a. f a
    fa
      {-# INLINE tpure #-}

      tprod :: forall (f :: * -> *) x (g :: * -> *).
    Product f f x -> Product f g x -> Product f (Product f g) x
    tprod (Pair f x
    fl f x
    gl) (Pair f x
    fr g x
    gr)
        = f x -> Product f g x -> Product f (Product f g) x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (f x
    fl f x -> f x -> f x
    forall a. f a -> f a -> f a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> f x
    fr) (f x -> g x -> Product f g x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f x
    gl g x
    gr)
      {-# INLINE tprod #-}

    instance Alternative f => ApplicativeT (Sum f) where
      tpure :: forall (f :: * -> *) x. (forall a. f a) -> Sum f f x
    tpure forall a. f a
    fa
        = f x -> Sum f f x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
    InR f x
    forall a. f a
    fa
      {-# INLINE tpure #-}

      tprod :: forall (f :: * -> *) x (g :: * -> *).
    Sum f f x -> Sum f g x -> Sum f (Product f g) x
    tprod Sum f f x
    l Sum f g x
    r
        = case (Sum f f x
    l, Sum f g x
    r) of
            (InR f x
    gl, InR g x
    gr) -> Product f g x -> Sum f (Product f g) x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
    InR (f x -> g x -> Product f g x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f x
    gl g x
    gr)
            (InR f x
    _,  InL f x
    fr) -> f x -> Sum f (Product f g) x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL f x
    fr
            (InL f x
    fl, InR g x
    _)  -> f x -> Sum f (Product f g) x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL f x
    fl
            (InL f x
    fl, InL f x
    fr) -> f x -> Sum f (Product f g) x
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL (f x
    fl f x -> f x -> f x
    forall a. f a -> f a -> f a
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> f x
    fr)
      {-# INLINE tprod #-}