From a7867c7949b9dad95216ad5f2946be2cafcb860c Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Wed, 18 Sep 2019 16:15:36 +0000 Subject: Get rid of PmFake The pattern match oracle can now cope with the abundance of information that ViewPatterns, NPlusKPats, overloaded lists, etc. provide. No need to have PmFake anymore! Also got rid of a spurious call to `allCompleteMatches`, which we used to call *for every constructor* match. Naturally this blows up quadratically for programs like `ManyAlternatives`. ------------------------- Metric Decrease: ManyAlternatives Metric Increase: T11822 ------------------------- --- compiler/deSugar/Check.hs | 277 ++++----------------- .../tests/pmcheck/should_compile/T11822.stderr | 2 +- 2 files changed, 49 insertions(+), 230 deletions(-) diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs index be2fb76bf0..dbb83ab0f5 100644 --- a/compiler/deSugar/Check.hs +++ b/compiler/deSugar/Check.hs @@ -33,7 +33,6 @@ import BasicTypes (Origin, isGenerated) import CoreSyn (CoreExpr, Expr(Var)) import CoreUtils (exprType) import FastString (unpackFS) -import Unify( tcMatchTy ) import DynFlags import GHC.Hs import TcHsSyn @@ -42,18 +41,15 @@ import ConLike import Name import FamInst import TysWiredIn -import TyCon import SrcLoc import Util import Outputable import DataCon -import PatSyn -import HscTypes (CompleteMatch(..)) import BasicTypes (Boxity(..)) import Var (EvVar) import Coercion import TcEvidence -import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr) +import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr, dsSyntaxExpr) import MatchLit (dsLit, dsOverLit) import IOEnv import DsMonad @@ -105,16 +101,12 @@ data PmPat where , pm_grd_expr :: CoreExpr } -> PmPat -- (PmGrd pat expr) matches expr against pat, binding the variables in pat - -- | A fake guard pattern (True <- _) used to represent cases we cannot handle. - PmFake :: PmPat - -- | Should not be user-facing. instance Outputable PmPat where ppr (PmCon alt _arg_tys _con_tvs con_args) = cparen (notNull con_args) (hsep [ppr alt, hsep (map ppr con_args)]) ppr (PmVar vid) = ppr vid ppr (PmGrd pv ge) = hsep (map ppr pv) <+> text "<-" <+> ppr ge - ppr PmFake = text "" -- data T a where -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p] @@ -435,12 +427,6 @@ truePattern :: PmPat truePattern = nullaryConPattern (RealDataCon trueDataCon) {-# INLINE truePattern #-} --- | Generate a `canFail` pattern vector of a specific type -mkCanFailPmPat :: Type -> DsM PatVec -mkCanFailPmPat ty = do - var <- mkPmVar ty - return [var, PmFake] - vanillaConPattern :: ConLike -> [Type] -> PatVec -> PmPat -- ADT constructor pattern => no existentials, no local constraints vanillaConPattern con arg_tys args = @@ -518,19 +504,20 @@ translatePat fam_insts pat = case pat of pure [xp,g] -- (n + k) ===> x (True <- x >= k) (n <- x-k) - NPlusKPat ty (dL->L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty + NPlusKPat pat_ty (dL->L _ n) k1 k2 ge minus -> do + (xp, xe) <- mkPmId2Forms pat_ty + let ke1 = HsOverLit noExtField (unLoc k1) + ke2 = HsOverLit noExtField k2 + g1 <- mkGuardSyntaxExpr [truePattern] ge [unLoc xe, ke1] + g2 <- mkGuardSyntaxExpr [PmVar n] minus [ke2] + return [xp, g1, g2] -- (fun -> pat) ===> x (pat <- fun x) ViewPat arg_ty lexpr lpat -> do ps <- translatePat fam_insts (unLoc lpat) - -- See Note [Guards and Approximation] - res <- allM cantFailPattern ps - case res of - True -> do - (xp,xe) <- mkPmId2Forms arg_ty - g <- mkGuard ps (HsApp noExtField lexpr xe) - return [xp, g] - False -> mkCanFailPmPat arg_ty + (xp,xe) <- mkPmId2Forms arg_ty + g <- mkGuard ps (HsApp noExtField lexpr xe) + return [xp, g] -- list ListPat (ListPatTc ty Nothing) ps -> do @@ -538,14 +525,20 @@ translatePat fam_insts pat = case pat of return (foldr (mkListPatVec ty) [nilPattern ty] pv) -- overloaded list - ListPat (ListPatTc _elem_ty (Just (pat_ty, _to_list))) lpats -> do + ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) lpats -> do dflags <- getDynFlags - if xopt LangExt.RebindableSyntax dflags - then mkCanFailPmPat pat_ty - else case splitListTyConApp_maybe pat_ty of - Just e_ty -> translatePat fam_insts - (ListPat (ListPatTc e_ty Nothing) lpats) - Nothing -> mkCanFailPmPat pat_ty + case splitListTyConApp_maybe pat_ty of + Just e_ty + | not (xopt LangExt.RebindableSyntax dflags) + -- Just translate it as a regular ListPat + -> translatePat fam_insts (ListPat (ListPatTc e_ty Nothing) lpats) + _ -> do + ps <- translatePatVec fam_insts (map unLoc lpats) + (xp, xe) <- mkPmId2Forms pat_ty + let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps + g <- mkGuardSyntaxExpr pats to_list [unLoc xe] + return [xp,g] + -- (a) In the presence of RebindableSyntax, we don't know anything about -- `toList`, we should treat `ListPat` as any other view pattern. -- @@ -568,16 +561,11 @@ translatePat fam_insts pat = case pat of , pat_arg_tys = arg_tys , pat_tvs = ex_tvs , pat_args = ps } -> do - let ty = conLikeResTy con arg_tys - groups <- allCompleteMatches ty - case groups of - [] -> mkCanFailPmPat ty - _ -> do - args <- translateConPatVec fam_insts arg_tys ex_tvs con ps - return [PmCon { pm_con_con = PmAltConLike con - , pm_con_arg_tys = arg_tys - , pm_con_tvs = ex_tvs - , pm_con_args = args }] + args <- translateConPatVec fam_insts arg_tys ex_tvs con ps + return [PmCon { pm_con_con = PmAltConLike con + , pm_con_arg_tys = arg_tys + , pm_con_tvs = ex_tvs + , pm_con_args = args }] NPat ty (dL->L _ olit) mb_neg _ -> do -- See Note [Literal short cut] in MatchLit.hs @@ -713,14 +701,6 @@ translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec translateGuards fam_insts guards = concat <$> mapM (translateGuard fam_insts) guards --- | Check whether a pattern can fail to match -cantFailPattern :: PmPat -> 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 translateGuard fam_insts guard = case guard of @@ -756,90 +736,19 @@ translateBoolGuard e {- Note [Guards and Approximation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Even if the algorithm is really expressive, the term oracle we use is not. -Hence, several features are not translated *properly* but we approximate. -The list includes: - -1. View Patterns ----------------- -A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term -oracle does not handle function applications so we know that the generated -constraints will not be handled at the end. Hence, we distinguish between two -cases: - a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right - thing*. - b) Pattern @p@ can fail. This means that when checking the guard, we will - generate several cases, with no useful information. E.g.: - - h (f -> [a,b]) = ... - h x ([a,b] <- f x) = ... - - uncovered set = { [x |> { False ~ (f x ~ []) }] - , [x |> { False ~ (f x ~ (t1:[])) }] - , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] } - - So we have two problems: - 1) Since we do not print the constraints in the general case (they may - be too many), the warning will look like this: - - Pattern match(es) are non-exhaustive - In an equation for `h': - Patterns not matched: - _ - _ - _ - Which is not short and not more useful than a single underscore. - 2) The size of the uncovered set increases a lot, without gaining more - expressivity in our warnings. - - Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy* - @PmFake@: @True <- _@. That is, we record that there is a possibility - of failure but we minimize it to a True/False. This generates a single - warning and much smaller uncovered sets. - -2. Overloaded Lists -------------------- -An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The -problem is exactly like above, as its solution. For future reference, the code -below is the *right thing to do*: - - ListPat (ListPatTc elem_ty (Just (pat_ty, _to_list))) lpats - otherwise -> do - (xp, xe) <- mkPmId2Forms pat_ty - ps <- translatePatVec (map unLoc lpats) - let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps - g = mkGuard pats (HsApp (noLoc to_list) xe) - return [xp,g] - -3. Overloaded Literals ----------------------- -The case with literals is a bit different. a literal @l@ should be translated -to @x (True <- x == from l)@. Since we want to have better warnings for -overloaded literals as it is a very common feature, we treat them differently. -They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmTypes. - -4. N+K Patterns & Pattern Synonyms ----------------------------------- -An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@. -Since the only pattern of the three that causes failure is guard @(n <- x-k)@, -and has two possible outcomes. Hence, there is no benefit in using a dummy and -we implement the proper thing. Pattern synonyms are simply not implemented yet. -Hence, to be conservative, we generate a dummy pattern, assuming that the -pattern can fail. - -5. Actual Guards ----------------- -During translation, boolean guards and pattern guards are translated properly. -Let bindings though are omitted by function @translateLet@. Since they are lazy -bindings, we do not actually want to generate a (strict) equality (like we do -in the pattern bind case). Hence, we safely drop them. - -Additionally, top-level guard translation (performed by @translateGuards@) -replaces guards that cannot be reasoned about (like the ones we described in -1-4) with a single @PmFake@ to record the possibility of failure to match. - -6. Combinatorial explosion --------------------------- +Precise pattern match exchaustiveness checking is necessarily exponential in +the size of some input programs. We implement a couple approximation and safe +guards to prevent exponential blow-up: + + * Guards usually provide little information gain while quickly leading to + exponential blow-up. See Note [Combinatorial explosion in guards]. + * Similar to the situation with guards, refining a variable to a pattern + synonym application provides little value while easily leading to + exponential blow-up due to lack of generativity compared to DataCons. + See Note [Limit the number of refinements]. + +Note [Combinatorial explosion in guards] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Function with many clauses and deeply nested guards like in #11195 tend to overwhelm the checker because they lead to exponential splitting behavior. See the comments on #11195 on refinement trees. Every guard refines the @@ -937,7 +846,6 @@ pmPatType (PmVar { pm_var_id = x }) = idType x pmPatType (PmGrd { pm_grd_pv = pv }) = ASSERT(patVecArity pv == 1) (pmPatType p) where Just p = find ((==1) . patternArity) pv -pmPatType PmFake = pmPatType truePattern {- Note [Extensions to GADTs Meet Their Match] @@ -963,6 +871,11 @@ the paper. This Note serves as a reference for these new features. mkGuard :: PatVec -> HsExpr GhcTc -> DsM PmPat mkGuard pv e = PmGrd pv <$> dsExpr e +mkGuardSyntaxExpr :: PatVec -> SyntaxExpr GhcTc -> [HsExpr GhcTc] -> DsM PmPat +mkGuardSyntaxExpr pv f args = do + core_args <- traverse dsExpr args + PmGrd pv <$> dsSyntaxExpr f core_args + -- | Generate a variable pattern of a given type mkPmVar :: Type -> DsM PmPat mkPmVar ty = PmVar <$> mkPmId ty @@ -979,80 +892,6 @@ mkPmId2Forms ty = do x <- mkPmId ty return (PmVar x, noLoc (HsVar noExtField (noLoc x))) --- | Check whether a 'PmAltCon' 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 :: PmAltCon -> [Type] -> DsM Bool -singleMatchConstructor PmAltLit{} _ = pure False -singleMatchConstructor (PmAltConLike cl) tys = - any isSingleton <$> allCompleteMatches (conLikeResTy 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 'PmFake' -(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 type, finds all the COMPLETE sets of conlikes that inhabit it. --- --- Note that for a data family instance, this must be the *representation* type. --- e.g. data instance T (a,b) = T1 a b --- leads to --- data TPair a b = T1 a b -- The "representation" type --- It is TPair a b, not T (a, b), that is given to allCompleteMatches --- --- 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. Note that we only use `COMPLETE` pragmas --- *all* of whose pattern types match. See #14135 -allCompleteMatches :: Type -> DsM [[ConLike]] -allCompleteMatches ty = case splitTyConApp_maybe ty of - Nothing -> pure [] -- NB: We don't know any COMPLETE set, as opposed to [[]] - Just (tc, tc_args) -> do - -- Look into the representation type of a data family instance, too. - env <- dsGetFamInstEnvs - let (tc', _tc_args', _co) = tcLookupDataFamInst env tc tc_args - let mb_rdcs = map RealDataCon <$> tyConDataCons_maybe tc' - let maybe_to_list = maybe [] (:[]) - let rdcs = maybe_to_list mb_rdcs - -- NB: tc, because COMPLETE sets are associated with the parent data family - -- TyCon - pragmas <- dsGetCompleteMatches tc - let fams = mapM dsLookupConLike . completeMatchConLikes - pscs <- mapM fams pragmas - let candidates = rdcs ++ pscs - -- Check that all the pattern synonym return types in a `COMPLETE` - -- pragma subsume the type we're matching. - -- See Note [Filtering out non-matching COMPLETE sets] - pure (filter (isValidCompleteMatch ty) candidates) - where - isValidCompleteMatch :: Type -> [ConLike] -> Bool - isValidCompleteMatch ty = all p - where - p (RealDataCon _) = True - p (PatSynCon ps) = isJust (tcMatchTy (projResTy (patSynSig ps)) ty) - projResTy (_, _, _, _, _, res_ty) = res_ty - {- Note [Filtering out non-matching COMPLETE sets] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1141,7 +980,6 @@ patVecArity = sum . map patternArity -- | Compute the arity of a pattern patternArity :: PmPat -> PmArity patternArity (PmGrd {}) = 0 -patternArity PmFake = 0 patternArity _other_pat = 1 {- @@ -1204,7 +1042,7 @@ pmcheckGuards [] _ delta = return (usimple delta) pmcheckGuards (gv:gvs) n delta = do (PartialResult cs unc ds) <- pmcheckI gv [] [] n delta let (n', unc') - -- See 6. in Note [Guards and Approximation] + -- See Note [Combinatorial explosion in guards] | Just n' <- tryMultiplyDeltas (length unc) n = (n', unc) | otherwise = (n, [delta]) (PartialResult css uncs dss) <- runMany (pmcheckGuardsI gvs n') unc' @@ -1228,16 +1066,6 @@ pmcheck [] guards [] n delta | otherwise = pmcheckGuardsI guards n delta -- Guard -pmcheck (PmFake : ps) guards vva n delta = - -- short-circuit if the guard pattern is useless. - -- we just have two possible outcomes: fail here or match and recurse - -- none of the two contains any useful information about the failure - -- though. So just have these two cases but do not do all the boilerplate - -- TODO: I don't think this should mkCons delta, rather than just replace the - -- presultUncovered by [delta] completely. Note that the uncovered set - -- returned from the recursive call can only be a refinement of the - -- original delta. - forces . mkCons delta <$> pmcheckI ps guards vva n delta pmcheck (p@PmGrd { pm_grd_pv = pv, pm_grd_expr = e } : ps) guards vva n delta = do tracePm "PmGrd: pmPatType" (vcat [ppr p, ppr (pmPatType p)]) x <- mkPmId (exprType e) @@ -1290,11 +1118,6 @@ pmcheck (_:_) _ [] _ _ = panic "pmcheck: cons-nil" -- ---------------------------------------------------------------------------- -- * Utilities for main checking -updateUncovered :: (Uncovered -> Uncovered) -> (PartialResult -> PartialResult) -updateUncovered f p@(PartialResult { presultUncovered = old }) - = p { presultUncovered = f old } - - -- | Initialise with default values for covering and divergent information and -- a singleton uncovered set. usimple :: Delta -> PartialResult @@ -1308,10 +1131,6 @@ usimple delta = mempty { presultUncovered = [delta] } mkUnion :: PartialResult -> PartialResult -> PartialResult mkUnion = mappend --- | Add a model to the uncovered set. -mkCons :: Delta -> PartialResult -> PartialResult -mkCons model = updateUncovered (model:) - -- | Set the divergent set to not empty forces :: PartialResult -> PartialResult forces pres = pres { presultDivergent = Diverged } diff --git a/testsuite/tests/pmcheck/should_compile/T11822.stderr b/testsuite/tests/pmcheck/should_compile/T11822.stderr index c9e87c5deb..4d60fc368c 100644 --- a/testsuite/tests/pmcheck/should_compile/T11822.stderr +++ b/testsuite/tests/pmcheck/should_compile/T11822.stderr @@ -3,7 +3,7 @@ T11822.hs:33:1: warning: [-Wincomplete-patterns (in -Wextra)] Pattern match(es) are non-exhaustive In an equation for ‘mkTreeNode’: Patterns not matched: - _ (Data.Sequence.Internal.Seq _) _ _ + _ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0} _ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0} _ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0} _ (Data.Sequence.Internal.Seq _) _ p where p is not one of {0} -- cgit v1.2.1