[Haskell-cafe] Bug in GADT Implementation?

[Dominic Steinitz]

Roberto Zunino wrote:
> Dominic Steinitz wrote:
>> I would expect
>>
>> foo r@(Range BITSTRING _ _) x = []
>>
>> to give an error but it doesn't. Writing
>>
>> t = Range BITSTRING
>>
>> gives one so why not the pattern match?
> 
> AFAICS, this is because when you construct a value, as in t, you have to
> provide the required context (Ord in this case) or face an error. OTOH,
> when you destruct a value, you simply get the context back and you are
> not required to provide anything, so no type error is generated.
> 
> This works in HEAD:
> 
> data A
> data Foo where F :: Num A => Foo
> 
> bar :: Foo -> A
> bar F = 42
> 
> Regards,
> Zun.
> 
> 
Zun,

This seems even worse to me. A is not inhabited so how can 42 be of type A?

BTW this doesn't compile in 6.6.

I suppose I could read my example as "if there is anything that matches
Range BITSTRING _ _ then do the following" and since nothing can ever
match it then it's a redundant case. But I would expect the compiler to
at least warn me that nothing can ever match this.

Dom.