Don't return empty initial uncovered set for an unsat context

Previously when the checker encountered an unsatisfiable term of type
context it would return an empty initial uncovered set. This caused all
pattern matches in the context to be reported as redudant.

This is arguably correct behaviour as they will never be reached but it
is better to recover and provide accurate warnings for these cases to
avoid error cascades. It would perhaps be better to report an error to
the user about an inacessible branch but this is certainly better than
many confusing redundant match warnings.

Reviewers: gkaracha, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3064

8 files changed, 16 insertions, 23 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 2b14739a37..720c2c96f0 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -46,7 +46,7 @@ import UniqSupply
 import DsGRHSs       (isTrueLHsExpr)
 
 import Data.List     (find)
-import Data.Maybe    (isJust)
+import Data.Maybe    (isJust, fromMaybe)
 import Control.Monad (forM, when, forM_)
 import Coercion
 import TcEvidence
@@ -1210,13 +1210,12 @@ mkInitialUncovered vars = do
   ty_cs  <- liftD getDictsDs
   tm_cs  <- map toComplex . bagToList <$> liftD getTmCsDs
   sat_ty <- tyOracle ty_cs
-  return $ case (sat_ty, tmOracle initialTmState tm_cs) of
-    (True, Just tm_state) -> [ValVec patterns (MkDelta ty_cs tm_state)]
+  let initTyCs = if sat_ty then ty_cs else emptyBag
+      initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
+      patterns  = map PmVar vars
     -- If any of the term/type constraints are non
-    -- satisfiable, the initial uncovered set is empty
-    _non_satisfiable      -> []
-  where
-    patterns  = map PmVar vars
+    -- satisfiable then return with the initialTmState. See #12957
+  return [ValVec patterns (MkDelta initTyCs initTmState)]
 
 -- | Increase the counter for elapsed algorithm iterations, check that the
 -- limit is not exceeded and call `pmcheck`
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index b9764c3b7b..527a987d7d 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -84,10 +84,6 @@ Defer01.hs:43:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In the expression: myOp 23
       In an equation for ‘j’: j = myOp 23
 
-Defer01.hs:47:1: warning: [-Woverlapping-patterns (in -Wdefault)]
-    Pattern match is redundant
-    In an equation for ‘k’: k x = ...
-
 Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘IO a0’
                   with actual type ‘Char -> IO ()’
diff --git a/testsuite/tests/pmcheck/should_compile/T12957.hs b/testsuite/tests/pmcheck/should_compile/T12957.hs
new file mode 100644
index 0000000000..d0956c6a5a
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T12957.hs
@@ -0,0 +1,5 @@
+module T12957 where
+
+data A = N | A { b :: Bool }
+f = case [] of (_:_) -> case () of
+                          a -> undefined
diff --git a/testsuite/tests/pmcheck/should_compile/T12957.stderr b/testsuite/tests/pmcheck/should_compile/T12957.stderr
new file mode 100644
index 0000000000..35a608e40d
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T12957.stderr
@@ -0,0 +1,4 @@
+
+T12957.hs:4:16: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: (_ : _) -> ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index f19e1deedf..7fc4fc5310 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -59,6 +59,7 @@ test('pmc007', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11245', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T12957', [], compile, ['-fwarn-overlapping-patterns'])
 
 # EmptyCase
 test('T10746', [], compile,
diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
deleted file mode 100644
index a27158092b..0000000000
--- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-FDsFromGivens.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
-    Pattern match is redundant
-    In an equation for ‘g1’: g1 x = ...
diff --git a/testsuite/tests/typecheck/should_fail/T10715.stderr b/testsuite/tests/typecheck/should_fail/T10715.stderr
deleted file mode 100644
index 68aa7f9689..0000000000
--- a/testsuite/tests/typecheck/should_fail/T10715.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-T10715.hs:18:1: warning: [-Woverlapping-patterns (in -Wdefault)]
-    Pattern match is redundant
-    In an equation for ‘doCoerce’: doCoerce = ...
diff --git a/testsuite/tests/typecheck/should_fail/T8392a.stderr b/testsuite/tests/typecheck/should_fail/T8392a.stderr
deleted file mode 100644
index bfc30e772e..0000000000
--- a/testsuite/tests/typecheck/should_fail/T8392a.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-T8392a.hs:11:1: warning: [-Woverlapping-patterns (in -Wdefault)]
-    Pattern match is redundant
-    In an equation for ‘foo’: foo x = ...