Don't return empty initial uncovered set for an unsat context
authorMatthew Pickering <matthewtpickering@gmail.com>
Mon, 6 Feb 2017 01:27:41 +0000 (20:27 -0500)
committerBen Gamari <ben@smart-cactus.org>
Mon, 6 Feb 2017 01:27:42 +0000 (20:27 -0500)
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

compiler/deSugar/Check.hs
testsuite/tests/ghci/scripts/Defer02.stderr
testsuite/tests/pmcheck/should_compile/T12957.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T12957.stderr [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/all.T
testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr [deleted file]
testsuite/tests/typecheck/should_fail/T10715.stderr [deleted file]
testsuite/tests/typecheck/should_fail/T8392a.stderr [deleted file]

index 2b14739..720c2c9 100644 (file)
@@ -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`
index b9764c3..527a987 100644 (file)
@@ -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 (file)
index 0000000..d0956c6
--- /dev/null
@@ -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 (file)
index 0000000..35a608e
--- /dev/null
@@ -0,0 +1,4 @@
+
+T12957.hs:4:16: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: (_ : _) -> ...
index f19e1de..7fc4fc5 100644 (file)
@@ -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 (file)
index a271580..0000000
+++ /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 (file)
index 68aa7f9..0000000
+++ /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 (file)
index bfc30e7..0000000
+++ /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 = ...