Heterogeneous equality into base?

[David Menendez]

Do you have any code examples that use heterogeneous equality? In the
past, GHC has been less flexible with kind variables than with type
variables, so I’m not sure what this would enable.

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



-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>