Fix Uncovered set of literal patterns
authorSebastian Graf <sebastian.graf@kit.edu>
Mon, 1 Apr 2019 17:59:45 +0000 (19:59 +0200)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Wed, 3 Apr 2019 08:03:47 +0000 (04:03 -0400)
Issues #16289 and #15713 are proof that the pattern match checker did
an unsound job of estimating the value set abstraction corresponding to
the uncovered set.

The reason is that the fix from #11303 introducing `NLit` was
incomplete: The `LitCon` case desugared to `Var` rather than `LitVar`,
which would have done the necessary case splitting analogous to the
`ConVar` case.

This patch rectifies that by introducing the fresh unification variable
in `LitCon` in value abstraction position rather than pattern postition,
recording a constraint equating it to the constructor expression rather
than the literal. Fixes #16289 and #15713.

compiler/deSugar/Check.hs
compiler/deSugar/TmOracle.hs
testsuite/tests/pmcheck/should_compile/T15713.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/T16289.hs [new file with mode: 0644]
testsuite/tests/pmcheck/should_compile/all.T

index 0c653da..1495280 100644 (file)
@@ -2118,15 +2118,22 @@ pmcheckHd (p@(PmLit l)) ps guards
 -- no information is lost
 
 -- LitCon
-pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
+pmcheckHd p@PmLit{} ps guards va@PmCon{} (ValVec vva delta)
   = do y <- liftD $ mkPmId (pmPatType va)
-       let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
+       -- Analogous to the ConVar case, we have to case split the value
+       -- abstraction on possible literals. We do so by introducing a fresh
+       -- variable that is equated to the constructor. LitVar will then take
+       -- care of the case split by resorting to NLit.
+       let tm_state = extendSubst y (vaToPmExpr va) (delta_tm_cs delta)
            delta'   = delta { delta_tm_cs = tm_state }
-       pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
+       pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
 
 -- ConLit
-pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
+pmcheckHd p@PmCon{} ps guards (PmLit l) (ValVec vva delta)
   = do y <- liftD $ mkPmId (pmPatType p)
+       -- This desugars to the ConVar case by introducing a fresh variable that
+       -- is equated to the literal via a constraint. ConVar will then properly
+       -- case split on all possible constructors.
        let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
            delta'   = delta { delta_tm_cs = tm_state }
        pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
index d6364be..87e5f0a 100644 (file)
@@ -33,6 +33,7 @@ import HsLit
 import TcHsSyn
 import MonadUtils
 import Util
+import Outputable
 
 import NameEnv
 
@@ -134,7 +135,8 @@ solveComplexEq solver_state@(standby, (unhandled, env)) eq@(e1, e2) = case eq of
 
   (PmExprEq _ _, PmExprEq _ _) -> Just (eq:standby, (unhandled, env))
 
-  _ -> Just (standby, (True, env)) -- I HATE CATCH-ALLS
+  _ -> WARN( True, text "solveComplexEq: Catch all" <+> ppr eq )
+       Just (standby, (True, env)) -- I HATE CATCH-ALLS
 
 -- | Extend the substitution and solve the (possibly updated) constraints.
 extendSubstAndSolve :: Name -> PmExpr -> TmState -> Maybe TmState
diff --git a/testsuite/tests/pmcheck/should_compile/T15713.hs b/testsuite/tests/pmcheck/should_compile/T15713.hs
new file mode 100644 (file)
index 0000000..96bfb9f
--- /dev/null
@@ -0,0 +1,17 @@
+{-# LANGUAGE OverloadedStrings, LambdaCase #-}
+
+module T15713 where
+
+import Data.String
+
+data Expr = App Expr Expr | Var String
+  deriving (Eq)
+
+instance IsString Expr where
+  fromString = Var . fromString
+
+go = \case
+  App ( App ( App "refWithFile" identM ) filenameM) exceptionMayM -> Just 2
+  App ( App "and" a ) b -> Just 3
+  App ( App "or" a ) b -> Just 4
+  _ -> Nothing
diff --git a/testsuite/tests/pmcheck/should_compile/T16289.hs b/testsuite/tests/pmcheck/should_compile/T16289.hs
new file mode 100644 (file)
index 0000000..ceb7b4c
--- /dev/null
@@ -0,0 +1,26 @@
+module Lib where
+
+data Value = Finite Integer | Infinity
+  deriving (Eq)
+
+instance Num Value where
+  (+)         = undefined
+  (*)         = undefined
+  abs         = undefined
+  signum      = undefined
+  negate      = undefined
+  fromInteger = Finite
+
+-- | @litCon _@ should not elicit an overlapping patterns warning when it
+-- passes through the LitCon case.
+litCon :: Value -> Bool
+litCon Infinity = True
+litCon 0        = True
+litCon _        = False
+
+-- | @conLit Infinity@ should not elicit an overlapping patterns warning when
+-- it passes through the ConLit case.
+conLit :: Value -> Bool
+conLit 0        = True
+conLit Infinity = True
+conLit _        = False
index 393ce92..a93a65f 100644 (file)
@@ -66,6 +66,10 @@ test('T15450', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15584', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15713', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T16289', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,