{-# 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 :: forall (x :: k).
GAll n c (M1 i k repbx) =>
M1 i k repbf x -> M1 i k repbdf x
gaddDicts
    = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 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
gaddDicts @n @c @f @repbx forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i (c :: Meta) (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 :: forall (x :: k). GAll n c V1 => V1 x -> V1 x
gaddDicts V1 x
_ = forall a. HasCallStack => a
undefined



type instance GAll n c U1 = ()

instance GConstraints n c f U1 U1 U1 where
  gaddDicts :: forall (x :: k). GAll n c U1 => U1 x -> U1 x
gaddDicts = 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 :: forall (x :: k).
GAll n c (lx :*: rx) =>
(:*:) lf rf x -> (:*:) ldf rdf x
gaddDicts (lf x
l :*: rf x
r)
    = (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) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (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 :: forall (x :: k).
GAll n c (lx :+: rx) =>
(:+:) lf rf x -> (:+:) ldf rdf x
gaddDicts = \case
    L1 lf x
l -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (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 -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (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 :: forall (x :: k).
GAll n c (Rec (P n X a') (X a)) =>
Rec (P n f a') (f a) x
-> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
gaddDicts
    = forall {k} p a (x :: k). K1 R a x -> Rec p a x
Rec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). c -> K1 i c p
K1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k i c (p :: k). K1 i c p -> c
unK1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} p a (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 :: forall (x :: k). GAll n c (Rec a' a) => Rec b' b x -> Rec b' b x
gaddDicts = 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