Check EmptyCase by simply adding a non-void constraintwip/pmcheck-case-strict

We can handle non-void constraints since !1733, so we can now express
the strictness of `-XEmptyCase` just by adding a non-void constraint
to the initial Uncovered set.

For `case x of {}` we thus check that the Uncovered set `{ x | x /~ ⊥ }`
is non-empty. This is conceptually simpler than the plan outlined in
 #17376, because it talks to the oracle directly.

In order for this patch to pass the testsuite, I had to fix handling of
newtypes in the pattern-match checker (#17248).

Since we use a different code path (well, the main code path) for
`-XEmptyCase` now, we apparently also handle #13717 correctly.
There's also some dead code that we can get rid off now.

`provideEvidence` has been updated to provide output more in line with
the old logic, which used `inhabitationCandidates` under the hood.

A consequence of the shift away from the `UncoveredPatterns` type is
that we don't report reduced type families for empty case matches,
because the pretty printer is pure and only knows the match variable's
type.

Fixes #13717, #17248, #17386

30 files changed, 468 insertions, 334 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index 637a8fd7e9..c712055d70 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -42,6 +42,7 @@ import SrcLoc
 import Util
 import Outputable
 import DataCon
+import TyCon
 import Var (EvVar)
 import Coercion
 import TcEvidence
@@ -236,7 +237,7 @@ instance Monoid PartialResult where
 data PmResult =
   PmResult {
       pmresultRedundant    :: [Located [LPat GhcTc]]
-    , pmresultUncovered    :: UncoveredCandidates
+    , pmresultUncovered    :: [Delta]
     , pmresultInaccessible :: [Located [LPat GhcTc]]
     , pmresultApproximate  :: Precision }
 
@@ -248,24 +249,6 @@ instance Outputable PmResult where
     , text "pmresultApproximate" <+> ppr (pmresultApproximate 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:
---
--- * The type of the scrutinee is a trivially inhabited type (like Int or Char)
--- * The type of the scrutinee cannot be reduced to WHNF.
---
--- In both these cases we have no inhabitation candidates for the type at hand,
--- but we don't want to issue just a wildcard as missing. Instead, we print a
--- type annotated wildcard, so that the user knows what kind of patterns is
--- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
-data UncoveredCandidates = UncoveredPatterns [Id] [Delta]
-                         | TypeOfUncovered Type
-
-instance Outputable UncoveredCandidates where
-  ppr (UncoveredPatterns vva deltas) = text "UnPat" <+> ppr vva $$ ppr deltas
-  ppr (TypeOfUncovered ty)   = text "UnTy" <+> ppr ty
-
 {-
 %************************************************************************
 %*                                                                      *
@@ -279,7 +262,7 @@ checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
   tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
   res <- checkSingle' locn var p
-  dsPmWarn dflags ctxt res
+  dsPmWarn dflags ctxt [var] res
 
 -- | Check a single pattern binding (let)
 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
@@ -291,11 +274,14 @@ checkSingle' locn var p = do
   PartialResult cs us ds pc <- pmCheck grds [] 1 missing
   dflags <- getDynFlags
   us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us
-  let uc = UncoveredPatterns [var] us'
+  let plain = PmResult { pmresultRedundant    = []
+                       , pmresultUncovered    = us'
+                       , pmresultInaccessible = []
+                       , pmresultApproximate  = pc }
   return $ case (cs,ds) of
-    (Covered,  _    )         -> PmResult [] uc [] pc -- useful
-    (NotCovered, NotDiverged) -> PmResult m  uc [] pc -- redundant
-    (NotCovered, Diverged )   -> PmResult [] uc m  pc -- inaccessible rhs
+    (Covered   , _          ) -> plain                              -- useful
+    (NotCovered, NotDiverged) -> plain { pmresultRedundant = m    } -- redundant
+    (NotCovered, Diverged   ) -> plain { pmresultInaccessible = m } -- inaccessible rhs
   where m = [cL locn [cL locn p]]
 
 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -324,30 +310,26 @@ checkMatches dflags ctxt vars matches = do
                                , text "Matches:"])
                                2
                                (vcat (map ppr matches)))
-  res <- case matches of
-    -- Check EmptyCase separately
-    -- See Note [Checking EmptyCase Expressions] in GHC.HsToCore.PmCheck.Oracle
-    [] | [var] <- vars -> checkEmptyCase' var
-    _normal_match      -> checkMatches' vars matches
-  dsPmWarn dflags ctxt res
-
--- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
--- list of matches. For empty case expressions, use checkEmptyCase' instead.
+  res <- checkMatches' vars matches
+  dsPmWarn dflags ctxt vars res
+
+-- | Check a matchgroup (case, functions, etc.).
 checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
-checkMatches' vars matches
-  | null matches = panic "checkMatches': EmptyCase"
-  | otherwise = do
-      missing    <- getPmDelta
-      tracePm "checkMatches': missing" (ppr missing)
-      (rs,us,ds,pc) <- go matches [missing]
-      dflags <- getDynFlags
-      us' <- getNFirstUncovered vars (maxUncoveredPatterns dflags + 1) us
-      let up = UncoveredPatterns vars us'
-      return $ PmResult {
-                   pmresultRedundant    = map hsLMatchToLPats rs
-                 , pmresultUncovered    = up
-                 , pmresultInaccessible = map hsLMatchToLPats ds
-                 , pmresultApproximate  = pc }
+checkMatches' vars matches = do
+  init_delta <- getPmDelta
+  missing <- case matches of
+    -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
+    [] | [var] <- vars -> maybeToList <$> addTmCt init_delta (TmVarNonVoid var)
+    _                  -> pure [init_delta]
+  tracePm "checkMatches': missing" (ppr missing)
+  (rs,us,ds,pc) <- go matches missing
+  dflags <- getDynFlags
+  us' <- getNFirstUncovered vars (maxUncoveredPatterns dflags + 1) us
+  return $ PmResult {
+                pmresultRedundant    = map hsLMatchToLPats rs
+              , pmresultUncovered    = us'
+              , pmresultInaccessible = map hsLMatchToLPats ds
+              , pmresultApproximate  = pc }
   where
     go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
        -> DsM ( [LMatch GhcTc (LHsExpr GhcTc)]
@@ -381,28 +363,32 @@ checkMatches' vars matches
     hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
     hsLMatchToLPats _                                   = panic "checkMatches'"
 
--- | Check an empty case expression. Since there are no clauses to process, we
---   only compute the uncovered set. See Note [Checking EmptyCase Expressions]
---   in "GHC.HsToCore.PmCheck.Oracle" for details.
-checkEmptyCase' :: Id -> DsM PmResult
-checkEmptyCase' x = do
-  delta         <- getPmDelta
-  us <- inhabitants delta (idType x) >>= \case
-    -- Inhabitation checking failed / the type is trivially inhabited
-    Left ty            -> pure (TypeOfUncovered ty)
-    -- A list of oracle states for the different satisfiable constructors is
-    -- available. Turn this into a value set abstraction.
-    Right (va, deltas) -> pure (UncoveredPatterns [va] deltas)
-  pure (PmResult [] us [] Precise)
-
 getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta]
 getNFirstUncovered _    0 _              = pure []
 getNFirstUncovered _    _ []             = pure []
 getNFirstUncovered vars n (delta:deltas) = do
-  front <- provideEvidenceForEquation vars n delta
+  front <- provideEvidence vars n delta
   back <- getNFirstUncovered vars (n - length front) deltas
   pure (front ++ back)
 
+{- Note [Checking EmptyCase]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-XEmptyCase is useful for matching on empty data types like 'Void'. For example,
+the following is a complete match:
+
+    f :: Void -> ()
+    f x = case x of {}
+
+Really, -XEmptyCase is the only way to write a program that at the same time is
+safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning
+(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an
+exception into divergence (@f x = f x@).
+
+Semantically, unlike every other case expression, -XEmptyCase is strict in its
+match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the
+initial Delta and check if there are any values left to match on.
+-}
+
 {-
 %************************************************************************
 %*                                                                      *
@@ -514,7 +500,7 @@ translatePat fam_insts x pat = case pat of
     translateListPat fam_insts x ps
 
   -- overloaded list
-  ListPat (ListPatTc _elem_ty (Just (pat_ty, to_list))) pats -> do
+  ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do
     dflags <- getDynFlags
     case splitListTyConApp_maybe pat_ty of
       Just _e_ty
@@ -522,7 +508,7 @@ translatePat fam_insts x pat = case pat of
         -- Just translate it as a regular ListPat
         -> translateListPat fam_insts x pats
       _ -> do
-        y <- selectMatchVar pat
+        y <- mkPmId (mkListTy elem_ty)
         grds <- translateListPat fam_insts y pats
         rhs_y <- dsSyntaxExpr to_list [Var x]
         pure $ PmLet y rhs_y : grds
@@ -1075,7 +1061,8 @@ pmCheck' (p : ps) guards n delta
   pr_pos <- pmCheckM ps guards n (addPmConCts delta x con dicts args)
 
   -- The var is forced regardless of whether @con@ was satisfiable
-  let pr_pos' = forceIfCanDiverge delta x pr_pos
+  -- See Note [Divergence of Newtype matches]
+  let pr_pos' = addConMatchStrictness delta x con pr_pos
 
   -- Stuff for <next equation>
   pr_neg <- addRefutableAltCon delta x con >>= \case
@@ -1120,6 +1107,13 @@ forceIfCanDiverge delta x
   | canDiverge delta x = forces
   | otherwise          = id
 
+-- | 'forceIfCanDiverge' if the 'PmAltCon' was not a Newtype.
+-- See Note [Divergence of Newtype matches].
+addConMatchStrictness :: Delta -> Id -> PmAltCon -> PartialResult -> PartialResult
+addConMatchStrictness _     _ (PmAltConLike (RealDataCon dc)) res
+  | isNewTyCon (dataConTyCon dc) = res
+addConMatchStrictness delta x _ res = forceIfCanDiverge delta x res
+
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
 
@@ -1242,14 +1236,12 @@ needToRunPmCheck dflags origin
   = notNull (filter (`wopt` dflags) allPmCheckWarnings)
 
 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
-dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
-dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
+dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM ()
+dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result
   = when (flag_i || flag_u) $ do
       let exists_r = flag_i && notNull redundant
           exists_i = flag_i && notNull inaccessible && not is_rec_upd
-          exists_u = flag_u && (case uncovered of
-                                  TypeOfUncovered   _     -> True
-                                  UncoveredPatterns _ unc -> notNull unc)
+          exists_u = flag_u && notNull uncovered
           approx   = precision == Approximate
 
       when (approx && (exists_u || exists_i)) $
@@ -1262,9 +1254,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
         putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
                                (pprEqn q "has inaccessible right hand side"))
       when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
-        case uncovered of
-          TypeOfUncovered ty    -> warnEmptyCase ty
-          UncoveredPatterns vars unc -> pprEqns vars unc
+        pprEqns vars uncovered
   where
     PmResult
       { pmresultRedundant = redundant
@@ -1293,11 +1283,6 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
                  in  hang (text "Patterns not matched:") 4
                        (vcat (take maxPatterns us) $$ dots maxPatterns us)
 
-    -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
-    -- which we only know the type and have no inhabitants at hand)
-    warnEmptyCase ty = pprContext False ctx (text "are non-exhaustive") $ \_ ->
-      hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
-
     approx_msg = vcat
       [ hang
           (text "Pattern match checker ran into -fmax-pmcheck-models="
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index ac21ebf589..1b5c5b24c8 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -8,20 +8,20 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
 
 -- | The pattern match oracle. The main export of the module are the functions
 -- 'addTmCt', 'addVarCoreCt', 'addRefutableAltCon' and 'addTypeEvidence' for
--- adding facts to the oracle, and 'provideEvidenceForEquation' to turn a
+-- adding facts to the oracle, and 'provideEvidence' to turn a
 -- 'Delta' into a concrete evidence for an equation.
 module GHC.HsToCore.PmCheck.Oracle (
 
         DsM, tracePm, mkPmId,
-        Delta, initDelta, canDiverge, lookupRefuts, lookupSolution,
+        Delta, initDelta, lookupRefuts, lookupSolution,
 
         TmCt(..),
-        inhabitants,
         addTypeEvidence,    -- Add type equalities
         addRefutableAltCon, -- Add a negative term equality
         addTmCt,            -- Add a positive term equality x ~ e
         addVarCoreCt,       -- Add a positive term equality x ~ core_expr
-        provideEvidenceForEquation,
+        canDiverge,         -- Try to add the term equality x ~ ⊥
+        provideEvidence,
     ) where
 
 #include "HsVersions.h"
@@ -35,6 +35,7 @@ import Outputable
 import ErrUtils
 import Util
 import Bag
+import UniqSet
 import UniqDSet
 import Unique
 import Id
@@ -75,9 +76,10 @@ import Control.Monad (guard, mzero)
 import Control.Monad.Trans.Class (lift)
 import Control.Monad.Trans.State.Strict
 import Data.Bifunctor (second)
-import Data.Foldable (foldlM)
+import Data.Foldable (foldlM, minimumBy)
 import Data.List     (find)
 import qualified Data.List.NonEmpty as NonEmpty
+import Data.Ord      (comparing)
 import qualified Data.Semigroup as Semigroup
 import Data.Tuple    (swap)
 
@@ -101,32 +103,10 @@ mkPmId ty = getUniqueM >>= \unique ->
 -- * Caching possible matches of a COMPLETE set
 
 markMatched :: ConLike -> PossibleMatches -> PossibleMatches
-markMatched con (PM tc ms) = PM tc (fmap (`delOneFromUniqDSet` con) ms)
-markMatched _   NoPM = NoPM
-
--- | Satisfiability decisions as a data type. The @proof@ can carry a witness
--- for satisfiability and might even be instantiated to 'Data.Void.Void' to
--- degenerate into a semi-decision predicate.
-data Satisfiability proof
-  = Unsatisfiable
-  | PossiblySatisfiable
-  | Satisfiable !proof
-
-maybeSatisfiable :: Maybe a -> Satisfiability a
-maybeSatisfiable (Just a) = Satisfiable a
-maybeSatisfiable Nothing  = Unsatisfiable
-
--- | Tries to return one of the possible 'ConLike's from one of the COMPLETE
--- sets. If the 'PossibleMatches' was inhabited before (cf. 'ensureInhabited')
--- this 'ConLike' is evidence for that assurance.
-getUnmatchedConstructor :: PossibleMatches -> Satisfiability ConLike
-getUnmatchedConstructor NoPM = PossiblySatisfiable
-getUnmatchedConstructor (PM _tc ms)
-  = maybeSatisfiable $ NonEmpty.head <$> traverse pick_one_conlike ms
+markMatched _   NoPM    = NoPM
+markMatched con (PM ms) = PM (del_one_con con <$> ms)
   where
-    pick_one_conlike cs = case uniqDSetToList cs of
-      [] -> Nothing
-      (cl:_) -> Just cl
+    del_one_con = flip delOneFromUniqDSet
 
 ---------------------------------------------------
 -- * Instantiating constructors, types and evidence
@@ -172,8 +152,13 @@ mkOneConFull arg_tys con = do
   -- to the type oracle
   let ty_cs = map TyCt (substTheta subst (eqSpecPreds eq_spec ++ thetas))
   -- Figure out the types of strict constructor fields
-  let arg_is_banged = map isBanged $ conLikeImplBangs con
-      strict_arg_tys = filterByList arg_is_banged field_tys'
+  let arg_is_strict
+        | RealDataCon dc <- con
+        , isNewTyCon (dataConTyCon dc)
+        = [True] -- See Note [Divergence of Newtype matches]
+        | otherwise
+        = map isBanged $ conLikeImplBangs con
+      strict_arg_tys = filterByList arg_is_strict field_tys'
   return (vars, listToBag ty_cs, strict_arg_tys)
 
 -------------------------
@@ -277,7 +262,7 @@ data TopNormaliseTypeResult
   -- ^ 'tcNormalise' was able to simplify the type with some local constraint
   -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type
   -- redex.
-  | HadRedexes Type [(Type, DataCon)] Type
+  | HadRedexes Type [(Type, DataCon, Type)] Type
   -- ^ 'tcNormalise' may or may not been able to simplify the type, but
   -- 'topNormaliseTypeX' made progress either way and got rid of at least one
   -- outermost type or data family redex or newtype.
@@ -289,8 +274,10 @@ data TopNormaliseTypeResult
   -- Core (modulo casts).
   -- The second field is the list of Newtype 'DataCon's that we looked through
   -- in the chain of reduction steps between the Source type and the Core type.
-  -- We also keep the type of the DataCon application, so that we don't have to
-  -- reconstruct it in inhabitationCandidates.build_newtype.
+  -- We also keep the type of the DataCon application and its field, so that we
+  -- don't have to reconstruct it in 'inhabitationCandidates' and
+  -- 'provideEvidence'.
+  -- For an example, see Note [Type normalisation].
 
 -- | Just give me the potentially normalised source type, unchanged or not!
 normalisedSourceType :: TopNormaliseTypeResult -> Type
@@ -298,6 +285,13 @@ normalisedSourceType (NoChange ty)                = ty
 normalisedSourceType (NormalisedByConstraints ty) = ty
 normalisedSourceType (HadRedexes ty _ _)          = ty
 
+-- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the
+-- other cases.
+tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
+tntrGuts (NoChange ty)                  = (ty,     [],      ty)
+tntrGuts (NormalisedByConstraints ty)   = (ty,     [],      ty)
+tntrGuts (HadRedexes src_ty ds core_ty) = (src_ty, ds, core_ty)
+
 instance Outputable TopNormaliseTypeResult where
   ppr (NoChange ty)                  = text "NoChange" <+> ppr ty
   ppr (NormalisedByConstraints ty)   = text "NormalisedByConstraints" <+> ppr ty
@@ -315,7 +309,7 @@ pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
 --
 -- Behaves like `topNormaliseType_maybe`, but instead of returning a
 -- coercion, it returns useful information for issuing pattern matching
--- warnings. See Note [Type normalisation for EmptyCase] for details.
+-- warnings. See Note [Type normalisation] for details.
 -- It also initially 'tcNormalise's the type with the bag of local constraints.
 --
 -- See 'TopNormaliseTypeResult' for the meaning of the return value.
@@ -327,7 +321,7 @@ pmTopNormaliseType (TySt inert) typ
   = do env <- dsGetFamInstEnvs
        -- Before proceeding, we chuck typ into the constraint solver, in case
        -- solving for given equalities may reduce typ some. See
-       -- "Wrinkle: local equalities" in Note [Type normalisation for EmptyCase].
+       -- "Wrinkle: local equalities" in Note [Type normalisation].
        (_, mb_typ') <- initTcDsForSolver $ tcNormalise inert typ
        -- If tcNormalise didn't manage to simplify the type, continue anyway.
        -- We might be able to reduce type applications nonetheless!
@@ -364,13 +358,13 @@ pmTopNormaliseType (TySt inert) typ
 
     -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
     -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
-    newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon)] -> [(Type, DataCon)])
+    newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
     newTypeStepper rec_nts tc tys
       | Just (ty', _co) <- instNewTyCon_maybe tc tys
       , let orig_ty = TyConApp tc tys
       = case checkRecTc rec_nts tc of
           Just rec_nts' -> let tyf = (orig_ty:)
-                               tmf = ((orig_ty, tyConSingleDataCon tc):)
+                               tmf = ((orig_ty, tyConSingleDataCon tc, ty'):)
                            in  NS_Step rec_nts' ty' (tyf, tmf)
           Nothing       -> NS_Abort
       | otherwise
@@ -423,13 +417,14 @@ pmIsClosedType ty
     is_algebraic_like :: TyCon -> Bool
     is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon
 
-{- Note [Type normalisation for EmptyCase]
+{- Note [Type normalisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-EmptyCase is an exception for pattern matching, since it is strict. This means
-that it boils down to checking whether the type of the scrutinee is inhabited.
-Function pmTopNormaliseType gets rid of the outermost type function/data
-family redex and newtypes, in search of an algebraic type constructor, which is
-easier to check for inhabitation.
+Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data
+constructor place a non-void constraint on the matched thing. This means that it
+boils down to checking whether the type of the scrutinee is inhabited. Function
+pmTopNormaliseType gets rid of the outermost type function/data family redex and
+newtypes, in search of an algebraic type constructor, which is easier to check
+for inhabitation.
 
 It returns 3 results instead of one, because there are 2 subtle points:
 1. Newtypes are isomorphic to the underlying type in core but not in the source
@@ -444,7 +439,8 @@ then
       newtypes.
   (b) dcs is the list of newtype constructors "skipped", every time we normalise
       a newtype to its core representation, we keep track of the source data
-      constructor and the type we unwrap.
+      constructor. For convenienve, we also track the type we unwrap and the
+      type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)]
   (c) core_ty is the rewritten type. That is,
         pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty)
       implies
@@ -468,7 +464,7 @@ To see how all cases come into play, consider the following example:
 
 In this case pmTopNormaliseType env ty_cs (F Int) results in
 
-  Just (G2, [(G2,MkG2),(G1,MkG1)], R:TInt)
+  Just (G2, [(G2,MkG2,G1),(G1,MkG1,T Int)], R:TInt)
 
 Which means that in source Haskell:
   - G2 is equivalent to F Int (in contrast, G1 isn't).
@@ -520,6 +516,7 @@ tyOracle :: TyState -> Bag TyCt -> DsM (Maybe TyState)
 tyOracle (TySt inert) cts
   = do { evs <- traverse nameTyCt cts
        ; let new_inert = inert `unionBags` evs
+       ; tracePm "tyOracle" (ppr cts)
        ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability new_inert
        ; case res of
             -- Note how this implicitly gives all former PredTyCts a name, so
@@ -534,8 +531,7 @@ tyOracle (TySt inert) cts
 -- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle
 -- for emptiness if the first argument is 'True'.
 tyIsSatisfiable :: Bool -> Bag TyCt -> SatisfiabilityCheck
-tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> do
-  tracePm "tyIsSatisfiable" (ppr new_ty_cs)
+tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta ->
   if isEmptyBag new_ty_cs
     then pure (Just delta)
     else tyOracle (delta_ty_st delta) new_ty_cs >>= \case
@@ -684,6 +680,12 @@ initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do
   let ty' = normalisedSourceType res
   case splitTyConApp_maybe ty' of
     Nothing -> pure vi{ vi_ty = ty' }
+    Just (tc, [_])
+      | tc == tYPETyCon
+      -- TYPE acts like an empty data type on the term-level (#14086), but
+      -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
+      -- special case.
+      -> pure vi{ vi_ty = ty', vi_cache = PM (pure emptyUniqDSet) }
     Just (tc, tc_args) -> do
       -- See Note [COMPLETE sets on data families]
       (tc_rep, tc_fam) <- case tyConFamInst_maybe tc of
@@ -703,7 +705,7 @@ initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do
       -- pprTrace "initPossibleMatches" (ppr ty $$ ppr ty' $$ ppr tc_rep <+> ppr tc_fam <+> ppr tc_args $$ ppr (rdcs ++ pscs)) (return ())
       case NonEmpty.nonEmpty (rdcs ++ pscs) of
         Nothing -> pure vi{ vi_ty = ty' } -- Didn't find any COMPLETE sets
-        Just cs -> pure vi{ vi_ty = ty', vi_cache = PM tc_rep (mkUniqDSet <$> cs) }
+        Just cs -> pure vi{ vi_ty = ty', vi_cache = PM (mkUniqDSet <$> cs) }
 initPossibleMatches _     vi                                   = pure vi
 
 -- | @initLookupVarInfo ts x@ looks up the 'VarInfo' for @x@ in @ts@ and tries
@@ -759,20 +761,42 @@ TyCon, so tc_rep = tc_fam afterwards.
 ------------------------------------------------
 -- * Exported utility functions querying 'Delta'
 
--- | Check whether a constraint (x ~ BOT) can succeed,
--- given the resulting state of the term oracle.
+-- | Check whether adding a constraint @x ~ BOT@ to 'Delta' succeeds.
 canDiverge :: Delta -> Id -> Bool
-canDiverge MkDelta{ delta_tm_st = ts } x
-  -- If the variable seems not evaluated, there is a possibility for
-  -- constraint x ~ BOT to be satisfiable. That's the case when we haven't found
-  -- a solution (i.e. some equivalent literal or constructor) for it yet.
-  -- Even if we don't have a solution yet, it might be involved in a negative
-  -- constraint, in which case we must already have evaluated it earlier.
-  | VI _ [] [] _ <- lookupVarInfo ts x
-  = True
-  -- Variable x is already in WHNF or we know some refutable shape, so the
-  -- constraint is non-satisfiable
-  | otherwise = False
+canDiverge delta@MkDelta{ delta_tm_st = ts } x
+  | VI _ pos neg _ <- lookupVarInfo ts x
+  = null neg && all pos_can_diverge pos
+  where
+    pos_can_diverge (PmAltConLike (RealDataCon dc), [y])
+      -- See Note [Divergence of Newtype matches]
+      | isNewTyCon (dataConTyCon dc) = canDiverge delta y
+    pos_can_diverge _ = False
+
+{- Note [Divergence of Newtype matches]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Newtypes behave rather strangely when compared to ordinary DataCons. In a
+pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation
+testing purposes (e.g. at construction sites), they behave rather like a DataCon
+with a *strict* field, because they don't contribute their own bottom and are
+inhabited iff the wrapped type is inhabited.
+
+This distinction becomes apparent in #17248:
+
+  newtype T2 a = T2 a
+  g _      True = ()
+  g (T2 _) True = ()
+  g !_     True = ()
+
+If we treat Newtypes like we treat regular DataCons, we would mark the third
+clause as redundant, which clearly is unsound. The solution:
+1. When checking the PmCon in 'pmCheck', never mark the result as Divergent if
+   it's a Newtype match.
+2. Regard @T2 x@ as 'canDiverge' iff @x@ 'canDiverge'. E.g. @T2 x ~ _|_@ <=>
+   @x ~ _|_@. This way, the third clause will still be marked as inaccessible
+   RHS instead of redundant.
+3. When testing for inhabitants ('mkOneConFull'), we regard the newtype field as
+   strict, so that the newtype is inhabited iff its field is inhabited.
+-}
 
 lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
 -- Unfortunately we need the extra bit of polymorphism and the unfortunate
@@ -922,8 +946,8 @@ addVarNonVoidCt delta@MkDelta{ delta_tm_st = TmSt env reps } x = do
   pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') reps}
 
 ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
-   -- Returns (Just vi) guarantees that at least one member
-   -- of each ConLike in the COMPLETE set satisfies the oracle
+   -- Returns (Just vi) if at least one member of each ConLike in the COMPLETE
+   -- set satisfies the oracle
    --
    -- Internally uses and updates the ConLikeSets in vi_cache.
    --
@@ -934,8 +958,8 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
   where
     set_cache vi cache = vi { vi_cache = cache }
 
-    test NoPM       = pure (Just NoPM)
-    test (PM tc ms) = runMaybeT (PM tc <$> traverse one_set ms)
+    test NoPM    = pure (Just NoPM)
+    test (PM ms) = runMaybeT (PM <$> traverse one_set ms)
 
     one_set cs = find_one_inh cs (uniqDSetToList cs)
 
@@ -961,6 +985,7 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
         Nothing -> pure True -- be conservative about this
         Just arg_tys -> do
           (_vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con
+          tracePm "inh_test" (ppr con $$ ppr ty_cs)
           -- No need to run the term oracle compared to pmIsSatisfiable
           fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
             -- Important to pass False to tyIsSatisfiable here, so that we won't
@@ -1108,27 +1133,23 @@ inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do
     NormalisedByConstraints ty'   -> alts_to_check ty'    ty'     []
     HadRedexes src_ty dcs core_ty -> alts_to_check src_ty core_ty dcs
   where
-    -- All these types are trivially inhabited
-    trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
-                          , intTyCon, wordTyCon, word8TyCon ]
-
-    build_newtype :: (Type, DataCon) -> Id -> DsM (Id, TmCt)
-    build_newtype (ty, dc) x = do
+    build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, TmCt)
+    build_newtype (ty, dc, _arg_ty) x = do
       -- ty is the type of @dc x@. It's a @dataConTyCon dc@ application.
       y <- mkPmId ty
       pure (y, TmVarCon y (PmAltConLike (RealDataCon dc)) [x])
 
-    build_newtypes :: Id -> [(Type, DataCon)] -> DsM (Id, [TmCt])
+    build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
     build_newtypes x = foldrM (\dc (x, cts) -> go dc x cts) (x, [])
       where
         go dc x cts = second (:cts) <$> build_newtype dc x
 
     -- Inhabitation candidates, using the result of pmTopNormaliseType
-    alts_to_check :: Type -> Type -> [(Type, DataCon)]
+    alts_to_check :: Type -> Type -> [(Type, DataCon, Type)]
                   -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
     alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
       Just (tc, _)
-        |  tc `elem` trivially_inhabited
+        |  isTyConTriviallyInhabited tc
         -> case dcs of
              []    -> return (Left src_ty)
              (_:_) -> do inner <- mkPmId core_ty
@@ -1150,16 +1171,14 @@ inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do
       -- For other types conservatively assume that they are inhabited.
       _other -> return (Left src_ty)
 
-inhabitants :: Delta -> Type -> DsM (Either Type (Id, [Delta]))
-inhabitants delta ty = inhabitationCandidates delta ty >>= \case
-  Left ty' -> pure (Left ty')
-  Right (_, va, candidates) -> do
-    deltas <- flip mapMaybeM candidates $
-        \InhabitationCandidate{ ic_tm_cs = tm_cs
-                              , ic_ty_cs = ty_cs
-                              , ic_strict_arg_tys = strict_arg_tys } -> do
-      pmIsSatisfiable delta tm_cs ty_cs strict_arg_tys
-    pure (Right (va, deltas))
+-- | All these types are trivially inhabited
+triviallyInhabitedTyCons :: UniqSet TyCon
+triviallyInhabitedTyCons = mkUniqSet [
+    charTyCon, doubleTyCon, floatTyCon, intTyCon, wordTyCon, word8TyCon
+  ]
+
+isTyConTriviallyInhabited :: TyCon -> Bool
+isTyConTriviallyInhabited tc = elementOfUniqSet tc triviallyInhabitedTyCons
 
 ----------------------------
 -- * Detecting vacuous types
@@ -1187,7 +1206,7 @@ we do the following:
    (c) A list of all newtype data constructors dcs, each one corresponding to a
        newtype rewrite performed in (b).
 
-   For an example see also Note [Type normalisation for EmptyCase]
+   For an example see also Note [Type normalisation]
    in types/FamInstEnv.hs.
 
 2. Function Check.checkEmptyCase' performs the check:
@@ -1282,8 +1301,8 @@ definitelyInhabitedType ty_st ty = do
            HadRedexes _ cons _ -> any meets_criteria cons
            _                   -> False
   where
-    meets_criteria :: (Type, DataCon) -> Bool
-    meets_criteria (_, con) =
+    meets_criteria :: (Type, DataCon, Type) -> Bool
+    meets_criteria (_, con, _) =
       null (dataConEqSpec con) && -- (1)
       null (dataConImplBangs con) -- (2)
 
@@ -1415,22 +1434,19 @@ on a list of strict argument types, we filter out all of the DI ones.
 --------------------------------------------
 -- * Providing positive evidence for a Delta
 
--- | @provideEvidenceForEquation vs n delta@ returns a list of
+-- | @provideEvidence vs n delta@ returns a list of
 -- at most @n@ (but perhaps empty) refinements of @delta@ that instantiate
 -- @vs@ to compatible constructor applications or wildcards.
 -- Negative information is only retained if literals are involved or when
 -- for recursive GADTs.
-provideEvidenceForEquation :: [Id] -> Int -> Delta -> DsM [Delta]
-provideEvidenceForEquation = go init_ts
+provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
+provideEvidence = go
   where
-    -- Choosing 1 here will not be enough for RedBlack, but any other bound
-    -- might potentially lead to combinatorial explosion, so we are extremely
-    -- cautious and pick 2 here.
-    init_ts                  = setRecTcMaxBound 2 initRecTc
-    go _      _      0 _     = pure []
-    go _      []     _ delta = pure [delta]
-    go rec_ts (x:xs) n delta = do
-      VI ty pos neg pm <- initLookupVarInfo delta x
+    go _      0 _     = pure []
+    go []     _ delta = pure [delta]
+    go (x:xs) n delta = do
+      tracePm "provideEvidence" (ppr x $$ ppr xs $$ ppr delta $$ ppr n)
+      VI _ pos neg _ <- initLookupVarInfo delta x
       case pos of
         _:_ -> do
           -- All solutions must be valid at once. Try to find candidates for their
@@ -1443,91 +1459,81 @@ provideEvidenceForEquation = go init_ts
           -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@
           -- and @z@ that is valid at the same time. These constitute arg_vas below.
           let arg_vas = concatMap (\(_cl, args) -> args) pos
-          go rec_ts (arg_vas ++ xs) n delta
+          go (arg_vas ++ xs) n delta
         []
-          -- First the simple case where we don't need to query the oracles
-          | isVanillaDataType ty
-              -- So no type info unleashed in pattern match
-          , null neg
-              -- No term-level info either
-          || notNull [ l | PmAltLit l <- neg ]
-              -- ... or there are literals involved, in which case we don't want
-              -- to split on possible constructors
-          -> go rec_ts xs n delta
-        [] -> do
-          -- We have to pick one of the available constructors and try it
-          -- It's important that each of the ConLikeSets in pm is still inhabited,
-          -- so that it doesn't matter from which we pick.
-          -- I think we implicitly uphold that invariant, but not too sure
-          case getUnmatchedConstructor pm of
-            Unsatisfiable -> pure []
-            -- No COMPLETE sets available, so we can assume it's inhabited
-            PossiblySatisfiable -> go rec_ts xs n delta
-            Satisfiable cl
-              | Just rec_ts' <- checkRecTc rec_ts (fst (splitTyConApp ty))
-              -> split_at_con rec_ts' delta n x xs cl
-              | otherwise
-              -- We ran out of fuel; just conservatively assume that this is
-              -- inhabited.
-              -> go rec_ts xs n delta
-
-    -- | @split_at_con _ delta _ x _ con@ splits the given delta into two
-    -- models: One where we assume x is con and one where we assume it can't be
-    -- con. Really similar to the ConVar case in Check, only that we don't
-    -- really have a pattern driving the split.
-    split_at_con
-      :: RecTcChecker -- ^ Detects when we split the same TyCon too often
-      -> Delta        -- ^ The model we like to refine to the split
-      -> Int          -- ^ The number of equations still to produce
-      -> Id -> [Id]   -- ^ Head and tail of the value abstractions
-      -> ConLike      -- ^ The ConLike over which to split
-      -> DsM [Delta]
-    split_at_con rec_ts delta n x xs cl = do
-      -- This will be really similar to the ConVar case
-      -- We may need to reduce type famlies/synonyms in x's type first
-      res <- pmTopNormaliseType (delta_ty_st delta) (idType x)
-      let res_ty = normalisedSourceType res
+          -- When there are literals involved, just print negative info
+          -- instead of listing missed constructors
+          | notNull [ l | PmAltLit l <- neg ]
+          -> go xs n delta
+        [] -> try_instantiate x xs n delta
+
+    -- | Tries to instantiate a variable by possibly following the chain of
+    -- newtypes and then instantiating to all ConLikes of the wrapped type's
+    -- minimal residual COMPLETE set.
+    try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta]
+    -- Convention: x binds the outer constructor in the chain, y the inner one.
+    try_instantiate x xs n delta = do
+      (_src_ty, dcs, core_ty) <- tntrGuts <$> pmTopNormaliseType (delta_ty_st delta) (idType x)
+      let build_newtype (x, delta) (_ty, dc, arg_ty) = do
+            y <- lift $ mkPmId arg_ty
+            delta' <- addVarConCt delta x (PmAltConLike (RealDataCon dc)) [y]
+            pure (y, delta')
+      runMaybeT (foldlM build_newtype (x, delta) dcs) >>= \case
+        Nothing -> pure []
+        Just (y, newty_delta) -> do
+          -- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥.
+          pm     <- vi_cache <$> initLookupVarInfo newty_delta y
+          mb_cls <- pickMinimalCompleteSet newty_delta pm
+          case uniqDSetToList <$> mb_cls of
+            Just cls@(_:_) -> instantiate_cons y core_ty xs n newty_delta cls
+            Just [] | not (canDiverge newty_delta y) -> pure []
+            -- Either ⊥ is still possible (think Void) or there are no COMPLETE
+            -- sets available, so we can assume it's inhabited
+            _ -> go xs n newty_delta
+
+    instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
+    instantiate_cons _ _  _  _ _     []       = pure []
+    instantiate_cons _ _  _  0 _     _        = pure []
+    instantiate_cons _ ty xs n delta _
+      -- We don't want to expose users to GHC-specific constructors for Int etc.
+      | fmap (isTyConTriviallyInhabited . fst) (splitTyConApp_maybe ty) == Just True
+      = go xs n delta
+    instantiate_cons x ty xs n delta (cl:cls) = do
       env <- dsGetFamInstEnvs
-      case guessConLikeUnivTyArgsFromResTy env res_ty cl of
-        Nothing      -> pure [delta] -- We can't split this one, so assume it's inhabited
+      case guessConLikeUnivTyArgsFromResTy env ty cl of
+        Nothing -> pure [delta] -- No idea idea how to refine this one, so just finish off with a wildcard
         Just arg_tys -> do
           (arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl
           let new_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
           -- Now check satifiability
           mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys
-          tracePm "split_at_con" (vcat [ ppr x
-                                       , ppr new_tm_cs
-                                       , ppr new_ty_cs
-                                       , ppr strict_arg_tys
-                                       , ppr delta
-                                       , ppr mb_delta ])
-          ev_pos <- case mb_delta of
+          tracePm "instantiate_cons" (vcat [ ppr x
+                                           , ppr (idType x)
+                                           , ppr ty
+                                           , ppr cl
+                                           , ppr arg_tys
+                                           , ppr new_tm_cs
+                                           , ppr new_ty_cs
+                                           , ppr strict_arg_tys
+                                           , ppr delta
+                                           , ppr mb_delta
+                                           , ppr n ])
+          con_deltas <- case mb_delta of
             Nothing     -> pure []
-            Just delta' -> go rec_ts (arg_vars ++ xs) n delta'
-
-          -- Only n' more equations to go...
-          let n' = n - length ev_pos
-          ev_neg <- addRefutableAltCon delta x (PmAltConLike cl) >>= \case
-            Nothing                          -> pure []
-            Just delta'                      -> go rec_ts (x:xs) n' delta'
-
-          -- Actually there was no need to split if we see that both branches
-          -- were inhabited and we had no negative information on the variable!
-          -- So only refine delta if we find that one branch was indeed
-          -- uninhabited.
-          let neg = lookupRefuts delta x
-          case (ev_pos, ev_neg) of
-            ([], _)       -> pure ev_neg
-            (_, [])       -> pure ev_pos
-            _ | null neg  -> pure [delta]
-              | otherwise -> pure (ev_pos ++ ev_neg)
-
--- | Checks if every data con of the type 'isVanillaDataCon'.
-isVanillaDataType :: Type -> Bool
-isVanillaDataType ty = fromMaybe False $ do
-  (tc, _) <- splitTyConApp_maybe ty
-  dcs <- tyConDataCons_maybe tc
-  pure (all isVanillaDataCon dcs)
+            -- NB: We don't prepend arg_vars as we don't have any evidence on
+            -- them and we only want to split once on a data type. They are
+            -- inhabited, otherwise pmIsSatisfiable would have refuted.
+            Just delta' -> go xs n delta'
+          other_cons_deltas <- instantiate_cons x ty xs (n - length con_deltas) delta cls
+          pure (con_deltas ++ other_cons_deltas)
+
+pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
+pickMinimalCompleteSet _ NoPM      = pure Nothing
+-- TODO: First prune sets with type info in delta. But this is good enough for
+-- now and less costly. See #17386.
+pickMinimalCompleteSet _ (PM clss) = do
+  tracePm "pickMinimalCompleteSet" (ppr $ NonEmpty.toList clss)
+  pure (Just (minimumBy (comparing sizeUniqDSet) clss))
 
 -- | See if we already encountered a semantically equivalent expression and
 -- return its representative.
@@ -1558,6 +1564,7 @@ addVarCoreCt delta x e = runMaybeT (execStateT (core_expr x e) delta)
     -- This is the right thing for casts involving data family instances and
     -- their representation TyCon, though (which are not visible in source
     -- syntax). See Note [COMPLETE sets on data families]
+    -- core_expr x e | pprTrace "core_expr" (ppr x $$ ppr e) False = undefined
     core_expr x (Cast e _co) = core_expr x e
     core_expr x (Tick _t e) = core_expr x e
     core_expr x e
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index 61d8c1864d..10f172a430 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -128,44 +128,6 @@ instance Eq PmLit where
 pmLitType :: PmLit -> Type
 pmLitType (PmLit ty _) = ty
 
--- | Type of a 'PmAltCon'
-pmAltConType :: PmAltCon -> [Type] -> Type
-pmAltConType (PmAltLit lit)     _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
-pmAltConType (PmAltConLike con) arg_tys  = conLikeResTy con arg_tys
-
-instance Outputable PmLitValue where
-  ppr (PmLitInt i)        = ppr i
-  ppr (PmLitRat r)        = ppr (double (fromRat r)) -- good enough
-  ppr (PmLitChar c)       = pprHsChar c
-  ppr (PmLitString s)     = pprHsString s
-  ppr (PmLitOverInt n i)  = minuses n (ppr i)
-  ppr (PmLitOverRat n r)  = minuses n (ppr (double (fromRat r)))
-  ppr (PmLitOverString s) = pprHsString s
-
--- Take care of negated literals
-minuses :: Int -> SDoc -> SDoc
-minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
-
-instance Outputable PmLit where
-  ppr (PmLit ty v) = ppr v <> suffix
-    where
-      -- Some ad-hoc hackery for displaying proper lit suffixes based on type
-      tbl = [ (intPrimTy, primIntSuffix)
-            , (int64PrimTy, primInt64Suffix)
-            , (wordPrimTy, primWordSuffix)
-            , (word64PrimTy, primWord64Suffix)
-            , (charPrimTy, primCharSuffix)
-            , (floatPrimTy, primFloatSuffix)
-            , (doublePrimTy, primDoubleSuffix) ]
-      suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
-
-instance Outputable PmAltCon where
-  ppr (PmAltConLike cl) = ppr cl
-  ppr (PmAltLit l)      = ppr l
-
-instance Outputable PmEquality where
-  ppr = text . show
-
 -- | Undecidable equality for values represented by 'ConLike's.
 -- See Note [Undecidable Equality for PmAltCons].
 -- 'PatSynCon's aren't enforced to be generative, so two syntactically different
@@ -222,6 +184,11 @@ eqPmAltCon _                  _                  = PossiblyOverlap
 instance Eq PmAltCon where
   a == b = eqPmAltCon a b == Equal
 
+-- | Type of a 'PmAltCon'
+pmAltConType :: PmAltCon -> [Type] -> Type
+pmAltConType (PmAltLit lit)     _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
+pmAltConType (PmAltConLike con) arg_tys  = conLikeResTy con arg_tys
+
 {- Note [Undecidable Equality for PmAltCons]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Equality on overloaded literals is undecidable in the general case. Consider
@@ -364,20 +331,53 @@ coreExprAsPmLit e = case collectArgs e of
       | otherwise
       = False
 
+instance Outputable PmLitValue where
+  ppr (PmLitInt i)        = ppr i
+  ppr (PmLitRat r)        = ppr (double (fromRat r)) -- good enough
+  ppr (PmLitChar c)       = pprHsChar c
+  ppr (PmLitString s)     = pprHsString s
+  ppr (PmLitOverInt n i)  = minuses n (ppr i)
+  ppr (PmLitOverRat n r)  = minuses n (ppr (double (fromRat r)))
+  ppr (PmLitOverString s) = pprHsString s
+
+-- Take care of negated literals
+minuses :: Int -> SDoc -> SDoc
+minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
+
+instance Outputable PmLit where
+  ppr (PmLit ty v) = ppr v <> suffix
+    where
+      -- Some ad-hoc hackery for displaying proper lit suffixes based on type
+      tbl = [ (intPrimTy, primIntSuffix)
+            , (int64PrimTy, primInt64Suffix)
+            , (wordPrimTy, primWordSuffix)
+            , (word64PrimTy, primWord64Suffix)
+            , (charPrimTy, primCharSuffix)
+            , (floatPrimTy, primFloatSuffix)
+            , (doublePrimTy, primDoubleSuffix) ]
+      suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
+
+instance Outputable PmAltCon where
+  ppr (PmAltConLike cl) = ppr cl
+  ppr (PmAltLit l)      = ppr l
+
+instance Outputable PmEquality where
+  ppr = text . show
+
 type ConLikeSet = UniqDSet ConLike
 
 -- | A data type caching the results of 'completeMatchConLikes' with support for
--- deletion of contructors that were already matched on.
+-- deletion of constructors that were already matched on.
 data PossibleMatches
-  = PM TyCon (NonEmpty.NonEmpty ConLikeSet)
-  -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE pragma
+  = PM (NonEmpty.NonEmpty ConLikeSet)
+  -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE set
   -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
-  -- set at all, for which we have 'NoPM'
+  -- set at all, for which we have 'NoPM'.
   | NoPM
   -- ^ No COMPLETE set for this type (yet). Think of overloaded literals.
 
 instance Outputable PossibleMatches where
-  ppr (PM _tc cs) = ppr (NonEmpty.toList cs)
+  ppr (PM cs) = ppr (NonEmpty.toList cs)
   ppr NoPM = text "<NoPM>"
 
 -- | Either @Indirect x@, meaning the value is represented by that of @x@, or
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index af2ed4b7e1..6421be4f16 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -241,7 +241,11 @@ tcCompleteSigs sigs =
 
           mkMatch :: [ConLike] -> TyCon -> CompleteMatch
           mkMatch cls ty_con = CompleteMatch {
-            completeMatchConLikes = map conLikeName cls,
+            -- foldM is a left-fold and will have accumulated the ConLikes in
+            -- the reverse order. foldrM would accumulate in the correct order,
+            -- but would type-check the last ConLike first, which might also be
+            -- confusing from the user's perspective. Hence reverse here.
+            completeMatchConLikes = reverse (map conLikeName cls),
             completeMatchTyCon = tyConName ty_con
             }
       doOne _ = return Nothing
@@ -287,7 +291,10 @@ tcCompleteSigs sigs =
                   <+> parens (quotes (ppr tc)
                                <+> text "resp."
                                <+> quotes (ppr tc'))
-  in  mapMaybeM (addLocM doOne) sigs
+  -- For some reason I haven't investigated further, the signatures come in
+  -- backwards wrt. declaration order. So we reverse them here, because it makes
+  -- a difference for incomplete match suggestions.
+  in  mapMaybeM (addLocM doOne) (reverse sigs) -- process in declaration order
 
 tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
 -- A hs-boot file has only one BindGroup, and it only has type
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 34bc4a8448..37015b30bc 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -693,7 +693,7 @@ It does *not* reduce type or data family applications or look through newtypes.
 Why is this useful? As one example, when coverage-checking an EmptyCase
 expression, it's possible that the type of the scrutinee will only reduce
 if some local equalities are solved for. See "Wrinkle: Local equalities"
-in Note [Type normalisation for EmptyCase] in Check.
+in Note [Type normalisation] in Check.
 
 To accomplish its stated goal, tcNormalise first feeds the local constraints
 into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.stderr b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
index 81bbc539cf..c36ee98d91 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.stderr
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
@@ -3,4 +3,7 @@ KindEqualities.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘zero’:
         Patterns not matched:
-            TyApp (TyApp p _) _ where p is not one of {TyInt}
+            TyApp (TyApp _ _) TyInt
+            TyApp (TyApp _ _) TyBool
+            TyApp (TyApp _ _) TyMaybe
+            TyApp (TyApp _ _) (TyApp _ _)
diff --git a/testsuite/tests/pmcheck/complete_sigs/T17386.hs b/testsuite/tests/pmcheck/complete_sigs/T17386.hs
new file mode 100644
index 0000000000..05afb44135
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T17386.hs
@@ -0,0 +1,18 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE PatternSynonyms #-}
+module Lib where
+
+data B = T | F
+pattern P :: B
+pattern P = T
+{-# COMPLETE P, F #-}
+
+f :: B -> ()
+f P = ()
+
+pattern Q :: B
+pattern Q = T
+{-# COMPLETE T, Q #-}
+
+g :: B -> ()
+g Q = ()
diff --git a/testsuite/tests/pmcheck/complete_sigs/T17386.stderr b/testsuite/tests/pmcheck/complete_sigs/T17386.stderr
new file mode 100644
index 0000000000..9b60c06636
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T17386.stderr
@@ -0,0 +1,8 @@
+
+T17386.hs:11:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘f’: Patterns not matched: F
+
+T17386.hs:18:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘g’: Patterns not matched: T
diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T
index 7e70f3aa10..bc4f39ac39 100644
--- a/testsuite/tests/pmcheck/complete_sigs/all.T
+++ b/testsuite/tests/pmcheck/complete_sigs/all.T
@@ -16,7 +16,7 @@ test('completesig15', normal, compile_fail, [''])
 test('T13021', normal, compile, [''])
 test('T13363a', normal, compile, [''])
 test('T13363b', normal, compile, [''])
-test('T13717', expect_broken('13717'), compile, [''])
+test('T13717', normal, compile, [''])
 test('T13964', normal, compile, [''])
 test('T13965', normal, compile, [''])
 test('T14059a', normal, compile, [''])
@@ -24,3 +24,4 @@ test('T14059b', expect_broken('14059'), compile, [''])
 test('T14253', normal, compile, [''])
 test('T14851', normal, compile, [''])
 test('T17149', normal, compile, [''])
+test('T17386', normal, compile, [''])
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr
index 66a7604ca9..8659a3b0aa 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr
@@ -25,5 +25,5 @@ completesig06.hs:29:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘m5’:
         Patterns not matched:
-            A _
-            B _
+            A D
+            B D
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
index 4c10a09085..d30cc52590 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
@@ -9,4 +9,4 @@ EmptyCase003.hs:32:6: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase003.hs:37:6: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Char
+    In a case alternative: Patterns not matched: _ :: C Int
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
index 1d185cc8bb..9c346b9c8b 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
@@ -30,4 +30,4 @@ EmptyCase005.hs:91:8: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase005.hs:101:8: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: H Char
+    In a case alternative: Patterns not matched: _ :: H Int
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
index 42cbcf380d..0ab13ca321 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
@@ -1,11 +1,11 @@
 
 EmptyCase007.hs:21:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Foo2 a
+    In a case alternative: Patterns not matched: Foo2 _
 
 EmptyCase007.hs:25:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Foo2 (a, a)
+    In a case alternative: Patterns not matched: Foo2 _
 
 EmptyCase007.hs:33:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
@@ -17,7 +17,7 @@ EmptyCase007.hs:37:7: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase007.hs:44:17: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Char
+    In a case alternative: Patterns not matched: _ :: FA Char
 
 EmptyCase007.hs:48:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
index b33e8ebb40..0d21dbfaca 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
@@ -8,7 +8,7 @@ EmptyCase008.hs:17:7: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase008.hs:21:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Foo3 a
+    In a case alternative: Patterns not matched: Foo3 _
 
 EmptyCase008.hs:40:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
@@ -16,4 +16,4 @@ EmptyCase008.hs:40:7: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase008.hs:48:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Foo4 a b
+    In a case alternative: Patterns not matched: Foo4 _
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
index e5ea398a60..de68e6dae8 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
@@ -1,7 +1,7 @@
 
 EmptyCase009.hs:21:9: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Bar f
+    In a case alternative: Patterns not matched: Bar _
 
 EmptyCase009.hs:33:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
index bfff6c7abe..4b374a0c24 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
@@ -31,7 +31,7 @@ EmptyCase010.hs:45:7: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase010.hs:57:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Baz (DC ()) a
+    In a case alternative: Patterns not matched: Baz _
 
 EmptyCase010.hs:69:7: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
@@ -39,4 +39,4 @@ EmptyCase010.hs:69:7: warning: [-Wincomplete-patterns (in -Wextra)]
 
 EmptyCase010.hs:73:9: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In a case alternative: Patterns not matched: _ :: Baz f a
+    In a case alternative: Patterns not matched: Baz _
diff --git a/testsuite/tests/pmcheck/should_compile/T10746.stderr b/testsuite/tests/pmcheck/should_compile/T10746.stderr
index 9c0a196a08..deb25953e2 100644
--- a/testsuite/tests/pmcheck/should_compile/T10746.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T10746.stderr
@@ -1,3 +1,4 @@
+
 T10746.hs:9:10: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative:
diff --git a/testsuite/tests/pmcheck/should_compile/T11336b.stderr b/testsuite/tests/pmcheck/should_compile/T11336b.stderr
index d824b8314f..f5fc88402d 100644
--- a/testsuite/tests/pmcheck/should_compile/T11336b.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T11336b.stderr
@@ -1,4 +1,4 @@
 
 T11336b.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In an equation for ‘fun’: Patterns not matched: _ :: Proxy a
+    In an equation for ‘fun’: Patterns not matched: Proxy
diff --git a/testsuite/tests/pmcheck/should_compile/T11822.stderr b/testsuite/tests/pmcheck/should_compile/T11822.stderr
index 4cefed97cb..66d365baaa 100644
--- a/testsuite/tests/pmcheck/should_compile/T11822.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T11822.stderr
@@ -10,8 +10,16 @@ T11822.hs:33:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘mkTreeNode’:
         Patterns not matched:
-            _ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0}
-            _ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0}
-            _ (Data.Sequence.Internal.Seq _) _ _
-            _ (Data.Sequence.Internal.Seq _) _ _
+            _ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
+            (Data.Set.Internal.Bin _ _ _ _) p
+                where p is not one of {0}
+            _ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
+            Data.Set.Internal.Tip p
+                where p is not one of {0}
+            _ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
+            (Data.Set.Internal.Bin _ _ _ _) p
+                where p is not one of {0}
+            _ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
+            Data.Set.Internal.Tip p
+                where p is not one of {0}
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17248.hs b/testsuite/tests/pmcheck/should_compile/T17248.hs
index e320bd5184..095153fb08 100644
--- a/testsuite/tests/pmcheck/should_compile/T17248.hs
+++ b/testsuite/tests/pmcheck/should_compile/T17248.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE BangPatterns #-}
 module Lib where
 
 data T1 a = T1 a
@@ -10,6 +11,7 @@ f _      _    = ()
 
 g :: T2 a -> Bool -> ()
 g _      True = ()
-g (T2 _) True = ()
+g (T2 _) True = () -- redundant
+g !_     True = () -- inaccessible
 g _      _    = ()
 
diff --git a/testsuite/tests/pmcheck/should_compile/T17248.stderr b/testsuite/tests/pmcheck/should_compile/T17248.stderr
index 991f167afb..d19619464e 100644
--- a/testsuite/tests/pmcheck/should_compile/T17248.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T17248.stderr
@@ -1,4 +1,12 @@
 
-T17248.hs:8:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+T17248.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match has inaccessible right hand side
     In an equation for ‘f’: f (T1 _) True = ...
+
+T17248.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g (T2 _) True = ...
+
+T17248.hs:15:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘g’: g !_ True = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17357.hs b/testsuite/tests/pmcheck/should_compile/T17357.hs
new file mode 100644
index 0000000000..db1b0ab4fd
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17357.hs
@@ -0,0 +1,51 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE BangPatterns #-}
+module Lib where
+
+import Data.Void
+
+strictConst :: a -> b -> a
+strictConst a b = seq b a
+
+pattern F  <- (const       False -> True)
+pattern SF <- (strictConst False -> True)
+
+-- | The second clause is redundant, really, because (the matcher of) 'F' is
+-- not strict in its argument. As a result, the third clause is *not*
+-- redundant, but inaccessible RHS! Deleting the third clause would be unsound.
+-- This is bad, especially because this outcome depends entirely on the
+-- strictness of 'F's matcher.
+f :: Bool -> Bool -> ()
+f _  True = ()
+f F  True = ()
+f !_ True = ()
+f _  _    = ()
+
+-- | In this example, the second clause really is inaccessible RHS (because SF
+-- is a strict match). And as a result, the third clause *is* redundant.
+f2 :: Bool -> Bool -> ()
+f2 _  True = ()
+f2 SF True = ()
+f2 !_ True = ()
+f2 _  _    = ()
+
+pattern T <- (const True -> True)
+{-# COMPLETE T, F :: Void #-}
+
+-- | But we consider COMPLETE signatures to cover bottom. Hence the last clause
+-- here should be redunant, not inaccessible RHS.
+f3 :: Void -> ()
+f3 T  = ()
+f3 F  = ()
+f3 !_ = ()
+
+-- The following is related to the same issue:
+
+-- | The following function definition is exhaustive.
+-- Its clauses are *not* inaccessible RHS, because neither
+-- pattern synonym is strict.
+g :: Void -> ()
+g F = ()
+g T = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17357.stderr b/testsuite/tests/pmcheck/should_compile/T17357.stderr
new file mode 100644
index 0000000000..84c596e076
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17357.stderr
@@ -0,0 +1,20 @@
+
+T17357.hs:22:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f F True = ...
+
+T17357.hs:23:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f !_ True = ...
+
+T17357.hs:30:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f2’: f2 SF True = ...
+
+T17357.hs:31:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f2’: f2 !_ True = ...
+
+T17357.hs:42:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f3’: f3 !_ = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17376.hs b/testsuite/tests/pmcheck/should_compile/T17376.hs
new file mode 100644
index 0000000000..ce6d7c7e87
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17376.hs
@@ -0,0 +1,7 @@
+module Lib where
+
+import Data.Void
+
+f :: Void -> ()
+f x = case x of _ -> ()
+
diff --git a/testsuite/tests/pmcheck/should_compile/T2204.stderr b/testsuite/tests/pmcheck/should_compile/T2204.stderr
index 26f70352e2..49fcdf6f91 100644
--- a/testsuite/tests/pmcheck/should_compile/T2204.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T2204.stderr
@@ -4,9 +4,9 @@ T2204.hs:6:1: warning: [-Wincomplete-patterns (in -Wextra)]
     In an equation for ‘f’:
         Patterns not matched:
             ('0':'1':_:_)
-            ('0':p:_) where p is not one of {'1'}
+            ['0', p] where p is not one of {'1'}
+            ('0':p:_:_) where p is not one of {'1'}
             ['0']
-            (p:_) where p is not one of {'0'}
             ...
 
 T2204.hs:9:1: warning: [-Wincomplete-patterns (in -Wextra)]
diff --git a/testsuite/tests/pmcheck/should_compile/T9951b.stderr b/testsuite/tests/pmcheck/should_compile/T9951b.stderr
index e4e337b153..51518bce7b 100644
--- a/testsuite/tests/pmcheck/should_compile/T9951b.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T9951b.stderr
@@ -4,7 +4,7 @@ T9951b.hs:7:1: warning: [-Wincomplete-patterns (in -Wextra)]
     In an equation for ‘f’:
         Patterns not matched:
             ('a':'b':_:_)
-            ('a':p:_) where p is not one of {'b'}
+            ['a', p] where p is not one of {'b'}
+            ('a':p:_:_) where p is not one of {'b'}
             ['a']
-            (p:_) where p is not one of {'a'}
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr b/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
index 8180eb1542..2fe93d32d9 100644
--- a/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
+++ b/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
@@ -8,7 +8,12 @@ TooManyDeltas.hs:14:1: warning:
 
 TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In an equation for ‘f’: Patterns not matched: _ _
+    In an equation for ‘f’:
+        Patterns not matched:
+            A A
+            A B
+            B A
+            B B
 
 TooManyDeltas.hs:19:1: warning:
     Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 503fb4041a..6185b0aebb 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -100,7 +100,11 @@ test('T17219', expect_broken(17219), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17234', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
-test('T17248', expect_broken(17248), compile,
+test('T17248', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17357', expect_broken(17357), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17376', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
diff --git a/testsuite/tests/pmcheck/should_compile/pmc007.stderr b/testsuite/tests/pmcheck/should_compile/pmc007.stderr
index d4bbe8fb73..77d2893b2a 100644
--- a/testsuite/tests/pmcheck/should_compile/pmc007.stderr
+++ b/testsuite/tests/pmcheck/should_compile/pmc007.stderr
@@ -10,8 +10,8 @@ pmc007.hs:12:1: warning: [-Wincomplete-patterns (in -Wextra)]
         Patterns not matched:
             ('a':'b':_:_)
             ('a':'c':_:_)
-            ('a':p:_) where p is not one of {'b', 'c'}
-            ['a']
+            ['a', p] where p is not one of {'b', 'c'}
+            ('a':p:_:_) where p is not one of {'b', 'c'}
             ...
 
 pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
@@ -20,6 +20,6 @@ pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
         Patterns not matched:
             ('a':'b':_:_)
             ('a':'c':_:_)
-            ('a':p:_) where p is not one of {'b', 'c'}
-            ['a']
+            ['a', p] where p is not one of {'b', 'c'}
+            ('a':p:_:_) where p is not one of {'b', 'c'}
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/pmc009.stderr b/testsuite/tests/pmcheck/should_compile/pmc009.stderr
index 84c360b6ff..d046b38d0f 100644
--- a/testsuite/tests/pmcheck/should_compile/pmc009.stderr
+++ b/testsuite/tests/pmcheck/should_compile/pmc009.stderr
@@ -1,5 +1,4 @@
 
 pmc009.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In an equation for ‘addPatSynSelector’:
-        Patterns not matched: _ :: LHsBind p
+    In an equation for ‘addPatSynSelector’: Patterns not matched: L _ _