Fix #13363wip/T13363

The pattern match checker doesn't handle pattern synonyms (yet); it
just regards them as additional data constructors. But that's wrong
from the perspective of redudancy checking: A match on a pattern synonym
will always lead to an overlap warning, because the mismatch case in
`ConCon` will always return `NotCovered`, which is unsound.

The proper conservative approximation is to return `Covered` whenever we
mismatched against a pattern synonym.

4 files changed, 45 insertions, 9 deletions

diff --git a/compiler/basicTypes/ConLike.hs b/compiler/basicTypes/ConLike.hs
index a9d7548b8a..9d3ae5798f 100644
--- a/compiler/basicTypes/ConLike.hs
+++ b/compiler/basicTypes/ConLike.hs
@@ -9,6 +9,8 @@
 
 module ConLike (
           ConLike(..)
+        , isRealDataCon
+        , isPatSynCon
         , conLikeArity
         , conLikeFieldLabels
         , conLikeInstOrigArgTys
@@ -53,6 +55,14 @@ import qualified Data.Data as Data
 data ConLike = RealDataCon DataCon
              | PatSynCon PatSyn
 
+isRealDataCon :: ConLike -> Bool
+isRealDataCon RealDataCon{} = True
+isRealDataCon _             = False
+
+isPatSynCon :: ConLike -> Bool
+isPatSynCon PatSynCon{} = True
+isPatSynCon _           = False
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 0c653da2b2..f70ca714e4 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -2032,7 +2032,7 @@ pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
           (va@(PmCon { pm_con_con = c2, pm_con_tvs = ex_tvs2
                      , pm_con_args = args2})) (ValVec vva delta)
   | c1 /= c2  =
-    return (usimple [ValVec (va:vva) delta])
+    return (coverIf (isPatSynCon c1) (usimple [ValVec (va:vva) delta]))
   | otherwise = do
     let to_evvar tv1 tv2 = nameType "pmConCon" $
                            mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
@@ -2071,13 +2071,13 @@ pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
     mb_sat <- pmIsSatisfiable delta tm_ct ty_cs strict_arg_tys
     pure $ fmap (ValVec (va:vva)) mb_sat
 
-  set_provenance prov .
-    force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
+  setProvenance prov .
+    forceIf (canDiverge (idName x) (delta_tm_cs delta)) <$>
       runMany (pmcheckI (p:ps) guards) inst_vsa
 
 -- LitVar
 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
-  = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
+  = forceIf (canDiverge (idName x) (delta_tm_cs delta)) <$>
       mkUnion non_matched <$>
         case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
           Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
@@ -2313,12 +2313,17 @@ forces :: PartialResult -> PartialResult
 forces pres = pres { presultDivergent = Diverged }
 
 -- | Set the divergent set to non-empty if the flag is `True`
-force_if :: Bool -> PartialResult -> PartialResult
-force_if True  pres = forces pres
-force_if False pres = pres
+forceIf :: Bool -> PartialResult -> PartialResult
+forceIf True  pres = forces pres
+forceIf False pres = pres
 
-set_provenance :: Provenance -> PartialResult -> PartialResult
-set_provenance prov pr = pr { presultProvenance = prov }
+-- | Set the covered set to non-empty if the flag is `True`
+coverIf :: Bool -> PartialResult -> PartialResult
+coverIf True  pres = pres { presultCovered = Covered }
+coverIf False pres = pres
+
+setProvenance :: Provenance -> PartialResult -> PartialResult
+setProvenance prov pr = pr { presultProvenance = prov }
 
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
diff --git a/testsuite/tests/pmcheck/should_compile/T13363.hs b/testsuite/tests/pmcheck/should_compile/T13363.hs
new file mode 100644
index 0000000000..bfe5247de2
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T13363.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+module Bug where
+
+data Boolean = F | T
+  deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue <- ((== T) -> True)
+  where
+    TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F               = 0
+catchAll TooGoodToBeTrue = 1
+catchAll _               = error "impossible"
+
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 393ce92463..6e1e849015 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -52,6 +52,8 @@ test('T11195', collect_compiler_stats('bytes allocated',10), compile,
 
 test('T11984', normal, compile,
     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T13363', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14098', normal, compile,