COMPLETE pragmas for enhanced pattern exhaustiveness checking
[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 {-# LANGUAGE TupleSections #-}
9
10 module Check (
11 -- Checking and printing
12 checkSingle, checkMatches, isAnyPmCheckEnabled,
13
14 -- See Note [Type and Term Equality Propagation]
15 genCaseTmCs1, genCaseTmCs2
16 ) where
17
18 #include "HsVersions.h"
19
20 import TmOracle
21
22 import DynFlags
23 import HsSyn
24 import TcHsSyn
25 import Id
26 import ConLike
27 import Name
28 import FamInstEnv
29 import TysWiredIn
30 import TyCon
31 import SrcLoc
32 import Util
33 import Outputable
34 import FastString
35 import DataCon
36 import HscTypes (CompleteMatch(..))
37
38 import DsMonad
39 import TcSimplify (tcCheckSatisfiability)
40 import TcType (toTcType, isStringTy, isIntTy, isWordTy)
41 import Bag
42 import ErrUtils
43 import Var (EvVar)
44 import Type
45 import UniqSupply
46 import DsGRHSs (isTrueLHsExpr)
47
48 import Data.List (find)
49 import Data.Maybe (isJust)
50 import Control.Monad (forM, when, forM_)
51 import Coercion
52 import TcEvidence
53 import IOEnv
54 import Data.Monoid ( Monoid(mappend) )
55
56 import ListT (ListT(..), fold, select)
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 is based on 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 -- We use the non-determinism monad to apply the algorithm to several
81 -- possible sets of constructors. Users can specify complete sets of
82 -- constructors by using COMPLETE pragmas.
83 -- The algorithm only picks out constructor
84 -- sets deep in the bowels which makes a simpler `mapM` more difficult to
85 -- implement. The non-determinism is only used in one place, see the ConVar
86 -- case in `pmCheckHd`.
87
88 type PmM a = ListT DsM a
89
90 liftD :: DsM a -> PmM a
91 liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
92
93 -- Pick the first match complete covered match or otherwise the "best" match.
94 -- The best match is the one with the least uncovered clauses, ties broken
95 -- by the number of inaccessible clauses followed by number of redudant
96 -- clauses
97 getResult :: PmM PmResult -> DsM PmResult
98 getResult ls = do
99 res <- fold ls goM (pure Nothing)
100 case res of
101 Nothing -> panic "getResult is empty"
102 Just a -> return a
103 where
104 goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
105 goM mpm dpm = do
106 pmr <- dpm
107 return $ go pmr mpm
108 -- Careful not to force unecessary results
109 go :: Maybe PmResult -> PmResult -> Maybe PmResult
110 go Nothing rs = Just rs
111 go old@(Just (PmResult prov rs us is)) new
112 | null us && null rs && null is = old
113 | otherwise =
114 let PmResult prov' rs' us' is' = new
115 lr = length rs
116 lr' = length rs'
117 li = length is
118 li' = length is'
119 in case compare (length us) (length us')
120 `mappend` (compare li li')
121 `mappend` (compare lr lr')
122 `mappend` (compare prov prov') of
123 GT -> Just new
124 EQ -> Just new
125 LT -> old
126
127 data PatTy = PAT | VA -- Used only as a kind, to index PmPat
128
129 -- The *arity* of a PatVec [p1,..,pn] is
130 -- the number of p1..pn that are not Guards
131
132 data PmPat :: PatTy -> * where
133 PmCon :: { pm_con_con :: ConLike
134 , pm_con_arg_tys :: [Type]
135 , pm_con_tvs :: [TyVar]
136 , pm_con_dicts :: [EvVar]
137 , pm_con_args :: [PmPat t] } -> PmPat t
138 -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
139 PmVar :: { pm_var_id :: Id } -> PmPat t
140 PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
141 PmNLit :: { pm_lit_id :: Id
142 , pm_lit_not :: [PmLit] } -> PmPat 'VA
143 PmGrd :: { pm_grd_pv :: PatVec
144 , pm_grd_expr :: PmExpr } -> PmPat 'PAT
145
146 -- data T a where
147 -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
148 -- or MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
149
150 type Pattern = PmPat 'PAT -- ^ Patterns
151 type ValAbs = PmPat 'VA -- ^ Value Abstractions
152
153 type PatVec = [Pattern] -- ^ Pattern Vectors
154 data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions
155
156 -- | Term and type constraints to accompany each value vector abstraction.
157 -- For efficiency, we store the term oracle state instead of the term
158 -- constraints. TODO: Do the same for the type constraints?
159 data Delta = MkDelta { delta_ty_cs :: Bag EvVar
160 , delta_tm_cs :: TmState }
161
162 type ValSetAbs = [ValVec] -- ^ Value Set Abstractions
163 type Uncovered = ValSetAbs
164
165 -- Instead of keeping the whole sets in memory, we keep a boolean for both the
166 -- covered and the divergent set (we store the uncovered set though, since we
167 -- want to print it). For both the covered and the divergent we have:
168 --
169 -- True <=> The set is non-empty
170 --
171 -- hence:
172 -- C = True ==> Useful clause (no warning)
173 -- C = False, D = True ==> Clause with inaccessible RHS
174 -- C = False, D = False ==> Redundant clause
175
176 data Covered = Covered | NotCovered
177 deriving Show
178
179 instance Outputable Covered where
180 ppr (Covered) = text "Covered"
181 ppr (NotCovered) = text "NotCovered"
182
183 -- Like the or monoid for booleans
184 -- Covered = True, Uncovered = False
185 instance Monoid Covered where
186 mempty = NotCovered
187 Covered `mappend` _ = Covered
188 _ `mappend` Covered = Covered
189 NotCovered `mappend` NotCovered = NotCovered
190
191 data Diverged = Diverged | NotDiverged
192 deriving Show
193
194 instance Outputable Diverged where
195 ppr Diverged = text "Diverged"
196 ppr NotDiverged = text "NotDiverged"
197
198 instance Monoid Diverged where
199 mempty = NotDiverged
200 Diverged `mappend` _ = Diverged
201 _ `mappend` Diverged = Diverged
202 NotDiverged `mappend` NotDiverged = NotDiverged
203
204 -- | When we learned that a given match group is complete
205 data Provenance =
206 FromBuiltin -- ^ From the original definition of the type
207 -- constructor.
208 | FromComplete -- ^ From a user-provided @COMPLETE@ pragma
209 deriving (Show, Eq, Ord)
210
211 instance Outputable Provenance where
212 ppr = text . show
213
214 instance Monoid Provenance where
215 mempty = FromBuiltin
216 FromComplete `mappend` _ = FromComplete
217 _ `mappend` FromComplete = FromComplete
218 _ `mappend` _ = FromBuiltin
219
220 data PartialResult = PartialResult {
221 presultProvenence :: Provenance
222 -- keep track of provenance because we don't want
223 -- to warn about redundant matches if the result
224 -- is contaiminated with a COMPLETE pragma
225 , presultCovered :: Covered
226 , presultUncovered :: Uncovered
227 , presultDivergent :: Diverged }
228
229 instance Outputable PartialResult where
230 ppr (PartialResult prov c vsa d)
231 = text "PartialResult" <+> ppr prov <+> ppr c
232 <+> ppr d <+> ppr vsa
233
234 instance Monoid PartialResult where
235 mempty = PartialResult mempty mempty [] mempty
236 (PartialResult prov1 cs1 vsa1 ds1)
237 `mappend` (PartialResult prov2 cs2 vsa2 ds2)
238 = PartialResult (prov1 `mappend` prov2)
239 (cs1 `mappend` cs2)
240 (vsa1 `mappend` vsa2)
241 (ds1 `mappend` ds2)
242
243 -- newtype ChoiceOf a = ChoiceOf [a]
244
245 -- | Pattern check result
246 --
247 -- * Redundant clauses
248 -- * Not-covered clauses
249 -- * Clauses with inaccessible RHS
250 data PmResult =
251 PmResult {
252 pmresultProvenance :: Provenance
253 , pmresultRedundant :: [Located [LPat Id]]
254 , pmresultUncovered :: Uncovered
255 , pmresultInaccessible :: [Located [LPat Id]] }
256
257 {-
258 %************************************************************************
259 %* *
260 Entry points to the checker: checkSingle and checkMatches
261 %* *
262 %************************************************************************
263 -}
264
265 -- | Check a single pattern binding (let)
266 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat Id -> DsM ()
267 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
268 tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
269 mb_pm_res <- tryM (getResult (checkSingle' locn var p))
270 case mb_pm_res of
271 Left _ -> warnPmIters dflags ctxt
272 Right res -> dsPmWarn dflags ctxt res
273
274 -- | Check a single pattern binding (let)
275 checkSingle' :: SrcSpan -> Id -> Pat Id -> PmM PmResult
276 checkSingle' locn var p = do
277 liftD resetPmIterDs -- set the iter-no to zero
278 fam_insts <- liftD dsGetFamInstEnvs
279 clause <- liftD $ translatePat fam_insts p
280 missing <- mkInitialUncovered [var]
281 tracePm "checkSingle: missing" (vcat (map pprValVecDebug missing))
282 -- no guards
283 PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
284 return $ case (cs,ds) of
285 (Covered, _ ) -> PmResult prov [] us [] -- useful
286 (NotCovered, NotDiverged) -> PmResult prov m us [] -- redundant
287 (NotCovered, Diverged ) -> PmResult prov [] us m -- inaccessible rhs
288 where m = [L locn [L locn p]]
289
290 -- | Check a matchgroup (case, functions, etc.)
291 checkMatches :: DynFlags -> DsMatchContext
292 -> [Id] -> [LMatch Id (LHsExpr Id)] -> DsM ()
293 checkMatches dflags ctxt vars matches = do
294 tracePmD "checkMatches" (hang (vcat [ppr ctxt
295 , ppr vars
296 , text "Matches:"])
297 2
298 (vcat (map ppr matches)))
299 mb_pm_res <- tryM (getResult (checkMatches' vars matches))
300 case mb_pm_res of
301 Left _ -> warnPmIters dflags ctxt
302 Right res -> dsPmWarn dflags ctxt res
303
304 -- | Check a matchgroup (case, functions, etc.)
305 checkMatches' :: [Id] -> [LMatch Id (LHsExpr Id)] -> PmM PmResult
306 checkMatches' vars matches
307 | null matches = return $ PmResult FromBuiltin [] [] []
308 | otherwise = do
309 liftD resetPmIterDs -- set the iter-no to zero
310 missing <- mkInitialUncovered vars
311 tracePm "checkMatches: missing" (vcat (map pprValVecDebug missing))
312 (prov, rs,us,ds) <- go matches missing
313 return
314 $ PmResult prov (map hsLMatchToLPats rs) us (map hsLMatchToLPats ds)
315 where
316 go :: [LMatch Id (LHsExpr Id)] -> Uncovered
317 -> PmM (Provenance
318 , [LMatch Id (LHsExpr Id)]
319 , Uncovered
320 , [LMatch Id (LHsExpr Id)])
321 go [] missing = return (mempty, [], missing, [])
322 go (m:ms) missing = do
323 tracePm "checMatches': go" (ppr m $$ ppr missing)
324 fam_insts <- liftD dsGetFamInstEnvs
325 (clause, guards) <- liftD $ translateMatch fam_insts m
326 r@(PartialResult prov cs missing' ds)
327 <- runMany (pmcheckI clause guards) missing
328 tracePm "checMatches': go: res" (ppr r)
329 (ms_prov, rs, final_u, is) <- go ms missing'
330 let final_prov = prov `mappend` ms_prov
331 return $ case (cs, ds) of
332 -- useful
333 (Covered, _ ) -> (final_prov, rs, final_u, is)
334 -- redundant
335 (NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
336 -- inaccessible
337 (NotCovered, Diverged ) -> (final_prov, rs, final_u, m:is)
338
339 hsLMatchToLPats :: LMatch id body -> Located [LPat id]
340 hsLMatchToLPats (L l (Match _ pats _ _)) = L l pats
341
342 {-
343 %************************************************************************
344 %* *
345 Transform source syntax to *our* syntax
346 %* *
347 %************************************************************************
348 -}
349
350 -- -----------------------------------------------------------------------
351 -- * Utilities
352
353 nullaryConPattern :: ConLike -> Pattern
354 -- Nullary data constructor and nullary type constructor
355 nullaryConPattern con =
356 PmCon { pm_con_con = con, pm_con_arg_tys = []
357 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
358 {-# INLINE nullaryConPattern #-}
359
360 truePattern :: Pattern
361 truePattern = nullaryConPattern (RealDataCon trueDataCon)
362 {-# INLINE truePattern #-}
363
364 -- | A fake guard pattern (True <- _) used to represent cases we cannot handle
365 fake_pat :: Pattern
366 fake_pat = PmGrd { pm_grd_pv = [truePattern]
367 , pm_grd_expr = PmExprOther EWildPat }
368 {-# INLINE fake_pat #-}
369
370 -- | Check whether a guard pattern is generated by the checker (unhandled)
371 isFakeGuard :: [Pattern] -> PmExpr -> Bool
372 isFakeGuard [PmCon { pm_con_con = RealDataCon c }] (PmExprOther EWildPat)
373 | c == trueDataCon = True
374 | otherwise = False
375 isFakeGuard _pats _e = False
376
377 -- | Generate a `canFail` pattern vector of a specific type
378 mkCanFailPmPat :: Type -> DsM PatVec
379 mkCanFailPmPat ty = do
380 var <- mkPmVar ty
381 return [var, fake_pat]
382
383 vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
384 -- ADT constructor pattern => no existentials, no local constraints
385 vanillaConPattern con arg_tys args =
386 PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
387 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
388 {-# INLINE vanillaConPattern #-}
389
390 -- | Create an empty list pattern of a given type
391 nilPattern :: Type -> Pattern
392 nilPattern ty =
393 PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
394 , pm_con_tvs = [], pm_con_dicts = []
395 , pm_con_args = [] }
396 {-# INLINE nilPattern #-}
397
398 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
399 mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
400 , pm_con_arg_tys = [ty]
401 , pm_con_tvs = [], pm_con_dicts = []
402 , pm_con_args = xs++ys }]
403 {-# INLINE mkListPatVec #-}
404
405 -- | Create a (non-overloaded) literal pattern
406 mkLitPattern :: HsLit -> Pattern
407 mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
408 {-# INLINE mkLitPattern #-}
409
410 -- -----------------------------------------------------------------------
411 -- * Transform (Pat Id) into of (PmPat Id)
412
413 translatePat :: FamInstEnvs -> Pat Id -> DsM PatVec
414 translatePat fam_insts pat = case pat of
415 WildPat ty -> mkPmVars [ty]
416 VarPat id -> return [PmVar (unLoc id)]
417 ParPat p -> translatePat fam_insts (unLoc p)
418 LazyPat _ -> mkPmVars [hsPatType pat] -- like a variable
419
420 -- ignore strictness annotations for now
421 BangPat p -> translatePat fam_insts (unLoc p)
422
423 AsPat lid p -> do
424 -- Note [Translating As Patterns]
425 ps <- translatePat fam_insts (unLoc p)
426 let [e] = map vaToPmExpr (coercePatVec ps)
427 g = PmGrd [PmVar (unLoc lid)] e
428 return (ps ++ [g])
429
430 SigPatOut p _ty -> translatePat fam_insts (unLoc p)
431
432 -- See Note [Translate CoPats]
433 CoPat wrapper p ty
434 | isIdHsWrapper wrapper -> translatePat fam_insts p
435 | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p
436 | otherwise -> do
437 ps <- translatePat fam_insts p
438 (xp,xe) <- mkPmId2Forms ty
439 let g = mkGuard ps (HsWrap wrapper (unLoc xe))
440 return [xp,g]
441
442 -- (n + k) ===> x (True <- x >= k) (n <- x-k)
443 NPlusKPat (L _ _n) _k1 _k2 _ge _minus ty -> mkCanFailPmPat ty
444
445 -- (fun -> pat) ===> x (pat <- fun x)
446 ViewPat lexpr lpat arg_ty -> do
447 ps <- translatePat fam_insts (unLoc lpat)
448 -- See Note [Guards and Approximation]
449 case all cantFailPattern ps of
450 True -> do
451 (xp,xe) <- mkPmId2Forms arg_ty
452 let g = mkGuard ps (HsApp lexpr xe)
453 return [xp,g]
454 False -> mkCanFailPmPat arg_ty
455
456 -- list
457 ListPat ps ty Nothing -> do
458 foldr (mkListPatVec ty) [nilPattern ty]
459 <$> translatePatVec fam_insts (map unLoc ps)
460
461 -- overloaded list
462 ListPat lpats elem_ty (Just (pat_ty, _to_list))
463 | Just e_ty <- splitListTyConApp_maybe pat_ty
464 , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty
465 -- elem_ty is frequently something like
466 -- `Item [Int]`, but we prefer `Int`
467 , norm_elem_ty `eqType` e_ty ->
468 -- We have to ensure that the element types are exactly the same.
469 -- Otherwise, one may give an instance IsList [Int] (more specific than
470 -- the default IsList [a]) with a different implementation for `toList'
471 translatePat fam_insts (ListPat lpats e_ty Nothing)
472 -- See Note [Guards and Approximation]
473 | otherwise -> mkCanFailPmPat pat_ty
474
475 ConPatOut { pat_con = L _ con
476 , pat_arg_tys = arg_tys
477 , pat_tvs = ex_tvs
478 , pat_dicts = dicts
479 , pat_args = ps } -> do
480 groups <- allCompleteMatches con arg_tys
481 case groups of
482 [] -> mkCanFailPmPat (conLikeResTy con arg_tys)
483 _ -> do
484 args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
485 return [PmCon { pm_con_con = con
486 , pm_con_arg_tys = arg_tys
487 , pm_con_tvs = ex_tvs
488 , pm_con_dicts = dicts
489 , pm_con_args = args }]
490
491 NPat (L _ ol) mb_neg _eq ty -> translateNPat fam_insts ol mb_neg ty
492
493 LitPat lit
494 -- If it is a string then convert it to a list of characters
495 | HsString src s <- lit ->
496 foldr (mkListPatVec charTy) [nilPattern charTy] <$>
497 translatePatVec fam_insts (map (LitPat . HsChar src) (unpackFS s))
498 | otherwise -> return [mkLitPattern lit]
499
500 PArrPat ps ty -> do
501 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
502 let fake_con = RealDataCon (parrFakeCon (length ps))
503 return [vanillaConPattern fake_con [ty] (concat tidy_ps)]
504
505 TuplePat ps boxity tys -> do
506 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
507 let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
508 return [vanillaConPattern tuple_con tys (concat tidy_ps)]
509
510 SumPat p alt arity ty -> do
511 tidy_p <- translatePat fam_insts (unLoc p)
512 let sum_con = RealDataCon (sumDataCon alt arity)
513 return [vanillaConPattern sum_con ty tidy_p]
514
515 -- --------------------------------------------------------------------------
516 -- Not supposed to happen
517 ConPatIn {} -> panic "Check.translatePat: ConPatIn"
518 SplicePat {} -> panic "Check.translatePat: SplicePat"
519 SigPatIn {} -> panic "Check.translatePat: SigPatIn"
520
521 -- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
522 translateNPat :: FamInstEnvs
523 -> HsOverLit Id -> Maybe (SyntaxExpr Id) -> Type -> DsM PatVec
524 translateNPat fam_insts (OverLit val False _ ty) mb_neg outer_ty
525 | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
526 = translatePat fam_insts (LitPat (HsString src s))
527 | not type_change, isIntTy ty, HsIntegral src i <- val
528 = translatePat fam_insts (mk_num_lit HsInt src i)
529 | not type_change, isWordTy ty, HsIntegral src i <- val
530 = translatePat fam_insts (mk_num_lit HsWordPrim src i)
531 where
532 type_change = not (outer_ty `eqType` ty)
533 mk_num_lit c src i = LitPat $ case mb_neg of
534 Nothing -> c src i
535 Just _ -> c src (-i)
536 translateNPat _ ol mb_neg _
537 = return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) ol }]
538
539 -- | Translate a list of patterns (Note: each pattern is translated
540 -- to a pattern vector but we do not concatenate the results).
541 translatePatVec :: FamInstEnvs -> [Pat Id] -> DsM [PatVec]
542 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
543
544 -- | Translate a constructor pattern
545 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
546 -> ConLike -> HsConPatDetails Id -> DsM PatVec
547 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
548 = concat <$> translatePatVec fam_insts (map unLoc ps)
549 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
550 = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
551 translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
552 -- Nothing matched. Make up some fresh term variables
553 | null fs = mkPmVars arg_tys
554 -- The data constructor was not defined using record syntax. For the
555 -- pattern to be in record syntax it should be empty (e.g. Just {}).
556 -- So just like the previous case.
557 | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
558 -- Some of the fields appear, in the original order (there may be holes).
559 -- Generate a simple constructor pattern and make up fresh variables for
560 -- the rest of the fields
561 | matched_lbls `subsetOf` orig_lbls
562 = ASSERT(length orig_lbls == length arg_tys)
563 let translateOne (lbl, ty) = case lookup lbl matched_pats of
564 Just p -> translatePat fam_insts p
565 Nothing -> mkPmVars [ty]
566 in concatMapM translateOne (zip orig_lbls arg_tys)
567 -- The fields that appear are not in the correct order. Make up fresh
568 -- variables for all fields and add guards after matching, to force the
569 -- evaluation in the correct order.
570 | otherwise = do
571 arg_var_pats <- mkPmVars arg_tys
572 translated_pats <- forM matched_pats $ \(x,pat) -> do
573 pvec <- translatePat fam_insts pat
574 return (x, pvec)
575
576 let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
577 guards = map (\(name,pvec) -> case lookup name zipped of
578 Just x -> PmGrd pvec (PmExprVar (idName x))
579 Nothing -> panic "translateConPatVec: lookup")
580 translated_pats
581
582 return (arg_var_pats ++ guards)
583 where
584 -- The actual argument types (instantiated)
585 arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
586
587 -- Some label information
588 orig_lbls = map flSelector $ conLikeFieldLabels c
589 matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
590 | L _ x <- fs]
591 matched_lbls = [ name | (name, _pat) <- matched_pats ]
592
593 subsetOf :: Eq a => [a] -> [a] -> Bool
594 subsetOf [] _ = True
595 subsetOf (_:_) [] = False
596 subsetOf (x:xs) (y:ys)
597 | x == y = subsetOf xs ys
598 | otherwise = subsetOf (x:xs) ys
599
600 -- Translate a single match
601 translateMatch :: FamInstEnvs -> LMatch Id (LHsExpr Id) -> DsM (PatVec,[PatVec])
602 translateMatch fam_insts (L _ (Match _ lpats _ grhss)) = do
603 pats' <- concat <$> translatePatVec fam_insts pats
604 guards' <- mapM (translateGuards fam_insts) guards
605 return (pats', guards')
606 where
607 extractGuards :: LGRHS Id (LHsExpr Id) -> [GuardStmt Id]
608 extractGuards (L _ (GRHS gs _)) = map unLoc gs
609
610 pats = map unLoc lpats
611 guards = map extractGuards (grhssGRHSs grhss)
612
613 -- -----------------------------------------------------------------------
614 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
615
616 -- | Translate a list of guard statements to a pattern vector
617 translateGuards :: FamInstEnvs -> [GuardStmt Id] -> DsM PatVec
618 translateGuards fam_insts guards = do
619 all_guards <- concat <$> mapM (translateGuard fam_insts) guards
620 return (replace_unhandled all_guards)
621 -- It should have been (return all_guards) but it is too expressive.
622 -- Since the term oracle does not handle all constraints we generate,
623 -- we (hackily) replace all constraints the oracle cannot handle with a
624 -- single one (we need to know if there is a possibility of falure).
625 -- See Note [Guards and Approximation] for all guard-related approximations
626 -- we implement.
627 where
628 replace_unhandled :: PatVec -> PatVec
629 replace_unhandled gv
630 | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
631 | otherwise = gv
632
633 any_unhandled :: PatVec -> Bool
634 any_unhandled gv = any (not . shouldKeep) gv
635
636 shouldKeep :: Pattern -> Bool
637 shouldKeep p
638 | PmVar {} <- p = True
639 | PmCon {} <- p = singleConstructor (pm_con_con p)
640 && all shouldKeep (pm_con_args p)
641 shouldKeep (PmGrd pv e)
642 | all shouldKeep pv = True
643 | isNotPmExprOther e = True -- expensive but we want it
644 shouldKeep _other_pat = False -- let the rest..
645
646 -- | Check whether a pattern can fail to match
647 cantFailPattern :: Pattern -> Bool
648 cantFailPattern p
649 | PmVar {} <- p = True
650 | PmCon {} <- p = singleConstructor (pm_con_con p)
651 && all cantFailPattern (pm_con_args p)
652 cantFailPattern (PmGrd pv _e)
653 = all cantFailPattern pv
654 cantFailPattern _ = False
655
656 -- | Translate a guard statement to Pattern
657 translateGuard :: FamInstEnvs -> GuardStmt Id -> DsM PatVec
658 translateGuard fam_insts guard = case guard of
659 BodyStmt e _ _ _ -> translateBoolGuard e
660 LetStmt binds -> translateLet (unLoc binds)
661 BindStmt p e _ _ _ -> translateBind fam_insts p e
662 LastStmt {} -> panic "translateGuard LastStmt"
663 ParStmt {} -> panic "translateGuard ParStmt"
664 TransStmt {} -> panic "translateGuard TransStmt"
665 RecStmt {} -> panic "translateGuard RecStmt"
666 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
667
668 -- | Translate let-bindings
669 translateLet :: HsLocalBinds Id -> DsM PatVec
670 translateLet _binds = return []
671
672 -- | Translate a pattern guard
673 translateBind :: FamInstEnvs -> LPat Id -> LHsExpr Id -> DsM PatVec
674 translateBind fam_insts (L _ p) e = do
675 ps <- translatePat fam_insts p
676 return [mkGuard ps (unLoc e)]
677
678 -- | Translate a boolean guard
679 translateBoolGuard :: LHsExpr Id -> DsM PatVec
680 translateBoolGuard e
681 | isJust (isTrueLHsExpr e) = return []
682 -- The formal thing to do would be to generate (True <- True)
683 -- but it is trivial to solve so instead we give back an empty
684 -- PatVec for efficiency
685 | otherwise = return [mkGuard [truePattern] (unLoc e)]
686
687 {- Note [Guards and Approximation]
688 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
689 Even if the algorithm is really expressive, the term oracle we use is not.
690 Hence, several features are not translated *properly* but we approximate.
691 The list includes:
692
693 1. View Patterns
694 ----------------
695 A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
696 oracle does not handle function applications so we know that the generated
697 constraints will not be handled at the end. Hence, we distinguish between two
698 cases:
699 a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
700 thing*.
701 b) Pattern @p@ can fail. This means that when checking the guard, we will
702 generate several cases, with no useful information. E.g.:
703
704 h (f -> [a,b]) = ...
705 h x ([a,b] <- f x) = ...
706
707 uncovered set = { [x |> { False ~ (f x ~ []) }]
708 , [x |> { False ~ (f x ~ (t1:[])) }]
709 , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
710
711 So we have two problems:
712 1) Since we do not print the constraints in the general case (they may
713 be too many), the warning will look like this:
714
715 Pattern match(es) are non-exhaustive
716 In an equation for `h':
717 Patterns not matched:
718 _
719 _
720 _
721 Which is not short and not more useful than a single underscore.
722 2) The size of the uncovered set increases a lot, without gaining more
723 expressivity in our warnings.
724
725 Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
726 @fake_pat@: @True <- _@. That is, we record that there is a possibility
727 of failure but we minimize it to a True/False. This generates a single
728 warning and much smaller uncovered sets.
729
730 2. Overloaded Lists
731 -------------------
732 An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
733 problem is exactly like above, as its solution. For future reference, the code
734 below is the *right thing to do*:
735
736 ListPat lpats elem_ty (Just (pat_ty, to_list))
737 otherwise -> do
738 (xp, xe) <- mkPmId2Forms pat_ty
739 ps <- translatePatVec (map unLoc lpats)
740 let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
741 g = mkGuard pats (HsApp (noLoc to_list) xe)
742 return [xp,g]
743
744 3. Overloaded Literals
745 ----------------------
746 The case with literals is a bit different. a literal @l@ should be translated
747 to @x (True <- x == from l)@. Since we want to have better warnings for
748 overloaded literals as it is a very common feature, we treat them differently.
749 They are mainly covered in Note [Undecidable Equality on Overloaded Literals]
750 in PmExpr.
751
752 4. N+K Patterns & Pattern Synonyms
753 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
754 An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
755 Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
756 and has two possible outcomes. Hence, there is no benefit in using a dummy and
757 we implement the proper thing. Pattern synonyms are simply not implemented yet.
758 Hence, to be conservative, we generate a dummy pattern, assuming that the
759 pattern can fail.
760
761 5. Actual Guards
762 ----------------
763 During translation, boolean guards and pattern guards are translated properly.
764 Let bindings though are omitted by function @translateLet@. Since they are lazy
765 bindings, we do not actually want to generate a (strict) equality (like we do
766 in the pattern bind case). Hence, we safely drop them.
767
768 Additionally, top-level guard translation (performed by @translateGuards@)
769 replaces guards that cannot be reasoned about (like the ones we described in
770 1-4) with a single @fake_pat@ to record the possibility of failure to match.
771
772 Note [Translate CoPats]
773 ~~~~~~~~~~~~~~~~~~~~~~~
774 The pattern match checker did not know how to handle coerced patterns `CoPat`
775 efficiently, which gave rise to #11276. The original approach translated
776 `CoPat`s:
777
778 pat |> co ===> x (pat <- (e |> co))
779
780 Instead, we now check whether the coercion is a hole or if it is just refl, in
781 which case we can drop it. Unfortunately, data families generate useful
782 coercions so guards are still generated in these cases and checking data
783 families is not really efficient.
784
785 %************************************************************************
786 %* *
787 Utilities for Pattern Match Checking
788 %* *
789 %************************************************************************
790 -}
791
792 -- ----------------------------------------------------------------------------
793 -- * Basic utilities
794
795 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
796 -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
797 pmPatType :: PmPat p -> Type
798 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
799 = conLikeResTy con tys
800 pmPatType (PmVar { pm_var_id = x }) = idType x
801 pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
802 pmPatType (PmNLit { pm_lit_id = x }) = idType x
803 pmPatType (PmGrd { pm_grd_pv = pv })
804 = ASSERT(patVecArity pv == 1) (pmPatType p)
805 where Just p = find ((==1) . patternArity) pv
806
807 -- | Generate a value abstraction for a given constructor (generate
808 -- fresh variables of the appropriate type for arguments)
809 mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
810 -- * x :: T tys, where T is an algebraic data type
811 -- NB: in the case of a data familiy, T is the *representation* TyCon
812 -- e.g. data instance T (a,b) = T1 a b
813 -- leads to
814 -- data TPair a b = T1 a b -- The "representation" type
815 -- It is TPair, not T, that is given to mkOneConFull
816 --
817 -- * 'con' K is a constructor of data type T
818 --
819 -- After instantiating the universal tyvars of K we get
820 -- K tys :: forall bs. Q => s1 .. sn -> T tys
821 --
822 -- Results: ValAbs: K (y1::s1) .. (yn::sn)
823 -- ComplexEq: x ~ K y1..yn
824 -- [EvVar]: Q
825 mkOneConFull x con = do
826 let -- res_ty == TyConApp (ConLikeTyCon cabs_con) cabs_arg_tys
827 res_ty = idType x
828 (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, _)
829 = conLikeFullSig con
830 tc_args = case splitTyConApp_maybe res_ty of
831 Just (_, tys) -> tys
832 Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty)
833 subst1 = zipTvSubst univ_tvs tc_args
834
835 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
836
837 -- Fresh term variables (VAs) as arguments to the constructor
838 arguments <- mapM mkPmVar (substTys subst arg_tys)
839 -- All constraints bound by the constructor (alpha-renamed)
840 let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
841 evvars <- mapM (nameType "pm") theta_cs
842 let con_abs = PmCon { pm_con_con = con
843 , pm_con_arg_tys = tc_args
844 , pm_con_tvs = ex_tvs'
845 , pm_con_dicts = evvars
846 , pm_con_args = arguments }
847 return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
848
849 -- ----------------------------------------------------------------------------
850 -- * More smart constructors and fresh variable generation
851
852 -- | Create a guard pattern
853 mkGuard :: PatVec -> HsExpr Id -> Pattern
854 mkGuard pv e
855 | all cantFailPattern pv = PmGrd pv expr
856 | PmExprOther {} <- expr = fake_pat
857 | otherwise = PmGrd pv expr
858 where
859 expr = hsExprToPmExpr e
860
861 -- | Create a term equality of the form: `(False ~ (x ~ lit))`
862 mkNegEq :: Id -> PmLit -> ComplexEq
863 mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
864 {-# INLINE mkNegEq #-}
865
866 -- | Create a term equality of the form: `(x ~ lit)`
867 mkPosEq :: Id -> PmLit -> ComplexEq
868 mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
869 {-# INLINE mkPosEq #-}
870
871 -- | Generate a variable pattern of a given type
872 mkPmVar :: Type -> DsM (PmPat p)
873 mkPmVar ty = PmVar <$> mkPmId ty
874 {-# INLINE mkPmVar #-}
875
876 -- | Generate many variable patterns, given a list of types
877 mkPmVars :: [Type] -> DsM PatVec
878 mkPmVars tys = mapM mkPmVar tys
879 {-# INLINE mkPmVars #-}
880
881 -- | Generate a fresh `Id` of a given type
882 mkPmId :: Type -> DsM Id
883 mkPmId ty = getUniqueM >>= \unique ->
884 let occname = mkVarOccFS (fsLit (show unique))
885 name = mkInternalName unique occname noSrcSpan
886 in return (mkLocalId name ty)
887
888 -- | Generate a fresh term variable of a given and return it in two forms:
889 -- * A variable pattern
890 -- * A variable expression
891 mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr Id)
892 mkPmId2Forms ty = do
893 x <- mkPmId ty
894 return (PmVar x, noLoc (HsVar (noLoc x)))
895
896 -- ----------------------------------------------------------------------------
897 -- * Converting between Value Abstractions, Patterns and PmExpr
898
899 -- | Convert a value abstraction an expression
900 vaToPmExpr :: ValAbs -> PmExpr
901 vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
902 = PmExprCon c (map vaToPmExpr ps)
903 vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
904 vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
905 vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
906
907 -- | Convert a pattern vector to a list of value abstractions by dropping the
908 -- guards (See Note [Translating As Patterns])
909 coercePatVec :: PatVec -> [ValAbs]
910 coercePatVec pv = concatMap coercePmPat pv
911
912 -- | Convert a pattern to a list of value abstractions (will be either an empty
913 -- list if the pattern is a guard pattern, or a singleton list in all other
914 -- cases) by dropping the guards (See Note [Translating As Patterns])
915 coercePmPat :: Pattern -> [ValAbs]
916 coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
917 coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
918 coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
919 , pm_con_tvs = tvs, pm_con_dicts = dicts
920 , pm_con_args = args })
921 = [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
922 , pm_con_tvs = tvs, pm_con_dicts = dicts
923 , pm_con_args = coercePatVec args }]
924 coercePmPat (PmGrd {}) = [] -- drop the guards
925
926 -- | Check whether a data constructor is the only way to construct
927 -- a data type.
928 singleConstructor :: ConLike -> Bool
929 singleConstructor (RealDataCon dc) =
930 case tyConDataCons (dataConTyCon dc) of
931 [_] -> True
932 _ -> False
933 singleConstructor _ = False
934
935 -- | For a given conlike, finds all the sets of patterns which could
936 -- be relevant to that conlike by consulting the result type.
937 --
938 -- These come from two places.
939 -- 1. From data constructors defined with the result type constructor.
940 -- 2. From `COMPLETE` pragmas which have the same type as the result
941 -- type constructor.
942 allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
943 allCompleteMatches cl tys = do
944 let fam = case cl of
945 RealDataCon dc ->
946 [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
947 PatSynCon _ -> []
948
949
950 from_pragma <- map ((FromComplete,) . completeMatch) <$>
951 case splitTyConApp_maybe (conLikeResTy cl tys) of
952 Just (tc, _) -> dsGetCompleteMatches tc
953 Nothing -> return []
954
955 let final_groups = fam ++ from_pragma
956 tracePmD "allCompleteMatches" (ppr final_groups)
957 return final_groups
958
959 -- -----------------------------------------------------------------------
960 -- * Types and constraints
961
962 newEvVar :: Name -> Type -> EvVar
963 newEvVar name ty = mkLocalId name (toTcType ty)
964
965 nameType :: String -> Type -> DsM EvVar
966 nameType name ty = do
967 unique <- getUniqueM
968 let occname = mkVarOccFS (fsLit (name++"_"++show unique))
969 idname = mkInternalName unique occname noSrcSpan
970 return (newEvVar idname ty)
971
972 {-
973 %************************************************************************
974 %* *
975 The type oracle
976 %* *
977 %************************************************************************
978 -}
979
980 -- | Check whether a set of type constraints is satisfiable.
981 tyOracle :: Bag EvVar -> PmM Bool
982 tyOracle evs
983 = liftD $
984 do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
985 ; case res of
986 Just sat -> return sat
987 Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
988
989 {-
990 %************************************************************************
991 %* *
992 Sanity Checks
993 %* *
994 %************************************************************************
995 -}
996
997 -- | The arity of a pattern/pattern vector is the
998 -- number of top-level patterns that are not guards
999 type PmArity = Int
1000
1001 -- | Compute the arity of a pattern vector
1002 patVecArity :: PatVec -> PmArity
1003 patVecArity = sum . map patternArity
1004
1005 -- | Compute the arity of a pattern
1006 patternArity :: Pattern -> PmArity
1007 patternArity (PmGrd {}) = 0
1008 patternArity _other_pat = 1
1009
1010 {-
1011 %************************************************************************
1012 %* *
1013 Heart of the algorithm: Function pmcheck
1014 %* *
1015 %************************************************************************
1016
1017 Main functions are:
1018
1019 * mkInitialUncovered :: [Id] -> PmM Uncovered
1020
1021 Generates the initial uncovered set. Term and type constraints in scope
1022 are checked, if they are inconsistent, the set is empty, otherwise, the
1023 set contains only a vector of variables with the constraints in scope.
1024
1025 * pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1026
1027 Checks redundancy, coverage and inaccessibility, using auxilary functions
1028 `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
1029 common in all three checks (see paper) and calls `pmcheckGuards` when the
1030 whole clause is checked, or `pmcheckHd` when the pattern vector does not
1031 start with a guard.
1032
1033 * pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1034
1035 Processes the guards.
1036
1037 * pmcheckHd :: Pattern -> PatVec -> [PatVec]
1038 -> ValAbs -> ValVec -> PmM PartialResult
1039
1040 Worker: This function implements functions `covered`, `uncovered` and
1041 `divergent` from the paper at once. Slightly different from the paper because
1042 it does not even produce the covered and uncovered sets. Since we only care
1043 about whether a clause covers SOMETHING or if it may forces ANY argument, we
1044 only store a boolean in both cases, for efficiency.
1045 -}
1046
1047 -- | Lift a pattern matching action from a single value vector abstration to a
1048 -- value set abstraction, but calling it on every vector and the combining the
1049 -- results.
1050 runMany :: (ValVec -> PmM PartialResult) -> (Uncovered -> PmM PartialResult)
1051 runMany _ [] = return mempty
1052 runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms
1053 {-# INLINE runMany #-}
1054
1055 -- | Generate the initial uncovered set. It initializes the
1056 -- delta with all term and type constraints in scope.
1057 mkInitialUncovered :: [Id] -> PmM Uncovered
1058 mkInitialUncovered vars = do
1059 ty_cs <- liftD getDictsDs
1060 tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
1061 sat_ty <- tyOracle ty_cs
1062 return $ case (sat_ty, tmOracle initialTmState tm_cs) of
1063 (True, Just tm_state) -> [ValVec patterns (MkDelta ty_cs tm_state)]
1064 -- If any of the term/type constraints are non
1065 -- satisfiable, the initial uncovered set is empty
1066 _non_satisfiable -> []
1067 where
1068 patterns = map PmVar vars
1069
1070 -- | Increase the counter for elapsed algorithm iterations, check that the
1071 -- limit is not exceeded and call `pmcheck`
1072 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1073 pmcheckI ps guards vva = do
1074 n <- liftD incrCheckPmIterDs
1075 tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
1076 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1077 $$ pprValVecDebug vva)
1078 res <- pmcheck ps guards vva
1079 tracePm "pmCheckResult:" (ppr res)
1080 return res
1081 {-# INLINE pmcheckI #-}
1082
1083 -- | Increase the counter for elapsed algorithm iterations, check that the
1084 -- limit is not exceeded and call `pmcheckGuards`
1085 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
1086 pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
1087 {-# INLINE pmcheckGuardsI #-}
1088
1089 -- | Increase the counter for elapsed algorithm iterations, check that the
1090 -- limit is not exceeded and call `pmcheckHd`
1091 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1092 -> PmM PartialResult
1093 pmcheckHdI p ps guards va vva = do
1094 n <- liftD incrCheckPmIterDs
1095 tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
1096 $$ pprPatVec ps
1097 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1098 $$ pprPmPatDebug va
1099 $$ pprValVecDebug vva)
1100
1101 res <- pmcheckHd p ps guards va vva
1102 tracePm "pmCheckHdI: res" (ppr res)
1103 return res
1104 {-# INLINE pmcheckHdI #-}
1105
1106 -- | Matching function: Check simultaneously a clause (takes separately the
1107 -- patterns and the list of guards) for exhaustiveness, redundancy and
1108 -- inaccessibility.
1109 pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1110 pmcheck [] guards vva@(ValVec [] _)
1111 | null guards = return $ mempty { presultCovered = Covered }
1112 | otherwise = pmcheckGuardsI guards vva
1113
1114 -- Guard
1115 pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta)
1116 -- short-circuit if the guard pattern is useless.
1117 -- we just have two possible outcomes: fail here or match and recurse
1118 -- none of the two contains any useful information about the failure
1119 -- though. So just have these two cases but do not do all the boilerplate
1120 | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
1121 | otherwise = do
1122 y <- liftD $ mkPmId (pmPatType p)
1123 let tm_state = extendSubst y e (delta_tm_cs delta)
1124 delta' = delta { delta_tm_cs = tm_state }
1125 utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
1126
1127 pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
1128 pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
1129
1130 pmcheck (p:ps) guards (ValVec (va:vva) delta)
1131 = pmcheckHdI p ps guards va (ValVec vva delta)
1132
1133 -- | Check the list of guards
1134 pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1135 pmcheckGuards [] vva = return (usimple [vva])
1136 pmcheckGuards (gv:gvs) vva = do
1137 (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva
1138 (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
1139 return $ PartialResult (prov1 `mappend` prov2)
1140 (cs `mappend` css)
1141 vsas
1142 (ds `mappend` dss)
1143
1144 -- | Worker function: Implements all cases described in the paper for all three
1145 -- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
1146 -- cases which are handled by `pmcheck`
1147 pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1148 -> PmM PartialResult
1149
1150 -- Var
1151 pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
1152 | Just tm_state <- solveOneEq (delta_tm_cs delta)
1153 (PmExprVar (idName x), vaToPmExpr va)
1154 = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
1155 | otherwise = return mempty
1156
1157 -- ConCon
1158 pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
1159 (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
1160 | c1 /= c2 =
1161 return (usimple [ValVec (va:vva) delta])
1162 | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
1163 <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)
1164
1165 -- LitLit
1166 pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
1167 case eqPmLit l1 l2 of
1168 True -> ucon va <$> pmcheckI ps guards vva
1169 False -> return $ ucon va (usimple [vva])
1170
1171 -- ConVar
1172 pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
1173 ps guards
1174 (PmVar x) (ValVec vva delta) = do
1175 (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
1176
1177 cons_cs <- mapM (liftD . mkOneConFull x) complete_match
1178
1179 inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
1180 let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
1181 sat_ty <- if isEmptyBag ty_cs then return True
1182 else tyOracle ty_state
1183 return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
1184 (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
1185 _ty_or_tm_failed -> []
1186
1187 set_provenance prov .
1188 force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1189 runMany (pmcheckI (p:ps) guards) inst_vsa
1190
1191 -- LitVar
1192 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
1193 = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1194 mkUnion non_matched <$>
1195 case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
1196 Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
1197 ValVec vva (delta {delta_tm_cs = tm_state})
1198 Nothing -> return mempty
1199 where
1200 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1201 = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
1202 | otherwise = []
1203
1204 non_matched = usimple us
1205
1206 -- LitNLit
1207 pmcheckHd (p@(PmLit l)) ps guards
1208 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
1209 | all (not . eqPmLit l) lits
1210 , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
1211 -- Both guards check the same so it would be sufficient to have only
1212 -- the second one. Nevertheless, it is much cheaper to check whether
1213 -- the literal is in the list so we check it first, to avoid calling
1214 -- the term oracle (`solveOneEq`) if possible
1215 = mkUnion non_matched <$>
1216 pmcheckHdI p ps guards (PmLit l)
1217 (ValVec vva (delta { delta_tm_cs = tm_state }))
1218 | otherwise = return non_matched
1219 where
1220 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1221 = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
1222 | otherwise = []
1223
1224 non_matched = usimple us
1225
1226 -- ----------------------------------------------------------------------------
1227 -- The following three can happen only in cases like #322 where constructors
1228 -- and overloaded literals appear in the same match. The general strategy is
1229 -- to replace the literal (positive/negative) by a variable and recurse. The
1230 -- fact that the variable is equal to the literal is recorded in `delta` so
1231 -- no information is lost
1232
1233 -- LitCon
1234 pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
1235 = do y <- liftD $ mkPmId (pmPatType va)
1236 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1237 delta' = delta { delta_tm_cs = tm_state }
1238 pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
1239
1240 -- ConLit
1241 pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
1242 = do y <- liftD $ mkPmId (pmPatType p)
1243 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1244 delta' = delta { delta_tm_cs = tm_state }
1245 pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
1246
1247 -- ConNLit
1248 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
1249 = pmcheckHdI p ps guards (PmVar x) vva
1250
1251 -- Impossible: handled by pmcheck
1252 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
1253
1254 -- ----------------------------------------------------------------------------
1255 -- * Utilities for main checking
1256
1257 updateVsa :: (ValSetAbs -> ValSetAbs) -> (PartialResult -> PartialResult)
1258 updateVsa f p@(PartialResult { presultUncovered = old })
1259 = p { presultUncovered = f old }
1260
1261
1262 -- | Initialise with default values for covering and divergent information.
1263 usimple :: ValSetAbs -> PartialResult
1264 usimple vsa = mempty { presultUncovered = vsa }
1265
1266 -- | Take the tail of all value vector abstractions in the uncovered set
1267 utail :: PartialResult -> PartialResult
1268 utail = updateVsa upd
1269 where upd vsa = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ]
1270
1271 -- | Prepend a value abstraction to all value vector abstractions in the
1272 -- uncovered set
1273 ucon :: ValAbs -> PartialResult -> PartialResult
1274 ucon va = updateVsa upd
1275 where
1276 upd vsa = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ]
1277
1278 -- | Given a data constructor of arity `a` and an uncovered set containing
1279 -- value vector abstractions of length `(a+n)`, pass the first `n` value
1280 -- abstractions to the constructor (Hence, the resulting value vector
1281 -- abstractions will have length `n+1`)
1282 kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
1283 -> PartialResult -> PartialResult
1284 kcon con arg_tys ex_tvs dicts
1285 = let n = conLikeArity con
1286 upd vsa =
1287 [ ValVec (va:vva) delta
1288 | ValVec vva' delta <- vsa
1289 , let (args, vva) = splitAt n vva'
1290 , let va = PmCon { pm_con_con = con
1291 , pm_con_arg_tys = arg_tys
1292 , pm_con_tvs = ex_tvs
1293 , pm_con_dicts = dicts
1294 , pm_con_args = args } ]
1295 in updateVsa upd
1296
1297 -- | Get the union of two covered, uncovered and divergent value set
1298 -- abstractions. Since the covered and divergent sets are represented by a
1299 -- boolean, union means computing the logical or (at least one of the two is
1300 -- non-empty).
1301
1302 mkUnion :: PartialResult -> PartialResult -> PartialResult
1303 mkUnion = mappend
1304
1305 -- | Add a value vector abstraction to a value set abstraction (uncovered).
1306 mkCons :: ValVec -> PartialResult -> PartialResult
1307 mkCons vva = updateVsa (vva:)
1308
1309 -- | Set the divergent set to not empty
1310 forces :: PartialResult -> PartialResult
1311 forces pres = pres { presultDivergent = Diverged }
1312
1313 -- | Set the divergent set to non-empty if the flag is `True`
1314 force_if :: Bool -> PartialResult -> PartialResult
1315 force_if True pres = forces pres
1316 force_if False pres = pres
1317
1318 set_provenance :: Provenance -> PartialResult -> PartialResult
1319 set_provenance prov pr = pr { presultProvenence = prov }
1320
1321 -- ----------------------------------------------------------------------------
1322 -- * Propagation of term constraints inwards when checking nested matches
1323
1324 {- Note [Type and Term Equality Propagation]
1325 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1326 When checking a match it would be great to have all type and term information
1327 available so we can get more precise results. For this reason we have functions
1328 `addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
1329 term constraints (respectively) as we go deeper.
1330
1331 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1332 in HsPat.hs. This handles bug #4139 ( see example
1333 https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
1334 where this is needed.
1335
1336 For term equalities we do less, we just generate equalities for HsCase. For
1337 example we accurately give 2 redundancy warnings for the marked cases:
1338
1339 f :: [a] -> Bool
1340 f x = case x of
1341
1342 [] -> case x of -- brings (x ~ []) in scope
1343 [] -> True
1344 (_:_) -> False -- can't happen
1345
1346 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1347 (_:_) -> True
1348 [] -> False -- can't happen
1349
1350 Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
1351 these constraints.
1352 -}
1353
1354 -- | Generate equalities when checking a case expression:
1355 -- case x of { p1 -> e1; ... pn -> en }
1356 -- When we go deeper to check e.g. e1 we record two equalities:
1357 -- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
1358 -- and (x ~ p1).
1359 genCaseTmCs2 :: Maybe (LHsExpr Id) -- Scrutinee
1360 -> [Pat Id] -- LHS (should have length 1)
1361 -> [Id] -- MatchVars (should have length 1)
1362 -> DsM (Bag SimpleEq)
1363 genCaseTmCs2 Nothing _ _ = return emptyBag
1364 genCaseTmCs2 (Just scr) [p] [var] = do
1365 fam_insts <- dsGetFamInstEnvs
1366 [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
1367 let scr_e = lhsExprToPmExpr scr
1368 return $ listToBag [(var, e), (var, scr_e)]
1369 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
1370
1371 -- | Generate a simple equality when checking a case expression:
1372 -- case x of { matches }
1373 -- When checking matches we record that (x ~ y) where y is the initial
1374 -- uncovered. All matches will have to satisfy this equality.
1375 genCaseTmCs1 :: Maybe (LHsExpr Id) -> [Id] -> Bag SimpleEq
1376 genCaseTmCs1 Nothing _ = emptyBag
1377 genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
1378 genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
1379
1380 {- Note [Literals in PmPat]
1381 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1382 Instead of translating a literal to a variable accompanied with a guard, we
1383 treat them like constructor patterns. The following example from
1384 "./libraries/base/GHC/IO/Encoding.hs" shows why:
1385
1386 mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
1387 mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
1388 "UTF8" -> return $ UTF8.mkUTF8 cfm
1389 "UTF16" -> return $ UTF16.mkUTF16 cfm
1390 "UTF16LE" -> return $ UTF16.mkUTF16le cfm
1391 ...
1392
1393 Each clause gets translated to a list of variables with an equal number of
1394 guards. For every guard we generate two cases (equals True/equals False) which
1395 means that we generate 2^n cases to feed the oracle with, where n is the sum of
1396 the length of all strings that appear in the patterns. For this particular
1397 example this means over 2^40 cases. Instead, by representing them like with
1398 constructor we get the following:
1399 1. We exploit the common prefix with our representation of VSAs
1400 2. We prune immediately non-reachable cases
1401 (e.g. False == (x == "U"), True == (x == "U"))
1402
1403 Note [Translating As Patterns]
1404 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1405 Instead of translating x@p as: x (p <- x)
1406 we instead translate it as: p (x <- coercePattern p)
1407 for performance reasons. For example:
1408
1409 f x@True = 1
1410 f y@False = 2
1411
1412 Gives the following with the first translation:
1413
1414 x |> {x == False, x == y, y == True}
1415
1416 If we use the second translation we get an empty set, independently of the
1417 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
1418 used as an expression. That's why we call `coercePatVec' to drop the guard and
1419 `vaToPmExpr' to transform the value abstraction to an expression in the
1420 guard pattern (value abstractions are a subset of expressions). We keep the
1421 guards in the first pattern `p' though.
1422
1423
1424 %************************************************************************
1425 %* *
1426 Pretty printing of exhaustiveness/redundancy check warnings
1427 %* *
1428 %************************************************************************
1429 -}
1430
1431 -- | Check whether any part of pattern match checking is enabled (does not
1432 -- matter whether it is the redundancy check or the exhaustiveness check).
1433 isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
1434 isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
1435 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
1436
1437 instance Outputable ValVec where
1438 ppr (ValVec vva delta)
1439 = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
1440 vector = substInValAbs subst vva
1441 in ppr_uncovered (vector, residual_eqs)
1442
1443 -- | Apply a term substitution to a value vector abstraction. All VAs are
1444 -- transformed to PmExpr (used only before pretty printing).
1445 substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
1446 substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
1447
1448 -- | Wrap up the term oracle's state once solving is complete. Drop any
1449 -- information about unhandled constraints (involving HsExprs) and flatten
1450 -- (height 1) the substitution.
1451 wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
1452 wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
1453
1454 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
1455 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
1456 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
1457 = when (flag_i || flag_u) $ do
1458 let exists_r = flag_i && notNull redundant && onlyBuiltin
1459 exists_i = flag_i && notNull inaccessible && onlyBuiltin
1460 exists_u = flag_u && notNull uncovered
1461 when exists_r $ forM_ redundant $ \(L l q) -> do
1462 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1463 (pprEqn q "is redundant"))
1464 when exists_i $ forM_ inaccessible $ \(L l q) -> do
1465 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1466 (pprEqn q "has inaccessible right hand side"))
1467 when exists_u $
1468 putSrcSpanDs loc (warnDs flag_u_reason (pprEqns uncovered))
1469 where
1470 PmResult
1471 { pmresultProvenance = prov
1472 , pmresultRedundant = redundant
1473 , pmresultUncovered = uncovered
1474 , pmresultInaccessible = inaccessible } = pm_result
1475
1476 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1477 flag_u = exhaustive dflags kind
1478 flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
1479
1480 onlyBuiltin = prov == FromBuiltin
1481
1482 maxPatterns = maxUncoveredPatterns dflags
1483
1484 -- Print a single clause (for redundant/with-inaccessible-rhs)
1485 pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
1486
1487 -- Print several clauses (for uncovered clauses)
1488 pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
1489 case qs of -- See #11245
1490 [ValVec [] _]
1491 -> text "Guards do not cover entire pattern space"
1492 _missing -> let us = map ppr qs
1493 in hang (text "Patterns not matched:") 4
1494 (vcat (take maxPatterns us)
1495 $$ dots maxPatterns us)
1496
1497 -- | Issue a warning when the predefined number of iterations is exceeded
1498 -- for the pattern match checker
1499 warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
1500 warnPmIters dflags (DsMatchContext kind loc)
1501 = when (flag_i || flag_u) $ do
1502 iters <- maxPmCheckIterations <$> getDynFlags
1503 putSrcSpanDs loc (warnDs NoReason (msg iters))
1504 where
1505 ctxt = pprMatchContext kind
1506 msg is = fsep [ text "Pattern match checker exceeded"
1507 , parens (ppr is), text "iterations in", ctxt <> dot
1508 , text "(Use -fmax-pmcheck-iterations=n"
1509 , text "to set the maximun number of iterations to n)" ]
1510
1511 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1512 flag_u = exhaustive dflags kind
1513
1514 dots :: Int -> [a] -> SDoc
1515 dots maxPatterns qs
1516 | qs `lengthExceeds` maxPatterns = text "..."
1517 | otherwise = empty
1518
1519 -- | Check whether the exhaustiveness checker should run (exhaustiveness only)
1520 exhaustive :: DynFlags -> HsMatchContext id -> Bool
1521 exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
1522
1523 -- | Denotes whether an exhaustiveness check is supported, and if so,
1524 -- via which 'WarningFlag' it's controlled.
1525 -- Returns 'Nothing' if check is not supported.
1526 exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
1527 exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
1528 exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
1529 exhaustiveWarningFlag IfAlt = Nothing
1530 exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
1531 exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
1532 exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
1533 exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
1534 exhaustiveWarningFlag ThPatSplice = Nothing
1535 exhaustiveWarningFlag PatSyn = Nothing
1536 exhaustiveWarningFlag ThPatQuote = Nothing
1537 exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns
1538 -- in list comprehensions, pattern guards
1539 -- etc. They are often *supposed* to be
1540 -- incomplete
1541
1542 -- True <==> singular
1543 pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
1544 pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
1545 = vcat [text txt <+> msg,
1546 sep [ text "In" <+> ppr_match <> char ':'
1547 , nest 4 (rest_of_msg_fun pref)]]
1548 where
1549 txt | singular = "Pattern match"
1550 | otherwise = "Pattern match(es)"
1551
1552 (ppr_match, pref)
1553 = case kind of
1554 FunRhs (L _ fun) _ -> (pprMatchContext kind,
1555 \ pp -> ppr fun <+> pp)
1556 _ -> (pprMatchContext kind, \ pp -> pp)
1557
1558 ppr_pats :: HsMatchContext Name -> [Pat Id] -> SDoc
1559 ppr_pats kind pats
1560 = sep [sep (map ppr pats), matchSeparator kind, text "..."]
1561
1562 ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat Id] -> SDoc
1563 ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
1564
1565 ppr_constraint :: (SDoc,[PmLit]) -> SDoc
1566 ppr_constraint (var, lits) = var <+> text "is not one of"
1567 <+> braces (pprWithCommas ppr lits)
1568
1569 ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
1570 ppr_uncovered (expr_vec, complex)
1571 | null cs = fsep vec -- there are no literal constraints
1572 | otherwise = hang (fsep vec) 4 $
1573 text "where" <+> vcat (map ppr_constraint cs)
1574 where
1575 sdoc_vec = mapM pprPmExprWithParens expr_vec
1576 (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
1577
1578 {- Note [Representation of Term Equalities]
1579 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1580 In the paper, term constraints always take the form (x ~ e). Of course, a more
1581 general constraint of the form (e1 ~ e1) can always be transformed to an
1582 equivalent set of the former constraints, by introducing a fresh, intermediate
1583 variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
1584 to #11160 (incredibly bad performance for literal pattern matching). Two are
1585 the main sources of this problem (the actual problem is how these two interact
1586 with each other):
1587
1588 1. Pattern matching on literals generates twice as many constraints as needed.
1589 Consider the following (tests/ghci/should_run/ghcirun004):
1590
1591 foo :: Int -> Int
1592 foo 1 = 0
1593 ...
1594 foo 5000 = 4999
1595
1596 The covered and uncovered set *should* look like:
1597 U0 = { x |> {} }
1598
1599 C1 = { 1 |> { x ~ 1 } }
1600 U1 = { x |> { False ~ (x ~ 1) } }
1601 ...
1602 C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
1603 U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
1604 ...
1605
1606 If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
1607 we get twice as many constraints. Also note that half of them are just the
1608 substitution [x |-> False].
1609
1610 2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
1611 (x ~ e) as substitutions [x |-> e]. More specifically, function
1612 `extendSubstAndSolve` applies such substitutions in the residual constraints
1613 and partitions them in the affected and non-affected ones, which are the new
1614 worklist. Essentially, this gives quadradic behaviour on the number of the
1615 residual constraints. (This would not be the case if the term oracle used
1616 mutable variables but, since we use it to handle disjunctions on value set
1617 abstractions (`Union` case), we chose a pure, incremental interface).
1618
1619 Now the problem becomes apparent (e.g. for clause 300):
1620 * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
1621 constraints that we know that will not reduce (stay in the worklist).
1622 * To check for consistency, we apply the substituting constraints ONE BY ONE
1623 (since `tmOracle` is called incrementally, it does not have all of them
1624 available at once). Hence, we go through the (non-progressing) constraints
1625 over and over, achieving over-quadradic behaviour.
1626
1627 If instead we allow constraints of the form (e ~ e),
1628 * All uncovered sets Ui contain no substituting constraints and i
1629 non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
1630 behaves linearly.
1631 * All covered sets Ci contain exactly (i-1) non-progressing constraints and
1632 a single substituting constraint. So the term oracle goes through the
1633 constraints only once.
1634
1635 The performance improvement becomes even more important when more arguments are
1636 involved.
1637 -}
1638
1639 -- Debugging Infrastructre
1640
1641 tracePm :: String -> SDoc -> PmM ()
1642 tracePm herald doc = liftD $ tracePmD herald doc
1643
1644
1645 tracePmD :: String -> SDoc -> DsM ()
1646 tracePmD herald doc = do
1647 dflags <- getDynFlags
1648 printer <- mkPrintUnqualifiedDs
1649 liftIO $ dumpIfSet_dyn_printer printer dflags
1650 Opt_D_dump_ec_trace (text herald $$ (nest 2 doc))
1651
1652
1653 pprPmPatDebug :: PmPat a -> SDoc
1654 pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
1655 = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
1656 pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
1657 pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
1658 pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
1659 pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv)
1660 <+> ppr ge
1661
1662 pprPatVec :: PatVec -> SDoc
1663 pprPatVec ps = hang (text "Pattern:") 2
1664 (brackets $ sep
1665 $ punctuate (comma <> char '\n') (map pprPmPatDebug ps))
1666
1667 pprValAbs :: [ValAbs] -> SDoc
1668 pprValAbs ps = hang (text "ValAbs:") 2
1669 (brackets $ sep
1670 $ punctuate (comma) (map pprPmPatDebug ps))
1671
1672 pprValVecDebug :: ValVec -> SDoc
1673 pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
1674 parens (pprValAbs vas)