    {-# LANGUAGE AllowAmbiguousTypes  #-}
    {-# LANGUAGE TypeFamilies         #-}
    {-# LANGUAGE PolyKinds            #-}
    module Barbies.Generics.Constraints
      ( GAll
      , X, Y
      , Self, Other, SelfOrOther
      , GConstraints(..)
      )

    where

    import Barbies.Internal.Dicts(Dict (..))

    import Data.Functor.Product (Product (..))
    import Data.Kind            (Constraint, Type)
    import GHC.TypeLits         (Nat)

    import Data.Generics.GenericN

    class GConstraints n c f repbx repbf repbdf where
      gaddDicts :: GAll n c repbx => repbf x -> repbdf x

    type family GAll (n :: Nat) (c :: k -> Constraint) (repbf :: Type -> Type) :: Constraint

    data X a
    data family Y :: k

    -- ----------------------------------
    -- Trivial cases
    -- ----------------------------------

    type instance GAll n c (M1 i k repbf) = GAll n c repbf

    instance
      GConstraints n c f repbx repbf repbdf
        => GConstraints n c f (M1 i k repbx)
                              (M1 i k repbf)
                              (M1 i k repbdf)
      where
      gaddDicts :: forall (x :: k).
    GAll n c (M1 i k repbx) =>
    M1 i k repbf x -> M1 i k repbdf x
    gaddDicts
        = repbdf x -> M1 i k repbdf x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 (repbdf x -> M1 i k repbdf x)
    -> (M1 i k repbf x -> repbdf x)
    -> M1 i k repbf x
    -> M1 i k repbdf x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (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 {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 @n @c @f @repbx (repbf x -> repbdf x)
    -> (M1 i k repbf x -> repbf x) -> M1 i k repbf x -> repbdf x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . M1 i k repbf x -> repbf x
    forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
    unM1
      {-# INLINE gaddDicts #-}

    type instance GAll n c V1 = ()

    instance GConstraints n c f V1 V1 V1 where
      gaddDicts :: forall (x :: k). GAll n c V1 => V1 x -> V1 x
    gaddDicts V1 x
    _ = V1 x
    forall a. HasCallStack => a
    undefined

    type instance GAll n c U1 = ()

    instance GConstraints n c f U1 U1 U1 where
      gaddDicts :: forall (x :: k). GAll n c U1 => U1 x -> U1 x
    gaddDicts = U1 x -> U1 x
    forall a. a -> a
    id
      {-# INLINE gaddDicts #-}

    type instance GAll n c (l :*: r)
      = (GAll n c l, GAll n c r)

    instance
      ( GConstraints n c f lx lf ldf
      , GConstraints n c f rx rf rdf
      ) => GConstraints n c f (lx  :*: rx)
                              (lf  :*: rf)
                              (ldf :*: rdf)
      where
      gaddDicts :: forall (x :: k).
    GAll n c (lx :*: rx) =>
    (:*:) lf rf x -> (:*:) ldf rdf x
    gaddDicts (lf x
    l :*: rf x
    r)
        = (forall (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 {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 @n @c @f @lx lf x
    l) ldf x -> rdf x -> (:*:) ldf rdf x
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: (forall (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 {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 @n @c @f @rx rf x
    r)
      {-# INLINE gaddDicts #-}

    type instance GAll n c (l :+: r) = (GAll n c l, GAll n c r)

    instance
      ( GConstraints n c f lx lf ldf
      , GConstraints n c f rx rf rdf
      ) => GConstraints n c f (lx  :+: rx)
                              (lf  :+: rf)
                              (ldf :+: rdf)
      where
      gaddDicts :: forall (x :: k).
    GAll n c (lx :+: rx) =>
    (:+:) lf rf x -> (:+:) ldf rdf x
    gaddDicts = \case
        L1 lf x
    l -> ldf x -> (:+:) ldf rdf x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
    L1 (forall (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 {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 @n @c @f @lx lf x
    l)
        R1 rf x
    r -> rdf x -> (:+:) ldf rdf x
    forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
    R1 (forall (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 {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 @n @c @f @rx rf x
    r)
      {-# INLINE gaddDicts #-}

    -- --------------------------------
    -- The interesting cases
    -- --------------------------------

    type P = Param

    type instance GAll n c (Rec l r) = GAllRec n c l r
    type family GAllRec
      (n :: Nat)
      (c :: k -> Constraint)
      (l :: Type)
      (r :: Type) :: Constraint
      where
        GAllRec n c (P n X _) (X a) = c a
        GAllRec _ _ _ _ = ()

    -- {{ Functor application -----------------------------------------------------
    instance
      -- a' is a, maybe with Param applications
      GConstraints n c f (Rec (P n X a') (X a))
                         (Rec (P n f a') (f a))
                         (Rec (P n (Dict c `Product` f) a')
                                  ((Dict c `Product` f) a))
      where
      gaddDicts :: forall (x :: k).
    GAll n c (Rec (P n X a') (X a)) =>
    Rec (P n f a') (f a) x
    -> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
    gaddDicts
        = K1 R (Product (Dict c) f a) x
    -> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
    forall {k} p a (x :: k). K1 R a x -> Rec p a x
    Rec (K1 R (Product (Dict c) f a) x
     -> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x)
    -> (Rec (P n f a') (f a) x -> K1 R (Product (Dict c) f a) x)
    -> Rec (P n f a') (f a) x
    -> Rec (P n (Product (Dict c) f) a') (Product (Dict c) f a) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Product (Dict c) f a -> K1 R (Product (Dict c) f a) x
    forall k i c (p :: k). c -> K1 i c p
    K1 (Product (Dict c) f a -> K1 R (Product (Dict c) f a) x)
    -> (Rec (P n f a') (f a) x -> Product (Dict c) f a)
    -> Rec (P n f a') (f a) x
    -> K1 R (Product (Dict c) f a) x
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dict c a -> f a -> Product (Dict c) f a
    forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
    f a -> g a -> Product f g a
    Pair Dict c a
    forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
    Dict (f a -> Product (Dict c) f a)
    -> (Rec (P n f a') (f a) x -> f a)
    -> Rec (P n f a') (f a) x
    -> Product (Dict c) f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . K1 R (f a) x -> f a
    forall k i c (p :: k). K1 i c p -> c
    unK1 (K1 R (f a) x -> f a)
    -> (Rec (P n f a') (f a) x -> K1 R (f a) x)
    -> Rec (P n f a') (f a) x
    -> f a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rec (P n f a') (f a) x -> K1 R (f a) x
    forall {k} p a (x :: k). Rec p a x -> K1 R a x
    unRec
      {-# INLINE gaddDicts #-}

    -- }} Functor application -----------------------------------------------------

    -- {{ Not a functor application -----------------------------------------------

    instance
      -- b is a, but with X or Y instead of Param ...
      -- a' is a, maybe with occurrences of Param
      -- b' is b, maybe with occurences of Param
      GConstraints n c f (Rec a' a) -- a' may contain Y or Param m (m > n)
                         (Rec b' b) -- a'' may only contain Param m (m > n)
                         (Rec b' b)
      where
      gaddDicts :: forall (x :: k). GAll n c (Rec a' a) => Rec b' b x -> Rec b' b x
    gaddDicts = Rec b' b x -> Rec b' b x
    forall a. a -> a
    id
      {-# INLINE gaddDicts #-}
    -- }} Not a functor application -----------------------------------------------

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

    data Self  (p :: Type) (a :: Type) (x :: Type)
    data Other (p :: Type) (a :: Type) (x :: Type)

    type family SelfOrOther (b :: k) (b' :: k) :: Type -> Type -> Type -> Type where
      SelfOrOther b b = Self
      SelfOrOther b b' = Other