    {-# LANGUAGE PolyKinds    #-}
    {-# LANGUAGE TypeFamilies #-}
    module Barbies.Generics.Functor
      ( GFunctor(..)
      )

    where

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

    import GHC.TypeLits (Nat)

    class GFunctor (n :: Nat) f g repbf repbg where
      gmap :: Proxy n -> (forall a . f a -> g a) -> repbf x -> repbg x

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

    instance
      ( GFunctor n f g bf bg
      ) => GFunctor n f g (M1 i c bf) (M1 i c bg)
      where
      gmap :: forall (x :: k).
    Proxy n
    -> (forall (a :: k). f a -> g a) -> M1 i c bf x -> M1 i c bg x
    gmap Proxy n
    pn forall (a :: k). f a -> g a
    h = bg x -> M1 i c bg x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (bg x -> M1 i c bg x)
    -> (M1 i c bf x -> bg x) -> M1 i c bf x -> M1 i c bg x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy n -> (forall (a :: k). f a -> g a) -> bf x -> bg x
    forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> bf x -> bg x
    forall {k} {k} (n :: Nat) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (x :: k).
    GFunctor n f g repbf repbg =>
    Proxy n -> (forall (a :: k). f a -> g a) -> repbf x -> repbg x
    gmap Proxy n
    pn f a -> g a
    forall (a :: k). f a -> g a
    h (bf x -> bg x) -> (M1 i c bf x -> bf x) -> M1 i c bf x -> bg x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . M1 i c bf x -> bf x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
    unM1
      {-# INLINE gmap #-}

    instance GFunctor n f g V1 V1 where
      gmap :: forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> V1 x -> V1 x
    gmap Proxy n
    _ forall (a :: k). f a -> g a
    _ V1 x
    _ = V1 x
    forall a. HasCallStack => a
    undefined

    instance GFunctor n f g U1 U1 where
      gmap :: forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> U1 x -> U1 x
    gmap Proxy n
    _ forall (a :: k). f a -> g a
    _ = U1 x -> U1 x
    forall a. a -> a
    id
      {-# INLINE gmap #-}

    instance
      ( GFunctor n f g l l'
      , GFunctor n f g r r'
      )
      => GFunctor n f g (l :*: r) (l' :*: r')
      where
      gmap :: forall (x :: k).
    Proxy n
    -> (forall (a :: k). f a -> g a) -> (:*:) l r x -> (:*:) l' r' x
    gmap Proxy n
    pn forall (a :: k). f a -> g a
    h (l x
    l :*: r x
    r) = (Proxy n -> (forall (a :: k). f a -> g a) -> l x -> l' x
    forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> l x -> l' x
    forall {k} {k} (n :: Nat) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (x :: k).
    GFunctor n f g repbf repbg =>
    Proxy n -> (forall (a :: k). f a -> g a) -> repbf x -> repbg x
    gmap Proxy n
    pn f a -> g a
    forall (a :: k). f a -> g a
    h l x
    l) l' x -> r' x -> (:*:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: Proxy n -> (forall (a :: k). f a -> g a) -> r x -> r' x
    forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> r x -> r' x
    forall {k} {k} (n :: Nat) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (x :: k).
    GFunctor n f g repbf repbg =>
    Proxy n -> (forall (a :: k). f a -> g a) -> repbf x -> repbg x
    gmap Proxy n
    pn f a -> g a
    forall (a :: k). f a -> g a
    h r x
    r
      {-# INLINE gmap #-}

    instance
      ( GFunctor n f g l l'
      , GFunctor n f g r r'
      ) => GFunctor n f g (l :+: r) (l' :+: r')
      where
      gmap :: forall (x :: k).
    Proxy n
    -> (forall (a :: k). f a -> g a) -> (:+:) l r x -> (:+:) l' r' x
    gmap Proxy n
    pn forall (a :: k). f a -> g a
    h = \case
        L1 l x
    l -> l' x -> (:+:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
    L1 (Proxy n -> (forall (a :: k). f a -> g a) -> l x -> l' x
    forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> l x -> l' x
    forall {k} {k} (n :: Nat) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (x :: k).
    GFunctor n f g repbf repbg =>
    Proxy n -> (forall (a :: k). f a -> g a) -> repbf x -> repbg x
    gmap Proxy n
    pn f a -> g a
    forall (a :: k). f a -> g a
    h l x
    l)
        R1 r x
    r -> r' x -> (:+:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
    R1 (Proxy n -> (forall (a :: k). f a -> g a) -> r x -> r' x
    forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> r x -> r' x
    forall {k} {k} (n :: Nat) (f :: k -> *) (g :: k -> *)
           (repbf :: k -> *) (repbg :: k -> *) (x :: k).
    GFunctor n f g repbf repbg =>
    Proxy n -> (forall (a :: k). f a -> g a) -> repbf x -> repbg x
    gmap Proxy n
    pn f a -> g a
    forall (a :: k). f a -> g a
    h r x
    r)
      {-# INLINE gmap #-}

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

    type P = Param

    -- {{ Functor application ------------------------------------
    instance
      GFunctor n f g (Rec (P n f a') (f a))
                     (Rec (P n g a') (g a))
      where
      gmap :: forall (x :: k).
    Proxy n
    -> (forall (a :: k). f a -> g a)
    -> Rec (P n f a') (f a) x
    -> Rec (P n g a') (g a) x
    gmap Proxy n
    _ forall (a :: k). f a -> g a
    h (Rec (K1 f a
    fa)) = K1 R (g a) x -> Rec (P n g a') (g a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (g a -> K1 R (g a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (f a -> g a
    forall (a :: k). f a -> g a
    h f a
    fa))
      {-# INLINE gmap #-}

    instance
      ( Functor h
      ) =>
      GFunctor n f g (Rec (h (P n f a')) (h (f a)))
                     (Rec (h (P n g a')) (h (g a)))
      where
      gmap :: forall (x :: k).
    Proxy n
    -> (forall (a :: k). f a -> g a)
    -> Rec (h (P n f a')) (h (f a)) x
    -> Rec (h (P n g a')) (h (g a)) x
    gmap Proxy n
    _ forall (a :: k). f a -> g a
    h (Rec (K1 h (f a)
    hfa)) = K1 R (h (g a)) x -> Rec (h (P n g a')) (h (g a)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (h (g a) -> K1 R (h (g a)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (f a -> g a
    forall (a :: k). f a -> g a
    h (f a -> g a) -> h (f a) -> h (g a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> h (f a)
    hfa))
      {-# INLINE gmap #-}
    -- }} Functor application ------------------------------------

    -- {{ Not a functor application --------------------------
    instance
      GFunctor n f g (Rec x x) (Rec x x)
      where
      gmap :: forall (x :: k).
    Proxy n -> (forall (a :: k). f a -> g a) -> Rec x x x -> Rec x x x
    gmap Proxy n
    _ forall (a :: k). f a -> g a
    _ = Rec x x x -> Rec x x x
    forall a. a -> a
    id
      {-# INLINE gmap #-}
    -- }} Not a functor application --------------------------