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

5 files changed, 65 insertions, 3 deletions

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,