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

19 files changed, 157 insertions, 29 deletions

diff --git a/testsuite/tests/deSugar/should_compile/T14773b.stderr b/testsuite/tests/deSugar/should_compile/T14773b.stderr
index b204b4f485..f76eb050e4 100644
--- a/testsuite/tests/deSugar/should_compile/T14773b.stderr
+++ b/testsuite/tests/deSugar/should_compile/T14773b.stderr
@@ -1,9 +1,13 @@
 
-T14773b.hs:4:10: warning: [-Woverlapping-patterns (in -Wdefault)]
-    Pattern match is redundant
-    In a pattern binding guards: = ...
-
 T14773b.hs:4:10: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a pattern binding guards:
         Guards do not cover entire pattern space
+
+T14773b.hs:4:12: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a pattern binding guards: | False = ...
+
+T14773b.hs:7:12: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a pattern binding guards: | False = ...
diff --git a/testsuite/tests/deSugar/should_compile/T2409.stderr b/testsuite/tests/deSugar/should_compile/T2409.stderr
new file mode 100644
index 0000000000..1efc5bae97
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/T2409.stderr
@@ -0,0 +1,8 @@
+
+T2409.hs:6:8: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f _ | () `seq` False = ...
+
+T2409.hs:10:8: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g _ | () `seq` False = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds002.stderr b/testsuite/tests/deSugar/should_compile/ds002.stderr
index 20705a351b..441add8d27 100644
--- a/testsuite/tests/deSugar/should_compile/ds002.stderr
+++ b/testsuite/tests/deSugar/should_compile/ds002.stderr
@@ -7,6 +7,22 @@ ds002.hs:9:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
     In an equation for ‘f’: f z = ...
 
-ds002.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+ds002.hs:12:11: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
-    In an equation for ‘g’: g x y z = ...
+    In an equation for ‘g’: g x y z | True = ...
+
+ds002.hs:13:11: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g x y z | True = ...
+
+ds002.hs:14:11: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g x y z | True = ...
+
+ds002.hs:15:11: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g x y z | True = ...
+
+ds002.hs:16:11: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g x y z | True = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds006.stderr b/testsuite/tests/deSugar/should_compile/ds006.stderr
new file mode 100644
index 0000000000..cc8bbd947b
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/ds006.stderr
@@ -0,0 +1,4 @@
+
+ds006.hs:6:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘v’: v | False = ...
diff --git a/testsuite/tests/deSugar/should_compile/ds021.stderr b/testsuite/tests/deSugar/should_compile/ds021.stderr
new file mode 100644
index 0000000000..0fd5686076
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/ds021.stderr
@@ -0,0 +1,4 @@
+
+ds021.hs:8:11: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f x y z | False = ...
diff --git a/testsuite/tests/indexed-types/should_compile/GivenCheck.stderr b/testsuite/tests/indexed-types/should_compile/GivenCheck.stderr
new file mode 100644
index 0000000000..8f50bf5058
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenCheck.stderr
@@ -0,0 +1,4 @@
+
+GivenCheck.hs:11:9: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g y | False = ...
diff --git a/testsuite/tests/indexed-types/should_compile/GivenCheckSwap.stderr b/testsuite/tests/indexed-types/should_compile/GivenCheckSwap.stderr
new file mode 100644
index 0000000000..2ef17fd6d9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenCheckSwap.stderr
@@ -0,0 +1,4 @@
+
+GivenCheckSwap.hs:11:9: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g y | False = ...
diff --git a/testsuite/tests/layout/layout006.stdout b/testsuite/tests/layout/layout006.stdout
index 0c5dd597f9..8037c234c5 100644
--- a/testsuite/tests/layout/layout006.stdout
+++ b/testsuite/tests/layout/layout006.stdout
@@ -1,4 +1,8 @@
 Running with -XNoAlternativeLayoutRule
+
+layout006.hs:12:4: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f | True = ...
 Running with -XAlternativeLayoutRule
 
 layout006.hs:12:2: error: parse error on input ‘|’
@@ -7,3 +11,7 @@ Running with -XAlternativeLayoutRule -XAlternativeLayoutRuleTransitional
 layout006.hs:12:2: warning: [-Walternative-layout-rule-transitional (in -Wdefault)]
     transitional layout will not be accepted in the future:
     `|' at the same depth as implicit layout block
+
+layout006.hs:12:4: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f | True = ...
diff --git a/testsuite/tests/perf/compiler/T12150.hs b/testsuite/tests/perf/compiler/T12150.hs
index a0d4ed5ce4..1712f4ecfc 100644
--- a/testsuite/tests/perf/compiler/T12150.hs
+++ b/testsuite/tests/perf/compiler/T12150.hs
@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
+
 module T12150 where
 
 data Result a = Success a | Error String
diff --git a/testsuite/tests/pmcheck/should_compile/T11822.stderr b/testsuite/tests/pmcheck/should_compile/T11822.stderr
index 66d365baaa..569cc74e99 100644
--- a/testsuite/tests/pmcheck/should_compile/T11822.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T11822.stderr
@@ -1,6 +1,6 @@
 
 T11822.hs:33:1: warning:
-    Pattern match checker ran into -fmax-pmcheck-models=100 limit, so
+    Pattern match checker ran into -fmax-pmcheck-models=30 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
@@ -11,15 +11,11 @@ T11822.hs:33:1: warning: [-Wincomplete-patterns (in -Wextra)]
     In an equation for ‘mkTreeNode’:
         Patterns not matched:
             _ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
-            (Data.Set.Internal.Bin _ _ _ _) p
-                where p is not one of {0}
+            (Data.Set.Internal.Bin _ _ _ _) (Depth _)
             _ (Data.Sequence.Internal.Seq Data.Sequence.Internal.EmptyT)
-            Data.Set.Internal.Tip p
-                where p is not one of {0}
+            Data.Set.Internal.Tip (Depth _)
             _ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
-            (Data.Set.Internal.Bin _ _ _ _) p
-                where p is not one of {0}
+            (Data.Set.Internal.Bin _ _ _ _) (Depth _)
             _ (Data.Sequence.Internal.Seq (Data.Sequence.Internal.Single _))
-            Data.Set.Internal.Tip p
-                where p is not one of {0}
+            Data.Set.Internal.Tip (Depth _)
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17465.hs b/testsuite/tests/pmcheck/should_compile/T17465.hs
new file mode 100644
index 0000000000..93d367bfe2
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17465.hs
@@ -0,0 +1,18 @@
+module Lib where
+
+f :: () -> ()
+f _
+  | False = ()
+  | otherwise = ()
+
+g :: () -> ()
+g ()
+  | False = ()
+  | False = ()
+  | otherwise = ()
+
+h :: () -> ()
+h x
+  | () <- x, False = ()
+  | False          = ()
+  | otherwise      = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17465.stderr b/testsuite/tests/pmcheck/should_compile/T17465.stderr
new file mode 100644
index 0000000000..6b0068201e
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17465.stderr
@@ -0,0 +1,20 @@
+
+T17465.hs:5:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f _ | False = ...
+
+T17465.hs:10:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g () | False = ...
+
+T17465.hs:11:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g () | False = ...
+
+T17465.hs:16:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘h’: h x | () <- x, False = ...
+
+T17465.hs:17:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘h’: h x | False = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T17646.hs b/testsuite/tests/pmcheck/should_compile/T17646.hs
new file mode 100644
index 0000000000..110068d5a8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17646.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+
+module T17646 where
+
+data T a where
+  A :: T True
+  B :: T False
+
+g :: ()
+g | B <- A = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T17646.stderr b/testsuite/tests/pmcheck/should_compile/T17646.stderr
new file mode 100644
index 0000000000..93a60bc466
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17646.stderr
@@ -0,0 +1,21 @@
+
+T17646.hs:11:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘g’: Guards do not cover entire pattern space
+
+T17646.hs:11:5: warning: [-Winaccessible-code (in -Wdefault)]
+    • Couldn't match type ‘'True’ with ‘'False’
+      Inaccessible code in
+        a pattern with constructor: B :: T 'False,
+        in a pattern binding in
+             a pattern guard for
+               an equation for ‘g’
+    • In the pattern: B
+      In a stmt of a pattern guard for
+                     an equation for ‘g’:
+        B <- A
+      In an equation for ‘g’: g | B <- A = ()
+
+T17646.hs:11:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘g’: g | B <- A = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T2204.stderr b/testsuite/tests/pmcheck/should_compile/T2204.stderr
index 49fcdf6f91..7b5a2b52f7 100644
--- a/testsuite/tests/pmcheck/should_compile/T2204.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T2204.stderr
@@ -3,9 +3,9 @@ T2204.hs:6:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
         Patterns not matched:
-            ('0':'1':_:_)
-            ['0', p] where p is not one of {'1'}
-            ('0':p:_:_) where p is not one of {'1'}
+            []
+            [p] where p is not one of {'0'}
+            (p:_:_) where p is not one of {'0'}
             ['0']
             ...
 
diff --git a/testsuite/tests/pmcheck/should_compile/T9951b.stderr b/testsuite/tests/pmcheck/should_compile/T9951b.stderr
index 51518bce7b..c9536b3160 100644
--- a/testsuite/tests/pmcheck/should_compile/T9951b.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T9951b.stderr
@@ -3,8 +3,8 @@ T9951b.hs:7:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
         Patterns not matched:
-            ('a':'b':_:_)
-            ['a', p] where p is not one of {'b'}
-            ('a':p:_:_) where p is not one of {'b'}
+            []
+            [p] where p is not one of {'a'}
+            (p:_:_) where p is not one of {'a'}
             ['a']
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 6185b0aebb..47aa073c66 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -106,6 +106,10 @@ test('T17357', expect_broken(17357), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T17376', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17465', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17646', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,
diff --git a/testsuite/tests/pmcheck/should_compile/pmc007.stderr b/testsuite/tests/pmcheck/should_compile/pmc007.stderr
index 77d2893b2a..9a3fe6efdc 100644
--- a/testsuite/tests/pmcheck/should_compile/pmc007.stderr
+++ b/testsuite/tests/pmcheck/should_compile/pmc007.stderr
@@ -8,18 +8,18 @@ pmc007.hs:12:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘g’:
         Patterns not matched:
-            ('a':'b':_:_)
-            ('a':'c':_:_)
-            ['a', p] where p is not one of {'b', 'c'}
-            ('a':p:_:_) where p is not one of {'b', 'c'}
+            []
+            [p] where p is not one of {'a'}
+            (p:_:_) where p is not one of {'a'}
+            ['a']
             ...
 
 pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative:
         Patterns not matched:
-            ('a':'b':_:_)
-            ('a':'c':_:_)
-            ['a', p] where p is not one of {'b', 'c'}
-            ('a':p:_:_) where p is not one of {'b', 'c'}
+            []
+            [p] where p is not one of {'a'}
+            (p:_:_) where p is not one of {'a'}
+            ['a']
             ...
diff --git a/testsuite/tests/typecheck/should_compile/tc017.stderr b/testsuite/tests/typecheck/should_compile/tc017.stderr
new file mode 100644
index 0000000000..7e7dfc3b40
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/tc017.stderr
@@ -0,0 +1,4 @@
+
+tc017.hs:4:5: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘v’: v | False = ...