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