{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
module Barbies.Generics.Constraints
  ( GAll
  , X, Y
  , Self, Other, SelfOrOther
  , GConstraints(..)
  )

where

import Barbies.Internal.Dicts(Dict (..))

import Data.Functor.Product (Product (..))
import Data.Kind            (Constraint, Type)
import GHC.TypeLits         (Nat)

import Data.Generics.GenericN

class GConstraints n c f repbx repbf repbdf where
  gaddDicts :: GAll n c repbx => repbf x -> repbdf x

type family GAll (n :: Nat) (c :: k -> Constraint) (repbf :: Type -> Type) :: Constraint

data X a
data family Y :: k

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

type instance GAll n c (M1 i k repbf) = GAll n c repbf

instance
  GConstraints n c f repbx repbf repbdf
    => GConstraints n c f (M1 i k repbx)
                          (M1 i k repbf)
                          (M1 i k repbdf)
  where
  gaddDicts :: M1 i k repbf x -> M1 i k repbdf x
gaddDicts
    = repbdf x -> M1 i k repbdf x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (repbdf x -> M1 i k repbdf x)
-> (M1 i k repbf x -> repbdf x)
-> M1 i k repbf x
-> M1 i k repbdf x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k k k (n :: Nat) (c :: k -> Constraint) (f :: k)
       (repbx :: * -> *) (repbf :: k -> *) (repbdf :: k -> *) (x :: k).
(GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
repbf x -> repbdf x
forall (repbf :: k -> *) (repbdf :: k -> *) (x :: k).
(GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
repbf x -> repbdf x
gaddDicts @n @c @f @repbx (repbf x -> repbdf x)
-> (M1 i k repbf x -> repbf x) -> M1 i k repbf x -> repbdf x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i k repbf x -> repbf x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gaddDicts #-}



type instance GAll n c V1 = ()

instance GConstraints n c f V1 V1 V1 where
  gaddDicts :: V1 x -> V1 x
gaddDicts V1 x
_ = V1 x
forall a. HasCallStack => a
undefined



type instance GAll n c U1 = ()

instance GConstraints n c f U1 U1 U1 where
  gaddDicts :: U1 x -> U1 x
gaddDicts = U1 x -> U1 x
forall a. a -> a
id
  {-# INLINE gaddDicts #-}


type instance GAll n c (l :*: r)
  = (GAll n c l, GAll n c r)

instance
  ( GConstraints n c f lx lf ldf
  , GConstraints n c f rx rf rdf
  ) => GConstraints n c f (lx  :*: rx)
                          (lf  :*: rf)
                          (ldf :*: rdf)
  where
  gaddDicts :: (:*:) lf rf x -> (:*:) ldf rdf x
gaddDicts (lf x
l :*: rf x
r)
    = (lf x -> ldf x
forall k k k (n :: Nat) (c :: k -> Constraint) (f :: k)
       (repbx :: * -> *) (repbf :: k -> *) (repbdf :: k -> *) (x :: k).
(GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
repbf x -> repbdf x
gaddDicts @n @c @f @lx lf x
l) ldf x -> rdf x -> (:*:) ldf rdf x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (rf x -> rdf x
forall k k k (n :: Nat) (c :: k -> Constraint) (f :: k)
       (repbx :: * -> *) (repbf :: k -> *) (repbdf :: k -> *) (x :: k).
(GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
repbf x -> repbdf x
gaddDicts @n @c @f @rx rf x
r)
  {-# INLINE gaddDicts #-}


type instance GAll n c (l :+: r) = (GAll n c l, GAll n c r)

instance
  ( GConstraints n c f lx lf ldf
  , GConstraints n c f rx rf rdf
  ) => GConstraints n c f (lx  :+: rx)
                          (lf  :+: rf)
                          (ldf :+: rdf)
  where
  gaddDicts :: (:+:) lf rf x -> (:+:) ldf rdf x
gaddDicts = \case
    L1 lf x
l -> ldf x -> (:+:) ldf rdf x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (lf x -> ldf x
forall k k k (n :: Nat) (c :: k -> Constraint) (f :: k)
       (repbx :: * -> *) (repbf :: k -> *) (repbdf :: k -> *) (x :: k).
(GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
repbf x -> repbdf x
gaddDicts @n @c @f @lx lf x
l)
    R1 rf x
r -> rdf x -> (:+:) ldf rdf x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (rf x -> rdf x
forall k k k (n :: Nat) (c :: k -> Constraint) (f :: k)
       (repbx :: * -> *) (repbf :: k -> *) (repbdf :: k -> *) (x :: k).
(GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
repbf x -> repbdf x
gaddDicts @n @c @f @rx rf x
r)
  {-# INLINE gaddDicts #-}


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

type P = Param

type instance GAll n c (Rec l r) = GAllRec n c l r
type family GAllRec
  (n :: Nat)
  (c :: k -> Constraint)
  (l :: Type)
  (r :: Type) :: Constraint
  where
    GAllRec n c (P n X _) (X a) = c a
    GAllRec _ _ _ _ = ()

-- {{ Functor application -----------------------------------------------------
instance
  -- a' is a, maybe with Param applications
  GConstraints n c f (Rec (P n X a') (X a))
                     (Rec (P n f a') (f a))
                     (Rec (P n (Dict c `Product` f) a')
                              ((Dict c `Product` f) a))
  where
  gaddDicts :: Rec (P n f a') (f a) x
-> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
gaddDicts
    = K1 R (Product (Dict c) f a) x
-> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (Product (Dict c) f a) x
 -> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x)
-> (Rec (P n f a') (f a) x -> K1 R (Product (Dict c) f a) x)
-> Rec (P n f a') (f a) x
-> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product (Dict c) f a -> K1 R (Product (Dict c) f a) x
forall k i c (p :: k). c -> K1 i c p
K1 (Product (Dict c) f a -> K1 R (Product (Dict c) f a) x)
-> (Rec (P n f a') (f a) x -> Product (Dict c) f a)
-> Rec (P n f a') (f a) x
-> K1 R (Product (Dict c) f a) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dict c a -> f a -> Product (Dict c) f a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair Dict c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict (f a -> Product (Dict c) f a)
-> (Rec (P n f a') (f a) x -> f a)
-> Rec (P n f a') (f a) x
-> Product (Dict c) f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R (f a) x -> f a
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 R (f a) x -> f a)
-> (Rec (P n f a') (f a) x -> K1 R (f a) x)
-> Rec (P n f a') (f a) x
-> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (P n f a') (f a) x -> K1 R (f a) x
forall p a k (x :: k). Rec p a x -> K1 R a x
unRec
  {-# INLINE gaddDicts #-}

-- }} Functor application -----------------------------------------------------

-- {{ Not a functor application -----------------------------------------------

instance
  -- b is a, but with X or Y instead of Param ...
  -- a' is a, maybe with occurrences of Param
  -- b' is b, maybe with occurences of Param
  GConstraints n c f (Rec a' a) -- a' may contain Y or Param m (m > n)
                     (Rec b' b) -- a'' may only contain Param m (m > n)
                     (Rec b' b)
  where
  gaddDicts :: Rec b' b x -> Rec b' b x
gaddDicts = Rec b' b x -> Rec b' b x
forall a. a -> a
id
  {-# INLINE gaddDicts #-}
-- }} Not a functor application -----------------------------------------------


-- ============================================================================
-- ## Identifying recursive usages of the barbie-type ##
--
-- ============================================================================

data Self  (p :: Type) (a :: Type) (x :: Type)
data Other (p :: Type) (a :: Type) (x :: Type)

type family SelfOrOther (b :: k) (b' :: k) :: Type -> Type -> Type -> Type where
  SelfOrOther b b = Self
  SelfOrOther b b' = Other