    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# OPTIONS_GHC -Wno-orphans #-}
    module Barbies.Internal.BareB
      ( Wear, Bare, Covered
      , BareB(..)
      , bstripFrom, bcoverWith
      , WearTwo

      , gbstripDefault
      , gbcoverDefault

      , CanDeriveBareB
      )

    where

    import Barbies.Generics.Bare(GBare(..))
    import Barbies.Internal.FunctorB (FunctorB(..))
    import Barbies.Internal.Wear(Bare, Covered, Wear, WearTwo)
    import Data.Functor.Identity (Identity(..))

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

    -- | Class of Barbie-types defined using 'Wear' and can therefore
    --   have 'Bare' versions. Must satisfy:
    --
    -- @
    -- 'bcover' . 'bstrip' = 'id'
    -- 'bstrip' . 'bcover' = 'id'
    -- @
    class FunctorB (b Covered) => BareB b where
        bstrip :: b Covered Identity -> b Bare Identity
        bcover :: b Bare Identity -> b Covered Identity

        default bstrip :: CanDeriveBareB b => b Covered Identity -> b Bare Identity
        bstrip = b Covered Identity -> b Bare Identity
    forall (b :: * -> (* -> *) -> *).
    CanDeriveBareB b =>
    b Covered Identity -> b Bare Identity
    gbstripDefault

        default bcover :: CanDeriveBareB b => b Bare Identity -> b Covered Identity
        bcover = b Bare Identity -> b Covered Identity
    forall (b :: * -> (* -> *) -> *).
    CanDeriveBareB b =>
    b Bare Identity -> b Covered Identity
    gbcoverDefault

    -- | Generalization of 'bstrip' to arbitrary functors
    bstripFrom :: BareB b => (forall a . f a -> a) -> b Covered f -> b Bare Identity
    bstripFrom :: forall (b :: * -> (* -> *) -> *) (f :: * -> *).
    BareB b =>
    (forall a. f a -> a) -> b Covered f -> b Bare Identity
    bstripFrom forall a. f a -> a
    f
      = b Covered Identity -> b Bare Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Covered Identity -> b Bare Identity
    bstrip (b Covered Identity -> b Bare Identity)
    -> (b Covered f -> b Covered Identity)
    -> b Covered f
    -> b Bare Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (forall a. f a -> Identity a) -> b Covered f -> b Covered Identity
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: * -> *) (g :: * -> *).
    (forall a. f a -> g a) -> b Covered f -> b Covered g
    bmap (a -> Identity a
    forall a. a -> Identity a
    Identity (a -> Identity a) -> (f a -> a) -> f a -> Identity a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . f a -> a
    forall a. f a -> a
    f)

    -- | Generalization of 'bcover' to arbitrary functors
    bcoverWith :: BareB b => (forall a . a -> f a) -> b Bare Identity -> b Covered f
    bcoverWith :: forall (b :: * -> (* -> *) -> *) (f :: * -> *).
    BareB b =>
    (forall a. a -> f a) -> b Bare Identity -> b Covered f
    bcoverWith forall a. a -> f a
    f
      = (forall a. Identity a -> f a) -> b Covered Identity -> b Covered f
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: * -> *) (g :: * -> *).
    (forall a. f a -> g a) -> b Covered f -> b Covered g
    bmap (a -> f a
    forall a. a -> f a
    f (a -> f a) -> (Identity a -> a) -> Identity a -> f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Identity a -> a
    forall a. Identity a -> a
    runIdentity) (b Covered Identity -> b Covered f)
    -> (b Bare Identity -> b Covered Identity)
    -> b Bare Identity
    -> b Covered f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b Bare Identity -> b Covered Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Bare Identity -> b Covered Identity
    bcover

    -- | All types that admit a generic 'FunctorB' instance, and have all
    --   their occurrences of @f@ under a 'Wear' admit a generic 'BareB'
    --   instance.
    type CanDeriveBareB b
      = ( GenericP 0 (b Bare Identity)
        , GenericP 0 (b Covered Identity)
        , GBare 0 (RepP 0 (b Covered Identity)) (RepP 0 (b Bare Identity))
        )

    -- | Default implementation of 'bstrip' based on 'Generic'.
    gbstripDefault :: CanDeriveBareB b => b Covered Identity -> b Bare Identity
    gbstripDefault :: forall (b :: * -> (* -> *) -> *).
    CanDeriveBareB b =>
    b Covered Identity -> b Bare Identity
    gbstripDefault
      = Proxy 0 -> RepP 0 (b Bare Identity) (ZonkAny 1) -> b Bare Identity
    forall (n :: Nat) a x. GenericP n a => Proxy n -> RepP n a x -> a
    forall x. Proxy 0 -> RepP 0 (b Bare Identity) x -> b Bare Identity
    toP (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0) (Zip
       (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
       (Rep (b Bare Identity))
       (ZonkAny 1)
     -> b Bare Identity)
    -> (b Covered Identity
        -> Zip
             (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
             (Rep (b Bare Identity))
             (ZonkAny 1))
    -> b Covered Identity
    -> b Bare Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy 0
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
         (Rep (b Covered Identity))
         (ZonkAny 1)
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
         (Rep (b Bare Identity))
         (ZonkAny 1)
    forall x.
    Proxy 0
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
         (Rep (b Covered Identity))
         x
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
         (Rep (b Bare Identity))
         x
    forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
    GBare n repbi repbb =>
    Proxy n -> repbi x -> repbb x
    gstrip (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0) (Zip
       (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
       (Rep (b Covered Identity))
       (ZonkAny 1)
     -> Zip
          (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
          (Rep (b Bare Identity))
          (ZonkAny 1))
    -> (b Covered Identity
        -> Zip
             (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
             (Rep (b Covered Identity))
             (ZonkAny 1))
    -> b Covered Identity
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
         (Rep (b Bare Identity))
         (ZonkAny 1)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy 0
    -> b Covered Identity -> RepP 0 (b Covered Identity) (ZonkAny 1)
    forall (n :: Nat) a x. GenericP n a => Proxy n -> a -> RepP n a x
    forall x.
    Proxy 0 -> b Covered Identity -> RepP 0 (b Covered Identity) x
    fromP (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0)
    {-# INLINE gbstripDefault #-}

    -- | Default implementation of 'bstrip' based on 'Generic'.
    gbcoverDefault :: CanDeriveBareB b => b Bare Identity -> b Covered Identity
    gbcoverDefault :: forall (b :: * -> (* -> *) -> *).
    CanDeriveBareB b =>
    b Bare Identity -> b Covered Identity
    gbcoverDefault
      = Proxy 0
    -> RepP 0 (b Covered Identity) (ZonkAny 0) -> b Covered Identity
    forall (n :: Nat) a x. GenericP n a => Proxy n -> RepP n a x -> a
    forall x.
    Proxy 0 -> RepP 0 (b Covered Identity) x -> b Covered Identity
    toP (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0) (Zip
       (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
       (Rep (b Covered Identity))
       (ZonkAny 0)
     -> b Covered Identity)
    -> (b Bare Identity
        -> Zip
             (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
             (Rep (b Covered Identity))
             (ZonkAny 0))
    -> b Bare Identity
    -> b Covered Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy 0
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
         (Rep (b Bare Identity))
         (ZonkAny 0)
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
         (Rep (b Covered Identity))
         (ZonkAny 0)
    forall x.
    Proxy 0
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
         (Rep (b Bare Identity))
         x
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
         (Rep (b Covered Identity))
         x
    forall {k} (n :: Nat) (repbi :: k -> *) (repbb :: k -> *) (x :: k).
    GBare n repbi repbb =>
    Proxy n -> repbb x -> repbi x
    gcover (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0) (Zip
       (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
       (Rep (b Bare Identity))
       (ZonkAny 0)
     -> Zip
          (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
          (Rep (b Covered Identity))
          (ZonkAny 0))
    -> (b Bare Identity
        -> Zip
             (Rep (FilterIndex 0 (Indexed b 2) Bare (Param 0 Identity)))
             (Rep (b Bare Identity))
             (ZonkAny 0))
    -> b Bare Identity
    -> Zip
         (Rep (FilterIndex 0 (Indexed b 2) Covered (Param 0 Identity)))
         (Rep (b Covered Identity))
         (ZonkAny 0)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Proxy 0 -> b Bare Identity -> RepP 0 (b Bare Identity) (ZonkAny 0)
    forall (n :: Nat) a x. GenericP n a => Proxy n -> a -> RepP n a x
    forall x. Proxy 0 -> b Bare Identity -> RepP 0 (b Bare Identity) x
    fromP (forall (t :: Nat). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @0)
    {-# INLINE gbcoverDefault #-}

    -- ------------------------------------------------------------
    -- Generic derivation: Special cases for FunctorB
    -- -----------------------------------------------------------
    type P = Param

    instance
      ( BareB b
      ) => GBare 0 (Rec (b Covered (P 0 Identity)) (b Covered Identity))
                   (Rec (b Bare    (P 0 Identity)) (b Bare    Identity))
      where
      gstrip :: forall (x :: k).
    Proxy 0
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    gstrip Proxy 0
    _ = K1 R (b Bare Identity) x
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (b Bare Identity) x
     -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x)
    -> (Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
        -> K1 R (b Bare Identity) x)
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b Bare Identity -> K1 R (b Bare Identity) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b Bare Identity -> K1 R (b Bare Identity) x)
    -> (Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
        -> b Bare Identity)
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    -> K1 R (b Bare Identity) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b Covered Identity -> b Bare Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Covered Identity -> b Bare Identity
    bstrip (b Covered Identity -> b Bare Identity)
    -> (Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
        -> b Covered Identity)
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    -> b Bare Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (b Covered Identity) x -> b Covered Identity
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (b Covered Identity) x -> b Covered Identity)
    -> (Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
        -> K1 R (b Covered Identity) x)
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    -> b Covered Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    -> K1 R (b Covered Identity) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gstrip #-}

      gcover :: forall (x :: k).
    Proxy 0
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    gcover Proxy 0
    _ = K1 R (b Covered Identity) x
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (b Covered Identity) x
     -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x)
    -> (Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
        -> K1 R (b Covered Identity) x)
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    -> Rec (b Covered (Param 0 Identity)) (b Covered Identity) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b Covered Identity -> K1 R (b Covered Identity) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b Covered Identity -> K1 R (b Covered Identity) x)
    -> (Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
        -> b Covered Identity)
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    -> K1 R (b Covered Identity) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .  b Bare Identity -> b Covered Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Bare Identity -> b Covered Identity
    bcover (b Bare Identity -> b Covered Identity)
    -> (Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
        -> b Bare Identity)
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    -> b Covered Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (b Bare Identity) x -> b Bare Identity
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (b Bare Identity) x -> b Bare Identity)
    -> (Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
        -> K1 R (b Bare Identity) x)
    -> Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    -> b Bare Identity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (b Bare (Param 0 Identity)) (b Bare Identity) x
    -> K1 R (b Bare Identity) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gcover #-}

    instance
      ( Functor h
      , BareB b
      ) =>  GBare 0 (Rec (h (b Covered (P 0 Identity))) (h (b Covered Identity)))
                    (Rec (h (b Bare    (P 0 Identity))) (h (b Bare    Identity)))
      where
      gstrip :: forall (x :: k).
    Proxy 0
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    gstrip Proxy 0
    _ = K1 R (h (b Bare Identity)) x
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (h (b Bare Identity)) x
     -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x)
    -> (Rec
          (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
        -> K1 R (h (b Bare Identity)) x)
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . h (b Bare Identity) -> K1 R (h (b Bare Identity)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (h (b Bare Identity) -> K1 R (h (b Bare Identity)) x)
    -> (Rec
          (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
        -> h (b Bare Identity))
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    -> K1 R (h (b Bare Identity)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b Covered Identity -> b Bare Identity)
    -> h (b Covered Identity) -> h (b Bare Identity)
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b Covered Identity -> b Bare Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Covered Identity -> b Bare Identity
    bstrip (h (b Covered Identity) -> h (b Bare Identity))
    -> (Rec
          (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
        -> h (b Covered Identity))
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    -> h (b Bare Identity)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (h (b Covered Identity)) x -> h (b Covered Identity)
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (h (b Covered Identity)) x -> h (b Covered Identity))
    -> (Rec
          (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
        -> K1 R (h (b Covered Identity)) x)
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    -> h (b Covered Identity)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    -> K1 R (h (b Covered Identity)) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gstrip #-}

      gcover :: forall (x :: k).
    Proxy 0
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    gcover Proxy 0
    _ = K1 R (h (b Covered Identity)) x
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (h (b Covered Identity)) x
     -> Rec
          (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x)
    -> (Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
        -> K1 R (h (b Covered Identity)) x)
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    -> Rec
         (h (b Covered (Param 0 Identity))) (h (b Covered Identity)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . h (b Covered Identity) -> K1 R (h (b Covered Identity)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (h (b Covered Identity) -> K1 R (h (b Covered Identity)) x)
    -> (Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
        -> h (b Covered Identity))
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    -> K1 R (h (b Covered Identity)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (b Bare Identity -> b Covered Identity)
    -> h (b Bare Identity) -> h (b Covered Identity)
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b Bare Identity -> b Covered Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Bare Identity -> b Covered Identity
    bcover (h (b Bare Identity) -> h (b Covered Identity))
    -> (Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
        -> h (b Bare Identity))
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    -> h (b Covered Identity)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (h (b Bare Identity)) x -> h (b Bare Identity)
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (h (b Bare Identity)) x -> h (b Bare Identity))
    -> (Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
        -> K1 R (h (b Bare Identity)) x)
    -> Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    -> h (b Bare Identity)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (h (b Bare (Param 0 Identity))) (h (b Bare Identity)) x
    -> K1 R (h (b Bare Identity)) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gcover #-}

    -- This instance is the same as the previous, but for nested Functors
    instance
      ( Functor h
      , Functor m
      , BareB b
      ) =>
           GBare 0 (Rec (m (h (b Covered (P 0 Identity)))) (m (h (b Covered Identity))))
                   (Rec (m (h (b Bare    (P 0 Identity)))) (m (h (b Bare    Identity))))
      where
      gstrip :: forall (x :: k).
    Proxy 0
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    gstrip Proxy 0
    _ = K1 R (m (h (b Bare Identity))) x
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (m (h (b Bare Identity))) x
     -> Rec
          (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x)
    -> (Rec
          (m (h (b Covered (Param 0 Identity))))
          (m (h (b Covered Identity)))
          x
        -> K1 R (m (h (b Bare Identity))) x)
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (h (b Bare Identity)) -> K1 R (m (h (b Bare Identity))) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (m (h (b Bare Identity)) -> K1 R (m (h (b Bare Identity))) x)
    -> (Rec
          (m (h (b Covered (Param 0 Identity))))
          (m (h (b Covered Identity)))
          x
        -> m (h (b Bare Identity)))
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    -> K1 R (m (h (b Bare Identity))) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (h (b Covered Identity) -> h (b Bare Identity))
    -> m (h (b Covered Identity)) -> m (h (b Bare Identity))
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b Covered Identity -> b Bare Identity)
    -> h (b Covered Identity) -> h (b Bare Identity)
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b Covered Identity -> b Bare Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Covered Identity -> b Bare Identity
    bstrip) (m (h (b Covered Identity)) -> m (h (b Bare Identity)))
    -> (Rec
          (m (h (b Covered (Param 0 Identity))))
          (m (h (b Covered Identity)))
          x
        -> m (h (b Covered Identity)))
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    -> m (h (b Bare Identity))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (m (h (b Covered Identity))) x -> m (h (b Covered Identity))
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (m (h (b Covered Identity))) x -> m (h (b Covered Identity)))
    -> (Rec
          (m (h (b Covered (Param 0 Identity))))
          (m (h (b Covered Identity)))
          x
        -> K1 R (m (h (b Covered Identity))) x)
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    -> m (h (b Covered Identity))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec
      (m (h (b Covered (Param 0 Identity))))
      (m (h (b Covered Identity)))
      x
    -> K1 R (m (h (b Covered Identity))) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gstrip #-}

      gcover :: forall (x :: k).
    Proxy 0
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    gcover Proxy 0
    _ = K1 R (m (h (b Covered Identity))) x
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (m (h (b Covered Identity))) x
     -> Rec
          (m (h (b Covered (Param 0 Identity))))
          (m (h (b Covered Identity)))
          x)
    -> (Rec
          (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
        -> K1 R (m (h (b Covered Identity))) x)
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    -> Rec
         (m (h (b Covered (Param 0 Identity))))
         (m (h (b Covered Identity)))
         x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . m (h (b Covered Identity)) -> K1 R (m (h (b Covered Identity))) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (m (h (b Covered Identity)) -> K1 R (m (h (b Covered Identity))) x)
    -> (Rec
          (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
        -> m (h (b Covered Identity)))
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    -> K1 R (m (h (b Covered Identity))) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (h (b Bare Identity) -> h (b Covered Identity))
    -> m (h (b Bare Identity)) -> m (h (b Covered Identity))
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((b Bare Identity -> b Covered Identity)
    -> h (b Bare Identity) -> h (b Covered Identity)
    forall a b. (a -> b) -> h a -> h b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b Bare Identity -> b Covered Identity
    forall (b :: * -> (* -> *) -> *).
    BareB b =>
    b Bare Identity -> b Covered Identity
    bcover) (m (h (b Bare Identity)) -> m (h (b Covered Identity)))
    -> (Rec
          (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
        -> m (h (b Bare Identity)))
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    -> m (h (b Covered Identity))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (m (h (b Bare Identity))) x -> m (h (b Bare Identity))
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (m (h (b Bare Identity))) x -> m (h (b Bare Identity)))
    -> (Rec
          (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
        -> K1 R (m (h (b Bare Identity))) x)
    -> Rec
         (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    -> m (h (b Bare Identity))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (m (h (b Bare (Param 0 Identity)))) (m (h (b Bare Identity))) x
    -> K1 R (m (h (b Bare Identity))) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gcover #-}