{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Barbies.Internal.ConstraintsB
  ( ConstraintsB(..)
  , bmapC
  , btraverseC
  , AllBF
  , bdicts
  , bpureC
  , bmempty
  , bzipWithC
  , bzipWith3C
  , bzipWith4C
  , bfoldMapC

  , CanDeriveConstraintsB
  , gbaddDictsDefault
  , GAllRepB

  , TagSelf0, TagSelf0'
  )

where

import Barbies.Generics.Constraints
  ( GConstraints(..)
  , GAll
  , Self
  , Other
  , SelfOrOther
  , X
  )
import Barbies.Internal.ApplicativeB(ApplicativeB(..))
import Barbies.Internal.Dicts(ClassF, Dict (..), requiringDict)
import Barbies.Internal.FunctorB(FunctorB (..))
import Barbies.Internal.TraversableB(TraversableB (..))

import Data.Functor.Compose (Compose (..))
import Data.Functor.Const   (Const (..))
import Data.Functor.Product (Product (..))
import Data.Functor.Sum     (Sum (..))
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 'AllB', and at run-time, in the form
--   of 'Dict', via 'baddDicts'.
--
--   A manual definition would look like this:
--
-- @
-- data T f = A (f 'Int') (f 'String') | B (f 'Bool') (f 'Int')
--
-- instance 'ConstraintsB' T where
--   type 'AllB' c T = (c 'Int', c 'String', c 'Bool')
--
--   'baddDicts' 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:
--
-- @
-- 'baddDicts' :: AllB Show b => b f -> b ('Dict' 'Show' `'Product'` f)
-- @
--
-- There is a default implementation of 'ConstraintsB' for
-- 'Generic' types, so in practice one will simply do:
--
-- @
-- derive instance 'Generic' (T f)
-- instance 'ConstraintsB' T
-- @
class FunctorB b => ConstraintsB (b :: (k -> Type) -> Type) where
  -- | @'AllB' c b@ should contain a constraint @c a@ for each
  --   @a@ occurring under an @f@ in @b f@. E.g.:
  --
  -- @
  -- 'AllB' 'Show' Person ~ ('Show' 'String', 'Show' 'Int')
  -- @
  --
  -- For requiring constraints of the form @c (f a)@, use 'AllBF'.
  type AllB (c :: k -> Constraint) b :: Constraint
  type AllB c b = GAll 0 c (GAllRepB b)

  baddDicts
    :: forall c f
    .  AllB c b
    => b f
    -> b (Dict c `Product` f)

  default baddDicts
    :: forall c f
    .  ( CanDeriveConstraintsB c b f
       , AllB c b
       )
    => b f -> b (Dict c `Product` f)
  baddDicts = forall {k} (b :: (k -> *) -> *) (c :: k -> Constraint)
       (f :: k -> *).
(CanDeriveConstraintsB c b f, AllB c b) =>
b f -> b (Product (Dict c) f)
gbaddDictsDefault


-- | Like 'bmap' but a constraint is allowed to be required on
--   each element of @b@
--
-- E.g. If all fields of @b@ are 'Show'able then you
-- could store each shown value in it's slot using 'Const':
--
-- > showFields :: (AllB Show b, ConstraintsB b) => b Identity -> b (Const String)
-- > showFields = bmapC @Show showField
-- >   where
-- >     showField :: forall a. Show a => Identity a -> Const String a
-- >     showField (Identity a) = Const (show a)
bmapC :: forall c b f g
      .  (AllB c b, ConstraintsB b)
      => (forall a. c a => f a -> g a)
      -> b f
      -> b g
bmapC :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *).
(AllB c b, ConstraintsB b) =>
(forall (a :: k). c a => f a -> g a) -> b f -> b g
bmapC forall (a :: k). c a => f a -> g a
f b f
bf
  = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap forall (a :: k). Product (Dict c) f a -> g a
go (forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts b f
bf)
  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 'btraverse' but with a constraint on the elements of @b@.
btraverseC
  :: forall c b f g e
  .  (TraversableB b, ConstraintsB b, AllB c b, Applicative e)
  => (forall a. c a => f a -> e (g a))
  -> b f
  -> e (b g)
btraverseC :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *) (e :: * -> *).
(TraversableB b, ConstraintsB b, AllB c b, Applicative e) =>
(forall (a :: k). c a => f a -> e (g a)) -> b f -> e (b g)
btraverseC forall (a :: k). c a => f a -> e (g a)
f b f
b
  = forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
       (g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
btraverse (\(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 k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts b f
b)

bfoldMapC
  :: forall c b m f
  .  (TraversableB b, ConstraintsB b,  AllB c b, Monoid m)
  => (forall a. c a => f a -> m)
  -> b f
  -> m
bfoldMapC :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *) m
       (f :: k -> *).
(TraversableB b, ConstraintsB b, AllB c b, Monoid m) =>
(forall (a :: k). c a => f a -> m) -> b f -> m
bfoldMapC 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} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *) (e :: * -> *).
(TraversableB b, ConstraintsB b, AllB c b, Applicative e) =>
(forall (a :: k). c a => f a -> e (g a)) -> b f -> e (b g)
btraverseC @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.bzipWith' but with a constraint on the elements of @b@.
bzipWithC
  :: forall c b f g h
  .  (AllB c b, ConstraintsB b, ApplicativeB b)
  => (forall a. c a => f a -> g a -> h a)
  -> b f
  -> b g
  -> b h
bzipWithC :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *) (h :: k -> *).
(AllB c b, ConstraintsB b, ApplicativeB b) =>
(forall (a :: k). c a => f a -> g a -> h a) -> b f -> b g -> b h
bzipWithC forall (a :: k). c a => f a -> g a -> h a
f b f
bf b g
bg
  = forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *).
(AllB c b, ConstraintsB b) =>
(forall (a :: k). c a => f a -> g a) -> b f -> b g
bmapC @c forall (a :: k). c a => Product f g a -> h a
go (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg)
  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.bzipWith3' but with a constraint on the elements of @b@.
bzipWith3C
  :: forall c b f g h i
  .  (AllB c b, ConstraintsB b, ApplicativeB b)
  => (forall a. c a => f a -> g a -> h a -> i a)
  -> b f -> b g -> b h -> b i
bzipWith3C :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *).
(AllB c b, ConstraintsB b, ApplicativeB b) =>
(forall (a :: k). c a => f a -> g a -> h a -> i a)
-> b f -> b g -> b h -> b i
bzipWith3C forall (a :: k). c a => f a -> g a -> h a -> i a
f b f
bf b g
bg b h
bh
  = forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *).
(AllB c b, ConstraintsB b) =>
(forall (a :: k). c a => f a -> g a) -> b f -> b g
bmapC @c forall (a :: k). c a => Product (Product f g) h a -> i a
go (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b h
bh)
  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.bzipWith4' but with a constraint on the elements of @b@.
bzipWith4C
  :: forall c b f g h i j
  .  (AllB c b, ConstraintsB b, ApplicativeB b)
  => (forall a. c a => f a -> g a -> h a -> i a -> j a)
  -> b f -> b g -> b h -> b i -> b j
bzipWith4C :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *) (h :: k -> *) (i :: k -> *)
       (j :: k -> *).
(AllB c b, ConstraintsB b, ApplicativeB b) =>
(forall (a :: k). c a => f a -> g a -> h a -> i a -> j a)
-> b f -> b g -> b h -> b i -> b j
bzipWith4C forall (a :: k). c a => f a -> g a -> h a -> i a -> j a
f b f
bf b g
bg b h
bh b i
bi
  = forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *)
       (f :: k -> *) (g :: k -> *).
(AllB c b, ConstraintsB b) =>
(forall (a :: k). c a => f a -> g a) -> b f -> b g
bmapC @c forall (a :: k).
c a =>
Product (Product (Product f g) h) i a -> j a
go (b f
bf forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b g
bg forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b h
bh forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
ApplicativeB b =>
b f -> b g -> b (Product f g)
`bprod` b i
bi)
  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 'AllB' but will put the functor argument @f@
--   between the constraint @c@ and the type @a@. For example:
--
--   @
--   'AllB'  'Show'   Person ~ ('Show'    'String',  'Show'    'Int')
--   'AllBF' 'Show' f Person ~ ('Show' (f 'String'), 'Show' (f 'Int'))
--   @
type AllBF c f b = AllB (ClassF c f) b


-- | Similar to 'baddDicts' but can produce the instance dictionaries
--   "out of the blue".
bdicts
  :: forall c b
  . (ConstraintsB b, ApplicativeB b,  AllB c b)
  => b (Dict c)
bdicts :: forall {k} (c :: k -> Constraint) (b :: (k -> *) -> *).
(ConstraintsB b, ApplicativeB b, AllB c b) =>
b (Dict c)
bdicts
  = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (\(Pair Dict c a
c Proxy a
_) -> Dict c a
c) forall a b. (a -> b) -> a -> b
$ forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts forall a b. (a -> b) -> a -> b
$ forall k (b :: (k -> *) -> *) (f :: k -> *).
ApplicativeB b =>
(forall (a :: k). f a) -> b f
bpure forall {k} (t :: k). Proxy t
Proxy


-- | Like 'bpure' but a constraint is allowed to be required on
--   each element of @b@.
bpureC
  :: forall c f b
  .  ( AllB c b
     , ConstraintsB b
     , ApplicativeB b
     )
  => (forall a . c a => f a)
  -> b f
bpureC :: forall {k} (c :: k -> Constraint) (f :: k -> *)
       (b :: (k -> *) -> *).
(AllB c b, ConstraintsB b, ApplicativeB b) =>
(forall (a :: k). c a => f a) -> b f
bpureC forall (a :: k). c a => f a
fa
  = forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
FunctorB b =>
(forall (a :: k). f a -> g a) -> b f -> b g
bmap (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 {k} (c :: k -> Constraint) (b :: (k -> *) -> *).
(ConstraintsB b, ApplicativeB b, AllB c b) =>
b (Dict c)
bdicts

-- | Builds a @b f@, by applying 'mempty' on every field of @b@.
bmempty
  :: forall f b
  .  ( AllBF Monoid f b
     , ConstraintsB b
     , ApplicativeB b
     )
  => b f
bmempty :: forall {k} (f :: k -> *) (b :: (k -> *) -> *).
(AllBF Monoid f b, ConstraintsB b, ApplicativeB b) =>
b f
bmempty
  = forall {k} (c :: k -> Constraint) (f :: k -> *)
       (b :: (k -> *) -> *).
(AllB c b, ConstraintsB b, ApplicativeB b) =>
(forall (a :: k). c a => f a) -> b f
bpureC @(ClassF Monoid f) forall a. Monoid a => a
mempty


-- | @'CanDeriveConstraintsB' B f g@ is in practice a predicate about @B@ only.
--   Intuitively, it says that the following holds, for any arbitrary @f@:
--
--     * There is an instance of @'Generic' (B f)@.
--
--     * @B f@ can contain fields of type @b f@ as long as there exists a
--       @'ConstraintsB' b@ instance. In particular, recursive usages of @B f@
--       are allowed.
type CanDeriveConstraintsB c b f
  = ( GenericN (b f)
    , GenericN (b (Dict c `Product` f))
    , AllB c b ~ GAll 0 c (GAllRepB b)
    , GConstraints 0 c f (GAllRepB b) (RepN (b f)) (RepN (b (Dict c `Product` f)))
    )

-- | The representation used for the generic computation of the @'AllB' c b@
--   constraints.
type GAllRepB b = TagSelf0 b


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

-- | Default implementation of 'baddDicts' based on 'Generic'.
gbaddDictsDefault
  :: forall b c f
  . ( CanDeriveConstraintsB c b f
    , AllB c b
    )
  => b f
  -> b (Dict c `Product` f)
gbaddDictsDefault :: forall {k} (b :: (k -> *) -> *) (c :: k -> Constraint)
       (f :: k -> *).
(CanDeriveConstraintsB c b f, AllB c b) =>
b f -> b (Product (Dict c) f)
gbaddDictsDefault
  = 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 @0 @c @f @(GAllRepB b) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. GenericN a => a -> RepN a x
fromN
{-# INLINE gbaddDictsDefault #-}


-- ------------------------------------------------------------
-- Generic derivation: Special cases for ConstraintsB
-- -----------------------------------------------------------

type P = Param

-- Break recursive case
type instance GAll 0 c (Self (b' (P 0 X)) (b X)) = ()

instance
  ( ConstraintsB b
  , AllB c b
  ) => -- b' is b with maybe some Param occurrences
       GConstraints 0 c f (Self (b' (P 0 X)) (b X))
                          (Rec (b' (P 0 f)) (b f))
                          (Rec (b' (P 0 (Dict c `Product` f)))
                               (b       (Dict c `Product` f)))
  where
  gaddDicts :: forall (x :: k).
GAll 0 c (Self (b' (P 0 X)) (b X)) =>
Rec (b' (P 0 f)) (b f) x
-> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) 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 (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts 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 0 c (Other (b' (P 0 X)) (b X)) = AllB c b


instance
  ( ConstraintsB b
  , AllB c b
  ) => -- b' is b with maybe some Param occurrences
       GConstraints 0 c f (Other (b' (P 0 X)) (b X))
                          (Rec (b' (P 0 f)) (b f))
                          (Rec (b' (P 0 (Dict c `Product` f)))
                               (b       (Dict c `Product` f)))
  where
  gaddDicts :: forall (x :: k).
GAll 0 c (Other (b' (P 0 X)) (b X)) =>
Rec (b' (P 0 f)) (b f) x
-> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) 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 (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts 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 #-}


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

instance ConstraintsB Proxy where
  type AllB c Proxy = ()

  baddDicts :: forall (c :: k -> Constraint) (f :: k -> *).
AllB c Proxy =>
Proxy f -> Proxy (Product (Dict c) f)
baddDicts Proxy f
_ = forall {k} (t :: k). Proxy t
Proxy
  {-# INLINE baddDicts #-}

instance (ConstraintsB a, ConstraintsB b) => ConstraintsB (Product a b) where
  type AllB c (Product a b) = (AllB c a, AllB c b)

  baddDicts :: forall (c :: k -> Constraint) (f :: k -> *).
AllB c (Product a b) =>
Product a b f -> Product a b (Product (Dict c) f)
baddDicts (Pair a f
x b f
y) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts a f
x) (forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts b f
y)
  {-# INLINE baddDicts #-}

instance (ConstraintsB a, ConstraintsB b) => ConstraintsB (Sum a b) where
  type AllB c (Sum a b) = (AllB c a, AllB c b)

  baddDicts :: forall (c :: k -> Constraint) (f :: k -> *).
AllB c (Sum a b) =>
Sum a b f -> Sum a b (Product (Dict c) f)
baddDicts (InL a f
x) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts a f
x)
  baddDicts (InR b f
x) = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts b f
x)
  {-# INLINE baddDicts #-}

instance ConstraintsB (Const a) where
  type AllB c (Const a) = ()

  baddDicts :: forall (c :: k -> Constraint) (f :: k -> *).
AllB c (Const a) =>
Const a f -> Const a (Product (Dict c) f)
baddDicts (Const a
x) = forall {k} a (b :: k). a -> Const a b
Const a
x
  {-# INLINE baddDicts #-}

instance (Functor f, ConstraintsB b) => ConstraintsB (f `Compose` b) where
  type AllB c (f `Compose` b) = AllB c b

  baddDicts :: forall (c :: k -> Constraint) (f :: k -> *).
AllB c (Compose f b) =>
Compose f b f -> Compose f b (Product (Dict c) f)
baddDicts (Compose f (b f)
x)
    = forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
(ConstraintsB b, AllB c b) =>
b f -> b (Product (Dict c) f)
baddDicts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (b f)
x)
  {-# INLINE baddDicts #-}

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

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

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

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

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

  TagSelf0' (b :: kf -> Type)
            (Rec ((b'  :: kf -> Type) f)
                 ((b'' :: kf -> Type) g)
            )
    = (SelfOrOther b b') (b' f) (b'' g)

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

  TagSelf0' b U1
    = U1

  TagSelf0' b V1
    = V1