Commit 16c7d9dc authored by carlostome's avatar carlostome Committed by Ben Gamari

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
parent eeb36ebd
......@@ -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
......
{-# 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
T14135.hs:16:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘f’: Patterns not matched: (Foo2 _)
......@@ -99,3 +99,4 @@ test('T13215', normal, compile, [''])
test('T13290', normal, compile, [''])
test('T13257', normal, compile, [''])
test('T13870', normal, compile, [''])
test('T14135', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment