Definition of heterogeneous equality rejected unless using a SAKS

The following definitions of heterogeneous equality are rejected on HEAD:

data (a :: k1) :~: (b :: k2) where
   HRefl :: a :~~: a

error:
    * Different names for the same type variable: `k1' and `k2'
    * In the data declaration for `:~~:'
  |
  | data (a :: k1) :~~: (b :: k2) where
  |       ^^^^^^^^^^^^^^^^^^^^^^

data (:~~:) :: k1 -> k2 -> Type where
   HRefl :: a :~~: a

error:
    * Different names for the same type variable: `k1' and `k2'
    * In the data declaration for `:~~:'
  |
  | data (:~~:) :: k1 -> k2 -> Type where
  |                ^^^^^^^^

Note that this remains true even if one enables -XCUSKs, so this doesn't fit the diagnostic of #20752 (comment 394357).

The only way to get this accepted is to write a standalone kind signature:

type (:~~:) :: k1 -> k2 -> Type
data a :~~: b where
   HRefl :: a :~~: a

It seems to me that the "different names for the same type variable" check is overly-eager for GADTs. In particular, the following is also rejected:

data (:~~:) :: k1 -> k2 -> Type where
  NotHRefl :: forall k1 k2 (a :: k1) (b :: k2). a :~~: b
  HRefl :: a :~~: a

error:
    * Different names for the same type variable: `k1' and `k2'
    * In the data declaration for `:~~:'
  |
  | data (:~~:) :: k1 -> k2 -> Type where
  |                ^^^^^^^^

I don't know how GHC concludes that k1 and k2 must refer to the same kind variable there.