Proposal: Add portable eliminator for Data.Type.Equality

[David Feuer]

Further support for my proposal: we already have the analogous partial version

Data.Typeable.gcast :: forall a b c. (Typeable a, Typeable b) => c a
-> Maybe (c b)

On Mon, Nov 14, 2016 at 3:21 PM, David Feuer <david.feuer at gmail.com> wrote:
> 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