    {-# 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 = b f -> b (Product (Dict c) f)
    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 (a :: k). Product (Dict c) f a -> g a)
    -> b (Product (Dict c) f) -> b g
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap Product (Dict c) f a -> g a
    forall (a :: k). Product (Dict c) f a -> g a
    go (b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    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) = (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 '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 (a :: k). Product (Dict c) f a -> e (g a))
    -> b (Product (Dict c) f) -> e (b g)
    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)
    forall (e :: * -> *) (f :: k -> *) (g :: k -> *).
    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) -> f a -> e (g a)
    forall (a :: k). c a => f a -> e (g a)
    f f a
    x) (b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    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 = Const m (b Any) -> m
    forall {k} a (b :: k). Const a b -> a
    getConst (Const m (b Any) -> m) -> (b f -> Const m (b Any)) -> b f -> m
    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)
    forall (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 (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.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
    forall (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 Product f g a -> h a
    forall (a :: k). c a => Product f g a -> h a
    go (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). 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) = 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.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
    forall (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 Product (Product f g) h a -> i a
    forall (a :: k). c a => Product (Product f g) h a -> i a
    go (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg b (Product f g) -> b h -> b (Product (Product f g) h)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). 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) = 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.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
    forall (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 Product (Product (Product f g) h) i a -> j a
    forall (a :: k).
    c a =>
    Product (Product (Product f g) h) i a -> j a
    go (b f
    bf b f -> b g -> b (Product f g)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b g
    bg b (Product f g) -> b h -> b (Product (Product f g) h)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). b f -> b g -> b (Product f g)
    `bprod` b h
    bh b (Product (Product f g) h)
    -> b i -> b (Product (Product (Product f g) h) i)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    ApplicativeB b =>
    b f -> b g -> b (Product f g)
    forall (f :: k -> *) (g :: k -> *). 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) = 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 '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 (a :: k). Product (Dict c) Proxy a -> Dict c a)
    -> b (Product (Dict c) Proxy) -> b (Dict c)
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (forall (a :: k). f a -> g a) -> b f -> b g
    bmap (\(Pair Dict c a
    c Proxy a
    _) -> Dict c a
    c) (b (Product (Dict c) Proxy) -> b (Dict c))
    -> b (Product (Dict c) Proxy) -> b (Dict c)
    forall a b. (a -> b) -> a -> b
    $ b Proxy -> b (Product (Dict c) Proxy)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    AllB c b =>
    b f -> b (Product (Dict c) f)
    baddDicts (b Proxy -> b (Product (Dict c) Proxy))
    -> b Proxy -> b (Product (Dict c) Proxy)
    forall a b. (a -> b) -> a -> b
    $ (forall (a :: k). Proxy a) -> b Proxy
    forall k (b :: (k -> *) -> *) (f :: k -> *).
    ApplicativeB b =>
    (forall (a :: k). f a) -> b f
    forall (f :: k -> *). (forall (a :: k). f a) -> b f
    bpure Proxy a
    forall (a :: k). Proxy a
    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 (a :: k). Dict c a -> f a) -> b (Dict c) -> b f
    forall k (b :: (k -> *) -> *) (f :: k -> *) (g :: k -> *).
    FunctorB b =>
    (forall (a :: k). f a -> g a) -> b f -> b g
    forall (f :: k -> *) (g :: k -> *).
    (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
    forall (c :: k -> Constraint) (a :: k) r.
    (c a => r) -> Dict c a -> r
    requiringDict @c f a
    c a => f a
    forall (a :: k). c a => f a
    fa) b (Dict c)
    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
    forall (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) f a
    forall (a :: k). ClassF Monoid f a => f a
    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
      = RepN (b (Product (Dict c) f)) Any -> b (Product (Dict c) f)
    Zip
      (Rep (Indexed b 1 (Param 0 (Product (Dict c) f))))
      (Rep (b (Product (Dict c) f)))
      Any
    -> b (Product (Dict c) f)
    forall a x. GenericN a => RepN a x -> a
    forall x. RepN (b (Product (Dict c) f)) x -> b (Product (Dict c) f)
    toN (Zip
       (Rep (Indexed b 1 (Param 0 (Product (Dict c) f))))
       (Rep (b (Product (Dict c) f)))
       Any
     -> b (Product (Dict c) f))
    -> (b f
        -> Zip
             (Rep (Indexed b 1 (Param 0 (Product (Dict c) f))))
             (Rep (b (Product (Dict c) f)))
             Any)
    -> b f
    -> b (Product (Dict c) f)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (n :: Nat) (c :: k -> Constraint) (f :: k -> *)
           (repbx :: * -> *) (repbf :: * -> *) (repbdf :: * -> *) x.
    (GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
    repbf x -> repbdf x
    forall {k} {k1} {k2} (n :: Nat) (c :: k -> Constraint) (f :: k1)
           (repbx :: * -> *) (repbf :: k2 -> *) (repbdf :: k2 -> *) (x :: k2).
    (GConstraints n c f repbx repbf repbdf, GAll n c repbx) =>
    repbf x -> repbdf x
    gaddDicts @0 @c @f @(GAllRepB b) (Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any
     -> Zip
          (Rep (Indexed b 1 (Param 0 (Product (Dict c) f))))
          (Rep (b (Product (Dict c) f)))
          Any)
    -> (b f -> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any)
    -> b f
    -> Zip
         (Rep (Indexed b 1 (Param 0 (Product (Dict c) f))))
         (Rep (b (Product (Dict c) f)))
         Any
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b f -> RepN (b f) Any
    b f -> Zip (Rep (Indexed b 1 (Param 0 f))) (Rep (b f)) Any
    forall x. b f -> RepN (b f) x
    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 :: k2).
    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
        = K1 R (b (Product (Dict c) f)) x
    -> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (b (Product (Dict c) f)) x
     -> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) x)
    -> (Rec (b' (P 0 f)) (b f) x -> K1 R (b (Product (Dict c) f)) x)
    -> Rec (b' (P 0 f)) (b f) x
    -> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b (Product (Dict c) f) -> K1 R (b (Product (Dict c) f)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b (Product (Dict c) f) -> K1 R (b (Product (Dict c) f)) x)
    -> (Rec (b' (P 0 f)) (b f) x -> b (Product (Dict c) f))
    -> Rec (b' (P 0 f)) (b f) x
    -> K1 R (b (Product (Dict c) f)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    AllB c b =>
    b f -> b (Product (Dict c) f)
    baddDicts (b f -> b (Product (Dict c) f))
    -> (Rec (b' (P 0 f)) (b f) x -> b f)
    -> Rec (b' (P 0 f)) (b f) x
    -> b (Product (Dict c) f)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (b f) x -> b f
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (b f) x -> b f)
    -> (Rec (b' (P 0 f)) (b f) x -> K1 R (b f) x)
    -> Rec (b' (P 0 f)) (b f) x
    -> b f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (b' (P 0 f)) (b f) x -> K1 R (b f) x
    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 :: k2).
    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
        = K1 R (b (Product (Dict c) f)) x
    -> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (b (Product (Dict c) f)) x
     -> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) x)
    -> (Rec (b' (P 0 f)) (b f) x -> K1 R (b (Product (Dict c) f)) x)
    -> Rec (b' (P 0 f)) (b f) x
    -> Rec (b' (P 0 (Product (Dict c) f))) (b (Product (Dict c) f)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b (Product (Dict c) f) -> K1 R (b (Product (Dict c) f)) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (b (Product (Dict c) f) -> K1 R (b (Product (Dict c) f)) x)
    -> (Rec (b' (P 0 f)) (b f) x -> b (Product (Dict c) f))
    -> Rec (b' (P 0 f)) (b f) x
    -> K1 R (b (Product (Dict c) f)) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    AllB c b =>
    b f -> b (Product (Dict c) f)
    baddDicts (b f -> b (Product (Dict c) f))
    -> (Rec (b' (P 0 f)) (b f) x -> b f)
    -> Rec (b' (P 0 f)) (b f) x
    -> b (Product (Dict c) f)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (b f) x -> b f
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (b f) x -> b f)
    -> (Rec (b' (P 0 f)) (b f) x -> K1 R (b f) x)
    -> Rec (b' (P 0 f)) (b f) x
    -> b f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (b' (P 0 f)) (b f) x -> K1 R (b f) x
    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
    _ = Proxy (Product (Dict c) 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) = a (Product (Dict c) f)
    -> b (Product (Dict c) f) -> Product a b (Product (Dict c) f)
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair (a f -> a (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    AllB c a =>
    a f -> a (Product (Dict c) f)
    baddDicts a f
    x) (b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    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) = a (Product (Dict c) f) -> Sum a b (Product (Dict c) f)
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
    InL (a f -> a (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    AllB c a =>
    a f -> a (Product (Dict c) f)
    baddDicts a f
    x)
      baddDicts (InR b f
    x) = b (Product (Dict c) f) -> Sum a b (Product (Dict c) f)
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
    InR (b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    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) = a -> Const a (Product (Dict c) f)
    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)
        = f (b (Product (Dict c) f)) -> Compose f b (Product (Dict c) f)
    forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
    f (g a) -> Compose f g a
    Compose (b f -> b (Product (Dict c) f)
    forall k (b :: (k -> *) -> *) (c :: k -> Constraint) (f :: k -> *).
    (ConstraintsB b, AllB c b) =>
    b f -> b (Product (Dict c) f)
    forall (c :: k -> Constraint) (f :: k -> *).
    AllB c b =>
    b f -> b (Product (Dict c) f)
    baddDicts (b f -> b (Product (Dict c) f))
    -> f (b f) -> f (b (Product (Dict c) f))
    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