apfelmus@quantentunnel.de wrote:
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 === _|_
But that makes it refutable! For the above, either coerce _|_ x === x or the notation is being abused. The trouble is that GADT pattern matching has an impact on types, as well as being a selector-destructor mechanism, and for the impact on types to be safe, the match must be strict. For existentials, I'm not sure, but it seems to me that there's not such a serious issue. Isn't the only way you can use the type which allegedly exists to project out some dictionary/other data which is packed inside the existential? Won't this projection will cause a nice safe _|_ instead of a nasty unsafe segfault? I think it's the extra power of GADTs to tell you more about type variables already in play which does the damage. All the best Conor