But that makes it refutable! For the above, either
coerce _|_ x === x
or the notation is being abused.
Making a pattern irrefutable does not mean that the function in question will become lazy: fromJust (~Just x) = x fromJust _|_ === _|_ The point with coerce is that it looks very much like being lazy in its first argument but in fact it is not.
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.
I think it's the extra power of GADTs to tell you more about type variables already in play which does the damage.
But I think that something still can be squeezed out, strictness is not absolutely necessary. I thought something along the lines of f :: Eq a b -> a -> Maybe b f ~Refl x = Just x with f _|_ x === Just _|_ The point is one can always output the constructor Just, it does not inspect the type of x. Now, I don't think anymore that this is feasible as the type of (Just x) still depends on the type of x (even if the constructor Just does not mention it). Nevertheless, I still want to remove strictness, see my next mail in this thread.
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 agree. The only practical problem I can imagine is that GHC internally treats existentials as GADTs. Regards, apfelmus