From d81d0a0e8ed6cf35b9772404ce9d7f109481bcd6 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Sat, 11 Feb 2023 18:31:07 -0500
Subject: 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.

(cherry picked from commit 96dc58b9225d91a7912957c6be5d9c7a95e51718)
---
 compiler/GHC/HsToCore/Pmc/Solver.hs                | 15 ++++++++++-----
 compiler/GHC/Rename/Module.hs                      | 22 ++++++++++++++++++++++
 testsuite/tests/pmcheck/should_compile/T22964.hs   | 15 +++++++++++++++
 testsuite/tests/pmcheck/should_compile/all.T       |  1 +
 .../tests/type-data/should_compile/T22948b.stderr  |  4 ++++
 5 files changed, 52 insertions(+), 5 deletions(-)
 create mode 100644 testsuite/tests/pmcheck/should_compile/T22964.hs
 create mode 100644 testsuite/tests/type-data/should_compile/T22948b.stderr

diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index 07176b87cc..e8ea1fef1b 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -147,11 +147,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 ff4f3cce8e..bc14c1b189 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2154,6 +2154,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)
diff --git a/testsuite/tests/pmcheck/should_compile/T22964.hs b/testsuite/tests/pmcheck/should_compile/T22964.hs
new file mode 100644
index 0000000000..76e2072d4a
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T22964.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeData #-}
+module X where
+
+type data T1 a where
+  A1 :: T1 Int
+  B1 :: T1 a
+
+f1 :: T1 a -> ()
+f1 x = case x of {}
+
+type data T2 a where
+  A2 :: T2 Int
+
+f2 :: T2 a -> ()
+f2 x = case x of {}
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 0980dbb157..94c044b3d8 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -158,3 +158,4 @@ test('EmptyCase009', [],  compile, [overlapping_incomplete])
 test('EmptyCase010', [],  compile, [overlapping_incomplete])
 test('T19271', [],  compile, [overlapping_incomplete])
 test('T21761', [],  compile, [overlapping_incomplete])
+test('T22964', [], compile, [overlapping_incomplete])
diff --git a/testsuite/tests/type-data/should_compile/T22948b.stderr b/testsuite/tests/type-data/should_compile/T22948b.stderr
new file mode 100644
index 0000000000..96fbac8cbd
--- /dev/null
+++ b/testsuite/tests/type-data/should_compile/T22948b.stderr
@@ -0,0 +1,4 @@
+
+T22948b.hs:8:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f !x = ...
-- 
cgit v1.2.1