pmcheck: Comments about undecidability of literal equality
[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 -- See Note [Undecidable Equality for Overloaded Literals]
1052 True -> VA va `mkCons` covered us gvsa ps vsa -- match
1053 False -> Empty -- mismatch
1054
1055 -- CConVar
1056 cMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
1057 = cMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa)
1058 where
1059 (us1, us2) = splitUniqSupply us
1060 (con_abs, all_cs) = mkOneConFull x us1 con
1061
1062 -- CLitVar
1063 cMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
1064 = cMatcher us gvsa p ps lit_abs (mkConstraint cs vsa)
1065 where
1066 lit_abs = PmLit l
1067 cs = [TmConstraint (PmExprVar x) (PmExprLit l)]
1068
1069 -- uMatcher
1070 -- ----------------------------------------------------------------------------
1071
1072 -- UVar
1073 uMatcher us gvsa (PmVar x) ps va vsa
1074 = VA va `mkCons` (cs `mkConstraint` uncovered us gvsa ps vsa)
1075 where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)]
1076
1077 -- ULitCon
1078 uMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
1079 = uMatcher us2 gvsa (PmVar y) ps va (mkConstraint cs vsa)
1080 where
1081 (us1, us2) = splitUniqSupply us
1082 y = mkPmId us1 (pmPatType va)
1083 cs = [TmConstraint (PmExprVar y) (PmExprLit l)]
1084
1085 -- UConLit
1086 uMatcher us gvsa (p@(PmCon {})) ps (PmLit l) vsa
1087 = uMatcher us2 gvsa p ps (PmVar y) (mkConstraint cs vsa)
1088 where
1089 (us1, us2) = splitUniqSupply us
1090 y = mkPmId us1 (pmPatType p)
1091 cs = [TmConstraint (PmExprVar y) (PmExprLit l)]
1092
1093 -- UConCon
1094 uMatcher us gvsa ( p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
1095 (va@(PmCon { pm_con_con = c2, pm_con_args = args2 })) vsa
1096 | c1 /= c2 = VA va `mkCons` vsa
1097 | otherwise = wrapK c1 (pm_con_arg_tys p)
1098 (pm_con_tvs p)
1099 (pm_con_dicts p)
1100 (uncovered us gvsa (args1 ++ ps)
1101 (foldr mkCons vsa args2))
1102
1103 -- ULitLit
1104 uMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
1105 -- See Note [Undecidable Equality for Overloaded Literals]
1106 True -> VA va `mkCons` uncovered us gvsa ps vsa -- match
1107 False -> VA va `mkCons` vsa -- mismatch
1108
1109 -- UConVar
1110 uMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
1111 = uncovered us2 gvsa (NonGuard p : ps) inst_vsa
1112 where
1113 (us1, us2) = splitUniqSupply us
1114
1115 -- Unfold the variable to all possible constructor patterns
1116 cons_cs = zipWith (mkOneConFull x) (listSplitUniqSupply us1)
1117 (allConstructors con)
1118 add_one (va,cs) valset = mkUnion valset
1119 (mkCons (VA va) (mkConstraint cs vsa))
1120 inst_vsa = foldr add_one Empty cons_cs -- instantiated vsa [x mapsto K_j ys]
1121
1122 -- ULitVar
1123 uMatcher us gvsa (p@(PmLit l)) ps (PmVar x) vsa
1124 = mkUnion (uMatcher us gvsa p ps (PmLit l) (mkConstraint match_cs vsa))
1125 (non_match_cs `mkConstraint` (VA (PmVar x) `mkCons` vsa))
1126 where
1127 match_cs = [ TmConstraint (PmExprVar x) (PmExprLit l)]
1128 -- See Note [Representation of Term Equalities]
1129 non_match_cs = [ TmConstraint falsePmExpr
1130 (PmExprEq (PmExprVar x) (PmExprLit l)) ]
1131
1132 -- dMatcher
1133 -- ----------------------------------------------------------------------------
1134
1135 -- DVar
1136 dMatcher us gvsa (PmVar x) ps va vsa
1137 = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
1138 where cs = [TmConstraint (PmExprVar x) (pmPatToPmExpr va)]
1139
1140 -- DLitCon
1141 dMatcher us gvsa (PmLit l) ps (va@(PmCon {})) vsa
1142 = VA va `mkCons` (cs `mkConstraint` divergent us gvsa ps vsa)
1143 where cs = [ TmConstraint (PmExprLit l) (pmPatToPmExpr va) ]
1144
1145 -- DConLit
1146 dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmLit l) vsa
1147 = dMatcher us3 gvsa p ps con_abs (mkConstraint cs vsa)
1148 where
1149 (us1, us2, us3) = splitUniqSupply3 us
1150 y = mkPmId us1 (pmPatType p)
1151 (con_abs, all_cs) = mkOneConFull y us2 con
1152 cs = TmConstraint (PmExprVar y) (PmExprLit l) : all_cs
1153
1154 -- DConCon
1155 dMatcher us gvsa (p@(PmCon { pm_con_con = c1, pm_con_args = args1 })) ps
1156 (PmCon { pm_con_con = c2, pm_con_args = args2 }) vsa
1157 | c1 /= c2 = Empty
1158 | otherwise = wrapK c1 (pm_con_arg_tys p)
1159 (pm_con_tvs p)
1160 (pm_con_dicts p)
1161 (divergent us gvsa (args1 ++ ps)
1162 (foldr mkCons vsa args2))
1163
1164 -- DLitLit
1165 dMatcher us gvsa (PmLit l1) ps (va@(PmLit l2)) vsa = case eqPmLit l1 l2 of
1166 -- See Note [Undecidable Equality for Overloaded Literals]
1167 True -> VA va `mkCons` divergent us gvsa ps vsa -- match
1168 False -> Empty -- mismatch
1169
1170 -- DConVar
1171 dMatcher us gvsa (p@(PmCon { pm_con_con = con })) ps (PmVar x) vsa
1172 = mkUnion (VA (PmVar x) `mkCons` mkConstraint [BtConstraint x] vsa)
1173 (dMatcher us2 gvsa p ps con_abs (mkConstraint all_cs vsa))
1174 where
1175 (us1, us2) = splitUniqSupply us
1176 (con_abs, all_cs) = mkOneConFull x us1 con
1177
1178 -- DLitVar
1179 dMatcher us gvsa (PmLit l) ps (PmVar x) vsa
1180 = mkUnion (VA (PmVar x) `mkCons` mkConstraint [BtConstraint x] vsa)
1181 (dMatcher us gvsa (PmLit l) ps (PmLit l) (mkConstraint cs vsa))
1182 where
1183 cs = [TmConstraint (PmExprVar x) (PmExprLit l)]
1184
1185 -- ----------------------------------------------------------------------------
1186 -- * Propagation of term constraints inwards when checking nested matches
1187
1188 {- Note [Type and Term Equality Propagation]
1189 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1190 When checking a match it would be great to have all type and term information
1191 available so we can get more precise results. For this reason we have functions
1192 `addDictsDs' and `addTmCsDs' in DsMonad that store in the environment type and
1193 term constraints (respectively) as we go deeper.
1194
1195 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1196 in HsPat.hs. This handles bug #4139 ( see example
1197 https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
1198 where this is needed.
1199
1200 For term equalities we do less, we just generate equalities for HsCase. For
1201 example we accurately give 2 redundancy warnings for the marked cases:
1202
1203 f :: [a] -> Bool
1204 f x = case x of
1205
1206 [] -> case x of -- brings (x ~ []) in scope
1207 [] -> True
1208 (_:_) -> False -- can't happen
1209
1210 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1211 (_:_) -> True
1212 [] -> False -- can't happen
1213
1214 Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
1215 these constraints.
1216 -}
1217
1218 -- | Generate equalities when checking a case expression:
1219 -- case x of { p1 -> e1; ... pn -> en }
1220 -- When we go deeper to check e.g. e1 we record two equalities:
1221 -- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
1222 -- and (x ~ p1).
1223 genCaseTmCs2 :: Maybe (LHsExpr Id) -- Scrutinee
1224 -> [Pat Id] -- LHS (should have length 1)
1225 -> [Id] -- MatchVars (should have length 1)
1226 -> DsM (Bag SimpleEq)
1227 genCaseTmCs2 Nothing _ _ = return emptyBag
1228 genCaseTmCs2 (Just scr) [p] [var] = liftUs $ do
1229 [e] <- map valAbsToPmExpr . coercePatVec <$> translatePat p
1230 let scr_e = lhsExprToPmExpr scr
1231 return $ listToBag [(var, e), (var, scr_e)]
1232 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
1233
1234 -- | Generate a simple equality when checking a case expression:
1235 -- case x of { matches }
1236 -- When checking matches we record that (x ~ y) where y is the initial
1237 -- uncovered. All matches will have to satisfy this equality.
1238 genCaseTmCs1 :: Maybe (LHsExpr Id) -> [Id] -> Bag SimpleEq
1239 genCaseTmCs1 Nothing _ = emptyBag
1240 genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
1241 genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
1242
1243 {- Note [Literals in PmPat]
1244 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1245 Instead of translating a literal to a variable accompanied with a guard, we
1246 treat them like constructor patterns. The following example from
1247 "./libraries/base/GHC/IO/Encoding.hs" shows why:
1248
1249 mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
1250 mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
1251 "UTF8" -> return $ UTF8.mkUTF8 cfm
1252 "UTF16" -> return $ UTF16.mkUTF16 cfm
1253 "UTF16LE" -> return $ UTF16.mkUTF16le cfm
1254 ...
1255
1256 Each clause gets translated to a list of variables with an equal number of
1257 guards. For every guard we generate two cases (equals True/equals False) which
1258 means that we generate 2^n cases to feed the oracle with, where n is the sum of
1259 the length of all strings that appear in the patterns. For this particular
1260 example this means over 2^40 cases. Instead, by representing them like with
1261 constructor we get the following:
1262 1. We exploit the common prefix with our representation of VSAs
1263 2. We prune immediately non-reachable cases
1264 (e.g. False == (x == "U"), True == (x == "U"))
1265
1266 Note [Translating As Patterns]
1267 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1268 Instead of translating x@p as: x (p <- x)
1269 we instead translate it as: p (x <- coercePattern p)
1270 for performance reasons. For example:
1271
1272 f x@True = 1
1273 f y@False = 2
1274
1275 Gives the following with the first translation:
1276
1277 x |> {x == False, x == y, y == True}
1278
1279 If we use the second translation we get an empty set, independently of the
1280 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
1281 used as an expression. That's why we call `coercePatVec' to drop the guard and
1282 `valAbsToPmExpr' to transform the value abstraction to an expression in the
1283 guard pattern (value abstractions are a subset of expressions). We keep the
1284 guards in the first pattern `p' though.
1285 -}
1286
1287 {-
1288 %************************************************************************
1289 %* *
1290 Pretty printing of exhaustiveness/redundancy check warnings
1291 %* *
1292 %************************************************************************
1293 -}
1294
1295 dsPmWarn :: DynFlags -> DsMatchContext -> DsM PmResult -> DsM ()
1296 dsPmWarn dflags ctx@(DsMatchContext kind loc) mPmResult
1297 = when (flag_i || flag_u) $ do
1298 (redundant, inaccessible, uncovered) <- mPmResult
1299 let exists_r = flag_i && notNull redundant
1300 exists_i = flag_i && notNull inaccessible
1301 exists_u = flag_u && notNull uncovered
1302 when exists_r $ putSrcSpanDs loc (warnDs (pprEqns redundant rmsg))
1303 when exists_i $ putSrcSpanDs loc (warnDs (pprEqns inaccessible imsg))
1304 when exists_u $ putSrcSpanDs loc (warnDs (pprEqnsU uncovered))
1305 where
1306 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1307 flag_u = exhaustive dflags kind
1308
1309 rmsg = "are redundant"
1310 imsg = "have inaccessible right hand side"
1311
1312 pprEqns qs text = pp_context ctx (ptext (sLit text)) $ \f ->
1313 vcat (map (ppr_eqn f kind) (take maximum_output qs)) $$ dots qs
1314
1315 pprEqnsU qs = pp_context ctx (ptext (sLit "are non-exhaustive")) $ \_ ->
1316 let us = map ppr_uncovered qs
1317 in hang (ptext (sLit "Patterns not matched:")) 4
1318 (vcat (take maximum_output us) $$ dots us)
1319
1320 dots :: [a] -> SDoc
1321 dots qs | qs `lengthExceeds` maximum_output = ptext (sLit "...")
1322 | otherwise = empty
1323
1324 exhaustive :: DynFlags -> HsMatchContext id -> Bool
1325 exhaustive dflags (FunRhs {}) = wopt Opt_WarnIncompletePatterns dflags
1326 exhaustive dflags CaseAlt = wopt Opt_WarnIncompletePatterns dflags
1327 exhaustive _dflags IfAlt = False
1328 exhaustive dflags LambdaExpr = wopt Opt_WarnIncompleteUniPatterns dflags
1329 exhaustive dflags PatBindRhs = wopt Opt_WarnIncompleteUniPatterns dflags
1330 exhaustive dflags ProcExpr = wopt Opt_WarnIncompleteUniPatterns dflags
1331 exhaustive dflags RecUpd = wopt Opt_WarnIncompletePatternsRecUpd dflags
1332 exhaustive _dflags ThPatSplice = False
1333 exhaustive _dflags PatSyn = False
1334 exhaustive _dflags ThPatQuote = False
1335 exhaustive _dflags (StmtCtxt {}) = False -- Don't warn about incomplete patterns
1336 -- in list comprehensions, pattern guards
1337 -- etc. They are often *supposed* to be
1338 -- incomplete
1339
1340 pp_context :: DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
1341 pp_context (DsMatchContext kind _loc) msg rest_of_msg_fun
1342 = vcat [ptext (sLit "Pattern match(es)") <+> msg,
1343 sep [ ptext (sLit "In") <+> ppr_match <> char ':'
1344 , nest 4 (rest_of_msg_fun pref)]]
1345 where
1346 (ppr_match, pref)
1347 = case kind of
1348 FunRhs fun -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
1349 _ -> (pprMatchContext kind, \ pp -> pp)
1350
1351 ppr_pats :: HsMatchContext Name -> [Pat Id] -> SDoc
1352 ppr_pats kind pats
1353 = sep [sep (map ppr pats), matchSeparator kind, ptext (sLit "...")]
1354
1355 ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat Id] -> SDoc
1356 ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
1357
1358 ppr_constraint :: (SDoc,[PmLit]) -> SDoc
1359 ppr_constraint (var, lits) = var <+> ptext (sLit "is not one of")
1360 <+> braces (pprWithCommas ppr lits)
1361
1362 ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
1363 ppr_uncovered (expr_vec, complex)
1364 | null cs = fsep vec -- there are no literal constraints
1365 | otherwise = hang (fsep vec) 4 $
1366 ptext (sLit "where") <+> vcat (map ppr_constraint cs)
1367 where
1368 sdoc_vec = mapM pprPmExprWithParens expr_vec
1369 (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
1370
1371 {- Note [Representation of Term Equalities]
1372 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1373 In the paper, term constraints always take the form (x ~ e). Of course, a more
1374 general constraint of the form (e1 ~ e1) can always be transformed to an
1375 equivalent set of the former constraints, by introducing a fresh, intermediate
1376 variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
1377 to #11160 (incredibly bad performance for literal pattern matching). Two are
1378 the main sources of this problem (the actual problem is how these two interact
1379 with each other):
1380
1381 1. Pattern matching on literals generates twice as many constraints as needed.
1382 Consider the following (tests/ghci/should_run/ghcirun004):
1383
1384 foo :: Int -> Int
1385 foo 1 = 0
1386 ...
1387 foo 5000 = 4999
1388
1389 The covered and uncovered set *should* look like:
1390 U0 = { x |> {} }
1391
1392 C1 = { 1 |> { x ~ 1 } }
1393 U1 = { x |> { False ~ (x ~ 1) } }
1394 ...
1395 C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
1396 U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
1397 ...
1398
1399 If replace { False ~ (x ~ 1) }, with { y ~ False, y ~ (x ~ 1) }
1400 we get twice as many constraints. Also note that half of them are just the
1401 substitution [x |-> False].
1402
1403 2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
1404 (x ~ e) as substitutions [x |-> e]. More specifically, function
1405 `extendSubstAndSolve` applies such substitutions in the residual constraints
1406 and partitions them in the affected and non-affected ones, which are the new
1407 worklist. Essentially, this gives quadradic behaviour on the number of the
1408 residual constraints. (This would not be the case if the term oracle used
1409 mutable variables but, since we use it to handle disjunctions on value set
1410 abstractions (`Union` case), we chose a pure, incremental interface).
1411
1412 Now the problem becomes apparent (e.g. for clause 300):
1413 * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
1414 constraints that we know that will not reduce (stay in the worklist).
1415 * To check for consistency, we apply the substituting constraints ONE BY ONE
1416 (since `tmOracle` is called incrementally, it does not have all of them
1417 available at once). Hence, we go through the (non-progressing) constraints
1418 over and over, achieving over-quadradic behaviour.
1419
1420 If instead we allow constraints of the form (e ~ e),
1421 * All uncovered sets Ui contain no substituting constraints and i
1422 non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
1423 behaves linearly.
1424 * All covered sets Ci contain exactly (i-1) non-progressing constraints and
1425 a single substituting constraint. So the term oracle goes through the
1426 constraints only once.
1427
1428 The performance improvement becomes even more important when more arguments are
1429 involved.
1430 -}