{-# 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 = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (a :: k). f a -> g a
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_ = 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
_ = 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) = (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 forall (a :: k). f a -> g a
h l x
l) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: 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 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 -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (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 forall (a :: k). f a -> g a
h l x
l)
    R1 r x
r -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (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 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)) = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (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)) = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec (forall k i c (p :: k). c -> K1 i c p
K1 (forall (a :: k). f a -> g a
h 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
_ = forall a. a -> a
id
  {-# INLINE gmap #-}
-- }} Not a functor application --------------------------