{-# LANGUAGE PolyKinds    #-}
{-# LANGUAGE TypeFamilies #-}
module Barbies.Generics.Bare
  ( GBare(..)
  )

where

import Data.Functor.Identity (Identity(..))

import Data.Coerce (Coercible, coerce)
import Data.Generics.GenericN
import Data.Proxy (Proxy(..))
import GHC.TypeLits (Nat)


class GBare (n :: Nat) repbi repbb where
  gstrip :: Proxy n -> repbi x -> repbb x
  gcover :: Proxy n -> repbb x -> repbi x

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

instance GBare n repbi repbb => GBare n (M1 i k repbi) (M1 i k repbb) where
  gstrip :: forall (x :: k). Proxy n -> M1 i k repbi x -> M1 i k repbb x
gstrip Proxy n
pn = 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} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn 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 gstrip #-}

  gcover :: forall (x :: k). Proxy n -> M1 i k repbb x -> M1 i k repbi x
gcover Proxy n
pn = 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} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn 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 gcover #-}


instance GBare n V1 V1 where
  gstrip :: forall (x :: k). Proxy n -> V1 x -> V1 x
gstrip Proxy n
_ V1 x
_ = forall a. HasCallStack => a
undefined
  gcover :: forall (x :: k). Proxy n -> V1 x -> V1 x
gcover Proxy n
_ V1 x
_ = forall a. HasCallStack => a
undefined

instance GBare n U1 U1 where
  gstrip :: forall (x :: k). Proxy n -> U1 x -> U1 x
gstrip Proxy n
_ = forall a. a -> a
id
  {-# INLINE gstrip #-}

  gcover :: forall (x :: k). Proxy n -> U1 x -> U1 x
gcover Proxy n
_ = forall a. a -> a
id
  {-# INLINE gcover #-}


instance (GBare n l l', GBare n r r') => GBare n (l :*: r) (l' :*: r') where
  gstrip :: forall (x :: k). Proxy n -> (:*:) l r x -> (:*:) l' r' x
gstrip Proxy n
pn (l x
l :*: r x
r) = (forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn l x
l) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn r x
r
  {-# INLINE gstrip #-}

  gcover :: forall (x :: k). Proxy n -> (:*:) l' r' x -> (:*:) l r x
gcover Proxy n
pn (l' x
l :*: r' x
r) = (forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn l' x
l) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn r' x
r
  {-# INLINE gcover #-}


instance (GBare n l l', GBare n r r') => GBare n (l :+: r) (l' :+: r') where
  gstrip :: forall (x :: k). Proxy n -> (:+:) l r x -> (:+:) l' r' x
gstrip Proxy n
pn = \case
    L1 l x
l -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn l x
l)
    R1 r x
r -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbi x -> repbb x
gstrip Proxy n
pn r x
r)
  {-# INLINE gstrip #-}

  gcover :: forall (x :: k). Proxy n -> (:+:) l' r' x -> (:+:) l r x
gcover Proxy n
pn = \case
    L1 l' x
l -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn l' x
l)
    R1 r' x
r -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
GBare n repbi repbb =>
Proxy n -> repbb x -> repbi x
gcover Proxy n
pn r' x
r)
  {-# INLINE gcover #-}

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

type P = Param

instance Coercible a b => GBare n (Rec (P n Identity a) (Identity a)) (Rec b b) where
  gstrip :: forall (x :: k).
Proxy n -> Rec (P n Identity a) (Identity a) x -> Rec b b x
gstrip Proxy n
_ = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE gstrip #-}

  gcover :: forall (x :: k).
Proxy n -> Rec b b x -> Rec (P n Identity a) (Identity a) x
gcover Proxy n
_ = coerce :: forall a b. Coercible a b => a -> b
coerce
  {-# INLINE gcover #-}

instance repbi ~ repbb => GBare n (Rec repbi repbi) (Rec repbb repbb) where
  gstrip :: forall (x :: k). Proxy n -> Rec repbi repbi x -> Rec repbb repbb x
gstrip Proxy n
_ = forall a. a -> a
id
  {-# INLINE gstrip #-}

  gcover :: forall (x :: k). Proxy n -> Rec repbb repbb x -> Rec repbi repbi x
gcover Proxy n
_ = forall a. a -> a
id
  {-# INLINE gcover #-}