PmCheck: Formulate as translation between Clause Trees

We used to check `GrdVec`s arising from multiple clauses and guards in
isolation. That resulted in a split between `pmCheck` and
`pmCheckGuards`, the implementations of which were similar, but subtly
different in detail. Also the throttling mechanism described in
`Note [Countering exponential blowup]` ultimately got quite complicated
because it had to cater for both checking functions.

This patch realises that pattern match checking doesn't just consider
single guarded RHSs, but that it's always a whole set of clauses, each
of which can have multiple guarded RHSs in turn. We do so by
translating a list of `Match`es to a `GrdTree`:

```haskell
data GrdTree
  = Rhs !RhsInfo
  | Guard !PmGrd !GrdTree      -- captures lef-to-right  match semantics
  | Sequence !GrdTree !GrdTree -- captures top-to-bottom match semantics
  | Empty                      -- For -XEmptyCase, neutral element of Sequence
```

Then we have a function `checkGrdTree` that matches a given `GrdTree`
against an incoming set of values, represented by `Deltas`:

```haskell
checkGrdTree :: GrdTree -> Deltas -> CheckResult
...
```

Throttling is isolated to the `Sequence` case and becomes as easy as one
would expect: When the union of uncovered values becomes too big, just
return the original incoming `Deltas` instead (which is always a
superset of the union, thus a sound approximation).

The returned `CheckResult` contains two things:

1. The set of values that were not covered by any of the clauses, for
   exhaustivity warnings.
2. The `AnnotatedTree` that enriches the syntactic structure of the
   input program with divergence and inaccessibility information.

This is `AnnotatedTree`:

```haskell
data AnnotatedTree
  = AccessibleRhs !RhsInfo
  | InaccessibleRhs !RhsInfo
  | MayDiverge !AnnotatedTree
  | SequenceAnn !AnnotatedTree !AnnotatedTree
  | EmptyAnn
```

Crucially, `MayDiverge` asserts that the tree may force diverging
values, so not all of its wrapped clauses can be redundant.

While the set of uncovered values can be used to generate the missing
equations for warning messages, redundant and proper inaccessible
equations can be extracted from `AnnotatedTree` by
`redundantAndInaccessibleRhss`.

For this to work properly, the interface to the Oracle had to change.
There's only `addPmCts` now, which takes a bag of `PmCt`s. There's a
whole bunch of `PmCt` variants to replace the different oracle functions
from before.

The new `AnnotatedTree` structure allows for more accurate warning
reporting (as evidenced by a number of changes spread throughout GHC's
code base), thus we fix #17465.

Fixes #17646 on the go.

Metric Decrease:
    T11822
    T9233
    PmSeriesS
    haddock.compiler

16 files changed, 521 insertions, 520 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index b494cbed47..99a1236d70 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -46,12 +46,14 @@ import TyCon
 import Var (EvVar)
 import Coercion
 import TcEvidence
+import TcType (evVarPred)
 import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr, dsSyntaxExpr)
 import {-# SOURCE #-} DsBinds (dsHsWrapper)
 import DsUtils (selectMatchVar)
 import MatchLit (dsLit, dsOverLit)
 import DsMonad
 import Bag
+import OrdList
 import TyCoRep
 import Type
 import DsUtils       (isTrueLHsExpr)
@@ -87,14 +89,12 @@ The algorithm is based on the paper:
 -- | A very simple language for pattern guards. Let bindings, bang patterns,
 -- and matching variables against flat constructor patterns.
 data PmGrd
-  = -- | @PmCon x K tvs dicts args@ corresponds to a
-    -- @K tvs dicts args <- x@ guard. The @tvs@ and @args@ are bound in this
-    -- construct, the @x@ is just a use.
+  = -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
+    -- The @args@ are bound in this construct, the @x@ is just a use.
     -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
     PmCon {
       pm_id          :: !Id,
       pm_con_con     :: !PmAltCon,
-      pm_con_tvs     :: ![TyVar],
       pm_con_dicts   :: ![EvVar],
       pm_con_args    :: ![Id]
     }
@@ -113,62 +113,13 @@ data PmGrd
 
 -- | Should not be user-facing.
 instance Outputable PmGrd where
-  ppr (PmCon x alt _con_tvs _con_dicts con_args)
+  ppr (PmCon x alt _con_dicts con_args)
     = hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
   ppr (PmBang x) = char '!' <> ppr x
   ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
 
 type GrdVec = [PmGrd]
 
--- | Each 'Delta' is proof (i.e., a model of the fact) that some values are not
--- covered by a pattern match. E.g. @f Nothing = <rhs>@ might be given an
--- uncovered set @[x :-> Just y]@ or @[x /= Nothing]@, where @x@ is the variable
--- matching against @f@'s first argument.
-type Uncovered = [Delta]
-
--- Instead of keeping the whole sets in memory, we keep a boolean for both the
--- covered and the divergent set (we store the uncovered set though, since we
--- want to print it). For both the covered and the divergent we have:
---
---   True <=> The set is non-empty
---
--- hence:
---  C = True             ==> Useful clause (no warning)
---  C = False, D = True  ==> Clause with inaccessible RHS
---  C = False, D = False ==> Redundant clause
-
-data Covered = Covered | NotCovered
-  deriving Show
-
-instance Outputable Covered where
-  ppr = text . show
-
--- Like the or monoid for booleans
--- Covered = True, Uncovered = False
-instance Semi.Semigroup Covered where
-  Covered <> _ = Covered
-  _ <> Covered = Covered
-  NotCovered <> NotCovered = NotCovered
-
-instance Monoid Covered where
-  mempty = NotCovered
-  mappend = (Semi.<>)
-
-data Diverged = Diverged | NotDiverged
-  deriving Show
-
-instance Outputable Diverged where
-  ppr = text . show
-
-instance Semi.Semigroup Diverged where
-  Diverged <> _ = Diverged
-  _ <> Diverged = Diverged
-  NotDiverged <> NotDiverged = NotDiverged
-
-instance Monoid Diverged where
-  mempty = NotDiverged
-  mappend = (Semi.<>)
-
 data Precision = Approximate | Precise
   deriving (Eq, Show)
 
@@ -176,78 +127,130 @@ instance Outputable Precision where
   ppr = text . show
 
 instance Semi.Semigroup Precision where
-  Approximate <> _ = Approximate
-  _ <> Approximate = Approximate
   Precise <> Precise = Precise
+  _       <> _       = Approximate
 
 instance Monoid Precision where
   mempty = Precise
   mappend = (Semi.<>)
 
--- | A triple <C,U,D> of covered, uncovered, and divergent sets.
---
--- Also stores a flag 'presultApprox' denoting whether we ran into the
--- 'maxPmCheckModels' limit for the purpose of hints in warning messages to
--- maybe increase the limit.
-data PartialResult = PartialResult {
-                        presultCovered   :: Covered
-                      , presultUncovered :: Uncovered
-                      , presultDivergent :: Diverged
-                      , presultApprox    :: Precision }
-
-emptyPartialResult :: PartialResult
-emptyPartialResult = PartialResult { presultUncovered = mempty
-                                   , presultCovered   = mempty
-                                   , presultDivergent = mempty
-                                   , presultApprox    = mempty }
-
-combinePartialResults :: PartialResult -> PartialResult -> PartialResult
-combinePartialResults (PartialResult cs1 vsa1 ds1 ap1) (PartialResult cs2 vsa2 ds2 ap2)
-  = PartialResult (cs1 Semi.<> cs2)
-                  (vsa1 Semi.<> vsa2)
-                  (ds1 Semi.<> ds2)
-                  (ap1 Semi.<> ap2) -- the result is approximate if either is
-
-instance Outputable PartialResult where
-  ppr (PartialResult c unc d pc)
-    = hang (text "PartialResult" <+> ppr c <+> ppr d <+> ppr pc) 2 (ppr_unc unc)
+-- | Means by which we identify a RHS for later pretty-printing in a warning
+-- message. 'SDoc' for the equation to show, 'Located' for the location.
+type RhsInfo = Located SDoc
+
+-- | A representation of the desugaring to 'PmGrd's of all clauses of a
+-- function definition/pattern match/etc.
+data GrdTree
+  = Rhs !RhsInfo
+  | Guard !PmGrd !GrdTree
+  -- ^ @Guard grd t@ will try to match @grd@ and on success continue to match
+  -- @t@. Falls through if either match fails. Models left-to-right semantics
+  -- of pattern matching.
+  | Sequence !GrdTree !GrdTree
+  -- ^ @Sequence l r@ first matches against @l@, and then matches all
+  -- fallen-through values against @r@. Models top-to-bottom semantics of
+  -- pattern matching.
+  | Empty
+  -- ^ A @GrdTree@ that always fails. Most useful for
+  -- Note [Checking EmptyCase]. A neutral element to 'Sequence'.
+
+-- | The digest of 'checkGrdTree', representing the annotated pattern-match
+-- tree. 'redundantAndInaccessibleRhss' can figure out redundant and proper
+-- inaccessible RHSs from this.
+data AnnotatedTree
+  = AccessibleRhs !RhsInfo
+  -- ^ A RHS deemed accessible.
+  | InaccessibleRhs !RhsInfo
+  -- ^ A RHS deemed inaccessible; no value could possibly reach it.
+  | MayDiverge !AnnotatedTree
+  -- ^ Asserts that the tree may force diverging values, so not all of its
+  -- clauses can be redundant.
+  | SequenceAnn !AnnotatedTree !AnnotatedTree
+  -- ^ Mirrors 'Sequence' for preserving the skeleton of a 'GrdTree's.
+  | EmptyAnn
+  -- ^ Mirrors 'Empty' for preserving the skeleton of a 'GrdTree's.
+
+pprRhsInfo :: RhsInfo -> SDoc
+pprRhsInfo (L (RealSrcSpan rss) _) = ppr (srcSpanStartLine rss)
+pprRhsInfo (L s _)                 = ppr s
+
+instance Outputable GrdTree where
+  ppr (Rhs info)      = text "->" <+> pprRhsInfo info
+  -- Format guards as "| True <- x, let x = 42, !z"
+  ppr g@Guard{} = fsep (prefix (map ppr grds)) <+> ppr t
     where
-      ppr_unc = braces . fsep . punctuate comma . map ppr
-
-instance Semi.Semigroup PartialResult where
-  (<>) = combinePartialResults
-
-instance Monoid PartialResult where
-  mempty = emptyPartialResult
-  mappend = (Semi.<>)
-
--- | Pattern check result
---
--- * Redundant clauses
--- * Not-covered clauses (or their type, if no pattern is available)
--- * Clauses with inaccessible RHS
--- * A flag saying whether we ran into the 'maxPmCheckModels' limit for the
---   purpose of suggesting to crank it up in the warning message
---
--- More details about the classification of clauses into useful, redundant
--- and with inaccessible right hand side can be found here:
---
---     https://gitlab.haskell.org/ghc/ghc/wikis/pattern-match-check
---
-data PmResult =
-  PmResult {
-      pmresultRedundant    :: [Located [LPat GhcTc]]
-    , pmresultUncovered    :: [Delta]
-    , pmresultInaccessible :: [Located [LPat GhcTc]]
-    , pmresultApproximate  :: Precision }
-
-instance Outputable PmResult where
-  ppr pmr = hang (text "PmResult") 2 $ vcat
-    [ text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
-    , text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
-    , text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
-    , text "pmresultApproximate" <+> ppr (pmresultApproximate pmr)
-    ]
+      (t, grds)                  = collect_grds g
+      collect_grds (Guard grd t) = (grd :) <$> collect_grds t
+      collect_grds t             = (t, [])
+      prefix []                  = []
+      prefix (s:sdocs)           = char '|' <+> s : map (comma <+>) sdocs
+  -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
+  ppr t@Sequence{}    = braces (space <> fsep (punctuate semi (collect_seqs t)) <> space)
+    where
+      collect_seqs (Sequence l r) = collect_seqs l ++ collect_seqs r
+      collect_seqs t              = [ppr t]
+  ppr Empty          = text "<empty case>"
+
+instance Outputable AnnotatedTree where
+  ppr (AccessibleRhs info)   = pprRhsInfo info
+  ppr (InaccessibleRhs info) = text "inaccessible" <+> pprRhsInfo info
+  ppr (MayDiverge t)         = text "div" <+> ppr t
+    -- Format nested Sequences in blocks "{ grds1; grds2; ... }"
+  ppr t@SequenceAnn{}        = braces (space <> fsep (punctuate semi (collect_seqs t)) <> space)
+    where
+      collect_seqs (SequenceAnn l r) = collect_seqs l ++ collect_seqs r
+      collect_seqs t                 = [ppr t]
+  ppr EmptyAnn               = text "<empty case>"
+
+newtype Deltas = MkDeltas (Bag Delta)
+
+instance Outputable Deltas where
+  ppr (MkDeltas deltas) = ppr deltas
+
+instance Semigroup Deltas where
+  MkDeltas l <> MkDeltas r = MkDeltas (l `unionBags` r)
+
+liftDeltasM :: Monad m => (Delta -> m (Maybe Delta)) -> Deltas -> m Deltas
+liftDeltasM f (MkDeltas ds) = MkDeltas . catBagMaybes <$> (traverse f ds)
+
+-- | Lift 'addPmCts' over 'Deltas'.
+addPmCtsDeltas :: Deltas -> PmCts -> DsM Deltas
+addPmCtsDeltas deltas cts = liftDeltasM (\d -> addPmCts d cts) deltas
+
+-- | 'addPmCtsDeltas' a single 'PmCt'.
+addPmCtDeltas :: Deltas -> PmCt -> DsM Deltas
+addPmCtDeltas deltas ct = addPmCtsDeltas deltas (unitBag ct)
+
+-- | Test if any of the 'Delta's is inhabited. Currently this is pure, because
+-- we preserve the invariant that there are no uninhabited 'Delta's. But that
+-- could change in the future, for example by implementing this function in
+-- terms of @notNull <$> provideEvidence 1 ds@.
+isInhabited :: Deltas -> DsM Bool
+isInhabited (MkDeltas ds) = pure (not (null ds))
+
+-- | Pattern-match check result
+data CheckResult
+  = CheckResult
+  { cr_clauses :: !AnnotatedTree
+  -- ^ Captures redundancy info for each clause in the original program.
+  --   (for -Woverlapping-patterns)
+  , cr_uncov   :: !Deltas
+  -- ^ The set of uncovered values falling out at the bottom.
+  --   (for -Wincomplete-patterns)
+  , cr_approx  :: !Precision
+  -- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
+  --   purpose of suggesting to crank it up in the warning message
+  }
+
+instance Outputable CheckResult where
+  ppr (CheckResult c unc pc)
+    = text "CheckResult" <+> ppr_precision pc <+> braces (fsep
+        [ field "clauses" c <> comma
+        , field "uncov" unc])
+    where
+      ppr_precision Precise     = empty
+      ppr_precision Approximate = text "(Approximate)"
+      field name value = text name <+> equals <+> ppr value
 
 {-
 %************************************************************************
@@ -257,32 +260,22 @@ instance Outputable PmResult where
 %************************************************************************
 -}
 
--- | Check a single pattern binding (let)
+-- | Check a single pattern binding (let) for exhaustiveness.
 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
-checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
+checkSingle dflags ctxt@(DsMatchContext kind locn) var p = do
   tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
-  res <- checkSingle' locn var p
-  dsPmWarn dflags ctxt [var] res
-
--- | Check a single pattern binding (let)
-checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
-checkSingle' locn var p = do
-  fam_insts <- dsGetFamInstEnvs
-  grds      <- translatePat fam_insts var p
-  missing   <- getPmDelta
-  tracePm "checkSingle': missing" (ppr missing)
-  PartialResult cs us ds pc <- pmCheck grds [] 1 missing
-  dflags <- getDynFlags
-  us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us
-  let plain = PmResult { pmresultRedundant    = []
-                       , pmresultUncovered    = us'
-                       , pmresultInaccessible = []
-                       , pmresultApproximate  = pc }
-  return $ case (cs,ds) of
-    (Covered   , _          ) -> plain                              -- useful
-    (NotCovered, NotDiverged) -> plain { pmresultRedundant = m    } -- redundant
-    (NotCovered, Diverged   ) -> plain { pmresultInaccessible = m } -- inaccessible rhs
-  where m = [L locn [L locn p]]
+  -- We only ever need to run this in a context where we need exhaustivity
+  -- warnings (so not in pattern guards or comprehensions, for example, because
+  -- they are perfectly fine to fail).
+  -- Omitting checking this flag emits redundancy warnings twice in obscure
+  -- cases like #17646.
+  when (exhaustive dflags kind) $ do
+    missing   <- MkDeltas . unitBag <$> getPmDelta
+    tracePm "checkSingle: missing" (ppr missing)
+    fam_insts <- dsGetFamInstEnvs
+    grd_tree  <- mkGrdTreeRhs (L locn $ ppr p) <$> translatePat fam_insts var p
+    res <- checkGrdTree grd_tree missing
+    dsPmWarn dflags ctxt [var] res
 
 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
 -- in @MultiIf@ expressions.
@@ -310,66 +303,18 @@ checkMatches dflags ctxt vars matches = do
                                , text "Matches:"])
                                2
                                (vcat (map ppr matches)))
-  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 = do
-  init_delta <- getPmDelta
+  init_deltas <- MkDeltas . unitBag <$> 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)]
-              , Uncovered
-              , [LMatch GhcTc (LHsExpr GhcTc)]
-              , Precision)
-    go []     missing = return ([], missing, [], Precise)
-    go (m:ms) missing = do
-      tracePm "checkMatches': go" (ppr m)
-      dflags             <- getDynFlags
-      fam_insts          <- dsGetFamInstEnvs
-      (clause, guards)   <- translateMatch fam_insts vars m
-      let limit                     = maxPmCheckModels dflags
-          n_siblings                = length missing
-          throttled_check delta     =
-            snd <$> throttle limit (pmCheck clause guards) n_siblings delta
-
-      r@(PartialResult cs missing' ds pc1) <- runMany throttled_check missing
-
-      tracePm "checkMatches': go: res" (ppr r)
-      (rs, final_u, is, pc2)  <- go ms missing'
-      return $ case (cs, ds) of
-        -- useful
-        (Covered,  _    )        -> (rs, final_u,    is, pc1 Semi.<> pc2)
-        -- redundant
-        (NotCovered, NotDiverged) -> (m:rs, final_u, is, pc1 Semi.<> pc2)
-        -- inaccessible
-        (NotCovered, Diverged )   -> (rs, final_u, m:is, pc1 Semi.<> pc2)
-
-    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
-    hsLMatchToLPats (L l (Match { m_pats = pats })) = L l pats
-    hsLMatchToLPats _                               = panic "checkMatches'"
-
-getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta]
-getNFirstUncovered _    0 _              = pure []
-getNFirstUncovered _    _ []             = pure []
-getNFirstUncovered vars n (delta:deltas) = do
-  front <- provideEvidence vars n delta
-  back <- getNFirstUncovered vars (n - length front) deltas
-  pure (front ++ back)
+    [] | [var] <- vars -> addPmCtDeltas init_deltas (PmNotBotCt var)
+    _                  -> pure init_deltas
+  tracePm "checkMatches: missing" (ppr missing)
+  fam_insts <- dsGetFamInstEnvs
+  grd_tree  <- mkGrdTreeMany [] <$> mapM (translateMatch fam_insts vars) matches
+  res <- checkGrdTree grd_tree missing
+
+  dsPmWarn dflags ctxt vars res
 
 {- Note [Checking EmptyCase]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -409,7 +354,7 @@ mkPmLetVar x y          = [PmLet x (Var y)]
 vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd
 vanillaConGrd scrut con arg_ids =
   PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con)
-        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids }
+        , pm_con_dicts = [], pm_con_args = arg_ids }
 
 -- | Creates a 'GrdVec' refining a match var of list type to a list,
 -- where list fields are matched against the incoming tagged 'GrdVec's.
@@ -417,7 +362,8 @@ vanillaConGrd scrut con arg_ids =
 --   @mkListGrds "a" "[(x, True <- x),(y, !y)]"@
 -- to
 --   @"[(x:b) <- a, True <- x, (y:c) <- b, seq y True, [] <- c]"@
--- where b,c are freshly allocated in @mkListGrds@ and a is the match variable.
+-- where @b@ and @c@ are freshly allocated in @mkListGrds@ and @a@ is the match
+-- variable.
 mkListGrds :: Id -> [(Id, GrdVec)] -> DsM GrdVec
 -- See Note [Order of guards matter] for why we need to intertwine guards
 -- on list elements.
@@ -432,9 +378,10 @@ mkPmLitGrds :: Id -> PmLit -> DsM GrdVec
 mkPmLitGrds x (PmLit _ (PmLitString s)) = do
   -- We translate String literals to list literals for better overlap reasoning.
   -- It's a little unfortunate we do this here rather than in
-  -- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much
-  -- simpler here.
-  -- See Note [Representation of Strings in TmState] in GHC.HsToCore.PmCheck.Oracle
+  -- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and
+  -- 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much simpler
+  -- here. See Note [Representation of Strings in TmState] in
+  -- GHC.HsToCore.PmCheck.Oracle
   vars <- traverse mkPmId (take (lengthFS s) (repeat charTy))
   let mk_char_lit y c = mkPmLitGrds y (PmLit charTy (PmLitChar c))
   char_grdss <- zipWithM mk_char_lit vars (unpackFS s)
@@ -442,7 +389,6 @@ mkPmLitGrds x (PmLit _ (PmLitString s)) = do
 mkPmLitGrds x lit = do
   let grd = PmCon { pm_id = x
                   , pm_con_con = PmAltLit lit
-                  , pm_con_tvs = []
                   , pm_con_dicts = []
                   , pm_con_args = [] }
   pure [grd]
@@ -639,7 +585,7 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
 
       -- 1. the constructor pattern match itself
       arg_ids <- zipWithM get_pat_id [0..] arg_tys
-      let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids
+      let con_grd = PmCon x (PmAltConLike con) dicts arg_ids
 
       -- 2. bang strict fields
       let arg_is_banged = map isBanged $ conLikeImplBangs con
@@ -654,30 +600,37 @@ translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case
       --      1.         2.           3.
       pure (con_grd : bang_grds ++ arg_grds)
 
+mkGrdTreeRhs :: Located SDoc -> GrdVec -> GrdTree
+mkGrdTreeRhs sdoc = foldr Guard (Rhs sdoc)
+
+mkGrdTreeMany :: GrdVec -> [GrdTree] -> GrdTree
+mkGrdTreeMany _    []    = Empty
+mkGrdTreeMany grds trees = foldr Guard (foldr1 Sequence trees) grds
+
 -- Translate a single match
 translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc)
-               -> DsM (GrdVec, [GrdVec])
-translateMatch fam_insts vars (L _ (Match { m_pats = pats, m_grhss = grhss }))
-  = do
-      pats'   <- concat <$> zipWithM (translateLPat fam_insts) vars pats
-      guards' <- mapM (translateGuards fam_insts) guards
-      -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards'])
-      return (pats', guards')
-      where
-        extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
-        extractGuards (L _ (GRHS _ gs _)) = map unLoc gs
-        extractGuards _                   = panic "translateMatch"
-
-        guards = map extractGuards (grhssGRHSs grhss)
-translateMatch _ _ _ = panic "translateMatch"
+               -> DsM GrdTree
+translateMatch fam_insts vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
+  pats'   <- concat <$> zipWithM (translateLPat fam_insts) vars pats
+  grhss' <- mapM (translateLGRHS fam_insts match_loc pats) (grhssGRHSs grhss)
+  -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr grhss, ppr grhss'])
+  return (mkGrdTreeMany pats' grhss')
+translateMatch _ _ (L _ (XMatch _)) = panic "translateMatch"
 
 -- -----------------------------------------------------------------------
 -- * Transform source guards (GuardStmt Id) to simpler PmGrds
 
--- | Translate a list of guard statements to a 'GrdVec'
-translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM GrdVec
-translateGuards fam_insts guards =
-  concat <$> mapM (translateGuard fam_insts) guards
+-- | Translate a guarded right-hand side to a single 'GrdTree'
+translateLGRHS :: FamInstEnvs -> SrcSpan -> [LPat GhcTc] -> LGRHS GhcTc (LHsExpr GhcTc) -> DsM GrdTree
+translateLGRHS fam_insts match_loc pats (L _loc (GRHS _ gs _)) =
+  -- _loc apparently points to the match separator that comes after the guards..
+  mkGrdTreeRhs loc_sdoc . concat <$> mapM (translateGuard fam_insts . unLoc) gs
+    where
+      loc_sdoc
+        | null gs   = L match_loc (sep (map ppr pats))
+        | otherwise = L grd_loc   (sep (map ppr pats) <+> vbar <+> interpp'SP gs)
+      L grd_loc _ = head gs
+translateLGRHS _ _ _ (L _ (XGRHS _)) = panic "translateLGRHS"
 
 -- | Translate a guard statement to a 'GrdVec'
 translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec
@@ -802,24 +755,12 @@ For exhaustivity, the converse applies: We will report @f@ as non-exhaustive
 and report @f _ _@ as missing, which is a superset of the actual missing
 matches. But soundness means we will never fail to report a missing match.
 
-This mechanism is implemented in the higher-order function 'throttle'.
-
-Note [Combinatorial explosion in guards]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Function with many clauses and deeply nested guards like in #11195 tend to
-overwhelm the checker because they lead to exponential splitting behavior.
-See the comments on #11195 on refinement trees. Every guard refines the
-disjunction of Deltas by another split. This no different than the ConVar case,
-but in stark contrast we mostly don't get any useful information out of that
-split! Hence splitting k-fold just means having k-fold more work. The problem
-exacerbates for larger k, because it gets even more unlikely that we can handle
-all of the arising Deltas better than just continue working on the original
-Delta.
-
-We simply apply the same mechanism as in Note [Countering exponential blowup].
-But we don't want to forget about actually useful info from pattern match
-clauses just because we had one clause with many guards. So we set the limit for
-guards much lower.
+This mechanism is implemented in 'throttle'.
+
+Guards are an extreme example in this regard, with #11195 being a particularly
+dreadful example: Since their RHS are often pretty much unique, we split on a
+variable (the one representing the RHS) that doesn't occur anywhere else in the
+program, so we don't actually get useful information out of that split!
 
 Note [Translate CoPats]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -938,182 +879,101 @@ brows.
 {-
 %************************************************************************
 %*                                                                      *
-            Heart of the algorithm: Function pmCheck
+            Heart of the algorithm: checkGrdTree
 %*                                                                      *
 %************************************************************************
-
-Main functions are:
-
-* pmCheck :: PatVec -> [PatVec] -> ValVec -> Delta -> DsM PartialResult
-
-  This function implements functions `covered`, `uncovered` and
-  `divergent` from the paper at once. Calls out to the auxiliary function
-  `pmCheckGuards` for handling (possibly multiple) guarded RHSs when the whole
-  clause is checked. Slightly different from the paper because it does not even
-  produce the covered and uncovered sets. Since we only care about whether a
-  clause covers SOMETHING or if it may forces ANY argument, we only store a
-  boolean in both cases, for efficiency.
-
-* pmCheckGuards :: [PatVec] -> ValVec -> Delta -> DsM PartialResult
-
-  Processes the guards.
 -}
 
--- | @throttle limit f n delta@ executes the pattern match action @f@ but
--- replaces the 'Uncovered' set by @[delta]@ if not doing so would lead to
--- too many Deltas to check.
---
--- See Note [Countering exponential blowup] and
--- Note [Combinatorial explosion in guards]
+-- | @throttle limit old new@ returns @old@ if the number of 'Delta's in @new@
+-- is exceeding the given @limit@ and the @old@ number of 'Delta's.
+-- See Note [Countering exponential blowup].
+throttle :: Int -> Deltas -> Deltas -> (Precision, Deltas)
+throttle limit old@(MkDeltas old_ds) new@(MkDeltas new_ds)
+  --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined
+  | length new_ds > max limit (length old_ds) = (Approximate, old)
+  | otherwise                                 = (Precise,     new)
+
+-- | Matching on a newtype doesn't force anything.
+-- See Note [Divergence of Newtype matches] in Oracle.
+conMatchForces :: PmAltCon -> Bool
+conMatchForces (PmAltConLike (RealDataCon dc))
+  | isNewTyCon (dataConTyCon dc) = False
+conMatchForces _                 = True
+
+-- | Makes sure that we only wrap a single 'MayDiverge' around an
+-- 'AnnotatedTree', purely for esthetic reasons.
+mayDiverge :: AnnotatedTree -> AnnotatedTree
+mayDiverge a@(MayDiverge _) = a
+mayDiverge a                = MayDiverge a
+
+-- | Computes two things:
 --
--- How many is "too many"? @throttle@ assumes that the pattern match action
--- will be executed against @n@ similar other Deltas, its "siblings". Now, by
--- observing the branching factor (i.e. the number of children) of executing
--- the action, we can estimate how many Deltas there would be in the next
--- generation. If we find that this number exceeds @limit@, we do
--- "birth control": We simply don't allow a branching factor of more than 1.
--- Otherwise we just return the singleton set of the original @delta@.
--- This amounts to forgetting about the refined facts we got from running the
--- action.
-throttle :: Int -> (Int -> Delta -> DsM PartialResult) -> Int -> Delta -> DsM (Int, PartialResult)
-throttle limit f n_siblings delta = do
-  res <- f n_siblings delta
-  let n_own_children = length (presultUncovered res)
-  let n_next_gen = n_siblings * n_own_children
-  -- Birth control!
-  if n_next_gen <= limit || n_own_children <= 1
-    then pure (n_next_gen, res)
-    else pure (n_siblings, res { presultUncovered = [delta], presultApprox = Approximate })
-
--- | Map a pattern matching action processing a single 'Delta' over a
--- 'Uncovered' set and return the combined 'PartialResult's.
-runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
-runMany f unc = mconcat <$> traverse f unc
-
--- | Print diagnostic info and actually call 'pmCheck''.
-pmCheck :: GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult
-pmCheck ps guards n delta = do
-  tracePm "pmCheck {" $ vcat [ ppr n <> colon
-                           , hang (text "patterns:") 2 (ppr ps)
-                           , hang (text "guards:") 2 (ppr guards)
-                           , ppr delta ]
-  res <- pmCheck' ps guards n delta
+--   * The set of uncovered values not matched by any of the clauses of the
+--     'GrdTree'. Note that 'PmCon' guards are the only way in which values
+--     fall through from one 'Many' branch to the next.
+--   * An 'AnnotatedTree' that contains divergence and inaccessibility info
+--     for all clauses. Will be fed to 'redundantAndInaccessibleRhss' for
+--     presenting redundant and proper innaccessible RHSs to the user.
+checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
+-- RHS: Check that it covers something and wrap Inaccessible if not
+checkGrdTree' (Rhs sdoc) deltas = do
+  is_covered <- isInhabited deltas
+  let clauses = if is_covered then AccessibleRhs sdoc else InaccessibleRhs sdoc
+  pure CheckResult
+    { cr_clauses = clauses
+    , cr_uncov   = MkDeltas emptyBag
+    , cr_approx  = Precise }
+-- let x = e: Refine with x ~ e
+checkGrdTree' (Guard (PmLet x e) tree) deltas = do
+  deltas' <- addPmCtDeltas deltas (PmCoreCt x e)
+  checkGrdTree' tree deltas'
+-- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
+checkGrdTree' (Guard (PmBang x) tree) deltas = do
+  has_diverged <- addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
+  deltas' <- addPmCtDeltas deltas (PmNotBotCt x)
+  res <- checkGrdTree' tree deltas'
+  pure res{ cr_clauses = applyWhen has_diverged mayDiverge (cr_clauses res) }
+-- Con: Diverge on x ~ ⊥, fall through on x /~ K and refine with x ~ K ys
+--      and type info
+checkGrdTree' (Guard (PmCon x con dicts args) tree) deltas = do
+  has_diverged <-
+    if conMatchForces con
+      then addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
+      else pure False
+  unc_this <- addPmCtDeltas deltas (PmNotConCt x con)
+  deltas' <- addPmCtsDeltas deltas $
+    listToBag (PmTyCt . evVarPred <$> dicts) `snocBag` PmConCt x con args
+  CheckResult tree' unc_inner prec <- checkGrdTree' tree deltas'
+  limit <- maxPmCheckModels <$> getDynFlags
+  let (prec', unc') = throttle limit deltas (unc_this Semi.<> unc_inner)
+  pure CheckResult
+    { cr_clauses = applyWhen has_diverged mayDiverge tree'
+    , cr_uncov = unc'
+    , cr_approx = prec Semi.<> prec' }
+-- Sequence: Thread residual uncovered sets from equation to equation
+checkGrdTree' (Sequence l r) unc_0 = do
+  CheckResult l' unc_1 prec_l <- checkGrdTree' l unc_0
+  CheckResult r' unc_2 prec_r <- checkGrdTree' r unc_1
+  pure CheckResult
+    { cr_clauses = SequenceAnn l' r'
+    , cr_uncov = unc_2
+    , cr_approx = prec_l Semi.<> prec_r }
+-- Empty: Fall through for all values
+checkGrdTree' Empty unc = do
+  pure CheckResult
+    { cr_clauses = EmptyAnn
+    , cr_uncov = unc
+    , cr_approx = Precise }
+
+-- | Print diagnostic info and actually call 'checkGrdTree''.
+checkGrdTree :: GrdTree -> Deltas -> DsM CheckResult
+checkGrdTree guards deltas = do
+  tracePm "checkGrdTree {" $ vcat [ ppr guards
+                                  , ppr deltas ]
+  res <- checkGrdTree' guards deltas
   tracePm "}:" (ppr res) -- braces are easier to match by tooling
   return res
 
--- | Lifts 'pmCheck' over a 'DsM (Maybe Delta)'.
-pmCheckM :: GrdVec -> [GrdVec] -> Int -> DsM (Maybe Delta) -> DsM PartialResult
-pmCheckM ps guards n m_mb_delta = m_mb_delta >>= \case
-  Nothing    -> pure mempty
-  Just delta -> pmCheck ps guards n delta
-
--- | Check the list of mutually exclusive guards
-pmCheckGuards :: [GrdVec] -> Int -> Delta -> DsM PartialResult
-pmCheckGuards []       _ delta = return (usimple delta)
-pmCheckGuards (gv:gvs) n delta = do
-  dflags <- getDynFlags
-  let limit = maxPmCheckModels dflags `div` 5
-  (n', PartialResult cs unc ds pc) <- throttle limit (pmCheck gv []) n delta
-  (PartialResult css uncs dss pcs) <- runMany (pmCheckGuards gvs n') unc
-  return $ PartialResult (cs `mappend` css)
-                         uncs
-                         (ds `mappend` dss)
-                         (pc `mappend` pcs)
-
--- | Matching function: Check simultaneously a clause (takes separately the
--- patterns and the list of guards) for exhaustiveness, redundancy and
--- inaccessibility.
-pmCheck'
-  :: GrdVec   -- ^ Patterns of the clause
-  -> [GrdVec] -- ^ (Possibly multiple) guards of the clause
-  -> Int      -- ^ Estimate on the number of similar 'Delta's to handle.
-              --   See 6. in Note [Countering exponential blowup]
-  -> Delta    -- ^ Oracle state giving meaning to the identifiers in the ValVec
-  -> DsM PartialResult
-pmCheck' [] guards n delta
-  | null guards = return $ mempty { presultCovered = Covered }
-  | otherwise   = pmCheckGuards guards n delta
-
--- let x = e: Add x ~ e to the oracle
-pmCheck' (PmLet { pm_id = x, pm_let_expr = e } : ps) guards n delta = do
-  tracePm "PmLet" (vcat [ppr x, ppr e])
-  -- x is fresh because it's bound by the let
-  delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e
-  pmCheck ps guards n delta'
-
--- Bang x: Add x /~ _|_ to the oracle
-pmCheck' (PmBang x : ps) guards n delta = do
-  tracePm "PmBang" (ppr x)
-  pr <- pmCheckM ps guards n (addTmCt delta (TmVarNonVoid x))
-  pure (forceIfCanDiverge delta x pr)
-
--- Con: Add x ~ K ys to the Covered set and x /~ K to the Uncovered set
-pmCheck' (p : ps) guards n delta
-  | PmCon{ pm_id = x, pm_con_con = con, pm_con_args = args
-         , pm_con_dicts = dicts } <- p = do
-  -- E.g   f (K p q) = <rhs>
-  --       <next equation>
-  -- Split delta into two refinements:
-  --    * one for <rhs>, binding x to (K p q)
-  --    * one for <next equation>, recording that x is /not/ (K _ _)
-
-  -- Stuff for <rhs>
-  pr_pos <- pmCheckM ps guards n (addPmConCts delta x con dicts args)
-
-  -- The var is forced regardless of whether @con@ was satisfiable
-  -- 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
-    Nothing     -> pure mempty
-    Just delta' -> pure (usimple delta')
-
-  tracePm "PmCon" (vcat [ppr p, ppr x, ppr pr_pos', ppr pr_neg])
-
-  -- Combine both into a single PartialResult
-  let pr = mkUnion pr_pos' pr_neg
-  pure pr
-
-addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM (Maybe Delta)
-addPmConCts delta x con dicts fields = runMaybeT $ do
-  delta_ty    <- MaybeT $ addTypeEvidence delta (listToBag dicts)
-  delta_tm_ty <- MaybeT $ addTmCt delta_ty (TmVarCon x con fields)
-  pure delta_tm_ty
-
--- ----------------------------------------------------------------------------
--- * Utilities for main checking
-
--- | Initialise with default values for covering and divergent information and
--- a singleton uncovered set.
-usimple :: Delta -> PartialResult
-usimple delta = mempty { presultUncovered = [delta] }
-
--- | Get the union of two covered, uncovered and divergent value set
--- abstractions. Since the covered and divergent sets are represented by a
--- boolean, union means computing the logical or (at least one of the two is
--- non-empty).
-
-mkUnion :: PartialResult -> PartialResult -> PartialResult
-mkUnion = mappend
-
--- | Set the divergent set to not empty
-forces :: PartialResult -> PartialResult
-forces pres = pres { presultDivergent = Diverged }
-
--- | Set the divergent set to non-empty if the variable has not been forced yet
-forceIfCanDiverge :: Delta -> Id -> PartialResult -> PartialResult
-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
 
@@ -1158,7 +1018,7 @@ locallyExtendPmDelta ext k = getPmDelta >>= ext >>= \case
 -- | Add in-scope type constraints
 addTyCsDs :: Bag EvVar -> DsM a -> DsM a
 addTyCsDs ev_vars =
-  locallyExtendPmDelta (\delta -> addTypeEvidence delta ev_vars)
+  locallyExtendPmDelta (\delta -> addPmCts delta (PmTyCt . evVarPred <$> ev_vars))
 
 -- | Add equalities for the scrutinee to the local 'DsM' environment when
 -- checking a case expression:
@@ -1169,9 +1029,15 @@ addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
 addScrutTmCs Nothing    _   k = k
 addScrutTmCs (Just scr) [x] k = do
   scr_e <- dsLExpr scr
-  locallyExtendPmDelta (\delta -> addVarCoreCt delta x scr_e) k
+  locallyExtendPmDelta (\delta -> addPmCts delta (unitBag (PmCoreCt x scr_e))) k
 addScrutTmCs _   _   _ = panic "addScrutTmCs: HsCase with more than one case binder"
 
+addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM (Maybe Delta)
+addPmConCts delta x con dicts fields = runMaybeT $ do
+  delta_ty    <- MaybeT $ addPmCts delta (listToBag (PmTyCt . evVarPred <$> dicts))
+  delta_tm_ty <- MaybeT $ addPmCts delta_ty (unitBag (PmConCt x con fields))
+  pure delta_tm_ty
+
 -- | Add equalities to the local 'DsM' environment when checking the RHS of a
 -- case expression:
 --     case e of x { p1 -> e1; ... pn -> en }
@@ -1197,7 +1063,7 @@ computeCovered :: GrdVec -> Delta -> DsM (Maybe Delta)
 -- ConVar case harder to understand.
 computeCovered [] delta = pure (Just delta)
 computeCovered (PmLet { pm_id = x, pm_let_expr = e } : ps) delta = do
-  delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e
+  delta' <- expectJust "x is fresh" <$> addPmCts delta (unitBag (PmCoreCt x e))
   computeCovered ps delta'
 computeCovered (PmBang{} : ps) delta = do
   computeCovered ps delta
@@ -1235,13 +1101,65 @@ needToRunPmCheck dflags origin
   | otherwise
   = notNull (filter (`wopt` dflags) allPmCheckWarnings)
 
+redundantAndInaccessibleRhss :: AnnotatedTree -> ([RhsInfo], [RhsInfo])
+redundantAndInaccessibleRhss tree = (fromOL ol_red, fromOL ol_inacc)
+  where
+    (_ol_acc, ol_inacc, ol_red) = go tree
+    -- | Collects RHSs which are
+    --    1. accessible
+    --    2. proper inaccessible (so we can't delete them)
+    --    3. hypothetically redundant (so not only inaccessible RHS, but we can
+    --       even safely delete the equation without altering semantics)
+    -- See Note [Determining inaccessible clauses]
+    go :: AnnotatedTree -> (OrdList RhsInfo, OrdList RhsInfo, OrdList RhsInfo)
+    go (AccessibleRhs info)   = (unitOL info, nilOL, nilOL)
+    go (InaccessibleRhs info) = (nilOL,       nilOL, unitOL info) -- presumably redundant
+    go (MayDiverge t)         = case go t of
+      -- See Note [Determining inaccessible clauses]
+      (acc, inacc, red)
+        | isNilOL acc && isNilOL inacc -> (nilOL, red, nilOL)
+      res                              -> res
+    go (SequenceAnn l r)      = go l Semi.<> go r
+    go EmptyAnn               = (nilOL,       nilOL, nilOL)
+
+{- Note [Determining inaccessible clauses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f _  True = ()
+  f () True = ()
+  f _  _    = ()
+Is f's second clause redundant? The perhaps surprising answer is, no, it isn't!
+@f (error "boom") False@ will force the error with clause 2, but will return
+() if it was deleted, so clearly not redundant. Yet for now combination of
+arguments we can ever reach clause 2's RHS, so we say it has inaccessible RHS
+(as opposed to being completely redundant).
+
+We detect an inaccessible RHS simply by pretending it's redundant, until we see
+that it's part of a sub-tree in the pattern match that forces some argument
+(which corresponds to wrapping the 'AnnotatedTree' in 'MayDiverge'). Then we
+turn all supposedly redundant RHSs into inaccessible ones.
+
+But as it turns out (@g@ from #17465) this is too conservative:
+  g () | False = ()
+       | otherwise = ()
+g's first clause has an inaccessible RHS, but it's also safe to delete. So it's
+redundant, really! But by just turning all redundant child clauses into
+inaccessible ones, we report the first clause as inaccessible.
+
+Clearly, it is enough if we say that we only degrade if *not all* of the child
+clauses are redundant. As long as there is at least one clause which we announce
+not to be redundant, the guard prefix responsible for the 'MayDiverge' will
+survive. Hence we check for that in 'redundantAndInaccessibleRhss'.
+-}
+
 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
-dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM ()
-dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result
+dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> CheckResult -> DsM ()
+dsPmWarn dflags ctx@(DsMatchContext kind loc) vars result
   = when (flag_i || flag_u) $ do
+      unc_examples <- getNFirstUncovered vars (maxPatterns + 1) uncovered
       let exists_r = flag_i && notNull redundant
           exists_i = flag_i && notNull inaccessible && not is_rec_upd
-          exists_u = flag_u && notNull uncovered
+          exists_u = flag_u && notNull unc_examples
           approx   = precision == Approximate
 
       when (approx && (exists_u || exists_i)) $
@@ -1253,14 +1171,15 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result
       when exists_i $ forM_ inaccessible $ \(L l q) -> do
         putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
                                (pprEqn q "has inaccessible right hand side"))
+
       when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
-        pprEqns vars uncovered
+        pprEqns vars unc_examples
   where
-    PmResult
-      { pmresultRedundant = redundant
-      , pmresultUncovered = uncovered
-      , pmresultInaccessible = inaccessible
-      , pmresultApproximate = precision } = pm_result
+    CheckResult
+      { cr_clauses = clauses
+      , cr_uncov   = uncovered
+      , cr_approx  = precision } = result
+    (redundant, inaccessible) = redundantAndInaccessibleRhss clauses
 
     flag_i = wopt Opt_WarnOverlappingPatterns dflags
     flag_u = exhaustive dflags kind
@@ -1273,7 +1192,7 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result
 
     -- Print a single clause (for redundant/with-inaccessible-rhs)
     pprEqn q txt = pprContext True ctx (text txt) $ \f ->
-      f (pprPats kind (map unLoc q))
+      f (q <+> matchSeparator kind <+> text "...")
 
     -- Print several clauses (for uncovered clauses)
     pprEqns vars deltas = pprContext False ctx (text "are non-exhaustive") $ \_ ->
@@ -1294,6 +1213,16 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result
           $$ bullet <+> text "Patterns reported as unmatched might actually be matched")
       , text "Increase the limit or resolve the warnings to suppress this message." ]
 
+getNFirstUncovered :: [Id] -> Int -> Deltas -> DsM [Delta]
+getNFirstUncovered vars n (MkDeltas deltas) = go n (bagToList deltas)
+  where
+    go 0 _              = pure []
+    go _ []             = pure []
+    go n (delta:deltas) = do
+      front <- provideEvidence vars n delta
+      back <- go (n - length front) deltas
+      pure (front ++ back)
+
 {- Note [Inaccessible warnings for record updates]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider (#12957)
@@ -1369,7 +1298,3 @@ pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
              FunRhs { mc_fun = L _ fun }
                   -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
              _    -> (pprMatchContext kind, \ pp -> pp)
-
-pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
-pprPats kind pats
-  = sep [sep (map ppr pats), matchSeparator kind, text "..."]
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index f5e2293155..3f135b6664 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -7,21 +7,20 @@ Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
 {-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-}
 
 -- | 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 'provideEvidence' to turn a
+-- 'addPmCts' for 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, lookupRefuts, lookupSolution,
 
-        TmCt(..),
-        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
+        PmCt(PmTyCt), PmCts, pattern PmVarCt, pattern PmCoreCt,
+        pattern PmConCt, pattern PmNotConCt, pattern PmBotCt,
+        pattern PmNotBotCt,
+
+        addPmCts,           -- Add a constraint to the oracle.
         canDiverge,         -- Try to add the term equality x ~ ⊥
-        provideEvidence,
+        provideEvidence
     ) where
 
 #include "HsVersions.h"
@@ -63,7 +62,6 @@ import TysPrim (tYPETyCon)
 import TyCoRep
 import Type
 import TcSimplify    (tcNormalise, tcCheckSatisfiability)
-import TcType        (evVarPred)
 import Unify         (tcMatchTy)
 import TcRnTypes     (completeMatchConLikes)
 import Coercion
@@ -76,7 +74,8 @@ 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, minimumBy)
+import Data.Either   (partitionEithers)
+import Data.Foldable (foldlM, minimumBy, toList)
 import Data.List     (find)
 import qualified Data.List.NonEmpty as NonEmpty
 import Data.Ord      (comparing)
@@ -150,7 +149,7 @@ mkOneConFull arg_tys con = do
   vars <- mapM mkPmId field_tys'
   -- All constraints bound by the constructor (alpha-renamed), these are added
   -- to the type oracle
-  let ty_cs = map TyCt (substTheta subst (eqSpecPreds eq_spec ++ thetas))
+  let ty_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
   -- Figure out the types of strict constructor fields
   let arg_is_strict
         | RealDataCon dc <- con
@@ -233,14 +232,14 @@ instance Monoid SatisfiabilityCheck where
 pmIsSatisfiable
   :: Delta       -- ^ The ambient term and type constraints
                  --   (known to be satisfiable).
-  -> Bag TmCt    -- ^ The new term constraints.
   -> Bag TyCt    -- ^ The new type constraints.
+  -> Bag TmCt    -- ^ The new term constraints.
   -> [Type]      -- ^ The strict argument types.
   -> DsM (Maybe Delta)
                  -- ^ @'Just' delta@ if the constraints (@delta@) are
                  -- satisfiable, and each strict argument type is inhabitable.
                  -- 'Nothing' otherwise.
-pmIsSatisfiable amb_cs new_tm_cs new_ty_cs strict_arg_tys =
+pmIsSatisfiable amb_cs new_ty_cs new_tm_cs strict_arg_tys =
   -- The order is important here! Check the new type constraints before we check
   -- whether strict argument types are inhabited given those constraints.
   runSatisfiabilityCheck amb_cs $ mconcat
@@ -495,16 +494,9 @@ equalities (such as i ~ Int) that may be in scope.
 ----------------
 -- * Type oracle
 
--- | Wraps a 'PredType', which is a constraint type.
-newtype TyCt = TyCt PredType
-
-instance Outputable TyCt where
-  ppr (TyCt pred_ty) = ppr pred_ty
-
--- | Allocates a fresh 'EvVar' name for 'PredTyCt's, or simply returns the
--- wrapped 'EvVar' for 'EvVarTyCt's.
-nameTyCt :: TyCt -> DsM EvVar
-nameTyCt (TyCt pred_ty) = do
+-- | Allocates a fresh 'EvVar' name for 'PredTy's.
+nameTyCt :: PredType -> DsM EvVar
+nameTyCt pred_ty = do
   unique <- getUniqueM
   let occname = mkVarOccFS (fsLit ("pm_"++show unique))
       idname  = mkInternalName unique occname noSrcSpan
@@ -512,15 +504,13 @@ nameTyCt (TyCt pred_ty) = do
 
 -- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
 -- find a contradiction (e.g. @Int ~ Bool@).
-tyOracle :: TyState -> Bag TyCt -> DsM (Maybe TyState)
+tyOracle :: TyState -> Bag PredType -> 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
-            -- that we don't needlessly re-allocate them every time!
             Just True  -> return (Just (TySt new_inert))
             Just False -> return Nothing
             Nothing    -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
@@ -530,7 +520,7 @@ tyOracle (TySt inert) cts
 -- ones. Doesn't bother calling out to the type oracle if the bag of new type
 -- 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 :: Bool -> Bag PredType -> SatisfiabilityCheck
 tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta ->
   if isEmptyBag new_ty_cs
     then pure (Just delta)
@@ -658,9 +648,7 @@ warning messages (which can be alleviated by someone with enough dedication).
 -- Returns a new 'Delta' if the new constraints are compatible with existing
 -- ones.
 tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
-tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM go delta new_tm_cs
-  where
-    go delta ct = MaybeT (addTmCt delta ct)
+tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM addTmCt delta new_tm_cs
 
 -----------------------
 -- * Looking up VarInfo
@@ -789,8 +777,8 @@ This distinction becomes apparent in #17248:
 
 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.
+1. When compiling the PmCon guard in 'pmCompileTree', don't add a @DivergeIf@,
+   because the match will never diverge.
 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.
@@ -823,36 +811,101 @@ lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
 -------------------------------
 -- * Adding facts to the oracle
 
--- | A term constraint. Either equates two variables or a variable with a
--- 'PmAltCon' application.
+-- | A term constraint.
 data TmCt
-  = TmVarVar     !Id !Id
-  | TmVarCon     !Id !PmAltCon ![Id]
-  | TmVarNonVoid !Id
+  = TmVarCt     !Id !Id
+  -- ^ @TmVarCt x y@ encodes "x ~ y", equating @x@ and @y@.
+  | TmCoreCt    !Id !CoreExpr
+  -- ^ @TmCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@.
+  | TmConCt     !Id !PmAltCon ![Id]
+  -- ^ @TmConCt x K ys@ encodes "x ~ K ys", equating @x@ with the 'PmAltCon'
+  -- application @K ys@.
+  | TmNotConCt  !Id !PmAltCon
+  -- ^ @TmNotConCt x K@ encodes "x /~ K", asserting that @x@ can't be headed
+  -- by @K@.
+  | TmBotCt     !Id
+  -- ^ @TmBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
+  -- by @K@.
+  | TmNotBotCt !Id
+  -- ^ @TmNotBotCt x y@ encodes "x /~ ⊥", asserting that @x@ can't be ⊥.
 
 instance Outputable TmCt where
-  ppr (TmVarVar x y)        = ppr x <+> char '~' <+> ppr y
-  ppr (TmVarCon x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args)
-  ppr (TmVarNonVoid x)      = ppr x <+> text "/~ ⊥"
-
--- | Add type equalities to 'Delta'.
-addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
-addTypeEvidence delta dicts
-  = runSatisfiabilityCheck delta (tyIsSatisfiable True (TyCt . evVarPred <$> dicts))
-
--- | Tries to equate two representatives in 'Delta'.
+  ppr (TmVarCt x y)        = ppr x <+> char '~' <+> ppr y
+  ppr (TmCoreCt x e)       = ppr x <+> char '~' <+> ppr e
+  ppr (TmConCt x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args)
+  ppr (TmNotConCt x con)   = ppr x <+> text "/~" <+> ppr con
+  ppr (TmBotCt x)          = ppr x <+> text "~ ⊥"
+  ppr (TmNotBotCt x)       = ppr x <+> text "/~ ⊥"
+
+type TyCt = PredType
+
+-- | An oracle constraint.
+data PmCt
+  = PmTyCt !TyCt
+  -- ^ @PmTy pred_ty@ carries 'PredType's, for example equality constraints.
+  | PmTmCt !TmCt
+  -- ^ A term constraint.
+
+type PmCts = Bag PmCt
+
+pattern PmVarCt :: Id -> Id -> PmCt
+pattern PmVarCt x y         = PmTmCt (TmVarCt x y)
+pattern PmCoreCt :: Id -> CoreExpr -> PmCt
+pattern PmCoreCt x e        = PmTmCt (TmCoreCt x e)
+pattern PmConCt :: Id -> PmAltCon -> [Id] -> PmCt
+pattern PmConCt x con args  = PmTmCt (TmConCt x con args)
+pattern PmNotConCt :: Id -> PmAltCon -> PmCt
+pattern PmNotConCt x con    = PmTmCt (TmNotConCt x con)
+pattern PmBotCt :: Id -> PmCt
+pattern PmBotCt x           = PmTmCt (TmBotCt x)
+pattern PmNotBotCt :: Id -> PmCt
+pattern PmNotBotCt x        = PmTmCt (TmNotBotCt x)
+{-# COMPLETE PmTyCt, PmVarCt, PmCoreCt, PmConCt, PmNotConCt, PmBotCt, PmNotBotCt #-}
+
+instance Outputable PmCt where
+  ppr (PmTyCt pred_ty) = ppr pred_ty
+  ppr (PmTmCt tm_ct)   = ppr tm_ct
+
+-- | Adds new constraints to 'Delta' and returns 'Nothing' if that leads to a
+-- contradiction.
+addPmCts :: Delta -> PmCts -> DsM (Maybe Delta)
 -- See Note [TmState invariants].
-addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
-addTmCt delta ct = runMaybeT $ case ct of
-  TmVarVar x y        -> addVarVarCt delta (x, y)
-  TmVarCon x con args -> addVarConCt delta x con args
-  TmVarNonVoid x      -> addVarNonVoidCt delta x
+addPmCts delta cts = do
+  let (ty_cts, tm_cts) = partitionTyTmCts cts
+  runSatisfiabilityCheck delta $ mconcat
+    [ tyIsSatisfiable True (listToBag ty_cts)
+    , tmIsSatisfiable (listToBag tm_cts)
+    ]
+
+partitionTyTmCts :: PmCts -> ([TyCt], [TmCt])
+partitionTyTmCts = partitionEithers . map to_either . toList
+  where
+    to_either (PmTyCt pred_ty) = Left pred_ty
+    to_either (PmTmCt tm_ct)   = Right tm_ct
+
+-- | Adds a single term constraint by dispatching to the various term oracle
+-- functions.
+addTmCt :: Delta -> TmCt -> MaybeT DsM Delta
+addTmCt delta (TmVarCt x y)        = addVarVarCt delta (x, y)
+addTmCt delta (TmCoreCt x e)       = addVarCoreCt delta x e
+addTmCt delta (TmConCt x con args) = addVarConCt delta x con args
+addTmCt delta (TmNotConCt x con)   = addRefutableAltCon delta x con
+addTmCt delta (TmBotCt x)          = addVarBotCt delta x
+addTmCt delta (TmNotBotCt x)       = addVarNonVoidCt delta x
+
+-- | In some future this will actually add a constraint to 'Delta' that we plan
+-- to preserve. But for now, we just check if we can add the constraint to the
+-- current 'Delta'. If so, we return the original 'Delta', if not, we fail.
+addVarBotCt :: Delta -> Id -> MaybeT DsM Delta
+addVarBotCt delta x
+  | canDiverge delta x = pure delta
+  | otherwise          = mzero
 
 -- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the
 -- 'Delta' and return @Nothing@ if that leads to a contradiction.
 -- See Note [TmState invariants].
-addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
-addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = runMaybeT $ do
+addRefutableAltCon :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta
+addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = do
   vi@(VI _ pos neg pm) <- lift (initLookupVarInfo delta x)
   -- 1. Bail out quickly when nalt contradicts a solution
   let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal
@@ -1052,7 +1105,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y
         let add_fact delta (cl, args) = addVarConCt delta y cl args
         delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x)
         -- Do the same for negative info
-        let add_refut delta nalt = MaybeT (addRefutableAltCon delta y nalt)
+        let add_refut delta nalt = addRefutableAltCon delta y nalt
         delta_neg <- foldlM add_refut delta_pos (vi_neg vi_x)
         -- vi_cache will be updated in addRefutableAltCon, so we are good to
         -- go!
@@ -1095,16 +1148,14 @@ addVarConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt args = do
 -- See @Note [Strict argument type constraints]@.
 data InhabitationCandidate =
   InhabitationCandidate
-  { ic_tm_cs          :: Bag TmCt
-  , ic_ty_cs          :: Bag TyCt
+  { ic_cs             :: PmCts
   , ic_strict_arg_tys :: [Type]
   }
 
 instance Outputable InhabitationCandidate where
-  ppr (InhabitationCandidate tm_cs ty_cs strict_arg_tys) =
+  ppr (InhabitationCandidate cs strict_arg_tys) =
     text "InhabitationCandidate" <+>
-      vcat [ text "ic_tm_cs          =" <+> ppr tm_cs
-           , text "ic_ty_cs          =" <+> ppr ty_cs
+      vcat [ text "ic_cs             =" <+> ppr cs
            , text "ic_strict_arg_tys =" <+> ppr strict_arg_tys ]
 
 mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
@@ -1114,8 +1165,7 @@ mkInhabitationCandidate x dc = do
   let tc_args = tyConAppArgs (idType x)
   (arg_vars, ty_cs, strict_arg_tys) <- mkOneConFull tc_args cl
   pure InhabitationCandidate
-        { ic_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
-        , ic_ty_cs = ty_cs
+        { ic_cs = PmTyCt <$> ty_cs `snocBag` PmConCt x (PmAltConLike cl) arg_vars
         , ic_strict_arg_tys = strict_arg_tys
         }
 
@@ -1133,13 +1183,13 @@ 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
-    build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, TmCt)
+    build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, PmCt)
     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])
+      pure (y, PmConCt y (PmAltConLike (RealDataCon dc)) [x])
 
-    build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
+    build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
     build_newtypes x = foldrM (\dc (x, cts) -> go dc x cts) (x, [])
       where
         go dc x cts = second (:cts) <$> build_newtype dc x
@@ -1155,8 +1205,8 @@ inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do
              (_:_) -> do inner <- mkPmId core_ty
                          (outer, new_tm_cts) <- build_newtypes inner dcs
                          return $ Right (tc, outer, [InhabitationCandidate
-                           { ic_tm_cs = listToBag new_tm_cts
-                           , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }])
+                           { ic_cs = listToBag new_tm_cts
+                           , ic_strict_arg_tys = [] }])
 
         |  pmIsClosedType core_ty && not (isAbstractTyCon tc)
            -- Don't consider abstract tycons since we don't know what their
@@ -1165,8 +1215,8 @@ inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do
         -> do
              inner <- mkPmId core_ty -- it would be wrong to unify inner
              alts <- mapM (mkInhabitationCandidate inner) (tyConDataCons tc)
-             (outer, new_tm_cts) <- build_newtypes inner dcs
-             let wrap_dcs alt = alt{ ic_tm_cs = listToBag new_tm_cts `unionBags` ic_tm_cs alt}
+             (outer, new_cts) <- build_newtypes inner dcs
+             let wrap_dcs alt = alt{ ic_cs = listToBag new_cts `unionBags` ic_cs alt}
              return $ Right (tc, outer, map wrap_dcs alts)
       -- For other types conservatively assume that they are inhabited.
       _other -> return (Left src_ty)
@@ -1278,12 +1328,12 @@ nonVoid rec_ts amb_cs strict_arg_ty = do
     cand_is_inhabitable :: RecTcChecker -> Delta
                         -> InhabitationCandidate -> DsM Bool
     cand_is_inhabitable rec_ts amb_cs
-      (InhabitationCandidate{ ic_tm_cs          = new_tm_cs
-                            , ic_ty_cs          = new_ty_cs
-                            , ic_strict_arg_tys = new_strict_arg_tys }) =
+      (InhabitationCandidate{ ic_cs             = new_cs
+                            , ic_strict_arg_tys = new_strict_arg_tys }) = do
+        let (new_ty_cs, new_tm_cs) = partitionTyTmCts new_cs
         fmap isJust $ runSatisfiabilityCheck amb_cs $ mconcat
-          [ tyIsSatisfiable False new_ty_cs
-          , tmIsSatisfiable new_tm_cs
+          [ tyIsSatisfiable False (listToBag new_ty_cs)
+          , tmIsSatisfiable (listToBag new_tm_cs)
           , tysAreNonVoid rec_ts new_strict_arg_tys
           ]
 
@@ -1504,9 +1554,9 @@ provideEvidence = go
         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)
+          let new_tm_cs = unitBag (TmConCt x (PmAltConLike cl) arg_vars)
           -- Now check satifiability
-          mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys
+          mb_delta <- pmIsSatisfiable delta new_ty_cs new_tm_cs strict_arg_tys
           tracePm "instantiate_cons" (vcat [ ppr x
                                            , ppr (idType x)
                                            , ppr ty
@@ -1538,14 +1588,11 @@ pickMinimalCompleteSet _ (PM clss) = do
 -- | See if we already encountered a semantically equivalent expression and
 -- return its representative.
 representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id)
-representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e = do
-  dflags <- getDynFlags
-  let e' = simpleOptExpr dflags e
-  case lookupCoreMap reps e' of
-    Just rep -> pure (delta, rep)
-    Nothing  -> do
-      rep <- mkPmId (exprType e')
-      let reps'  = extendCoreMap reps e' rep
+representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e
+  | Just rep <- lookupCoreMap reps e = pure (delta, rep)
+  | otherwise = do
+      rep <- mkPmId (exprType e)
+      let reps'  = extendCoreMap reps e rep
       let delta' = delta{ delta_tm_st = ts{ ts_reps = reps' } }
       pure (delta', rep)
 
@@ -1554,8 +1601,12 @@ representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e = d
 -- type PmM a = StateT Delta (MaybeT DsM) a
 
 -- | Records that a variable @x@ is equal to a 'CoreExpr' @e@.
-addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta)
-addVarCoreCt delta x e = runMaybeT (execStateT (core_expr x e) delta)
+addVarCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
+addVarCoreCt delta x e = do
+  dflags <- getDynFlags
+  let e' = simpleOptExpr dflags e
+  lift $ tracePm "addVarCoreCt" (ppr x $$ ppr e $$ ppr e')
+  execStateT (core_expr x e') delta
   where
     -- | Takes apart a 'CoreExpr' and tries to extract as much information about
     -- literals and constructor applications as possible.
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index 10f172a430..e5b9bcf0ef 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -531,7 +531,7 @@ initDelta :: Delta
 initDelta = MkDelta initTyState initTmState
 
 instance Outputable Delta where
-  ppr delta = vcat [
+  ppr delta = hang (text "Delta") 2 $ vcat [
       -- intentionally formatted this way enable the dev to comment in only
       -- the info she needs
       ppr (delta_tm_st delta),
diff --git a/compiler/basicTypes/Demand.hs b/compiler/basicTypes/Demand.hs
index 2ac18a4393..b64663b970 100644
--- a/compiler/basicTypes/Demand.hs
+++ b/compiler/basicTypes/Demand.hs
@@ -700,7 +700,7 @@ cleanEvalProdDmd n = JD { sd = HeadStr, ud = UProd (replicate n useTop) }
 {-
 ************************************************************************
 *                                                                      *
-           Demand: combining strictness and usage
+           Demand: Combining Strictness and Usage
 *                                                                      *
 ************************************************************************
 -}
diff --git a/compiler/ghci/Linker.hs b/compiler/ghci/Linker.hs
index ec717d7399..cf4ef8bf28 100644
--- a/compiler/ghci/Linker.hs
+++ b/compiler/ghci/Linker.hs
@@ -1139,7 +1139,8 @@ unload_wkr hsc_env keep_linkables pls@PersistentLinkerState{..}  = do
 
       -- Code unloading currently disabled due to instability.
       -- See #16841.
-      | False -- otherwise
+      -- id False, so that the pattern-match checker doesn't complain
+      | id False -- otherwise
       = mapM_ (unloadObj hsc_env) [f | DotO f <- linkableUnlinked lnk]
                 -- The components of a BCO linkable may contain
                 -- dot-o files.  Which is very confusing.
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 3662b9c33f..61f83c6437 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -1340,12 +1340,15 @@ parseCfgWeights s oldWeights =
             = [s1]
             | (s1,rest) <- break (== ',') s
             = [s1] ++ settings (drop 1 rest)
+#if __GLASGOW_HASKELL__ <= 810
             | otherwise = panic $ "Invalid cfg parameters." ++ exampleString
+#endif
         assignment as
             | (name, _:val) <- break (== '=') as
             = (name,read val)
             | otherwise
             = panic $ "Invalid cfg parameters." ++ exampleString
+
         exampleString = "Example parameters: uncondWeight=1000," ++
             "condBranchWeight=800,switchWeight=0,callWeight=300" ++
             ",likelyCondWeight=900,unlikelyCondWeight=300" ++
@@ -1952,7 +1955,7 @@ defaultDynFlags mySettings llvmConfig =
         maxRefHoleFits     = Just 6,
         refLevelHoleFits   = Nothing,
         maxUncoveredPatterns    = 4,
-        maxPmCheckModels        = 100,
+        maxPmCheckModels        = 30,
         simplTickFactor         = 100,
         specConstrThreshold     = Just 2000,
         specConstrCount         = Just 3,
diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs
index b97360bab9..5d67a9a39c 100644
--- a/compiler/main/InteractiveEval.hs
+++ b/compiler/main/InteractiveEval.hs
@@ -385,8 +385,10 @@ handleRunStatus step expr bindings final_ids status history
     | EvalComplete alloc (EvalException e) <- status
     = return (ExecComplete (Left (fromSerializableException e)) alloc)
 
+#if __GLASGOW_HASKELL__ <= 810
     | otherwise
     = panic "not_tracing" -- actually exhaustive, but GHC can't tell
+#endif
 
 
 resumeExec :: GhcMonad m => (SrcSpan->Bool) -> SingleStep -> m ExecResult
diff --git a/compiler/nativeGen/BlockLayout.hs b/compiler/nativeGen/BlockLayout.hs
index f0e98cda75..5e81316ab3 100644
--- a/compiler/nativeGen/BlockLayout.hs
+++ b/compiler/nativeGen/BlockLayout.hs
@@ -718,8 +718,10 @@ sequenceChain  info weights'     blocks@((BasicBlock entry _):_) =
             = [masterChain]
             | (rest,entry) <- breakChainAt entry masterChain
             = [entry,rest]
+#if __GLASGOW_HASKELL__ <= 810
             | otherwise = pprPanic "Entry point eliminated" $
                             ppr masterChain
+#endif
 
         blockList
             = ASSERT(noDups [masterChain])
diff --git a/compiler/nativeGen/RegAlloc/Graph/Main.hs b/compiler/nativeGen/RegAlloc/Graph/Main.hs
index 1171689e66..177a73bf81 100644
--- a/compiler/nativeGen/RegAlloc/Graph/Main.hs
+++ b/compiler/nativeGen/RegAlloc/Graph/Main.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 -- | Graph coloring register allocator.
@@ -376,8 +377,10 @@ graphAddCoalesce (r1, r2) graph
         , RegReal _             <- r2
         = graph
 
+#if __GLASGOW_HASKELL__ <= 810
         | otherwise
         = panic "graphAddCoalesce"
+#endif
 
 
 -- | Patch registers in code using the reg -> reg mapping in this graph.
diff --git a/compiler/nativeGen/RegAlloc/Graph/SpillClean.hs b/compiler/nativeGen/RegAlloc/Graph/SpillClean.hs
index 6d7b377d68..79dbf63a66 100644
--- a/compiler/nativeGen/RegAlloc/Graph/SpillClean.hs
+++ b/compiler/nativeGen/RegAlloc/Graph/SpillClean.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 
 -- | Clean out unneeded spill\/reload instructions.
 --
@@ -393,9 +394,11 @@ cleanBackward' liveSlotsOnEntry reloadedBy noReloads acc (li : instrs)
 
                 cleanBackward liveSlotsOnEntry noReloads' (li : acc) instrs
 
+#if __GLASGOW_HASKELL__ <= 810
         -- some other instruction
         | otherwise
         = cleanBackward liveSlotsOnEntry noReloads (li : acc) instrs
+#endif
 
 
 -- | Combine the associations from all the inward control flow edges.
@@ -611,4 +614,3 @@ closeAssoc a assoc
 intersectAssoc :: Assoc a -> Assoc a -> Assoc a
 intersectAssoc a b
         = intersectUFM_C (intersectUniqSets) a b
-
diff --git a/compiler/nativeGen/RegAlloc/Linear/SPARC/FreeRegs.hs b/compiler/nativeGen/RegAlloc/Linear/SPARC/FreeRegs.hs
index 5df329359d..fc67159f0f 100644
--- a/compiler/nativeGen/RegAlloc/Linear/SPARC/FreeRegs.hs
+++ b/compiler/nativeGen/RegAlloc/Linear/SPARC/FreeRegs.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 
 -- | Free regs map for SPARC
 module RegAlloc.Linear.SPARC.FreeRegs
@@ -55,7 +56,9 @@ getFreeRegs cls (FreeRegs g f d)
         | RcInteger <- cls = map RealRegSingle                  $ go 1 g 1 0
         | RcFloat   <- cls = map RealRegSingle                  $ go 1 f 1 32
         | RcDouble  <- cls = map (\i -> RealRegPair i (i+1))    $ go 2 d 1 32
+#if __GLASGOW_HASKELL__ <= 810
         | otherwise = pprPanic "RegAllocLinear.getFreeRegs: Bad register class " (ppr cls)
+#endif
         where
                 go _    _      0    _
                         = []
@@ -184,4 +187,3 @@ showFreeRegs regs
         ++ "    integer: " ++ (show $ getFreeRegs RcInteger regs)       ++ "\n"
         ++ "      float: " ++ (show $ getFreeRegs RcFloat   regs)       ++ "\n"
         ++ "     double: " ++ (show $ getFreeRegs RcDouble  regs)       ++ "\n"
-
diff --git a/compiler/simplCore/SimplCore.hs b/compiler/simplCore/SimplCore.hs
index 1d55c17d36..b8fb162432 100644
--- a/compiler/simplCore/SimplCore.hs
+++ b/compiler/simplCore/SimplCore.hs
@@ -743,7 +743,9 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
                 -- Loop
            do_iteration us2 (iteration_no + 1) (counts1:counts_so_far) binds2 rules1
            } }
+#if __GLASGOW_HASKELL__ <= 810
       | otherwise = panic "do_iteration"
+#endif
       where
         (us1, us2) = splitUniqSupply us
 
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index a53cdac72e..b1a0820e66 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -2370,8 +2370,10 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
        ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
        ; return new_ev }
 
+#if __GLASGOW_HASKELL__ <= 810
   | otherwise
   = panic "rewriteEvidence"
+#endif
   where
     new_pred = mkTcEqPredLikeEv old_ev nlhs nrhs
 
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 06733d8f4d..45147cd048 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -853,7 +853,9 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name
        ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
        ; return builder_binds } } }
 
+#if __GLASGOW_HASKELL__ <= 810
   | otherwise = panic "tcPatSynBuilderBind"  -- Both cases dealt with
+#endif
   where
     mb_match_group
        = case dir of
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 9df6b3cda4..c4afb5d891 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -735,7 +735,9 @@ checkHiBootIface tcg_env boot_info
              -- TODO: Maybe setGlobalTypeEnv should be strict.
           setGlobalTypeEnv tcg_env_w_binds type_env' }
 
+#if __GLASGOW_HASKELL__ <= 810
   | otherwise = panic "checkHiBootIface: unreachable code"
+#endif
 
 {- Note [DFun impedance matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index d4cc7eea71..6b49eeda68 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2174,7 +2174,9 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
          -- overlap done by dropDominatedAxioms
        ; return fam_tc } }
 
+#if __GLASGOW_HASKELL__ <= 810
   | otherwise = panic "tcFamInst1"  -- Silence pattern-exhaustiveness checker
+#endif
 tcFamDecl1 _ (XFamilyDecl nec) = noExtCon nec
 
 -- | Maybe return a list of Bools that say whether a type family was declared