Treat type data declarations as empty when checking pattern-matching coverage

The data constructors for a `type data` declaration don't exist at the value
level, so we don't want GHC to warn users to match on them.

Fixes #22964.

2 files changed, 32 insertions, 5 deletions

diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index 30b55388dd..18b5b5c2d6 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -146,11 +146,16 @@ updRcm f (RCM vanilla pragmas)
 -- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
 vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
 vanillaCompleteMatchTC tc =
-  let -- TYPE acts like an empty data type on the term-level (#14086), but
-      -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
-      -- special case.
-      mb_dcs | tc == tYPETyCon = Just []
-             | otherwise       = tyConDataCons_maybe tc
+  let mb_dcs | -- TYPE acts like an empty data type on the term level (#14086),
+               -- but it is a PrimTyCon, so tyConDataCons_maybe returns Nothing.
+               -- Hence a special case.
+               tc == tYPETyCon    = Just []
+             | -- Similarly, treat `type data` declarations as empty data types on
+               -- the term level, as `type data` data constructors only exist at
+               -- the type level (#22964).
+               -- See Note [Type data declarations] in GHC.Rename.Module.
+               isTypeDataTyCon tc = Just []
+             | otherwise          = tyConDataCons_maybe tc
   in vanillaCompleteMatch . mkUniqDSet . map RealDataCon <$> mb_dcs
 
 -- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas)
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 8a0d6eb734..e9b8d40d83 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2147,6 +2147,28 @@ The main parts of the implementation are:
   If `T` were an ordinary `data` declaration, then `A` would have a wrapper
   to account for the GADT-like equality in its return type. Because `T` is
   declared as a `type data` declaration, however, the wrapper is omitted.
+
+* Although `type data` data constructors do not exist at the value level,
+  it is still possible to match on a value whose type is headed by a `type data`
+  type constructor, such as this example from #22964:
+
+    type data T a where
+      A :: T Int
+      B :: T a
+
+    f :: T a -> ()
+    f x = case x of {}
+
+  This has two consequences:
+
+  * During checking the coverage of `f`'s pattern matches, we treat `T` as if it
+    were an empty data type so that GHC does not warn the user to match against
+    `A` or `B`. (Otherwise, you end up with the bug reported in #22964.)
+    See GHC.HsToCore.Pmc.Solver.vanillaCompleteMatchTC.
+
+  * In `GHC.Core.Utils.refineDataAlt`, do /not/ fill in the DEFAULT case with
+    the data constructor. See
+    Note [Refine DEFAULT case alternatives] Exception 2, in GHC.Core.Utils.
 -}
 
 warnNoDerivStrat :: Maybe (LDerivStrategy GhcRn)