Make `singleConstructor` cope with pattern synonyms

Previously, `singleConstructor` didn't handle singleton `COMPLETE` sets
of a single pattern synonym, resulting in incomplete pattern warnings
in #15753.

This is fixed by making `singleConstructor` (now named
`singleMatchConstructor`) query `allCompleteMatches`, necessarily making
it effectful. As a result, most of this patch is concerned with
threading the side-effect through to `singleMatchConstructor`.

Unfortunately, this is not enough to completely fix the original
reproduction from #15753 and #15884, which are related to function
applications in pattern guards being translated too conservatively.

5 files changed, 143 insertions, 53 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 1495280..8496786 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -4,9 +4,13 @@ Author: George Karachalias <george.karachalias@cs.kuleuven.be>
 Pattern Matching Coverage Checking.
 -}
 
-{-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE ViewPatterns  #-}
+{-# LANGUAGE CPP            #-}
+{-# LANGUAGE GADTs          #-}
+{-# LANGUAGE DataKinds      #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TupleSections  #-}
+{-# LANGUAGE ViewPatterns   #-}
+{-# LANGUAGE MultiWayIf     #-}
 
 module Check (
         -- Checking and printing
@@ -55,7 +59,7 @@ import qualified GHC.LanguageExtensions as LangExt
 
 import Data.List     (find)
 import Data.Maybe    (catMaybes, isJust, fromMaybe)
-import Control.Monad (forM, when, forM_, zipWithM)
+import Control.Monad (forM, when, forM_, zipWithM, filterM)
 import Coercion
 import TcEvidence
 import TcSimplify    (tcNormalise)
@@ -289,6 +293,14 @@ data PmResult =
     , pmresultUncovered    :: UncoveredCandidates
     , pmresultInaccessible :: [Located [LPat GhcTc]] }
 
+instance Outputable PmResult where
+  ppr pmr = hang (text "PmResult") 2 $ vcat
+    [ text "pmresultProvenance" <+> ppr (pmresultProvenance pmr)
+    , text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
+    , text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
+    , text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
+    ]
+
 -- | Either a list of patterns that are not covered, or their type, in case we
 -- have no patterns at hand. Not having patterns at hand can arise when
 -- handling EmptyCase expressions, in two cases:
@@ -303,6 +315,10 @@ data PmResult =
 data UncoveredCandidates = UncoveredPatterns Uncovered
                          | TypeOfUncovered Type
 
+instance Outputable UncoveredCandidates where
+  ppr (UncoveredPatterns uc) = text "UnPat" <+> ppr uc
+  ppr (TypeOfUncovered ty)   = text "UnTy" <+> ppr ty
+
 -- | The empty pattern check result
 emptyPmResult :: PmResult
 emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
@@ -987,7 +1003,7 @@ translatePat fam_insts pat = case pat of
     | otherwise -> do
         ps      <- translatePat fam_insts p
         (xp,xe) <- mkPmId2Forms ty
-        let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
+        g <- mkGuard ps (mkHsWrap wrapper (unLoc xe))
         return [xp,g]
 
   -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
@@ -997,10 +1013,11 @@ translatePat fam_insts pat = case pat of
   ViewPat arg_ty lexpr lpat -> do
     ps <- translatePat fam_insts (unLoc lpat)
     -- See Note [Guards and Approximation]
-    case all cantFailPattern ps of
+    res <- allM cantFailPattern ps
+    case res of
       True  -> do
         (xp,xe) <- mkPmId2Forms arg_ty
-        let g = mkGuard ps (HsApp noExt lexpr xe)
+        g <- mkGuard ps (HsApp noExt lexpr xe)
         return [xp,g]
       False -> mkCanFailPmPat arg_ty
 
@@ -1255,41 +1272,38 @@ translateMatch _ _ = panic "translateMatch"
 translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
 translateGuards fam_insts guards = do
   all_guards <- concat <$> mapM (translateGuard fam_insts) guards
-  return (replace_unhandled all_guards)
-  -- It should have been (return all_guards) but it is too expressive.
+  let
+    shouldKeep :: Pattern -> DsM Bool
+    shouldKeep p
+      | PmVar {} <- p = pure True
+      | PmCon {} <- p = (&&)
+                          <$> singleMatchConstructor (pm_con_con p) (pm_con_arg_tys p)
+                          <*> allM shouldKeep (pm_con_args p)
+    shouldKeep (PmGrd pv e)
+      | isNotPmExprOther e = pure True  -- expensive but we want it
+      | otherwise          = allM shouldKeep pv
+    shouldKeep _other_pat  = pure False -- let the rest..
+
+  all_handled <- allM shouldKeep all_guards
+  -- It should have been @pure all_guards@ but it is too expressive.
   -- Since the term oracle does not handle all constraints we generate,
   -- we (hackily) replace all constraints the oracle cannot handle with a
-  -- single one (we need to know if there is a possibility of falure).
+  -- single one (we need to know if there is a possibility of failure).
   -- See Note [Guards and Approximation] for all guard-related approximations
   -- we implement.
-  where
-    replace_unhandled :: PatVec -> PatVec
-    replace_unhandled gv
-      | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
-      | otherwise        = gv
-
-    any_unhandled :: PatVec -> Bool
-    any_unhandled gv = any (not . shouldKeep) gv
-
-    shouldKeep :: Pattern -> Bool
-    shouldKeep p
-      | PmVar {} <- p      = True
-      | PmCon {} <- p      = singleConstructor (pm_con_con p)
-                             && all shouldKeep (pm_con_args p)
-    shouldKeep (PmGrd pv e)
-      | all shouldKeep pv  = True
-      | isNotPmExprOther e = True  -- expensive but we want it
-    shouldKeep _other_pat  = False -- let the rest..
+  if all_handled
+    then pure all_guards
+    else do
+      kept <- filterM shouldKeep all_guards
+      pure (fake_pat : kept)
 
 -- | Check whether a pattern can fail to match
-cantFailPattern :: Pattern -> Bool
-cantFailPattern p
-  | PmVar {} <- p = True
-  | PmCon {} <- p = singleConstructor (pm_con_con p)
-                    && all cantFailPattern (pm_con_args p)
-cantFailPattern (PmGrd pv _e)
-                  = all cantFailPattern pv
-cantFailPattern _ = False
+cantFailPattern :: Pattern -> DsM Bool
+cantFailPattern PmVar {}      = pure True
+cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps}
+  = (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps
+cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
+cantFailPattern _             = pure False
 
 -- | Translate a guard statement to Pattern
 translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
@@ -1312,7 +1326,8 @@ translateLet _binds = return []
 translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
 translateBind fam_insts (dL->L _ p) e = do
   ps <- translatePat fam_insts p
-  return [mkGuard ps (unLoc e)]
+  g <- mkGuard ps (unLoc e)
+  return [g]
 
 -- | Translate a boolean guard
 translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
@@ -1321,7 +1336,7 @@ translateBoolGuard e
     -- The formal thing to do would be to generate (True <- True)
     -- but it is trivial to solve so instead we give back an empty
     -- PatVec for efficiency
-  | otherwise = return [mkGuard [truePattern] (unLoc e)]
+  | otherwise = (:[]) <$> mkGuard [truePattern] (unLoc e)
 
 {- Note [Guards and Approximation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1658,13 +1673,14 @@ mkOneConFull x con = do
 -- * More smart constructors and fresh variable generation
 
 -- | Create a guard pattern
-mkGuard :: PatVec -> HsExpr GhcTc -> Pattern
-mkGuard pv e
-  | all cantFailPattern pv = PmGrd pv expr
-  | PmExprOther {} <- expr = fake_pat
-  | otherwise              = PmGrd pv expr
-  where
-    expr = hsExprToPmExpr e
+mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern
+mkGuard pv e = do
+  res <- allM cantFailPattern pv
+  let expr = hsExprToPmExpr e
+  tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
+  if | res                    -> pure (PmGrd pv expr)
+     | PmExprOther {} <- expr -> pure fake_pat
+     | otherwise              -> pure (PmGrd pv expr)
 
 -- | Create a term equality of the form: `(False ~ (x ~ lit))`
 mkNegEq :: Id -> PmLit -> ComplexEq
@@ -1738,14 +1754,37 @@ coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
            , pm_con_args = coercePatVec args }]
 coercePmPat (PmGrd {}) = [] -- drop the guards
 
--- | Check whether a data constructor is the only way to construct
--- a data type.
-singleConstructor :: ConLike -> Bool
-singleConstructor (RealDataCon dc) =
-  case tyConDataCons (dataConTyCon dc) of
-    [_] -> True
-    _   -> False
-singleConstructor _ = False
+-- | Check whether a 'ConLike' has the /single match/ property, i.e. whether
+-- it is the only possible match in the given context. See also
+-- 'allCompleteMatches' and Note [Single match constructors].
+singleMatchConstructor :: ConLike -> [Type] -> DsM Bool
+singleMatchConstructor cl tys =
+  any (isSingleton . snd) <$> allCompleteMatches cl tys
+
+{-
+Note [Single match constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When translating pattern guards for consumption by the checker, we desugar
+every pattern guard that might fail ('cantFailPattern') to 'fake_pat'
+(True <- _). Which patterns can't fail? Exactly those that only match on
+'singleMatchConstructor's.
+
+Here are a few examples:
+  * @f a | (a, b) <- foo a = 42@: Product constructors are generally
+    single match. This extends to single constructors of GADTs like 'Refl'.
+  * If @f | Id <- id () = 42@, where @pattern Id = ()@ and 'Id' is part of a
+    singleton `COMPLETE` set, then 'Id' has the single match property.
+
+In effect, we can just enumerate 'allCompleteMatches' and check if the conlike
+occurs as a singleton set.
+There's the chance that 'Id' is part of multiple `COMPLETE` sets. That's
+irrelevant; If the user specified a singleton set, it is single-match.
+
+Note that this doesn't really take into account incoming type constraints;
+It might be obvious from type context that a particular GADT constructor has
+the single-match property. We currently don't (can't) check this in the
+translation step. See #15753 for why this yields surprising results.
+-}
 
 -- | For a given conlike, finds all the sets of patterns which could
 -- be relevant to that conlike by consulting the result type.
diff --git a/testsuite/tests/pmcheck/should_compile/T15753a.hs b/testsuite/tests/pmcheck/should_compile/T15753a.hs
new file mode 100644
index 0000000..81030f9
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15753a.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+module Bug where
+
+import Data.Type.Equality
+
+data G a where
+  GInt  :: G Int
+  GBool :: G Bool
+
+ex1, ex2, ex3
+  :: a :~: Int
+  -> G a
+  -> ()
+
+ex1 Refl g
+  | GInt <- id g
+  = ()
+
+ex2 Refl g
+  | GInt <- g
+  = ()
+
+ex3 Refl g
+  = case id g of
+      GInt -> ()
+
diff --git a/testsuite/tests/pmcheck/should_compile/T15753b.hs b/testsuite/tests/pmcheck/should_compile/T15753b.hs
new file mode 100644
index 0000000..cb629c3
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15753b.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE PatternSynonyms #-}
+module Bug where
+
+{-# COMPLETE Id #-}
+pattern Id :: ()
+pattern Id = ()
+
+bug :: ()
+bug | Id <- id () = ()
+
diff --git a/testsuite/tests/pmcheck/should_compile/T15884.hs b/testsuite/tests/pmcheck/should_compile/T15884.hs
new file mode 100644
index 0000000..676aee7
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15884.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module Bug where
+
+f :: Maybe a -> Bool
+f (id->Nothing)  = False
+f (id->(Just _)) = True
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index a93a65f..e04f2cf 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -68,6 +68,12 @@ test('T15584', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15713', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15753a', expect_broken(15753), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15753b', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15884', expect_broken(15884), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T16289', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])