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

[Conor McBride]

apfelmus at 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