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

On 9/30/06, apfelmus@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