[GHC] #4139: Spurious non-exhaustive pattern match warnings are given using GADTs

[GHC]

#4139: Spurious non-exhaustive pattern match warnings are given using GADTs
-------------------------------------+-------------------------------------
        Reporter:  blarsen           |         Owner:
            Type:  bug               |        Status:  closed
        Priority:  normal            |     Milestone:
       Component:  Compiler          |       Version:  7.4.1
      Resolution:  duplicate         |      Keywords:  GADTs, warnings,
                                     |  pattern matching
Operating System:  Unknown/Multiple  |  Architecture:  Unknown/Multiple
 Type of failure:  Incorrect         |     Test Case:
  warning at compile-time            |
      Blocked By:                    |      Blocking:
 Related Tickets:  #3927             |
-------------------------------------+-------------------------------------

Comment (by George Karachalias <george.karachalias@…>):

 In [changeset:"8a506104d5b5b71d5640afc69c992e0af40f2213/ghc"
 8a506104/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="8a506104d5b5b71d5640afc69c992e0af40f2213"
 Major Overhaul of Pattern Match Checking (Fixes #595)

 This patch adresses several problems concerned with exhaustiveness and
 redundancy checking of pattern matching. The list of improvements
 includes:

 * Making the check type-aware (handles GADTs, Type Families, DataKinds,
 etc.).
   This fixes #4139, #3927, #8970 and other related tickets.

 * Making the check laziness-aware. Cases that are overlapped but affect
   evaluation are issued now with "Patterns have inaccessible right hand
 side".
   Additionally, "Patterns are overlapped" is now replaced by "Patterns are
   redundant".

 * Improved messages for literals. This addresses tickets #5724, #2204,
 etc.

 * Improved reasoning concerning cases where simple and overloaded
   patterns are matched (See #322).

 * Substantially improved reasoning for pattern guards. Addresses #3078.

 * OverloadedLists extension does not break exhaustiveness checking anymore
   (addresses #9951). Note that in general this cannot be handled but if we
 know
   that an argument has type '[a]', we treat it as a list since, the
 instance of
   'IsList' gives the identity for both 'fromList' and 'toList'. If the
 type is
   not clear or is not the list type, then the check cannot do much still.
 I am
   a bit concerned about OverlappingInstances though, since one may
 override the
   '[a]' instance with e.g. an '[Int]' instance that is not the identity.

 * Improved reasoning for nested pattern matching (partial solution). Now
 we
   propagate type and (some) term constraints deeper when checking, so we
 can
   detect more inconsistencies. For example, this is needed for #4139.

 I am still not satisfied with several things but I would like to address
 at
 least the following before the next release:
     Term constraints are too many and not printed for non-exhaustive
 matches
 (with the exception of literals). This sometimes results in two identical
 (in
 appearance) uncovered warnings. Unless we actually show their difference,
 I
 would like to have a single warning.
 }}}

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