I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:

dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
             Typeable t
          => (forall d. Data d => c (t d))
          -> Maybe (c a)

But this doesn't typecheck:

    • Could not deduce (Typeable (t k0))
      from the context: (Data a, Typeable (t k))
        bound by the type signature for:
                   dataCast1 :: forall a.
                                Data a =>
                                forall k (c :: * -> *) (t :: forall k1. k1 -> *).
                                Typeable (t k) =>
                                (forall d. Data d => c (t * d)) -> Maybe (c a)
        at NewData.hs:(170,3)-(173,26)
      The type variable ‘k0’ is ambiguous
    • In the ambiguity check for ‘dataCast1’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        dataCast1 :: forall a.
                     Data a =>
                     forall k (c :: * -> *) (t :: forall k1. k1 -> *).
                     Typeable (t k) =>
                     (forall d. Data d => c (t * d)) -> Maybe (c a)
      In the class declaration for ‘Data’
    |
170 |   dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
    |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

This makes sense, since GHC has no way to conclude that the k in t's kind is also Typeable. I tried to convince GHC of that fact:

dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).
             Typeable t
          => (forall d. Data d => c (t d))
          -> Maybe (c a)

But this also doesn't work:

NewData.hs:171:25: error:
    • Illegal constraint in a type: Typeable k0
    • In the first argument of ‘Typeable’, namely ‘t’
      In the type signature:
        dataCast1 :: forall (c :: Type -> Type)
                            (t :: forall (k :: Type). Typeable k => k -> Type).
                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
      In the class declaration for ‘Data’
    |
171 |                Typeable t
    |                         ^

NewData.hs:172:40: error:
    • Illegal constraint in a type: Typeable k0
    • In the first argument of ‘c’, namely ‘(t d)’
      In the type signature:
        dataCast1 :: forall (c :: Type -> Type)
                            (t :: forall (k :: Type). Typeable k => k -> Type).
                     Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
      In the class declaration for ‘Data’
    |
172 |             => (forall d. Data d => c (t d))
    |                                        ^^^

At this point, I'm stuck, since I have no idea how to work around this Illegal constraint in a type error. This error message appears to have originated as a part of the TypeInType patch, since there's even a test case checking for this behavior.

But is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?