GitLab

Consider

{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)

data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c

GHC rejects this with

Foo.hs:10:9: error:
    • Different names for the same type variable: ‘p’ and ‘q’
    • In the data declaration for ‘T’
   |
10 | data T1 (a :: p) (b :: q) c = MkT (SameKind a b) c
   |         ^^^^^^^^^^^^^^^^^^

If T is a CUSK, it is similarly rejected, abeit with a different message

{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures #-}
data SameKind (a :: k) (b :: k)

data T2 (a :: p) (b :: q) = MkT (SameKind a b)

we get

Foo.hs:10:45: error:
    • Expected kind ‘p’, but ‘b’ has kind ‘q’
      ‘q’ is a rigid type variable bound by
        the data type declaration for ‘T2’
        at Foo.hs:10:10-24
      ‘p’ is a rigid type variable bound by
        the data type declaration for ‘T2’
        at Foo.hs:10:10-24
    • In the second argument of ‘SameKind’, namely ‘b’
      In the type ‘(SameKind a b)’
      In the definition of data constructor ‘MkT’
   |
10 | data T2 (a :: p) (b :: q) = MkT (SameKind a b)
   |                                             ^

because p and q are created as distinct skolems.

BUT alas with standalone kind signatures we don't this

{-# LANGUAGE CUSKs, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}

type T3 :: k -> k -> Type
data T3 (a :: p) (b :: q) = MkT

This is accepted by HEAD. That's highly inconsistent. We should reject.