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