Proposal: Add portable eliminator for Data.Type.Equality

David Feuer david.feuer at
Mon Nov 14 20:21:54 UTC 2016

Most of Data.Type.Equality can be supported by any Haskell
implementation with Rank2Types and TypeOperators, using, for example,
the well-known definition

newtype a :~: b = Equality { subst :: forall f . f a -> f b }

(The parts that can't be supported so are the gcastWith function, the
~~ constraint, and the == type family.)

What's most prominently missing is the ability to *use* equality for
anything beyond castWith without leaning on GHC's equality

I propose that we add the eliminator subst as a function:

subst :: a :~: b -> f a -> f b
subst Refl x = x

Note that we already have an introduction rule :: a :~: a

David Feuer

More information about the Libraries mailing list