Fix #14135 by validity checking matches

We filter the complete patterns given in a COMPLETE set to only those that
subsume the type we are matching. Otherwise we end up introducing an ill-typed
equation into the overlap checking, provoking a crash. This was the cause of
Trac #14135.

Reviewers: austin, bgamari, mpickering, gkaracha, simonpj, RyanGlScott,
carlostome

Reviewed By: bgamari

Subscribers: carter, dfeuer, RyanGlScott, goldfire, rwbarton, thomie

GHC Trac Issues: #14135

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

4 files changed, 38 insertions, 9 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index d49a5c3ab8..d35615ca86 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -1263,24 +1263,32 @@ singleConstructor _ = False
 -- These come from two places.
 --  1. From data constructors defined with the result type constructor.
 --  2. From `COMPLETE` pragmas which have the same type as the result
---     type constructor.
+--     type constructor. Note that we only use `COMPLETE` pragmas
+--     *all* of whose pattern types match. See #14135
 allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
 allCompleteMatches cl tys = do
   let fam = case cl of
            RealDataCon dc ->
             [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
            PatSynCon _    -> []
-
-  pragmas <- case splitTyConApp_maybe (conLikeResTy cl tys) of
-              Just (tc, _) -> dsGetCompleteMatches tc
-              Nothing -> return []
-  let fams cm = fmap (FromComplete,) $
+      ty  = conLikeResTy cl tys
+  pragmas <- case splitTyConApp_maybe ty of
+               Just (tc, _) -> dsGetCompleteMatches tc
+               Nothing      -> return []
+  let fams cm = (FromComplete,) <$>
                 mapM dsLookupConLike (completeMatchConLikes cm)
-  from_pragma <- mapM fams pragmas
-
+  from_pragma <- filter (\(_,m) -> isValidCompleteMatch ty m) <$>
+                mapM fams pragmas
   let final_groups = fam ++ from_pragma
-  tracePmD "allCompleteMatches" (ppr final_groups)
   return final_groups
+    where
+      -- Check that all the pattern types in a `COMPLETE`
+      -- pragma subsume the type we're matching. See #14135.
+      isValidCompleteMatch :: Type -> [ConLike] -> Bool
+      isValidCompleteMatch ty =
+        isJust . mapM (flip tcMatchTy ty . resTy . conLikeFullSig)
+        where
+          resTy (_, _, _, _, _, _, res_ty) = res_ty
 
 -- -----------------------------------------------------------------------
 -- * Types and constraints
diff --git a/testsuite/tests/deSugar/should_compile/T14135.hs b/testsuite/tests/deSugar/should_compile/T14135.hs
new file mode 100644
index 0000000000..fbdd5bd4c6
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/T14135.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -Wincomplete-patterns #-}
+{-# LANGUAGE GADTs #-}
+module T14135 where
+
+data Foo a where
+  Foo1 :: a -> Foo a
+  Foo2 :: Int -> Foo Int
+
+pattern MyFoo2 :: (a ~ Int) => Int -> Foo a
+pattern MyFoo2 i = Foo2 i
+
+{-# COMPLETE Foo1, MyFoo2 #-}
+
+f :: Foo a -> a
+f (Foo1 x) = x
diff --git a/testsuite/tests/deSugar/should_compile/T14135.stderr b/testsuite/tests/deSugar/should_compile/T14135.stderr
new file mode 100644
index 0000000000..23a3e90aaf
--- /dev/null
+++ b/testsuite/tests/deSugar/should_compile/T14135.stderr
@@ -0,0 +1,4 @@
+
+T14135.hs:16:1: warning: [-Wincomplete-patterns (in -Wextra)]
+    Pattern match(es) are non-exhaustive
+    In an equation for ‘f’: Patterns not matched: (Foo2 _)
diff --git a/testsuite/tests/deSugar/should_compile/all.T b/testsuite/tests/deSugar/should_compile/all.T
index 0a20fbb833..fe6535ea3f 100644
--- a/testsuite/tests/deSugar/should_compile/all.T
+++ b/testsuite/tests/deSugar/should_compile/all.T
@@ -99,3 +99,4 @@ test('T13215', normal, compile, [''])
 test('T13290', normal, compile, [''])
 test('T13257', normal, compile, [''])
 test('T13870', normal, compile, [''])
+test('T14135', normal, compile, [''])