Heterogeneous equality into base?

Wolfgang Jeltsch wolfgang-it at jeltsch.info
Thu Jul 6 20:45:32 UTC 2017


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

> {-# 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,

More information about the Libraries mailing list