Encode shape information in `PmOracle`
[ghc.git] / compiler / deSugar / Check.hs
1 {-
2 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
3
4 Pattern Matching Coverage Checking.
5 -}
6
7 {-# LANGUAGE CPP #-}
8 {-# LANGUAGE GADTs #-}
9 {-# LANGUAGE DataKinds #-}
10 {-# LANGUAGE KindSignatures #-}
11 {-# LANGUAGE TupleSections #-}
12 {-# LANGUAGE ViewPatterns #-}
13 {-# LANGUAGE MultiWayIf #-}
14 {-# LANGUAGE LambdaCase #-}
15
16 module Check (
17 -- Checking and printing
18 checkSingle, checkMatches, checkGuardMatches,
19 needToRunPmCheck, isMatchContextPmChecked,
20
21 -- See Note [Type and Term Equality Propagation]
22 addTyCsDs, addScrutTmCs, addPatTmCs
23 ) where
24
25 #include "HsVersions.h"
26
27 import GhcPrelude
28
29 import PmExpr
30 import PmOracle
31 import PmPpr
32 import BasicTypes (Origin, isGenerated)
33 import CoreSyn (CoreExpr, Expr(Var))
34 import CoreUtils (exprType)
35 import FastString (unpackFS)
36 import Unify( tcMatchTy )
37 import DynFlags
38 import HsSyn
39 import TcHsSyn
40 import Id
41 import ConLike
42 import Name
43 import FamInst
44 import TysWiredIn
45 import TyCon
46 import SrcLoc
47 import Util
48 import Outputable
49 import DataCon
50 import PatSyn
51 import HscTypes (CompleteMatch(..))
52 import BasicTypes (Boxity(..))
53 import Var (EvVar)
54
55 import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr)
56 import MatchLit (dsLit, dsOverLit)
57 import DsMonad
58 import Bag
59 import TyCoRep
60 import Type
61 import DsUtils (isTrueLHsExpr)
62 import Maybes (isJust, expectJust)
63 import qualified GHC.LanguageExtensions as LangExt
64
65 import Data.List (find)
66 import Control.Monad (forM, when, forM_)
67 import Control.Monad.Trans.Class (lift)
68 import Control.Monad.Trans.Maybe
69 import Coercion
70 import TcEvidence
71 import IOEnv
72 import qualified Data.Semigroup as Semi
73
74 {-
75 This module checks pattern matches for:
76 \begin{enumerate}
77 \item Equations that are redundant
78 \item Equations with inaccessible right-hand-side
79 \item Exhaustiveness
80 \end{enumerate}
81
82 The algorithm is based on the paper:
83
84 "GADTs Meet Their Match:
85 Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
86
87 http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf
88
89 %************************************************************************
90 %* *
91 Pattern Match Check Types
92 %* *
93 %************************************************************************
94 -}
95
96 data PmPat where
97 -- | For the arguments' meaning see 'HsPat.ConPatOut'.
98 PmCon :: { pm_con_con :: PmAltCon
99 , pm_con_arg_tys :: [Type]
100 , pm_con_tvs :: [TyVar]
101 , pm_con_args :: [PmPat] } -> PmPat
102
103 PmVar :: { pm_var_id :: Id } -> PmPat
104
105 PmGrd :: { pm_grd_pv :: PatVec -- ^ Always has 'patVecArity' 1.
106 , pm_grd_expr :: CoreExpr } -> PmPat
107 -- (PmGrd pat expr) matches expr against pat, binding the variables in pat
108
109 -- | A fake guard pattern (True <- _) used to represent cases we cannot handle.
110 PmFake :: PmPat
111
112 -- | Should not be user-facing.
113 instance Outputable PmPat where
114 ppr (PmCon alt _arg_tys _con_tvs con_args)
115 = cparen (notNull con_args) (hsep [ppr alt, hsep (map ppr con_args)])
116 ppr (PmVar vid) = ppr vid
117 ppr (PmGrd pv ge) = hsep (map ppr pv) <+> text "<-" <+> ppr ge
118 ppr PmFake = text "<PmFake>"
119
120 -- data T a where
121 -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
122 -- or MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
123
124 -- | Pattern Vectors. The *arity* of a PatVec [p1,..,pn] is
125 -- the number of p1..pn that are not Guards. See 'patternArity'.
126 type PatVec = [PmPat]
127 type ValVec = [Id] -- ^ Value Vector Abstractions
128
129 -- | Each 'Delta' is proof (i.e., a model of the fact) that some values are not
130 -- covered by a pattern match. E.g. @f Nothing = <rhs>@ might be given an
131 -- uncovered set @[x :-> Just y]@ or @[x /= Nothing]@, where @x@ is the variable
132 -- matching against @f@'s first argument.
133 type Uncovered = [Delta]
134
135 -- Instead of keeping the whole sets in memory, we keep a boolean for both the
136 -- covered and the divergent set (we store the uncovered set though, since we
137 -- want to print it). For both the covered and the divergent we have:
138 --
139 -- True <=> The set is non-empty
140 --
141 -- hence:
142 -- C = True ==> Useful clause (no warning)
143 -- C = False, D = True ==> Clause with inaccessible RHS
144 -- C = False, D = False ==> Redundant clause
145
146 data Covered = Covered | NotCovered
147 deriving Show
148
149 instance Outputable Covered where
150 ppr = text . show
151
152 -- Like the or monoid for booleans
153 -- Covered = True, Uncovered = False
154 instance Semi.Semigroup Covered where
155 Covered <> _ = Covered
156 _ <> Covered = Covered
157 NotCovered <> NotCovered = NotCovered
158
159 instance Monoid Covered where
160 mempty = NotCovered
161 mappend = (Semi.<>)
162
163 data Diverged = Diverged | NotDiverged
164 deriving Show
165
166 instance Outputable Diverged where
167 ppr = text . show
168
169 instance Semi.Semigroup Diverged where
170 Diverged <> _ = Diverged
171 _ <> Diverged = Diverged
172 NotDiverged <> NotDiverged = NotDiverged
173
174 instance Monoid Diverged where
175 mempty = NotDiverged
176 mappend = (Semi.<>)
177
178 -- | A triple <C,U,D> of covered, uncovered, and divergent sets.
179 data PartialResult = PartialResult {
180 presultCovered :: Covered
181 , presultUncovered :: Uncovered
182 , presultDivergent :: Diverged }
183
184 emptyPartialResult :: PartialResult
185 emptyPartialResult = PartialResult { presultUncovered = mempty
186 , presultCovered = mempty
187 , presultDivergent = mempty }
188
189 combinePartialResults :: PartialResult -> PartialResult -> PartialResult
190 combinePartialResults (PartialResult cs1 vsa1 ds1) (PartialResult cs2 vsa2 ds2)
191 = PartialResult (cs1 Semi.<> cs2)
192 (vsa1 Semi.<> vsa2)
193 (ds1 Semi.<> ds2)
194
195 instance Outputable PartialResult where
196 ppr (PartialResult c vsa d)
197 = hang (text "PartialResult" <+> ppr c <+> ppr d) 2 (ppr_vsa vsa)
198 where
199 ppr_vsa = braces . fsep . punctuate comma . map ppr
200
201 instance Semi.Semigroup PartialResult where
202 (<>) = combinePartialResults
203
204 instance Monoid PartialResult where
205 mempty = emptyPartialResult
206 mappend = (Semi.<>)
207
208 -- | Pattern check result
209 --
210 -- * Redundant clauses
211 -- * Not-covered clauses (or their type, if no pattern is available)
212 -- * Clauses with inaccessible RHS
213 --
214 -- More details about the classification of clauses into useful, redundant
215 -- and with inaccessible right hand side can be found here:
216 --
217 -- https://gitlab.haskell.org/ghc/ghc/wikis/pattern-match-check
218 --
219 data PmResult =
220 PmResult {
221 pmresultRedundant :: [Located [LPat GhcTc]]
222 , pmresultUncovered :: UncoveredCandidates
223 , pmresultInaccessible :: [Located [LPat GhcTc]] }
224
225 instance Outputable PmResult where
226 ppr pmr = hang (text "PmResult") 2 $ vcat
227 [ text "pmresultRedundant" <+> ppr (pmresultRedundant pmr)
228 , text "pmresultUncovered" <+> ppr (pmresultUncovered pmr)
229 , text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr)
230 ]
231
232 -- | Either a list of patterns that are not covered, or their type, in case we
233 -- have no patterns at hand. Not having patterns at hand can arise when
234 -- handling EmptyCase expressions, in two cases:
235 --
236 -- * The type of the scrutinee is a trivially inhabited type (like Int or Char)
237 -- * The type of the scrutinee cannot be reduced to WHNF.
238 --
239 -- In both these cases we have no inhabitation candidates for the type at hand,
240 -- but we don't want to issue just a wildcard as missing. Instead, we print a
241 -- type annotated wildcard, so that the user knows what kind of patterns is
242 -- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
243 data UncoveredCandidates = UncoveredPatterns [Id] [Delta]
244 | TypeOfUncovered Type
245
246 instance Outputable UncoveredCandidates where
247 ppr (UncoveredPatterns vva deltas) = text "UnPat" <+> ppr vva $$ ppr deltas
248 ppr (TypeOfUncovered ty) = text "UnTy" <+> ppr ty
249
250 {-
251 %************************************************************************
252 %* *
253 Entry points to the checker: checkSingle and checkMatches
254 %* *
255 %************************************************************************
256 -}
257
258 -- | Check a single pattern binding (let)
259 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
260 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
261 tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
262 mb_pm_res <- tryM (checkSingle' locn var p)
263 case mb_pm_res of
264 Left _ -> warnPmIters dflags ctxt
265 Right res -> dsPmWarn dflags ctxt res
266
267 -- | Check a single pattern binding (let)
268 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult
269 checkSingle' locn var p = do
270 resetPmIterDs -- set the iter-no to zero
271 fam_insts <- dsGetFamInstEnvs
272 clause <- translatePat fam_insts p
273 missing <- getPmDelta
274 tracePm "checkSingle': missing" (ppr missing)
275 PartialResult cs us ds <- pmcheckI clause [] [var] 1 missing
276 dflags <- getDynFlags
277 us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us
278 let uc = UncoveredPatterns [var] us'
279 return $ case (cs,ds) of
280 (Covered, _ ) -> PmResult [] uc [] -- useful
281 (NotCovered, NotDiverged) -> PmResult m uc [] -- redundant
282 (NotCovered, Diverged ) -> PmResult [] uc m -- inaccessible rhs
283 where m = [cL locn [cL locn p]]
284
285 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
286 -- in @MultiIf@ expressions.
287 checkGuardMatches :: HsMatchContext Name -- Match context
288 -> GRHSs GhcTc (LHsExpr GhcTc) -- Guarded RHSs
289 -> DsM ()
290 checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
291 dflags <- getDynFlags
292 let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
293 dsMatchContext = DsMatchContext hs_ctx combinedLoc
294 match = cL combinedLoc $
295 Match { m_ext = noExtField
296 , m_ctxt = hs_ctx
297 , m_pats = []
298 , m_grhss = guards }
299 checkMatches dflags dsMatchContext [] [match]
300 checkGuardMatches _ (XGRHSs nec) = noExtCon nec
301
302 -- | Check a matchgroup (case, functions, etc.)
303 checkMatches :: DynFlags -> DsMatchContext
304 -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
305 checkMatches dflags ctxt vars matches = do
306 tracePm "checkMatches" (hang (vcat [ppr ctxt
307 , ppr vars
308 , text "Matches:"])
309 2
310 (vcat (map ppr matches)))
311 mb_pm_res <- tryM $ case matches of
312 -- Check EmptyCase separately
313 -- See Note [Checking EmptyCase Expressions] in PmOracle
314 [] | [var] <- vars -> checkEmptyCase' var
315 _normal_match -> checkMatches' vars matches
316 case mb_pm_res of
317 Left _ -> warnPmIters dflags ctxt
318 Right res -> dsPmWarn dflags ctxt res
319
320 -- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
321 -- list of matches. For empty case expressions, use checkEmptyCase' instead.
322 checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult
323 checkMatches' vars matches
324 | null matches = panic "checkMatches': EmptyCase"
325 | otherwise = do
326 resetPmIterDs -- set the iter-no to zero
327 missing <- getPmDelta
328 tracePm "checkMatches': missing" (ppr missing)
329 (rs,us,ds) <- go matches [missing]
330 dflags <- getDynFlags
331 us' <- getNFirstUncovered vars (maxUncoveredPatterns dflags + 1) us
332 let up = UncoveredPatterns vars us'
333 return $ PmResult {
334 pmresultRedundant = map hsLMatchToLPats rs
335 , pmresultUncovered = up
336 , pmresultInaccessible = map hsLMatchToLPats ds }
337 where
338 go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
339 -> DsM ( [LMatch GhcTc (LHsExpr GhcTc)]
340 , Uncovered
341 , [LMatch GhcTc (LHsExpr GhcTc)])
342 go [] missing = return ([], missing, [])
343 go (m:ms) missing = do
344 tracePm "checkMatches': go" (ppr m)
345 fam_insts <- dsGetFamInstEnvs
346 (clause, guards) <- translateMatch fam_insts m
347 r@(PartialResult cs missing' ds)
348 <- runMany (pmcheckI clause guards vars (length missing)) missing
349 tracePm "checkMatches': go: res" (ppr r)
350 (rs, final_u, is) <- go ms missing'
351 return $ case (cs, ds) of
352 -- useful
353 (Covered, _ ) -> (rs, final_u, is)
354 -- redundant
355 (NotCovered, NotDiverged) -> (m:rs, final_u,is)
356 -- inaccessible
357 (NotCovered, Diverged ) -> (rs, final_u, m:is)
358
359 hsLMatchToLPats :: LMatch id body -> Located [LPat id]
360 hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
361 hsLMatchToLPats _ = panic "checkMatches'"
362
363 -- | Check an empty case expression. Since there are no clauses to process, we
364 -- only compute the uncovered set. See Note [Checking EmptyCase Expressions]
365 -- in "PmOracle" for details.
366 checkEmptyCase' :: Id -> DsM PmResult
367 checkEmptyCase' x = do
368 delta <- getPmDelta
369 us <- inhabitants delta (idType x) >>= \case
370 -- Inhabitation checking failed / the type is trivially inhabited
371 Left ty -> pure (TypeOfUncovered ty)
372 -- A list of oracle states for the different satisfiable constructors is
373 -- available. Turn this into a value set abstraction.
374 Right (va, deltas) -> pure (UncoveredPatterns [va] deltas)
375 pure (PmResult [] us [])
376
377 getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta]
378 getNFirstUncovered _ 0 _ = pure []
379 getNFirstUncovered _ _ [] = pure []
380 getNFirstUncovered vars n (delta:deltas) = do
381 front <- provideEvidenceForEquation vars n delta
382 back <- getNFirstUncovered vars (n - length front) deltas
383 pure (front ++ back)
384
385 -- | The maximum successive number of refinements ('refineToAltCon') we allow
386 -- per representative. See Note [Limit the number of refinements].
387 mAX_REFINEMENTS :: Int
388 -- The current number is chosen so that PrelRules is still checked with
389 -- reasonable performance. If this is set to below 2, ds022 will start to fail.
390 -- Although that is probably due to the fact that we always increase the
391 -- refinement counter instead of just increasing it when the contraposition
392 -- is satisfiable (when the not taken case 'addRefutableAltCon' is
393 -- satisfiable, that is). That would be the first thing I'd try if we have
394 -- performance problems on one test while decreasing the threshold leads to
395 -- other tests being broken like ds022 above.
396 mAX_REFINEMENTS = 3
397
398 -- | The threshold for detecting exponential blow-up in the number of 'Delta's
399 -- to check introduced by guards.
400 tHRESHOLD_GUARD_DELTAS :: Int
401 tHRESHOLD_GUARD_DELTAS = 100
402
403 -- | Multiply the estimated number of 'Delta's to process by a constant
404 -- branching factor induced by a guard and return the new estimate if it
405 -- doesn't exceed a constant threshold.
406 -- See 6. in Note [Guards and Approximation].
407 tryMultiplyDeltas :: Int -> Int -> Maybe Int
408 tryMultiplyDeltas multiplier n_delta
409 -- The ^2 below is intentional: We want to give up on guards with a large
410 -- branching factor rather quickly, still leaving room for small informative
411 -- ones later on.
412 | n_delta*multiplier^(2::Int) < tHRESHOLD_GUARD_DELTAS
413 = Just (n_delta*multiplier)
414 | otherwise
415 = Nothing
416
417 {-
418 %************************************************************************
419 %* *
420 Transform source syntax to *our* syntax
421 %* *
422 %************************************************************************
423 -}
424
425 -- -----------------------------------------------------------------------
426 -- * Utilities
427
428 nullaryConPattern :: ConLike -> PmPat
429 -- Nullary data constructor and nullary type constructor
430 nullaryConPattern con =
431 PmCon { pm_con_con = (PmAltConLike con), pm_con_arg_tys = []
432 , pm_con_tvs = [], pm_con_args = [] }
433 {-# INLINE nullaryConPattern #-}
434
435 truePattern :: PmPat
436 truePattern = nullaryConPattern (RealDataCon trueDataCon)
437 {-# INLINE truePattern #-}
438
439 -- | Generate a `canFail` pattern vector of a specific type
440 mkCanFailPmPat :: Type -> DsM PatVec
441 mkCanFailPmPat ty = do
442 var <- mkPmVar ty
443 return [var, PmFake]
444
445 vanillaConPattern :: ConLike -> [Type] -> PatVec -> PmPat
446 -- ADT constructor pattern => no existentials, no local constraints
447 vanillaConPattern con arg_tys args =
448 PmCon { pm_con_con = PmAltConLike con, pm_con_arg_tys = arg_tys
449 , pm_con_tvs = [], pm_con_args = args }
450 {-# INLINE vanillaConPattern #-}
451
452 -- | Create an empty list pattern of a given type
453 nilPattern :: Type -> PmPat
454 nilPattern ty =
455 PmCon { pm_con_con = PmAltConLike (RealDataCon nilDataCon)
456 , pm_con_arg_tys = [ty], pm_con_tvs = [], pm_con_args = [] }
457 {-# INLINE nilPattern #-}
458
459 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
460 mkListPatVec ty xs ys = [PmCon { pm_con_con = PmAltConLike (RealDataCon consDataCon)
461 , pm_con_arg_tys = [ty]
462 , pm_con_tvs = []
463 , pm_con_args = xs++ys }]
464 {-# INLINE mkListPatVec #-}
465
466 -- | Create a literal pattern
467 mkPmLitPattern :: PmLit -> PatVec
468 mkPmLitPattern lit@(PmLit _ val)
469 -- We translate String literals to list literals for better overlap reasoning.
470 -- It's a little unfortunate we do this here rather than in
471 -- 'PmOracle.trySolve' and 'PmOracle.addRefutableAltCon', but it's so much
472 -- simpler here.
473 -- See Note [Representation of Strings in TmState] in PmOracle
474 | PmLitString s <- val
475 , let mk_char_lit c = mkPmLitPattern (PmLit charTy (PmLitChar c))
476 = foldr (\c p -> mkListPatVec charTy (mk_char_lit c) p)
477 [nilPattern charTy]
478 (unpackFS s)
479 | otherwise
480 = [PmCon { pm_con_con = PmAltLit lit
481 , pm_con_arg_tys = []
482 , pm_con_tvs = []
483 , pm_con_args = [] }]
484 {-# INLINE mkPmLitPattern #-}
485
486 -- -----------------------------------------------------------------------
487 -- * Transform (Pat Id) into [PmPat]
488 -- The arity of the [PmPat] is always 1, but it may be a combination
489 -- of a vanilla pattern and a guard pattern.
490 -- Example: view pattern (f y -> Just x)
491 -- becomes [PmVar z, PmGrd [PmPat (Just x), f y]]
492 -- where z is fresh
493
494 translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
495 translatePat fam_insts pat = case pat of
496 WildPat ty -> mkPmVars [ty]
497 VarPat _ id -> return [PmVar (unLoc id)]
498 ParPat _ p -> translatePat fam_insts (unLoc p)
499 LazyPat _ _ -> mkPmVars [hsPatType pat] -- like a variable
500
501 -- ignore strictness annotations for now
502 BangPat _ p -> translatePat fam_insts (unLoc p)
503
504 -- (x@pat) ===> x (pat <- x)
505 AsPat _ (dL->L _ x) p -> do
506 pat <- translatePat fam_insts (unLoc p)
507 pure [PmVar x, PmGrd pat (Var x)]
508
509 SigPat _ p _ty -> translatePat fam_insts (unLoc p)
510
511 -- See Note [Translate CoPats]
512 CoPat _ wrapper p ty
513 | isIdHsWrapper wrapper -> translatePat fam_insts p
514 | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p
515 | otherwise -> do
516 ps <- translatePat fam_insts p
517 (xp,xe) <- mkPmId2Forms ty
518 g <- mkGuard ps (mkHsWrap wrapper (unLoc xe))
519 pure [xp,g]
520
521 -- (n + k) ===> x (True <- x >= k) (n <- x-k)
522 NPlusKPat ty (dL->L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty
523
524 -- (fun -> pat) ===> x (pat <- fun x)
525 ViewPat arg_ty lexpr lpat -> do
526 ps <- translatePat fam_insts (unLoc lpat)
527 -- See Note [Guards and Approximation]
528 res <- allM cantFailPattern ps
529 case res of
530 True -> do
531 (xp,xe) <- mkPmId2Forms arg_ty
532 g <- mkGuard ps (HsApp noExtField lexpr xe)
533 return [xp, g]
534 False -> mkCanFailPmPat arg_ty
535
536 -- list
537 ListPat (ListPatTc ty Nothing) ps -> do
538 pv <- translatePatVec fam_insts (map unLoc ps)
539 return (foldr (mkListPatVec ty) [nilPattern ty] pv)
540
541 -- overloaded list
542 ListPat (ListPatTc _elem_ty (Just (pat_ty, _to_list))) lpats -> do
543 dflags <- getDynFlags
544 if xopt LangExt.RebindableSyntax dflags
545 then mkCanFailPmPat pat_ty
546 else case splitListTyConApp_maybe pat_ty of
547 Just e_ty -> translatePat fam_insts
548 (ListPat (ListPatTc e_ty Nothing) lpats)
549 Nothing -> mkCanFailPmPat pat_ty
550 -- (a) In the presence of RebindableSyntax, we don't know anything about
551 -- `toList`, we should treat `ListPat` as any other view pattern.
552 --
553 -- (b) In the absence of RebindableSyntax,
554 -- - If the pat_ty is `[a]`, then we treat the overloaded list pattern
555 -- as ordinary list pattern. Although we can give an instance
556 -- `IsList [Int]` (more specific than the default `IsList [a]`), in
557 -- practice, we almost never do that. We assume the `_to_list` is
558 -- the `toList` from `instance IsList [a]`.
559 --
560 -- - Otherwise, we treat the `ListPat` as ordinary view pattern.
561 --
562 -- See #14547, especially comment#9 and comment#10.
563 --
564 -- Here we construct CanFailPmPat directly, rather can construct a view
565 -- pattern and do further translation as an optimization, for the reason,
566 -- see Note [Guards and Approximation].
567
568 ConPatOut { pat_con = (dL->L _ con)
569 , pat_arg_tys = arg_tys
570 , pat_tvs = ex_tvs
571 , pat_args = ps } -> do
572 let ty = conLikeResTy con arg_tys
573 groups <- allCompleteMatches ty
574 case groups of
575 [] -> mkCanFailPmPat ty
576 _ -> do
577 args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
578 return [PmCon { pm_con_con = PmAltConLike con
579 , pm_con_arg_tys = arg_tys
580 , pm_con_tvs = ex_tvs
581 , pm_con_args = args }]
582
583 NPat ty (dL->L _ olit) mb_neg _ -> do
584 -- See Note [Literal short cut] in MatchLit.hs
585 -- We inline the Literal short cut for @ty@ here, because @ty@ is more
586 -- precise than the field of OverLitTc, which is all that dsOverLit (which
587 -- normally does the literal short cut) can look at. Also @ty@ matches the
588 -- type of the scrutinee, so info on both pattern and scrutinee (for which
589 -- short cutting in dsOverLit works properly) is overloaded iff either is.
590 dflags <- getDynFlags
591 core_expr <- case olit of
592 OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ }
593 | not rebindable
594 , Just expr <- shortCutLit dflags val ty
595 -> dsExpr expr
596 _ -> dsOverLit olit
597 let lit = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr)
598 let lit' = case mb_neg of
599 Just _ -> expectJust "failed to negate lit" (negatePmLit lit)
600 Nothing -> lit
601 return (mkPmLitPattern lit')
602
603 LitPat _ lit -> do
604 core_expr <- dsLit (convertLit lit)
605 let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr)
606 return (mkPmLitPattern lit)
607
608 TuplePat tys ps boxity -> do
609 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
610 let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
611 tys' = case boxity of
612 Boxed -> tys
613 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
614 Unboxed -> map getRuntimeRep tys ++ tys
615 return [vanillaConPattern tuple_con tys' (concat tidy_ps)]
616
617 SumPat ty p alt arity -> do
618 tidy_p <- translatePat fam_insts (unLoc p)
619 let sum_con = RealDataCon (sumDataCon alt arity)
620 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
621 return [vanillaConPattern sum_con (map getRuntimeRep ty ++ ty) tidy_p]
622
623 -- --------------------------------------------------------------------------
624 -- Not supposed to happen
625 ConPatIn {} -> panic "Check.translatePat: ConPatIn"
626 SplicePat {} -> panic "Check.translatePat: SplicePat"
627 XPat {} -> panic "Check.translatePat: XPat"
628
629 -- | Translate a list of patterns (Note: each pattern is translated
630 -- to a pattern vector but we do not concatenate the results).
631 translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
632 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
633
634 -- | Translate a constructor pattern
635 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
636 -> ConLike -> HsConPatDetails GhcTc
637 -> DsM PatVec
638 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
639 = concat <$> translatePatVec fam_insts (map unLoc ps)
640 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
641 = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
642 translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
643 -- Nothing matched. Make up some fresh term variables
644 | null fs = mkPmVars arg_tys
645 -- The data constructor was not defined using record syntax. For the
646 -- pattern to be in record syntax it should be empty (e.g. Just {}).
647 -- So just like the previous case.
648 | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
649 -- Some of the fields appear, in the original order (there may be holes).
650 -- Generate a simple constructor pattern and make up fresh variables for
651 -- the rest of the fields
652 | matched_lbls `subsetOf` orig_lbls
653 = ASSERT(orig_lbls `equalLength` arg_tys)
654 let translateOne (lbl, ty) = case lookup lbl matched_pats of
655 Just p -> translatePat fam_insts p
656 Nothing -> mkPmVars [ty]
657 in concatMapM translateOne (zip orig_lbls arg_tys)
658 -- The fields that appear are not in the correct order. Make up fresh
659 -- variables for all fields and add guards after matching, to force the
660 -- evaluation in the correct order.
661 | otherwise = do
662 arg_var_pats <- mkPmVars arg_tys
663 translated_pats <- forM matched_pats $ \(x,pat) -> do
664 pvec <- translatePat fam_insts pat
665 return (x, pvec)
666
667 let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
668 guards = map (\(name,pvec) -> case lookup name zipped of
669 Just x -> PmGrd pvec (Var x)
670 Nothing -> panic "translateConPatVec: lookup")
671 translated_pats
672
673 return (arg_var_pats ++ guards)
674 where
675 -- The actual argument types (instantiated)
676 arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
677
678 -- Some label information
679 orig_lbls = map flSelector $ conLikeFieldLabels c
680 matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
681 | (dL->L _ x) <- fs]
682 matched_lbls = [ name | (name, _pat) <- matched_pats ]
683
684 subsetOf :: Eq a => [a] -> [a] -> Bool
685 subsetOf [] _ = True
686 subsetOf (_:_) [] = False
687 subsetOf (x:xs) (y:ys)
688 | x == y = subsetOf xs ys
689 | otherwise = subsetOf (x:xs) ys
690
691 -- Translate a single match
692 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
693 -> DsM (PatVec, [PatVec])
694 translateMatch fam_insts (dL->L _ (Match { m_pats = lpats, m_grhss = grhss }))
695 = do
696 pats' <- concat <$> translatePatVec fam_insts pats
697 guards' <- mapM (translateGuards fam_insts) guards
698 -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards'])
699 return (pats', guards')
700 where
701 extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
702 extractGuards (dL->L _ (GRHS _ gs _)) = map unLoc gs
703 extractGuards _ = panic "translateMatch"
704
705 pats = map unLoc lpats
706 guards = map extractGuards (grhssGRHSs grhss)
707 translateMatch _ _ = panic "translateMatch"
708
709 -- -----------------------------------------------------------------------
710 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
711
712 -- | Translate a list of guard statements to a pattern vector
713 translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
714 translateGuards fam_insts guards =
715 concat <$> mapM (translateGuard fam_insts) guards
716
717 -- | Check whether a pattern can fail to match
718 cantFailPattern :: PmPat -> DsM Bool
719 cantFailPattern PmVar {} = pure True
720 cantFailPattern PmCon { pm_con_con = c, pm_con_arg_tys = tys, pm_con_args = ps}
721 = (&&) <$> singleMatchConstructor c tys <*> allM cantFailPattern ps
722 cantFailPattern (PmGrd pv _e) = allM cantFailPattern pv
723 cantFailPattern _ = pure False
724
725 -- | Translate a guard statement to Pattern
726 translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
727 translateGuard fam_insts guard = case guard of
728 BodyStmt _ e _ _ -> translateBoolGuard e
729 LetStmt _ binds -> translateLet (unLoc binds)
730 BindStmt _ p e _ _ -> translateBind fam_insts p e
731 LastStmt {} -> panic "translateGuard LastStmt"
732 ParStmt {} -> panic "translateGuard ParStmt"
733 TransStmt {} -> panic "translateGuard TransStmt"
734 RecStmt {} -> panic "translateGuard RecStmt"
735 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
736 XStmtLR nec -> noExtCon nec
737
738 -- | Translate let-bindings
739 translateLet :: HsLocalBinds GhcTc -> DsM PatVec
740 translateLet _binds = return []
741
742 -- | Translate a pattern guard
743 translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
744 translateBind fam_insts (dL->L _ p) e = do
745 ps <- translatePat fam_insts p
746 g <- mkGuard ps (unLoc e)
747 return [g]
748
749 -- | Translate a boolean guard
750 translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
751 translateBoolGuard e
752 | isJust (isTrueLHsExpr e) = return []
753 -- The formal thing to do would be to generate (True <- True)
754 -- but it is trivial to solve so instead we give back an empty
755 -- PatVec for efficiency
756 | otherwise = (:[]) <$> mkGuard [truePattern] (unLoc e)
757
758 {- Note [Guards and Approximation]
759 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
760 Even if the algorithm is really expressive, the term oracle we use is not.
761 Hence, several features are not translated *properly* but we approximate.
762 The list includes:
763
764 1. View Patterns
765 ----------------
766 A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
767 oracle does not handle function applications so we know that the generated
768 constraints will not be handled at the end. Hence, we distinguish between two
769 cases:
770 a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
771 thing*.
772 b) Pattern @p@ can fail. This means that when checking the guard, we will
773 generate several cases, with no useful information. E.g.:
774
775 h (f -> [a,b]) = ...
776 h x ([a,b] <- f x) = ...
777
778 uncovered set = { [x |> { False ~ (f x ~ []) }]
779 , [x |> { False ~ (f x ~ (t1:[])) }]
780 , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
781
782 So we have two problems:
783 1) Since we do not print the constraints in the general case (they may
784 be too many), the warning will look like this:
785
786 Pattern match(es) are non-exhaustive
787 In an equation for `h':
788 Patterns not matched:
789 _
790 _
791 _
792 Which is not short and not more useful than a single underscore.
793 2) The size of the uncovered set increases a lot, without gaining more
794 expressivity in our warnings.
795
796 Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
797 @PmFake@: @True <- _@. That is, we record that there is a possibility
798 of failure but we minimize it to a True/False. This generates a single
799 warning and much smaller uncovered sets.
800
801 2. Overloaded Lists
802 -------------------
803 An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
804 problem is exactly like above, as its solution. For future reference, the code
805 below is the *right thing to do*:
806
807 ListPat (ListPatTc elem_ty (Just (pat_ty, _to_list))) lpats
808 otherwise -> do
809 (xp, xe) <- mkPmId2Forms pat_ty
810 ps <- translatePatVec (map unLoc lpats)
811 let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
812 g = mkGuard pats (HsApp (noLoc to_list) xe)
813 return [xp,g]
814
815 3. Overloaded Literals
816 ----------------------
817 The case with literals is a bit different. a literal @l@ should be translated
818 to @x (True <- x == from l)@. Since we want to have better warnings for
819 overloaded literals as it is a very common feature, we treat them differently.
820 They are mainly covered in Note [Undecidable Equality for PmAltCons] in PmExpr.
821
822 4. N+K Patterns & Pattern Synonyms
823 ----------------------------------
824 An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
825 Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
826 and has two possible outcomes. Hence, there is no benefit in using a dummy and
827 we implement the proper thing. Pattern synonyms are simply not implemented yet.
828 Hence, to be conservative, we generate a dummy pattern, assuming that the
829 pattern can fail.
830
831 5. Actual Guards
832 ----------------
833 During translation, boolean guards and pattern guards are translated properly.
834 Let bindings though are omitted by function @translateLet@. Since they are lazy
835 bindings, we do not actually want to generate a (strict) equality (like we do
836 in the pattern bind case). Hence, we safely drop them.
837
838 Additionally, top-level guard translation (performed by @translateGuards@)
839 replaces guards that cannot be reasoned about (like the ones we described in
840 1-4) with a single @PmFake@ to record the possibility of failure to match.
841
842 6. Combinatorial explosion
843 --------------------------
844 Function with many clauses and deeply nested guards like in #11195 tend to
845 overwhelm the checker because they lead to exponential splitting behavior.
846 See the comments on #11195 on refinement trees. Every guard refines the
847 disjunction of Deltas by another split. This no different than the ConVar case,
848 but in stark contrast we mostly don't get any useful information out of that
849 split! Hence splitting k-fold just means having k-fold more work. The problem
850 exacerbates for larger k, because it gets even more unlikely that we can handle
851 all of the arising Deltas better than just continue working on the original
852 Delta.
853 Long story short: At each point we estimate the number of Deltas we possibly
854 have to check in the same manner as the current Delta. If we hit a guard that
855 splits the current Delta k-fold, we check whether this split would get us beyond
856 a certain threshold ('tryMultiplyDeltas') and continue to check the other guards
857 with the original Delta.
858
859 Note [Limit the number of refinements]
860 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
861 In PrelRules, we have a huge case with relatively deep matches on pattern
862 synonyms. Since we allow multiple compatible solutions in the oracle
863 (i.e. @x ~ [I# y, 42]@), and every pattern synonym is compatible according to
864 'eqPmAltCon' with every other (no generativity as with DataCons), what would
865 usually result in a ConVar split where only one branch is satisfiable results
866 in a blow-up of Deltas. Here's an example:
867 case x of
868 A (A _) -> ()
869 B (B _) -> ()
870 ...
871 By the time we hit the first clause's RHS, we have split the initial Delta twice
872 and handled the {x~A y, y ~ A z} case, leaving {x/~A} and {x~A y, y/~A} models
873 for the second clause to check.
874
875 Now consider what happens if A=Left, B=Right. We get x~B y' from the match,
876 which contradicts with {x~A y, y/~A}, because A and B are incompatible due to
877 the generative nature of DataCons. This leaves only {x/~A} for checking B's
878 clause, which ultimately leaves {x/~[A,B]} and {x~B y', y'/~B} uncovered.
879 Resulting in three models to check for the next clause. That's only linear
880 growth in the number of models for each clause.
881
882 Consider A and B were arbitrary pattern synonyms instead. We still get x~B y'
883 from the match, but this no longer refutes {x~A y, y/~A}, because we don't
884 assume generativity for pattern synonyms. Ergo, @eqPmAltCon A B == Nothing@
885 and we get to check the second clause's inner match with {x~B y', x/~A} and
886 {x~[A y,B y'], y/~A}, splitting both in turn. That makes 4 instead of 3 deltas.
887 If we keep on doing this, we see that in the nth clause we'd have O(2^n) models
888 to check instead of just O(n) as above!
889
890 Clearly we have to put a stop to this. So we count in the oracle the number of
891 times we refined x to some constructor. If the number of splits exceeds the
892 'mAX_REFINEMENTS', we check the next clause using the original Delta rather
893 than the union of Deltas arising from the ConVar split.
894
895 If for the above example we had mAX_REFINEMENTS=1, then in the second clause
896 we would still check the inner match with {x~B y', x/~A} and {x~[A y,B y'], y/~A}
897 but *discard* the two Deltas arising from splitting {x~[A y,B y'], y/~A},
898 checking the next clause with {x~A y, y/~A} instead of its two refinements.
899 In addition to {x~B y', y'~B z', x/~A} (which arose from the other split) and
900 {x/~[A,B]} that makes 3 models for the third equation, so linear :).
901
902 Note [Translate CoPats]
903 ~~~~~~~~~~~~~~~~~~~~~~~
904 The pattern match checker did not know how to handle coerced patterns `CoPat`
905 efficiently, which gave rise to #11276. The original approach translated
906 `CoPat`s:
907
908 pat |> co ===> x (pat <- (x |> co))
909
910 Why did we do this seemingly unnecessary expansion in the first place?
911 The reason is that the type of @pat |> co@ (which is the type of the value
912 abstraction we match against) might be different than that of @pat@. Data
913 instances such as @Sing (a :: Bool)@ are a good example of this: If we would
914 just drop the coercion, we'd get a type error when matching @pat@ against its
915 value abstraction, with the result being that pmIsSatisfiable decides that every
916 possible data constructor fitting @pat@ is rejected as uninhabitated, leading to
917 a lot of false warnings.
918
919 But we can check whether the coercion is a hole or if it is just refl, in
920 which case we can drop it.
921
922 %************************************************************************
923 %* *
924 Utilities for Pattern Match Checking
925 %* *
926 %************************************************************************
927 -}
928
929 -- ----------------------------------------------------------------------------
930 -- * Basic utilities
931
932 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
933 -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
934 pmPatType :: PmPat -> Type
935 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
936 = pmAltConType con tys
937 pmPatType (PmVar { pm_var_id = x }) = idType x
938 pmPatType (PmGrd { pm_grd_pv = pv })
939 = ASSERT(patVecArity pv == 1) (pmPatType p)
940 where Just p = find ((==1) . patternArity) pv
941 pmPatType PmFake = pmPatType truePattern
942
943 {-
944 Note [Extensions to GADTs Meet Their Match]
945 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
946 The GADTs Meet Their Match paper presents the formalism that GHC's coverage
947 checker adheres to. Since the paper's publication, there have been some
948 additional features added to the coverage checker which are not described in
949 the paper. This Note serves as a reference for these new features.
950
951 * Value abstractions are severely simplified to the point where they are just
952 variables. The information about the PmExpr shape of a variable is encoded in
953 the oracle state 'Delta' instead.
954 * Handling of uninhabited fields like `!Void`.
955 See Note [Strict argument type constraints] in PmOracle.
956 * Efficient handling of literal splitting, large enumerations and accurate
957 redundancy warnings for `COMPLETE` groups through the oracle.
958 -}
959
960 -- ----------------------------------------------------------------------------
961 -- * More smart constructors and fresh variable generation
962
963 -- | Create a guard pattern
964 mkGuard :: PatVec -> HsExpr GhcTc -> DsM PmPat
965 mkGuard pv e = PmGrd pv <$> dsExpr e
966
967 -- | Generate a variable pattern of a given type
968 mkPmVar :: Type -> DsM PmPat
969 mkPmVar ty = PmVar <$> mkPmId ty
970
971 -- | Generate many variable patterns, given a list of types
972 mkPmVars :: [Type] -> DsM PatVec
973 mkPmVars tys = mapM mkPmVar tys
974
975 -- | Generate a fresh term variable of a given and return it in two forms:
976 -- * A variable pattern
977 -- * A variable expression
978 mkPmId2Forms :: Type -> DsM (PmPat, LHsExpr GhcTc)
979 mkPmId2Forms ty = do
980 x <- mkPmId ty
981 return (PmVar x, noLoc (HsVar noExtField (noLoc x)))
982
983 -- | Check whether a 'PmAltCon' has the /single match/ property, i.e. whether
984 -- it is the only possible match in the given context. See also
985 -- 'allCompleteMatches' and Note [Single match constructors].
986 singleMatchConstructor :: PmAltCon -> [Type] -> DsM Bool
987 singleMatchConstructor PmAltLit{} _ = pure False
988 singleMatchConstructor (PmAltConLike cl) tys =
989 any isSingleton <$> allCompleteMatches (conLikeResTy cl tys)
990
991 {-
992 Note [Single match constructors]
993 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
994 When translating pattern guards for consumption by the checker, we desugar
995 every pattern guard that might fail ('cantFailPattern') to 'PmFake'
996 (True <- _). Which patterns can't fail? Exactly those that only match on
997 'singleMatchConstructor's.
998
999 Here are a few examples:
1000 * @f a | (a, b) <- foo a = 42@: Product constructors are generally
1001 single match. This extends to single constructors of GADTs like 'Refl'.
1002 * If @f | Id <- id () = 42@, where @pattern Id = ()@ and 'Id' is part of a
1003 singleton `COMPLETE` set, then 'Id' has the single match property.
1004
1005 In effect, we can just enumerate 'allCompleteMatches' and check if the conlike
1006 occurs as a singleton set.
1007 There's the chance that 'Id' is part of multiple `COMPLETE` sets. That's
1008 irrelevant; If the user specified a singleton set, it is single-match.
1009
1010 Note that this doesn't really take into account incoming type constraints;
1011 It might be obvious from type context that a particular GADT constructor has
1012 the single-match property. We currently don't (can't) check this in the
1013 translation step. See #15753 for why this yields surprising results.
1014 -}
1015
1016 -- | For a given type, finds all the COMPLETE sets of conlikes that inhabit it.
1017 --
1018 -- Note that for a data family instance, this must be the *representation* type.
1019 -- e.g. data instance T (a,b) = T1 a b
1020 -- leads to
1021 -- data TPair a b = T1 a b -- The "representation" type
1022 -- It is TPair a b, not T (a, b), that is given to allCompleteMatches
1023 --
1024 -- These come from two places.
1025 -- 1. From data constructors defined with the result type constructor.
1026 -- 2. From `COMPLETE` pragmas which have the same type as the result
1027 -- type constructor. Note that we only use `COMPLETE` pragmas
1028 -- *all* of whose pattern types match. See #14135
1029 allCompleteMatches :: Type -> DsM [[ConLike]]
1030 allCompleteMatches ty = case splitTyConApp_maybe ty of
1031 Nothing -> pure [] -- NB: We don't know any COMPLETE set, as opposed to [[]]
1032 Just (tc, tc_args) -> do
1033 -- Look into the representation type of a data family instance, too.
1034 env <- dsGetFamInstEnvs
1035 let (tc', _tc_args', _co) = tcLookupDataFamInst env tc tc_args
1036 let mb_rdcs = map RealDataCon <$> tyConDataCons_maybe tc'
1037 let maybe_to_list = maybe [] (:[])
1038 let rdcs = maybe_to_list mb_rdcs
1039 -- NB: tc, because COMPLETE sets are associated with the parent data family
1040 -- TyCon
1041 pragmas <- dsGetCompleteMatches tc
1042 let fams = mapM dsLookupConLike . completeMatchConLikes
1043 pscs <- mapM fams pragmas
1044 let candidates = rdcs ++ pscs
1045 -- Check that all the pattern synonym return types in a `COMPLETE`
1046 -- pragma subsume the type we're matching.
1047 -- See Note [Filtering out non-matching COMPLETE sets]
1048 pure (filter (isValidCompleteMatch ty) candidates)
1049 where
1050 isValidCompleteMatch :: Type -> [ConLike] -> Bool
1051 isValidCompleteMatch ty = all p
1052 where
1053 p (RealDataCon _) = True
1054 p (PatSynCon ps) = isJust (tcMatchTy (projResTy (patSynSig ps)) ty)
1055 projResTy (_, _, _, _, _, res_ty) = res_ty
1056
1057 {-
1058 Note [Filtering out non-matching COMPLETE sets]
1059 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1060 Currently, conlikes in a COMPLETE set are simply grouped by the
1061 type constructor heading the return type. This is nice and simple, but it does
1062 mean that there are scenarios when a COMPLETE set might be incompatible with
1063 the type of a scrutinee. For instance, consider (from #14135):
1064
1065 data Foo a = Foo1 a | Foo2 a
1066
1067 pattern MyFoo2 :: Int -> Foo Int
1068 pattern MyFoo2 i = Foo2 i
1069
1070 {-# COMPLETE Foo1, MyFoo2 #-}
1071
1072 f :: Foo a -> a
1073 f (Foo1 x) = x
1074
1075 `f` has an incomplete pattern-match, so when choosing which constructors to
1076 report as unmatched in a warning, GHC must choose between the original set of
1077 data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe
1078 that GHC shouldn't even consider the COMPLETE set as a possibility: the return
1079 type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since
1080 there's no substitution `s` such that s(Foo Int) = Foo a.
1081
1082 To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern
1083 synonym constructor's return type matches the type of the scrutinee, and if one
1084 doesn't, then we remove the whole COMPLETE set from consideration.
1085
1086 One might wonder why GHC only checks /pattern synonym/ constructors, and not
1087 /data/ constructors as well. The reason is because that the type of a
1088 GADT constructor very well may not match the type of a scrutinee, and that's
1089 OK. Consider this example (from #14059):
1090
1091 data SBool (z :: Bool) where
1092 SFalse :: SBool False
1093 STrue :: SBool True
1094
1095 pattern STooGoodToBeTrue :: forall (z :: Bool). ()
1096 => z ~ True
1097 => SBool z
1098 pattern STooGoodToBeTrue = STrue
1099 {-# COMPLETE SFalse, STooGoodToBeTrue #-}
1100
1101 wobble :: SBool z -> Bool
1102 wobble STooGoodToBeTrue = True
1103
1104 In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse
1105 should be matched against, even though its type, SBool False, does not match
1106 the scrutinee type, SBool z.
1107
1108 SG: Another angle at this is that the implied constraints when we instantiate
1109 universal type variables in the return type of a GADT will lead to *provided*
1110 thetas, whereas when we instantiate the return type of a pattern synonym that
1111 corresponds to a *required* theta. See Note [Pattern synonym result type] in
1112 PatSyn. Note how isValidCompleteMatches will successfully filter out
1113
1114 pattern Just42 :: Maybe Int
1115 pattern Just42 = Just 42
1116
1117 But fail to filter out the equivalent
1118
1119 pattern Just'42 :: (a ~ Int) => Maybe a
1120 pattern Just'42 = Just 42
1121
1122 Which seems fine as far as tcMatchTy is concerned, but it raises a few eye
1123 brows.
1124 -}
1125
1126 {-
1127 %************************************************************************
1128 %* *
1129 Sanity Checks
1130 %* *
1131 %************************************************************************
1132 -}
1133
1134 -- | The arity of a pattern/pattern vector is the
1135 -- number of top-level patterns that are not guards
1136 type PmArity = Int
1137
1138 -- | Compute the arity of a pattern vector
1139 patVecArity :: PatVec -> PmArity
1140 patVecArity = sum . map patternArity
1141
1142 -- | Compute the arity of a pattern
1143 patternArity :: PmPat -> PmArity
1144 patternArity (PmGrd {}) = 0
1145 patternArity PmFake = 0
1146 patternArity _other_pat = 1
1147
1148 {-
1149 %************************************************************************
1150 %* *
1151 Heart of the algorithm: Function pmcheck
1152 %* *
1153 %************************************************************************
1154
1155 Main functions are:
1156
1157 * pmcheck :: PatVec -> [PatVec] -> ValVec -> Delta -> DsM PartialResult
1158
1159 This function implements functions `covered`, `uncovered` and
1160 `divergent` from the paper at once. Calls out to the auxilary function
1161 `pmcheckGuards` for handling (possibly multiple) guarded RHSs when the whole
1162 clause is checked. Slightly different from the paper because it does not even
1163 produce the covered and uncovered sets. Since we only care about whether a
1164 clause covers SOMETHING or if it may forces ANY argument, we only store a
1165 boolean in both cases, for efficiency.
1166
1167 * pmcheckGuards :: [PatVec] -> ValVec -> Delta -> DsM PartialResult
1168
1169 Processes the guards.
1170 -}
1171
1172 -- | Lift a pattern matching action from a single value vector abstration to a
1173 -- value set abstraction, but calling it on every vector and combining the
1174 -- results.
1175 runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult
1176 runMany _ [] = return emptyPartialResult
1177 runMany pm (m:ms) = do
1178 res <- pm m
1179 combinePartialResults res <$> runMany pm ms
1180
1181 -- | Increase the counter for elapsed algorithm iterations, check that the
1182 -- limit is not exceeded and call `pmcheck`
1183 pmcheckI :: PatVec -> [PatVec] -> ValVec -> Int -> Delta -> DsM PartialResult
1184 pmcheckI ps guards vva n delta = do
1185 m <- incrCheckPmIterDs
1186 tracePm "pmCheck" (ppr m <> colon
1187 $$ hang (text "patterns:") 2 (ppr ps)
1188 $$ hang (text "guards:") 2 (ppr guards)
1189 $$ ppr vva
1190 $$ ppr delta)
1191 res <- pmcheck ps guards vva n delta
1192 tracePm "pmCheckResult:" (ppr res)
1193 return res
1194 {-# INLINE pmcheckI #-}
1195
1196 -- | Increase the counter for elapsed algorithm iterations, check that the
1197 -- limit is not exceeded and call `pmcheckGuards`
1198 pmcheckGuardsI :: [PatVec] -> Int -> Delta -> DsM PartialResult
1199 pmcheckGuardsI gvs n delta = incrCheckPmIterDs >> pmcheckGuards gvs n delta
1200 {-# INLINE pmcheckGuardsI #-}
1201
1202 -- | Check the list of mutually exclusive guards
1203 pmcheckGuards :: [PatVec] -> Int -> Delta -> DsM PartialResult
1204 pmcheckGuards [] _ delta = return (usimple delta)
1205 pmcheckGuards (gv:gvs) n delta = do
1206 (PartialResult cs unc ds) <- pmcheckI gv [] [] n delta
1207 let (n', unc')
1208 -- See 6. in Note [Guards and Approximation]
1209 | Just n' <- tryMultiplyDeltas (length unc) n = (n', unc)
1210 | otherwise = (n, [delta])
1211 (PartialResult css uncs dss) <- runMany (pmcheckGuardsI gvs n') unc'
1212 return $ PartialResult (cs `mappend` css)
1213 uncs
1214 (ds `mappend` dss)
1215
1216 -- | Matching function: Check simultaneously a clause (takes separately the
1217 -- patterns and the list of guards) for exhaustiveness, redundancy and
1218 -- inaccessibility.
1219 pmcheck
1220 :: PatVec -- ^ Patterns of the clause
1221 -> [PatVec] -- ^ (Possibly multiple) guards of the clause
1222 -> ValVec -- ^ The value vector abstraction to match against
1223 -> Int -- ^ Estimate on the number of similar 'Delta's to handle.
1224 -- See 6. in Note [Guards and Approximation]
1225 -> Delta -- ^ Oracle state giving meaning to the identifiers in the ValVec
1226 -> DsM PartialResult
1227 pmcheck [] guards [] n delta
1228 | null guards = return $ mempty { presultCovered = Covered }
1229 | otherwise = pmcheckGuardsI guards n delta
1230
1231 -- Guard
1232 pmcheck (PmFake : ps) guards vva n delta =
1233 -- short-circuit if the guard pattern is useless.
1234 -- we just have two possible outcomes: fail here or match and recurse
1235 -- none of the two contains any useful information about the failure
1236 -- though. So just have these two cases but do not do all the boilerplate
1237 -- TODO: I don't think this should mkCons delta, rather than just replace the
1238 -- presultUncovered by [delta] completely. Note that the uncovered set
1239 -- returned from the recursive call can only be a refinement of the
1240 -- original delta.
1241 forces . mkCons delta <$> pmcheckI ps guards vva n delta
1242 pmcheck (p@PmGrd { pm_grd_pv = pv, pm_grd_expr = e } : ps) guards vva n delta = do
1243 tracePm "PmGrd: pmPatType" (vcat [ppr p, ppr (pmPatType p)])
1244 x <- mkPmId (exprType e)
1245 delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e
1246 pmcheckI (pv ++ ps) guards (x : vva) n delta'
1247
1248 -- Var: Add x :-> y to the oracle and recurse
1249 pmcheck (PmVar x : ps) guards (y : vva) n delta = do
1250 delta' <- expectJust "x is fresh" <$> addTmCt delta (TmVarVar x y)
1251 pmcheckI ps guards vva n delta'
1252
1253 -- ConVar
1254 pmcheck (p@PmCon{ pm_con_con = con, pm_con_args = args
1255 , pm_con_arg_tys = arg_tys, pm_con_tvs = ex_tvs } : ps)
1256 guards (x : vva) n delta = do
1257 -- E.g f (K p q) = <rhs>
1258 -- <next equation>
1259 -- Split the value vector into two value vectors:
1260 -- * one for <rhs>, binding x to (K p q)
1261 -- * one for <next equation>, recording that x is /not/ (K _ _)
1262
1263 -- Stuff for <rhs>
1264 pr_pos <- refineToAltCon delta x con arg_tys ex_tvs >>= \case
1265 Nothing -> pure mempty
1266 Just (delta', arg_vas) ->
1267 pmcheckI (args ++ ps) guards (arg_vas ++ vva) n delta'
1268
1269 -- Stuff for <next equation>
1270 -- The var is forced regardless of whether @con@ was satisfiable
1271 let pr_pos' = forceIfCanDiverge delta x pr_pos
1272 pr_neg <- addRefutableAltCon delta x con >>= \case
1273 Nothing -> pure mempty
1274 Just delta' -> pure (usimple delta')
1275
1276 tracePm "ConVar" (vcat [ppr p, ppr x, ppr pr_pos', ppr pr_neg])
1277
1278 -- Combine both into a single PartialResult
1279 let pr = mkUnion pr_pos' pr_neg
1280 case (presultUncovered pr_pos', presultUncovered pr_neg) of
1281 ([], _) -> pure pr
1282 (_, []) -> pure pr
1283 -- See Note [Limit the number of refinements]
1284 _ | lookupNumberOfRefinements delta x < mAX_REFINEMENTS
1285 -> pure pr
1286 | otherwise -> pure pr{ presultUncovered = [delta] }
1287
1288 pmcheck [] _ (_:_) _ _ = panic "pmcheck: nil-cons"
1289 pmcheck (_:_) _ [] _ _ = panic "pmcheck: cons-nil"
1290
1291 -- ----------------------------------------------------------------------------
1292 -- * Utilities for main checking
1293
1294 updateUncovered :: (Uncovered -> Uncovered) -> (PartialResult -> PartialResult)
1295 updateUncovered f p@(PartialResult { presultUncovered = old })
1296 = p { presultUncovered = f old }
1297
1298
1299 -- | Initialise with default values for covering and divergent information and
1300 -- a singleton uncovered set.
1301 usimple :: Delta -> PartialResult
1302 usimple delta = mempty { presultUncovered = [delta] }
1303
1304 -- | Get the union of two covered, uncovered and divergent value set
1305 -- abstractions. Since the covered and divergent sets are represented by a
1306 -- boolean, union means computing the logical or (at least one of the two is
1307 -- non-empty).
1308
1309 mkUnion :: PartialResult -> PartialResult -> PartialResult
1310 mkUnion = mappend
1311
1312 -- | Add a model to the uncovered set.
1313 mkCons :: Delta -> PartialResult -> PartialResult
1314 mkCons model = updateUncovered (model:)
1315
1316 -- | Set the divergent set to not empty
1317 forces :: PartialResult -> PartialResult
1318 forces pres = pres { presultDivergent = Diverged }
1319
1320 -- | Set the divergent set to non-empty if the variable has not been forced yet
1321 forceIfCanDiverge :: Delta -> Id -> PartialResult -> PartialResult
1322 forceIfCanDiverge delta x
1323 | canDiverge delta x = forces
1324 | otherwise = id
1325
1326 -- ----------------------------------------------------------------------------
1327 -- * Propagation of term constraints inwards when checking nested matches
1328
1329 {- Note [Type and Term Equality Propagation]
1330 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1331 When checking a match it would be great to have all type and term information
1332 available so we can get more precise results. For this reason we have functions
1333 `addDictsDs' and `addTmVarCsDs' in DsMonad that store in the environment type and
1334 term constraints (respectively) as we go deeper.
1335
1336 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1337 in HsPat.hs. This handles bug #4139 ( see example
1338 https://gitlab.haskell.org/ghc/ghc/snippets/672 )
1339 where this is needed.
1340
1341 For term equalities we do less, we just generate equalities for HsCase. For
1342 example we accurately give 2 redundancy warnings for the marked cases:
1343
1344 f :: [a] -> Bool
1345 f x = case x of
1346
1347 [] -> case x of -- brings (x ~ []) in scope
1348 [] -> True
1349 (_:_) -> False -- can't happen
1350
1351 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1352 (_:_) -> True
1353 [] -> False -- can't happen
1354
1355 Functions `addScrutTmCs' and `addPatTmCs' are responsible for generating
1356 these constraints.
1357 -}
1358
1359 locallyExtendPmDelta :: (Delta -> DsM (Maybe Delta)) -> DsM a -> DsM a
1360 locallyExtendPmDelta ext k = getPmDelta >>= ext >>= \case
1361 -- If adding a constraint would lead to a contradiction, don't add it.
1362 -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@
1363 -- for why this is done.
1364 Nothing -> k
1365 Just delta' -> updPmDelta delta' k
1366
1367 -- | Add in-scope type constraints
1368 addTyCsDs :: Bag EvVar -> DsM a -> DsM a
1369 addTyCsDs ev_vars =
1370 locallyExtendPmDelta (\delta -> addTypeEvidence delta ev_vars)
1371
1372 -- | Add equalities for the scrutinee to the local 'DsM' environment when
1373 -- checking a case expression:
1374 -- case e of x { matches }
1375 -- When checking matches we record that (x ~ e) where x is the initial
1376 -- uncovered. All matches will have to satisfy this equality.
1377 addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
1378 addScrutTmCs Nothing _ k = k
1379 addScrutTmCs (Just scr) [x] k = do
1380 scr_e <- dsLExpr scr
1381 locallyExtendPmDelta (\delta -> addVarCoreCt delta x scr_e) k
1382 addScrutTmCs _ _ _ = panic "addScrutTmCs: HsCase with more than one case binder"
1383
1384 -- | Add equalities to the local 'DsM' environment when checking the RHS of a
1385 -- case expression:
1386 -- case e of x { p1 -> e1; ... pn -> en }
1387 -- When we go deeper to check e.g. e1 we record (x ~ p1).
1388 addPatTmCs :: [Pat GhcTc] -- LHS (should have length 1)
1389 -> [Id] -- MatchVars (should have length 1)
1390 -> DsM a
1391 -> DsM a
1392 -- Morally, this computes an approximation of the Covered set for p1
1393 -- (which pmcheck currently discards). TODO: Re-use pmcheck instead of calling
1394 -- out to awkard addVarPatVecCt.
1395 addPatTmCs ps xs k = do
1396 fam_insts <- dsGetFamInstEnvs
1397 pv <- concat <$> translatePatVec fam_insts ps
1398 locallyExtendPmDelta (\delta -> addVarPatVecCt delta xs pv) k
1399
1400 -- ----------------------------------------------------------------------------
1401 -- * Converting between Value Abstractions, Patterns and PmExpr
1402
1403 -- | Add a constraint equating a variable to a 'PatVec'. Picks out the single
1404 -- 'PmPat' of arity 1 and equates x to it. Returns the original Delta if that
1405 -- fails. Otherwise it returns Nothing when the resulting Delta would be
1406 -- unsatisfiable, or @Just delta'@ when the extended @delta'@ is still possibly
1407 -- satisfiable.
1408 addVarPatVecCt :: Delta -> [Id] -> PatVec -> DsM (Maybe Delta)
1409 -- This is just a simple version of pmcheck to compute the Covered Delta
1410 -- (which pmcheck doesn't even attempt to keep).
1411 -- Also PmGrd, although having pattern arity 0, really stores important info.
1412 -- For example, as-patterns desugar to a plain variable match and an associated
1413 -- PmGrd for the RHS of the @. We don't currently look into that PmGrd and I'm
1414 -- not willing to duplicate any more of pmcheck.
1415 addVarPatVecCt delta (x:xs) (pat:pv)
1416 | patternArity pat == 1 -- PmVar or PmCon
1417 = runMaybeT $ do
1418 delta' <- MaybeT (addVarPatCt delta x pat)
1419 MaybeT (addVarPatVecCt delta' xs pv)
1420 | otherwise -- PmGrd or PmFake
1421 = addVarPatVecCt delta (x:xs) pv
1422 addVarPatVecCt delta [] pv = ASSERT( patVecArity pv == 0 ) pure (Just delta)
1423 addVarPatVecCt _ (_:_) [] = panic "More match vars than patterns"
1424
1425 -- | Convert a pattern to a 'PmExpr' (will be either 'Nothing' if the pattern is
1426 -- a guard pattern, or 'Just' an expression in all other cases) by dropping the
1427 -- guards
1428 addVarPatCt :: Delta -> Id -> PmPat -> DsM (Maybe Delta)
1429 addVarPatCt delta x (PmVar { pm_var_id = y }) = addTmCt delta (TmVarVar x y)
1430 addVarPatCt delta x (PmCon { pm_con_con = con, pm_con_args = args }) = runMaybeT $ do
1431 arg_ids <- traverse (lift . mkPmId . pmPatType) args
1432 delta' <- foldlM (\delta (y, arg) -> MaybeT (addVarPatCt delta y arg)) delta (zip arg_ids args)
1433 MaybeT (addTmCt delta' (TmVarCon x con arg_ids))
1434 addVarPatCt delta _ _pat = ASSERT( patternArity _pat == 0 ) pure (Just delta)
1435
1436 {-
1437 %************************************************************************
1438 %* *
1439 Pretty printing of exhaustiveness/redundancy check warnings
1440 %* *
1441 %************************************************************************
1442 -}
1443
1444 -- | Check whether any part of pattern match checking is enabled for this
1445 -- 'HsMatchContext' (does not matter whether it is the redundancy check or the
1446 -- exhaustiveness check).
1447 isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
1448 isMatchContextPmChecked dflags origin kind
1449 | isGenerated origin
1450 = False
1451 | otherwise
1452 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
1453
1454 -- | Return True when any of the pattern match warnings ('allPmCheckWarnings')
1455 -- are enabled, in which case we need to run the pattern match checker.
1456 needToRunPmCheck :: DynFlags -> Origin -> Bool
1457 needToRunPmCheck dflags origin
1458 | isGenerated origin
1459 = False
1460 | otherwise
1461 = notNull (filter (`wopt` dflags) allPmCheckWarnings)
1462
1463 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
1464 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
1465 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
1466 = when (flag_i || flag_u) $ do
1467 let exists_r = flag_i && notNull redundant
1468 exists_i = flag_i && notNull inaccessible && not is_rec_upd
1469 exists_u = flag_u && (case uncovered of
1470 TypeOfUncovered _ -> True
1471 UncoveredPatterns _ unc -> notNull unc)
1472
1473 when exists_r $ forM_ redundant $ \(dL->L l q) -> do
1474 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1475 (pprEqn q "is redundant"))
1476 when exists_i $ forM_ inaccessible $ \(dL->L l q) -> do
1477 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1478 (pprEqn q "has inaccessible right hand side"))
1479 when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
1480 case uncovered of
1481 TypeOfUncovered ty -> warnEmptyCase ty
1482 UncoveredPatterns vars unc -> pprEqns vars unc
1483 where
1484 PmResult
1485 { pmresultRedundant = redundant
1486 , pmresultUncovered = uncovered
1487 , pmresultInaccessible = inaccessible } = pm_result
1488
1489 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1490 flag_u = exhaustive dflags kind
1491 flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
1492
1493 is_rec_upd = case kind of { RecUpd -> True; _ -> False }
1494 -- See Note [Inaccessible warnings for record updates]
1495
1496 maxPatterns = maxUncoveredPatterns dflags
1497
1498 -- Print a single clause (for redundant/with-inaccessible-rhs)
1499 pprEqn q txt = pprContext True ctx (text txt) $ \f ->
1500 f (pprPats kind (map unLoc q))
1501
1502 -- Print several clauses (for uncovered clauses)
1503 pprEqns vars deltas = pprContext False ctx (text "are non-exhaustive") $ \_ ->
1504 case vars of -- See #11245
1505 [] -> text "Guards do not cover entire pattern space"
1506 _ -> let us = map (\delta -> pprUncovered delta vars) deltas
1507 in hang (text "Patterns not matched:") 4
1508 (vcat (take maxPatterns us) $$ dots maxPatterns us)
1509
1510 -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
1511 -- which we only know the type and have no inhabitants at hand)
1512 warnEmptyCase ty = pprContext False ctx (text "are non-exhaustive") $ \_ ->
1513 hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
1514
1515 {- Note [Inaccessible warnings for record updates]
1516 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1517 Consider (#12957)
1518 data T a where
1519 T1 :: { x :: Int } -> T Bool
1520 T2 :: { x :: Int } -> T a
1521 T3 :: T a
1522
1523 f :: T Char -> T a
1524 f r = r { x = 3 }
1525
1526 The desugarer will (conservatively generate a case for T1 even though
1527 it's impossible:
1528 f r = case r of
1529 T1 x -> T1 3 -- Inaccessible branch
1530 T2 x -> T2 3
1531 _ -> error "Missing"
1532
1533 We don't want to warn about the inaccessible branch because the programmer
1534 didn't put it there! So we filter out the warning here.
1535 -}
1536
1537 -- | Issue a warning when the predefined number of iterations is exceeded
1538 -- for the pattern match checker
1539 warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
1540 warnPmIters dflags (DsMatchContext kind loc)
1541 = when (flag_i || flag_u) $ do
1542 iters <- maxPmCheckIterations <$> getDynFlags
1543 putSrcSpanDs loc (warnDs NoReason (msg iters))
1544 where
1545 ctxt = pprMatchContext kind
1546 msg is = fsep [ text "Pattern match checker exceeded"
1547 , parens (ppr is), text "iterations in", ctxt <> dot
1548 , text "(Use -fmax-pmcheck-iterations=n"
1549 , text "to set the maximum number of iterations to n)" ]
1550
1551 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1552 flag_u = exhaustive dflags kind
1553
1554 dots :: Int -> [a] -> SDoc
1555 dots maxPatterns qs
1556 | qs `lengthExceeds` maxPatterns = text "..."
1557 | otherwise = empty
1558
1559 -- | All warning flags that need to run the pattern match checker.
1560 allPmCheckWarnings :: [WarningFlag]
1561 allPmCheckWarnings =
1562 [ Opt_WarnIncompletePatterns
1563 , Opt_WarnIncompleteUniPatterns
1564 , Opt_WarnIncompletePatternsRecUpd
1565 , Opt_WarnOverlappingPatterns
1566 ]
1567
1568 -- | Check whether the exhaustiveness checker should run (exhaustiveness only)
1569 exhaustive :: DynFlags -> HsMatchContext id -> Bool
1570 exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
1571
1572 -- | Denotes whether an exhaustiveness check is supported, and if so,
1573 -- via which 'WarningFlag' it's controlled.
1574 -- Returns 'Nothing' if check is not supported.
1575 exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
1576 exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
1577 exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
1578 exhaustiveWarningFlag IfAlt = Just Opt_WarnIncompletePatterns
1579 exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
1580 exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
1581 exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
1582 exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
1583 exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
1584 exhaustiveWarningFlag ThPatSplice = Nothing
1585 exhaustiveWarningFlag PatSyn = Nothing
1586 exhaustiveWarningFlag ThPatQuote = Nothing
1587 exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns
1588 -- in list comprehensions, pattern guards
1589 -- etc. They are often *supposed* to be
1590 -- incomplete
1591
1592 -- True <==> singular
1593 pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
1594 pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun
1595 = vcat [text txt <+> msg,
1596 sep [ text "In" <+> ppr_match <> char ':'
1597 , nest 4 (rest_of_msg_fun pref)]]
1598 where
1599 txt | singular = "Pattern match"
1600 | otherwise = "Pattern match(es)"
1601
1602 (ppr_match, pref)
1603 = case kind of
1604 FunRhs { mc_fun = (dL->L _ fun) }
1605 -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
1606 _ -> (pprMatchContext kind, \ pp -> pp)
1607
1608 pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
1609 pprPats kind pats
1610 = sep [sep (map ppr pats), matchSeparator kind, text "..."]