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