[commit: ghc] ghc-8.4: Fix #14135 by validity checking matches (cc034b3)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-8.4
Link       : http://ghc.haskell.org/trac/ghc/changeset/cc034b35a6890bd67739e59319f50dc020f04da7/ghc

>---------------------------------------------------------------

commit cc034b35a6890bd67739e59319f50dc020f04da7
Author: Carlos Tomé <carlostome1990 at gmail.com>
Date:   Mon Dec 11 15:38:03 2017 -0500

    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
    
    (cherry picked from commit 16c7d9dc9ea7505256e0792c958cab8ae7c8a5c4)


>---------------------------------------------------------------

cc034b35a6890bd67739e59319f50dc020f04da7
 compiler/deSugar/Check.hs                          | 26 ++++++++++++++--------
 testsuite/tests/deSugar/should_compile/T14135.hs   | 16 +++++++++++++
 .../tests/deSugar/should_compile/T14135.stderr     |  4 ++++
 testsuite/tests/deSugar/should_compile/all.T       |  1 +
 4 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index d49a5c3..d35615c 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 0000000..fbdd5bd
--- /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 0000000..23a3e90
--- /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 0a20fbb..fe6535e 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, [''])