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