{-# 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 = 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 {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 k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(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 = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
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 = forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
Barbie (forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq 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) = forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
Barbie (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
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
  = forall a x. GenericN a => RepN a x -> a
toN forall a b. (a -> b) -> a -> b
$ 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
Proxy @f) (forall {k} (t :: k). Proxy t
Proxy @g) (forall a x. GenericN a => a -> RepN a x
fromN b f
l) (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
  = forall a x. GenericN a => RepN a x -> a
toN forall a b. (a -> b) -> a -> b
$ 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
Proxy @f) (forall {k} (t :: k). Proxy t
Proxy @(RepN (b f))) (forall {k} (t :: k). Proxy t
Proxy @(RepN (b (f `Product` f)))) 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) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (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 = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (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
Proxy @repf) (forall {k} (t :: k). Proxy t
Proxy @repfg) 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 = 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
_ = 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) 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 = 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 = 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 = (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
Proxy @lf) (forall {k} (t :: k). Proxy t
Proxy @lfg) forall (a :: k). f a
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: 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
Proxy @rf) (forall {k} (t :: k). Proxy t
Proxy @rfg) 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))
    = 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 {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 = 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
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))
    = 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 (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
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 = 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 k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq 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
_ = 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
_ = 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) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
b f -> b g -> b (Product f g)
bprod a f
ll a g
rl) (forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ProductB b =>
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 = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq forall (a :: k). f a
x) (forall k (b :: (k -> *) -> *) (f :: k -> *).
ProductB b =>
(forall (a :: k). f a) -> b f
buniq forall (a :: k). f a
x)
  {-# INLINE buniq #-}