Don't warn when empty casing on Type

Summary:
`Type` (a.k.a. `TYPE LiftedRep`) can be used at the type level thanks
to `TypeInType`. However, expressions like

```lang=haskell
f :: Type -> Int
f x = case x of {}
```

were falsely claiming that the empty case on the value of type `Type` was
non-exhaustive. The reason is a bit silly: `TYPE` is technically not an empty
datatype in GHC's eyes, since it's a builtin, primitive type. To convince the
pattern coverage checker otherwise, this adds a special case for `TYPE`.

Test Plan: make test TEST=T14086

Reviewers: gkaracha, austin, bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, thomie

GHC Trac Issues: #14086

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

3 files changed, 22 insertions, 0 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 2b1995cdd5..b0155d3e2f 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -27,6 +27,7 @@ import Id
 import ConLike
 import Name
 import FamInstEnv
+import TysPrim (tYPETyCon)
 import TysWiredIn
 import TyCon
 import SrcLoc
@@ -440,6 +441,19 @@ inhabitationCandidates fam_insts ty
             (_:_) -> do var <- liftD $ mkPmId (toTcType core_ty)
                         let va = build_tm (PmVar var) dcs
                         return $ Right [(va, mkIdEq var, emptyBag)]
+
+          -- TYPE (which is the underlying kind behind Type, among others)
+          -- is conceptually an empty datatype, so one would expect this code
+          -- (from #14086) to compile without warnings:
+          --
+          --   f :: Type -> Int
+          --   f x = case x of {}
+          --
+          -- However, since TYPE is a primitive builtin type, not an actual
+          -- datatype, we must convince the coverage checker of this fact by
+          -- adding a special case here.
+        | tc == tYPETyCon -> pure (Right [])
+
         | isClosedAlgType core_ty -> liftD $ do
             var  <- mkPmId (toTcType core_ty) -- it would be wrong to unify x
             alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
diff --git a/testsuite/tests/pmcheck/should_compile/T14086.hs b/testsuite/tests/pmcheck/should_compile/T14086.hs
new file mode 100644
index 0000000000..de91229c24
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14086.hs
@@ -0,0 +1,6 @@
+{-# language TypeInType, EmptyCase #-}
+module T14086 where
+import Data.Kind
+
+f :: Type -> Int
+f x = case x of
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index f44034b0d2..cabe23950b 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -41,6 +41,8 @@ test('T11276', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-pa
 test('T11303b', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 test('T11374', compile_timeout_multiplier(0.01), compile, ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M1G -RTS'])
 test('T11195', compile_timeout_multiplier(0.60), compile, ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
+test('T14086', normal, compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
 # Other tests
 test('pmc001', [], compile,