Heterogeneous equality into base?

Hi! The module Data.Type.Equality in the base package contains the type (:~:) for homogeneous equality. However, a type for heterogeneous equality would be very useful as well. I would define such a type as follows:

{-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}   data (a :: k) :~~: (b :: l) where       Refl :: a :~~: a

Is there already such a type in the base package? If not, does it make sense to file a feature request (or would such a proposal be likely to not being accepted for some reason)? All the best, Wolfgang