Commit d236d9d0 authored by Sebastian Graf's avatar Sebastian Graf Committed by Marge Bot
Browse files

Make `singleConstructor` cope with pattern synonyms

Previously, `singleConstructor` didn't handle singleton `COMPLETE` sets
of a single pattern synonym, resulting in incomplete pattern warnings
in #15753.

This is fixed by making `singleConstructor` (now named
`singleMatchConstructor`) query `allCompleteMatches`, necessarily making
it effectful. As a result, most of this patch is concerned with
threading the side-effect through to `singleMatchConstructor`.

Unfortunately, this is not enough to completely fix the original
reproduction from #15753 and #15884, which are related to function
applications in pattern guards being translated too conservatively.
parent 4dda2270
......@@ -4,9 +4,13 @@ Author: George Karachalias <george.karachalias@cs.kuleuven.be>
Pattern Matching Coverage Checking.
-}
{-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE MultiWayIf #-}
module Check (
-- Checking and printing
......@@ -55,7 +59,7 @@ import qualified GHC.LanguageExtensions as LangExt
import Data.List (find)
import Data.Maybe (catMaybes, isJust, fromMaybe)
import Control.Monad (forM, when, forM_, zipWithM)
import Control.Monad (forM, when, forM_, zipWithM, filterM)
import Coercion
import TcEvidence
import TcSimplify (tcNormalise)
......@@ -289,6 +293,14 @@ data PmResult =
, pmresultUncovered :: UncoveredCandidates
, pmresultInaccessible :: [Located [LPat GhcTc]] }
instance Outputable PmResult where
ppr pmr = hang (text "PmResult") 2 $ vcat
[ text "pmresultProvenance" <+> ppr (pmresultProvenance pmr)
, text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
, text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
, text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
]
-- | Either a list of patterns that are not covered, or their type, in case we
-- have no patterns at hand. Not having patterns at hand can arise when
-- handling EmptyCase expressions, in two cases:
......@@ -303,6 +315,10 @@ data PmResult =
data UncoveredCandidates = UncoveredPatterns Uncovered
| TypeOfUncovered Type
instance Outputable UncoveredCandidates where
ppr (UncoveredPatterns uc) = text "UnPat" <+> ppr uc
ppr (TypeOfUncovered ty) = text "UnTy" <+> ppr ty
-- | The empty pattern check result
emptyPmResult :: PmResult
emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
......@@ -987,7 +1003,7 @@ translatePat fam_insts pat = case pat of
| otherwise -> do
ps <- translatePat fam_insts p
(xp,xe) <- mkPmId2Forms ty
let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
g <- mkGuard ps (mkHsWrap wrapper (unLoc xe))
return [xp,g]
-- (n + k) ===> x (True <- x >= k) (n <- x-k)
......@@ -997,10 +1013,11 @@ translatePat fam_insts pat = case pat of
ViewPat arg_ty lexpr lpat -> do
ps <- translatePat fam_insts (unLoc lpat)
-- See Note [Guards and Approximation]
case all cantFailPattern ps of
res <- allM cantFailPattern ps
case res of
True -> do
(xp,xe) <- mkPmId2Forms arg_ty
let g = mkGuard ps (HsApp noExt lexpr xe)
g <- mkGuard ps (HsApp noExt lexpr xe)
return [xp,g]
False -> mkCanFailPmPat arg_ty
......@@ -1255,41 +1272,38 @@ translateMatch _ _ = panic "translateMatch"
translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
translateGuards fam_insts guards = do
all_guards <- concat <$> mapM (translateGuard fam_insts) guards
return (replace_unhandled all_guards)
-- It should have been (return all_guards) but it is too expressive.
let
shouldKeep :: Pattern -> DsM Bool
shouldKeep p
| PmVar {} <- p = pure True
| PmCon {} <- p = (&&)
<$> singleMatchConstructor (pm_con_con p) (pm_con_arg_tys p)
<*> allM shouldKeep (pm_con_args p)
shouldKeep (PmGrd pv e)
| isNotPmExprOther e = pure True -- expensive but we want it
| otherwise = allM shouldKeep pv
shouldKeep _other_pat = pure False -- let the rest..
all_handled <- allM shouldKeep all_guards
-- It should have been @pure all_guards@ but it is too expressive.
-- Since the term oracle does not handle all constraints we generate,
-- we (hackily) replace all constraints the oracle cannot handle with a
-- single one (we need to know if there is a possibility of falure).
-- single one (we need to know if there is a possibility of failure).
-- See Note [Guards and Approximation] for all guard-related approximations
-- we implement.
where
replace_unhandled :: PatVec -> PatVec
replace_unhandled gv
| any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
| otherwise = gv
any_unhandled :: PatVec -> Bool
any_unhandled gv = any (not . shouldKeep) gv
shouldKeep :: Pattern -> Bool
shouldKeep p
| PmVar {} <- p = True
| PmCon {} <- p = singleConstructor (pm_con_con p)
&& all shouldKeep (pm_con_args p)
shouldKeep (PmGrd pv e)
| all shouldKeep pv = True
| isNotPmExprOther e = True -- expensive but we want it
shouldKeep _other_pat = False -- let the rest..
if all_handled
then pure all_guards
else do
kept <- filterM shouldKeep all_guards
pure (fake_pat : kept)
-- | Check whether a pattern can fail to match
cantFailPattern :: Pattern -> Bool
cantFailPattern p
| PmVar {} <- p = True
| PmCon {} <- p = singleConstructor (pm_con_con p)
&& all cantFailPattern (pm_con_args p)
cantFailPattern (PmGrd pv _e)
= all cantFailPattern pv
cantFailPattern _ = False
cantFailPattern :: Pattern -> DsM Bool
cantFailPattern PmVar {} = pure True
cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps}
= (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps
cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
cantFailPattern _ = pure False
-- | Translate a guard statement to Pattern
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
......@@ -1312,7 +1326,8 @@ translateLet _binds = return []
translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
translateBind fam_insts (dL->L _ p) e = do
ps <- translatePat fam_insts p
return [mkGuard ps (unLoc e)]
g <- mkGuard ps (unLoc e)
return [g]
-- | Translate a boolean guard
translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
......@@ -1321,7 +1336,7 @@ translateBoolGuard e
-- The formal thing to do would be to generate (True <- True)
-- but it is trivial to solve so instead we give back an empty
-- PatVec for efficiency
| otherwise = return [mkGuard [truePattern] (unLoc e)]
| otherwise = (:[]) <$> mkGuard [truePattern] (unLoc e)
{- Note [Guards and Approximation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1658,13 +1673,14 @@ mkOneConFull x con = do
-- * More smart constructors and fresh variable generation
-- | Create a guard pattern
mkGuard :: PatVec -> HsExpr GhcTc -> Pattern
mkGuard pv e
| all cantFailPattern pv = PmGrd pv expr
| PmExprOther {} <- expr = fake_pat
| otherwise = PmGrd pv expr
where
expr = hsExprToPmExpr e
mkGuard :: PatVec -> HsExpr GhcTc -> DsM Pattern
mkGuard pv e = do
res <- allM cantFailPattern pv
let expr = hsExprToPmExpr e
tracePmD "mkGuard" (vcat [ppr pv, ppr e, ppr res, ppr expr])
if | res -> pure (PmGrd pv expr)
| PmExprOther {} <- expr -> pure fake_pat
| otherwise -> pure (PmGrd pv expr)
-- | Create a term equality of the form: `(False ~ (x ~ lit))`
mkNegEq :: Id -> PmLit -> ComplexEq
......@@ -1738,14 +1754,37 @@ coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
, pm_con_args = coercePatVec args }]
coercePmPat (PmGrd {}) = [] -- drop the guards
-- | Check whether a data constructor is the only way to construct
-- a data type.
singleConstructor :: ConLike -> Bool
singleConstructor (RealDataCon dc) =
case tyConDataCons (dataConTyCon dc) of
[_] -> True
_ -> False
singleConstructor _ = False
-- | Check whether a 'ConLike' has the /single match/ property, i.e. whether
-- it is the only possible match in the given context. See also
-- 'allCompleteMatches' and Note [Single match constructors].
singleMatchConstructor :: ConLike -> [Type] -> DsM Bool
singleMatchConstructor cl tys =
any (isSingleton . snd) <$> allCompleteMatches cl tys
{-
Note [Single match constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When translating pattern guards for consumption by the checker, we desugar
every pattern guard that might fail ('cantFailPattern') to 'fake_pat'
(True <- _). Which patterns can't fail? Exactly those that only match on
'singleMatchConstructor's.
Here are a few examples:
* @f a | (a, b) <- foo a = 42@: Product constructors are generally
single match. This extends to single constructors of GADTs like 'Refl'.
* If @f | Id <- id () = 42@, where @pattern Id = ()@ and 'Id' is part of a
singleton `COMPLETE` set, then 'Id' has the single match property.
In effect, we can just enumerate 'allCompleteMatches' and check if the conlike
occurs as a singleton set.
There's the chance that 'Id' is part of multiple `COMPLETE` sets. That's
irrelevant; If the user specified a singleton set, it is single-match.
Note that this doesn't really take into account incoming type constraints;
It might be obvious from type context that a particular GADT constructor has
the single-match property. We currently don't (can't) check this in the
translation step. See #15753 for why this yields surprising results.
-}
-- | For a given conlike, finds all the sets of patterns which could
-- be relevant to that conlike by consulting the result type.
......
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}
module Bug where
import Data.Type.Equality
data G a where
GInt :: G Int
GBool :: G Bool
ex1, ex2, ex3
:: a :~: Int
-> G a
-> ()
ex1 Refl g
| GInt <- id g
= ()
ex2 Refl g
| GInt <- g
= ()
ex3 Refl g
= case id g of
GInt -> ()
{-# LANGUAGE PatternSynonyms #-}
module Bug where
{-# COMPLETE Id #-}
pattern Id :: ()
pattern Id = ()
bug :: ()
bug | Id <- id () = ()
{-# LANGUAGE ViewPatterns #-}
module Bug where
f :: Maybe a -> Bool
f (id->Nothing) = False
f (id->(Just _)) = True
......@@ -68,6 +68,12 @@ test('T15584', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15713', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15753a', expect_broken(15753), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15753b', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T15884', expect_broken(15884), compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
test('T16289', normal, compile,
['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
......
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