Fix Uncovered set of literal patterns

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.

5 files changed, 61 insertions, 5 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 0c653da2b2..1495280f94 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -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')
diff --git a/compiler/deSugar/TmOracle.hs b/compiler/deSugar/TmOracle.hs
index d6364bef52..87e5f0a268 100644
--- a/compiler/deSugar/TmOracle.hs
+++ b/compiler/deSugar/TmOracle.hs
@@ -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
index 0000000000..96bfb9faac
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15713.hs
@@ -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
index 0000000000..ceb7b4c587
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T16289.hs
@@ -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
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 393ce92463..a93a65f7f6 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -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,