    {-# LANGUAGE PolyKinds            #-}
    {-# LANGUAGE TypeFamilies         #-}
    module Barbies.Generics.Applicative
      ( GApplicative(..)
      )

    where

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

    import Data.Generics.GenericN

    class GApplicative n (f :: k -> Type) (g :: k -> Type) repbf repbg repbfg where
      gprod
        :: Proxy n
        -> Proxy f
        -> Proxy g
        -> repbf x
        -> repbg x
        -> repbfg x

      gpure
        :: (f ~ g, repbf ~ repbg)
        => Proxy n
        -> Proxy f
        -> Proxy repbf
        -> Proxy repbfg
        -> (forall a . f a)
        -> repbf x

    -- ----------------------------------
    -- Trivial cases
    -- ----------------------------------

    instance
      ( GApplicative n f g repf repg repfg
      ) => GApplicative n f g (M1 i c repf)
                              (M1 i c repg)
                              (M1 i c repfg)
      where
      gprod :: forall (x :: k).
    Proxy n
    -> Proxy f
    -> Proxy g
    -> M1 i c repf x
    -> M1 i c repg x
    -> M1 i c repfg x
    gprod Proxy n
    pn Proxy f
    pf Proxy g
    pg (M1 repf x
    l) (M1 repg x
    r)
        = repfg x -> M1 i c repfg x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (Proxy n -> Proxy f -> Proxy g -> repf x -> repg x -> repfg x
    forall (x :: k).
    Proxy n -> Proxy f -> Proxy g -> repf x -> repg x -> repfg x
    forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GApplicative n f g repbf repbg repbfg =>
    Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gprod Proxy n
    pn Proxy f
    pf Proxy g
    pg repf x
    l repg x
    r)
      {-# INLINE gprod #-}

      gpure :: forall (x :: k).
    (f ~ g, M1 i c repf ~ M1 i c repg) =>
    Proxy n
    -> Proxy f
    -> Proxy (M1 i c repf)
    -> Proxy (M1 i c repfg)
    -> (forall (a :: k). f a)
    -> M1 i c repf x
    gpure Proxy n
    pn Proxy f
    pf Proxy (M1 i c repf)
    _ Proxy (M1 i c repfg)
    _ forall (a :: k). f a
    x
        = repf x -> M1 i c repf x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (Proxy n
    -> Proxy f
    -> Proxy repf
    -> Proxy repfg
    -> (forall (a :: k). f a)
    -> repf x
    forall (x :: k).
    (f ~ g, repf ~ repg) =>
    Proxy n
    -> Proxy f
    -> Proxy repf
    -> Proxy repfg
    -> (forall (a :: k). f a)
    -> repf x
    forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy n
    -> Proxy f
    -> Proxy repbf
    -> Proxy repbfg
    -> (forall (a :: k). f a)
    -> repbf x
    gpure Proxy n
    pn Proxy f
    pf (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @repf) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @repfg) f a
    forall (a :: k). f a
    x)
      {-# INLINE gpure #-}

    instance GApplicative n f g U1 U1 U1 where
      gprod :: forall (x :: k).
    Proxy n -> Proxy f -> Proxy g -> U1 x -> U1 x -> U1 x
    gprod Proxy n
    _ Proxy f
    _ Proxy g
    _ U1 x
    U1 U1 x
    U1 = U1 x
    forall k (p :: k). U1 p
    U1
      {-# INLINE gprod #-}

      gpure :: forall (x :: k).
    (f ~ g, U1 ~ U1) =>
    Proxy n
    -> Proxy f
    -> Proxy U1
    -> Proxy U1
    -> (forall (a :: k). f a)
    -> U1 x
    gpure Proxy n
    _ Proxy f
    _ Proxy U1
    _ Proxy U1
    _ forall (a :: k). f a
    _ = U1 x
    forall k (p :: k). U1 p
    U1
      {-# INLINE gpure #-}

    instance
      ( GApplicative n f g lf lg lfg
      , GApplicative n f g rf rg rfg
      ) => GApplicative n f g (lf  :*: rf)
                              (lg  :*: rg)
                              (lfg :*: rfg) where
      gprod :: forall (x :: k).
    Proxy n
    -> Proxy f
    -> Proxy g
    -> (:*:) lf rf x
    -> (:*:) lg rg x
    -> (:*:) lfg rfg x
    gprod Proxy n
    pn Proxy f
    pf Proxy g
    pg (lf x
    l1 :*: rf x
    l2) (lg x
    r1 :*: rg x
    r2)
        = (lf x
    l1 lf x -> lg x -> lfg x
    `lprod` lg x
    r1) lfg x -> rfg x -> (:*:) lfg rfg x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: (rf x
    l2 rf x -> rg x -> rfg x
    `rprod` rg x
    r2)
        where
          lprod :: lf x -> lg x -> lfg x
    lprod = Proxy n -> Proxy f -> Proxy g -> lf x -> lg x -> lfg x
    forall (x :: k).
    Proxy n -> Proxy f -> Proxy g -> lf x -> lg x -> lfg x
    forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GApplicative n f g repbf repbg repbfg =>
    Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gprod Proxy n
    pn Proxy f
    pf Proxy g
    pg
          rprod :: rf x -> rg x -> rfg x
    rprod = Proxy n -> Proxy f -> Proxy g -> rf x -> rg x -> rfg x
    forall (x :: k).
    Proxy n -> Proxy f -> Proxy g -> rf x -> rg x -> rfg x
    forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GApplicative n f g repbf repbg repbfg =>
    Proxy n -> Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gprod Proxy n
    pn Proxy f
    pf Proxy g
    pg
      {-# INLINE gprod #-}

      gpure :: forall (x :: k).
    (f ~ g, (lf :*: rf) ~ (lg :*: rg)) =>
    Proxy n
    -> Proxy f
    -> Proxy (lf :*: rf)
    -> Proxy (lfg :*: rfg)
    -> (forall (a :: k). f a)
    -> (:*:) lf rf x
    gpure Proxy n
    pn Proxy f
    pf Proxy (lf :*: rf)
    _ Proxy (lfg :*: rfg)
    _ forall (a :: k). f a
    x
        =   Proxy n
    -> Proxy f
    -> Proxy lf
    -> Proxy lfg
    -> (forall (a :: k). f a)
    -> lf x
    forall (x :: k).
    (f ~ g, lf ~ lg) =>
    Proxy n
    -> Proxy f
    -> Proxy lf
    -> Proxy lfg
    -> (forall (a :: k). f a)
    -> lf x
    forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy n
    -> Proxy f
    -> Proxy repbf
    -> Proxy repbfg
    -> (forall (a :: k). f a)
    -> repbf x
    gpure Proxy n
    pn Proxy f
    pf (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @lf) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @lfg) f a
    forall (a :: k). f a
    x
        lf x -> rf x -> (:*:) lf rf x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: Proxy n
    -> Proxy f
    -> Proxy rf
    -> Proxy rfg
    -> (forall (a :: k). f a)
    -> rf x
    forall (x :: k).
    (f ~ g, rf ~ rg) =>
    Proxy n
    -> Proxy f
    -> Proxy rf
    -> Proxy rfg
    -> (forall (a :: k). f a)
    -> rf x
    forall {k} {k} k (n :: k) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GApplicative n f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy n
    -> Proxy f
    -> Proxy repbf
    -> Proxy repbfg
    -> (forall (a :: k). f a)
    -> repbf x
    gpure Proxy n
    pn Proxy f
    pf (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @rf) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @rfg) f a
    forall (a :: k). f a
    x
      {-# INLINE gpure #-}

    -- --------------------------------
    -- The interesting cases
    -- --------------------------------

    type P = Param

    -- {{ Functor application -----------------------------------------------------
    instance
      GApplicative n f g (Rec (P n f a) (f a))
                         (Rec (P n g a) (g a))
                         (Rec (P n (f `Product` g) a) ((f `Product` g) a))
      where
      gpure :: forall (x :: k).
    (f ~ g, Rec (P n f a) (f a) ~ Rec (P n g a) (g a)) =>
    Proxy n
    -> Proxy f
    -> Proxy (Rec (P n f a) (f a))
    -> Proxy (Rec (P n (Product f g) a) (Product f g a))
    -> (forall (a :: k). f a)
    -> Rec (P n f a) (f a) x
    gpure Proxy n
    _ Proxy f
    _ Proxy (Rec (P n f a) (f a))
    _ Proxy (Rec (P n (Product f g) a) (Product f g a))
    _ forall (a :: k). f a
    x
        = K1 R (f a) x -> Rec (P n f a) (f a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (f a -> K1 R (f a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 f a
    forall (a :: k). f a
    x)
      {-# INLINE gpure #-}

      gprod :: forall (x :: k).
    Proxy n
    -> Proxy f
    -> Proxy g
    -> Rec (P n f a) (f a) x
    -> Rec (P n g a) (g a) x
    -> Rec (P n (Product f g) a) (Product f g a) x
    gprod Proxy n
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 f a
    fa)) (Rec (K1 g a
    ga))
        = K1 R (Product f g a) x
    -> Rec (P n (Product f g) a) (Product f g a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (Product f g a -> K1 R (Product f g a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (f a -> g a -> Product f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f a
    fa g a
    ga))
      {-# INLINE gprod #-}

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

      gprod :: forall (x :: k).
    Proxy n
    -> Proxy f
    -> Proxy g
    -> Rec (h (P n f a)) (h (f a)) x
    -> Rec (h (P n g a)) (h (g a)) x
    -> Rec (h (P n (Product f g) a)) (h (Product f g a)) x
    gprod Proxy n
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 h (f a)
    fa)) (Rec (K1 h (g a)
    ga))
        = K1 R (h (Product f g a)) x
    -> Rec (h (P n (Product f g) a)) (h (Product f g a)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (h (Product f g a) -> K1 R (h (Product f g a)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (f a -> g a -> Product f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (f a -> g a -> Product f g a)
    -> h (f a) -> h (g a -> Product f g a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> h (f a)
    fa h (g a -> Product f g a) -> h (g a) -> h (Product f g a)
    forall a b. h (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> h (g a)
    ga))
      {-# INLINE gprod #-}
    -- }} Functor application -----------------------------------------------------

    -- {{ Not a functor application -----------------------------------------------
    instance
      ( Monoid x
      ) => GApplicative n f g (Rec x x) (Rec x x) (Rec x x)
      where
      gpure :: forall (x :: k).
    (f ~ g, Rec x x ~ Rec x x) =>
    Proxy n
    -> Proxy f
    -> Proxy (Rec x x)
    -> Proxy (Rec x x)
    -> (forall (a :: k). f a)
    -> Rec x x x
    gpure Proxy n
    _ Proxy f
    _ Proxy (Rec x x)
    _ Proxy (Rec x x)
    _ forall (a :: k). f a
    _
        = K1 R x x -> Rec x x x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (x -> K1 R x x
    forall k i c (p :: k). c -> K1 i c p
    K1 x
    forall a. Monoid a => a
    mempty)
      {-# INLINE gpure #-}

      gprod :: forall (x :: k).
    Proxy n
    -> Proxy f -> Proxy g -> Rec x x x -> Rec x x x -> Rec x x x
    gprod Proxy n
    _ Proxy f
    _ Proxy g
    _ (Rec (K1 x
    l)) (Rec (K1 x
    r))
        = K1 R x x -> Rec x x x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (x -> K1 R x x
    forall k i c (p :: k). c -> K1 i c p
    K1 (x
    l x -> x -> x
    forall a. Semigroup a => a -> a -> a
    <> x
    r))
      {-# INLINE gprod #-}
    -- }} Not a functor application -----------------------------------------------