Heterogeneous equality

Hi! The base package contains the module Data.Type.Equality, which contains the type (:~:) for homogeneous equality. I was a bit surprised that there is no type for heterogeneous equality there. Is there such a type somewhere else in the standard library? I tried to define a type for heterogeneous equality myself as follows:

{-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}

data a :~~: b where

    HRefl :: a :~~: a

To my surprise, the kind of (:~~:) defined this way is k -> k -> *, not k -> l -> *. Why is this? Apparently, the latter, more general, kind is possible, since we can define (:~~:) :: k -> l -> * as follows:

{-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}

data (a :: k) :~~: (b :: l) where

    HRefl :: a :~~: a

All the best, Wolfgang