Proposal: Add portable eliminator for Data.Type.Equality

[wren romano]

On Mon, Nov 14, 2016 at 12:21 PM, David Feuer <david.feuer at gmail.com> wrote:
> I propose that we add the eliminator subst as a function:
>
> subst :: a :~: b -> f a -> f b
> subst Refl x = x

I'm all for adding this function, but do note that the type is
suboptimal since GHC lacks general functions (and higher-order pattern
matching) at the type level. Which means we'll actually end up wanting
a family of different "subst" functions to cover all the (relevant)
cases the definition above would cover in a language like Agda, Coq,
etc.

E.g.,

    Prelude> let x :: Either Bool Int; x = Right 42

    Prelude> :t (`subst` x)
    (`subst` x) :: Int :~: b -> Either Bool b

When I might've really wanted/meant (Bool :~: b -> Either b Int)

-- 
Live well,
~wren