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