Fix a bad interaction between GADTs and COMPLETE sets

As observed in #14059 (starting at comment 5), the error
messages surrounding a program involving GADTs and a `COMPLETE` set
became worse between 8.2 and 8.4. The culprit was a new validity
check in 8.4 which filters out `COMPLETE` set candidates if a return
type of any conlike in the set doesn't match the type of the
scrutinee. However, this check was too conservative, since it removed
perfectly valid `COMPLETE` sets that contained GADT constructors,
which quite often have return types that don't match the type of a
scrutinee.

To fix this, I adopted the most straightforward possible solution of
only performing this validity check on //pattern synonym//
constructors, not //data// constructors.

Note that this does not fix #14059 entirely, but instead simply fixes
a particular buglet that was discovered in that ticket.

Test Plan: make test TEST=T14059

Reviewers: bgamari, mpickering

Reviewed By: mpickering

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14059

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

4 files changed, 94 insertions, 5 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index d5449f373a..a776abe076 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -40,6 +40,7 @@ import Util
 import Outputable
 import FastString
 import DataCon
+import PatSyn
 import HscTypes (CompleteMatch(..))
 
 import DsMonad
@@ -1313,13 +1314,69 @@ allCompleteMatches cl tys = do
   let final_groups = fam ++ from_pragma
   return final_groups
     where
-      -- Check that all the pattern types in a `COMPLETE`
-      -- pragma subsume the type we're matching. See #14135.
+      -- Check that all the pattern synonym return types in a `COMPLETE`
+      -- pragma subsume the type we're matching.
+      -- See Note [Filtering out non-matching COMPLETE sets]
       isValidCompleteMatch :: Type -> [ConLike] -> Bool
-      isValidCompleteMatch ty =
-        isJust . mapM (flip tcMatchTy ty . resTy . conLikeFullSig)
+      isValidCompleteMatch ty = all go
         where
-          resTy (_, _, _, _, _, _, res_ty) = res_ty
+          go (RealDataCon {}) = True
+          go (PatSynCon psc)  = isJust $ flip tcMatchTy ty $ patSynResTy
+                                       $ patSynSig psc
+
+          patSynResTy (_, _, _, _, _, res_ty) = res_ty
+
+{-
+Note [Filtering out non-matching COMPLETE sets]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Currently, conlikes in a COMPLETE set are simply grouped by the
+type constructor heading the return type. This is nice and simple, but it does
+mean that there are scenarios when a COMPLETE set might be incompatible with
+the type of a scrutinee. For instance, consider (from #14135):
+
+  data Foo a = Foo1 a | Foo2 a
+
+  pattern MyFoo2 :: Int -> Foo Int
+  pattern MyFoo2 i = Foo2 i
+
+  {-# COMPLETE Foo1, MyFoo2 #-}
+
+  f :: Foo a -> a
+  f (Foo1 x) = x
+
+`f` has an incomplete pattern-match, so when choosing which constructors to
+report as unmatched in a warning, GHC must choose between the original set of
+data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe
+that GHC shouldn't even consider the COMPLETE set as a possibility: the return
+type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since
+there's no substitution `s` such that s(Foo Int) = Foo a.
+
+To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern
+synonym constructor's return type matches the type of the scrutinee, and if one
+doesn't, then we remove the whole COMPLETE set from consideration.
+
+One might wonder why GHC only checks /pattern synonym/ constructors, and not
+/data/ constructors as well. The reason is because that the type of a
+GADT constructor very well may not match the type of a scrutinee, and that's
+OK. Consider this example (from #14059):
+
+  data SBool (z :: Bool) where
+    SFalse :: SBool False
+    STrue  :: SBool True
+
+  pattern STooGoodToBeTrue :: forall (z :: Bool). ()
+                           => z ~ True
+                           => SBool z
+  pattern STooGoodToBeTrue = STrue
+  {-# COMPLETE SFalse, STooGoodToBeTrue #-}
+
+  wobble :: SBool z -> Bool
+  wobble STooGoodToBeTrue = True
+
+In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse
+should be matched against, even though its type, SBool False, does not match
+the scrutinee type, SBool z.
+-}
 
 -- -----------------------------------------------------------------------
 -- * Types and constraints
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14059a.hs b/testsuite/tests/pmcheck/complete_sigs/T14059a.hs
new file mode 100644
index 0000000000..6128a8beaa
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T14059a.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+module T14059a where
+
+data SBool (z :: Bool) where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+pattern STooGoodToBeTrue :: forall (z :: Bool). ()
+                         => z ~ True
+                         => SBool z
+pattern STooGoodToBeTrue = STrue
+{-# COMPLETE SFalse, STooGoodToBeTrue #-}
+
+wibble :: SBool z -> Bool
+wibble STrue = True
+
+wobble :: SBool z -> Bool
+wobble STooGoodToBeTrue = True
diff --git a/testsuite/tests/pmcheck/complete_sigs/T14059a.stderr b/testsuite/tests/pmcheck/complete_sigs/T14059a.stderr
new file mode 100644
index 0000000000..4a52c97dfe
--- /dev/null
+++ b/testsuite/tests/pmcheck/complete_sigs/T14059a.stderr
@@ -0,0 +1,8 @@
+
+T14059a.hs:20:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘wibble’: Patterns not matched: SFalse
+
+T14059a.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘wobble’: Patterns not matched: SFalse
diff --git a/testsuite/tests/pmcheck/complete_sigs/all.T b/testsuite/tests/pmcheck/complete_sigs/all.T
index 7e47877c1b..d58c182f8e 100644
--- a/testsuite/tests/pmcheck/complete_sigs/all.T
+++ b/testsuite/tests/pmcheck/complete_sigs/all.T
@@ -13,4 +13,5 @@ test('completesig12', normal, compile, [''])
 test('completesig13', normal, compile, [''])
 test('completesig14', normal, compile, [''])
 test('completesig15', normal, compile_fail, [''])
+test('T14059a', normal, compile, [''])
 test('T14253', expect_broken(14253), compile, [''])