Consider

data SameKind :: k -> k -> *

data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)

This code should be rejected. Yet it is accepted. The problem is that, when kind-checking a datatype declaration without a CUSK, GHC uses SigTvs for user-written kind variables. SigTvs are allowed to unify with other SigTvs, leading to incorrect behavior here.

The motivating scenario is this:

data T (a :: k1) x = MkT (S a ())
data S (b :: k2) y = MkS (T b ())

This program should be accepted. Neither type has a CUSK and therefore is not generalized before kind-checking the group. GHC must then unify k1 and k2. If they were skolems, this unification would fail and this pair of definitions would be rejected.

This ticket is identical in spirit to #9201 (closed), but that example has a CUSK and thus works. The bug can happen only when there is no CUSK.