[Haskell-cafe] Re: Bug in GADT Implementation?

[Simon Peyton-Jones]

| > 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.
|
| Why is there nothing that can match 'Range BITSTRING _ _'?
|
| Some other module may define an instance 'Ord BitString'.

Arie's right -- that's the reason.

In general, rejecting code because it can't possibly be executed is nice when GHC can be absolutely definitely sure that it can't be executed.  But if there's any doubt at all, it has to accept the program. After all, if the function can't be called, there's no harm to soundness.  But if it's certain that the code is dead, its better to report it sooner.

Simon