[Haskell-cafe] Re: irrefutable patterns for existential types / GADTs

[Jim Apple]

On 9/30/06, apfelmus at quantentunnel.de <apfelmus at quantentunnel.de> wrote:
>   data Eq a b where Refl :: Eq a a
>
>   coerce :: Eq a b -> a -> b
>   coerce ~Refl x = x

But this works well with Leibniz-style equality (
http://homepage.mac.com/pasalic/p2/papers/thesis.pdf ), because the
Equality proof/term is actually used:

data Equal a b = Equal (forall f . f a -> f b)
newtype Id x = Id { unId :: x}
coerce :: Equal a b -> a -> b
coerce ~(Equal f) x = unId (f (Id x))

Jim