    {-# LANGUAGE AllowAmbiguousTypes  #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE PolyKinds            #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# OPTIONS_GHC -Wno-orphans #-}
    module Barbies.Internal.ConstraintsT
      ( ConstraintsT(..)
      , tmapC
      , ttraverseC
      , tforC
      , 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 {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 (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
    forall (f :: k -> *) (g :: k -> *) (x :: kr).
    (forall (a :: k). f a -> g a) -> t f x -> t g x
    tmap Product (Dict c) f a -> g a
    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
    forall (c :: k -> Constraint) (f :: k -> *) (x :: kr).
    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) = (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 {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 (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)
    forall (e :: * -> *) (f :: k -> *) (g :: k -> *) (x :: kr).
    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) -> 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
    forall (c :: k -> Constraint) (f :: k -> *) (x :: kr).
    AllT c t =>
    t f x -> t (Product (Dict c) f) x
    taddDicts t f x
    t)

    -- | Like 'ttraverseC' but with the arguments flipped.
    --
    -- @since 2.1.0.0
    tforC
      :: forall c t f g e x
      .  (TraversableT t, ConstraintsT t, AllT c t, Applicative e)
      => t f x
      -> (forall a. c a => f a -> e (g a))
      -> e (t g x)
    tforC :: forall {kl} {kr} (c :: kl -> Constraint)
           (t :: (kl -> *) -> kr -> *) (f :: kl -> *) (g :: kl -> *)
           (e :: * -> *) (x :: kr).
    (TraversableT t, ConstraintsT t, AllT c t, Applicative e) =>
    t f x -> (forall (a :: kl). c a => f a -> e (g a)) -> e (t g x)
    tforC t f x
    t forall (a :: kl). c a => f a -> e (g a)
    f
      = 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)
    forall (c :: kl -> Constraint) (t :: (kl -> *) -> kr -> *)
           (f :: kl -> *) (g :: kl -> *) (e :: * -> *) (x :: kr).
    (TraversableT t, ConstraintsT t, AllT c t, Applicative e) =>
    (forall (a :: kl). c a => f a -> e (g a)) -> t f x -> e (t g x)
    ttraverseC @c f a -> e (g a)
    forall (a :: kl). c a => f a -> e (g a)
    f 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 = Const m (t (ZonkAny 1) x) -> m
    forall {k} a (b :: k). Const a b -> a
    getConst (Const m (t (ZonkAny 1) x) -> m)
    -> (t f x -> Const m (t (ZonkAny 1) x)) -> t f x -> m
    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)
    forall (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 (ZonkAny 1 a)
    forall {k} a (b :: k). a -> Const a b
    Const (m -> Const m (ZonkAny 1 a))
    -> (f a -> m) -> f a -> Const m (ZonkAny 1 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 {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
    forall (c :: k -> Constraint) (t :: (k -> *) -> k' -> *)
           (f :: k -> *) (g :: k -> *) (x :: k').
    (AllT c t, ConstraintsT t) =>
    (forall (a :: k). c a => f a -> g a) -> t f x -> t g x
    tmapC @c Product f g a -> h a
    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
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    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) = 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 {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
    forall (c :: k -> Constraint) (t :: (k -> *) -> k' -> *)
           (f :: k -> *) (g :: k -> *) (x :: k').
    (AllT c t, ConstraintsT t) =>
    (forall (a :: k). c a => f a -> g a) -> t f x -> t g x
    tmapC @c Product (Product f g) h a -> i a
    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
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    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
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    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) = 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 {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
    forall (c :: k -> Constraint) (t :: (k -> *) -> k' -> *)
           (f :: k -> *) (g :: k -> *) (x :: k').
    (AllT c t, ConstraintsT t) =>
    (forall (a :: k). c a => f a -> g a) -> t f x -> t g x
    tmapC @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 (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
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    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
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    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
    forall (f :: k -> *) (x :: k') (g :: k -> *).
    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) = 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 :: forall {kl} {kr} (c :: kl -> Constraint)
           (t :: (kl -> *) -> kr -> *) (x :: kr).
    (ConstraintsT t, ApplicativeT t, AllT c t) =>
    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
    forall (f :: kl -> *) (g :: kl -> *) (x :: kr).
    (forall (a :: kl). f a -> g a) -> t f x -> t g x
    tmap (\(Pair Dict c a
    c Proxy a
    _) -> 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
    forall (c :: kl -> Constraint) (f :: kl -> *) (x :: kr).
    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
    forall (f :: kl -> *) (x :: kr). (forall (a :: kl). f a) -> t f x
    tpure Proxy a
    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 {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 (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
    forall (f :: k -> *) (g :: k -> *) (x :: k').
    (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
    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) 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 :: 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
    forall (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) f a
    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 :: 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
      = RepN (t (Product (Dict c) f) x) (ZonkAny 0)
    -> t (Product (Dict c) f) x
    Zip
      (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
      (Rep (t (Product (Dict c) f) x))
      (ZonkAny 0)
    -> t (Product (Dict c) f) x
    forall a x. GenericN a => RepN a x -> a
    forall x.
    RepN (t (Product (Dict c) f) x) x -> t (Product (Dict c) f) x
    toN (Zip
       (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
       (Rep (t (Product (Dict c) f) x))
       (ZonkAny 0)
     -> 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))
             (ZonkAny 0))
    -> t f x
    -> t (Product (Dict c) f) x
    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 @1 @c @f @(GAllRepT t) (Zip
       (Rep (Indexed t 2 (Param 1 f) (Param 0 x)))
       (Rep (t f x))
       (ZonkAny 0)
     -> Zip
          (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
          (Rep (t (Product (Dict c) f) x))
          (ZonkAny 0))
    -> (t f x
        -> Zip
             (Rep (Indexed t 2 (Param 1 f) (Param 0 x)))
             (Rep (t f x))
             (ZonkAny 0))
    -> t f x
    -> Zip
         (Rep (Indexed t 2 (Param 1 (Product (Dict c) f)) (Param 0 x)))
         (Rep (t (Product (Dict c) f) x))
         (ZonkAny 0)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . t f x -> RepN (t f x) (ZonkAny 0)
    t f x
    -> Zip
         (Rep (Indexed t 2 (Param 1 f) (Param 0 x)))
         (Rep (t f x))
         (ZonkAny 0)
    forall x. t f x -> RepN (t f x) x
    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 :: k2).
    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
        = 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
    forall (c :: k -> Constraint) (f :: k -> *) (x :: k).
    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 k i c (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 {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 :: k2).
    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
        = 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
    forall (c :: k -> Constraint) (f :: k -> *) (x :: k).
    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 k i c (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 {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