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