Check for exhaustive patterns is broken

[nobody]

When some of the patterns in a function definition or
case expression contain guards, the compiler gives
false warnings about non-exhaustive pattern matches.  A
pity, because this kind of warning is very useful
indeed!

For example, I get 
 >ghc --make -Wall See.hs
 ghc-5.02.1: chasing modules from: See.hs
 Compiling See              ( See.hs, ./See.o )

 See.hs:17: Warning: Pattern match(es) are
non-exhaustive
     In the definition of `insert':
 	Patterns not matched: _ _ (TREE _ _ _ _)

 See.hs:41: Warning: Pattern match(es) are
non-exhaustive
    In a case alternative EMPTY: Patterns not matched:
TREE _ _ _ _

for the attached file.

[I am not sure filling in the e-mail address box had
any effect on the last two complaints I submitted, so I
repeat my address here:
feliks@crt.se]

[sewardj]

Logged In: YES 
user_id=50143


Code is:

insert k v EMPTY = Just (TREE k v EMPTY EMPTY) 


insert k v (TREE k' v' left right) 

| k < k' = case insert k v left of 
Nothing -> Nothing 
Just left' -> Just (TREE k' v' 
left' right) 

| k > k' = case insert k v right of 
Nothing -> Nothing 
Just right' -> Just (TREE k' v' 
left right') 

| k == k' = Nothing 

[simonmar]

See also #1307

[simonmar]

See #595

[ganesh]

This is an unsolvable issue. Consider this simplified example:

foo x | x == 0 = 0
      | x /= 0 = 0

For "correct" Eq implementations these patterns are indeed exhaustive. But (a) GHC has no evidence that all Eq implementations are "correct", and (b) in general it would be undecidable to check whether arbitrary guards are exhaustive or not.

[ganesh]

Closing this with the approval of the GHC team ( http://www.haskell.org/pipermail/glasgow-haskell-users/2009-November/018017.html)