Proposal: Add portable eliminator for Data.Type.Equality

wren romano winterkoninkje at
Tue Nov 15 05:24:42 UTC 2016

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


    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,

More information about the Libraries mailing list