{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-deprecations #-}
module Data.Barbie.Internal.ProductC
  ( ProductBC(..)
  , buniqC

  , CanDeriveProductBC
  , GAll
  , GProductBC(..)
  , gbdictsDefault
  )

where

import Barbies.Generics.Constraints(GAll, Self, Other, X)
import Barbies.Internal.ConstraintsB(ConstraintsB(..), GAllRepB)
import Barbies.Internal.Dicts(Dict (..), requiringDict)
import Barbies.Internal.FunctorB(FunctorB(bmap))
import Barbies.Internal.Trivial(Unit(..))
import Barbies.Internal.Wrappers(Barbie(..))

import Data.Barbie.Internal.Product(ProductB(..))
import Data.Generics.GenericN

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

class (ConstraintsB b, ProductB b) => ProductBC (b :: (k -> Type) -> Type) where
  bdicts :: AllB c b => b (Dict c)

  default bdicts :: (CanDeriveProductBC c b, AllB c b) => b (Dict c)
  bdicts = b (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(CanDeriveProductBC c b, AllB c b) =>
b (Dict c)
gbdictsDefault


type CanDeriveProductBC c b
  = ( GenericN (b (Dict c))
    , AllB c b ~ GAll 0 c (GAllRepB b)
    , GProductBC c (GAllRepB b) (RepN (b (Dict c)))
    )

{-# DEPRECATED buniqC "Use bpureC instead" #-}
buniqC :: forall c f b . (AllB c b, ProductBC b) => (forall a . c a => f a) -> b f
buniqC :: (forall (a :: k). c a => f a) -> b f
buniqC forall (a :: k). c a => f a
x
  = (forall (a :: k). Dict c a -> f a) -> b (Dict c) -> b f
forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap ((c a => f a) -> Dict c a -> f a
forall k (c :: k -> Constraint) (a :: k) r.
(c a => r) -> Dict c a -> r
requiringDict @c c a => f a
forall (a :: k). c a => f a
x) b (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
bdicts

instance ProductBC b => ProductBC (Barbie b) where
  bdicts :: Barbie b (Dict c)
bdicts = b (Dict c) -> Barbie b (Dict c)
forall k (b :: (k -> *) -> *) (f :: k -> *). b f -> Barbie b f
Barbie b (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
bdicts

instance ProductBC Unit where
  bdicts :: Unit (Dict c)
bdicts = Unit (Dict c)
forall k (f :: k -> *). Unit f
Unit


-- ===============================================================
--  Generic derivations
-- ===============================================================

-- | Default implementation of 'bdicts' based on 'Generic'.
gbdictsDefault
  :: forall b c
  .  ( CanDeriveProductBC c b
     , AllB c b
     )
  => b (Dict c)
gbdictsDefault :: b (Dict c)
gbdictsDefault
  = RepN (b (Dict c)) Any -> b (Dict c)
forall a x. GenericN a => RepN a x -> a
toN (RepN (b (Dict c)) Any -> b (Dict c))
-> RepN (b (Dict c)) Any -> b (Dict c)
forall a b. (a -> b) -> a -> b
$ forall k k (c :: k -> Constraint) (repbx :: * -> *)
       (repbd :: k -> *) (x :: k).
(GProductBC c repbx repbd, GAll 0 c repbx) =>
repbd x
forall (repbd :: * -> *) x.
(GProductBC c (GAllRepB b) repbd, GAll 0 c (GAllRepB b)) =>
repbd x
gbdicts @c @(GAllRepB b)
{-# INLINE gbdictsDefault #-}


class GProductBC c repbx repbd where
  gbdicts :: GAll 0 c repbx => repbd x

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

instance GProductBC c repbx repbd => GProductBC c (M1 i k repbx) (M1 i k repbd) where
  gbdicts :: M1 i k repbd x
gbdicts = repbd x -> M1 i k repbd x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k k (c :: k -> Constraint) (repbx :: * -> *)
       (repbd :: k -> *) (x :: k).
(GProductBC c repbx repbd, GAll 0 c repbx) =>
repbd x
forall (repbd :: k -> *) (x :: k).
(GProductBC c repbx repbd, GAll 0 c repbx) =>
repbd x
gbdicts @c @repbx)
  {-# INLINE gbdicts #-}

instance GProductBC c U1 U1 where
  gbdicts :: U1 x
gbdicts = U1 x
forall k (p :: k). U1 p
U1
  {-# INLINE gbdicts #-}

instance
  ( GProductBC c lx ld
  , GProductBC c rx rd
  ) => GProductBC c (lx :*: rx)
                    (ld :*: rd) where
  gbdicts :: (:*:) ld rd x
gbdicts = forall (x :: k). (GProductBC c lx ld, GAll 0 c lx) => ld x
forall k k (c :: k -> Constraint) (repbx :: * -> *)
       (repbd :: k -> *) (x :: k).
(GProductBC c repbx repbd, GAll 0 c repbx) =>
repbd x
gbdicts @c @lx @ld ld x -> rd x -> (:*:) ld rd x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (x :: k). (GProductBC c rx rd, GAll 0 c rx) => rd x
forall k k (c :: k -> Constraint) (repbx :: * -> *)
       (repbd :: k -> *) (x :: k).
(GProductBC c repbx repbd, GAll 0 c repbx) =>
repbd x
gbdicts @c @rx @rd
  {-# INLINE gbdicts #-}


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

type P0 = Param 0

instance c a => GProductBC c (Rec (P0 X a_or_pma) (X a))
                             (Rec (P0 (Dict c) a_or_pma) (Dict c a)) where
  gbdicts :: Rec (P0 (Dict c) a_or_pma) (Dict c a) x
gbdicts = K1 R (Dict c a) x -> Rec (P0 (Dict c) a_or_pma) (Dict c a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (Dict c a -> K1 R (Dict c a) x
forall k i c (p :: k). c -> K1 i c p
K1 Dict c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict)
  {-# INLINE gbdicts #-}

instance
  ( ProductBC b
  , AllB c b
  ) => GProductBC c (Self (b' (P0 X)) (b X))
                    (Rec (b' (P0 (Dict c))) (b (Dict c))) where
  gbdicts :: Rec (b' (P0 (Dict c))) (b (Dict c)) x
gbdicts = K1 R (b (Dict c)) x -> Rec (b' (P0 (Dict c))) (b (Dict c)) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (b (Dict c)) x -> Rec (b' (P0 (Dict c))) (b (Dict c)) x)
-> K1 R (b (Dict c)) x -> Rec (b' (P0 (Dict c))) (b (Dict c)) x
forall a b. (a -> b) -> a -> b
$ b (Dict c) -> K1 R (b (Dict c)) x
forall k i c (p :: k). c -> K1 i c p
K1 (b (Dict c) -> K1 R (b (Dict c)) x)
-> b (Dict c) -> K1 R (b (Dict c)) x
forall a b. (a -> b) -> a -> b
$ forall (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
bdicts @_ @b

instance
  ( ProductBC b
  , AllB c b
  ) => GProductBC c (Other (b' (P0 X)) (b X))
                    (Rec (b' (P0 (Dict c))) (b (Dict c))) where
  gbdicts :: Rec (b' (P0 (Dict c))) (b (Dict c)) x
gbdicts = K1 R (b (Dict c)) x -> Rec (b' (P0 (Dict c))) (b (Dict c)) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (b (Dict c)) x -> Rec (b' (P0 (Dict c))) (b (Dict c)) x)
-> K1 R (b (Dict c)) x -> Rec (b' (P0 (Dict c))) (b (Dict c)) x
forall a b. (a -> b) -> a -> b
$ b (Dict c) -> K1 R (b (Dict c)) x
forall k i c (p :: k). c -> K1 i c p
K1 (b (Dict c) -> K1 R (b (Dict c)) x)
-> b (Dict c) -> K1 R (b (Dict c)) x
forall a b. (a -> b) -> a -> b
$ forall (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
bdicts @_ @b


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

instance ProductBC Proxy where
  bdicts :: Proxy (Dict c)
bdicts = Proxy (Dict c)
forall k (t :: k). Proxy t
Proxy
  {-# INLINE bdicts #-}

instance (ProductBC a, ProductBC b) => ProductBC (Product a b) where
  bdicts :: Product a b (Dict c)
bdicts = a (Dict c) -> b (Dict c) -> Product a b (Dict c)
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair a (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
bdicts b (Dict c)
forall k (b :: (k -> *) -> *) (c :: k -> Constraint).
(ProductBC b, AllB c b) =>
b (Dict c)
bdicts
  {-# INLINE bdicts #-}