Encode shape information in `PmOracle`

Previously, we had an elaborate mechanism for selecting the warnings to
generate in the presence of different `COMPLETE` matching groups that,
albeit finely-tuned, produced wrong results from an end user's
perspective in some cases (#13363).

The underlying issue is that at the point where the `ConVar` case has to
commit to a particular `COMPLETE` group, there's not enough information
to do so and the status quo was to just enumerate all possible complete
sets nondeterministically.  The `getResult` function would then pick the
outcome according to metrics defined in accordance to the user's guide.
But crucially, it lacked knowledge about the order in which affected
clauses appear, leading to the surprising behavior in #13363.

In !1010 we taught the term oracle to reason about literal values a
variable can certainly not take on. This MR extends that idea to
`ConLike`s and thereby fixes #13363: Instead of committing to a
particular `COMPLETE` group in the `ConVar` case, we now split off the
matching constructor incrementally and record the newly covered case as
a refutable shape in the oracle. Whenever the set of refutable shapes
covers any `COMPLETE` set, the oracle recognises vacuosity of the
uncovered set.

This patch goes a step further: Since at this point the information
in value abstractions is merely a cut down representation of what the
oracle knows, value abstractions degenerate to a single `Id`, the
semantics of which is determined by the oracle state `Delta`.
Value vectors become lists of `[Id]` given meaning to by a single
`Delta`, value set abstractions (of which the uncovered set is an
instance) correspond to a union of `Delta`s which instantiate the
same `[Id]` (akin to models of formula).

Fixes #11528 #13021, #13363, #13965, #14059, #14253, #14851, #15753, #17096, #17149

-------------------------
Metric Decrease:
    ManyAlternatives
    T11195
-------------------------

50 files changed, 877 insertions, 36 deletions

diff --git a/testsuite/tests/deSugar/should_compile/T14546d.hs b/testsuite/tests/deSugar/should_compile/T14546d.hs
new file mode 100644
index 0000000000..099e64727a
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/T14546d.hs
@@ -0,0 +1,8 @@
+data D = D deriving Eq
+
+instance Num D where
+  fromInteger _ = D
+
+main = do
+    case 3 :: D of
+        1 -> putStrLn "A"
diff --git a/testsuite/tests/deSugar/should_compile/T14546d.stderr b/testsuite/tests/deSugar/should_compile/T14546d.stderr
new file mode 100644
index 0000000000..db5b9ca285
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/T14546d.stderr
@@ -0,0 +1,9 @@
+
+T14546d.hs:3:10: warning: [-Wmissing-methods (in -Wdefault)]
+    • No explicit implementation for
+        ‘+’, ‘*’, ‘abs’, ‘signum’, and (either ‘negate’ or ‘-’)
+    • In the instance declaration for ‘Num D’
+
+T14546d.hs:7:5: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: 3
diff --git a/testsuite/tests/deSugar/should_compile/T14773b.stderr b/testsuite/tests/deSugar/should_compile/T14773b.stderr
index 557b10b8f0..b204b4f485 100644
--- a/testsuite/tests/deSugar/should_compile/T14773b.stderr
+++ b/testsuite/tests/deSugar/should_compile/T14773b.stderr
@@ -1,4 +1,8 @@
 
+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:
diff --git a/testsuite/tests/deSugar/should_compile/all.T b/testsuite/tests/deSugar/should_compile/all.T
index 5369b3f473..21cf1b058d 100644
--- a/testsuite/tests/deSugar/should_compile/all.T
+++ b/testsuite/tests/deSugar/should_compile/all.T
@@ -102,6 +102,7 @@ test('T14135', normal, compile, [''])
 test('T14546a', normal, compile, ['-Wincomplete-patterns'])
 test('T14546b', normal, compile, ['-Wincomplete-patterns'])
 test('T14546c', normal, compile, ['-Wincomplete-patterns'])
+test('T14546d', normal, compile, ['-Wincomplete-patterns'])
 test('T14547', normal, compile, ['-Wincomplete-patterns'])
 test('T14773a', normal, compile, ['-Wincomplete-patterns'])
 test('T14773b', normal, compile, ['-Wincomplete-patterns'])
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.stderr b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
index ad9562eae8..684c1380aa 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.stderr
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
@@ -2,4 +2,5 @@
 KindEqualities.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘zero’:
-        Patterns not matched: (TyApp (TyApp _ _) _)
+        Patterns not matched:
+            (TyApp (TyApp p _) _) where p is not one of {TyInt}
diff --git a/testsuite/tests/driver/T8101.stderr b/testsuite/tests/driver/T8101.stderr
index 9f57360448..a486f965e3 100644
--- a/testsuite/tests/driver/T8101.stderr
+++ b/testsuite/tests/driver/T8101.stderr
@@ -1,3 +1,4 @@
+
 T8101.hs:7:9: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative:
diff --git a/testsuite/tests/haddock/should_compile_noflag_haddock/haddockSimplUtilsBug.stderr b/testsuite/tests/haddock/should_compile_noflag_haddock/haddockSimplUtilsBug.stderr
new file mode 100644
index 0000000000..2d3393b249
--- /dev/null
+++ b/testsuite/tests/haddock/should_compile_noflag_haddock/haddockSimplUtilsBug.stderr
@@ -0,0 +1,4 @@
+
+haddockSimplUtilsBug.hs:28:7: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: _ -> ...
diff --git a/testsuite/tests/parser/should_compile/read044.stderr b/testsuite/tests/parser/should_compile/read044.stderr
new file mode 100644
index 0000000000..d459248082
--- /dev/null
+++ b/testsuite/tests/parser/should_compile/read044.stderr
@@ -0,0 +1,4 @@
+
+read044.hs:5:13: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: False -> ...
diff --git a/testsuite/tests/patsyn/should_run/all.T b/testsuite/tests/patsyn/should_run/all.T
index 57bc41fc73..90f577174e 100644
--- a/testsuite/tests/patsyn/should_run/all.T
+++ b/testsuite/tests/patsyn/should_run/all.T
@@ -13,7 +13,7 @@ test('unboxed-wrapper', normal, compile_and_run, [''])
 test('records-run', normal, compile_and_run, [''])
 test('ghci', just_ghci, ghci_script, ['ghci.script'])
 test('T11985', just_ghci, ghci_script, ['T11985.script'])
-test('T11224', normal, compile_and_run, [''])
+test('T11224', normal, compile_and_run, ['-Wincomplete-patterns -Woverlapping-patterns'])
 # we omit profasm/profthreaded because it doesn't bring much to the table but
 # introduces its share of complexity, as the test as it is fails with
 # profasm:
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13021.hs b/testsuite/tests/pmcheck/complete_sigs/T13021.hs
new file mode 100644
index 0000000000..cb2a725a98
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13021.hs
@@ -0,0 +1,11 @@
+{-# OPTIONS_GHC -Woverlapping-patterns -Wincomplete-patterns #-}
+
+module Lib where
+
+data T = A | B | C
+
+{-# COMPLETE B #-}
+
+foo :: T -> ()
+foo A = ()
+foo B = ()
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363a.hs b/testsuite/tests/pmcheck/complete_sigs/T13363a.hs
new file mode 100644
index 0000000000..1d614b7d05
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363a.hs
@@ -0,0 +1,16 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -Woverlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data Boolean = F | T
+  deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F               = 0
+catchAll TooGoodToBeTrue = 1
+catchAll _               = error "impossible"
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363a.stderr b/testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
new file mode 100644
index 0000000000..a91b02806a
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363a.stderr
@@ -0,0 +1,4 @@
+
+T13363a.hs:16:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘catchAll’: catchAll _ = ...
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363b.hs b/testsuite/tests/pmcheck/complete_sigs/T13363b.hs
new file mode 100644
index 0000000000..0ef350e491
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363b.hs
@@ -0,0 +1,17 @@
+{-# OPTIONS_GHC -Wincomplete-patterns -Woverlapping-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+module Lib where
+
+data T = A | B | C
+  deriving Eq
+
+pattern BC :: T
+pattern BC = C
+
+{-# COMPLETE A, BC #-}
+
+f A  = 1
+f B  = 2
+f BC = 3
+f _  = error "impossible"
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13363b.stderr b/testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
new file mode 100644
index 0000000000..541c084be1
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13363b.stderr
@@ -0,0 +1,4 @@
+
+T13363b.hs:17:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘f’: f _ = ...
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13717.hs b/testsuite/tests/pmcheck/complete_sigs/T13717.hs
new file mode 100644
index 0000000000..e9460371c8
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13717.hs
@@ -0,0 +1,41 @@
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE EmptyCase #-}
+
+module Fin (Nat (..), Fin (FZ, FS)) where
+import Numeric.Natural
+import Unsafe.Coerce
+
+data Nat = Z | S Nat
+
+-- Fin *must* be exported abstractly (or placed in an Unsafe
+-- module) to maintain type safety.
+newtype Fin (n :: Nat) = Fin Natural
+
+data FinView n where
+  VZ :: FinView ('S n)
+  VS :: !(Fin n) -> FinView ('S n)
+
+viewFin :: Fin n -> FinView n
+viewFin (Fin 0) = unsafeCoerce VZ
+viewFin (Fin n) = unsafeCoerce (VS (Fin (n - 1)))
+
+pattern FZ :: () => n ~ 'S m => Fin n
+pattern FZ <- (viewFin -> VZ) where
+  FZ = Fin 0
+
+pattern FS :: () => n ~ 'S m => Fin m -> Fin n
+pattern FS m <- (viewFin -> VS m) where
+  FS (Fin m) = Fin (1 + m)
+
+{-# COMPLETE FZ, FS #-}
+
+finZAbsurd :: Fin 'Z -> a
+finZAbsurd x = case x of
+
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13964.hs b/testsuite/tests/pmcheck/complete_sigs/T13964.hs
new file mode 100644
index 0000000000..36a87a9a25
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13964.hs
@@ -0,0 +1,20 @@
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where
+
+data Boolean = F | T
+  deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue <- ((== T) -> True)
+  where
+    TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F               = 0
+-- catchAll TooGoodToBeTrue = 1
+
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13964.stderr b/testsuite/tests/pmcheck/complete_sigs/T13964.stderr
new file mode 100644
index 0000000000..606756a783
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13964.stderr
@@ -0,0 +1,4 @@
+
+T13964.hs:18:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘catchAll’: Patterns not matched: T
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13965.hs b/testsuite/tests/pmcheck/complete_sigs/T13965.hs
new file mode 100644
index 0000000000..ac18dad115
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13965.hs
@@ -0,0 +1,20 @@
+{-# OPTIONS_GHC -Woverlapping-patterns #-}
+
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+module Bug (Boolean(F, TooGoodToBeTrue), catchAll) where
+
+data Boolean = F | T
+  deriving Eq
+
+pattern TooGoodToBeTrue :: Boolean
+pattern TooGoodToBeTrue <- ((== T) -> True)
+  where
+    TooGoodToBeTrue = T
+{-# COMPLETE F, TooGoodToBeTrue #-}
+
+catchAll :: Boolean -> Int
+catchAll F               = 0
+catchAll TooGoodToBeTrue = 1
+catchAll F               = 2
+
diff --git a/testsuite/tests/pmcheck/complete_sigs/T13965.stderr b/testsuite/tests/pmcheck/complete_sigs/T13965.stderr
new file mode 100644
index 0000000000..78aaa9490a
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T13965.stderr
@@ -0,0 +1,4 @@
+
+T13965.hs:19:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘catchAll’: catchAll F = ...
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14059b.hs b/testsuite/tests/pmcheck/complete_sigs/T14059b.hs
new file mode 100644
index 0000000000..52f3593ecd
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T14059b.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+module Bug where
+
+data family Sing (a :: k)
+
+data instance Sing (z :: Bool) where
+  SFalse :: Sing False
+  STrue  :: Sing True
+
+pattern STooGoodToBeTrue :: forall (z :: Bool). ()
+                         => z ~ True
+                         => Sing z
+pattern STooGoodToBeTrue = STrue
+{-# COMPLETE SFalse, STooGoodToBeTrue #-}
+
+wibble :: Sing (z :: Bool) -> Bool
+wibble STrue = True
+
+wobble :: Sing (z :: Bool) -> Bool
+wobble STooGoodToBeTrue = True
+
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14059b.stderr b/testsuite/tests/pmcheck/complete_sigs/T14059b.stderr
new file mode 100644
index 0000000000..8c8569c638
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T14059b.stderr
@@ -0,0 +1,10 @@
+
+T14059b.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘wibble’:
+        Patterns not matched: p where p is not one of {STrue}
+
+T14059b.hs:26:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘wobble’:
+        Patterns not matched: p where p is not one of {STooGoodToBeTrue}
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14851.hs b/testsuite/tests/pmcheck/complete_sigs/T14851.hs
new file mode 100644
index 0000000000..d5baac58a2
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T14851.hs
@@ -0,0 +1,21 @@
+{-# OPTIONS_GHC -Woverlapping-patterns #-}
+
+{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
+
+module Bug where
+
+import Type.Reflection
+
+pattern X arg <- (checkFun -> arg)
+
+checkFun :: TypeRep fun -> a
+checkFun = undefined
+
+f x = case (x, True) of
+          (X _, _) -> 5
+          _        -> 6
+
+g x = case x of
+          (X _) -> 5
+          _     -> 6
+
diff --git a/testsuite/tests/pmcheck/complete_sigs/T17149.hs b/testsuite/tests/pmcheck/complete_sigs/T17149.hs
new file mode 100644
index 0000000000..ba68154f3c
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T17149.hs
@@ -0,0 +1,21 @@
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module Bug where
+
+class Member a b where
+  prj :: b -> Maybe a
+
+pattern P :: Member a b => a -> b
+pattern P a <- (prj -> Just a)
+
+{-# COMPLETE P :: Bool #-}
+
+-- | Trying to instantiate P with 0 type arguments doesn't work, it takes 2.
+-- This seemingly unrelated fact, only relevant through the COMPLETE set, may
+-- not lead the compiler to crash or do shady stuff.
+fun :: Bool -> ()
+fun True = ()
+fun _    = ()
diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T
index d58c182f8e..7e70f3aa10 100644
--- a/testsuite/tests/pmcheck/complete_sigs/all.T
+++ b/testsuite/tests/pmcheck/complete_sigs/all.T
@@ -13,5 +13,14 @@ test('completesig12', normal, compile, [''])
 test('completesig13', normal, compile, [''])
 test('completesig14', normal, compile, [''])
 test('completesig15', normal, compile_fail, [''])
+test('T13021', normal, compile, [''])
+test('T13363a', normal, compile, [''])
+test('T13363b', normal, compile, [''])
+test('T13717', expect_broken('13717'), compile, [''])
+test('T13964', normal, compile, [''])
+test('T13965', normal, compile, [''])
 test('T14059a', normal, compile, [''])
-test('T14253', expect_broken(14253), compile, [''])
+test('T14059b', expect_broken('14059'), compile, [''])
+test('T14253', normal, compile, [''])
+test('T14851', normal, compile, [''])
+test('T17149', normal, compile, [''])
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig01.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig01.stderr
new file mode 100644
index 0000000000..63cff81b5b
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig01.stderr
@@ -0,0 +1,4 @@
+
+completesig01.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘b’: b C = ...
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig02.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig02.stderr
index 25b24fd836..6da127a674 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig02.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig02.stderr
@@ -1,4 +1,4 @@
 
 completesig02.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In an equation for ‘a’: Patterns not matched: _
+    In an equation for ‘a’: Patterns not matched: ()
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr
index 50bc9bfebf..66a7604ca9 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig06.stderr
@@ -18,8 +18,8 @@ completesig06.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘m4’:
         Patterns not matched:
-            B D
             A D
+            B D
 
 completesig06.hs:29:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig07.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig07.stderr
index bf5edb9205..b8e56892c9 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig07.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig07.stderr
@@ -1,4 +1,12 @@
 
+completesig07.hs:14:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m1’: m1 A = ...
+
+completesig07.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m2’: m2 A D = ...
+
 completesig07.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘m3’:
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig08.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig08.stderr
new file mode 100644
index 0000000000..2c7d6658e7
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig08.stderr
@@ -0,0 +1,20 @@
+
+completesig08.hs:15:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m1’: m1 C = ...
+
+completesig08.hs:20:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m2’: m2 C D = ...
+
+completesig08.hs:25:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m3’: m3 A E = ...
+
+completesig08.hs:26:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m3’: m3 A F = ...
+
+completesig08.hs:30:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m4’: m4 E = ...
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig10.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig10.stderr
index 3d97bb47d7..36b367068c 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig10.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig10.stderr
@@ -1,4 +1,12 @@
 
+completesig10.hs:15:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m1’: m1 C = ...
+
+completesig10.hs:16:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘m1’: m1 D = ...
+
 completesig10.hs:20:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘m2’: Patterns not matched: A
diff --git a/testsuite/tests/pmcheck/complete_sigs/completesig11.stderr b/testsuite/tests/pmcheck/complete_sigs/completesig11.stderr
index 8107071008..d7bf2f3079 100644
--- a/testsuite/tests/pmcheck/complete_sigs/completesig11.stderr
+++ b/testsuite/tests/pmcheck/complete_sigs/completesig11.stderr
@@ -1,4 +1,4 @@
 
 completesig11.hs:14:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
-    In an equation for ‘m1’: Patterns not matched: BS
+    In an equation for ‘m1’: Patterns not matched: B
diff --git a/testsuite/tests/pmcheck/should_compile/CaseOfKnownCon.hs b/testsuite/tests/pmcheck/should_compile/CaseOfKnownCon.hs
new file mode 100644
index 0000000000..0933baae96
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/CaseOfKnownCon.hs
@@ -0,0 +1,8 @@
+-- | Ideally, we want the pattern match in `f` to be discovered as exhaustive,
+-- with a redundant match on the second clause.
+module Lib where
+
+f :: ()
+f = case (True, False) of
+  (True, False) -> ()
+  (True, True) -> ()
diff --git a/testsuite/tests/pmcheck/should_compile/CaseOfKnownCon.stderr b/testsuite/tests/pmcheck/should_compile/CaseOfKnownCon.stderr
new file mode 100644
index 0000000000..1f09323956
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/CaseOfKnownCon.stderr
@@ -0,0 +1,4 @@
+
+CaseOfKnownCon.hs:8:3: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: (True, True) -> ...
diff --git a/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
index fde022c5cb..3f37b66b54 100644
--- a/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
+++ b/testsuite/tests/pmcheck/should_compile/CyclicSubst.hs
@@ -1,5 +1,5 @@
 -- | The following match demonstrates why we need to detect cyclic solutions
--- when extending 'TmOracle.tm_pos'.
+-- when extending 'PmOracle.tm_pos'.
 --
 -- TLDR; solving @x :-> y@ where @x@ is the representative of @y@'s equivalence
 -- class can easily lead to a cycle in the substitution.
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
index 53be507400..8cedcddaf5 100644
--- a/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
@@ -1,3 +1,4 @@
+
 EmptyCase005.hs:24:8: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: (Void3 _)
diff --git a/testsuite/tests/pmcheck/should_compile/PmExprVars.hs b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
index 7b17cd5b66..fc95d43246 100644
--- a/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
+++ b/testsuite/tests/pmcheck/should_compile/PmExprVars.hs
@@ -1,20 +1,5 @@
 module PmExprVars where
 
--- | Demonstrates why we can't lower constructors as flexible meta variables.
--- If we did, we'd get a warning that cases 1 and 2 were redundant, implying
--- cases 0 and 3 are not. Arguably this might be better than not warning at
--- all, but it's very surprising having to supply the third case but not the
--- first two cases. And it's probably buggy somwhere else. Delete this when we
--- detect that all but the last case is redundant.
-consAreRigid :: Int
-consAreRigid = case False of
-  False -> case False of
-    False -> 0
-    True -> 1
-  True -> case False of
-    False -> 2
-    True -> 3
-
 data D a = A | B
 
 class C a where
diff --git a/testsuite/tests/pmcheck/should_compile/T11336b.hs b/testsuite/tests/pmcheck/should_compile/T11336b.hs
new file mode 100644
index 0000000000..37734eabb6
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T11336b.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- | Derived from T11336. Note that the pattern synonym makes it so that the
+-- pattern match checker can't see any complete sets: It only sees @s a@
+-- instead of @Proxy a@ for the match in 'PProxy'.
+module Bug where
+
+import Data.Proxy
+
+class Prj s where
+  prj :: Proxy a -> s a
+
+instance Prj Proxy where
+  prj = id
+
+pattern PProxy :: Prj s => s a -> Proxy a
+pattern PProxy s <- (prj -> s)
+
+-- | Although this is technically a complete match, the pattern match checker
+-- can't in general look through the pattern synonym. So, it should warn that
+-- some pattern wasn't matched. It should still flag the redundant second
+-- clause, though!
+fun :: Proxy a -> ()
+fun (PProxy Proxy) = ()
+fun (PProxy Proxy) = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T11336b.stderr b/testsuite/tests/pmcheck/should_compile/T11336b.stderr
new file mode 100644
index 0000000000..5d479c3756
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T11336b.stderr
@@ -0,0 +1,4 @@
+
+T11336b.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘fun’: Patterns not matched: _
diff --git a/testsuite/tests/pmcheck/should_compile/T15753c.hs b/testsuite/tests/pmcheck/should_compile/T15753c.hs
new file mode 100644
index 0000000000..d04a889e00
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15753c.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+module Bug where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..))
+import Data.Void (Void)
+
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+data SUnit :: () -> Type where
+  SUnit :: SUnit '()
+
+type family IsUnit (u :: ()) :: Bool where
+  IsUnit '() = True
+
+sIsUnit :: SUnit u -> SBool (IsUnit u)
+sIsUnit SUnit = STrue
+
+type family If (c :: Bool) (t :: Type) (f :: Type) :: Type where
+  If True  t _ = t
+  If False _ f = f
+
+type family F (u1 :: ()) (u2 :: ()) :: Type where
+  F u1 u2 =
+    If (IsUnit u1) (Case u2) Int
+
+type family Case (u :: ()) :: Type where
+  Case '() = Int
+
+g1 :: F u1 u2 :~: Char
+   -> SUnit u1 -> SUnit u2
+   -> Void
+g1 Refl su1 su2
+  | STrue <- sIsUnit su1
+  = case su2 of {}
+
+g2 :: F u1 u2 :~: Char
+   -> SUnit u1 -> SUnit u2
+   -> Void
+g2 Refl su1 su2
+  = case sIsUnit su1 of
+      STrue ->
+        case su2 of {}
+
diff --git a/testsuite/tests/pmcheck/should_compile/T15753d.hs b/testsuite/tests/pmcheck/should_compile/T15753d.hs
new file mode 100644
index 0000000000..5935cf7d9d
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T15753d.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
+module Bug where
+
+import Data.Kind
+import Data.Type.Bool
+import Data.Type.Equality ((:~:)(..))
+import Data.Void
+
+data family Sing :: forall k. k -> Type
+data instance Sing :: Bool -> Type where
+  SFalse :: Sing False
+  STrue  :: Sing True
+data instance Sing :: forall a. [a] -> Type where
+  SNil  :: Sing '[]
+  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+data instance Sing :: forall a b. (a, b) -> Type where
+  STuple2 :: Sing x -> Sing y -> Sing '(x, y)
+newtype instance Sing (f :: k1 ~> k2) =
+  SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family (f :: k1 ~> k2) @@ (x :: k1) :: k2
+infixl 9 @@
+
+newtype Map k v = MkMap [(k, v)]
+data instance Sing :: forall k v. Map k v -> Type where
+  SMkMap :: Sing x -> Sing (MkMap x)
+
+type family MapEmpty :: Map k v where
+  MapEmpty = MkMap '[]
+
+type family MapInsertWith (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v) :: Map k v where
+  MapInsertWith _ new_k new_v (MkMap '[]) = MkMap '[ '(new_k, new_v)]
+  MapInsertWith f new_k new_v (MkMap ('(old_k,old_v):old_kvs)) =
+    If (old_k == new_k)
+       (MkMap ('(new_k,f @@ new_v @@ old_v):old_kvs))
+       (Case (MapInsertWith f new_k new_v (MkMap old_kvs)) old_k old_v)
+
+type family Case (m :: Map k v) (old_k :: k) (old_v :: v) :: Map k v where
+  Case (MkMap kvs) old_k old_v = MkMap ('(old_k,old_v) : kvs)
+
+sMapInsertWith :: forall k v (f :: v ~> v ~> v) (new_k :: k) (new_v :: v) (m :: Map k v).
+                  SEq k
+               => Sing f -> Sing new_k -> Sing new_v -> Sing m
+               -> Sing (MapInsertWith f new_k new_v m)
+sMapInsertWith _  snew_k snew_v (SMkMap SNil) = SMkMap (STuple2 snew_k snew_v `SCons` SNil)
+sMapInsertWith sf snew_k snew_v (SMkMap (STuple2 sold_k sold_v `SCons` sold_kvs)) =
+  case sold_k %== snew_k of
+    STrue -> SMkMap (STuple2 snew_k (sf @@ snew_v @@ sold_v) `SCons` sold_kvs)
+    SFalse ->
+      case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of
+        SMkMap skvs -> SMkMap (STuple2 sold_k sold_v `SCons` skvs)
+
+class PEq a where
+  type (x :: a) == (y :: a) :: Bool
+class SEq a where
+  (%==) :: forall (x :: a) (y :: a).
+           Sing x -> Sing y -> Sing (x == y)
+
+mapInsertWithNonEmpty1 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])
+                                     (new_k :: k) (new_v :: v) (m :: Map k v).
+                          SEq k
+                       => Sing f -> Sing new_k -> Sing new_v -> Sing m
+                       -> m :~: MkMap ('(old_k,old_v) : old_kvs)
+                       -> MapInsertWith f new_k new_v m :~: MapEmpty
+                       -> Void
+mapInsertWithNonEmpty1 sf snew_k snew_v (SMkMap sm) Refl Refl
+  | STuple2 sold_k _ `SCons` sold_kvs <- sm
+  , SFalse <- sold_k %== snew_k
+  = case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}
+
+mapInsertWithNonEmpty2 :: forall k v (f :: v ~> v ~> v) (old_k :: k) (old_v :: v) (old_kvs :: [(k,v)])
+                                     (new_k :: k) (new_v :: v) (m :: Map k v).
+                          SEq k
+                       => Sing f -> Sing new_k -> Sing new_v -> Sing m
+                       -> m :~: MkMap ('(old_k,old_v) : old_kvs)
+                       -> MapInsertWith f new_k new_v m :~: MapEmpty
+                       -> Void
+mapInsertWithNonEmpty2 sf snew_k snew_v (SMkMap sm) Refl Refl
+  | STuple2 sold_k _ `SCons` sold_kvs <- sm
+  = case sold_k %== snew_k of
+      SFalse ->
+        case sMapInsertWith sf snew_k snew_v (SMkMap sold_kvs) of {}
+
diff --git a/testsuite/tests/pmcheck/should_compile/T17096.hs b/testsuite/tests/pmcheck/should_compile/T17096.hs
new file mode 100755
index 0000000000..5fc4e6e879
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T17096.hs
@@ -0,0 +1,319 @@
+{-# language PatternSynonyms #-}
+-- Taken from the Dhall library
+module T17096 where
+
+data Expr s a
+    = Const String
+    | Var Int
+    | Lam String (Expr s a) (Expr s a)
+    | Pi  String (Expr s a) (Expr s a)
+    | App (Expr s a) (Expr s a)
+    | Let String (Maybe (Expr s a)) (Expr s a) (Expr s a)
+    | Annot (Expr s a) (Expr s a)
+    | Bool
+    | BoolLit Bool
+    | BoolAnd (Expr s a) (Expr s a)
+    | BoolOr  (Expr s a) (Expr s a)
+    | BoolEQ  (Expr s a) (Expr s a)
+    | BoolNE  (Expr s a) (Expr s a)
+    | BoolIf (Expr s a) (Expr s a) (Expr s a)
+    | Natural
+    | NaturalLit Integer
+    | NaturalFold
+    | NaturalBuild
+    | NaturalIsZero
+    | NaturalEven
+    | NaturalOdd
+    | NaturalToInteger
+    | NaturalShow
+    | NaturalSubtract
+    | NaturalPlus (Expr s a) (Expr s a)
+    | NaturalTimes (Expr s a) (Expr s a)
+    | Integer
+    | IntegerLit Integer
+    | IntegerShow
+    | IntegerToDouble
+    | Double
+    | DoubleLit Double
+    | DoubleShow
+    | String
+    | StringLit String
+    | StringAppend (Expr s a) (Expr s a)
+    | StringShow
+    | List
+    | ListLit (Maybe (Expr s a)) [Expr s a]
+    | ListAppend (Expr s a) (Expr s a)
+    | ListBuild
+    | ListFold
+    | ListLength
+    | ListHead
+    | ListLast
+    | ListIndexed
+    | ListReverse
+    | Optional
+    | Some (Expr s a)
+    | None
+    | OptionalFold
+    | OptionalBuild
+    | Record    [(String, Expr s a)]
+    | RecordLit [(String, Expr s a)]
+    | Union     [(String, Maybe (Expr s a))]
+    | Combine (Expr s a) (Expr s a)
+    | CombineTypes (Expr s a) (Expr s a)
+    | Prefer (Expr s a) (Expr s a)
+    | Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
+    | ToMap (Expr s a) (Maybe (Expr s a))
+    | Field (Expr s a) String
+    | Project (Expr s a) (Either [String] (Expr s a))
+    | Assert (Expr s a)
+    | Equivalent (Expr s a) (Expr s a)
+    | Note s (Expr s a)
+    | ImportAlt (Expr s a) (Expr s a)
+    | Embed a
+
+isNormalized :: Eq a => Expr s a -> Bool
+isNormalized = loop
+  where
+    loop e = case e of
+      Const _ -> True
+      Var _ -> True
+      Lam _ a b -> loop a && loop b
+      Pi _ a b -> loop a && loop b
+      App f a -> loop f && loop a && case App f a of
+          App (Lam _ _ _) _ -> False
+          App (App ListBuild _) (App (App ListFold _) _) -> False
+          App NaturalBuild (App NaturalFold _) -> False
+          App (App OptionalBuild _) (App (App OptionalFold _) _) -> False
+          App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
+          App NaturalFold (NaturalLit _) -> False
+          App NaturalBuild _ -> False
+          App NaturalIsZero (NaturalLit _) -> False
+          App NaturalEven (NaturalLit _) -> False
+          App NaturalOdd (NaturalLit _) -> False
+          App NaturalShow (NaturalLit _) -> False
+          App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False
+          App (App NaturalSubtract (NaturalLit 0)) _ -> False
+          App (App NaturalSubtract _) (NaturalLit 0) -> False
+          App (App NaturalSubtract x) y -> not (undefined x y)
+          App NaturalToInteger (NaturalLit _) -> False
+          App IntegerShow (IntegerLit _) -> False
+          App IntegerToDouble (IntegerLit _) -> False
+          App DoubleShow (DoubleLit _) -> False
+          App (App OptionalBuild _) _ -> False
+          App (App ListBuild _) _ -> False
+          App (App (App (App (App ListFold _) (ListLit _ _)) _) _) _ ->
+              False
+          App (App ListLength _) (ListLit _ _) -> False
+          App (App ListHead _) (ListLit _ _) -> False
+          App (App ListLast _) (ListLit _ _) -> False
+          App (App ListIndexed _) (ListLit _ _) -> False
+          App (App ListReverse _) (ListLit _ _) -> False
+          App (App (App (App (App OptionalFold _) (Some _)) _) _) _ ->
+              False
+          App (App (App (App (App OptionalFold _) (App None _)) _) _) _ ->
+              False
+          App StringShow (StringLit _) ->
+              False
+          _ -> True
+      Let _ _ _ _ -> False
+      Annot _ _ -> False
+      Bool -> True
+      BoolLit _ -> True
+      BoolAnd x y -> loop x && loop y && decide x y
+        where
+          decide (BoolLit _)  _          = False
+          decide  _          (BoolLit _) = False
+          decide  l           r          = not (undefined l r)
+      BoolOr x y -> loop x && loop y && decide x y
+        where
+          decide (BoolLit _)  _          = False
+          decide  _          (BoolLit _) = False
+          decide  l           r          = not (undefined l r)
+      BoolEQ x y -> loop x && loop y && decide x y
+        where
+          decide (BoolLit True)  _             = False
+          decide  _             (BoolLit True) = False
+          decide  l              r             = not (undefined l r)
+      BoolNE x y -> loop x && loop y && decide x y
+        where
+          decide (BoolLit False)  _               = False
+          decide  _              (BoolLit False ) = False
+          decide  l               r               = not (undefined l r)
+      BoolIf x y z ->
+          loop x && loop y && loop z && decide x y z
+        where
+          decide (BoolLit _)  _              _              = False
+          decide  _          (BoolLit True) (BoolLit False) = False
+          decide  _           l              r              = not (undefined l r)
+      Natural -> True
+      NaturalLit _ -> True
+      NaturalFold -> True
+      NaturalBuild -> True
+      NaturalIsZero -> True
+      NaturalEven -> True
+      NaturalOdd -> True
+      NaturalShow -> True
+      NaturalSubtract -> True
+      NaturalToInteger -> True
+      NaturalPlus x y -> loop x && loop y && decide x y
+        where
+          decide (NaturalLit 0)  _             = False
+          decide  _             (NaturalLit 0) = False
+          decide (NaturalLit _) (NaturalLit _) = False
+          decide  _              _             = True
+      NaturalTimes x y -> loop x && loop y && decide x y
+        where
+          decide (NaturalLit 0)  _             = False
+          decide  _             (NaturalLit 0) = False
+          decide (NaturalLit 1)  _             = False
+          decide  _             (NaturalLit 1) = False
+          decide (NaturalLit _) (NaturalLit _) = False
+          decide  _              _             = True
+      Integer -> True
+      IntegerLit _ -> True
+      IntegerShow -> True
+      IntegerToDouble -> True
+      Double -> True
+      DoubleLit _ -> True
+      DoubleShow -> True
+      String -> True
+      StringLit _ -> False
+      StringAppend _ _ -> False
+      StringShow -> True
+      List -> True
+      ListLit t es -> all loop t && all loop es
+      ListAppend x y -> loop x && loop y && decide x y
+        where
+          decide (ListLit _ m)  _            | null m = False
+          decide  _            (ListLit _ n) | null n = False
+          decide (ListLit _ _) (ListLit _ _)          = False
+          decide  _             _                     = True
+      ListBuild -> True
+      ListFold -> True
+      ListLength -> True
+      ListHead -> True
+      ListLast -> True
+      ListIndexed -> True
+      ListReverse -> True
+      Optional -> True
+      Some a -> loop a
+      None -> True
+      OptionalFold -> True
+      OptionalBuild -> True
+      Record kts -> undefined kts && all loop (map snd kts)
+      RecordLit kvs -> undefined kvs && all loop (map snd kvs)
+      Union kts -> undefined kts && all (all loop) (map snd kts)
+      Combine x y -> loop x && loop y && decide x y
+        where
+          decide (RecordLit m) _ | null m = False
+          decide _ (RecordLit n) | null n = False
+          decide (RecordLit _) (RecordLit _) = False
+          decide  _ _ = True
+      CombineTypes x y -> loop x && loop y && decide x y
+        where
+          decide (Record m) _ | null m = False
+          decide _ (Record n) | null n = False
+          decide (Record _) (Record _) = False
+          decide  _ _ = True
+      Prefer x y -> loop x && loop y && decide x y
+        where
+          decide (RecordLit m) _ | null m = False
+          decide _ (RecordLit n) | null n = False
+          decide (RecordLit _) (RecordLit _) = False
+          decide l r = not (undefined l r)
+      Merge x y t -> loop x && loop y && all loop t
+      ToMap x t -> case x of
+          RecordLit _ -> False
+          _ -> loop x && all loop t
+      Field r k -> case r of
+          RecordLit _ -> False
+          Project _ _ -> False
+          Prefer (RecordLit m) _ -> map fst m == [k] && loop r
+          Prefer _ (RecordLit _) -> False
+          Combine (RecordLit m) _ -> map fst m == [k] && loop r
+          Combine _ (RecordLit m) -> map fst m == [k] && loop r
+          _ -> loop r
+      Project r p -> loop r &&
+          case p of
+              Left s -> case r of
+                  RecordLit _ -> False
+                  _ -> not (null s) && undefined s
+              Right e' -> case e' of
+                  Record _ -> False
+                  _ -> loop e'
+      Assert t -> loop t
+      Equivalent l r -> loop l && loop r
+      Note _ e' -> loop e'
+      ImportAlt l _r -> loop l
+      Embed _ -> True
+
+{-# COMPLETE
+      Let'
+    , Const
+    , Var
+    , Lam
+    , Pi
+    , App
+    , Annot
+    , Bool
+    , BoolLit
+    , BoolAnd
+    , BoolOr
+    , BoolEQ
+    , BoolNE
+    , BoolIf
+    , Natural
+    , NaturalLit
+    , NaturalFold
+    , NaturalBuild
+    , NaturalIsZero
+    , NaturalEven
+    , NaturalOdd
+    , NaturalToInteger
+    , NaturalShow
+    , NaturalSubtract
+    , NaturalPlus
+    , NaturalTimes
+    , Integer
+    , IntegerLit
+    , IntegerShow
+    , IntegerToDouble
+    , Double
+    , DoubleLit
+    , DoubleShow
+    , String
+    , StringLit
+    , StringAppend
+    , StringShow
+    , List
+    , ListLit
+    , ListAppend
+    , ListBuild
+    , ListFold
+    , ListLength
+    , ListHead
+    , ListLast
+    , ListIndexed
+    , ListReverse
+    , Optional
+    , Some
+    , None
+    , OptionalFold
+    , OptionalBuild
+    , Record
+    , RecordLit
+    , Union
+    , Combine
+    , CombineTypes
+    , Prefer
+    , Merge
+    , ToMap
+    , Field
+    , Project
+    , Assert
+    , Equivalent
+    , Note
+    , ImportAlt
+    , Embed
+ #-}
+pattern Let' x mA a b = Let x mA a b
diff --git a/testsuite/tests/pmcheck/should_compile/T2204.stderr b/testsuite/tests/pmcheck/should_compile/T2204.stderr
index c2e2251fc9..26f70352e2 100644
--- a/testsuite/tests/pmcheck/should_compile/T2204.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T2204.stderr
@@ -3,10 +3,10 @@ T2204.hs:6:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
         Patterns not matched:
-            []
-            (p:_) where p is not one of {'0'}
-            ['0']
+            ('0':'1':_:_)
             ('0':p:_) where p is not one of {'1'}
+            ['0']
+            (p:_) where p is not one of {'0'}
             ...
 
 T2204.hs:9:1: warning: [-Wincomplete-patterns (in -Wextra)]
diff --git a/testsuite/tests/pmcheck/should_compile/T9951b.stderr b/testsuite/tests/pmcheck/should_compile/T9951b.stderr
index ff6696b466..e4e337b153 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:
-            []
-            (p:_) where p is not one of {'a'}
-            ['a']
+            ('a':'b':_:_)
             ('a':p:_) where p is not one of {'b'}
+            ['a']
+            (p:_) where p is not one of {'a'}
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 87874f81c8..5a24832945 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -68,14 +68,20 @@ test('T15584', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15713', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
-test('T15753a', expect_broken(15753), compile,
+test('T15753a', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15753b', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15753c', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T15753d', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15884', expect_broken(15884), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T16289', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T17096', collect_compiler_stats('bytes allocated',10), compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
 test('T17112', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
@@ -94,8 +100,14 @@ test('pmc006', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('pmc007', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc008', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('pmc009', [], compile,
+     ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11245', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T11336b', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T12949', [],  compile, ['-fwarn-overlapping-patterns'])
 test('T12957', [], compile, ['-fwarn-overlapping-patterns'])
 test('T12957a', [], compile, ['-fwarn-overlapping-patterns'])
@@ -103,6 +115,8 @@ test('PmExprVars', [],  compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('CyclicSubst', [],  compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('CaseOfKnownCon', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # EmptyCase
 test('T10746', [], compile,
diff --git a/testsuite/tests/pmcheck/should_compile/pmc007.stderr b/testsuite/tests/pmcheck/should_compile/pmc007.stderr
index f6e4ece88c..d4bbe8fb73 100644
--- a/testsuite/tests/pmcheck/should_compile/pmc007.stderr
+++ b/testsuite/tests/pmcheck/should_compile/pmc007.stderr
@@ -2,24 +2,24 @@
 pmc007.hs:7:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’:
-        Patterns not matched: p where p is not one of {"ac", "ab"}
+        Patterns not matched: p where p is not one of {"ab", "ac"}
 
 pmc007.hs:12:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In an equation for ‘g’:
         Patterns not matched:
-            []
-            (p:_) where p is not one of {'a'}
+            ('a':'b':_:_)
+            ('a':'c':_:_)
+            ('a':p:_) where p is not one of {'b', 'c'}
             ['a']
-            ('a':p:_) where p is not one of {'c', 'b'}
             ...
 
 pmc007.hs:18:11: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative:
         Patterns not matched:
-            []
-            (p:_) where p is not one of {'a'}
+            ('a':'b':_:_)
+            ('a':'c':_:_)
+            ('a':p:_) where p is not one of {'b', 'c'}
             ['a']
-            ('a':p:_) where p is not one of {'c', 'b'}
             ...
diff --git a/testsuite/tests/pmcheck/should_compile/pmc008.hs b/testsuite/tests/pmcheck/should_compile/pmc008.hs
new file mode 100644
index 0000000000..29e39b573b
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/pmc008.hs
@@ -0,0 +1,9 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
+
+module PMC008 where
+
+-- complete match, but because of the guard, the information that `x` is not
+-- `Just` has to flow through the term oracle.
+foo :: Maybe Int -> Int
+foo x | Just y <- x = y
+foo Nothing = 43
diff --git a/testsuite/tests/pmcheck/should_compile/pmc009.hs b/testsuite/tests/pmcheck/should_compile/pmc009.hs
new file mode 100644
index 0000000000..ac8f5c2dd5
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/pmc009.hs
@@ -0,0 +1,12 @@
+module HsUtils where
+import HsBinds
+import SrcLoc
+
+
+-- | We have to be careful to normalise @SrcSpanLess (LHsBind)@ to
+-- @LHsBindLR l r@ before passing the representative of @unLoc bind@ on to
+-- @mkOneConFull@, otherwise this triggers a panic in @zipTvSubst@.
+addPatSynSelector:: LHsBind p -> [a]
+addPatSynSelector bind
+  | PatSynBind _ _ <- unLoc bind
+  = []
diff --git a/testsuite/tests/pmcheck/should_compile/pmc009.stderr b/testsuite/tests/pmcheck/should_compile/pmc009.stderr
new file mode 100644
index 0000000000..8eaa4ab61a
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/pmc009.stderr
@@ -0,0 +1,4 @@
+
+pmc009.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘addPatSynSelector’: Patterns not matched: _
diff --git a/testsuite/tests/th/TH_repUnboxedTuples.stderr b/testsuite/tests/th/TH_repUnboxedTuples.stderr
index 5b1f2b386e..8439b12547 100644
--- a/testsuite/tests/th/TH_repUnboxedTuples.stderr
+++ b/testsuite/tests/th/TH_repUnboxedTuples.stderr
@@ -7,3 +7,7 @@ case (# 'b', GHC.Types.False #) of
 TH_repUnboxedTuples.hs:18:13: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
     In a case alternative: (# 'a', True #) -> ...
+
+TH_repUnboxedTuples.hs:18:13: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: (# _, _ #) -> ...
diff --git a/testsuite/tests/typecheck/should_compile/Vta2.stderr b/testsuite/tests/typecheck/should_compile/Vta2.stderr
new file mode 100644
index 0000000000..0598cc0226
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/Vta2.stderr
@@ -0,0 +1,4 @@
+
+Vta2.hs:14:17: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In a case alternative: False -> ...