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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
