Normalise EmptyCase types using the constraint solver

Summary:
Certain `EmptyCase` expressions were mistakently producing
warnings since their types did not have as many type families reduced
as they could have. The most direct way to fix this is to normalise
these types initially using the constraint solver to solve for any
local equalities that may be in scope.

Test Plan: make test TEST=T14813

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #14813

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

4 files changed, 31 insertions, 6 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T14813.hs b/testsuite/tests/pmcheck/should_compile/T14813.hs
new file mode 100644
index 0000000000..1dcfe756f9
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14813.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# OPTIONS_GHC -Wall #-}
+module T14813 where
+
+import Data.Kind
+import Data.Void
+
+data SBool (z :: Bool) where
+  SFalse :: SBool 'False
+  STrue  :: SBool 'True
+
+type family F (b :: Bool) (a :: Type) :: Type where
+  F 'True  a = a
+  F 'False _ = Void
+
+dispatch :: forall (b :: Bool) (a :: Type). SBool b -> F b a -> a
+dispatch STrue  x = x
+dispatch SFalse x = case x of {}
+
+type family G a
+type instance G Int = Void
+
+fun :: i ~ Int => G i -> a
+fun x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/T15305.hs b/testsuite/tests/pmcheck/should_compile/T15305.hs
index 82214b7e19..8ee1a18385 100644
--- a/testsuite/tests/pmcheck/should_compile/T15305.hs
+++ b/testsuite/tests/pmcheck/should_compile/T15305.hs
@@ -36,15 +36,10 @@ data HsImplicitBndrs pass
 
 fun2 :: HsImplicitBndrs (GhcPass pass) -> ()
 fun2 UsefulConstructor = ()
-{-
-NB: the seemingly equivalent function
 
 fun2' :: (p ~ GhcPass pass) => HsImplicitBndrs p -> ()
 fun2' UsefulConstructor = ()
 
-Is mistakenly deemed non-exhaustive at the moment due to #14813.
--}
-
 -- Example 3
 
 data Abyss = MkAbyss !Abyss
diff --git a/testsuite/tests/pmcheck/should_compile/T15305.stderr b/testsuite/tests/pmcheck/should_compile/T15305.stderr
index bb88a9be5b..54cb90af5e 100644
--- a/testsuite/tests/pmcheck/should_compile/T15305.stderr
+++ b/testsuite/tests/pmcheck/should_compile/T15305.stderr
@@ -1,4 +1,4 @@
 
-T15305.hs:53:23: warning: [-Wincomplete-patterns (in -Wextra)]
+T15305.hs:48:23: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
     In a case alternative: Patterns not matched: (MkAbyss _)
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 20eef3ff95..079978b5f5 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -63,6 +63,8 @@ test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14098', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T14813', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15305', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T15385', normal, compile,