[GHC] #3927: Incomplete/overlapped pattern warnings + GADTs = inadequate

[GHC]

#3927: Incomplete/overlapped pattern warnings + GADTs = inadequate
---------------------------------+------------------------------------------
    Reporter:  simonpj           |        Owner:  simonpj     
        Type:  bug               |       Status:  new         
    Priority:  high              |    Milestone:  7.2.1       
   Component:  Compiler          |      Version:  6.12.1      
    Keywords:                    |     Testcase:              
   Blockedby:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Blocking:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------

Comment(by simonpj):

 Yes, this is another example of `f1` above.  And since GHC now rejects
 inacccessible case branches, you can't even put in the missing cases. Well
 you can say
 {{{
 _ `applyV` _ = undefined
 }}}
 to suppress the warning.

 I wish this was easier to fix.  The difficulty is that the type inference
 engine (which has a sophisticated constraint solver) only sees one
 equation at a time, and hence can't check exhaustiveness).  But the
 overlap checker (which sees all the equations at once) does not have a
 sophisticated solver.

 Obviously this is fixable with enough work.  But annoyingly it needs real
 work.  For example the desugarer could collect constraints, and call the
 solver to make the check.

 To be honest I keep putting this off because it doesn't seem that
 important, and there are always more important things to do.  So keep
 adding examples to this ticket if you come across them, and adding
 yourself to the cc list.  The more complaints the more likely I am to put
 off other things to do this one!

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927#comment:15>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler