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
-------------------------

1 files changed, 12 insertions, 10 deletions

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