As you know type-level foralls don't float, so we may want to write HRefl's kind

-- Different from
--   HREFL :: forall k1 k2. k1 -> k2 -> Type
-- 
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
  HREFL :: HREFL a a

Let us capture forall k2. k2 -> .. with a kind synonym

type HRank2 ty = forall k2. k2 -> ty

data HREFL :: forall k. k -> HRank2 Type where
  HREFL :: HREFL a a

Works fine. Phew. Let's do the same for forall k1. k1 -> ..

type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty

data HREFL :: HRank1 (HRank2 Type) where
  HREFL :: HREFL a a 

Works fine. Phew.

“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!

data HREFL :: HRank1 (HRank1 Type) -- FAILS
data HREFL :: HRank1 (HRank2 Type) -- OK
data HREFL :: HRank2 (HRank1 Type) -- OK 
data HREFL :: HRank2 (HRank2 Type) -- FAILS

$ ghci -ignore-dot-ghci /tmp/Weird.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/Weird.hs, interpreted )

/tmp/Weird.hs:8:1: error:
    • These kind and type variables: (b :: k2) k2 (d :: k2)
      are out of dependency order. Perhaps try this ordering:
        k2 (b :: k2) (d :: k2)
    • In the data type declaration for ‘HREFL’
  |
8 | data HREFL :: HRank2 (HRank2 Type) 
  | ^^^^^^^^^^
Failed, 0 modules loaded.
Prelude> 

Same happens defining HRank2 in terms of HRank1

type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = HRank1 ty