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