    {-# LANGUAGE AllowAmbiguousTypes  #-}
    {-# LANGUAGE PolyKinds            #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# OPTIONS_GHC -Wno-orphans -Wno-deprecations #-}
    module Data.Barbie.Internal.Product
      ( ProductB(buniq, bprod)
      , CanDeriveProductB
      , gbprodDefault, gbuniqDefault
      , GProductB(..)
      )

    where

    import Barbies.Internal.FunctorB (FunctorB)
    import Barbies.Internal.Trivial (Unit)
    import Barbies.Internal.Wrappers (Barbie(..))
    import qualified Barbies.Internal.ApplicativeB as App

    import Data.Functor.Product (Product (..))
    import Data.Kind            (Type)
    import Data.Proxy           (Proxy (..))

    import Data.Generics.GenericN

    {-# DEPRECATED ProductB "Use ApplicativeB" #-}
    {-# DEPRECATED buniq "Use bpure" #-}
    class App.ApplicativeB b => ProductB (b :: (k -> Type) -> Type) where
      bprod :: b f -> b g -> b (f `Product` g)

      buniq :: (forall a . f a) -> b f

      default bprod :: CanDeriveProductB b f g => b f -> b g -> b (f `Product` g)
      bprod = b f -> b g -> b (Product f g)
    forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    CanDeriveProductB b f g =>
    b f -> b g -> b (Product f g)
    gbprodDefault

      default buniq :: CanDeriveProductB b f f => (forall a . f a) -> b f
      buniq = (forall (a :: k). f a) -> b f
    forall {k} (b :: (k -> *) -> *) (f :: k -> *).
    CanDeriveProductB b f f =>
    (forall (a :: k). f a) -> b f
    gbuniqDefault

    type CanDeriveProductB b f g
      = ( GenericN (b f)
        , GenericN (b g)
        , GenericN (b (f `Product` g))
        , GProductB f g (RepN (b f)) (RepN (b g)) (RepN (b (f `Product` g)))
        )

    instance {-# OVERLAPPABLE #-} (ProductB b, FunctorB b) => App.ApplicativeB b where
      bpure :: forall (f :: k -> *). (forall (a :: k). f a) -> b f
    bpure = (forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ProductB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    Data.Barbie.Internal.Product.buniq
      bprod :: forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod = b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ProductB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    Data.Barbie.Internal.Product.bprod

    instance ProductB Unit where

    instance ProductB b => ProductB (Barbie b) where
        buniq :: forall (f :: k -> *). (forall (a :: k). f a) -> Barbie b f
    buniq forall (a :: k). f a
    x = b f -> Barbie b f
    forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
    Barbie ((forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ProductB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    buniq f a
    forall (a :: k). f a
    x)
        bprod :: forall (f :: k -> *) (g :: k -> *).
    Barbie b f -> Barbie b g -> Barbie b (Product f g)
    bprod (Barbie b f
    l) (Barbie b g
    r) = b (Product f g) -> Barbie b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
    Barbie (b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ProductB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod b f
    l b g
    r)

    -- ======================================
    -- Generic derivation of instances
    -- ======================================

    -- | Default implementation of 'bprod' based on 'Generic'.
    gbprodDefault
      :: forall b f g
      .  CanDeriveProductB b f g
      => b f -> b g -> b (f `Product` g)
    gbprodDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    CanDeriveProductB b f g =>
    b f -> b g -> b (Product f g)
    gbprodDefault b f
    l b g
    r
      = RepN (b (Product f g)) Any -> b (Product f g)
    forall a x. GenericN a => RepN a x -> a
    forall x. RepN (b (Product f g)) x -> b (Product f g)
    toN (RepN (b (Product f g)) Any -> b (Product f g))
    -> RepN (b (Product f g)) Any -> b (Product f g)
    forall a b. (a -> b) -> a -> b
    $ Proxy f
    -> Proxy g
    -> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any
    -> Zip (Rep (Indexed b 1 (Param 0 g))) (Rep (b g)) Any
    -> Zip
         (Rep (Indexed b 1 (Param 0 (Product f g))))
         (Rep (b (Product f g)))
         Any
    forall x.
    Proxy f
    -> Proxy g
    -> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) x
    -> Zip (Rep (Indexed b 1 (Param 0 g))) (Rep (b g)) x
    -> Zip
         (Rep (Indexed b 1 (Param 0 (Product f g))))
         (Rep (b (Product f g)))
         x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GProductB f g repbf repbg repbfg =>
    Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gbprod (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @f) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @g) (b f -> RepN (b f) Any
    forall x. b f -> RepN (b f) x
    forall a x. GenericN a => a -> RepN a x
    fromN b f
    l) (b g -> RepN (b g) Any
    forall x. b g -> RepN (b g) x
    forall a x. GenericN a => a -> RepN a x
    fromN b g
    r)
    {-# INLINE gbprodDefault #-}

    gbuniqDefault:: forall b f . CanDeriveProductB b f f => (forall a . f a) -> b f
    gbuniqDefault :: forall {k} (b :: (k -> *) -> *) (f :: k -> *).
    CanDeriveProductB b f f =>
    (forall (a :: k). f a) -> b f
    gbuniqDefault forall (a :: k). f a
    x
      = RepN (b f) Any -> b f
    forall a x. GenericN a => RepN a x -> a
    forall x. RepN (b f) x -> b f
    toN (RepN (b f) Any -> b f) -> RepN (b f) Any -> b f
    forall a b. (a -> b) -> a -> b
    $ Proxy f
    -> Proxy (Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)))
    -> Proxy
         (Zip
            (Rep (Indexed b 1 (Param 0 (Product f f))))
            (Rep (b (Product f f))))
    -> (forall (a :: k). f a)
    -> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any
    forall x.
    (f ~ f,
     Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f))
     ~ Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f))) =>
    Proxy f
    -> Proxy (Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)))
    -> Proxy
         (Zip
            (Rep (Indexed b 1 (Param 0 (Product f f))))
            (Rep (b (Product f f))))
    -> (forall (a :: k). f a)
    -> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy f
    -> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
    gbuniq (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @f) (forall {k} (t :: k). Proxy t
    forall (t :: * -> *). Proxy t
    Proxy @(RepN (b f))) (forall {k} (t :: k). Proxy t
    forall (t :: * -> *). Proxy t
    Proxy @(RepN (b (f `Product` f)))) f a
    forall (a :: k). f a
    x
    {-# INLINE gbuniqDefault #-}

    class GProductB (f :: k -> Type) (g :: k -> Type) repbf repbg repbfg where
      gbprod :: Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x

      gbuniq :: (f ~ g, repbf ~ repbg) => Proxy f -> Proxy repbf -> Proxy repbfg -> (forall a . f a) -> repbf x

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

    instance GProductB f g repf repg repfg => GProductB f g (M1 i c repf)
                                                            (M1 i c repg)
                                                            (M1 i c repfg) where
      gbprod :: forall (x :: k).
    Proxy f
    -> Proxy g -> M1 i c repf x -> M1 i c repg x -> M1 i c repfg x
    gbprod Proxy f
    pf Proxy g
    pg (M1 repf x
    l) (M1 repg x
    r) = repfg x -> M1 i c repfg x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (Proxy f -> Proxy g -> repf x -> repg x -> repfg x
    forall (x :: k). Proxy f -> Proxy g -> repf x -> repg x -> repfg x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GProductB f g repbf repbg repbfg =>
    Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gbprod Proxy f
    pf Proxy g
    pg repf x
    l repg x
    r)
      {-# INLINE gbprod #-}

      gbuniq :: forall (x :: k).
    (f ~ g, M1 i c repf ~ M1 i c repg) =>
    Proxy f
    -> Proxy (M1 i c repf)
    -> Proxy (M1 i c repfg)
    -> (forall (a :: k). f a)
    -> M1 i c repf x
    gbuniq Proxy f
    pf Proxy (M1 i c repf)
    _ Proxy (M1 i c repfg)
    _ forall (a :: k). f a
    x = repf x -> M1 i c repf x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (Proxy f
    -> Proxy repf -> Proxy repfg -> (forall (a :: k). f a) -> repf x
    forall (x :: k).
    (f ~ g, repf ~ repg) =>
    Proxy f
    -> Proxy repf -> Proxy repfg -> (forall (a :: k). f a) -> repf x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy f
    -> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
    gbuniq Proxy f
    pf (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @repf) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @repfg) f a
    forall (a :: k). f a
    x)
      {-# INLINE gbuniq #-}

    instance GProductB f g U1 U1 U1 where
      gbprod :: forall (x :: k). Proxy f -> Proxy g -> U1 x -> U1 x -> U1 x
    gbprod Proxy f
    _ Proxy g
    _ U1 x
    U1 U1 x
    U1 = U1 x
    forall k (p :: k). U1 p
    U1
      {-# INLINE gbprod #-}

      gbuniq :: forall (x :: k).
    (f ~ g, U1 ~ U1) =>
    Proxy f -> Proxy U1 -> Proxy U1 -> (forall (a :: k). f a) -> U1 x
    gbuniq Proxy f
    _ Proxy U1
    _ Proxy U1
    _ forall (a :: k). f a
    _ = U1 x
    forall k (p :: k). U1 p
    U1
      {-# INLINE gbuniq #-}

    instance
      ( GProductB f g lf lg lfg
      , GProductB f g rf rg rfg
      ) => GProductB f g (lf  :*: rf)
                         (lg  :*: rg)
                         (lfg :*: rfg) where
      gbprod :: forall (x :: k).
    Proxy f
    -> Proxy g -> (:*:) lf rf x -> (:*:) lg rg x -> (:*:) lfg rfg x
    gbprod Proxy f
    pf Proxy g
    pg (lf x
    l1 :*: rf x
    l2) (lg x
    r1 :*: rg x
    r2)
        = (lf x
    l1 lf x -> lg x -> lfg x
    `lprod` lg x
    r1) lfg x -> rfg x -> (:*:) lfg rfg x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: (rf x
    l2 rf x -> rg x -> rfg x
    `rprod` rg x
    r2)
        where
          lprod :: lf x -> lg x -> lfg x
    lprod = Proxy f -> Proxy g -> lf x -> lg x -> lfg x
    forall (x :: k). Proxy f -> Proxy g -> lf x -> lg x -> lfg x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GProductB f g repbf repbg repbfg =>
    Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gbprod Proxy f
    pf Proxy g
    pg
          rprod :: rf x -> rg x -> rfg x
    rprod = Proxy f -> Proxy g -> rf x -> rg x -> rfg x
    forall (x :: k). Proxy f -> Proxy g -> rf x -> rg x -> rfg x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    GProductB f g repbf repbg repbfg =>
    Proxy f -> Proxy g -> repbf x -> repbg x -> repbfg x
    gbprod Proxy f
    pf Proxy g
    pg
      {-# INLINE gbprod #-}

      gbuniq :: forall (x :: k).
    (f ~ g, (lf :*: rf) ~ (lg :*: rg)) =>
    Proxy f
    -> Proxy (lf :*: rf)
    -> Proxy (lfg :*: rfg)
    -> (forall (a :: k). f a)
    -> (:*:) lf rf x
    gbuniq Proxy f
    pf Proxy (lf :*: rf)
    _ Proxy (lfg :*: rfg)
    _ forall (a :: k). f a
    x = (Proxy f -> Proxy lf -> Proxy lfg -> (forall (a :: k). f a) -> lf x
    forall (x :: k).
    (f ~ g, lf ~ lg) =>
    Proxy f -> Proxy lf -> Proxy lfg -> (forall (a :: k). f a) -> lf x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy f
    -> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
    gbuniq Proxy f
    pf (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @lf) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @lfg) f a
    forall (a :: k). f a
    x lf x -> rf x -> (:*:) lf rf x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: Proxy f -> Proxy rf -> Proxy rfg -> (forall (a :: k). f a) -> rf x
    forall (x :: k).
    (f ~ g, rf ~ rg) =>
    Proxy f -> Proxy rf -> Proxy rfg -> (forall (a :: k). f a) -> rf x
    forall {k} k (f :: k -> *) (g :: k -> *) (repbf :: k -> *)
           (repbg :: k -> *) (repbfg :: k -> *) (x :: k).
    (GProductB f g repbf repbg repbfg, f ~ g, repbf ~ repbg) =>
    Proxy f
    -> Proxy repbf -> Proxy repbfg -> (forall (a :: k). f a) -> repbf x
    gbuniq Proxy f
    pf (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @rf) (forall {k} (t :: k). Proxy t
    forall (t :: k -> *). Proxy t
    Proxy @rfg) f a
    forall (a :: k). f a
    x)
      {-# INLINE gbuniq #-}

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

    type P0 = Param 0

    instance GProductB f g (Rec (P0 f a_or_pma) (f a))
                           (Rec (P0 g a_or_pma) (g a))
                           (Rec (P0 (f `Product` g) a_or_pma) ((f `Product` g) a)) where
      gbprod :: forall (x :: k).
    Proxy f
    -> Proxy g
    -> Rec (P0 f a_or_pma) (f a) x
    -> Rec (P0 g a_or_pma) (g a) x
    -> Rec (P0 (Product f g) a_or_pma) (Product f g a) x
    gbprod Proxy f
    _ Proxy g
    _ (Rec (K1 f a
    fa)) (Rec (K1 g a
    ga))
        = K1 R (Product f g a) x
    -> Rec (P0 (Product f g) a_or_pma) (Product f g a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (Product f g a -> K1 R (Product f g a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (f a -> g a -> Product f g a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair f a
    fa g a
    ga))
      {-# INLINE gbprod #-}

      gbuniq :: forall (x :: k).
    (f ~ g, Rec (P0 f a_or_pma) (f a) ~ Rec (P0 g a_or_pma) (g a)) =>
    Proxy f
    -> Proxy (Rec (P0 f a_or_pma) (f a))
    -> Proxy (Rec (P0 (Product f g) a_or_pma) (Product f g a))
    -> (forall (a :: k). f a)
    -> Rec (P0 f a_or_pma) (f a) x
    gbuniq Proxy f
    _ Proxy (Rec (P0 f a_or_pma) (f a))
    _ Proxy (Rec (P0 (Product f g) a_or_pma) (Product f g a))
    _ forall (a :: k). f a
    x = K1 R (f a) x -> Rec (P0 f a_or_pma) (f a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (f a -> K1 R (f a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 f a
    forall (a :: k). f a
    x)
      {-# INLINE gbuniq #-}

    -- b' is b, maybe with 'Param' annotations
    instance
      ( ProductB b
      ) => GProductB f g (Rec (b' (P0 f)) (b f))
                         (Rec (b' (P0 g)) (b g))
                         (Rec (b' (P0 (f `Product` g))) (b (f `Product` g))) where
      gbprod :: forall (x :: k).
    Proxy f
    -> Proxy g
    -> Rec (b' (P0 f)) (b f) x
    -> Rec (b' (P0 g)) (b g) x
    -> Rec (b' (P0 (Product f g))) (b (Product f g)) x
    gbprod Proxy f
    _ Proxy g
    _ (Rec (K1 b f
    bf)) (Rec (K1 b g
    bg))
        = K1 R (b (Product f g)) x
    -> Rec (b' (P0 (Product f g))) (b (Product f g)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (b (Product f g) -> K1 R (b (Product f g)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ProductB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg))
      {-# INLINE gbprod #-}

      gbuniq :: forall (x :: k).
    (f ~ g, Rec (b' (P0 f)) (b f) ~ Rec (b' (P0 g)) (b g)) =>
    Proxy f
    -> Proxy (Rec (b' (P0 f)) (b f))
    -> Proxy (Rec (b' (P0 (Product f g))) (b (Product f g)))
    -> (forall (a :: k). f a)
    -> Rec (b' (P0 f)) (b f) x
    gbuniq Proxy f
    _ Proxy (Rec (b' (P0 f)) (b f))
    _ Proxy (Rec (b' (P0 (Product f g))) (b (Product f g)))
    _ forall (a :: k). f a
    x = K1 R (b f) x -> Rec (b' (P0 f)) (b f) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (b f -> K1 R (b f) x
    forall k i c (p :: k). c -> K1 i c p
    K1 ((forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ProductB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    buniq f a
    forall (a :: k). f a
    x))
      {-# INLINE gbuniq #-}

    -- --------------------------------
    -- Instances for base types
    -- --------------------------------

    instance ProductB Proxy where
      bprod :: forall (f :: k -> *) (g :: k -> *).
    Proxy f -> Proxy g -> Proxy (Product f g)
    bprod Proxy f
    _ Proxy g
    _ = Proxy (Product f g)
    forall {k} (t :: k). Proxy t
    Proxy
      {-# INLINE bprod #-}

      buniq :: forall (f :: k -> *). (forall (a :: k). f a) -> Proxy f
    buniq forall (a :: k). f a
    _ = Proxy f
    forall {k} (t :: k). Proxy t
    Proxy
      {-# INLINE buniq #-}

    instance (ProductB a, ProductB b) => ProductB (Product a b) where
      bprod :: forall (f :: k -> *) (g :: k -> *).
    Product a b f -> Product a b g -> Product a b (Product f g)
    bprod (Pair a f
    ll b f
    lr) (Pair a g
    rl b g
    rr) = a (Product f g) -> b (Product f g) -> Product a b (Product f g)
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (a f -> a g -> a (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ProductB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). a f -> a g -> a (Product f g)
    bprod a f
    ll a g
    rl) (b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ProductB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    bprod b f
    lr b g
    rr)
      {-# INLINE bprod #-}

      buniq :: forall (f :: k -> *). (forall (a :: k). f a) -> Product a b f
    buniq forall (a :: k). f a
    x = a f -> b f -> Product a b f
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair ((forall (a :: k). f a) -> a f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ProductB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> a f
    buniq f a
    forall (a :: k). f a
    x) ((forall (a :: k). f a) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ProductB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    buniq f a
    forall (a :: k). f a
    x)
      {-# INLINE buniq #-}