Exhaustiveness check for EmptyCase (Trac #10746)

Empty case expressions have strict semantics so the problem boils down
to inhabitation checking for the type of the scrutinee. 3 main functions
added:

- pmTopNormaliseType_maybe for the normalisation of the scrutinee type

- inhabitationCandidates for generating the possible patterns of the
  appropriate type

- checkEmptyCase' to filter out the candidates that give rise to
  unsatisfiable constraints.

See Note [Checking EmptyCase Expressions] in Check
and Note [Type normalisation for EmptyCase] in FamInstEnv

Test Plan: validate

Reviewers: simonpj, goldfire, dfeuer, austin, bgamari

Reviewed By: bgamari

Subscribers: mpickering, thomie

Differential Revision: https://phabricator.haskell.org/D2105

GHC Trac Issues: #10746

23 files changed, 831 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase001.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase001.hs
new file mode 100644
index 0000000000..99e414d357
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase001.hs
@@ -0,0 +1,18 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns  #-}
+{-# LANGUAGE EmptyCase, LambdaCase          #-}
+
+-- Check some predefined types
+module EmptyCase001 where
+
+-- Non-exhaustive with *infinite* inhabitants
+f1 :: Int -> a
+f1 = \case
+
+-- Non-exhaustive. Since a string is just a list of characters
+-- (that is, an algebraic type), we have [] and (_:_) as missing.
+f2 :: String -> a
+f2 x = case x of {}
+
+-- Non-exhaustive (do not unfold the alternatives)
+f3 :: Char -> a
+f3 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr
new file mode 100644
index 0000000000..ba9e61fc51
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase001.stderr
@@ -0,0 +1,14 @@
+EmptyCase001.hs:9:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Int
+
+EmptyCase001.hs:14:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            []
+            (_:_)
+
+EmptyCase001.hs:18:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Char
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase002.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase002.hs
new file mode 100644
index 0000000000..8af96be77c
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase002.hs
@@ -0,0 +1,54 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns  #-}
+{-# LANGUAGE EmptyCase, LambdaCase          #-}
+{-# LANGUAGE GADTs, TypeFamilies            #-}
+
+-- Check some newtypes, in combination with GADTs and TypeFamilies
+module EmptyCase002 where
+
+newtype T = MkT H
+newtype G = MkG T
+newtype H = MkH G
+
+-- Exhaustive but it cannot be detected.
+f1 :: T -> a
+f1 = \case
+
+data A
+
+data B = B1 | B2
+
+data C :: * -> * where
+  C1 :: C Int
+  C2 :: C Bool
+
+data D :: * -> * -> * where
+  D1 :: D Int  Bool
+  D2 :: D Bool Char
+
+type family E (a :: *) :: * where
+  E Int  = Bool
+  E Bool = Char
+
+newtype T1 a = MkT1 a
+newtype T2 b = MkT2 b
+
+-- Exhaustive
+f2 :: T1 A -> z
+f2 = \case
+
+-- Non-exhaustive. Missing cases: MkT1 B1, MkT1 B2
+f3 :: T1 B -> z
+f3 = \case
+
+-- Non-exhaustive. Missing cases: MkT1 False, MkT1 True
+f4 :: T1 (E Int) -> z
+f4 = \case
+
+-- Non-exhaustive. Missing cases: MkT1 (MkT2 (MkT1 D2))
+f5 :: T1 (T2 (T1 (D (E Int) (E (E Int))))) -> z
+f5 = \case
+
+-- Exhaustive. Not an EmptyCase but good to have for
+-- comparison with the example above
+f6 :: T1 (T2 (T1 (D (E Int) (E (E Int))))) -> ()
+f6 = \case MkT1 (MkT2 (MkT1 D2)) -> ()
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr
new file mode 100644
index 0000000000..8979fda155
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase002.stderr
@@ -0,0 +1,22 @@
+EmptyCase002.hs:14:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (MkT _)
+
+EmptyCase002.hs:41:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (MkT1 B1)
+            (MkT1 B2)
+
+EmptyCase002.hs:45:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (MkT1 False)
+            (MkT1 True)
+
+EmptyCase002.hs:49:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched: (MkT1 (MkT2 (MkT1 D2)))
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase003.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase003.hs
new file mode 100644
index 0000000000..14f5c60747
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase003.hs
@@ -0,0 +1,95 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns      #-}
+{-# LANGUAGE EmptyCase, LambdaCase              #-}
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+
+-- Check some type families and type synonyms
+module EmptyCase003 where
+
+type family A (a :: *) :: *
+
+-- Conservatively considered non-exhaustive (A a missing),
+-- since A a does not reduce to anything.
+f1 :: A a -> a -> b
+f1 = \case
+
+data Void
+
+type family B (a :: *) :: *
+type instance B a = Void
+
+-- Exhaustive
+f2 :: B a -> b
+f2 = \case
+
+type family C (a :: *) :: *
+type instance C Int  = Char
+type instance C Bool = Void
+
+-- Non-exhaustive (C a missing, no info about `a`)
+f3 :: C a -> a -> b
+f3 = \case
+
+-- Non-exhaustive (_ :: Char missing): C Int rewrites
+-- to Char (which is trivially inhabited)
+f4 :: C Int -> a
+f4 = \case
+
+-- Exhaustive: C Bool rewrites to Void
+f5 :: C Bool -> a
+f5 = \case
+
+-- type family D (a :: *) :: *
+-- type instance D x = D x -- non-terminating
+--
+-- -- Exhaustive but *impossible* to detect that, since rewriting
+-- -- D Int does not terminate (the checker should loop).
+-- f6 :: D Int -> a
+-- f6 = \case
+
+data Zero
+data Succ n
+
+type TenC n = Succ (Succ (Succ (Succ (Succ
+             (Succ (Succ (Succ (Succ (Succ n)))))))))
+
+type Ten = TenC Zero
+
+type Hundred = TenC (TenC (TenC (TenC (TenC
+              (TenC (TenC (TenC (TenC (TenC Zero)))))))))
+
+type family E (n :: *) (a :: *) :: *
+type instance E Zero     b = b
+type instance E (Succ n) b = E n b
+
+-- Exhaustive (10 rewrites)
+f7 :: E Ten Void -> b
+f7 = \case
+
+-- Exhaustive (100 rewrites)
+f8 :: E Hundred Void -> b
+f8 = \case
+
+type family Add (a :: *) (b :: *) :: *
+type instance Add Zero     m = m
+type instance Add (Succ n) m = Succ (Add n m)
+
+type family Mult (a :: *) (b :: *) :: *
+type instance Mult Zero     m = Zero
+type instance Mult (Succ n) m = Add m (Mult n m)
+
+type Five = Succ (Succ (Succ (Succ (Succ Zero))))
+type Four = Succ (Succ (Succ (Succ Zero)))
+
+-- Exhaustive (80 rewrites)
+f9 :: E (Mult Four (Mult Four Five)) Void -> a
+f9 = \case
+
+-- This gets killed on my dell
+--
+-- -- Exhaustive (390625 rewrites)
+-- f10 :: E (Mult (Mult (Mult Five Five)
+--                      (Mult Five Five))
+--                (Mult (Mult Five Five)
+--                      (Mult Five Five)))
+--          Void -> a
+-- f10 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
new file mode 100644
index 0000000000..8db12ac5b5
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase003.stderr
@@ -0,0 +1,11 @@
+EmptyCase003.hs:13:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: A a
+
+EmptyCase003.hs:30:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: C a
+
+EmptyCase003.hs:35:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Char
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase004.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase004.hs
new file mode 100644
index 0000000000..31ba020c33
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase004.hs
@@ -0,0 +1,49 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE GADTs, KindSignatures, EmptyCase, LambdaCase #-}
+
+-- Check some GADTs
+module EmptyCase004 where
+
+data A :: * -> * where
+  A1 :: A Int
+  A2 :: A Bool
+
+-- Non-exhaustive: Missing A2
+f1 :: A Bool -> a
+f1 = \case
+
+-- Non-exhaustive: missing both A1 & A2
+f2 :: A a -> b
+f2 = \case
+
+-- Exhaustive
+f3 :: A [a] -> b
+f3 = \case
+
+data B :: * -> * -> * where
+  B1 :: Int -> B Bool Bool
+  B2 ::        B Int  Bool
+
+-- Non-exhaustive: missing (B1 _)
+g1 :: B a a -> b
+g1 x = case x of
+
+-- Non-exhaustive: missing both (B1 _) & B2
+g2 :: B a b -> c
+g2 = \case
+
+-- Exhaustive
+g3 :: B Char a -> b
+g3 = \case
+
+-- NOTE: A lambda-case always has ONE scrutinee and a lambda case refers
+-- always to the first of the arguments. Hence, the following warnings are
+-- valid:
+
+-- Non-exhaustive: Missing both A1 & A2
+h1 :: A a -> A a -> b
+h1 = \case
+
+h2 :: A a -> B a b -> ()
+h2 A1 = \case -- Non-exhaustive, missing B2
+h2 A2 = \case -- Non-exhaustive, missing (B1 _)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr
new file mode 100644
index 0000000000..1e002e18c5
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase004.stderr
@@ -0,0 +1,36 @@
+EmptyCase004.hs:13:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: A2
+
+EmptyCase004.hs:17:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            A1
+            A2
+
+EmptyCase004.hs:29:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (B1 _)
+
+EmptyCase004.hs:33:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (B1 _)
+            B2
+
+EmptyCase004.hs:45:6: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            A1
+            A2
+
+EmptyCase004.hs:48:9: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: B2
+
+EmptyCase004.hs:49:9: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (B1 _)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase005.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase005.hs
new file mode 100644
index 0000000000..b05dd9d4af
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase005.hs
@@ -0,0 +1,101 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, EmptyCase, LambdaCase #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- Check some DataFamilies, warning appearance and other stuff
+module EmptyCase005 where
+
+data Void
+
+newtype Void2 = Void2 Void
+data    Void3 = Void3 Void
+
+-- Exhaustive
+f1 :: Void2 -> Bool
+f1 x = case x of {}
+-- > f1 undefined
+-- *** Exception: Prelude.undefined
+--
+-- > f1 (Void2 undefined)
+-- *** Exception: Prelude.undefined
+
+-- Non-exhaustive: missing (Void3 _)
+f2 :: Void3 -> Bool
+f2 x = case x of {}
+-- > f2 undefined
+-- *** Exception: Prelude.undefined
+--
+-- > f2 (Void3 undefined)
+-- *** Exception: Void.hs:31:7-10: Non-exhaustive patterns in case
+
+newtype V1 = V1 Void
+newtype V2 = V2 V1
+newtype V3 = V3 V2
+newtype V4 = V4 V3
+
+-- Exhaustive
+f3 :: V4 -> Bool
+f3 x = case x of {}
+-- > v undefined
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 undefined)
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 (V3 undefined))
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 (V3 (V2 undefined)))
+-- *** Exception: Prelude.undefined
+--
+-- > v (V4 (V3 (V2 (V1 undefined))))
+-- *** Exception: Prelude.undefined
+
+-- Exhaustive
+type family A a
+type instance A Bool = V4
+
+f4 :: A Bool -> Bool
+f4 x = case x of {}
+
+data family T a
+
+data instance T () = T1 | T2
+
+-- Non-exhaustive: missing both T1 & T2
+f5 :: T () -> Bool
+f5 x = case x of {}
+
+newtype instance T Bool = MkTBool Bool
+
+-- Non-exhaustive: missing both (MkTBool True) & (MkTBool False)
+f6 :: T Bool -> Bool
+f6 x = case x of {}
+
+newtype instance T Int = MkTInt Char
+
+-- Non-exhaustive: missing (MkTInt _)
+f7 :: T Int -> Bool
+f7 x = case x of {}
+
+newtype V = MkV Bool
+
+type family F a
+type instance F Bool = V
+
+type family G a
+type instance G Int = F Bool
+
+-- Non-exhaustive: missing MkV True & MkV False
+f8 :: G Int -> Bool
+f8 x = case x of {}
+
+type family H a
+type instance H Int  = H Bool
+type instance H Bool = H Char
+
+-- Non-exhaustive: missing (_ :: H Char)
+-- (H Int), (H Bool) and (H Char) are all the same and stuck, but we want to
+-- show the latest rewrite, that is, (H Char) and not (H Int) or (H Bool).
+f9 :: H Int -> Bool
+f9 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
new file mode 100644
index 0000000000..53be507400
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase005.stderr
@@ -0,0 +1,32 @@
+EmptyCase005.hs:24:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Void3 _)
+
+EmptyCase005.hs:67:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            T1
+            T2
+
+EmptyCase005.hs:73:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (MkTBool False)
+            (MkTBool True)
+
+EmptyCase005.hs:79:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (MkTInt _)
+
+EmptyCase005.hs:91:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (MkV False)
+            (MkV True)
+
+EmptyCase005.hs:101:8: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: H Char
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase006.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase006.hs
new file mode 100644
index 0000000000..bf902b766d
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase006.hs
@@ -0,0 +1,28 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE GADTs, KindSignatures, EmptyCase, LambdaCase #-}
+
+-- Check interaction between Newtypes and GADTs
+module EmptyCase006 where
+
+data GA :: * -> * where
+  MkGA1 :: GA Int
+  MkGA2 :: GA a -> GA [a]
+  MkGA3 :: GA (a,a)
+
+newtype Foo1 a = Foo1 (GA a)
+
+-- Non-exhaustive. Missing: Foo1 MkGA1
+f01 :: Foo1 Int -> ()
+f01 = \case
+
+-- Exhaustive
+f02 :: Foo1 (Int, Bool) -> ()
+f02 = \case
+
+-- Non-exhaustive. Missing: Foo1 MkGA1, Foo1 (MkGA2 _), Foo1 MkGA3
+f03 :: Foo1 a -> ()
+f03 = \case
+
+-- Exhaustive
+f04 :: Foo1 () -> ()
+f04 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr
new file mode 100644
index 0000000000..a1d372b14f
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase006.stderr
@@ -0,0 +1,11 @@
+EmptyCase006.hs:16:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Foo1 MkGA1)
+
+EmptyCase006.hs:24:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (Foo1 MkGA1)
+            (Foo1 (MkGA2 _))
+            (Foo1 MkGA3)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase007.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase007.hs
new file mode 100644
index 0000000000..71a3d2606c
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase007.hs
@@ -0,0 +1,46 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, EmptyCase, LambdaCase #-}
+
+-- Check interaction between Newtypes and Type Families
+module EmptyCase007 where
+
+type family FA a :: * -- just an open type family
+type instance FA Int     = (Char, Bool)
+type instance FA Char    = Char
+type instance FA [a]     = [FA a]
+type instance FA (a,b,b) = Void1
+
+newtype Foo2 a = Foo2 (FA a)
+
+data Void1
+
+-- Non-exhaustive. Missing: (_ :: Foo2 a) (no info about a)
+f05 :: Foo2 a -> ()
+f05 = \case
+
+-- Non-exhaustive. Missing: (_ :: Foo2 (a, a)) (does not reduce)
+f06 :: Foo2 (a, a) -> ()
+f06 = \case
+
+-- Exhaustive (reduces to Void)
+f07 :: Foo2 (Int, Char, Char) -> ()
+f07 = \case
+
+-- Non-exhaustive. Missing: Foo2 (_, _)
+f08 :: Foo2 Int -> ()
+f08 = \case
+
+-- Non-exhaustive. Missing: Foo2 _
+f09 :: Foo2 Char -> ()
+f09 = \case
+
+-- Non-exhaustive. Missing: (_ :: Char)
+-- This is a more general trick: If the warning gives you a constructor form
+-- and you don't know what the type of the underscore is, just match against
+-- the constructor form, and the warning you'll get will fill the type in.
+f09' :: Foo2 Char -> ()
+f09' (Foo2 x) = case x of {}
+
+-- Non-exhaustive. Missing: Foo2 [], Foo2 (_:_)
+f10 :: Foo2 [Int] -> ()
+f10 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
new file mode 100644
index 0000000000..822baee3bb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase007.stderr
@@ -0,0 +1,26 @@
+EmptyCase007.hs:19:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Foo2 a
+
+EmptyCase007.hs:23:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Foo2 (a, a)
+
+EmptyCase007.hs:31:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Foo2 (_, _))
+
+EmptyCase007.hs:35:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Foo2 _)
+
+EmptyCase007.hs:42:17: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Char
+
+EmptyCase007.hs:46:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (Foo2 [])
+            (Foo2 (_:_))
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase008.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase008.hs
new file mode 100644
index 0000000000..b1f6a0ae73
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase008.hs
@@ -0,0 +1,52 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyCase, LambdaCase #-}
+
+-- Check interaction between Newtypes and DataFamilies
+module EmptyCase008 where
+
+data family DA a
+
+newtype Foo3 a = Foo3 (DA a)
+
+data instance DA Int = MkDA1 Char | MkDA2
+
+-- Non-exhaustive. Missing: MkDA1 Char, MkDA2
+f11 :: Foo3 Int -> ()
+f11 = \case
+
+-- Non-exhaustive. (no info about a)
+f12 :: Foo3 a -> ()
+f12 = \case
+
+data instance DA () -- Empty data type
+
+-- Exhaustive.
+f13 :: Foo3 () -> ()
+f13 = \case
+
+-- ----------------
+data family DB a :: * -> *
+
+data instance DB Int a where
+  MkDB1 :: DB Int ()
+  MkDB2 :: DB Int Bool
+
+newtype Foo4 a b = Foo4 (DB a b)
+
+-- Non-exhaustive. Missing: Foo4 MkDB1
+f14 :: Foo4 Int () -> ()
+f14 = \case
+
+-- Exhaustive
+f15 :: Foo4 Int [a] -> ()
+f15 = \case
+
+-- Non-exhaustive. Missing: (_ :: Foo4 a b) (no information about a or b)
+f16 :: Foo4 a b -> ()
+f16 = \case
+
+data instance DB Char Bool -- Empty data type
+
+-- Exhaustive (empty data type)
+f17 :: Foo4 Char Bool -> ()
+f17 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
new file mode 100644
index 0000000000..a13e61aa67
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase008.stderr
@@ -0,0 +1,18 @@
+EmptyCase008.hs:15:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (Foo3 (MkDA1 _))
+            (Foo3 MkDA2)
+
+EmptyCase008.hs:19:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Foo3 a
+
+EmptyCase008.hs:38:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Foo4 MkDB1)
+
+EmptyCase008.hs:46:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Foo4 a b
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase009.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase009.hs
new file mode 100644
index 0000000000..f6741b88c8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase009.hs
@@ -0,0 +1,40 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, GADTs, EmptyCase, LambdaCase #-}
+
+-- Arrow Kind, Newtypes, GADTs, DataFamilies
+module EmptyCase009 where
+
+data family DB a :: * -> *
+
+data instance DB Int a where
+  MkDB1 :: DB Int ()
+  MkDB2 :: DB Int Bool
+
+data instance DB Char Bool -- Empty data type
+
+newtype Bar f = Bar (f Int)
+
+-- Non-exhaustive. Missing: (_ :: Bar f)
+f17 :: Bar f -> ()
+f17 x = case x of {}
+
+-- Exhaustive (Bar (DB Int) ~ DB Int Int, incompatible with both MkDB1 & MkDB2)
+f18 :: Bar (DB Int) -> ()
+f18 x = case x of {}
+
+data instance DB () a where
+  MkDB1_u :: DB () ()
+  MkDB2_u :: DB () Int
+
+-- Non-exhaustive. Missing: Bar MkDB2_u
+f19 :: Bar (DB ()) -> ()
+f19 = \case
+
+data GB :: * -> * where
+  MkGB1 :: Int -> GB ()
+  MkGB2 :: GB (a,a)
+  MkGB3 :: GB b
+
+-- Non-exhaustive. Missing: Bar MkGB3
+f20 :: Bar GB -> ()
+f20 = \case
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
new file mode 100644
index 0000000000..ab3fb0a45f
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase009.stderr
@@ -0,0 +1,11 @@
+EmptyCase009.hs:19:9: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Bar f
+
+EmptyCase009.hs:31:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Bar MkDB2_u)
+
+EmptyCase009.hs:40:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Bar MkGB3)
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase010.hs b/testsuite/tests/pmcheck/should_compile/EmptyCase010.hs
new file mode 100644
index 0000000000..48b1a247b8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase010.hs
@@ -0,0 +1,71 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds
+           , EmptyCase, LambdaCase #-}
+
+-- Newtypes, PolyKinds, DataKinds, GADTs, DataFamilies
+module EmptyCase010 where
+
+newtype Baz (f :: k -> *) (a :: k) = Baz (f a)
+
+data T = T1 | T2 T | T3 T T | T4 () -- only promoted
+
+data GC :: T -> * where
+  MkGC1 :: GC 'T1
+  MkGC2 :: T -> GC (T4 '())
+
+-- Exhaustive: GC ('T2 'T1) is not strictly inhabited
+f21 :: Baz GC ('T2 'T1) -> ()
+f21 = \case
+
+-- Non-exhaustive. Missing: Baz MkGC1, Baz (MkGC2 _)
+f22 :: Baz GC a -> ()
+f22 = \case
+
+-- Non-exhaustive. Missing: Baz MkGC1
+f23 :: Baz GC 'T1 -> ()
+f23 = \case
+
+data GD :: (* -> *) -> * where
+  MkGD1 :: GD Maybe
+  MkGD2 :: GD []
+  MkGD3 :: GD f
+
+-- Non-exhaustive. Missing: Baz MkGD1, Baz MkGD3
+f24 :: Baz GD Maybe -> ()
+f24 = \case
+
+-- Non-exhaustive. Missing: Baz MkGD3
+f25 :: Baz GD (Either Int) -> ()
+f25 x = case x of {}
+
+-- Non-exhaustive. Missing: Baz MkGD1, Baz MkGD2, Baz MkGD3
+f26 :: Baz GD f -> ()
+f26 = \case
+
+data family DC a :: * -> *
+
+data instance DC () Int -- Empty type
+
+-- Exhaustive
+f27 :: Baz (DC ()) Int -> ()
+f27 = \case
+
+-- Non-exhaustive. Missing: _ :: Baz (DC ()) a (a is unknown)
+f28 :: Baz (DC ()) a -> ()
+f28 = \case
+
+data instance DC Bool a where
+  MkDC1 :: DC Bool Int
+  MkDC2 :: DC Bool [a]
+
+-- Exhaustive. (DC Bool Char) is not strictly inhabited
+f29 :: Baz (DC Bool) Char -> ()
+f29 = \case
+
+-- Non-exhaustive. Missing: Baz MkDC2
+f30 :: Baz (DC Bool) [Int] -> ()
+f30 = \case
+
+-- Non-exhaustive. Missing: Baz f a (a and f unknown (and the kind too))
+f31 :: Baz f a -> ()
+f31 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr b/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
new file mode 100644
index 0000000000..d4ccce34bb
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/EmptyCase010.stderr
@@ -0,0 +1,41 @@
+EmptyCase010.hs:22:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (Baz MkGC1)
+            (Baz (MkGC2 _))
+
+EmptyCase010.hs:26:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Baz MkGC1)
+
+EmptyCase010.hs:35:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (Baz MkGD1)
+            (Baz MkGD3)
+
+EmptyCase010.hs:39:9: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Baz MkGD3)
+
+EmptyCase010.hs:43:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            (Baz MkGD1)
+            (Baz MkGD2)
+            (Baz MkGD3)
+
+EmptyCase010.hs:55:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Baz (DC ()) a
+
+EmptyCase010.hs:67:7: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: (Baz MkDC2)
+
+EmptyCase010.hs:71:9: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative: Patterns not matched: _ :: Baz f a
diff --git a/testsuite/tests/pmcheck/should_compile/T10746.hs b/testsuite/tests/pmcheck/should_compile/T10746.hs
new file mode 100644
index 0000000000..8b06abcde8
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T10746.hs
@@ -0,0 +1,25 @@
+{-# OPTIONS_GHC -fwarn-incomplete-patterns  #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs, DataKinds #-}
+
+module Test where
+
+-- Non-exhaustive (missing True & False)
+test :: Bool -> Int
+test a = case a of
+
+data Void
+
+-- Exhaustive
+absurd :: Void -> a
+absurd a = case a of {}
+
+data Nat = Zero | Succ Nat
+
+data Fin n where
+  FZ ::          Fin (Succ n)
+  FS :: Fin n -> Fin (Succ n)
+
+-- Exhaustive
+f :: Fin Zero -> a
+f x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/T10746.stderr b/testsuite/tests/pmcheck/should_compile/T10746.stderr
new file mode 100644
index 0000000000..9c0a196a08
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T10746.stderr
@@ -0,0 +1,6 @@
+T10746.hs:9:10: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In a case alternative:
+        Patterns not matched:
+            False
+            True
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 3f4e0c8af8..f19e1deedf 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -59,3 +59,27 @@ test('pmc007', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11245', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+
+# EmptyCase
+test('T10746', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase001', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase002', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase003', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase004', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase005', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase006', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase007', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase008', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase009', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('EmptyCase010', [],  compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])