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