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