    {-# 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 = repbb x -> M1 i k repbb x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (repbb x -> M1 i k repbb x)
    -> (M1 i k repbi x -> repbb x) -> M1 i k repbi x -> M1 i k repbb x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy n -> repbi x -> repbb x
    forall (x :: k). Proxy n -> repbi x -> repbb x
    forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
    GBare n repbi repbb =>
    Proxy n -> repbi x -> repbb x
    gstrip Proxy n
    pn (repbi x -> repbb x)
    -> (M1 i k repbi x -> repbi x) -> M1 i k repbi x -> repbb x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . M1 i k repbi x -> repbi x
    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 = repbi x -> M1 i k repbi x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (repbi x -> M1 i k repbi x)
    -> (M1 i k repbb x -> repbi x) -> M1 i k repbb x -> M1 i k repbi x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy n -> repbb x -> repbi x
    forall (x :: k). Proxy n -> repbb x -> repbi x
    forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
    GBare n repbi repbb =>
    Proxy n -> repbb x -> repbi x
    gcover Proxy n
    pn (repbb x -> repbi x)
    -> (M1 i k repbb x -> repbb x) -> M1 i k repbb x -> repbi x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . M1 i k repbb x -> repbb x
    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
    _ = V1 x
    forall a. HasCallStack => a
    undefined
      gcover :: forall (x :: k). Proxy n -> V1 x -> V1 x
    gcover Proxy n
    _ V1 x
    _ = 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
    _ = U1 x -> U1 x
    forall a. a -> a
    id
      {-# INLINE gstrip #-}

      gcover :: forall (x :: k). Proxy n -> U1 x -> U1 x
    gcover Proxy n
    _ = U1 x -> U1 x
    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) = (Proxy n -> l x -> l' x
    forall (x :: k). Proxy n -> l x -> l' x
    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) l' x -> r' x -> (:*:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: Proxy n -> r x -> r' x
    forall (x :: k). Proxy n -> r x -> r' x
    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) = (Proxy n -> l' x -> l x
    forall (x :: k). Proxy n -> l' x -> l x
    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) l x -> r x -> (:*:) l r x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: Proxy n -> r' x -> r x
    forall (x :: k). Proxy n -> r' x -> r x
    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 -> l' x -> (:+:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
    L1 (Proxy n -> l x -> l' x
    forall (x :: k). Proxy n -> l x -> l' x
    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 -> r' x -> (:+:) l' r' x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
    R1 (Proxy n -> r x -> r' x
    forall (x :: k). Proxy n -> r x -> r' x
    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 -> l x -> (:+:) l r x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
    L1 (Proxy n -> l' x -> l x
    forall (x :: k). Proxy n -> l' x -> l x
    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 -> r x -> (:+:) l r x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
    R1 (Proxy n -> r' x -> r x
    forall (x :: k). Proxy n -> r' x -> r x
    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
    _ = Rec (P n Identity a) (Identity a) x -> Rec b b x
    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
    _ = Rec b b x -> Rec (P n Identity a) (Identity a) x
    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
    _ = Rec repbi repbi x -> Rec repbi repbi x
    Rec repbi repbi x -> Rec repbb repbb x
    forall a. a -> a
    id
      {-# INLINE gstrip #-}

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