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