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