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

1 files changed, 17 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