Overhaul the Overhauled Pattern Match Checker
[ghc.git] / compiler / deSugar / Check.hs
1 {-
2 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
3
4 Pattern Matching Coverage Checking.
5 -}
6
7 {-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
8
9 module Check (
10 -- Checking and printing
11 checkSingle, checkMatches, isAnyPmCheckEnabled,
12
13 -- See Note [Type and Term Equality Propagation]
14 genCaseTmCs1, genCaseTmCs2
15 ) where
16
17 #include "HsVersions.h"
18
19 import TmOracle
20
21 import DynFlags
22 import HsSyn
23 import TcHsSyn
24 import Id
25 import ConLike
26 import DataCon
27 import Name
28 import FamInstEnv
29 import TysWiredIn
30 import TyCon
31 import SrcLoc
32 import Util
33 import Outputable
34 import FastString
35
36 import DsMonad -- DsM, initTcDsForSolver, getDictsDs
37 import TcSimplify -- tcCheckSatisfiability
38 import TcType -- toTcType, toTcTypeBag
39 import Bag
40 import ErrUtils
41 import MonadUtils -- MonadIO
42 import Var -- EvVar
43 import Type
44 import UniqSupply
45 import DsGRHSs -- isTrueLHsExpr
46
47 import Data.List -- find
48 import Data.Maybe -- isNothing, isJust, fromJust
49 import Control.Monad -- liftM3, forM
50 import Coercion
51 import TcEvidence
52 import IOEnv
53
54 {-
55 This module checks pattern matches for:
56 \begin{enumerate}
57 \item Equations that are redundant
58 \item Equations with inaccessible right-hand-side
59 \item Exhaustiveness
60 \end{enumerate}
61
62 The algorithm is based on the paper:
63
64 "GADTs Meet Their Match:
65 Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
66
67 http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf
68
69 %************************************************************************
70 %* *
71 Pattern Match Check Types
72 %* *
73 %************************************************************************
74 -}
75
76 type PmM a = DsM a
77
78 data PatTy = PAT | VA -- Used only as a kind, to index PmPat
79
80 -- The *arity* of a PatVec [p1,..,pn] is
81 -- the number of p1..pn that are not Guards
82
83 data PmPat :: PatTy -> * where
84 PmCon :: { pm_con_con :: DataCon
85 , pm_con_arg_tys :: [Type]
86 , pm_con_tvs :: [TyVar]
87 , pm_con_dicts :: [EvVar]
88 , pm_con_args :: [PmPat t] } -> PmPat t
89 -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
90 PmVar :: { pm_var_id :: Id } -> PmPat t
91 PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
92 PmNLit :: { pm_lit_id :: Id
93 , pm_lit_not :: [PmLit] } -> PmPat 'VA
94 PmGrd :: { pm_grd_pv :: PatVec
95 , pm_grd_expr :: PmExpr } -> PmPat 'PAT
96
97 -- data T a where
98 -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
99 -- or MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
100
101 type Pattern = PmPat 'PAT -- ^ Patterns
102 type ValAbs = PmPat 'VA -- ^ Value Abstractions
103
104 type PatVec = [Pattern] -- ^ Pattern Vectors
105 data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions
106
107 -- | Term and type constraints to accompany each value vector abstraction.
108 -- For efficiency, we store the term oracle state instead of the term
109 -- constraints. TODO: Do the same for the type constraints?
110 data Delta = MkDelta { delta_ty_cs :: Bag EvVar
111 , delta_tm_cs :: TmState }
112
113 type ValSetAbs = [ValVec] -- ^ Value Set Abstractions
114 type Uncovered = ValSetAbs
115
116 -- Instead of keeping the whole sets in memory, we keep a boolean for both the
117 -- covered and the divergent set (we store the uncovered set though, since we
118 -- want to print it). For both the covered and the divergent we have:
119 --
120 -- True <=> The set is non-empty
121 --
122 -- hence:
123 -- C = True ==> Useful clause (no warning)
124 -- C = False, D = True ==> Clause with inaccessible RHS
125 -- C = False, D = False ==> Redundant clause
126 type Triple = (Bool, Uncovered, Bool)
127
128 -- | Pattern check result
129 --
130 -- * Redundant clauses
131 -- * Not-covered clauses
132 -- * Clauses with inaccessible RHS
133 type PmResult = ([[LPat Id]], Uncovered, [[LPat Id]])
134
135 {-
136 %************************************************************************
137 %* *
138 Entry points to the checker: checkSingle and checkMatches
139 %* *
140 %************************************************************************
141 -}
142
143 -- | Check a single pattern binding (let)
144 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat Id -> DsM ()
145 checkSingle dflags ctxt var p = do
146 mb_pm_res <- tryM (checkSingle' var p)
147 case mb_pm_res of
148 Left _ -> warnPmIters dflags ctxt
149 Right res -> dsPmWarn dflags ctxt res
150
151 -- | Check a single pattern binding (let)
152 checkSingle' :: Id -> Pat Id -> DsM PmResult
153 checkSingle' var p = do
154 resetPmIterDs -- set the iter-no to zero
155 fam_insts <- dsGetFamInstEnvs
156 clause <- translatePat fam_insts p
157 missing <- mkInitialUncovered [var]
158 (cs,us,ds) <- runMany (pmcheckI clause []) missing -- no guards
159 return $ case (cs,ds) of
160 (True, _ ) -> ([], us, []) -- useful
161 (False, False) -> ( m, us, []) -- redundant
162 (False, True ) -> ([], us, m) -- inaccessible rhs
163 where m = [[noLoc p]]
164
165 -- | Check a matchgroup (case, functions, etc.)
166 checkMatches :: DynFlags -> DsMatchContext
167 -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM ()
168 checkMatches dflags ctxt vars matches = do
169 mb_pm_res <- tryM (checkMatches' vars matches)
170 case mb_pm_res of
171 Left _ -> warnPmIters dflags ctxt
172 Right res -> dsPmWarn dflags ctxt res
173
174 -- | Check a matchgroup (case, functions, etc.)
175 checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> DsM PmResult
176 checkMatches' vars matches
177 | null matches = return ([], [], [])
178 | otherwise = do
179 resetPmIterDs -- set the iter-no to zero
180 missing <- mkInitialUncovered vars
181 (rs,us,ds) <- go matches missing
182 return (map hsLMatchPats rs, us, map hsLMatchPats ds)
183 where
184 go [] missing = return ([], missing, [])
185 go (m:ms) missing = do
186 fam_insts <- dsGetFamInstEnvs
187 (clause, guards) <- translateMatch fam_insts m
188 (cs, missing', ds) <- runMany (pmcheckI clause guards) missing
189 (rs, final_u, is) <- go ms missing'
190 return $ case (cs, ds) of
191 (True, _ ) -> ( rs, final_u, is) -- useful
192 (False, False) -> (m:rs, final_u, is) -- redundant
193 (False, True ) -> ( rs, final_u, m:is) -- inaccessible
194
195 {-
196 %************************************************************************
197 %* *
198 Transform source syntax to *our* syntax
199 %* *
200 %************************************************************************
201 -}
202
203 -- -----------------------------------------------------------------------
204 -- * Utilities
205
206 nullaryConPattern :: DataCon -> Pattern
207 -- Nullary data constructor and nullary type constructor
208 nullaryConPattern con =
209 PmCon { pm_con_con = con, pm_con_arg_tys = []
210 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
211 {-# INLINE nullaryConPattern #-}
212
213 truePattern :: Pattern
214 truePattern = nullaryConPattern trueDataCon
215 {-# INLINE truePattern #-}
216
217 -- | A fake guard pattern (True <- _) used to represent cases we cannot handle
218 fake_pat :: Pattern
219 fake_pat = PmGrd { pm_grd_pv = [truePattern]
220 , pm_grd_expr = PmExprOther EWildPat }
221 {-# INLINE fake_pat #-}
222
223 -- | Check whether a guard pattern is generated by the checker (unhandled)
224 isFakeGuard :: [Pattern] -> PmExpr -> Bool
225 isFakeGuard [PmCon { pm_con_con = c }] (PmExprOther EWildPat)
226 | c == trueDataCon = True
227 | otherwise = False
228 isFakeGuard _pats _e = False
229
230 -- | Generate a `canFail` pattern vector of a specific type
231 mkCanFailPmPat :: Type -> PmM PatVec
232 mkCanFailPmPat ty = do
233 var <- mkPmVar ty
234 return [var, fake_pat]
235
236 vanillaConPattern :: DataCon -> [Type] -> PatVec -> Pattern
237 -- ADT constructor pattern => no existentials, no local constraints
238 vanillaConPattern con arg_tys args =
239 PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
240 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
241 {-# INLINE vanillaConPattern #-}
242
243 -- | Create an empty list pattern of a given type
244 nilPattern :: Type -> Pattern
245 nilPattern ty =
246 PmCon { pm_con_con = nilDataCon, pm_con_arg_tys = [ty]
247 , pm_con_tvs = [], pm_con_dicts = []
248 , pm_con_args = [] }
249 {-# INLINE nilPattern #-}
250
251 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
252 mkListPatVec ty xs ys = [PmCon { pm_con_con = consDataCon
253 , pm_con_arg_tys = [ty]
254 , pm_con_tvs = [], pm_con_dicts = []
255 , pm_con_args = xs++ys }]
256 {-# INLINE mkListPatVec #-}
257
258 -- | Create a (non-overloaded) literal pattern
259 mkLitPattern :: HsLit -> Pattern
260 mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
261 {-# INLINE mkLitPattern #-}
262
263 -- -----------------------------------------------------------------------
264 -- * Transform (Pat Id) into of (PmPat Id)
265
266 translatePat :: FamInstEnvs -> Pat Id -> PmM PatVec
267 translatePat fam_insts pat = case pat of
268 WildPat ty -> mkPmVars [ty]
269 VarPat id -> return [PmVar (unLoc id)]
270 ParPat p -> translatePat fam_insts (unLoc p)
271 LazyPat _ -> mkPmVars [hsPatType pat] -- like a variable
272
273 -- ignore strictness annotations for now
274 BangPat p -> translatePat fam_insts (unLoc p)
275
276 AsPat lid p -> do
277 -- Note [Translating As Patterns]
278 ps <- translatePat fam_insts (unLoc p)
279 let [e] = map vaToPmExpr (coercePatVec ps)
280 g = PmGrd [PmVar (unLoc lid)] e
281 return (ps ++ [g])
282
283 SigPatOut p _ty -> translatePat fam_insts (unLoc p)
284
285 -- See Note [Translate CoPats]
286 CoPat wrapper p ty
287 | isIdHsWrapper wrapper -> translatePat fam_insts p
288 | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p
289 | otherwise -> do
290 ps <- translatePat fam_insts p
291 (xp,xe) <- mkPmId2Forms ty
292 let g = mkGuard ps (HsWrap wrapper (unLoc xe))
293 return [xp,g]
294
295 -- (n + k) ===> x (True <- x >= k) (n <- x-k)
296 NPlusKPat (L _ _n) _k1 _k2 _ge _minus ty -> mkCanFailPmPat ty
297
298 -- (fun -> pat) ===> x (pat <- fun x)
299 ViewPat lexpr lpat arg_ty -> do
300 ps <- translatePat fam_insts (unLoc lpat)
301 -- See Note [Guards and Approximation]
302 case all cantFailPattern ps of
303 True -> do
304 (xp,xe) <- mkPmId2Forms arg_ty
305 let g = mkGuard ps (HsApp lexpr xe)
306 return [xp,g]
307 False -> mkCanFailPmPat arg_ty
308
309 -- list
310 ListPat ps ty Nothing -> do
311 foldr (mkListPatVec ty) [nilPattern ty]
312 <$> translatePatVec fam_insts (map unLoc ps)
313
314 -- overloaded list
315 ListPat lpats elem_ty (Just (pat_ty, _to_list))
316 | Just e_ty <- splitListTyConApp_maybe pat_ty
317 , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty
318 -- elem_ty is frequently something like
319 -- `Item [Int]`, but we prefer `Int`
320 , norm_elem_ty `eqType` e_ty ->
321 -- We have to ensure that the element types are exactly the same.
322 -- Otherwise, one may give an instance IsList [Int] (more specific than
323 -- the default IsList [a]) with a different implementation for `toList'
324 translatePat fam_insts (ListPat lpats e_ty Nothing)
325 -- See Note [Guards and Approximation]
326 | otherwise -> mkCanFailPmPat pat_ty
327
328 ConPatOut { pat_con = L _ (PatSynCon _) } ->
329 -- Pattern synonyms have a "matcher"
330 -- (see Note [Pattern synonym representation] in PatSyn.hs
331 -- We should be able to transform (P x y)
332 -- to v (Just (x, y) <- matchP v (\x y -> Just (x,y)) Nothing
333 -- That is, a combination of a variable pattern and a guard
334 -- But there are complications with GADTs etc, and this isn't done yet
335 mkCanFailPmPat (hsPatType pat)
336
337 ConPatOut { pat_con = L _ (RealDataCon con)
338 , pat_arg_tys = arg_tys
339 , pat_tvs = ex_tvs
340 , pat_dicts = dicts
341 , pat_args = ps } -> do
342 args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
343 return [PmCon { pm_con_con = con
344 , pm_con_arg_tys = arg_tys
345 , pm_con_tvs = ex_tvs
346 , pm_con_dicts = dicts
347 , pm_con_args = args }]
348
349 NPat (L _ ol) mb_neg _eq ty -> translateNPat fam_insts ol mb_neg ty
350
351 LitPat lit
352 -- If it is a string then convert it to a list of characters
353 | HsString src s <- lit ->
354 foldr (mkListPatVec charTy) [nilPattern charTy] <$>
355 translatePatVec fam_insts (map (LitPat . HsChar src) (unpackFS s))
356 | otherwise -> return [mkLitPattern lit]
357
358 PArrPat ps ty -> do
359 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
360 let fake_con = parrFakeCon (length ps)
361 return [vanillaConPattern fake_con [ty] (concat tidy_ps)]
362
363 TuplePat ps boxity tys -> do
364 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
365 let tuple_con = tupleDataCon boxity (length ps)
366 return [vanillaConPattern tuple_con tys (concat tidy_ps)]
367
368 -- --------------------------------------------------------------------------
369 -- Not supposed to happen
370 ConPatIn {} -> panic "Check.translatePat: ConPatIn"
371 SplicePat {} -> panic "Check.translatePat: SplicePat"
372 SigPatIn {} -> panic "Check.translatePat: SigPatIn"
373
374 -- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
375 translateNPat :: FamInstEnvs
376 -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> Type -> PmM PatVec
377 translateNPat fam_insts (OverLit val False _ ty) mb_neg outer_ty
378 | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
379 = translatePat fam_insts (LitPat (HsString src s))
380 | not type_change, isIntTy ty, HsIntegral src i <- val
381 = translatePat fam_insts (mk_num_lit HsInt src i)
382 | not type_change, isWordTy ty, HsIntegral src i <- val
383 = translatePat fam_insts (mk_num_lit HsWordPrim src i)
384 where
385 type_change = not (outer_ty `eqType` ty)
386 mk_num_lit c src i = LitPat $ case mb_neg of
387 Nothing -> c src i
388 Just _ -> c src (-i)
389 translateNPat _ ol mb_neg _
390 = return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) ol }]
391
392 -- | Translate a list of patterns (Note: each pattern is translated
393 -- to a pattern vector but we do not concatenate the results).
394 translatePatVec :: FamInstEnvs -> [Pat Id] -> PmM [PatVec]
395 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
396
397 -- | Translate a constructor pattern
398 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
399 -> DataCon -> HsConPatDetails Id -> PmM PatVec
400 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
401 = concat <$> translatePatVec fam_insts (map unLoc ps)
402 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
403 = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
404 translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
405 -- Nothing matched. Make up some fresh term variables
406 | null fs = mkPmVars arg_tys
407 -- The data constructor was not defined using record syntax. For the
408 -- pattern to be in record syntax it should be empty (e.g. Just {}).
409 -- So just like the previous case.
410 | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
411 -- Some of the fields appear, in the original order (there may be holes).
412 -- Generate a simple constructor pattern and make up fresh variables for
413 -- the rest of the fields
414 | matched_lbls `subsetOf` orig_lbls
415 = ASSERT(length orig_lbls == length arg_tys)
416 let translateOne (lbl, ty) = case lookup lbl matched_pats of
417 Just p -> translatePat fam_insts p
418 Nothing -> mkPmVars [ty]
419 in concatMapM translateOne (zip orig_lbls arg_tys)
420 -- The fields that appear are not in the correct order. Make up fresh
421 -- variables for all fields and add guards after matching, to force the
422 -- evaluation in the correct order.
423 | otherwise = do
424 arg_var_pats <- mkPmVars arg_tys
425 translated_pats <- forM matched_pats $ \(x,pat) -> do
426 pvec <- translatePat fam_insts pat
427 return (x, pvec)
428
429 let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
430 guards = map (\(name,pvec) -> case lookup name zipped of
431 Just x -> PmGrd pvec (PmExprVar (idName x))
432 Nothing -> panic "translateConPatVec: lookup")
433 translated_pats
434
435 return (arg_var_pats ++ guards)
436 where
437 -- The actual argument types (instantiated)
438 arg_tys = dataConInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
439
440 -- Some label information
441 orig_lbls = map flSelector $ dataConFieldLabels c
442 matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
443 | L _ x <- fs]
444 matched_lbls = [ name | (name, _pat) <- matched_pats ]
445
446 subsetOf :: Eq a => [a] -> [a] -> Bool
447 subsetOf [] _ = True
448 subsetOf (_:_) [] = False
449 subsetOf (x:xs) (y:ys)
450 | x == y = subsetOf xs ys
451 | otherwise = subsetOf (x:xs) ys
452
453 -- Translate a single match
454 translateMatch :: FamInstEnvs -> LMatch Id (LHsExpr Id) -> PmM (PatVec,[PatVec])
455 translateMatch fam_insts (L _ (Match _ lpats _ grhss)) = do
456 pats' <- concat <$> translatePatVec fam_insts pats
457 guards' <- mapM (translateGuards fam_insts) guards
458 return (pats', guards')
459 where
460 extractGuards :: LGRHS Id (LHsExpr Id) -> [GuardStmt Id]
461 extractGuards (L _ (GRHS gs _)) = map unLoc gs
462
463 pats = map unLoc lpats
464 guards = map extractGuards (grhssGRHSs grhss)
465
466 -- -----------------------------------------------------------------------
467 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
468
469 -- | Translate a list of guard statements to a pattern vector
470 translateGuards :: FamInstEnvs -> [GuardStmt Id] -> PmM PatVec
471 translateGuards fam_insts guards = do
472 all_guards <- concat <$> mapM (translateGuard fam_insts) guards
473 return (replace_unhandled all_guards)
474 -- It should have been (return all_guards) but it is too expressive.
475 -- Since the term oracle does not handle all constraints we generate,
476 -- we (hackily) replace all constraints the oracle cannot handle with a
477 -- single one (we need to know if there is a possibility of falure).
478 -- See Note [Guards and Approximation] for all guard-related approximations
479 -- we implement.
480 where
481 replace_unhandled :: PatVec -> PatVec
482 replace_unhandled gv
483 | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
484 | otherwise = gv
485
486 any_unhandled :: PatVec -> Bool
487 any_unhandled gv = any (not . shouldKeep) gv
488
489 shouldKeep :: Pattern -> Bool
490 shouldKeep p
491 | PmVar {} <- p = True
492 | PmCon {} <- p = length (allConstructors (pm_con_con p)) == 1
493 && all shouldKeep (pm_con_args p)
494 shouldKeep (PmGrd pv e)
495 | all shouldKeep pv = True
496 | isNotPmExprOther e = True -- expensive but we want it
497 shouldKeep _other_pat = False -- let the rest..
498
499 -- | Check whether a pattern can fail to match
500 cantFailPattern :: Pattern -> Bool
501 cantFailPattern p
502 | PmVar {} <- p = True
503 | PmCon {} <- p = length (allConstructors (pm_con_con p)) == 1
504 && all cantFailPattern (pm_con_args p)
505 cantFailPattern (PmGrd pv _e)
506 = all cantFailPattern pv
507 cantFailPattern _ = False
508
509 -- | Translate a guard statement to Pattern
510 translateGuard :: FamInstEnvs -> GuardStmt Id -> PmM PatVec
511 translateGuard fam_insts guard = case guard of
512 BodyStmt e _ _ _ -> translateBoolGuard e
513 LetStmt binds -> translateLet (unLoc binds)
514 BindStmt p e _ _ _ -> translateBind fam_insts p e
515 LastStmt {} -> panic "translateGuard LastStmt"
516 ParStmt {} -> panic "translateGuard ParStmt"
517 TransStmt {} -> panic "translateGuard TransStmt"
518 RecStmt {} -> panic "translateGuard RecStmt"
519 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
520
521 -- | Translate let-bindings
522 translateLet :: HsLocalBinds Id -> PmM PatVec
523 translateLet _binds = return []
524
525 -- | Translate a pattern guard
526 translateBind :: FamInstEnvs -> LPat Id -> LHsExpr Id -> PmM PatVec
527 translateBind fam_insts (L _ p) e = do
528 ps <- translatePat fam_insts p
529 return [mkGuard ps (unLoc e)]
530
531 -- | Translate a boolean guard
532 translateBoolGuard :: LHsExpr Id -> PmM PatVec
533 translateBoolGuard e
534 | isJust (isTrueLHsExpr e) = return []
535 -- The formal thing to do would be to generate (True <- True)
536 -- but it is trivial to solve so instead we give back an empty
537 -- PatVec for efficiency
538 | otherwise = return [mkGuard [truePattern] (unLoc e)]
539
540 {- Note [Guards and Approximation]
541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
542 Even if the algorithm is really expressive, the term oracle we use is not.
543 Hence, several features are not translated *properly* but we approximate.
544 The list includes:
545
546 1. View Patterns
547 ----------------
548 A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
549 oracle does not handle function applications so we know that the generated
550 constraints will not be handled at the end. Hence, we distinguish between two
551 cases:
552 a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
553 thing*.
554 b) Pattern @p@ can fail. This means that when checking the guard, we will
555 generate several cases, with no useful information. E.g.:
556
557 h (f -> [a,b]) = ...
558 h x ([a,b] <- f x) = ...
559
560 uncovered set = { [x |> { False ~ (f x ~ []) }]
561 , [x |> { False ~ (f x ~ (t1:[])) }]
562 , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
563
564 So we have two problems:
565 1) Since we do not print the constraints in the general case (they may
566 be too many), the warning will look like this:
567
568 Pattern match(es) are non-exhaustive
569 In an equation for `h':
570 Patterns not matched:
571 _
572 _
573 _
574 Which is not short and not more useful than a single underscore.
575 2) The size of the uncovered set increases a lot, without gaining more
576 expressivity in our warnings.
577
578 Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
579 @fake_pat@: @True <- _@. That is, we record that there is a possibility
580 of failure but we minimize it to a True/False. This generates a single
581 warning and much smaller uncovered sets.
582
583 2. Overloaded Lists
584 -------------------
585 An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
586 problem is exactly like above, as its solution. For future reference, the code
587 below is the *right thing to do*:
588
589 ListPat lpats elem_ty (Just (pat_ty, to_list))
590 otherwise -> do
591 (xp, xe) <- mkPmId2Forms pat_ty
592 ps <- translatePatVec (map unLoc lpats)
593 let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
594 g = mkGuard pats (HsApp (noLoc to_list) xe)
595 return [xp,g]
596
597 3. Overloaded Literals
598 ----------------------
599 The case with literals is a bit different. a literal @l@ should be translated
600 to @x (True <- x == from l)@. Since we want to have better warnings for
601 overloaded literals as it is a very common feature, we treat them differently.
602 They are mainly covered in Note [Undecidable Equality on Overloaded Literals]
603 in PmExpr.
604
605 4. N+K Patterns & Pattern Synonyms
606 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
607 An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
608 Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
609 and has two possible outcomes. Hence, there is no benefit in using a dummy and
610 we implement the proper thing. Pattern synonyms are simply not implemented yet.
611 Hence, to be conservative, we generate a dummy pattern, assuming that the
612 pattern can fail.
613
614 5. Actual Guards
615 ----------------
616 During translation, boolean guards and pattern guards are translated properly.
617 Let bindings though are omitted by function @translateLet@. Since they are lazy
618 bindings, we do not actually want to generate a (strict) equality (like we do
619 in the pattern bind case). Hence, we safely drop them.
620
621 Additionally, top-level guard translation (performed by @translateGuards@)
622 replaces guards that cannot be reasoned about (like the ones we described in
623 1-4) with a single @fake_pat@ to record the possibility of failure to match.
624
625 Note [Translate CoPats]
626 ~~~~~~~~~~~~~~~~~~~~~~~
627 The pattern match checker did not know how to handle coerced patterns `CoPat`
628 efficiently, which gave rise to #11276. The original approach translated
629 `CoPat`s:
630
631 pat |> co ===> x (pat <- (e |> co))
632
633 Instead, we now check whether the coercion is a hole or if it is just refl, in
634 which case we can drop it. Unfortunately, data families generate useful
635 coercions so guards are still generated in these cases and checking data
636 families is not really efficient.
637
638 %************************************************************************
639 %* *
640 Utilities for Pattern Match Checking
641 %* *
642 %************************************************************************
643 -}
644
645 -- ----------------------------------------------------------------------------
646 -- * Basic utilities
647
648 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
649 -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
650 pmPatType :: PmPat p -> Type
651 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
652 = mkTyConApp (dataConTyCon con) tys
653 pmPatType (PmVar { pm_var_id = x }) = idType x
654 pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
655 pmPatType (PmNLit { pm_lit_id = x }) = idType x
656 pmPatType (PmGrd { pm_grd_pv = pv })
657 = ASSERT(patVecArity pv == 1) (pmPatType p)
658 where Just p = find ((==1) . patternArity) pv
659
660 -- | Generate a value abstraction for a given constructor (generate
661 -- fresh variables of the appropriate type for arguments)
662 mkOneConFull :: Id -> DataCon -> PmM (ValAbs, ComplexEq, Bag EvVar)
663 -- * x :: T tys, where T is an algebraic data type
664 -- NB: in the case of a data familiy, T is the *representation* TyCon
665 -- e.g. data instance T (a,b) = T1 a b
666 -- leads to
667 -- data TPair a b = T1 a b -- The "representation" type
668 -- It is TPair, not T, that is given to mkOneConFull
669 --
670 -- * 'con' K is a constructor of data type T
671 --
672 -- After instantiating the universal tyvars of K we get
673 -- K tys :: forall bs. Q => s1 .. sn -> T tys
674 --
675 -- Results: ValAbs: K (y1::s1) .. (yn::sn)
676 -- ComplexEq: x ~ K y1..yn
677 -- [EvVar]: Q
678 mkOneConFull x con = do
679 let -- res_ty == TyConApp (dataConTyCon cabs_con) cabs_arg_tys
680 res_ty = idType x
681 (univ_tvs, ex_tvs, eq_spec, thetas, arg_tys, _) = dataConFullSig con
682 data_tc = dataConTyCon con -- The representation TyCon
683 tc_args = case splitTyConApp_maybe res_ty of
684 Just (tc, tys) -> ASSERT( tc == data_tc ) tys
685 Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty)
686 subst1 = zipTvSubst univ_tvs tc_args
687
688 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
689
690 -- Fresh term variables (VAs) as arguments to the constructor
691 arguments <- mapM mkPmVar (substTys subst arg_tys)
692 -- All constraints bound by the constructor (alpha-renamed)
693 let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
694 evvars <- mapM (nameType "pm") theta_cs
695 let con_abs = PmCon { pm_con_con = con
696 , pm_con_arg_tys = tc_args
697 , pm_con_tvs = ex_tvs'
698 , pm_con_dicts = evvars
699 , pm_con_args = arguments }
700 return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
701
702 -- ----------------------------------------------------------------------------
703 -- * More smart constructors and fresh variable generation
704
705 -- | Create a guard pattern
706 mkGuard :: PatVec -> HsExpr Id -> Pattern
707 mkGuard pv e
708 | all cantFailPattern pv = PmGrd pv expr
709 | PmExprOther {} <- expr = fake_pat
710 | otherwise = PmGrd pv expr
711 where
712 expr = hsExprToPmExpr e
713
714 -- | Create a term equality of the form: `(False ~ (x ~ lit))`
715 mkNegEq :: Id -> PmLit -> ComplexEq
716 mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
717 {-# INLINE mkNegEq #-}
718
719 -- | Create a term equality of the form: `(x ~ lit)`
720 mkPosEq :: Id -> PmLit -> ComplexEq
721 mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
722 {-# INLINE mkPosEq #-}
723
724 -- | Generate a variable pattern of a given type
725 mkPmVar :: Type -> PmM (PmPat p)
726 mkPmVar ty = PmVar <$> mkPmId ty
727 {-# INLINE mkPmVar #-}
728
729 -- | Generate many variable patterns, given a list of types
730 mkPmVars :: [Type] -> PmM PatVec
731 mkPmVars tys = mapM mkPmVar tys
732 {-# INLINE mkPmVars #-}
733
734 -- | Generate a fresh `Id` of a given type
735 mkPmId :: Type -> PmM Id
736 mkPmId ty = getUniqueM >>= \unique ->
737 let occname = mkVarOccFS (fsLit (show unique))
738 name = mkInternalName unique occname noSrcSpan
739 in return (mkLocalId name ty)
740
741 -- | Generate a fresh term variable of a given and return it in two forms:
742 -- * A variable pattern
743 -- * A variable expression
744 mkPmId2Forms :: Type -> PmM (Pattern, LHsExpr Id)
745 mkPmId2Forms ty = do
746 x <- mkPmId ty
747 return (PmVar x, noLoc (HsVar (noLoc x)))
748
749 -- ----------------------------------------------------------------------------
750 -- * Converting between Value Abstractions, Patterns and PmExpr
751
752 -- | Convert a value abstraction an expression
753 vaToPmExpr :: ValAbs -> PmExpr
754 vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
755 = PmExprCon c (map vaToPmExpr ps)
756 vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
757 vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
758 vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
759
760 -- | Convert a pattern vector to a list of value abstractions by dropping the
761 -- guards (See Note [Translating As Patterns])
762 coercePatVec :: PatVec -> [ValAbs]
763 coercePatVec pv = concatMap coercePmPat pv
764
765 -- | Convert a pattern to a list of value abstractions (will be either an empty
766 -- list if the pattern is a guard pattern, or a singleton list in all other
767 -- cases) by dropping the guards (See Note [Translating As Patterns])
768 coercePmPat :: Pattern -> [ValAbs]
769 coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
770 coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
771 coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
772 , pm_con_tvs = tvs, pm_con_dicts = dicts
773 , pm_con_args = args })
774 = [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
775 , pm_con_tvs = tvs, pm_con_dicts = dicts
776 , pm_con_args = coercePatVec args }]
777 coercePmPat (PmGrd {}) = [] -- drop the guards
778
779 -- | Get all constructors in the family (including given)
780 allConstructors :: DataCon -> [DataCon]
781 allConstructors = tyConDataCons . dataConTyCon
782
783 -- -----------------------------------------------------------------------
784 -- * Types and constraints
785
786 newEvVar :: Name -> Type -> EvVar
787 newEvVar name ty = mkLocalId name (toTcType ty)
788
789 nameType :: String -> Type -> PmM EvVar
790 nameType name ty = do
791 unique <- getUniqueM
792 let occname = mkVarOccFS (fsLit (name++"_"++show unique))
793 idname = mkInternalName unique occname noSrcSpan
794 return (newEvVar idname ty)
795
796 {-
797 %************************************************************************
798 %* *
799 The type oracle
800 %* *
801 %************************************************************************
802 -}
803
804 -- | Check whether a set of type constraints is satisfiable.
805 tyOracle :: Bag EvVar -> PmM Bool
806 tyOracle evs
807 = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
808 ; case res of
809 Just sat -> return sat
810 Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
811
812 {-
813 %************************************************************************
814 %* *
815 Sanity Checks
816 %* *
817 %************************************************************************
818 -}
819
820 -- | The arity of a pattern/pattern vector is the
821 -- number of top-level patterns that are not guards
822 type PmArity = Int
823
824 -- | Compute the arity of a pattern vector
825 patVecArity :: PatVec -> PmArity
826 patVecArity = sum . map patternArity
827
828 -- | Compute the arity of a pattern
829 patternArity :: Pattern -> PmArity
830 patternArity (PmGrd {}) = 0
831 patternArity _other_pat = 1
832
833 {-
834 %************************************************************************
835 %* *
836 Heart of the algorithm: Function pmcheck
837 %* *
838 %************************************************************************
839
840 Main functions are:
841
842 * mkInitialUncovered :: [Id] -> PmM Uncovered
843
844 Generates the initial uncovered set. Term and type constraints in scope
845 are checked, if they are inconsistent, the set is empty, otherwise, the
846 set contains only a vector of variables with the constraints in scope.
847
848 * pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM Triple
849
850 Checks redundancy, coverage and inaccessibility, using auxilary functions
851 `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
852 common in all three checks (see paper) and calls `pmcheckGuards` when the
853 whole clause is checked, or `pmcheckHd` when the pattern vector does not
854 start with a guard.
855
856 * pmcheckGuards :: [PatVec] -> ValVec -> PmM Triple
857
858 Processes the guards.
859
860 * pmcheckHd :: Pattern -> PatVec -> [PatVec]
861 -> ValAbs -> ValVec -> PmM Triple
862
863 Worker: This function implements functions `covered`, `uncovered` and
864 `divergent` from the paper at once. Slightly different from the paper because
865 it does not even produce the covered and uncovered sets. Since we only care
866 about whether a clause covers SOMETHING or if it may forces ANY argument, we
867 only store a boolean in both cases, for efficiency.
868 -}
869
870 -- | Lift a pattern matching action from a single value vector abstration to a
871 -- value set abstraction, but calling it on every vector and the combining the
872 -- results.
873 runMany :: (ValVec -> PmM Triple) -> (Uncovered -> PmM Triple)
874 runMany pm us = mapAndUnzip3M pm us >>= \(css, uss, dss) ->
875 return (or css, concat uss, or dss)
876 {-# INLINE runMany #-}
877
878 -- | Generate the initial uncovered set. It initializes the
879 -- delta with all term and type constraints in scope.
880 mkInitialUncovered :: [Id] -> PmM Uncovered
881 mkInitialUncovered vars = do
882 ty_cs <- getDictsDs
883 tm_cs <- map toComplex . bagToList <$> getTmCsDs
884 sat_ty <- tyOracle ty_cs
885 return $ case (sat_ty, tmOracle initialTmState tm_cs) of
886 (True, Just tm_state) -> [ValVec patterns (MkDelta ty_cs tm_state)]
887 -- If any of the term/type constraints are non
888 -- satisfiable, the initial uncovered set is empty
889 _non_satisfiable -> []
890 where
891 patterns = map PmVar vars
892
893 -- | Increase the counter for elapsed algorithm iterations, check that the
894 -- limit is not exceeded and call `pmcheck`
895 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM Triple
896 pmcheckI ps guards vva = incrCheckPmIterDs >> pmcheck ps guards vva
897 {-# INLINE pmcheckI #-}
898
899 -- | Increase the counter for elapsed algorithm iterations, check that the
900 -- limit is not exceeded and call `pmcheckGuards`
901 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM Triple
902 pmcheckGuardsI gvs vva = incrCheckPmIterDs >> pmcheckGuards gvs vva
903 {-# INLINE pmcheckGuardsI #-}
904
905 -- | Increase the counter for elapsed algorithm iterations, check that the
906 -- limit is not exceeded and call `pmcheckHd`
907 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -> PmM Triple
908 pmcheckHdI p ps guards va vva = incrCheckPmIterDs >>
909 pmcheckHd p ps guards va vva
910 {-# INLINE pmcheckHdI #-}
911
912 -- | Matching function: Check simultaneously a clause (takes separately the
913 -- patterns and the list of guards) for exhaustiveness, redundancy and
914 -- inaccessibility.
915 pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM Triple
916 pmcheck [] guards vva@(ValVec [] _)
917 | null guards = return (True, [], False)
918 | otherwise = pmcheckGuardsI guards vva
919
920 -- Guard
921 pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta)
922 -- short-circuit if the guard pattern is useless.
923 -- we just have two possible outcomes: fail here or match and recurse
924 -- none of the two contains any useful information about the failure
925 -- though. So just have these two cases but do not do all the boilerplate
926 | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
927 | otherwise = do
928 y <- mkPmId (pmPatType p)
929 let tm_state = extendSubst y e (delta_tm_cs delta)
930 delta' = delta { delta_tm_cs = tm_state }
931 utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
932
933 pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
934 pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
935
936 pmcheck (p:ps) guards (ValVec (va:vva) delta)
937 = pmcheckHdI p ps guards va (ValVec vva delta)
938
939 -- | Check the list of guards
940 pmcheckGuards :: [PatVec] -> ValVec -> PmM Triple
941 pmcheckGuards [] vva = return (False, [vva], False)
942 pmcheckGuards (gv:gvs) vva = do
943 (cs, vsa, ds ) <- pmcheckI gv [] vva
944 (css, vsas, dss) <- runMany (pmcheckGuardsI gvs) vsa
945 return (cs || css, vsas, ds || dss)
946
947 -- | Worker function: Implements all cases described in the paper for all three
948 -- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
949 -- cases which are handled by `pmcheck`
950 pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec -> PmM Triple
951
952 -- Var
953 pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
954 | Just tm_state <- solveOneEq (delta_tm_cs delta)
955 (PmExprVar (idName x), vaToPmExpr va)
956 = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
957 | otherwise = return (False, [], False)
958
959 -- ConCon
960 pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
961 (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
962 | c1 /= c2 = return (False, [ValVec (va:vva) delta], False)
963 | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
964 <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)
965
966 -- LitLit
967 pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva = case eqPmLit l1 l2 of
968 True -> ucon va <$> pmcheckI ps guards vva
969 False -> return $ ucon va (False, [vva], False)
970
971 -- ConVar
972 pmcheckHd (p@(PmCon { pm_con_con = con })) ps guards
973 (PmVar x) (ValVec vva delta) = do
974 cons_cs <- mapM (mkOneConFull x) (allConstructors con)
975 inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
976 let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
977 sat_ty <- if isEmptyBag ty_cs then return True
978 else tyOracle ty_state
979 return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
980 (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
981 _ty_or_tm_failed -> []
982
983 force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
984 runMany (pmcheckI (p:ps) guards) inst_vsa
985
986 -- LitVar
987 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
988 = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
989 mkUnion non_matched <$>
990 case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
991 Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
992 ValVec vva (delta {delta_tm_cs = tm_state})
993 Nothing -> return (False, [], False)
994 where
995 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
996 = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
997 | otherwise = []
998
999 non_matched = (False, us, False)
1000
1001 -- LitNLit
1002 pmcheckHd (p@(PmLit l)) ps guards
1003 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
1004 | all (not . eqPmLit l) lits
1005 , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
1006 -- Both guards check the same so it would be sufficient to have only
1007 -- the second one. Nevertheless, it is much cheaper to check whether
1008 -- the literal is in the list so we check it first, to avoid calling
1009 -- the term oracle (`solveOneEq`) if possible
1010 = mkUnion non_matched <$>
1011 pmcheckHdI p ps guards (PmLit l)
1012 (ValVec vva (delta { delta_tm_cs = tm_state }))
1013 | otherwise = return non_matched
1014 where
1015 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1016 = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
1017 | otherwise = []
1018
1019 non_matched = (False, us, False)
1020
1021 -- ----------------------------------------------------------------------------
1022 -- The following three can happen only in cases like #322 where constructors
1023 -- and overloaded literals appear in the same match. The general strategy is
1024 -- to replace the literal (positive/negative) by a variable and recurse. The
1025 -- fact that the variable is equal to the literal is recorded in `delta` so
1026 -- no information is lost
1027
1028 -- LitCon
1029 pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
1030 = do y <- mkPmId (pmPatType va)
1031 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1032 delta' = delta { delta_tm_cs = tm_state }
1033 pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
1034
1035 -- ConLit
1036 pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
1037 = do y <- mkPmId (pmPatType p)
1038 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1039 delta' = delta { delta_tm_cs = tm_state }
1040 pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
1041
1042 -- ConNLit
1043 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
1044 = pmcheckHdI p ps guards (PmVar x) vva
1045
1046 -- Impossible: handled by pmcheck
1047 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
1048
1049 -- ----------------------------------------------------------------------------
1050 -- * Utilities for main checking
1051
1052 -- | Take the tail of all value vector abstractions in the uncovered set
1053 utail :: Triple -> Triple
1054 utail (cs, vsa, ds) = (cs, vsa', ds)
1055 where vsa' = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ]
1056
1057 -- | Prepend a value abstraction to all value vector abstractions in the
1058 -- uncovered set
1059 ucon :: ValAbs -> Triple -> Triple
1060 ucon va (cs, vsa, ds) = (cs, vsa', ds)
1061 where vsa' = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ]
1062
1063 -- | Given a data constructor of arity `a` and an uncovered set containing
1064 -- value vector abstractions of length `(a+n)`, pass the first `n` value
1065 -- abstractions to the constructor (Hence, the resulting value vector
1066 -- abstractions will have length `n+1`)
1067 kcon :: DataCon -> [Type] -> [TyVar] -> [EvVar] -> Triple -> Triple
1068 kcon con arg_tys ex_tvs dicts (cs, vsa, ds)
1069 = (cs, [ ValVec (va:vva) delta
1070 | ValVec vva' delta <- vsa
1071 , let (args, vva) = splitAt n vva'
1072 , let va = PmCon { pm_con_con = con
1073 , pm_con_arg_tys = arg_tys
1074 , pm_con_tvs = ex_tvs
1075 , pm_con_dicts = dicts
1076 , pm_con_args = args } ]
1077 , ds)
1078 where n = dataConSourceArity con
1079
1080 -- | Get the union of two covered, uncovered and divergent value set
1081 -- abstractions. Since the covered and divergent sets are represented by a
1082 -- boolean, union means computing the logical or (at least one of the two is
1083 -- non-empty).
1084 mkUnion :: Triple -> Triple -> Triple
1085 mkUnion (cs1, vsa1, ds1) (cs2, vsa2, ds2)
1086 = (cs1 || cs2, vsa1 ++ vsa2, ds1 || ds2)
1087
1088 -- | Add a value vector abstraction to a value set abstraction (uncovered).
1089 mkCons :: ValVec -> Triple -> Triple
1090 mkCons vva (cs, vsa, ds) = (cs, vva:vsa, ds)
1091
1092 -- | Set the divergent set to not empty
1093 forces :: Triple -> Triple
1094 forces (cs, us, _) = (cs, us, True)
1095
1096 -- | Set the divergent set to non-empty if the flag is `True`
1097 force_if :: Bool -> Triple -> Triple
1098 force_if True (cs,us,_) = (cs,us,True)
1099 force_if False triple = triple
1100
1101 -- ----------------------------------------------------------------------------
1102 -- * Propagation of term constraints inwards when checking nested matches
1103
1104 {- Note [Type and Term Equality Propagation]
1105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1106 When checking a match it would be great to have all type and term information
1107 available so we can get more precise results. For this reason we have functions
1108 `addDictsDs' and `addTmCsDs' in DsMonad that store in the environment type and
1109 term constraints (respectively) as we go deeper.
1110
1111 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1112 in HsPat.hs. This handles bug #4139 ( see example
1113 https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
1114 where this is needed.
1115
1116 For term equalities we do less, we just generate equalities for HsCase. For
1117 example we accurately give 2 redundancy warnings for the marked cases:
1118
1119 f :: [a] -> Bool
1120 f x = case x of
1121
1122 [] -> case x of -- brings (x ~ []) in scope
1123 [] -> True
1124 (_:_) -> False -- can't happen
1125
1126 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1127 (_:_) -> True
1128 [] -> False -- can't happen
1129
1130 Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
1131 these constraints.
1132 -}
1133
1134 -- | Generate equalities when checking a case expression:
1135 -- case x of { p1 -> e1; ... pn -> en }
1136 -- When we go deeper to check e.g. e1 we record two equalities:
1137 -- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
1138 -- and (x ~ p1).
1139 genCaseTmCs2 :: Maybe (LHsExpr Id) -- Scrutinee
1140 -> [Pat Id] -- LHS (should have length 1)
1141 -> [Id] -- MatchVars (should have length 1)
1142 -> DsM (Bag SimpleEq)
1143 genCaseTmCs2 Nothing _ _ = return emptyBag
1144 genCaseTmCs2 (Just scr) [p] [var] = do
1145 fam_insts <- dsGetFamInstEnvs
1146 [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
1147 let scr_e = lhsExprToPmExpr scr
1148 return $ listToBag [(var, e), (var, scr_e)]
1149 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
1150
1151 -- | Generate a simple equality when checking a case expression:
1152 -- case x of { matches }
1153 -- When checking matches we record that (x ~ y) where y is the initial
1154 -- uncovered. All matches will have to satisfy this equality.
1155 genCaseTmCs1 :: Maybe (LHsExpr Id) -> [Id] -> Bag SimpleEq
1156 genCaseTmCs1 Nothing _ = emptyBag
1157 genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
1158 genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
1159
1160 {- Note [Literals in PmPat]
1161 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1162 Instead of translating a literal to a variable accompanied with a guard, we
1163 treat them like constructor patterns. The following example from
1164 "./libraries/base/GHC/IO/Encoding.hs" shows why:
1165
1166 mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
1167 mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
1168 "UTF8" -> return $ UTF8.mkUTF8 cfm
1169 "UTF16" -> return $ UTF16.mkUTF16 cfm
1170 "UTF16LE" -> return $ UTF16.mkUTF16le cfm
1171 ...
1172
1173 Each clause gets translated to a list of variables with an equal number of
1174 guards. For every guard we generate two cases (equals True/equals False) which
1175 means that we generate 2^n cases to feed the oracle with, where n is the sum of
1176 the length of all strings that appear in the patterns. For this particular
1177 example this means over 2^40 cases. Instead, by representing them like with
1178 constructor we get the following:
1179 1. We exploit the common prefix with our representation of VSAs
1180 2. We prune immediately non-reachable cases
1181 (e.g. False == (x == "U"), True == (x == "U"))
1182
1183 Note [Translating As Patterns]
1184 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1185 Instead of translating x@p as: x (p <- x)
1186 we instead translate it as: p (x <- coercePattern p)
1187 for performance reasons. For example:
1188
1189 f x@True = 1
1190 f y@False = 2
1191
1192 Gives the following with the first translation:
1193
1194 x |> {x == False, x == y, y == True}
1195
1196 If we use the second translation we get an empty set, independently of the
1197 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
1198 used as an expression. That's why we call `coercePatVec' to drop the guard and
1199 `vaToPmExpr' to transform the value abstraction to an expression in the
1200 guard pattern (value abstractions are a subset of expressions). We keep the
1201 guards in the first pattern `p' though.
1202
1203
1204 %************************************************************************
1205 %* *
1206 Pretty printing of exhaustiveness/redundancy check warnings
1207 %* *
1208 %************************************************************************
1209 -}
1210
1211 -- | Check whether any part of pattern match checking is enabled (does not
1212 -- matter whether it is the redundancy check or the exhaustiveness check).
1213 isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
1214 isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
1215 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
1216
1217 instance Outputable ValVec where
1218 ppr (ValVec vva delta)
1219 = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
1220 vector = substInValAbs subst vva
1221 in ppr_uncovered (vector, residual_eqs)
1222
1223 -- | Apply a term substitution to a value vector abstraction. All VAs are
1224 -- transformed to PmExpr (used only before pretty printing).
1225 substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
1226 substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
1227
1228 -- | Wrap up the term oracle's state once solving is complete. Drop any
1229 -- information about unhandled constraints (involving HsExprs) and flatten
1230 -- (height 1) the substitution.
1231 wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
1232 wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
1233
1234 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
1235 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
1236 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
1237 = when (flag_i || flag_u) $ do
1238 let exists_r = flag_i && notNull redundant
1239 exists_i = flag_i && notNull inaccessible
1240 exists_u = flag_u && notNull uncovered
1241 when exists_r $ putSrcSpanDs loc (warnDs (pprEqns redundant rmsg))
1242 when exists_i $ putSrcSpanDs loc (warnDs (pprEqns inaccessible imsg))
1243 when exists_u $ putSrcSpanDs loc (warnDs (pprEqnsU uncovered))
1244 where
1245 (redundant, uncovered, inaccessible) = pm_result
1246
1247 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1248 flag_u = exhaustive dflags kind
1249
1250 rmsg = "are redundant"
1251 imsg = "have inaccessible right hand side"
1252
1253 pprEqns qs txt = pp_context ctx (text txt) $ \f ->
1254 vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$ dots qs
1255
1256 pprEqnsU qs = pp_context ctx (text "are non-exhaustive") $ \_ ->
1257 case qs of -- See #11245
1258 [ValVec [] _]
1259 -> text "Guards do not cover entire pattern space"
1260 _missing -> let us = map ppr qs
1261 in hang (text "Patterns not matched:") 4
1262 (vcat (take maximum_output us) $$ dots us)
1263
1264 -- | Issue a warning when the predefined number of iterations is exceeded
1265 -- for the pattern match checker
1266 warnPmIters :: DynFlags -> DsMatchContext -> PmM ()
1267 warnPmIters dflags (DsMatchContext kind loc)
1268 = when (flag_i || flag_u) $ do
1269 iters <- maxPmCheckIterations <$> getDynFlags
1270 putSrcSpanDs loc (warnDs (msg iters))
1271 where
1272 ctxt = pprMatchContext kind
1273 msg is = fsep [ text "Pattern match checker exceeded"
1274 , parens (ppr is), text "iterations in", ctxt <> dot
1275 , text "(Use fmax-pmcheck-iterations=n"
1276 , text "to set the maximun number of iterations to n)" ]
1277
1278 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1279 flag_u = exhaustive dflags kind
1280
1281 dots :: [a] -> SDoc
1282 dots qs | qs `lengthExceeds` maximum_output = text "..."
1283 | otherwise = empty
1284
1285 -- | Check whether the exhaustiveness checker should run (exhaustiveness only)
1286 exhaustive :: DynFlags -> HsMatchContext id -> Bool
1287 exhaustive dflags (FunRhs {}) = wopt Opt_WarnIncompletePatterns dflags
1288 exhaustive dflags CaseAlt = wopt Opt_WarnIncompletePatterns dflags
1289 exhaustive _dflags IfAlt = False
1290 exhaustive dflags LambdaExpr = wopt Opt_WarnIncompleteUniPatterns dflags
1291 exhaustive dflags PatBindRhs = wopt Opt_WarnIncompleteUniPatterns dflags
1292 exhaustive dflags ProcExpr = wopt Opt_WarnIncompleteUniPatterns dflags
1293 exhaustive dflags RecUpd = wopt Opt_WarnIncompletePatternsRecUpd dflags
1294 exhaustive _dflags ThPatSplice = False
1295 exhaustive _dflags PatSyn = False
1296 exhaustive _dflags ThPatQuote = False
1297 exhaustive _dflags (StmtCtxt {}) = False -- Don't warn about incomplete patterns
1298 -- in list comprehensions, pattern guards
1299 -- etc. They are often *supposed* to be
1300 -- incomplete
1301
1302 pp_context :: DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
1303 pp_context (DsMatchContext kind _loc) msg rest_of_msg_fun
1304 = vcat [text "Pattern match(es)" <+> msg,
1305 sep [ text "In" <+> ppr_match <> char ':'
1306 , nest 4 (rest_of_msg_fun pref)]]
1307 where
1308 (ppr_match, pref)
1309 = case kind of
1310 FunRhs fun -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
1311 _ -> (pprMatchContext kind, \ pp -> pp)
1312
1313 ppr_pats :: HsMatchContext Name -> [Pat Id] -> SDoc
1314 ppr_pats kind pats
1315 = sep [sep (map ppr pats), matchSeparator kind, text "..."]
1316
1317 ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat Id] -> SDoc
1318 ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
1319
1320 ppr_constraint :: (SDoc,[PmLit]) -> SDoc
1321 ppr_constraint (var, lits) = var <+> text "is not one of"
1322 <+> braces (pprWithCommas ppr lits)
1323
1324 ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
1325 ppr_uncovered (expr_vec, complex)
1326 | null cs = fsep vec -- there are no literal constraints
1327 | otherwise = hang (fsep vec) 4 $
1328 text "where" <+> vcat (map ppr_constraint cs)
1329 where
1330 sdoc_vec = mapM pprPmExprWithParens expr_vec
1331 (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
1332
1333 -- | This variable shows the maximum number of lines of output generated for
1334 -- warnings. It will limit the number of patterns/equations displayed to
1335 -- maximum_output. (TODO: add command-line option?)
1336 maximum_output :: Int
1337 maximum_output = 4
1338
1339 {- Note [Representation of Term Equalities]
1340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1341 In the paper, term constraints always take the form (x ~ e). Of course, a more
1342 general constraint of the form (e1 ~ e1) can always be transformed to an
1343 equivalent set of the former constraints, by introducing a fresh, intermediate
1344 variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
1345 to #11160 (incredibly bad performance for literal pattern matching). Two are
1346 the main sources of this problem (the actual problem is how these two interact
1347 with each other):
1348
1349 1. Pattern matching on literals generates twice as many constraints as needed.
1350 Consider the following (tests/ghci/should_run/ghcirun004):
1351
1352 foo :: Int -> Int
1353 foo 1 = 0
1354 ...
1355 foo 5000 = 4999
1356
1357 The covered and uncovered set *should* look like:
1358 U0 = { x |> {} }
1359
1360 C1 = { 1 |> { x ~ 1 } }
1361 U1 = { x |> { False ~ (x ~ 1) } }
1362 ...
1363 C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
1364 U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
1365 ...
1366
1367 If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
1368 we get twice as many constraints. Also note that half of them are just the
1369 substitution [x |-> False].
1370
1371 2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
1372 (x ~ e) as substitutions [x |-> e]. More specifically, function
1373 `extendSubstAndSolve` applies such substitutions in the residual constraints
1374 and partitions them in the affected and non-affected ones, which are the new
1375 worklist. Essentially, this gives quadradic behaviour on the number of the
1376 residual constraints. (This would not be the case if the term oracle used
1377 mutable variables but, since we use it to handle disjunctions on value set
1378 abstractions (`Union` case), we chose a pure, incremental interface).
1379
1380 Now the problem becomes apparent (e.g. for clause 300):
1381 * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
1382 constraints that we know that will not reduce (stay in the worklist).
1383 * To check for consistency, we apply the substituting constraints ONE BY ONE
1384 (since `tmOracle` is called incrementally, it does not have all of them
1385 available at once). Hence, we go through the (non-progressing) constraints
1386 over and over, achieving over-quadradic behaviour.
1387
1388 If instead we allow constraints of the form (e ~ e),
1389 * All uncovered sets Ui contain no substituting constraints and i
1390 non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
1391 behaves linearly.
1392 * All covered sets Ci contain exactly (i-1) non-progressing constraints and
1393 a single substituting constraint. So the term oracle goes through the
1394 constraints only once.
1395
1396 The performance improvement becomes even more important when more arguments are
1397 involved.
1398 -}