PmCheck: Only ever check constantly many models against a single pattern

Introduces a new flag `-fmax-pmcheck-deltas` to achieve that. Deprecates
the old `-fmax-pmcheck-iter` mechanism in favor of this new flag.

From the user's guide:

Pattern match checking can be exponential in some cases. This limit makes sure
we scale polynomially in the number of patterns, by forgetting refined
information gained from a partially successful match. For example, when
matching `x` against `Just 4`, we split each incoming matching model into two
sub-models: One where `x` is not `Nothing` and one where `x` is `Just y` but
`y` is not `4`. When the number of incoming models exceeds the limit, we
continue checking the next clause with the original, unrefined model.

This also retires the incredibly hard to understand "maximum number of
refinements" mechanism, because the current mechanism is more general
and should catch the same exponential cases like PrelRules at the same
time.

-------------------------
Metric Decrease:
    T11822
-------------------------

16 files changed, 278 insertions, 274 deletions

diff --git a/compiler/GHC/StgToCmm/Prim.hs b/compiler/GHC/StgToCmm/Prim.hs
index dc69a51916..81848c9427 100644
--- a/compiler/GHC/StgToCmm/Prim.hs
+++ b/compiler/GHC/StgToCmm/Prim.hs
@@ -1,6 +1,10 @@
 {-# LANGUAGE CPP #-}
+
+#if __GLASGOW_HASKELL__ <= 808
+-- GHC 8.10 deprecates this flag, but GHC 8.8 needs it
 -- emitPrimOp is quite large
 {-# OPTIONS_GHC -fmax-pmcheck-iterations=4000000 #-}
+#endif
 
 ----------------------------------------------------------------------------
 --
diff --git a/compiler/cmm/CmmOpt.hs b/compiler/cmm/CmmOpt.hs
index ed8b386238..5b542a390e 100644
--- a/compiler/cmm/CmmOpt.hs
+++ b/compiler/cmm/CmmOpt.hs
@@ -1,7 +1,3 @@
--- The default iteration limit is a bit too low for the definitions
--- in this module.
-{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
-
 -----------------------------------------------------------------------------
 --
 -- Cmm optimisation
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index dbb83ab0f5..52f8c376bc 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -166,28 +166,50 @@ instance Monoid Diverged where
   mempty = NotDiverged
   mappend = (Semi.<>)
 
+data Precision = Approximate | Precise
+  deriving (Eq, Show)
+
+instance Outputable Precision where
+  ppr = text . show
+
+instance Semi.Semigroup Precision where
+  Approximate <> _ = Approximate
+  _ <> Approximate = Approximate
+  Precise <> Precise = Precise
+
+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 }
+                      , presultDivergent :: Diverged
+                      , presultApprox    :: Precision }
 
 emptyPartialResult :: PartialResult
 emptyPartialResult = PartialResult { presultUncovered = mempty
                                    , presultCovered   = mempty
-                                   , presultDivergent = mempty }
+                                   , presultDivergent = mempty
+                                   , presultApprox    = mempty }
 
 combinePartialResults :: PartialResult -> PartialResult -> PartialResult
-combinePartialResults (PartialResult cs1 vsa1 ds1) (PartialResult cs2 vsa2 ds2)
+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 vsa d)
-    = hang (text "PartialResult" <+> ppr c <+> ppr d) 2  (ppr_vsa vsa)
+  ppr (PartialResult c unc d pc)
+    = hang (text "PartialResult" <+> ppr c <+> ppr d <+> ppr pc) 2 (ppr_unc unc)
     where
-      ppr_vsa = braces . fsep . punctuate comma . map ppr
+      ppr_unc = braces . fsep . punctuate comma . map ppr
 
 instance Semi.Semigroup PartialResult where
   (<>) = combinePartialResults
@@ -201,6 +223,8 @@ instance Monoid PartialResult where
 -- * 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:
@@ -211,13 +235,15 @@ data PmResult =
   PmResult {
       pmresultRedundant    :: [Located [LPat GhcTc]]
     , pmresultUncovered    :: UncoveredCandidates
-    , pmresultInaccessible :: [Located [LPat GhcTc]] }
+    , 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)
     ]
 
 -- | Either a list of patterns that are not covered, or their type, in case we
@@ -250,27 +276,24 @@ instance Outputable UncoveredCandidates where
 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
   tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
-  mb_pm_res <- tryM (checkSingle' locn var p)
-  case mb_pm_res of
-    Left  _   -> warnPmIters dflags ctxt
-    Right res -> dsPmWarn dflags ctxt res
+  res <- checkSingle' locn var p
+  dsPmWarn dflags ctxt res
 
 -- | Check a single pattern binding (let)
 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
 checkSingle' locn var p = do
-  resetPmIterDs -- set the iter-no to zero
   fam_insts <- dsGetFamInstEnvs
   clause    <- translatePat fam_insts p
   missing   <- getPmDelta
   tracePm "checkSingle': missing" (ppr missing)
-  PartialResult cs us ds <- pmcheckI clause [] [var] 1 missing
+  PartialResult cs us ds pc <- pmcheckI clause [] [var] 1 missing
   dflags <- getDynFlags
   us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us
   let uc = UncoveredPatterns [var] us'
   return $ case (cs,ds) of
-    (Covered,  _    )         -> PmResult [] uc [] -- useful
-    (NotCovered, NotDiverged) -> PmResult m  uc [] -- redundant
-    (NotCovered, Diverged )   -> PmResult [] uc m  -- inaccessible rhs
+    (Covered,  _    )         -> PmResult [] uc [] pc -- useful
+    (NotCovered, NotDiverged) -> PmResult m  uc [] pc -- redundant
+    (NotCovered, Diverged )   -> PmResult [] uc m  pc -- inaccessible rhs
   where m = [cL locn [cL locn p]]
 
 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
@@ -299,14 +322,12 @@ checkMatches dflags ctxt vars matches = do
                                , text "Matches:"])
                                2
                                (vcat (map ppr matches)))
-  mb_pm_res <- tryM $ case matches of
+  res <- case matches of
     -- Check EmptyCase separately
     -- See Note [Checking EmptyCase Expressions] in PmOracle
     [] | [var] <- vars -> checkEmptyCase' var
     _normal_match      -> checkMatches' vars matches
-  case mb_pm_res of
-    Left  _   -> warnPmIters dflags ctxt
-    Right res -> dsPmWarn dflags ctxt res
+  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.
@@ -314,38 +335,45 @@ checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
 checkMatches' vars matches
   | null matches = panic "checkMatches': EmptyCase"
   | otherwise = do
-      resetPmIterDs -- set the iter-no to zero
       missing    <- getPmDelta
       tracePm "checkMatches': missing" (ppr missing)
-      (rs,us,ds) <- go matches [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 }
+                 , pmresultInaccessible = map hsLMatchToLPats ds
+                 , pmresultApproximate  = pc }
   where
     go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
        -> DsM ( [LMatch GhcTc (LHsExpr GhcTc)]
               , Uncovered
-              , [LMatch GhcTc (LHsExpr GhcTc)])
-    go []     missing = return ([], missing, [])
+              , [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 m
-      r@(PartialResult cs missing' ds)
-        <- runMany (pmcheckI clause guards vars (length missing)) missing
+      let limit           = maxPmCheckModels dflags
+          n_siblings      = length missing
+          throttled_check delta =
+            snd <$> throttle limit (pmcheckI clause guards vars) n_siblings delta
+
+      r@(PartialResult cs missing' ds pc1) <- runMany throttled_check missing
+
       tracePm "checkMatches': go: res" (ppr r)
-      (rs, final_u, is)  <- go ms missing'
+      (rs, final_u, is, pc2)  <- go ms missing'
       return $ case (cs, ds) of
         -- useful
-        (Covered,  _    )        -> (rs, final_u,   is)
+        (Covered,  _    )        -> (rs, final_u,    is, pc1 Semi.<> pc2)
         -- redundant
-        (NotCovered, NotDiverged) -> (m:rs, final_u,is)
+        (NotCovered, NotDiverged) -> (m:rs, final_u, is, pc1 Semi.<> pc2)
         -- inaccessible
-        (NotCovered, Diverged )   -> (rs, final_u, m:is)
+        (NotCovered, Diverged )   -> (rs, final_u, m:is, pc1 Semi.<> pc2)
 
     hsLMatchToLPats :: LMatch id body -> Located [LPat id]
     hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
@@ -363,7 +391,7 @@ checkEmptyCase' x = do
     -- 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 [])
+  pure (PmResult [] us [] Precise)
 
 getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta]
 getNFirstUncovered _    0 _              = pure []
@@ -373,38 +401,6 @@ getNFirstUncovered vars n (delta:deltas) = do
   back <- getNFirstUncovered vars (n - length front) deltas
   pure (front ++ back)
 
--- | The maximum successive number of refinements ('refineToAltCon') we allow
--- per representative. See Note [Limit the number of refinements].
-mAX_REFINEMENTS :: Int
--- The current number is chosen so that PrelRules is still checked with
--- reasonable performance. If this is set to below 2, ds022 will start to fail.
--- Although that is probably due to the fact that we always increase the
--- refinement counter instead of just increasing it when the contraposition
--- is satisfiable (when the not taken case 'addRefutableAltCon' is
--- satisfiable, that is). That would be the first thing I'd try if we have
--- performance problems on one test while decreasing the threshold leads to
--- other tests being broken like ds022 above.
-mAX_REFINEMENTS = 3
-
--- | The threshold for detecting exponential blow-up in the number of 'Delta's
--- to check introduced by guards.
-tHRESHOLD_GUARD_DELTAS :: Int
-tHRESHOLD_GUARD_DELTAS = 100
-
--- | Multiply the estimated number of 'Delta's to process by a constant
--- branching factor induced by a guard and return the new estimate if it
--- doesn't exceed a constant threshold.
--- See 6. in Note [Guards and Approximation].
-tryMultiplyDeltas :: Int -> Int -> Maybe Int
-tryMultiplyDeltas multiplier n_delta
-  -- The ^2 below is intentional: We want to give up on guards with a large
-  -- branching factor rather quickly, still leaving room for small informative
-  -- ones later on.
-  | n_delta*multiplier^(2::Int) < tHRESHOLD_GUARD_DELTAS
-  = Just (n_delta*multiplier)
-  | otherwise
-  = Nothing
-
 {-
 %************************************************************************
 %*                                                                      *
@@ -555,7 +551,7 @@ translatePat fam_insts pat = case pat of
     --
     -- Here we construct CanFailPmPat directly, rather can construct a view
     -- pattern and do further translation as an optimization, for the reason,
-    -- see Note [Guards and Approximation].
+    -- see Note [Countering exponential blowup].
 
   ConPatOut { pat_con     = (dL->L _ con)
             , pat_arg_tys = arg_tys
@@ -734,18 +730,41 @@ translateBoolGuard e
     -- PatVec for efficiency
   | otherwise = (:[]) <$> mkGuard [truePattern] (unLoc e)
 
-{- Note [Guards and Approximation]
+{- Note [Countering exponential blowup]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Precise pattern match exchaustiveness checking is necessarily exponential in
-the size of some input programs. We implement a couple approximation and safe
-guards to prevent exponential blow-up:
+Precise pattern match exhaustiveness checking is necessarily exponential in
+the size of some input programs. We implement a counter-measure in the form of
+the -fmax-pmcheck-models flag, limiting the number of Deltas we check against
+each pattern by a constant.
+
+How do we do that? Consider
+
+  f True True = ()
+  f True True = ()
+
+And imagine we set our limit to 1 for the sake of the example. The first clause
+will be checked against the initial Delta, {}. Doing so will produce an
+Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}.
+Also we find the first clause to cover the model {x~True,y~True}.
+
+But the Uncovered set we get out of the match is too huge! We somehow have to
+ensure not to make things worse as they are already, so we continue checking
+with a singleton Uncovered set of the initial Delta {}. Why is this
+sound (wrt. notion of the GADTs Meet their Match paper)? Well, it basically
+amounts to forgetting that we matched against the first clause. The values
+represented by {} are a superset of those represented by its two refinements
+{x/~True} and {x~True,y/~True}.
 
-  * Guards usually provide little information gain while quickly leading to
-    exponential blow-up. See Note [Combinatorial explosion in guards].
-  * Similar to the situation with guards, refining a variable to a pattern
-    synonym application provides little value while easily leading to
-    exponential blow-up due to lack of generativity compared to DataCons.
-    See Note [Limit the number of refinements].
+This forgetfulness becomes very apparent in the example above: By continuing
+with {} we don't detect the second clause as redundant, as it again covers the
+same non-empty subset of {}. So we don't flag everything as redundant anymore,
+but still will never flag something as redundant that isn't.
+
+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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -758,54 +777,11 @@ 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.
-Long story short: At each point we estimate the number of Deltas we possibly
-have to check in the same manner as the current Delta. If we hit a guard that
-splits the current Delta k-fold, we check whether this split would get us beyond
-a certain threshold ('tryMultiplyDeltas') and continue to check the other guards
-with the original Delta.
-
-Note [Limit the number of refinements]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In PrelRules, we have a huge case with relatively deep matches on pattern
-synonyms. Since we allow multiple compatible solutions in the oracle
-(i.e. @x ~ [I# y, 42]@), and every pattern synonym is compatible according to
-'eqPmAltCon' with every other (no generativity as with DataCons), what would
-usually result in a ConVar split where only one branch is satisfiable results
-in a blow-up of Deltas. Here's an example:
-    case x of
-      A (A _) -> ()
-      B (B _) -> ()
-      ...
-By the time we hit the first clause's RHS, we have split the initial Delta twice
-and handled the {x~A y, y ~ A z} case, leaving {x/~A} and {x~A y, y/~A} models
-for the second clause to check.
-
-Now consider what happens if A=Left, B=Right. We get x~B y' from the match,
-which contradicts with {x~A y, y/~A}, because A and B are incompatible due to
-the generative nature of DataCons. This leaves only {x/~A} for checking B's
-clause, which ultimately leaves {x/~[A,B]} and {x~B y', y'/~B} uncovered.
-Resulting in three models to check for the next clause. That's only linear
-growth in the number of models for each clause.
-
-Consider A and B were arbitrary pattern synonyms instead. We still get x~B y'
-from the match, but this no longer refutes {x~A y, y/~A}, because we don't
-assume generativity for pattern synonyms. Ergo, @eqPmAltCon A B == Nothing@
-and we get to check the second clause's inner match with {x~B y', x/~A} and
-{x~[A y,B y'], y/~A}, splitting both in turn. That makes 4 instead of 3 deltas.
-If we keep on doing this, we see that in the nth clause we'd have O(2^n) models
-to check instead of just O(n) as above!
-
-Clearly we have to put a stop to this. So we count in the oracle the number of
-times we refined x to some constructor. If the number of splits exceeds the
-'mAX_REFINEMENTS', we check the next clause using the original Delta rather
-than the union of Deltas arising from the ConVar split.
-
-If for the above example we had mAX_REFINEMENTS=1, then in the second clause
-we would still check the inner match with {x~B y', x/~A} and {x~[A y,B y'], y/~A}
-but *discard* the two Deltas arising from splitting {x~[A y,B y'], y/~A},
-checking the next clause with {x~A y, y/~A} instead of its two refinements.
-In addition to {x~B y', y'~B z', x/~A} (which arose from the other split) and
-{x/~[A,B]} that makes 3 models for the third equation, so linear :).
+
+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.
 
 Note [Translate CoPats]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -1006,49 +982,62 @@ Main functions are:
   Processes the guards.
 -}
 
--- | Lift a pattern matching action from a single value vector abstration to a
--- value set abstraction, but calling it on every vector and combining the
--- results.
+-- | @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]
+--
+-- 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 _  []     = return emptyPartialResult
-runMany pm (m:ms) = do
-  res <- pm m
-  combinePartialResults res <$> runMany pm ms
+runMany f unc = mconcat <$> traverse f unc
 
--- | Increase the counter for elapsed algorithm iterations, check that the
--- limit is not exceeded and call `pmcheck`
+-- | Print diagnostic info and actually call 'pmcheck'.
 pmcheckI :: PatVec -> [PatVec] -> ValVec -> Int -> Delta -> DsM PartialResult
 pmcheckI ps guards vva n delta = do
-  m <- incrCheckPmIterDs
-  tracePm "pmCheck" (ppr m <> colon
-                        $$ hang (text "patterns:") 2 (ppr ps)
-                        $$ hang (text "guards:") 2 (ppr guards)
-                        $$ ppr vva
-                        $$ ppr delta)
+  tracePm "pmCheck {" $ vcat [ ppr n <> colon
+                           , hang (text "patterns:") 2 (ppr ps)
+                           , hang (text "guards:") 2 (ppr guards)
+                           , ppr vva
+                           , ppr delta ]
   res <- pmcheck ps guards vva n delta
-  tracePm "pmCheckResult:" (ppr res)
+  tracePm "}:" (ppr res) -- braces are easier to match by tooling
   return res
 {-# INLINE pmcheckI #-}
 
--- | Increase the counter for elapsed algorithm iterations, check that the
--- limit is not exceeded and call `pmcheckGuards`
-pmcheckGuardsI :: [PatVec] -> Int -> Delta -> DsM PartialResult
-pmcheckGuardsI gvs n delta = incrCheckPmIterDs >> pmcheckGuards gvs n delta
-{-# INLINE pmcheckGuardsI #-}
-
 -- | Check the list of mutually exclusive guards
 pmcheckGuards :: [PatVec] -> Int -> Delta -> DsM PartialResult
 pmcheckGuards []       _ delta = return (usimple delta)
 pmcheckGuards (gv:gvs) n delta = do
-  (PartialResult cs unc ds) <- pmcheckI gv [] [] n delta
-  let (n', unc')
-        -- See Note [Combinatorial explosion in guards]
-        | Just n' <- tryMultiplyDeltas (length unc) n = (n', unc)
-        | otherwise                                   = (n, [delta])
-  (PartialResult css uncs dss) <- runMany (pmcheckGuardsI gvs n') unc'
+  dflags <- getDynFlags
+  let limit = maxPmCheckModels dflags `div` 5
+  (n', PartialResult cs unc ds pc) <- throttle limit (pmcheckI 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
@@ -1058,12 +1047,12 @@ pmcheck
   -> [PatVec] -- ^ (Possibly multiple) guards of the clause
   -> ValVec   -- ^ The value vector abstraction to match against
   -> Int      -- ^ Estimate on the number of similar 'Delta's to handle.
-              --   See 6. in Note [Guards and Approximation]
+              --   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   = pmcheckGuardsI guards n delta
+  | otherwise   = pmcheckGuards guards n delta
 
 -- Guard
 pmcheck (p@PmGrd { pm_grd_pv = pv, pm_grd_expr = e } : ps) guards vva n delta = do
@@ -1104,13 +1093,7 @@ pmcheck (p@PmCon{ pm_con_con = con, pm_con_args = args
 
   -- Combine both into a single PartialResult
   let pr = mkUnion pr_pos' pr_neg
-  case (presultUncovered pr_pos', presultUncovered pr_neg) of
-    ([], _)                                   -> pure pr
-    (_, [])                                   -> pure pr
-    -- See Note [Limit the number of refinements]
-    _ | lookupNumberOfRefinements delta x < mAX_REFINEMENTS
-      -> pure pr
-      | otherwise                             -> pure pr{ presultUncovered = [delta] }
+  pure pr
 
 pmcheck [] _ (_:_) _ _ = panic "pmcheck: nil-cons"
 pmcheck (_:_) _ [] _ _ = panic "pmcheck: cons-nil"
@@ -1284,6 +1267,10 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
           exists_u = flag_u && (case uncovered of
                                   TypeOfUncovered   _     -> True
                                   UncoveredPatterns _ unc -> notNull unc)
+          approx   = precision == Approximate
+
+      when (approx && (exists_u || exists_i)) $
+        putSrcSpanDs loc (warnDs NoReason approx_msg)
 
       when exists_r $ forM_ redundant $ \(dL->L l q) -> do
         putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
@@ -1299,7 +1286,8 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
     PmResult
       { pmresultRedundant = redundant
       , pmresultUncovered = uncovered
-      , pmresultInaccessible = inaccessible } = pm_result
+      , pmresultInaccessible = inaccessible
+      , pmresultApproximate = precision } = pm_result
 
     flag_i = wopt Opt_WarnOverlappingPatterns dflags
     flag_u = exhaustive dflags kind
@@ -1327,6 +1315,17 @@ dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
     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="
+            <> int (maxPmCheckModels dflags)
+            <> text " limit, so")
+          2
+          (  bullet <+> text "Redundant clauses might not be reported at all"
+          $$ bullet <+> text "Redundant clauses might be reported as inaccessible"
+          $$ bullet <+> text "Patterns reported as unmatched might actually be matched")
+      , text "Increase the limit or resolve the warnings to suppress this message." ]
+
 {- Note [Inaccessible warnings for record updates]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider (#12957)
@@ -1349,23 +1348,6 @@ We don't want to warn about the inaccessible branch because the programmer
 didn't put it there!  So we filter out the warning here.
 -}
 
--- | Issue a warning when the predefined number of iterations is exceeded
--- for the pattern match checker
-warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
-warnPmIters dflags (DsMatchContext kind loc)
-  = when (flag_i || flag_u) $ do
-      iters <- maxPmCheckIterations <$> getDynFlags
-      putSrcSpanDs loc (warnDs NoReason (msg iters))
-  where
-    ctxt   = pprMatchContext kind
-    msg is = fsep [ text "Pattern match checker exceeded"
-                  , parens (ppr is), text "iterations in", ctxt <> dot
-                  , text "(Use -fmax-pmcheck-iterations=n"
-                  , text "to set the maximum number of iterations to n)" ]
-
-    flag_i = wopt Opt_WarnOverlappingPatterns dflags
-    flag_u = exhaustive dflags kind
-
 dots :: Int -> [a] -> SDoc
 dots maxPatterns qs
     | qs `lengthExceeds` maxPatterns = text "..."
diff --git a/compiler/deSugar/DsMonad.hs b/compiler/deSugar/DsMonad.hs
index eac17bfea0..045647f27c 100644
--- a/compiler/deSugar/DsMonad.hs
+++ b/compiler/deSugar/DsMonad.hs
@@ -32,8 +32,8 @@ module DsMonad (
         -- Getting and setting pattern match oracle states
         getPmDelta, updPmDelta,
 
-        -- Iterations for pm checking
-        incrCheckPmIterDs, resetPmIterDs, dsGetCompleteMatches,
+        -- Get COMPLETE sets of a TyCon
+        dsGetCompleteMatches,
 
         -- Warnings and errors
         DsWarning, warnDs, warnIfSetDs, errDs, errDsCoreExpr,
@@ -190,8 +190,7 @@ mkDsEnvsFromTcGbl :: MonadIO m
                   => HscEnv -> IORef Messages -> TcGblEnv
                   -> m (DsGblEnv, DsLclEnv)
 mkDsEnvsFromTcGbl hsc_env msg_var tcg_env
-  = do { pm_iter_var <- liftIO $ newIORef 0
-       ; cc_st_var   <- liftIO $ newIORef newCostCentreState
+  = do { cc_st_var   <- liftIO $ newIORef newCostCentreState
        ; let dflags   = hsc_dflags hsc_env
              this_mod = tcg_mod tcg_env
              type_env = tcg_type_env tcg_env
@@ -200,7 +199,7 @@ mkDsEnvsFromTcGbl hsc_env msg_var tcg_env
              complete_matches = hptCompleteSigs hsc_env
                                 ++ tcg_complete_matches tcg_env
        ; return $ mkDsEnvs dflags this_mod rdr_env type_env fam_inst_env
-                           msg_var pm_iter_var cc_st_var complete_matches
+                           msg_var cc_st_var complete_matches
        }
 
 runDs :: HscEnv -> (DsGblEnv, DsLclEnv) -> DsM a -> IO (Messages, Maybe a)
@@ -219,8 +218,7 @@ runDs hsc_env (ds_gbl, ds_lcl) thing_inside
 -- | Run a 'DsM' action in the context of an existing 'ModGuts'
 initDsWithModGuts :: HscEnv -> ModGuts -> DsM a -> IO (Messages, Maybe a)
 initDsWithModGuts hsc_env guts thing_inside
-  = do { pm_iter_var <- newIORef 0
-       ; cc_st_var   <- newIORef newCostCentreState
+  = do { cc_st_var   <- newIORef newCostCentreState
        ; msg_var <- newIORef emptyMessages
        ; let dflags   = hsc_dflags hsc_env
              type_env = typeEnvFromEntities ids (mg_tcs guts) (mg_fam_insts guts)
@@ -235,8 +233,8 @@ initDsWithModGuts hsc_env guts thing_inside
              ids = concatMap bindsToIds (mg_binds guts)
 
              envs  = mkDsEnvs dflags this_mod rdr_env type_env
-                              fam_inst_env msg_var pm_iter_var
-                              cc_st_var complete_matches
+                              fam_inst_env msg_var cc_st_var
+                              complete_matches
        ; runDs hsc_env envs thing_inside
        }
 
@@ -264,9 +262,9 @@ initTcDsForSolver thing_inside
          thing_inside }
 
 mkDsEnvs :: DynFlags -> Module -> GlobalRdrEnv -> TypeEnv -> FamInstEnv
-         -> IORef Messages -> IORef Int -> IORef CostCentreState
-         -> [CompleteMatch] -> (DsGblEnv, DsLclEnv)
-mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var pmvar cc_st_var
+         -> IORef Messages -> IORef CostCentreState -> [CompleteMatch]
+         -> (DsGblEnv, DsLclEnv)
+mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var cc_st_var
          complete_matches
   = let if_genv = IfGblEnv { if_doc       = text "mkDsEnvs",
                              if_rec_types = Just (mod, return type_env) }
@@ -285,7 +283,6 @@ mkDsEnvs dflags mod rdr_env type_env fam_inst_env msg_var pmvar cc_st_var
         lcl_env = DsLclEnv { dsl_meta    = emptyNameEnv
                            , dsl_loc     = real_span
                            , dsl_delta   = initDelta
-                           , dsl_pm_iter = pmvar
                            }
     in (gbl_env, lcl_env)
 
@@ -393,22 +390,6 @@ getPmDelta = do { env <- getLclEnv; return (dsl_delta env) }
 updPmDelta :: Delta -> DsM a -> DsM a
 updPmDelta delta = updLclEnv (\env -> env { dsl_delta = delta })
 
--- | Increase the counter for elapsed pattern match check iterations.
--- If the current counter is already over the limit, fail
-incrCheckPmIterDs :: DsM Int
-incrCheckPmIterDs = do
-  env <- getLclEnv
-  cnt <- readTcRef (dsl_pm_iter env)
-  max_iters <- maxPmCheckIterations <$> getDynFlags
-  if cnt >= max_iters
-    then failM
-    else updTcRef (dsl_pm_iter env) (+1)
-  return cnt
-
--- | Reset the counter for pattern match check iterations to zero
-resetPmIterDs :: DsM ()
-resetPmIterDs = do { env <- getLclEnv; writeTcRef (dsl_pm_iter env) 0 }
-
 getSrcSpanDs :: DsM SrcSpan
 getSrcSpanDs = do { env <- getLclEnv
                   ; return (RealSrcSpan (dsl_loc env)) }
diff --git a/compiler/deSugar/PmOracle.hs b/compiler/deSugar/PmOracle.hs
index 2b88bb61e7..fd5d47c748 100644
--- a/compiler/deSugar/PmOracle.hs
+++ b/compiler/deSugar/PmOracle.hs
@@ -14,7 +14,6 @@ module PmOracle (
 
         DsM, tracePm, mkPmId,
         Delta, initDelta, canDiverge, lookupRefuts, lookupSolution,
-        lookupNumberOfRefinements,
 
         TmCt(..),
         inhabitants,
@@ -702,7 +701,7 @@ tmOracle delta = runMaybeT . foldlM go delta
 -- * Looking up VarInfo
 
 emptyVarInfo :: Id -> VarInfo
-emptyVarInfo x = VI (idType x) [] [] NoPM 0
+emptyVarInfo x = VI (idType x) [] [] NoPM
 
 lookupVarInfo :: TmState -> Id -> VarInfo
 -- (lookupVarInfo tms x) tells what we know about 'x'
@@ -740,7 +739,7 @@ canDiverge MkDelta{ delta_tm_st = ts } x
   -- 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
+  | VI _ [] [] _ <- lookupVarInfo ts x
   = True
   -- Variable x is already in WHNF or we know some refutable shape, so the
   -- constraint is non-satisfiable
@@ -768,13 +767,6 @@ lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
     | Just sol <- find isDataConSolution pos -> Just sol
     | otherwise                              -> Just (head pos)
 
--- | @lookupNumberOfRefinements delta x@ Looks up how many times we have refined
--- ('refineToAltCon') @x@ for some 'PmAltCon' to arrive at @delta@. This number
--- is always less or equal to @length (lookupSolution delta x)@!
-lookupNumberOfRefinements :: Delta -> Id -> Int
-lookupNumberOfRefinements delta x
-  = vi_n_refines (lookupVarInfo (delta_tm_st delta) x)
-
 -------------------------------
 -- * Adding facts to the oracle
 
@@ -805,7 +797,7 @@ addTmCt delta ct = runMaybeT $ case ct of
 -- See Note [TmState invariants].
 addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
 addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env } x nalt = runMaybeT $ do
-  vi@(VI _ pos neg pm _) <- lift (initLookupVarInfo delta x)
+  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
   guard (not (any (contradicts nalt) pos))
@@ -955,7 +947,7 @@ ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env }
 refineToAltCon :: Delta -> Id -> PmAltCon -> [Type] -> [TyVar] -> DsM (Maybe (Delta, [Id]))
 refineToAltCon delta x l@PmAltLit{}           _arg_tys _ex_tvs1 = runMaybeT $ do
   delta' <- addVarConCt delta x l []
-  pure (markRefined delta' x, [])
+  pure (delta', [])
 refineToAltCon delta x alt@(PmAltConLike con) arg_tys  ex_tvs1  = do
   -- The plan for ConLikes:
   -- Suppose K :: forall a b y z. (y,b) -> z -> T a b
@@ -988,15 +980,7 @@ refineToAltCon delta x alt@(PmAltConLike con) arg_tys  ex_tvs1  = do
                                  , ppr mb_delta ])
   case mb_delta of
     Nothing     -> pure Nothing
-    Just delta' -> pure (Just (markRefined delta' x, arg_vars))
-
--- | This is the only place that actualy increments 'vi_n_refines'.
-markRefined :: Delta -> Id -> Delta
-markRefined delta@MkDelta{ delta_tm_st = ts@(TmSt env) } x
-  = delta{ delta_tm_st = TmSt env' }
-  where
-    vi = lookupVarInfo ts x
-    env' = setEntrySDIE env x vi{ vi_n_refines = vi_n_refines vi + 1 }
+    Just delta' -> pure (Just (delta', arg_vars))
 
 {-
 Note [Coverage checking and existential tyvars]
@@ -1153,8 +1137,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env } x y
         -- First assume that x and y are in the same equivalence class
         let env_ind = setIndirectSDIE env x y
         -- Then sum up the refinement counters
-        let vi_y' = vi_y{ vi_n_refines = vi_n_refines vi_x + vi_n_refines vi_y }
-        let env_refs = setEntrySDIE env_ind y vi_y'
+        let env_refs = setEntrySDIE env_ind y vi_y
         let delta_refs = delta{ delta_tm_st = TmSt env_refs }
         -- and then gradually merge every positive fact we have on x into y
         let add_fact delta (cl, args) = addVarConCt delta y cl args
@@ -1173,7 +1156,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env } x y
 -- See Note [TmState invariants].
 addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta
 addVarConCt delta@MkDelta{ delta_tm_st = TmSt env } x alt args = do
-  VI ty pos neg cache n <- lift (initLookupVarInfo delta x)
+  VI ty pos neg cache <- lift (initLookupVarInfo delta x)
   -- First try to refute with a negative fact
   guard (all ((/= Equal) . eqPmAltCon alt) neg)
   -- Then see if any of the other solutions (remember: each of them is an
@@ -1190,7 +1173,7 @@ addVarConCt delta@MkDelta{ delta_tm_st = TmSt env } x alt args = do
       -- the new solution)
       let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg
       let pos' = (alt,args):pos
-      pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache n))}
+      pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache))}
 
 ----------------------------------------
 -- * Enumerating inhabitation candidates
@@ -1563,7 +1546,7 @@ provideEvidenceForEquation = go init_ts
     go _      _      0 _     = pure []
     go _      []     _ delta = pure [delta]
     go rec_ts (x:xs) n delta = do
-      VI ty pos neg pm _ <- initLookupVarInfo delta x
+      VI ty pos neg pm <- initLookupVarInfo delta x
       case pos of
         _:_ -> do
           -- All solutions must be valid at once. Try to find candidates for their
diff --git a/compiler/deSugar/PmTypes.hs b/compiler/deSugar/PmTypes.hs
index ee89cf7eb7..ddbaa01b4a 100644
--- a/compiler/deSugar/PmTypes.hs
+++ b/compiler/deSugar/PmTypes.hs
@@ -447,8 +447,7 @@ newtype TmState = TmSt (SharedDIdEnv VarInfo)
 -- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
 -- and negative ('vi_neg') facts, like "x is not (:)".
 -- Also caches the type ('vi_ty'), the 'PossibleMatches' of a COMPLETE set
--- ('vi_cache') and the number of times each variable was refined
--- ('vi_n_refines').
+-- ('vi_cache').
 --
 -- Subject to Note [The Pos/Neg invariant].
 data VarInfo
@@ -485,15 +484,6 @@ data VarInfo
   -- possible constructors of each COMPLETE set. So, if it's not in here, we
   -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
   -- to recognise completion of a COMPLETE set efficiently for large enums.
-
-  , vi_n_refines :: !Int
-  -- ^ Purely for Check performance reasons. The number of times this
-  -- representative was refined ('refineToAltCon') in the Check's ConVar split.
-  -- Sadly, we can't store this info in the Check module, as it's tightly coupled
-  -- to the particular 'Delta' and also is per *representative*, not per
-  -- syntactic variable. Note that this number does not always correspond to the
-  -- length of solutions: 'addVarConCt' might add a solution without
-  -- incurring the potential exponential blowup by ConVar.
   }
 
 -- | Not user-facing.
@@ -502,8 +492,8 @@ instance Outputable TmState where
 
 -- | Not user-facing.
 instance Outputable VarInfo where
-  ppr (VI ty pos neg cache n)
-    = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache, ppr n]))
+  ppr (VI ty pos neg cache)
+    = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache]))
 
 -- | Initial state of the oracle.
 initTmState :: TmState
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 45a465bd9c..02499d2f74 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -976,7 +976,6 @@ data DynFlags = DynFlags {
   debugLevel            :: Int,         -- ^ How much debug information to produce
   simplPhases           :: Int,         -- ^ Number of simplifier phases
   maxSimplIterations    :: Int,         -- ^ Max simplifier iterations
-  maxPmCheckIterations  :: Int,         -- ^ Max no iterations for pm checking
   ruleCheck             :: Maybe String,
   inlineCheck           :: Maybe String, -- ^ A prefix to report inlining decisions about
   strictnessBefore      :: [Int],       -- ^ Additional demand analysis
@@ -1000,6 +999,10 @@ data DynFlags = DynFlags {
                                         --   error messages
   maxUncoveredPatterns  :: Int,         -- ^ Maximum number of unmatched patterns to show
                                         --   in non-exhaustiveness warnings
+  maxPmCheckModels      :: Int,         -- ^ Soft limit on the number of models
+                                        --   the pattern match checker checks
+                                        --   a pattern against. A safe guard
+                                        --   against exponential blow-up.
   simplTickFactor       :: Int,         -- ^ Multiplier for simplifier ticks
   specConstrThreshold   :: Maybe Int,   -- ^ Threshold for SpecConstr
   specConstrCount       :: Maybe Int,   -- ^ Max number of specialisations for any one function
@@ -1928,7 +1931,6 @@ defaultDynFlags mySettings (myLlvmTargets, myLlvmPasses) =
         debugLevel              = 0,
         simplPhases             = 2,
         maxSimplIterations      = 4,
-        maxPmCheckIterations    = 2000000,
         ruleCheck               = Nothing,
         inlineCheck             = Nothing,
         binBlobThreshold        = 500000, -- 500K is a good default (see #16190)
@@ -1937,6 +1939,7 @@ defaultDynFlags mySettings (myLlvmTargets, myLlvmPasses) =
         maxRefHoleFits     = Just 6,
         refLevelHoleFits   = Nothing,
         maxUncoveredPatterns    = 4,
+        maxPmCheckModels        = 100,
         simplTickFactor         = 100,
         specConstrThreshold     = Just 2000,
         specConstrCount         = Just 3,
@@ -3601,12 +3604,16 @@ dynamic_flags_deps = [
             "vectors registers are now passed in registers by default."
   , make_ord_flag defFlag "fmax-uncovered-patterns"
       (intSuffix (\n d -> d { maxUncoveredPatterns = n }))
+  , make_ord_flag defFlag "fmax-pmcheck-models"
+      (intSuffix (\n d -> d { maxPmCheckModels = n }))
   , make_ord_flag defFlag "fsimplifier-phases"
       (intSuffix (\n d -> d { simplPhases = n }))
   , make_ord_flag defFlag "fmax-simplifier-iterations"
       (intSuffix (\n d -> d { maxSimplIterations = n }))
-  , make_ord_flag defFlag "fmax-pmcheck-iterations"
-      (intSuffix (\n d -> d{ maxPmCheckIterations = n }))
+  , (Deprecated, defFlag "fmax-pmcheck-iterations"
+      (intSuffixM (\_ d ->
+       do { deprecate $ "use -fmax-pmcheck-models instead"
+          ; return d })))
   , make_ord_flag defFlag "fsimpl-tick-factor"
       (intSuffix (\n d -> d { simplTickFactor = n }))
   , make_ord_flag defFlag "fspec-constr-threshold"
diff --git a/compiler/nativeGen/X86/CodeGen.hs b/compiler/nativeGen/X86/CodeGen.hs
index 9f0af9429d..864013efb4 100644
--- a/compiler/nativeGen/X86/CodeGen.hs
+++ b/compiler/nativeGen/X86/CodeGen.hs
@@ -1,8 +1,11 @@
 {-# LANGUAGE CPP, GADTs, NondecreasingIndentation #-}
 
+#if __GLASGOW_HASKELL__ <= 808
+-- GHC 8.10 deprecates this flag, but GHC 8.8 needs it
 -- The default iteration limit is a bit too low for the definitions
 -- in this module.
 {-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
+#endif
 
 -----------------------------------------------------------------------------
 --
diff --git a/compiler/prelude/PrimOp.hs b/compiler/prelude/PrimOp.hs
index ac4f162e08..f338a6094f 100644
--- a/compiler/prelude/PrimOp.hs
+++ b/compiler/prelude/PrimOp.hs
@@ -6,9 +6,6 @@
 
 {-# LANGUAGE CPP #-}
 
--- The default is a bit too low for the quite large primOpInfo definition
-{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
-
 module PrimOp (
         PrimOp(..), PrimOpVecCat(..), allThePrimOps,
         primOpType, primOpSig,
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 8f301a0391..83616bdb82 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -392,10 +392,7 @@ data DsLclEnv = DsLclEnv {
         -- See Note [Note [Type and Term Equality Propagation] in Check.hs
         -- The oracle state Delta is augmented as we walk inwards,
         -- through each pattern match in turn
-        dsl_delta   :: Delta,
-
-        dsl_pm_iter :: IORef Int  -- Number of iterations for pmcheck so far
-                                  -- We fail if this gets too big
+        dsl_delta   :: Delta
      }
 
 -- Inside [| |] brackets, the desugarer looks
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 31060d701d..fa44b1a370 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -831,20 +831,22 @@ of ``-W(no-)*``.
         h = \[] -> 2
         Just k = f y
 
-.. ghc-flag:: -fmax-pmcheck-iterations=⟨n⟩
-    :shortdesc: the iteration limit for the pattern match checker
+.. ghc-flag:: -fmax-pmcheck-models=⟨n⟩
+    :shortdesc: soft limit on the number of parallel models the pattern match
+        checker should check a pattern match clause against
     :type: dynamic
     :category:
 
-    :default: 2000000
+    :default: 100
 
-    Sets how many iterations of the pattern-match checker will perform before
-    giving up. This limit is to catch cases where pattern-match checking might
-    be excessively costly (due to the exponential complexity of coverage
-    checking in the general case). It typically shouldn't be necessary to set
-    this unless GHC informs you that it has exceeded the pattern match checker's
-    iteration limit (in which case you may want to consider refactoring your
-    pattern match, for the sake of future readers of your code.
+    Pattern match checking can be exponential in some cases. This limit makes
+    sure we scale polynomially in the number of patterns, by forgetting refined
+    information gained from a partially successful match. For example, when
+    matching ``x`` against ``Just 4``, we split each incoming matching model
+    into two sub-models: One where ``x`` is not ``Nothing`` and one where ``x``
+    is ``Just y`` but ``y`` is not ``4``. When the number of incoming models
+    exceeds the limit, we continue checking the next clause with the original,
+    unrefined model.
 
 .. ghc-flag:: -Wincomplete-record-updates
     :shortdesc: warn when a record update could fail
diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs
index 0c35b4fd27..80d31ab8a7 100644
--- a/testsuite/tests/pmcheck/should_compile/T11195.hs
+++ b/testsuite/tests/pmcheck/should_compile/T11195.hs
@@ -1,5 +1,4 @@
 {-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
-{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-}
 
 module T11195 where
 
diff --git a/testsuite/tests/pmcheck/should_compile/T11822.stderr b/testsuite/tests/pmcheck/should_compile/T11822.stderr
index 4d60fc368c..7198efc588 100644
--- a/testsuite/tests/pmcheck/should_compile/T11822.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T11822.stderr
@@ -1,10 +1,17 @@
 
+T11822.hs:33:1: warning:
+    Pattern match checker ran into -fmax-pmcheck-models=100 limit, so
+       Redundant clauses might not be reported at all
+       Redundant clauses might be reported as inaccessible
+       Patterns reported as unmatched might actually be matched
+    Increase the limit or resolve the warnings to suppress this message.
+
 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 _) _ 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 _) _ _
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs b/testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs
new file mode 100644
index 0000000000..4b0d7df233
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/TooManyDeltas.hs
@@ -0,0 +1,28 @@
+-- | The function here exploit matches of arity 2 that split the uncovered set
+-- in two. Too many for -fmax-pmcheck-models=0!
+-- As a result, these functions elicit the symptoms describe in the warnings
+-- message, e.g.
+--   - False positives on exhaustivity
+--   - Turns redundant into inaccessible clauses
+--   - Fails to report redundant matches
+module TooManyDeltas where
+
+data T = A | B
+
+-- | Reports that a clause for _ _ is missing.
+f :: T -> T -> ()
+f A A = ()
+
+-- | Reports that the third clause is inaccessible, when really it is
+-- redundant.
+g :: T -> T -> ()
+g _ A = ()
+g A A = () -- inaccessible, correctly flagged
+g A A = () -- redundant, not inaccessible!
+g _ _ = () -- (this one is not about exhaustivity)
+
+-- | Fails to report that the second clause is redundant.
+h :: T -> T -> ()
+h A A = () -- covered, emits no warning
+h A A = () -- redundant, not covered!
+h _ _ = () -- (this one is not about exhaustivity)
diff --git a/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr b/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
new file mode 100644
index 0000000000..8180eb1542
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/TooManyDeltas.stderr
@@ -0,0 +1,26 @@
+
+TooManyDeltas.hs:14:1: warning:
+    Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
+      • Redundant clauses might not be reported at all
+      • Redundant clauses might be reported as inaccessible
+      • Patterns reported as unmatched might actually be matched
+    Increase the limit or resolve the warnings to suppress this message.
+
+TooManyDeltas.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘f’: Patterns not matched: _ _
+
+TooManyDeltas.hs:19:1: warning:
+    Pattern match checker ran into -fmax-pmcheck-models=0 limit, so
+      • Redundant clauses might not be reported at all
+      • Redundant clauses might be reported as inaccessible
+      • Patterns reported as unmatched might actually be matched
+    Increase the limit or resolve the warnings to suppress this message.
+
+TooManyDeltas.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘g’: g A A = ...
+
+TooManyDeltas.hs:21:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘g’: g A A = ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 9c38d636eb..e41d7f211c 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -115,6 +115,8 @@ test('CyclicSubst', [],  compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('CaseOfKnownCon', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('TooManyDeltas', [], compile,
+     ['-fmax-pmcheck-models=0 -fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # EmptyCase
 test('T10746', [], compile,