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

[apfelmus at quantentunnel.de]

Ross Paterson wrote:
> The story so far:
> apfelmus: why are there no irrefutable patterns for GADTs?
> Conor: because you could use them to write unsafeCoerce
> Ross: how about irrefutable patterns (or newtypes) for existential types?
> Simon: Try giving the translation into System F + (existential) data types

I'd like to add that I see no problem with

   coerce :: Eq a b -> a -> b
   coerce ~Refl x = x

as long as we have

   coerce _|_ x === _|_

The wish is that

   f = \refl -> Just . coerce refl
     = \~Refl x -> Just x

should satisfy

   f _|_ x === Just _|_
   f _|_ x =/= _|_

and likewise for any other constructor than Just.

Regards,
apfelmus