    {-# LANGUAGE PolyKinds    #-}
    {-# LANGUAGE TypeFamilies #-}
    module Barbies.Generics.Distributive
      ( GDistributive(..)
      )

    where

    import Data.Generics.GenericN
    import Data.Proxy (Proxy (..))

    import Data.Functor.Compose   (Compose (..))
    import Data.Distributive      (Distributive(..))

    import GHC.TypeLits (Nat)

    class (Functor f) => GDistributive (n :: Nat) f repbg repbfg where
      gdistribute :: Proxy n -> f (repbg x) -> repbfg x

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

    instance
      ( GDistributive n f bg bfg
      ) => GDistributive n f (M1 i c bg) (M1 i c bfg)
      where
      gdistribute :: forall (x :: k). Proxy n -> f (M1 i c bg x) -> M1 i c bfg x
    gdistribute Proxy n
    pn = bfg x -> M1 i c bfg x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (bfg x -> M1 i c bfg x)
    -> (f (M1 i c bg x) -> bfg x) -> f (M1 i c bg x) -> M1 i c bfg x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy n -> f (bg x) -> bfg x
    forall (x :: k). Proxy n -> f (bg x) -> bfg x
    forall {k} (n :: Nat) (f :: * -> *) (repbg :: k -> *)
           (repbfg :: k -> *) (x :: k).
    GDistributive n f repbg repbfg =>
    Proxy n -> f (repbg x) -> repbfg x
    gdistribute Proxy n
    pn (f (bg x) -> bfg x)
    -> (f (M1 i c bg x) -> f (bg x)) -> f (M1 i c bg x) -> bfg x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (M1 i c bg x -> bg x) -> f (M1 i c bg x) -> f (bg x)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap M1 i c bg x -> bg x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
    unM1
      {-# INLINE gdistribute #-}

    instance
      ( Functor f
      ) => GDistributive n f U1 U1
      where
      gdistribute :: forall (x :: k). Proxy n -> f (U1 x) -> U1 x
    gdistribute Proxy n
    _ = U1 x -> f (U1 x) -> U1 x
    forall a b. a -> b -> a
    const U1 x
    forall k (p :: k). U1 p
    U1
      {-# INLINE gdistribute #-}

    fstF :: (l :*: r) a -> l a
    fstF :: forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> l a
    fstF (l a
    x :*: r a
    _y) = l a
    x

    sndF :: (l :*: r) a -> r a
    sndF :: forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> r a
    sndF (l a
    _x :*: r a
    y) = r a
    y

    instance
      ( GDistributive n f l l'
      , GDistributive n f r r'
      )
      => GDistributive n f (l :*: r) (l' :*: r')
      where
      gdistribute :: forall (x :: k). Proxy n -> f ((:*:) l r x) -> (:*:) l' r' x
    gdistribute Proxy n
    pn f ((:*:) l r x)
    lr = Proxy n -> f (l x) -> l' x
    forall (x :: k). Proxy n -> f (l x) -> l' x
    forall {k} (n :: Nat) (f :: * -> *) (repbg :: k -> *)
           (repbfg :: k -> *) (x :: k).
    GDistributive n f repbg repbfg =>
    Proxy n -> f (repbg x) -> repbfg x
    gdistribute Proxy n
    pn ((:*:) l r x -> l x
    forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> l a
    fstF ((:*:) l r x -> l x) -> f ((:*:) l r x) -> f (l x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f ((:*:) l r x)
    lr) l' x -> r' x -> (:*:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: Proxy n -> f (r x) -> r' x
    forall (x :: k). Proxy n -> f (r x) -> r' x
    forall {k} (n :: Nat) (f :: * -> *) (repbg :: k -> *)
           (repbfg :: k -> *) (x :: k).
    GDistributive n f repbg repbfg =>
    Proxy n -> f (repbg x) -> repbfg x
    gdistribute Proxy n
    pn ((:*:) l r x -> r x
    forall {k} (l :: k -> *) (r :: k -> *) (a :: k). (:*:) l r a -> r a
    sndF ((:*:) l r x -> r x) -> f ((:*:) l r x) -> f (r x)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f ((:*:) l r x)
    lr)
      {-# INLINE gdistribute #-}

    -- ---------------------------------------------------------
    -- The interesting cases.
    -- There are more interesting cases for specific values of n
    -- ---------------------------------------------------------

    type P = Param

    instance
      ( Functor f
      ) =>
      GDistributive n f (Rec (P n g a) (g a)) (Rec (P n (Compose f g) a) (Compose f g a))
      where
      gdistribute :: forall (x :: k).
    Proxy n
    -> f (Rec (P n g a) (g a) x)
    -> Rec (P n (Compose f g) a) (Compose f g a) x
    gdistribute Proxy n
    _ = K1 R (Compose f g a) x
    -> Rec (P n (Compose f g) a) (Compose f g a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (Compose f g a) x
     -> Rec (P n (Compose f g) a) (Compose f g a) x)
    -> (f (Rec (P n g a) (g a) x) -> K1 R (Compose f g a) x)
    -> f (Rec (P n g a) (g a) x)
    -> Rec (P n (Compose f g) a) (Compose f g a) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Compose f g a -> K1 R (Compose f g a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (Compose f g a -> K1 R (Compose f g a) x)
    -> (f (Rec (P n g a) (g a) x) -> Compose f g a)
    -> f (Rec (P n g a) (g a) x)
    -> K1 R (Compose f g a) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (g a) -> Compose f g a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (f (g a) -> Compose f g a)
    -> (f (Rec (P n g a) (g a) x) -> f (g a))
    -> f (Rec (P n g a) (g a) x)
    -> Compose f g a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (g a) -> f (g a)
    forall a. a -> a
    id (f (g a) -> f (g a))
    -> (f (Rec (P n g a) (g a) x) -> f (g a))
    -> f (Rec (P n g a) (g a) x)
    -> f (g a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Rec (P n g a) (g a) x -> g a)
    -> f (Rec (P n g a) (g a) x) -> f (g a)
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (K1 R (g a) x -> g a
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (g a) x -> g a)
    -> (Rec (P n g a) (g a) x -> K1 R (g a) x)
    -> Rec (P n g a) (g a) x
    -> g a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (P n g a) (g a) x -> K1 R (g a) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec)
      {-# INLINE gdistribute #-}

    instance
      ( Functor f
      , Distributive h
      ) =>
      GDistributive n f (Rec (h (P n g a)) (h (g a))) (Rec (h (P n (Compose f g) a)) (h (Compose f g a)))
      where
      gdistribute :: forall (x :: k).
    Proxy n
    -> f (Rec (h (P n g a)) (h (g a)) x)
    -> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
    gdistribute Proxy n
    _ = K1 R (h (Compose f g a)) x
    -> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (h (Compose f g a)) x
     -> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x)
    -> (f (Rec (h (P n g a)) (h (g a)) x)
        -> K1 R (h (Compose f g a)) x)
    -> f (Rec (h (P n g a)) (h (g a)) x)
    -> Rec (h (P n (Compose f g) a)) (h (Compose f g a)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . h (Compose f g a) -> K1 R (h (Compose f g a)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (h (Compose f g a) -> K1 R (h (Compose f g a)) x)
    -> (f (Rec (h (P n g a)) (h (g a)) x) -> h (Compose f g a))
    -> f (Rec (h (P n g a)) (h (g a)) x)
    -> K1 R (h (Compose f g a)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (f (g a) -> Compose f g a) -> h (f (g a)) -> h (Compose f g a)
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap f (g a) -> Compose f g a
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (h (f (g a)) -> h (Compose f g a))
    -> (f (Rec (h (P n g a)) (h (g a)) x) -> h (f (g a)))
    -> f (Rec (h (P n g a)) (h (g a)) x)
    -> h (Compose f g a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f (h (g a)) -> h (f (g a))
    forall (g :: * -> *) (f :: * -> *) a.
    (Distributive g, Functor f) =>
    f (g a) -> g (f a)
    forall (f :: * -> *) a. Functor f => f (h a) -> h (f a)
    distribute (f (h (g a)) -> h (f (g a)))
    -> (f (Rec (h (P n g a)) (h (g a)) x) -> f (h (g a)))
    -> f (Rec (h (P n g a)) (h (g a)) x)
    -> h (f (g a))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Rec (h (P n g a)) (h (g a)) x -> h (g a))
    -> f (Rec (h (P n g a)) (h (g a)) x) -> f (h (g a))
    forall a b. (a -> b) -> f a -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (K1 R (h (g a)) x -> h (g a)
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (h (g a)) x -> h (g a))
    -> (Rec (h (P n g a)) (h (g a)) x -> K1 R (h (g a)) x)
    -> Rec (h (P n g a)) (h (g a)) x
    -> h (g a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (h (P n g a)) (h (g a)) x -> K1 R (h (g a)) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec)
      {-# INLINE gdistribute #-}