{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Barbies.Internal.ConstraintsT
  ( ConstraintsT(..)
  , tmapC
  , ttraverseC
  , AllTF
  , tdicts
  , tpureC
  , tmempty
  , tzipWithC
  , tzipWith3C
  , tzipWith4C
  , tfoldMapC

  , CanDeriveConstraintsT
  , gtaddDictsDefault
  , GAllRepT

  , TagSelf1, TagSelf1'
  )

where

import Barbies.Internal.ApplicativeT(ApplicativeT (..))
import Barbies.Generics.Constraints
  ( GConstraints(..)
  , GAll
  , Self, Other, SelfOrOther
  , X, Y
  )
import Barbies.Internal.Dicts(ClassF, Dict (..), requiringDict)
import Barbies.Internal.FunctorT(FunctorT (..))
import Barbies.Internal.TraversableT(TraversableT (..))

import Data.Functor.Const(Const(..))
import Data.Functor.Product(Product(..))
import Data.Kind(Constraint, Type)
import Data.Proxy(Proxy(..))

import Data.Generics.GenericN


-- | Instances of this class provide means to talk about constraints,
--   both at compile-time, using 'AllT', and at run-time, in the form
--   of 'Dict', via 'taddDicts'.
--
--   A manual definition would look like this:
--
-- @
-- data T f a = A (f 'Int') (f 'String') | B (f 'Bool') (f 'Int')
--
-- instance 'ConstraintsT' T where
--   type 'AllT' c T = (c 'Int', c 'String', c 'Bool')
--
--   'taddDicts' t = case t of
--     A x y -> A ('Pair' 'Dict' x) ('Pair' 'Dict' y)
--     B z w -> B ('Pair' 'Dict' z) ('Pair' 'Dict' w)
-- @
--
-- Now, when we given a @T f@, if we need to use the 'Show' instance of
-- their fields, we can use:
--
-- @
-- 'taddDicts' :: AllT Show t => t f -> t ('Dict' 'Show' `'Product'` f)
-- @
--
-- There is a default implementation of 'ConstraintsT' for
-- 'Generic' types, so in practice one will simply do:
--
-- @
-- derive instance 'Generic' (T f a)
-- instance 'ConstraintsT' T
-- @
class FunctorT t => ConstraintsT (t :: (kl -> Type) -> (kr -> Type)) where
  -- | @'AllT' c t@ should contain a constraint @c a@ for each
  --   @a@ occurring under an @f@ in @t f@.
  --
  -- For requiring constraints of the form @c (f a)@, use 'AllTF'.
  type AllT (c :: k -> Constraint) t :: Constraint
  type AllT c t = GAll 1 c (GAllRepT t)

  taddDicts
    :: forall c f x
    .  AllT c t
    => t f x
    -> t (Dict c `Product` f) x

  default taddDicts
    :: forall c f x
    .  ( CanDeriveConstraintsT c t f x
       , AllT c t
       )
    => t f x
    -> t (Dict c `Product` f) x
  taddDicts = forall {k} {kr} (t :: (k -> *) -> kr -> *) (c :: k -> Constraint)
       (f :: k -> *) (x :: kr).
(CanDeriveConstraintsT c t f x, AllT c t) =>
t f x -> t (Product (Dict c) f) x
gtaddDictsDefault


-- | Like 'tmap' but a constraint is allowed to be required on
--   each element of @t@.
tmapC :: forall c t f g x
      .  (AllT c t, ConstraintsT t)
      => (forall a. c a => f a -> g a)
      -> t f x
      -> t g x
tmapC :: forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *)
       (f :: k -> *) (g :: k -> *) (x :: kr).
(AllT c t, ConstraintsT t) =>
(forall (a :: k). c a => f a -> g a) -> t f x -> t g x
tmapC forall (a :: k). c a => f a -> g a
f t f x
tf
  = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap forall (a :: k). Product (Dict c) f a -> g a
go (forall kl kr (t :: (kl -> *) -> kr -> *) (c :: kl -> Constraint)
       (f :: kl -> *) (x :: kr).
(ConstraintsT t, AllT c t) =>
t f x -> t (Product (Dict c) f) x
taddDicts t f x
tf)
  where
    go :: forall a. (Dict c `Product` f) a -> g a
    go :: forall (a :: k). Product (Dict c) f a -> g a
go (Dict c a
d `Pair` f a
fa) = forall {k} (c :: k -> Constraint) (a :: k) r.
(c a => r) -> Dict c a -> r
requiringDict (forall (a :: k). c a => f a -> g a
f f a
fa) Dict c a
d

-- | Like 'ttraverse' but with a constraint on the elements of @t@.
ttraverseC
  :: forall c t f g e x
  .  (TraversableT t, ConstraintsT t, AllT c t, Applicative e)
  => (forall a. c a => f a -> e (g a))
  -> t f x
  -> e (t g x)
ttraverseC :: forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *)
       (f :: k -> *) (g :: k -> *) (e :: * -> *) (x :: kr).
(TraversableT t, ConstraintsT t, AllT c t, Applicative e) =>
(forall (a :: k). c a => f a -> e (g a)) -> t f x -> e (t g x)
ttraverseC forall (a :: k). c a => f a -> e (g a)
f t f x
t
  = forall k k' (t :: (k -> *) -> k' -> *) (e :: * -> *) (f :: k -> *)
       (g :: k -> *) (x :: k').
(TraversableT t, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> t f x -> e (t g x)
ttraverse (\(Pair (Dict c a
Dict :: Dict c a) f a
x) -> forall (a :: k). c a => f a -> e (g a)
f f a
x) (forall kl kr (t :: (kl -> *) -> kr -> *) (c :: kl -> Constraint)
       (f :: kl -> *) (x :: kr).
(ConstraintsT t, AllT c t) =>
t f x -> t (Product (Dict c) f) x
taddDicts t f x
t)

-- | Like 'Data.Functor.Transformer.tfoldMap' but with a constraint on the function.
tfoldMapC
  :: forall c t m f x
  .  (TraversableT t, ConstraintsT t,  AllT c t, Monoid m)
  => (forall a. c a => f a -> m)
  -> t f x
  -> m
tfoldMapC :: forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *) m
       (f :: k -> *) (x :: kr).
(TraversableT t, ConstraintsT t, AllT c t, Monoid m) =>
(forall (a :: k). c a => f a -> m) -> t f x -> m
tfoldMapC forall (a :: k). c a => f a -> m
f = forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *)
       (f :: k -> *) (g :: k -> *) (e :: * -> *) (x :: kr).
(TraversableT t, ConstraintsT t, AllT c t, Applicative e) =>
(forall (a :: k). c a => f a -> e (g a)) -> t f x -> e (t g x)
ttraverseC @c (forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: k). c a => f a -> m
f)


-- | Like 'Data.Functor.Barbie.tzipWith' but with a constraint on the elements of @t@.
tzipWithC
  :: forall c t f g h x
  .  (AllT c t, ConstraintsT t, ApplicativeT t)
  => (forall a. c a => f a -> g a -> h a)
  -> t f x
  -> t g x
  -> t h x
tzipWithC :: forall {k} {k'} (c :: k -> Constraint) (t :: (k -> *) -> k' -> *)
       (f :: k -> *) (g :: k -> *) (h :: k -> *) (x :: k').
(AllT c t, ConstraintsT t, ApplicativeT t) =>
(forall (a :: k). c a => f a -> g a -> h a)
-> t f x -> t g x -> t h x
tzipWithC forall (a :: k). c a => f a -> g a -> h a
f t f x
tf t g x
tg
  = forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *)
       (f :: k -> *) (g :: k -> *) (x :: kr).
(AllT c t, ConstraintsT t) =>
(forall (a :: k). c a => f a -> g a) -> t f x -> t g x
tmapC @c forall (a :: k). c a => Product f g a -> h a
go (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg)
  where
    go :: forall a. c a => Product f g a -> h a
    go :: forall (a :: k). c a => Product f g a -> h a
go (Pair f a
fa g a
ga) = forall (a :: k). c a => f a -> g a -> h a
f f a
fa g a
ga

-- | Like 'Data.Functor.Barbie.tzipWith3' but with a constraint on the elements of @t@.
tzipWith3C
  :: forall c t f g h i x
  .  (AllT c t, ConstraintsT t, ApplicativeT t)
  => (forall a. c a => f a -> g a -> h a -> i a)
  -> t f x
  -> t g x
  -> t h x
  -> t i x
tzipWith3C :: forall {k} {k'} (c :: k -> Constraint) (t :: (k -> *) -> k' -> *)
       (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *) (x :: k').
(AllT c t, ConstraintsT t, ApplicativeT t) =>
(forall (a :: k). c a => f a -> g a -> h a -> i a)
-> t f x -> t g x -> t h x -> t i x
tzipWith3C forall (a :: k). c a => f a -> g a -> h a -> i a
f t f x
tf t g x
tg t h x
th
  = forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *)
       (f :: k -> *) (g :: k -> *) (x :: kr).
(AllT c t, ConstraintsT t) =>
(forall (a :: k). c a => f a -> g a) -> t f x -> t g x
tmapC @c forall (a :: k). c a => Product (Product f g) h a -> i a
go (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t h x
th)
  where
    go :: forall a. c a => Product (Product f g) h a -> i a
    go :: forall (a :: k). c a => Product (Product f g) h a -> i a
go (Pair (Pair f a
fa g a
ga) h a
ha) = forall (a :: k). c a => f a -> g a -> h a -> i a
f f a
fa g a
ga h a
ha

-- | Like 'Data.Functor.Barbie.tzipWith4' but with a constraint on the elements of @t@.
tzipWith4C
  :: forall c t f g h i j x
  .  (AllT c t, ConstraintsT t, ApplicativeT t)
  => (forall a. c a => f a -> g a -> h a -> i a -> j a)
  -> t f x
  -> t g x
  -> t h x
  -> t i x
  -> t j x
tzipWith4C :: forall {k} {k'} (c :: k -> Constraint) (t :: (k -> *) -> k' -> *)
       (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *)
       (j :: k -> *) (x :: k').
(AllT c t, ConstraintsT t, ApplicativeT t) =>
(forall (a :: k). c a => f a -> g a -> h a -> i a -> j a)
-> t f x -> t g x -> t h x -> t i x -> t j x
tzipWith4C forall (a :: k). c a => f a -> g a -> h a -> i a -> j a
f t f x
tf t g x
tg t h x
th t i x
ti
  = forall {k} {kr} (c :: k -> Constraint) (t :: (k -> *) -> kr -> *)
       (f :: k -> *) (g :: k -> *) (x :: kr).
(AllT c t, ConstraintsT t) =>
(forall (a :: k). c a => f a -> g a) -> t f x -> t g x
tmapC @c forall (a :: k).
c a =>
Product (Product (Product f g) h) i a -> j a
go (t f x
tf forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t g x
tg forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t h x
th forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k')
       (g :: k -> *).
ApplicativeT t =>
t f x -> t g x -> t (Product f g) x
`tprod` t i x
ti)
  where
    go :: forall a. c a => Product (Product (Product f g) h) i a -> j a
    go :: forall (a :: k).
c a =>
Product (Product (Product f g) h) i a -> j a
go (Pair (Pair (Pair f a
fa g a
ga) h a
ha) i a
ia) = forall (a :: k). c a => f a -> g a -> h a -> i a -> j a
f f a
fa g a
ga h a
ha i a
ia


-- | Similar to 'AllT' but will put the functor argument @f@
--   between the constraint @c@ and the type @a@.
type AllTF c f t = AllT (ClassF c f) t


-- | Similar to 'taddDicts' but can produce the instance dictionaries
--   "out of the blue".
tdicts
  :: forall c t x
  . (ConstraintsT t, ApplicativeT t,  AllT c t)
  => t (Dict c) x
tdicts :: forall {kl} {kr} (c :: kl -> Constraint)
       (t :: (kl -> *) -> kr -> *) (x :: kr).
(ConstraintsT t, ApplicativeT t, AllT c t) =>
t (Dict c) x
tdicts
  = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (\(Pair Dict c a
c Proxy a
_) -> Dict c a
c) forall a b. (a -> b) -> a -> b
$ forall kl kr (t :: (kl -> *) -> kr -> *) (c :: kl -> Constraint)
       (f :: kl -> *) (x :: kr).
(ConstraintsT t, AllT c t) =>
t f x -> t (Product (Dict c) f) x
taddDicts forall a b. (a -> b) -> a -> b
$ forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a) -> t f x
tpure forall {k} (t :: k). Proxy t
Proxy


-- | Like 'tpure' but a constraint is allowed to be required on
--   each element of @t@.
tpureC
  :: forall c f t x
  .  ( AllT c t
     , ConstraintsT t
     , ApplicativeT t
     )
  => (forall a . c a => f a)
  -> t f x
tpureC :: forall {k} {k'} (c :: k -> Constraint) (f :: k -> *)
       (t :: (k -> *) -> k' -> *) (x :: k').
(AllT c t, ConstraintsT t, ApplicativeT t) =>
(forall (a :: k). c a => f a) -> t f x
tpureC forall (a :: k). c a => f a
fa
  = forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (g :: k -> *)
       (x :: k').
FunctorT t =>
(forall (a :: k). f a -> g a) -> t f x -> t g x
tmap (forall {k} (c :: k -> Constraint) (a :: k) r.
(c a => r) -> Dict c a -> r
requiringDict @c forall (a :: k). c a => f a
fa) forall {kl} {kr} (c :: kl -> Constraint)
       (t :: (kl -> *) -> kr -> *) (x :: kr).
(ConstraintsT t, ApplicativeT t, AllT c t) =>
t (Dict c) x
tdicts

-- | Builds a @t f x@, by applying 'mempty' on every field of @t@.
tmempty
  :: forall f t x
  .  ( AllTF Monoid f t
     , ConstraintsT t
     , ApplicativeT t
     )
  => t f x
tmempty :: forall {k} {k'} (f :: k -> *) (t :: (k -> *) -> k' -> *) (x :: k').
(AllTF Monoid f t, ConstraintsT t, ApplicativeT t) =>
t f x
tmempty
  = forall {k} {k'} (c :: k -> Constraint) (f :: k -> *)
       (t :: (k -> *) -> k' -> *) (x :: k').
(AllT c t, ConstraintsT t, ApplicativeT t) =>
(forall (a :: k). c a => f a) -> t f x
tpureC @(ClassF Monoid f) forall a. Monoid a => a
mempty


-- | @'CanDeriveConstraintsT' T f g x@ is in practice a predicate about @T@ only.
--   Intuitively, it says that the following holds, for any arbitrary @f@ and @x@:
--
--     * There is an instance of @'Generic' (T f x)@.
--
--     * @T f@ can contain fields of type @t f x@ as long as there exists a
--       @'ConstraintsT' t@ instance. In particular, recursive usages of @T f x@
--       are allowed.
type CanDeriveConstraintsT c t f x
  = ( GenericN (t f x)
    , GenericN (t (Dict c `Product` f) x)
    , AllT c t ~ GAll 1 c (GAllRepT t)
    , GConstraints 1 c f (GAllRepT t) (RepN (t f x)) (RepN (t (Dict c `Product` f) x))
    )

-- | The representation used for the generic computation of the @'AllT' c t@
--   constraints. .
type GAllRepT t = TagSelf1 t


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

-- | Default implementation of ibaddDicts' based on 'Generic'.
gtaddDictsDefault
  :: forall t c f x
  . ( CanDeriveConstraintsT c t f x
    , AllT c t
    )
  => t f x
  -> t (Dict c `Product` f) x
gtaddDictsDefault :: forall {k} {kr} (t :: (k -> *) -> kr -> *) (c :: k -> Constraint)
       (f :: k -> *) (x :: kr).
(CanDeriveConstraintsT c t f x, AllT c t) =>
t f x -> t (Product (Dict c) f) x
gtaddDictsDefault
  = forall a x. GenericN a => RepN a x -> a
toN 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 @1 @c @f @(GAllRepT t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. GenericN a => a -> RepN a x
fromN

{-# INLINE gtaddDictsDefault #-}


-- ------------------------------------------------------------
-- Generic derivation: Special cases for ConstraintsT
-- -----------------------------------------------------------

type P = Param

-- Break recursive case
type instance GAll 1 c (Self (t' (P 1 X) Y) (t X Y)) = ()

instance
  ( ConstraintsT t
  , AllT c t
  ) => -- t' is t, maybe with some Param occurrences
       GConstraints 1 c f (Self (t' (P 1 X) Y) (t X Y))
                          (Rec (t' (P 1 f) (P 0 y)) (t f y))
                          (Rec (t' (P 1 (Dict c `Product` f)) (P 0 y))
                               (t       (Dict c `Product` f)       y))
  where
  gaddDicts :: forall (x :: k).
GAll 1 c (Self (t' (P 1 X) Y) (t X Y)) =>
Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> Rec
     (t' (P 1 (Product (Dict c) f)) (P 0 y))
     (t (Product (Dict c) f) y)
     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 kl kr (t :: (kl -> *) -> kr -> *) (c :: kl -> Constraint)
       (f :: kl -> *) (x :: kr).
(ConstraintsT t, AllT c t) =>
t f x -> t (Product (Dict c) f) x
taddDicts 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 #-}


type instance GAll 1 c (Other (t' (P 1 X) Y) (t X Y)) = AllT c t

instance
  ( ConstraintsT t
  , AllT c t
  ) => -- t' is t maybe with some Param occurrences
       GConstraints 1 c f (Other (t' (P 1 X) Y) (t X Y))
                          (Rec (t' (P 1 f) (P 0 y)) (t f y))
                          (Rec (t' (P 1 (Dict c `Product` f)) (P 0 y))
                               (t       (Dict c `Product` f)       y))
  where
  gaddDicts :: forall (x :: k).
GAll 1 c (Other (t' (P 1 X) Y) (t X Y)) =>
Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> Rec
     (t' (P 1 (Product (Dict c) f)) (P 0 y))
     (t (Product (Dict c) f) y)
     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 kl kr (t :: (kl -> *) -> kr -> *) (c :: kl -> Constraint)
       (f :: kl -> *) (x :: kr).
(ConstraintsT t, AllT c t) =>
t f x -> t (Product (Dict c) f) x
taddDicts 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 #-}

-- | We use the type-families to generically compute @'Barbies.AllT' c b@.
--   Intuitively, if @t' f' x'@ occurs inside @t f x@, then we should just add
--   @'Barbies.AllT' t' c@ to @'Barbies.AllT' t c@. The problem is that if @t@
--   is a recursive type, and @t'@ is @t@, then ghc will choke and blow the
--   stack (instead of computing a fixpoint).
--
--   So, we would like to behave differently when @t = t'@ and add @()@ instead
--   of @'Barbies.AllT' t c@ to break the recursion. Our trick will be to use a
--   type family to inspect @'Rep' (t X Y)@, for arbitrary @X@ and @Y@ and
--   distinguish recursive usages from non-recursive ones, tagging them with
--   different types, so we can distinguish them in the instances.
type TagSelf1 b
  = TagSelf1' (Indexed b 2) (Zip (Rep (Indexed (b X) 1 Y)) (Rep (b X Y)))

type family TagSelf1' (b :: kf -> kg -> Type) (repbf :: Type -> Type) :: Type -> Type where
  TagSelf1' b (M1 mt m s)
    = M1 mt m (TagSelf1' b s)

  TagSelf1' b (l :+: r)
    = TagSelf1' b l :+: TagSelf1' b r

  TagSelf1' b (l :*: r)
    = TagSelf1' b l :*: TagSelf1' b r

  TagSelf1' (b :: kf -> kg -> Type)
            (Rec ((b'  :: kf -> kg -> Type) fl fr)
                 ((b'' :: kf -> kg -> Type) gl gr)
            )
    = (SelfOrOther b b') (b' fl gr) (b'' gl gr)

  TagSelf1' b (Rec x y)
    = Rec x y

  TagSelf1' b U1
    = U1

  TagSelf1' b V1
    = V1