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