That seems generally reasonable to me. It'll need the usual discussion
process here and then it can be added to `base`. However, I think it
should not be added to `Data.Type.Equality`, but rather to a new
module, perhaps `Data.Type.Equality.Heterogeneous`. That module will
then be able to offer the full complement of basic functions (sym,
trans, ...) without stepping on the pre-existing names. I imagine
you'll also want one or two extra casting operations, and conversions
between `:~:` and `:~~:`. Also, you have called the constructor of
this type HRefl in the past, which strikes me as better than Refl.

David

On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
<wolfgang-it@jeltsch.info> wrote:
> 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
> _______________________________________________
> Libraries mailing list
> Libraries@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries