Proposal: Add portable eliminator for Data.Type.Equality

[David Feuer]

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
constraints.

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

Control.Category.id :: a :~: a

David Feuer