Heterogeneous equality into base?

[Wolfgang Jeltsch]

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