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