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.

14 files changed, 26 insertions, 50 deletions

diff --git a/testsuite/tests/deSugar/should_compile/T2395.stderr b/testsuite/tests/deSugar/should_compile/T2395.stderr
index 940f263412..a2ed232e78 100644
--- a/testsuite/tests/deSugar/should_compile/T2395.stderr
+++ b/testsuite/tests/deSugar/should_compile/T2395.stderr
@@ -1,4 +1,4 @@
 
-T2395.hs:12:1: Warning:
-    Pattern match(es) are overlapped
+T2395.hs:12:1: warning:
+    Pattern match(es) are redundant
     In an equation for ‘bar’: bar _ = ...
diff --git a/testsuite/tests/deSugar/should_compile/T5117.stderr b/testsuite/tests/deSugar/should_compile/T5117.stderr
index 93de2cf9e7..954844d5f9 100644
--- a/testsuite/tests/deSugar/should_compile/T5117.stderr
+++ b/testsuite/tests/deSugar/should_compile/T5117.stderr
@@ -1,4 +1,4 @@
 
 T5117.hs:15:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f3’: f3 (MyString "a") = ...
diff --git a/testsuite/tests/deSugar/should_compile/all.T b/testsuite/tests/deSugar/should_compile/all.T
index c6b024f1b9..dbc327f237 100644
--- a/testsuite/tests/deSugar/should_compile/all.T
+++ b/testsuite/tests/deSugar/should_compile/all.T
@@ -63,7 +63,6 @@ test('ds056', normal, compile, ['-Wall -fno-warn-tabs'])
 test('ds057', normal, compile, [''])
 test('ds058', normal, compile, ['-W -fno-warn-tabs'])
 test('ds059', normal, compile, ['-W'])
-test('ds060', expect_broken(322), compile, [''])
 test('ds062', normal, compile, [''])
 test('ds063', normal, compile, [''])
 
diff --git a/testsuite/tests/deSugar/should_compile/ds002.stderr b/testsuite/tests/deSugar/should_compile/ds002.stderr
index fe4ec94873..3810c1b77b 100644
--- a/testsuite/tests/deSugar/should_compile/ds002.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds002.stderr
@@ -1,10 +1,10 @@
 
 ds002.hs:7:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f’:
         f y = ...
         f z = ...
 
 ds002.hs:11:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘g’: g x y z = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds003.stderr b/testsuite/tests/deSugar/should_compile/ds003.stderr
index 1b4c018b62..fdde26f10e 100644
--- a/testsuite/tests/deSugar/should_compile/ds003.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds003.stderr
@@ -1,6 +1,6 @@
 
 ds003.hs:5:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f’:
         f (x : x1 : x2 : x3) ~(y, ys) z = ...
         f x y True = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds019.stderr b/testsuite/tests/deSugar/should_compile/ds019.stderr
index 4d6e60f1fa..0a99306cd2 100644
--- a/testsuite/tests/deSugar/should_compile/ds019.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds019.stderr
@@ -1,6 +1,6 @@
 
 ds019.hs:5:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f’:
         f d (j, k) p = ...
         f (e, f, g) l q = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds020.stderr b/testsuite/tests/deSugar/should_compile/ds020.stderr
index 4120a957d3..8775bc6d6e 100644
--- a/testsuite/tests/deSugar/should_compile/ds020.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds020.stderr
@@ -1,18 +1,18 @@
 
 ds020.hs:8:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘a’: a ~(~[], ~[], ~[]) = ...
 
 ds020.hs:11:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘b’: b ~(~x : ~xs : ~ys) = ...
 
 ds020.hs:16:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘d’:
         d ~(n+43) = ...
         d ~(n+999) = ...
 
 ds020.hs:22:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f’: f x@(~[]) = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds022.hs b/testsuite/tests/deSugar/should_compile/ds022.hs
index 2ac429f95b..a857ef44b0 100644
--- a/testsuite/tests/deSugar/should_compile/ds022.hs
+++ b/testsuite/tests/deSugar/should_compile/ds022.hs
@@ -1,5 +1,7 @@
 -- !!! ds022 -- literal patterns (wimp version)
 --
+{-# OPTIONS_GHC -fwarn-overlapping-patterns #-}
+
 module ShouldCompile where
 
 f 1 1.1 = []
diff --git a/testsuite/tests/deSugar/should_compile/ds022.stderr b/testsuite/tests/deSugar/should_compile/ds022.stderr
index 45fe3d8a95..17b62fee02 100644
--- a/testsuite/tests/deSugar/should_compile/ds022.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds022.stderr
@@ -1,6 +1,6 @@
 
-ds022.hs:20:1: Warning:
-    Pattern match(es) are overlapped
+ds022.hs:22:1: Warning:
+    Pattern match(es) are redundant
     In an equation for ‘i’:
         i 1 0.011e2 = ...
         i 2 2.20000 = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds043.stderr b/testsuite/tests/deSugar/should_compile/ds043.stderr
index 8529a8c737..0339745bab 100644
--- a/testsuite/tests/deSugar/should_compile/ds043.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds043.stderr
@@ -1,4 +1,4 @@
 
-ds043.hs:8:2:
-    Warning: Pattern match(es) are overlapped
-	     In a case alternative: B {e = True, f = False} -> ...
+ds043.hs:8:2: warning:
+    Pattern match(es) are redundant
+    In a case alternative: B {e = True, f = False} -> ...
diff --git a/testsuite/tests/deSugar/should_compile/ds051.stderr b/testsuite/tests/deSugar/should_compile/ds051.stderr
index 76bc4d3968..4777dfcc2d 100644
--- a/testsuite/tests/deSugar/should_compile/ds051.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds051.stderr
@@ -1,12 +1,12 @@
 
 ds051.hs:6:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f1’: f1 "ab" = ...
 
 ds051.hs:11:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f2’: f2 ('a' : 'b' : []) = ...
 
 ds051.hs:16:1: Warning:
-    Pattern match(es) are overlapped
+    Pattern match(es) are redundant
     In an equation for ‘f3’: f3 "ab" = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds056.stderr b/testsuite/tests/deSugar/should_compile/ds056.stderr
index 3f44267f2a..bcea3fdb07 100644
--- a/testsuite/tests/deSugar/should_compile/ds056.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds056.stderr
@@ -1,4 +1,4 @@
 
-ds056.hs:8:1: Warning:
-    Pattern match(es) are overlapped
+ds056.hs:8:1: warning:
+    Pattern match(es) are redundant
     In an equation for ‘g’: g _ = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds058.stderr b/testsuite/tests/deSugar/should_compile/ds058.stderr
index fb504cc514..82f8141280 100644
--- a/testsuite/tests/deSugar/should_compile/ds058.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds058.stderr
@@ -1,4 +1,4 @@
 
-ds058.hs:5:7:
-    Warning: Pattern match(es) are overlapped
-	     In a case alternative: Just _ -> ...
+ds058.hs:5:7: warning:
+    Pattern match(es) are redundant
+    In a case alternative: Just _ -> ...
diff --git a/testsuite/tests/deSugar/should_compile/ds060.hs b/testsuite/tests/deSugar/should_compile/ds060.hs
deleted file mode 100644
index b822605742..0000000000
--- a/testsuite/tests/deSugar/should_compile/ds060.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-
--- Test for trac #322
-
-module ShouldCompile where
-
-instance (Num a) => Num (Maybe a) where
-    (Just a) + (Just b) = Just (a + b)
-    _ + _ = Nothing
-    (Just a) - (Just b) = Just (a - b)
-    _ - _ = Nothing
-    (Just a) * (Just b) = Just (a * b)
-    _ * _ = Nothing
-    negate (Just a) = Just (negate a)
-    negate _ = Nothing
-    abs (Just a) = Just (abs a)
-    abs _ = Nothing
-    signum (Just a) = Just (signum a)
-    signum _ = Nothing
-    fromInteger = Just . fromInteger
-
-f :: Maybe Int -> Int
-f 1 = 1
-f Nothing = 2 -- Gives bogus "Warning: Pattern match(es) are overlapped"
-f _ = 3
-