{-# 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 = t f x -> t (Product (Dict c) f) x
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 (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 (a :: k). Product (Dict c) f a -> g a)
-> t (Product (Dict c) f) x -> t g x
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 (t f x -> t (Product (Dict c) f) 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
tf)
  where
    go :: forall a. (Dict c `Product` f) a -> g a
    go :: Product (Dict c) f a -> g a
go (Dict c a
d `Pair` f a
fa) = (c a => g a) -> Dict c a -> g a
forall k (c :: k -> Constraint) (a :: k) r.
(c a => r) -> Dict c a -> r
requiringDict (f a -> g a
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 (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 (a :: k). Product (Dict c) f a -> e (g a))
-> t (Product (Dict c) f) x -> e (t g x)
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 :: Dict c a) x) -> f a -> e (g a)
forall (a :: k). c a => f a -> e (g a)
f f a
x) (t f x -> t (Product (Dict c) f) 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 (a :: k). c a => f a -> m) -> t f x -> m
tfoldMapC forall (a :: k). c a => f a -> m
f = Const m (t Any x) -> m
forall a k (b :: k). Const a b -> a
getConst (Const m (t Any x) -> m)
-> (t f x -> Const m (t Any x)) -> t f x -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: k). c a => f a -> Const m (Any a))
-> t f x -> Const m (t Any x)
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 (m -> Const m (Any a)
forall k a (b :: k). a -> Const a b
Const (m -> Const m (Any a)) -> (f a -> m) -> f a -> Const m (Any a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> m
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 (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 (a :: k). c a => Product f g a -> h a)
-> t (Product f g) x -> t h x
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 t f x -> t g x -> t (Product f g) x
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 :: Product f g a -> h a
go (Pair f a
fa g a
ga) = f a -> g a -> h a
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 (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 (a :: k). c a => Product (Product f g) h a -> i a)
-> t (Product (Product f g) h) x -> t i x
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 t f x -> t g x -> t (Product f g) x
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 t (Product f g) x -> t h x -> t (Product (Product f g) h) x
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 :: Product (Product f g) h a -> i a
go (Pair (Pair f a
fa g a
ga) h a
ha) = f a -> g a -> h a -> i a
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 (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 (a :: k).
 c a =>
 Product (Product (Product f g) h) i a -> j a)
-> t (Product (Product (Product f g) h) i) x -> t j x
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 t f x -> t g x -> t (Product f g) x
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 t (Product f g) x -> t h x -> t (Product (Product f g) h) x
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 t (Product (Product f g) h) x
-> t i x -> t (Product (Product (Product f g) h) i) x
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 :: 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) = f a -> g a -> h a -> i a -> j a
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 :: t (Dict c) x
tdicts
  = (forall (a :: kl). Product (Dict c) Proxy a -> Dict c a)
-> t (Product (Dict c) Proxy) x -> t (Dict c) x
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 c _) -> Dict c a
c) (t (Product (Dict c) Proxy) x -> t (Dict c) x)
-> t (Product (Dict c) Proxy) x -> t (Dict c) x
forall a b. (a -> b) -> a -> b
$ t Proxy x -> t (Product (Dict c) Proxy) 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 Proxy x -> t (Product (Dict c) Proxy) x)
-> t Proxy x -> t (Product (Dict c) Proxy) x
forall a b. (a -> b) -> a -> b
$ (forall (a :: kl). Proxy a) -> t Proxy x
forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *) (x :: k').
ApplicativeT t =>
(forall (a :: k). f a) -> t f x
tpure forall (a :: kl). Proxy a
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 (a :: k). c a => f a) -> t f x
tpureC forall (a :: k). c a => f a
fa
  = (forall (a :: k). Dict c a -> f a) -> t (Dict c) x -> t f x
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 ((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
fa) t (Dict c) x
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 :: t f x
tmempty
  = (forall (a :: k). ClassF Monoid f a => f a) -> t f x
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 :: k). ClassF Monoid f a => f a
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 :: t f x -> t (Product (Dict c) f) x
gtaddDictsDefault
  = Zip
  (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
  (Rep (t (Product (Dict c) f) x))
  Any
-> t (Product (Dict c) f) x
forall a x. GenericN a => RepN a x -> a
toN (Zip
   (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
   (Rep (t (Product (Dict c) f) x))
   Any
 -> t (Product (Dict c) f) x)
-> (t f x
    -> Zip
         (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
         (Rep (t (Product (Dict c) f) x))
         Any)
-> t f x
-> t (Product (Dict c) f) 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 :: * -> *) (repbdf :: * -> *) x.
(GConstraints 1 c f (GAllRepT t) repbf repbdf,
 GAll 1 c (GAllRepT t)) =>
repbf x -> repbdf x
gaddDicts @1 @c @f @(GAllRepT t) (Zip (Rep (Indexed t 2 (Param 1 f) (Param 0 x))) (Rep (t f x)) Any
 -> Zip
      (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
      (Rep (t (Product (Dict c) f) x))
      Any)
-> (t f x
    -> Zip
         (Rep (Indexed t 2 (Param 1 f) (Param 0 x))) (Rep (t f x)) Any)
-> t f x
-> Zip
     (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
     (Rep (t (Product (Dict c) f) x))
     Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t f x
-> Zip
     (Rep (Indexed t 2 (Param 1 f) (Param 0 x))) (Rep (t f x)) Any
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 :: 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
    = K1 R (t (Product (Dict c) f) y) x
-> Rec
     (t' (P 1 (Product (Dict c) f)) (P 0 y))
     (t (Product (Dict c) f) y)
     x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (t (Product (Dict c) f) y) x
 -> Rec
      (t' (P 1 (Product (Dict c) f)) (P 0 y))
      (t (Product (Dict c) f) y)
      x)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x
    -> K1 R (t (Product (Dict c) f) y) x)
-> 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
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (Product (Dict c) f) y -> K1 R (t (Product (Dict c) f) y) x
forall k i c (p :: k). c -> K1 i c p
K1 (t (Product (Dict c) f) y -> K1 R (t (Product (Dict c) f) y) x)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x -> t (Product (Dict c) f) y)
-> Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> K1 R (t (Product (Dict c) f) y) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t f y -> t (Product (Dict c) f) y
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 y -> t (Product (Dict c) f) y)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x -> t f y)
-> Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> t (Product (Dict c) f) y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R (t f y) x -> t f y
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 R (t f y) x -> t f y)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x -> K1 R (t f y) x)
-> Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> t f y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (t' (P 1 f) (P 0 y)) (t f y) x -> K1 R (t f y) x
forall p a k (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 :: 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
    = K1 R (t (Product (Dict c) f) y) x
-> Rec
     (t' (P 1 (Product (Dict c) f)) (P 0 y))
     (t (Product (Dict c) f) y)
     x
forall k p a (x :: k). K1 R a x -> Rec p a x
Rec (K1 R (t (Product (Dict c) f) y) x
 -> Rec
      (t' (P 1 (Product (Dict c) f)) (P 0 y))
      (t (Product (Dict c) f) y)
      x)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x
    -> K1 R (t (Product (Dict c) f) y) x)
-> 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
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (Product (Dict c) f) y -> K1 R (t (Product (Dict c) f) y) x
forall k i c (p :: k). c -> K1 i c p
K1 (t (Product (Dict c) f) y -> K1 R (t (Product (Dict c) f) y) x)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x -> t (Product (Dict c) f) y)
-> Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> K1 R (t (Product (Dict c) f) y) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t f y -> t (Product (Dict c) f) y
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 y -> t (Product (Dict c) f) y)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x -> t f y)
-> Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> t (Product (Dict c) f) y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R (t f y) x -> t f y
forall i c k (p :: k). K1 i c p -> c
unK1 (K1 R (t f y) x -> t f y)
-> (Rec (t' (P 1 f) (P 0 y)) (t f y) x -> K1 R (t f y) x)
-> Rec (t' (P 1 f) (P 0 y)) (t f y) x
-> t f y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (t' (P 1 f) (P 0 y)) (t f y) x -> K1 R (t f y) x
forall p a k (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