[Haskell-beginners] Question re "Pattern match(es) are non-exhaustive"

[Frerich Raabe]

On 2015-02-10 14:52, Brandon Allbery wrote:
> On Tue, Feb 10, 2015 at 8:18 AM, Mike Meyer <mwm at mired.org> wrote:
> 
>> ghc can't decide whether or not the tests in the guards are complete or 
>> not.
> 
> Expanding on this: that < and >= cover all cases is something that is 
> convention for Ord instances, not something absolutely guaranteed to be
> true. (In fact, they *don't* cover all cases for IEEE floating point math, 
> if either value is NaN. An SQL numeric value type would also not
> cover all cases because of the behavior of NULL. In both those cases, *both* 
> conditions would return False.) The fact that you specified a
> type for which it does happen to be true doesn't really matter, because 
> there's no way to convey a proof to the compiler that it's true for
> some types but not others. (Some argue that this and some other things are 
> signs that the Ord typeclass is poorly designed; that is a fairly
> complex discussion.)

Interesting! This got me thinking - is this issue because the compiler 
doesn't (cannot?) see the implementation of e.g. (<=)?

I noticed that a similiar case exists with

   f :: Bool -> Bool
   f x | x = True
       | not x = False

...which yields the same warning. I suppose this is because the compiler 
doesn't know the definition of 'not' so it doesn't understand that either of 
the two guards will always be True.

Is there some technical reason for this - maybe it's very time consuming 
prove that the guards are exhaustive?

-- 
Frerich Raabe - raabe at froglogic.com
www.froglogic.com - Multi-Platform GUI Testing