Fix #15385 by using addDictsDs in matchGuards
[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, checkGuardMatches, isAnyPmCheckEnabled,
13
14 -- See Note [Type and Term Equality Propagation]
15 genCaseTmCs1, genCaseTmCs2,
16
17 -- Pattern-match-specific type operations
18 pmIsClosedType, pmTopNormaliseType_maybe
19 ) where
20
21 #include "HsVersions.h"
22
23 import GhcPrelude
24
25 import TmOracle
26 import Unify( tcMatchTy )
27 import DynFlags
28 import HsSyn
29 import TcHsSyn
30 import Id
31 import ConLike
32 import Name
33 import FamInstEnv
34 import TysPrim (tYPETyCon)
35 import TysWiredIn
36 import TyCon
37 import SrcLoc
38 import Util
39 import Outputable
40 import FastString
41 import DataCon
42 import PatSyn
43 import HscTypes (CompleteMatch(..))
44
45 import DsMonad
46 import TcSimplify (tcCheckSatisfiability)
47 import TcType (isStringTy)
48 import Bag
49 import ErrUtils
50 import Var (EvVar)
51 import TyCoRep
52 import Type
53 import UniqSupply
54 import DsUtils (isTrueLHsExpr)
55 import Maybes (expectJust)
56 import qualified GHC.LanguageExtensions as LangExt
57
58 import Data.List (find)
59 import Data.Maybe (catMaybes, isJust, fromMaybe)
60 import Control.Monad (forM, when, forM_, zipWithM)
61 import Coercion
62 import TcEvidence
63 import IOEnv
64 import qualified Data.Semigroup as Semi
65
66 import ListT (ListT(..), fold, select)
67
68 {-
69 This module checks pattern matches for:
70 \begin{enumerate}
71 \item Equations that are redundant
72 \item Equations with inaccessible right-hand-side
73 \item Exhaustiveness
74 \end{enumerate}
75
76 The algorithm is based on the paper:
77
78 "GADTs Meet Their Match:
79 Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
80
81 http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf
82
83 %************************************************************************
84 %* *
85 Pattern Match Check Types
86 %* *
87 %************************************************************************
88 -}
89
90 -- We use the non-determinism monad to apply the algorithm to several
91 -- possible sets of constructors. Users can specify complete sets of
92 -- constructors by using COMPLETE pragmas.
93 -- The algorithm only picks out constructor
94 -- sets deep in the bowels which makes a simpler `mapM` more difficult to
95 -- implement. The non-determinism is only used in one place, see the ConVar
96 -- case in `pmCheckHd`.
97
98 type PmM a = ListT DsM a
99
100 liftD :: DsM a -> PmM a
101 liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
102
103 -- Pick the first match complete covered match or otherwise the "best" match.
104 -- The best match is the one with the least uncovered clauses, ties broken
105 -- by the number of inaccessible clauses followed by number of redundant
106 -- clauses.
107 --
108 -- This is specified in the
109 -- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
110 -- users' guide. If you update the implementation of this function, make sure
111 -- to update that section of the users' guide as well.
112 getResult :: PmM PmResult -> DsM PmResult
113 getResult ls
114 = do { res <- fold ls goM (pure Nothing)
115 ; case res of
116 Nothing -> panic "getResult is empty"
117 Just a -> return a }
118 where
119 goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
120 goM mpm dpm = do { pmr <- dpm
121 ; return $ Just $ go pmr mpm }
122
123 -- Careful not to force unecessary results
124 go :: Maybe PmResult -> PmResult -> PmResult
125 go Nothing rs = rs
126 go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
127 | null us && null rs && null is = old
128 | otherwise =
129 let PmResult prov' rs' (UncoveredPatterns us') is' = new
130 in case compareLength us us'
131 `mappend` (compareLength is is')
132 `mappend` (compareLength rs rs')
133 `mappend` (compare prov prov') of
134 GT -> new
135 EQ -> new
136 LT -> old
137 go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
138 = panic "getResult: No inhabitation candidates"
139
140 data PatTy = PAT | VA -- Used only as a kind, to index PmPat
141
142 -- The *arity* of a PatVec [p1,..,pn] is
143 -- the number of p1..pn that are not Guards
144
145 data PmPat :: PatTy -> * where
146 PmCon :: { pm_con_con :: ConLike
147 , pm_con_arg_tys :: [Type]
148 , pm_con_tvs :: [TyVar]
149 , pm_con_dicts :: [EvVar]
150 , pm_con_args :: [PmPat t] } -> PmPat t
151 -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
152 PmVar :: { pm_var_id :: Id } -> PmPat t
153 PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
154 PmNLit :: { pm_lit_id :: Id
155 , pm_lit_not :: [PmLit] } -> PmPat 'VA
156 PmGrd :: { pm_grd_pv :: PatVec
157 , pm_grd_expr :: PmExpr } -> PmPat 'PAT
158
159 -- data T a where
160 -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
161 -- or MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
162
163 type Pattern = PmPat 'PAT -- ^ Patterns
164 type ValAbs = PmPat 'VA -- ^ Value Abstractions
165
166 type PatVec = [Pattern] -- ^ Pattern Vectors
167 data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions
168
169 -- | Term and type constraints to accompany each value vector abstraction.
170 -- For efficiency, we store the term oracle state instead of the term
171 -- constraints. TODO: Do the same for the type constraints?
172 data Delta = MkDelta { delta_ty_cs :: Bag EvVar
173 , delta_tm_cs :: TmState }
174
175 type ValSetAbs = [ValVec] -- ^ Value Set Abstractions
176 type Uncovered = ValSetAbs
177
178 -- Instead of keeping the whole sets in memory, we keep a boolean for both the
179 -- covered and the divergent set (we store the uncovered set though, since we
180 -- want to print it). For both the covered and the divergent we have:
181 --
182 -- True <=> The set is non-empty
183 --
184 -- hence:
185 -- C = True ==> Useful clause (no warning)
186 -- C = False, D = True ==> Clause with inaccessible RHS
187 -- C = False, D = False ==> Redundant clause
188
189 data Covered = Covered | NotCovered
190 deriving Show
191
192 instance Outputable Covered where
193 ppr (Covered) = text "Covered"
194 ppr (NotCovered) = text "NotCovered"
195
196 -- Like the or monoid for booleans
197 -- Covered = True, Uncovered = False
198 instance Semi.Semigroup Covered where
199 Covered <> _ = Covered
200 _ <> Covered = Covered
201 NotCovered <> NotCovered = NotCovered
202
203 instance Monoid Covered where
204 mempty = NotCovered
205 mappend = (Semi.<>)
206
207 data Diverged = Diverged | NotDiverged
208 deriving Show
209
210 instance Outputable Diverged where
211 ppr Diverged = text "Diverged"
212 ppr NotDiverged = text "NotDiverged"
213
214 instance Semi.Semigroup Diverged where
215 Diverged <> _ = Diverged
216 _ <> Diverged = Diverged
217 NotDiverged <> NotDiverged = NotDiverged
218
219 instance Monoid Diverged where
220 mempty = NotDiverged
221 mappend = (Semi.<>)
222
223 -- | When we learned that a given match group is complete
224 data Provenance =
225 FromBuiltin -- ^ From the original definition of the type
226 -- constructor.
227 | FromComplete -- ^ From a user-provided @COMPLETE@ pragma
228 deriving (Show, Eq, Ord)
229
230 instance Outputable Provenance where
231 ppr = text . show
232
233 instance Semi.Semigroup Provenance where
234 FromComplete <> _ = FromComplete
235 _ <> FromComplete = FromComplete
236 _ <> _ = FromBuiltin
237
238 instance Monoid Provenance where
239 mempty = FromBuiltin
240 mappend = (Semi.<>)
241
242 data PartialResult = PartialResult {
243 presultProvenance :: Provenance
244 -- keep track of provenance because we don't want
245 -- to warn about redundant matches if the result
246 -- is contaminated with a COMPLETE pragma
247 , presultCovered :: Covered
248 , presultUncovered :: Uncovered
249 , presultDivergent :: Diverged }
250
251 instance Outputable PartialResult where
252 ppr (PartialResult prov c vsa d)
253 = text "PartialResult" <+> ppr prov <+> ppr c
254 <+> ppr d <+> ppr vsa
255
256
257 instance Semi.Semigroup PartialResult where
258 (PartialResult prov1 cs1 vsa1 ds1)
259 <> (PartialResult prov2 cs2 vsa2 ds2)
260 = PartialResult (prov1 Semi.<> prov2)
261 (cs1 Semi.<> cs2)
262 (vsa1 Semi.<> vsa2)
263 (ds1 Semi.<> ds2)
264
265
266 instance Monoid PartialResult where
267 mempty = PartialResult mempty mempty [] mempty
268 mappend = (Semi.<>)
269
270 -- newtype ChoiceOf a = ChoiceOf [a]
271
272 -- | Pattern check result
273 --
274 -- * Redundant clauses
275 -- * Not-covered clauses (or their type, if no pattern is available)
276 -- * Clauses with inaccessible RHS
277 --
278 -- More details about the classification of clauses into useful, redundant
279 -- and with inaccessible right hand side can be found here:
280 --
281 -- https://ghc.haskell.org/trac/ghc/wiki/PatternMatchCheck
282 --
283 data PmResult =
284 PmResult {
285 pmresultProvenance :: Provenance
286 , pmresultRedundant :: [Located [LPat GhcTc]]
287 , pmresultUncovered :: UncoveredCandidates
288 , pmresultInaccessible :: [Located [LPat GhcTc]] }
289
290 -- | Either a list of patterns that are not covered, or their type, in case we
291 -- have no patterns at hand. Not having patterns at hand can arise when
292 -- handling EmptyCase expressions, in two cases:
293 --
294 -- * The type of the scrutinee is a trivially inhabited type (like Int or Char)
295 -- * The type of the scrutinee cannot be reduced to WHNF.
296 --
297 -- In both these cases we have no inhabitation candidates for the type at hand,
298 -- but we don't want to issue just a wildcard as missing. Instead, we print a
299 -- type annotated wildcard, so that the user knows what kind of patterns is
300 -- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
301 data UncoveredCandidates = UncoveredPatterns Uncovered
302 | TypeOfUncovered Type
303
304 -- | The empty pattern check result
305 emptyPmResult :: PmResult
306 emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
307
308 -- | Non-exhaustive empty case with unknown/trivial inhabitants
309 uncoveredWithTy :: Type -> PmResult
310 uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
311
312 {-
313 %************************************************************************
314 %* *
315 Entry points to the checker: checkSingle and checkMatches
316 %* *
317 %************************************************************************
318 -}
319
320 -- | Check a single pattern binding (let)
321 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
322 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
323 tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
324 mb_pm_res <- tryM (getResult (checkSingle' locn var p))
325 case mb_pm_res of
326 Left _ -> warnPmIters dflags ctxt
327 Right res -> dsPmWarn dflags ctxt res
328
329 -- | Check a single pattern binding (let)
330 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
331 checkSingle' locn var p = do
332 liftD resetPmIterDs -- set the iter-no to zero
333 fam_insts <- liftD dsGetFamInstEnvs
334 clause <- liftD $ translatePat fam_insts p
335 missing <- mkInitialUncovered [var]
336 tracePm "checkSingle: missing" (vcat (map pprValVecDebug missing))
337 -- no guards
338 PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
339 let us' = UncoveredPatterns us
340 return $ case (cs,ds) of
341 (Covered, _ ) -> PmResult prov [] us' [] -- useful
342 (NotCovered, NotDiverged) -> PmResult prov m us' [] -- redundant
343 (NotCovered, Diverged ) -> PmResult prov [] us' m -- inaccessible rhs
344 where m = [L locn [L locn p]]
345
346 -- | Exhaustive for guard matches, is used for guards in pattern bindings and
347 -- in @MultiIf@ expressions.
348 checkGuardMatches :: HsMatchContext Name -- Match context
349 -> GRHSs GhcTc (LHsExpr GhcTc) -- Guarded RHSs
350 -> DsM ()
351 checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
352 dflags <- getDynFlags
353 let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
354 dsMatchContext = DsMatchContext hs_ctx combinedLoc
355 match = L combinedLoc $
356 Match { m_ext = noExt
357 , m_ctxt = hs_ctx
358 , m_pats = []
359 , m_grhss = guards }
360 checkMatches dflags dsMatchContext [] [match]
361 checkGuardMatches _ (XGRHSs _) = panic "checkGuardMatches"
362
363 -- | Check a matchgroup (case, functions, etc.)
364 checkMatches :: DynFlags -> DsMatchContext
365 -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
366 checkMatches dflags ctxt vars matches = do
367 tracePmD "checkMatches" (hang (vcat [ppr ctxt
368 , ppr vars
369 , text "Matches:"])
370 2
371 (vcat (map ppr matches)))
372 mb_pm_res <- tryM $ getResult $ case matches of
373 -- Check EmptyCase separately
374 -- See Note [Checking EmptyCase Expressions]
375 [] | [var] <- vars -> checkEmptyCase' var
376 _normal_match -> checkMatches' vars matches
377 case mb_pm_res of
378 Left _ -> warnPmIters dflags ctxt
379 Right res -> dsPmWarn dflags ctxt res
380
381 -- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
382 -- list of matches. For empty case expressions, use checkEmptyCase' instead.
383 checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
384 checkMatches' vars matches
385 | null matches = panic "checkMatches': EmptyCase"
386 | otherwise = do
387 liftD resetPmIterDs -- set the iter-no to zero
388 missing <- mkInitialUncovered vars
389 tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
390 (prov, rs,us,ds) <- go matches missing
391 return $ PmResult {
392 pmresultProvenance = prov
393 , pmresultRedundant = map hsLMatchToLPats rs
394 , pmresultUncovered = UncoveredPatterns us
395 , pmresultInaccessible = map hsLMatchToLPats ds }
396 where
397 go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
398 -> PmM (Provenance
399 , [LMatch GhcTc (LHsExpr GhcTc)]
400 , Uncovered
401 , [LMatch GhcTc (LHsExpr GhcTc)])
402 go [] missing = return (mempty, [], missing, [])
403 go (m:ms) missing = do
404 tracePm "checMatches': go" (ppr m $$ ppr missing)
405 fam_insts <- liftD dsGetFamInstEnvs
406 (clause, guards) <- liftD $ translateMatch fam_insts m
407 r@(PartialResult prov cs missing' ds)
408 <- runMany (pmcheckI clause guards) missing
409 tracePm "checMatches': go: res" (ppr r)
410 (ms_prov, rs, final_u, is) <- go ms missing'
411 let final_prov = prov `mappend` ms_prov
412 return $ case (cs, ds) of
413 -- useful
414 (Covered, _ ) -> (final_prov, rs, final_u, is)
415 -- redundant
416 (NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
417 -- inaccessible
418 (NotCovered, Diverged ) -> (final_prov, rs, final_u, m:is)
419
420 hsLMatchToLPats :: LMatch id body -> Located [LPat id]
421 hsLMatchToLPats (L l (Match { m_pats = pats })) = L l pats
422 hsLMatchToLPats (L _ (XMatch _)) = panic "checMatches'"
423
424 -- | Check an empty case expression. Since there are no clauses to process, we
425 -- only compute the uncovered set. See Note [Checking EmptyCase Expressions]
426 -- for details.
427 checkEmptyCase' :: Id -> PmM PmResult
428 checkEmptyCase' var = do
429 tm_css <- map toComplex . bagToList <$> liftD getTmCsDs
430 case tmOracle initialTmState tm_css of
431 Just tm_state -> do
432 ty_css <- liftD getDictsDs
433 fam_insts <- liftD dsGetFamInstEnvs
434 mb_candidates <- inhabitationCandidates fam_insts (idType var)
435 case mb_candidates of
436 -- Inhabitation checking failed / the type is trivially inhabited
437 Left ty -> return (uncoveredWithTy ty)
438
439 -- A list of inhabitant candidates is available: Check for each
440 -- one for the satisfiability of the constraints it gives rise to.
441 Right candidates -> do
442 missing_m <- flip concatMapM candidates $ \(va,tm_ct,ty_cs) -> do
443 let all_ty_cs = unionBags ty_cs ty_css
444 sat_ty <- tyOracle all_ty_cs
445 return $ case (sat_ty, tmOracle tm_state (tm_ct:tm_css)) of
446 (True, Just tm_state') -> [(va, all_ty_cs, tm_state')]
447 _non_sat -> []
448 let mkValVec (va,all_ty_cs,tm_state')
449 = ValVec [va] (MkDelta all_ty_cs tm_state')
450 uncovered = UncoveredPatterns (map mkValVec missing_m)
451 return $ if null missing_m
452 then emptyPmResult
453 else PmResult FromBuiltin [] uncovered []
454 Nothing -> return emptyPmResult
455
456 -- | Returns 'True' if the argument 'Type' is a fully saturated application of
457 -- a closed type constructor.
458 --
459 -- Closed type constructors are those with a fixed right hand side, as
460 -- opposed to e.g. associated types. These are of particular interest for
461 -- pattern-match coverage checking, because GHC can exhaustively consider all
462 -- possible forms that values of a closed type can take on.
463 --
464 -- Note that this function is intended to be used to check types of value-level
465 -- patterns, so as a consequence, the 'Type' supplied as an argument to this
466 -- function should be of kind @Type@.
467 pmIsClosedType :: Type -> Bool
468 pmIsClosedType ty
469 = case splitTyConApp_maybe ty of
470 Just (tc, ty_args)
471 | is_algebraic_like tc && not (isFamilyTyCon tc)
472 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
473 _other -> False
474 where
475 -- This returns True for TyCons which /act like/ algebraic types.
476 -- (See "Type#type_classification" for what an algebraic type is.)
477 --
478 -- This is qualified with \"like\" because of a particular special
479 -- case: TYPE (the underlyind kind behind Type, among others). TYPE
480 -- is conceptually a datatype (and thus algebraic), but in practice it is
481 -- a primitive builtin type, so we must check for it specially.
482 --
483 -- NB: it makes sense to think of TYPE as a closed type in a value-level,
484 -- pattern-matching context. However, at the kind level, TYPE is certainly
485 -- not closed! Since this function is specifically tailored towards pattern
486 -- matching, however, it's OK to label TYPE as closed.
487 is_algebraic_like :: TyCon -> Bool
488 is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon
489
490 pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
491 -- ^ Get rid of *outermost* (or toplevel)
492 -- * type function redex
493 -- * data family redex
494 -- * newtypes
495 --
496 -- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
497 -- coercion, it returns useful information for issuing pattern matching
498 -- warnings. See Note [Type normalisation for EmptyCase] for details.
499 pmTopNormaliseType_maybe env typ
500 = do ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ
501 return (eq_src_ty ty (typ : ty_f [ty]), tm_f [], ty)
502 where
503 -- Find the first type in the sequence of rewrites that is a data type,
504 -- newtype, or a data family application (not the representation tycon!).
505 -- This is the one that is equal (in source Haskell) to the initial type.
506 -- If none is found in the list, then all of them are type family
507 -- applications, so we simply return the last one, which is the *simplest*.
508 eq_src_ty :: Type -> [Type] -> Type
509 eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys)
510
511 is_closed_or_data_family :: Type -> Bool
512 is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty
513
514 -- For efficiency, represent both lists as difference lists.
515 -- comb performs the concatenation, for both lists.
516 comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2)
517
518 stepper = newTypeStepper `composeSteppers` tyFamStepper
519
520 -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
521 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
522 newTypeStepper :: NormaliseStepper ([Type] -> [Type],[DataCon] -> [DataCon])
523 newTypeStepper rec_nts tc tys
524 | Just (ty', _co) <- instNewTyCon_maybe tc tys
525 = case checkRecTc rec_nts tc of
526 Just rec_nts' -> let tyf = ((TyConApp tc tys):)
527 tmf = ((tyConSingleDataCon tc):)
528 in NS_Step rec_nts' ty' (tyf, tmf)
529 Nothing -> NS_Abort
530 | otherwise
531 = NS_Done
532
533 tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
534 tyFamStepper rec_nts tc tys -- Try to step a type/data family
535 = let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in
536 -- NB: It's OK to use normaliseTcArgs here instead of
537 -- normalise_tc_args (which takes the LiftingContext described
538 -- in Note [Normalising types]) because the reduceTyFamApp below
539 -- works only at top level. We'll never recur in this function
540 -- after reducing the kind of a bound tyvar.
541
542 case reduceTyFamApp_maybe env Representational tc ntys of
543 Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
544 _ -> NS_Done
545
546 {- Note [Type normalisation for EmptyCase]
547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
548 EmptyCase is an exception for pattern matching, since it is strict. This means
549 that it boils down to checking whether the type of the scrutinee is inhabited.
550 Function pmTopNormaliseType_maybe gets rid of the outermost type function/data
551 family redex and newtypes, in search of an algebraic type constructor, which is
552 easier to check for inhabitation.
553
554 It returns 3 results instead of one, because there are 2 subtle points:
555 1. Newtypes are isomorphic to the underlying type in core but not in the source
556 language,
557 2. The representational data family tycon is used internally but should not be
558 shown to the user
559
560 Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
561 (a) src_ty is the rewritten type which we can show to the user. That is, the
562 type we get if we rewrite type families but not data families or
563 newtypes.
564 (b) dcs is the list of data constructors "skipped", every time we normalise a
565 newtype to it's core representation, we keep track of the source data
566 constructor.
567 (c) core_ty is the rewritten type. That is,
568 pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty)
569 implies
570 topNormaliseType_maybe env ty = Just (co, core_ty)
571 for some coercion co.
572
573 To see how all cases come into play, consider the following example:
574
575 data family T a :: *
576 data instance T Int = T1 | T2 Bool
577 -- Which gives rise to FC:
578 -- data T a
579 -- data R:TInt = T1 | T2 Bool
580 -- axiom ax_ti : T Int ~R R:TInt
581
582 newtype G1 = MkG1 (T Int)
583 newtype G2 = MkG2 G1
584
585 type instance F Int = F Char
586 type instance F Char = G2
587
588 In this case pmTopNormaliseType_maybe env (F Int) results in
589
590 Just (G2, [MkG2,MkG1], R:TInt)
591
592 Which means that in source Haskell:
593 - G2 is equivalent to F Int (in contrast, G1 isn't).
594 - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
595 -}
596
597 -- | Generate all inhabitation candidates for a given type. The result is
598 -- either (Left ty), if the type cannot be reduced to a closed algebraic type
599 -- (or if it's one trivially inhabited, like Int), or (Right candidates), if it
600 -- can. In this case, the candidates are the signature of the tycon, each one
601 -- accompanied by the term- and type- constraints it gives rise to.
602 -- See also Note [Checking EmptyCase Expressions]
603 inhabitationCandidates :: FamInstEnvs -> Type
604 -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
605 inhabitationCandidates fam_insts ty
606 = case pmTopNormaliseType_maybe fam_insts ty of
607 Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
608 Nothing -> alts_to_check ty ty []
609 where
610 -- All these types are trivially inhabited
611 trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
612 , intTyCon, wordTyCon, word8TyCon ]
613
614 -- Note: At the moment we leave all the typing and constraint fields of
615 -- PmCon empty, since we know that they are not gonna be used. Is the
616 -- right-thing-to-do to actually create them, even if they are never used?
617 build_tm :: ValAbs -> [DataCon] -> ValAbs
618 build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e])
619
620 -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
621 alts_to_check :: Type -> Type -> [DataCon]
622 -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
623 alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
624 Just (tc, _)
625 | tc `elem` trivially_inhabited -> case dcs of
626 [] -> return (Left src_ty)
627 (_:_) -> do var <- liftD $ mkPmId core_ty
628 let va = build_tm (PmVar var) dcs
629 return $ Right [(va, mkIdEq var, emptyBag)]
630
631 | pmIsClosedType core_ty -> liftD $ do
632 var <- mkPmId core_ty -- it would be wrong to unify x
633 alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
634 return $ Right [(build_tm va dcs, eq, cs) | (va, eq, cs) <- alts]
635 -- For other types conservatively assume that they are inhabited.
636 _other -> return (Left src_ty)
637
638 {- Note [Checking EmptyCase Expressions]
639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
640 Empty case expressions are strict on the scrutinee. That is, `case x of {}`
641 will force argument `x`. Hence, `checkMatches` is not sufficient for checking
642 empty cases, because it assumes that the match is not strict (which is true
643 for all other cases, apart from EmptyCase). This gave rise to #10746. Instead,
644 we do the following:
645
646 1. We normalise the outermost type family redex, data family redex or newtype,
647 using pmTopNormaliseType_maybe (in types/FamInstEnv.hs). This computes 3
648 things:
649 (a) A normalised type src_ty, which is equal to the type of the scrutinee in
650 source Haskell (does not normalise newtypes or data families)
651 (b) The actual normalised type core_ty, which coincides with the result
652 topNormaliseType_maybe. This type is not necessarily equal to the input
653 type in source Haskell. And this is precicely the reason we compute (a)
654 and (c): the reasoning happens with the underlying types, but both the
655 patterns and types we print should respect newtypes and also show the
656 family type constructors and not the representation constructors.
657
658 (c) A list of all newtype data constructors dcs, each one corresponding to a
659 newtype rewrite performed in (b).
660
661 For an example see also Note [Type normalisation for EmptyCase]
662 in types/FamInstEnv.hs.
663
664 2. Function checkEmptyCase' performs the check:
665 - If core_ty is not an algebraic type, then we cannot check for
666 inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming
667 that the type is inhabited.
668 - If core_ty is an algebraic type, then we unfold the scrutinee to all
669 possible constructor patterns, using inhabitationCandidates, and then
670 check each one for constraint satisfiability, same as we for normal
671 pattern match checking.
672
673 %************************************************************************
674 %* *
675 Transform source syntax to *our* syntax
676 %* *
677 %************************************************************************
678 -}
679
680 -- -----------------------------------------------------------------------
681 -- * Utilities
682
683 nullaryConPattern :: ConLike -> Pattern
684 -- Nullary data constructor and nullary type constructor
685 nullaryConPattern con =
686 PmCon { pm_con_con = con, pm_con_arg_tys = []
687 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
688 {-# INLINE nullaryConPattern #-}
689
690 truePattern :: Pattern
691 truePattern = nullaryConPattern (RealDataCon trueDataCon)
692 {-# INLINE truePattern #-}
693
694 -- | A fake guard pattern (True <- _) used to represent cases we cannot handle
695 fake_pat :: Pattern
696 fake_pat = PmGrd { pm_grd_pv = [truePattern]
697 , pm_grd_expr = PmExprOther (EWildPat noExt) }
698 {-# INLINE fake_pat #-}
699
700 -- | Check whether a guard pattern is generated by the checker (unhandled)
701 isFakeGuard :: [Pattern] -> PmExpr -> Bool
702 isFakeGuard [PmCon { pm_con_con = RealDataCon c }] (PmExprOther (EWildPat _))
703 | c == trueDataCon = True
704 | otherwise = False
705 isFakeGuard _pats _e = False
706
707 -- | Generate a `canFail` pattern vector of a specific type
708 mkCanFailPmPat :: Type -> DsM PatVec
709 mkCanFailPmPat ty = do
710 var <- mkPmVar ty
711 return [var, fake_pat]
712
713 vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
714 -- ADT constructor pattern => no existentials, no local constraints
715 vanillaConPattern con arg_tys args =
716 PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
717 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
718 {-# INLINE vanillaConPattern #-}
719
720 -- | Create an empty list pattern of a given type
721 nilPattern :: Type -> Pattern
722 nilPattern ty =
723 PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
724 , pm_con_tvs = [], pm_con_dicts = []
725 , pm_con_args = [] }
726 {-# INLINE nilPattern #-}
727
728 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
729 mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
730 , pm_con_arg_tys = [ty]
731 , pm_con_tvs = [], pm_con_dicts = []
732 , pm_con_args = xs++ys }]
733 {-# INLINE mkListPatVec #-}
734
735 -- | Create a (non-overloaded) literal pattern
736 mkLitPattern :: HsLit GhcTc -> Pattern
737 mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
738 {-# INLINE mkLitPattern #-}
739
740 -- -----------------------------------------------------------------------
741 -- * Transform (Pat Id) into of (PmPat Id)
742
743 translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
744 translatePat fam_insts pat = case pat of
745 WildPat ty -> mkPmVars [ty]
746 VarPat _ id -> return [PmVar (unLoc id)]
747 ParPat _ p -> translatePat fam_insts (unLoc p)
748 LazyPat _ _ -> mkPmVars [hsPatType pat] -- like a variable
749
750 -- ignore strictness annotations for now
751 BangPat _ p -> translatePat fam_insts (unLoc p)
752
753 AsPat _ lid p -> do
754 -- Note [Translating As Patterns]
755 ps <- translatePat fam_insts (unLoc p)
756 let [e] = map vaToPmExpr (coercePatVec ps)
757 g = PmGrd [PmVar (unLoc lid)] e
758 return (ps ++ [g])
759
760 SigPat _ty p -> translatePat fam_insts (unLoc p)
761
762 -- See Note [Translate CoPats]
763 CoPat _ wrapper p ty
764 | isIdHsWrapper wrapper -> translatePat fam_insts p
765 | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p
766 | otherwise -> do
767 ps <- translatePat fam_insts p
768 (xp,xe) <- mkPmId2Forms ty
769 let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
770 return [xp,g]
771
772 -- (n + k) ===> x (True <- x >= k) (n <- x-k)
773 NPlusKPat ty (L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty
774
775 -- (fun -> pat) ===> x (pat <- fun x)
776 ViewPat arg_ty lexpr lpat -> do
777 ps <- translatePat fam_insts (unLoc lpat)
778 -- See Note [Guards and Approximation]
779 case all cantFailPattern ps of
780 True -> do
781 (xp,xe) <- mkPmId2Forms arg_ty
782 let g = mkGuard ps (HsApp noExt lexpr xe)
783 return [xp,g]
784 False -> mkCanFailPmPat arg_ty
785
786 -- list
787 ListPat (ListPatTc ty Nothing) ps -> do
788 foldr (mkListPatVec ty) [nilPattern ty]
789 <$> translatePatVec fam_insts (map unLoc ps)
790
791 -- overloaded list
792 ListPat (ListPatTc _elem_ty (Just (pat_ty, _to_list))) lpats -> do
793 dflags <- getDynFlags
794 if xopt LangExt.RebindableSyntax dflags
795 then mkCanFailPmPat pat_ty
796 else case splitListTyConApp_maybe pat_ty of
797 Just e_ty -> translatePat fam_insts
798 (ListPat (ListPatTc e_ty Nothing) lpats)
799 Nothing -> mkCanFailPmPat pat_ty
800 -- (a) In the presence of RebindableSyntax, we don't know anything about
801 -- `toList`, we should treat `ListPat` as any other view pattern.
802 --
803 -- (b) In the absence of RebindableSyntax,
804 -- - If the pat_ty is `[a]`, then we treat the overloaded list pattern
805 -- as ordinary list pattern. Although we can give an instance
806 -- `IsList [Int]` (more specific than the default `IsList [a]`), in
807 -- practice, we almost never do that. We assume the `_to_list` is
808 -- the `toList` from `instance IsList [a]`.
809 --
810 -- - Otherwise, we treat the `ListPat` as ordinary view pattern.
811 --
812 -- See Trac #14547, especially comment#9 and comment#10.
813 --
814 -- Here we construct CanFailPmPat directly, rather can construct a view
815 -- pattern and do further translation as an optimization, for the reason,
816 -- see Note [Guards and Approximation].
817
818 ConPatOut { pat_con = L _ con
819 , pat_arg_tys = arg_tys
820 , pat_tvs = ex_tvs
821 , pat_dicts = dicts
822 , pat_args = ps } -> do
823 groups <- allCompleteMatches con arg_tys
824 case groups of
825 [] -> mkCanFailPmPat (conLikeResTy con arg_tys)
826 _ -> do
827 args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
828 return [PmCon { pm_con_con = con
829 , pm_con_arg_tys = arg_tys
830 , pm_con_tvs = ex_tvs
831 , pm_con_dicts = dicts
832 , pm_con_args = args }]
833
834 -- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
835 NPat _ (L _ olit) mb_neg _
836 | OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit
837 , isStringTy ty ->
838 foldr (mkListPatVec charTy) [nilPattern charTy] <$>
839 translatePatVec fam_insts
840 (map (LitPat noExt . HsChar src) (unpackFS s))
841 | otherwise -> return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) olit }]
842
843 -- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
844 LitPat _ lit
845 | HsString src s <- lit ->
846 foldr (mkListPatVec charTy) [nilPattern charTy] <$>
847 translatePatVec fam_insts
848 (map (LitPat noExt . HsChar src) (unpackFS s))
849 | otherwise -> return [mkLitPattern lit]
850
851 TuplePat tys ps boxity -> do
852 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
853 let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
854 return [vanillaConPattern tuple_con tys (concat tidy_ps)]
855
856 SumPat ty p alt arity -> do
857 tidy_p <- translatePat fam_insts (unLoc p)
858 let sum_con = RealDataCon (sumDataCon alt arity)
859 return [vanillaConPattern sum_con ty tidy_p]
860
861 -- --------------------------------------------------------------------------
862 -- Not supposed to happen
863 ConPatIn {} -> panic "Check.translatePat: ConPatIn"
864 SplicePat {} -> panic "Check.translatePat: SplicePat"
865 XPat {} -> panic "Check.translatePat: XPat"
866
867 {- Note [Translate Overloaded Literal for Exhaustiveness Checking]
868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
869 The translation of @NPat@ in exhaustiveness checker is a bit different
870 from translation in pattern matcher.
871
872 * In pattern matcher (see `tidyNPat' in deSugar/MatchLit.hs), we
873 translate integral literals to HsIntPrim or HsWordPrim and translate
874 overloaded strings to HsString.
875
876 * In exhaustiveness checker, in `genCaseTmCs1/genCaseTmCs2`, we use
877 `lhsExprToPmExpr` to generate uncovered set. In `hsExprToPmExpr`,
878 however we generate `PmOLit` for HsOverLit, rather than refine
879 `HsOverLit` inside `NPat` to HsIntPrim/HsWordPrim. If we do
880 the same thing in `translatePat` as in `tidyNPat`, the exhaustiveness
881 checker will fail to match the literals patterns correctly. See
882 Trac #14546.
883
884 In Note [Undecidable Equality for Overloaded Literals], we say: "treat
885 overloaded literals that look different as different", but previously we
886 didn't do such things.
887
888 Now, we translate the literal value to match and the literal patterns
889 consistently:
890
891 * For integral literals, we parse both the integral literal value and
892 the patterns as OverLit HsIntegral. For example:
893
894 case 0::Int of
895 0 -> putStrLn "A"
896 1 -> putStrLn "B"
897 _ -> putStrLn "C"
898
899 When checking the exhaustiveness of pattern matching, we translate the 0
900 in value position as PmOLit, but translate the 0 and 1 in pattern position
901 as PmSLit. The inconsistency leads to the failure of eqPmLit to detect the
902 equality and report warning of "Pattern match is redundant" on pattern 0,
903 as reported in Trac #14546. In this patch we remove the specialization of
904 OverLit patterns, and keep the overloaded number literal in pattern as it
905 is to maintain the consistency. We know nothing about the `fromInteger`
906 method (see Note [Undecidable Equality for Overloaded Literals]). Now we
907 can capture the exhaustiveness of pattern 0 and the redundancy of pattern
908 1 and _.
909
910 * For string literals, we parse the string literals as HsString. When
911 OverloadedStrings is enabled, it further be turned as HsOverLit HsIsString.
912 For example:
913
914 case "foo" of
915 "foo" -> putStrLn "A"
916 "bar" -> putStrLn "B"
917 "baz" -> putStrLn "C"
918
919 Previously, the overloaded string values are translated to PmOLit and the
920 non-overloaded string values are translated to PmSLit. However the string
921 patterns, both overloaded and non-overloaded, are translated to list of
922 characters. The inconsistency leads to wrong warnings about redundant and
923 non-exhaustive pattern matching warnings, as reported in Trac #14546.
924
925 In order to catch the redundant pattern in following case:
926
927 case "foo" of
928 ('f':_) -> putStrLn "A"
929 "bar" -> putStrLn "B"
930
931 in this patch, we translate non-overloaded string literals, both in value
932 position and pattern position, as list of characters. For overloaded string
933 literals, we only translate it to list of characters only when it's type
934 is stringTy, since we know nothing about the toString methods. But we know
935 that if two overloaded strings are syntax equal, then they are equal. Then
936 if it's type is not stringTy, we just translate it to PmOLit. We can still
937 capture the exhaustiveness of pattern "foo" and the redundancy of pattern
938 "bar" and "baz" in the following code:
939
940 {-# LANGUAGE OverloadedStrings #-}
941 main = do
942 case "foo" of
943 "foo" -> putStrLn "A"
944 "bar" -> putStrLn "B"
945 "baz" -> putStrLn "C"
946
947 We must ensure that doing the same translation to literal values and patterns
948 in `translatePat` and `hsExprToPmExpr`. The previous inconsistent work led to
949 Trac #14546.
950 -}
951
952 -- | Translate a list of patterns (Note: each pattern is translated
953 -- to a pattern vector but we do not concatenate the results).
954 translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
955 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
956
957 -- | Translate a constructor pattern
958 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
959 -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
960 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
961 = concat <$> translatePatVec fam_insts (map unLoc ps)
962 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
963 = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
964 translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
965 -- Nothing matched. Make up some fresh term variables
966 | null fs = mkPmVars arg_tys
967 -- The data constructor was not defined using record syntax. For the
968 -- pattern to be in record syntax it should be empty (e.g. Just {}).
969 -- So just like the previous case.
970 | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
971 -- Some of the fields appear, in the original order (there may be holes).
972 -- Generate a simple constructor pattern and make up fresh variables for
973 -- the rest of the fields
974 | matched_lbls `subsetOf` orig_lbls
975 = ASSERT(orig_lbls `equalLength` arg_tys)
976 let translateOne (lbl, ty) = case lookup lbl matched_pats of
977 Just p -> translatePat fam_insts p
978 Nothing -> mkPmVars [ty]
979 in concatMapM translateOne (zip orig_lbls arg_tys)
980 -- The fields that appear are not in the correct order. Make up fresh
981 -- variables for all fields and add guards after matching, to force the
982 -- evaluation in the correct order.
983 | otherwise = do
984 arg_var_pats <- mkPmVars arg_tys
985 translated_pats <- forM matched_pats $ \(x,pat) -> do
986 pvec <- translatePat fam_insts pat
987 return (x, pvec)
988
989 let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
990 guards = map (\(name,pvec) -> case lookup name zipped of
991 Just x -> PmGrd pvec (PmExprVar (idName x))
992 Nothing -> panic "translateConPatVec: lookup")
993 translated_pats
994
995 return (arg_var_pats ++ guards)
996 where
997 -- The actual argument types (instantiated)
998 arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
999
1000 -- Some label information
1001 orig_lbls = map flSelector $ conLikeFieldLabels c
1002 matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
1003 | L _ x <- fs]
1004 matched_lbls = [ name | (name, _pat) <- matched_pats ]
1005
1006 subsetOf :: Eq a => [a] -> [a] -> Bool
1007 subsetOf [] _ = True
1008 subsetOf (_:_) [] = False
1009 subsetOf (x:xs) (y:ys)
1010 | x == y = subsetOf xs ys
1011 | otherwise = subsetOf (x:xs) ys
1012
1013 -- Translate a single match
1014 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
1015 -> DsM (PatVec,[PatVec])
1016 translateMatch fam_insts (L _ (Match { m_pats = lpats, m_grhss = grhss })) = do
1017 pats' <- concat <$> translatePatVec fam_insts pats
1018 guards' <- mapM (translateGuards fam_insts) guards
1019 return (pats', guards')
1020 where
1021 extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
1022 extractGuards (L _ (GRHS _ gs _)) = map unLoc gs
1023 extractGuards (L _ (XGRHS _)) = panic "translateMatch"
1024
1025 pats = map unLoc lpats
1026 guards = map extractGuards (grhssGRHSs grhss)
1027 translateMatch _ (L _ (XMatch _)) = panic "translateMatch"
1028
1029 -- -----------------------------------------------------------------------
1030 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
1031
1032 -- | Translate a list of guard statements to a pattern vector
1033 translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
1034 translateGuards fam_insts guards = do
1035 all_guards <- concat <$> mapM (translateGuard fam_insts) guards
1036 return (replace_unhandled all_guards)
1037 -- It should have been (return all_guards) but it is too expressive.
1038 -- Since the term oracle does not handle all constraints we generate,
1039 -- we (hackily) replace all constraints the oracle cannot handle with a
1040 -- single one (we need to know if there is a possibility of falure).
1041 -- See Note [Guards and Approximation] for all guard-related approximations
1042 -- we implement.
1043 where
1044 replace_unhandled :: PatVec -> PatVec
1045 replace_unhandled gv
1046 | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
1047 | otherwise = gv
1048
1049 any_unhandled :: PatVec -> Bool
1050 any_unhandled gv = any (not . shouldKeep) gv
1051
1052 shouldKeep :: Pattern -> Bool
1053 shouldKeep p
1054 | PmVar {} <- p = True
1055 | PmCon {} <- p = singleConstructor (pm_con_con p)
1056 && all shouldKeep (pm_con_args p)
1057 shouldKeep (PmGrd pv e)
1058 | all shouldKeep pv = True
1059 | isNotPmExprOther e = True -- expensive but we want it
1060 shouldKeep _other_pat = False -- let the rest..
1061
1062 -- | Check whether a pattern can fail to match
1063 cantFailPattern :: Pattern -> Bool
1064 cantFailPattern p
1065 | PmVar {} <- p = True
1066 | PmCon {} <- p = singleConstructor (pm_con_con p)
1067 && all cantFailPattern (pm_con_args p)
1068 cantFailPattern (PmGrd pv _e)
1069 = all cantFailPattern pv
1070 cantFailPattern _ = False
1071
1072 -- | Translate a guard statement to Pattern
1073 translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
1074 translateGuard fam_insts guard = case guard of
1075 BodyStmt _ e _ _ -> translateBoolGuard e
1076 LetStmt _ binds -> translateLet (unLoc binds)
1077 BindStmt _ p e _ _ -> translateBind fam_insts p e
1078 LastStmt {} -> panic "translateGuard LastStmt"
1079 ParStmt {} -> panic "translateGuard ParStmt"
1080 TransStmt {} -> panic "translateGuard TransStmt"
1081 RecStmt {} -> panic "translateGuard RecStmt"
1082 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
1083 XStmtLR {} -> panic "translateGuard RecStmt"
1084
1085 -- | Translate let-bindings
1086 translateLet :: HsLocalBinds GhcTc -> DsM PatVec
1087 translateLet _binds = return []
1088
1089 -- | Translate a pattern guard
1090 translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
1091 translateBind fam_insts (L _ p) e = do
1092 ps <- translatePat fam_insts p
1093 return [mkGuard ps (unLoc e)]
1094
1095 -- | Translate a boolean guard
1096 translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
1097 translateBoolGuard e
1098 | isJust (isTrueLHsExpr e) = return []
1099 -- The formal thing to do would be to generate (True <- True)
1100 -- but it is trivial to solve so instead we give back an empty
1101 -- PatVec for efficiency
1102 | otherwise = return [mkGuard [truePattern] (unLoc e)]
1103
1104 {- Note [Guards and Approximation]
1105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1106 Even if the algorithm is really expressive, the term oracle we use is not.
1107 Hence, several features are not translated *properly* but we approximate.
1108 The list includes:
1109
1110 1. View Patterns
1111 ----------------
1112 A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
1113 oracle does not handle function applications so we know that the generated
1114 constraints will not be handled at the end. Hence, we distinguish between two
1115 cases:
1116 a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
1117 thing*.
1118 b) Pattern @p@ can fail. This means that when checking the guard, we will
1119 generate several cases, with no useful information. E.g.:
1120
1121 h (f -> [a,b]) = ...
1122 h x ([a,b] <- f x) = ...
1123
1124 uncovered set = { [x |> { False ~ (f x ~ []) }]
1125 , [x |> { False ~ (f x ~ (t1:[])) }]
1126 , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
1127
1128 So we have two problems:
1129 1) Since we do not print the constraints in the general case (they may
1130 be too many), the warning will look like this:
1131
1132 Pattern match(es) are non-exhaustive
1133 In an equation for `h':
1134 Patterns not matched:
1135 _
1136 _
1137 _
1138 Which is not short and not more useful than a single underscore.
1139 2) The size of the uncovered set increases a lot, without gaining more
1140 expressivity in our warnings.
1141
1142 Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
1143 @fake_pat@: @True <- _@. That is, we record that there is a possibility
1144 of failure but we minimize it to a True/False. This generates a single
1145 warning and much smaller uncovered sets.
1146
1147 2. Overloaded Lists
1148 -------------------
1149 An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
1150 problem is exactly like above, as its solution. For future reference, the code
1151 below is the *right thing to do*:
1152
1153 ListPat (ListPatTc elem_ty (Just (pat_ty, _to_list))) lpats
1154 otherwise -> do
1155 (xp, xe) <- mkPmId2Forms pat_ty
1156 ps <- translatePatVec (map unLoc lpats)
1157 let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
1158 g = mkGuard pats (HsApp (noLoc to_list) xe)
1159 return [xp,g]
1160
1161 3. Overloaded Literals
1162 ----------------------
1163 The case with literals is a bit different. a literal @l@ should be translated
1164 to @x (True <- x == from l)@. Since we want to have better warnings for
1165 overloaded literals as it is a very common feature, we treat them differently.
1166 They are mainly covered in Note [Undecidable Equality for Overloaded Literals]
1167 in PmExpr.
1168
1169 4. N+K Patterns & Pattern Synonyms
1170 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1171 An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
1172 Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
1173 and has two possible outcomes. Hence, there is no benefit in using a dummy and
1174 we implement the proper thing. Pattern synonyms are simply not implemented yet.
1175 Hence, to be conservative, we generate a dummy pattern, assuming that the
1176 pattern can fail.
1177
1178 5. Actual Guards
1179 ----------------
1180 During translation, boolean guards and pattern guards are translated properly.
1181 Let bindings though are omitted by function @translateLet@. Since they are lazy
1182 bindings, we do not actually want to generate a (strict) equality (like we do
1183 in the pattern bind case). Hence, we safely drop them.
1184
1185 Additionally, top-level guard translation (performed by @translateGuards@)
1186 replaces guards that cannot be reasoned about (like the ones we described in
1187 1-4) with a single @fake_pat@ to record the possibility of failure to match.
1188
1189 Note [Translate CoPats]
1190 ~~~~~~~~~~~~~~~~~~~~~~~
1191 The pattern match checker did not know how to handle coerced patterns `CoPat`
1192 efficiently, which gave rise to #11276. The original approach translated
1193 `CoPat`s:
1194
1195 pat |> co ===> x (pat <- (e |> co))
1196
1197 Instead, we now check whether the coercion is a hole or if it is just refl, in
1198 which case we can drop it. Unfortunately, data families generate useful
1199 coercions so guards are still generated in these cases and checking data
1200 families is not really efficient.
1201
1202 %************************************************************************
1203 %* *
1204 Utilities for Pattern Match Checking
1205 %* *
1206 %************************************************************************
1207 -}
1208
1209 -- ----------------------------------------------------------------------------
1210 -- * Basic utilities
1211
1212 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
1213 -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
1214 pmPatType :: PmPat p -> Type
1215 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
1216 = conLikeResTy con tys
1217 pmPatType (PmVar { pm_var_id = x }) = idType x
1218 pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
1219 pmPatType (PmNLit { pm_lit_id = x }) = idType x
1220 pmPatType (PmGrd { pm_grd_pv = pv })
1221 = ASSERT(patVecArity pv == 1) (pmPatType p)
1222 where Just p = find ((==1) . patternArity) pv
1223
1224 -- | Generate a value abstraction for a given constructor (generate
1225 -- fresh variables of the appropriate type for arguments)
1226 mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
1227 -- * x :: T tys, where T is an algebraic data type
1228 -- NB: in the case of a data family, T is the *representation* TyCon
1229 -- e.g. data instance T (a,b) = T1 a b
1230 -- leads to
1231 -- data TPair a b = T1 a b -- The "representation" type
1232 -- It is TPair, not T, that is given to mkOneConFull
1233 --
1234 -- * 'con' K is a constructor of data type T
1235 --
1236 -- After instantiating the universal tyvars of K we get
1237 -- K tys :: forall bs. Q => s1 .. sn -> T tys
1238 --
1239 -- Results: ValAbs: K (y1::s1) .. (yn::sn)
1240 -- ComplexEq: x ~ K y1..yn
1241 -- [EvVar]: Q
1242 mkOneConFull x con = do
1243 let res_ty = idType x
1244 (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
1245 = conLikeFullSig con
1246 tc_args = tyConAppArgs res_ty
1247 subst1 = case con of
1248 RealDataCon {} -> zipTvSubst univ_tvs tc_args
1249 PatSynCon {} -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty)
1250 -- See Note [Pattern synonym result type] in PatSyn
1251
1252 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
1253
1254 -- Fresh term variables (VAs) as arguments to the constructor
1255 arguments <- mapM mkPmVar (substTys subst arg_tys)
1256 -- All constraints bound by the constructor (alpha-renamed)
1257 let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
1258 evvars <- mapM (nameType "pm") theta_cs
1259 let con_abs = PmCon { pm_con_con = con
1260 , pm_con_arg_tys = tc_args
1261 , pm_con_tvs = ex_tvs'
1262 , pm_con_dicts = evvars
1263 , pm_con_args = arguments }
1264 return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
1265
1266 -- ----------------------------------------------------------------------------
1267 -- * More smart constructors and fresh variable generation
1268
1269 -- | Create a guard pattern
1270 mkGuard :: PatVec -> HsExpr GhcTc -> Pattern
1271 mkGuard pv e
1272 | all cantFailPattern pv = PmGrd pv expr
1273 | PmExprOther {} <- expr = fake_pat
1274 | otherwise = PmGrd pv expr
1275 where
1276 expr = hsExprToPmExpr e
1277
1278 -- | Create a term equality of the form: `(False ~ (x ~ lit))`
1279 mkNegEq :: Id -> PmLit -> ComplexEq
1280 mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
1281 {-# INLINE mkNegEq #-}
1282
1283 -- | Create a term equality of the form: `(x ~ lit)`
1284 mkPosEq :: Id -> PmLit -> ComplexEq
1285 mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
1286 {-# INLINE mkPosEq #-}
1287
1288 -- | Create a term equality of the form: `(x ~ x)`
1289 -- (always discharged by the term oracle)
1290 mkIdEq :: Id -> ComplexEq
1291 mkIdEq x = (PmExprVar name, PmExprVar name)
1292 where name = idName x
1293 {-# INLINE mkIdEq #-}
1294
1295 -- | Generate a variable pattern of a given type
1296 mkPmVar :: Type -> DsM (PmPat p)
1297 mkPmVar ty = PmVar <$> mkPmId ty
1298 {-# INLINE mkPmVar #-}
1299
1300 -- | Generate many variable patterns, given a list of types
1301 mkPmVars :: [Type] -> DsM PatVec
1302 mkPmVars tys = mapM mkPmVar tys
1303 {-# INLINE mkPmVars #-}
1304
1305 -- | Generate a fresh `Id` of a given type
1306 mkPmId :: Type -> DsM Id
1307 mkPmId ty = getUniqueM >>= \unique ->
1308 let occname = mkVarOccFS $ fsLit "$pm"
1309 name = mkInternalName unique occname noSrcSpan
1310 in return (mkLocalId name ty)
1311
1312 -- | Generate a fresh term variable of a given and return it in two forms:
1313 -- * A variable pattern
1314 -- * A variable expression
1315 mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
1316 mkPmId2Forms ty = do
1317 x <- mkPmId ty
1318 return (PmVar x, noLoc (HsVar noExt (noLoc x)))
1319
1320 -- ----------------------------------------------------------------------------
1321 -- * Converting between Value Abstractions, Patterns and PmExpr
1322
1323 -- | Convert a value abstraction an expression
1324 vaToPmExpr :: ValAbs -> PmExpr
1325 vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
1326 = PmExprCon c (map vaToPmExpr ps)
1327 vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
1328 vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
1329 vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
1330
1331 -- | Convert a pattern vector to a list of value abstractions by dropping the
1332 -- guards (See Note [Translating As Patterns])
1333 coercePatVec :: PatVec -> [ValAbs]
1334 coercePatVec pv = concatMap coercePmPat pv
1335
1336 -- | Convert a pattern to a list of value abstractions (will be either an empty
1337 -- list if the pattern is a guard pattern, or a singleton list in all other
1338 -- cases) by dropping the guards (See Note [Translating As Patterns])
1339 coercePmPat :: Pattern -> [ValAbs]
1340 coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
1341 coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
1342 coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
1343 , pm_con_tvs = tvs, pm_con_dicts = dicts
1344 , pm_con_args = args })
1345 = [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
1346 , pm_con_tvs = tvs, pm_con_dicts = dicts
1347 , pm_con_args = coercePatVec args }]
1348 coercePmPat (PmGrd {}) = [] -- drop the guards
1349
1350 -- | Check whether a data constructor is the only way to construct
1351 -- a data type.
1352 singleConstructor :: ConLike -> Bool
1353 singleConstructor (RealDataCon dc) =
1354 case tyConDataCons (dataConTyCon dc) of
1355 [_] -> True
1356 _ -> False
1357 singleConstructor _ = False
1358
1359 -- | For a given conlike, finds all the sets of patterns which could
1360 -- be relevant to that conlike by consulting the result type.
1361 --
1362 -- These come from two places.
1363 -- 1. From data constructors defined with the result type constructor.
1364 -- 2. From `COMPLETE` pragmas which have the same type as the result
1365 -- type constructor. Note that we only use `COMPLETE` pragmas
1366 -- *all* of whose pattern types match. See #14135
1367 allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
1368 allCompleteMatches cl tys = do
1369 let fam = case cl of
1370 RealDataCon dc ->
1371 [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
1372 PatSynCon _ -> []
1373 ty = conLikeResTy cl tys
1374 pragmas <- case splitTyConApp_maybe ty of
1375 Just (tc, _) -> dsGetCompleteMatches tc
1376 Nothing -> return []
1377 let fams cm = (FromComplete,) <$>
1378 mapM dsLookupConLike (completeMatchConLikes cm)
1379 from_pragma <- filter (\(_,m) -> isValidCompleteMatch ty m) <$>
1380 mapM fams pragmas
1381 let final_groups = fam ++ from_pragma
1382 return final_groups
1383 where
1384 -- Check that all the pattern synonym return types in a `COMPLETE`
1385 -- pragma subsume the type we're matching.
1386 -- See Note [Filtering out non-matching COMPLETE sets]
1387 isValidCompleteMatch :: Type -> [ConLike] -> Bool
1388 isValidCompleteMatch ty = all go
1389 where
1390 go (RealDataCon {}) = True
1391 go (PatSynCon psc) = isJust $ flip tcMatchTy ty $ patSynResTy
1392 $ patSynSig psc
1393
1394 patSynResTy (_, _, _, _, _, res_ty) = res_ty
1395
1396 {-
1397 Note [Filtering out non-matching COMPLETE sets]
1398 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1399 Currently, conlikes in a COMPLETE set are simply grouped by the
1400 type constructor heading the return type. This is nice and simple, but it does
1401 mean that there are scenarios when a COMPLETE set might be incompatible with
1402 the type of a scrutinee. For instance, consider (from #14135):
1403
1404 data Foo a = Foo1 a | Foo2 a
1405
1406 pattern MyFoo2 :: Int -> Foo Int
1407 pattern MyFoo2 i = Foo2 i
1408
1409 {-# COMPLETE Foo1, MyFoo2 #-}
1410
1411 f :: Foo a -> a
1412 f (Foo1 x) = x
1413
1414 `f` has an incomplete pattern-match, so when choosing which constructors to
1415 report as unmatched in a warning, GHC must choose between the original set of
1416 data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe
1417 that GHC shouldn't even consider the COMPLETE set as a possibility: the return
1418 type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since
1419 there's no substitution `s` such that s(Foo Int) = Foo a.
1420
1421 To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern
1422 synonym constructor's return type matches the type of the scrutinee, and if one
1423 doesn't, then we remove the whole COMPLETE set from consideration.
1424
1425 One might wonder why GHC only checks /pattern synonym/ constructors, and not
1426 /data/ constructors as well. The reason is because that the type of a
1427 GADT constructor very well may not match the type of a scrutinee, and that's
1428 OK. Consider this example (from #14059):
1429
1430 data SBool (z :: Bool) where
1431 SFalse :: SBool False
1432 STrue :: SBool True
1433
1434 pattern STooGoodToBeTrue :: forall (z :: Bool). ()
1435 => z ~ True
1436 => SBool z
1437 pattern STooGoodToBeTrue = STrue
1438 {-# COMPLETE SFalse, STooGoodToBeTrue #-}
1439
1440 wobble :: SBool z -> Bool
1441 wobble STooGoodToBeTrue = True
1442
1443 In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse
1444 should be matched against, even though its type, SBool False, does not match
1445 the scrutinee type, SBool z.
1446 -}
1447
1448 -- -----------------------------------------------------------------------
1449 -- * Types and constraints
1450
1451 newEvVar :: Name -> Type -> EvVar
1452 newEvVar name ty = mkLocalId name ty
1453
1454 nameType :: String -> Type -> DsM EvVar
1455 nameType name ty = do
1456 unique <- getUniqueM
1457 let occname = mkVarOccFS (fsLit (name++"_"++show unique))
1458 idname = mkInternalName unique occname noSrcSpan
1459 return (newEvVar idname ty)
1460
1461 {-
1462 %************************************************************************
1463 %* *
1464 The type oracle
1465 %* *
1466 %************************************************************************
1467 -}
1468
1469 -- | Check whether a set of type constraints is satisfiable.
1470 tyOracle :: Bag EvVar -> PmM Bool
1471 tyOracle evs
1472 = liftD $
1473 do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
1474 ; case res of
1475 Just sat -> return sat
1476 Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
1477
1478 {-
1479 %************************************************************************
1480 %* *
1481 Sanity Checks
1482 %* *
1483 %************************************************************************
1484 -}
1485
1486 -- | The arity of a pattern/pattern vector is the
1487 -- number of top-level patterns that are not guards
1488 type PmArity = Int
1489
1490 -- | Compute the arity of a pattern vector
1491 patVecArity :: PatVec -> PmArity
1492 patVecArity = sum . map patternArity
1493
1494 -- | Compute the arity of a pattern
1495 patternArity :: Pattern -> PmArity
1496 patternArity (PmGrd {}) = 0
1497 patternArity _other_pat = 1
1498
1499 {-
1500 %************************************************************************
1501 %* *
1502 Heart of the algorithm: Function pmcheck
1503 %* *
1504 %************************************************************************
1505
1506 Main functions are:
1507
1508 * mkInitialUncovered :: [Id] -> PmM Uncovered
1509
1510 Generates the initial uncovered set. Term and type constraints in scope
1511 are checked, if they are inconsistent, the set is empty, otherwise, the
1512 set contains only a vector of variables with the constraints in scope.
1513
1514 * pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1515
1516 Checks redundancy, coverage and inaccessibility, using auxilary functions
1517 `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
1518 common in all three checks (see paper) and calls `pmcheckGuards` when the
1519 whole clause is checked, or `pmcheckHd` when the pattern vector does not
1520 start with a guard.
1521
1522 * pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1523
1524 Processes the guards.
1525
1526 * pmcheckHd :: Pattern -> PatVec -> [PatVec]
1527 -> ValAbs -> ValVec -> PmM PartialResult
1528
1529 Worker: This function implements functions `covered`, `uncovered` and
1530 `divergent` from the paper at once. Slightly different from the paper because
1531 it does not even produce the covered and uncovered sets. Since we only care
1532 about whether a clause covers SOMETHING or if it may forces ANY argument, we
1533 only store a boolean in both cases, for efficiency.
1534 -}
1535
1536 -- | Lift a pattern matching action from a single value vector abstration to a
1537 -- value set abstraction, but calling it on every vector and the combining the
1538 -- results.
1539 runMany :: (ValVec -> PmM PartialResult) -> (Uncovered -> PmM PartialResult)
1540 runMany _ [] = return mempty
1541 runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms
1542
1543 -- | Generate the initial uncovered set. It initializes the
1544 -- delta with all term and type constraints in scope.
1545 mkInitialUncovered :: [Id] -> PmM Uncovered
1546 mkInitialUncovered vars = do
1547 ty_cs <- liftD getDictsDs
1548 tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
1549 sat_ty <- tyOracle ty_cs
1550 let initTyCs = if sat_ty then ty_cs else emptyBag
1551 initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
1552 patterns = map PmVar vars
1553 -- If any of the term/type constraints are non
1554 -- satisfiable then return with the initialTmState. See #12957
1555 return [ValVec patterns (MkDelta initTyCs initTmState)]
1556
1557 -- | Increase the counter for elapsed algorithm iterations, check that the
1558 -- limit is not exceeded and call `pmcheck`
1559 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1560 pmcheckI ps guards vva = do
1561 n <- liftD incrCheckPmIterDs
1562 tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
1563 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1564 $$ pprValVecDebug vva)
1565 res <- pmcheck ps guards vva
1566 tracePm "pmCheckResult:" (ppr res)
1567 return res
1568 {-# INLINE pmcheckI #-}
1569
1570 -- | Increase the counter for elapsed algorithm iterations, check that the
1571 -- limit is not exceeded and call `pmcheckGuards`
1572 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
1573 pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
1574 {-# INLINE pmcheckGuardsI #-}
1575
1576 -- | Increase the counter for elapsed algorithm iterations, check that the
1577 -- limit is not exceeded and call `pmcheckHd`
1578 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1579 -> PmM PartialResult
1580 pmcheckHdI p ps guards va vva = do
1581 n <- liftD incrCheckPmIterDs
1582 tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
1583 $$ pprPatVec ps
1584 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1585 $$ pprPmPatDebug va
1586 $$ pprValVecDebug vva)
1587
1588 res <- pmcheckHd p ps guards va vva
1589 tracePm "pmCheckHdI: res" (ppr res)
1590 return res
1591 {-# INLINE pmcheckHdI #-}
1592
1593 -- | Matching function: Check simultaneously a clause (takes separately the
1594 -- patterns and the list of guards) for exhaustiveness, redundancy and
1595 -- inaccessibility.
1596 pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1597 pmcheck [] guards vva@(ValVec [] _)
1598 | null guards = return $ mempty { presultCovered = Covered }
1599 | otherwise = pmcheckGuardsI guards vva
1600
1601 -- Guard
1602 pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta)
1603 -- short-circuit if the guard pattern is useless.
1604 -- we just have two possible outcomes: fail here or match and recurse
1605 -- none of the two contains any useful information about the failure
1606 -- though. So just have these two cases but do not do all the boilerplate
1607 | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
1608 | otherwise = do
1609 y <- liftD $ mkPmId (pmPatType p)
1610 let tm_state = extendSubst y e (delta_tm_cs delta)
1611 delta' = delta { delta_tm_cs = tm_state }
1612 utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
1613
1614 pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
1615 pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
1616
1617 pmcheck (p:ps) guards (ValVec (va:vva) delta)
1618 = pmcheckHdI p ps guards va (ValVec vva delta)
1619
1620 -- | Check the list of guards
1621 pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1622 pmcheckGuards [] vva = return (usimple [vva])
1623 pmcheckGuards (gv:gvs) vva = do
1624 (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva
1625 (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
1626 return $ PartialResult (prov1 `mappend` prov2)
1627 (cs `mappend` css)
1628 vsas
1629 (ds `mappend` dss)
1630
1631 -- | Worker function: Implements all cases described in the paper for all three
1632 -- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
1633 -- cases which are handled by `pmcheck`
1634 pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1635 -> PmM PartialResult
1636
1637 -- Var
1638 pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
1639 | Just tm_state <- solveOneEq (delta_tm_cs delta)
1640 (PmExprVar (idName x), vaToPmExpr va)
1641 = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
1642 | otherwise = return mempty
1643
1644 -- ConCon
1645 pmcheckHd ( p@(PmCon { pm_con_con = c1, pm_con_tvs = ex_tvs1
1646 , pm_con_args = args1})) ps guards
1647 (va@(PmCon { pm_con_con = c2, pm_con_tvs = ex_tvs2
1648 , pm_con_args = args2})) (ValVec vva delta)
1649 | c1 /= c2 =
1650 return (usimple [ValVec (va:vva) delta])
1651 | otherwise = do
1652 let to_evvar tv1 tv2 = nameType "pmConCon" $
1653 mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
1654 mb_to_evvar tv1 tv2
1655 -- If we have identical constructors but different existential
1656 -- tyvars, then generate extra equality constraints to ensure the
1657 -- existential tyvars.
1658 -- See Note [Coverage checking and existential tyvars].
1659 | tv1 == tv2 = pure Nothing
1660 | otherwise = Just <$> to_evvar tv1 tv2
1661 evvars <- (listToBag . catMaybes) <$>
1662 ASSERT(ex_tvs1 `equalLength` ex_tvs2)
1663 liftD (zipWithM mb_to_evvar ex_tvs1 ex_tvs2)
1664 let delta' = delta { delta_ty_cs = evvars `unionBags` delta_ty_cs delta }
1665 kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
1666 <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta')
1667
1668 -- LitLit
1669 pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
1670 case eqPmLit l1 l2 of
1671 True -> ucon va <$> pmcheckI ps guards vva
1672 False -> return $ ucon va (usimple [vva])
1673
1674 -- ConVar
1675 pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
1676 ps guards
1677 (PmVar x) (ValVec vva delta) = do
1678 (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
1679
1680 cons_cs <- mapM (liftD . mkOneConFull x) complete_match
1681
1682 inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
1683 let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
1684 sat_ty <- if isEmptyBag ty_cs then return True
1685 else tyOracle ty_state
1686 return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
1687 (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
1688 _ty_or_tm_failed -> []
1689
1690 set_provenance prov .
1691 force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1692 runMany (pmcheckI (p:ps) guards) inst_vsa
1693
1694 -- LitVar
1695 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
1696 = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1697 mkUnion non_matched <$>
1698 case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
1699 Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
1700 ValVec vva (delta {delta_tm_cs = tm_state})
1701 Nothing -> return mempty
1702 where
1703 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1704 = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
1705 | otherwise = []
1706
1707 non_matched = usimple us
1708
1709 -- LitNLit
1710 pmcheckHd (p@(PmLit l)) ps guards
1711 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
1712 | all (not . eqPmLit l) lits
1713 , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
1714 -- Both guards check the same so it would be sufficient to have only
1715 -- the second one. Nevertheless, it is much cheaper to check whether
1716 -- the literal is in the list so we check it first, to avoid calling
1717 -- the term oracle (`solveOneEq`) if possible
1718 = mkUnion non_matched <$>
1719 pmcheckHdI p ps guards (PmLit l)
1720 (ValVec vva (delta { delta_tm_cs = tm_state }))
1721 | otherwise = return non_matched
1722 where
1723 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1724 = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
1725 | otherwise = []
1726
1727 non_matched = usimple us
1728
1729 -- ----------------------------------------------------------------------------
1730 -- The following three can happen only in cases like #322 where constructors
1731 -- and overloaded literals appear in the same match. The general strategy is
1732 -- to replace the literal (positive/negative) by a variable and recurse. The
1733 -- fact that the variable is equal to the literal is recorded in `delta` so
1734 -- no information is lost
1735
1736 -- LitCon
1737 pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
1738 = do y <- liftD $ mkPmId (pmPatType va)
1739 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1740 delta' = delta { delta_tm_cs = tm_state }
1741 pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
1742
1743 -- ConLit
1744 pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
1745 = do y <- liftD $ mkPmId (pmPatType p)
1746 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1747 delta' = delta { delta_tm_cs = tm_state }
1748 pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
1749
1750 -- ConNLit
1751 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
1752 = pmcheckHdI p ps guards (PmVar x) vva
1753
1754 -- Impossible: handled by pmcheck
1755 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
1756
1757 {-
1758 Note [Coverage checking and existential tyvars]
1759 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1760 GHC's implementation of the pattern-match coverage algorithm (as described in
1761 the GADTs Meet Their Match paper) must take some care to emit enough type
1762 constraints when handling data constructors with exisentially quantified type
1763 variables. To better explain what the challenge is, consider a constructor K
1764 of the form:
1765
1766 K @e_1 ... @e_m ev_1 ... ev_v ty_1 ... ty_n :: T u_1 ... u_p
1767
1768 Where:
1769
1770 * e_1, ..., e_m are the existentially bound type variables.
1771 * ev_1, ..., ev_v are evidence variables, which may inhabit a dictionary type
1772 (e.g., Eq) or an equality constraint (e.g., e_1 ~ Int).
1773 * ty_1, ..., ty_n are the types of K's fields.
1774 * T u_1 ... u_p is the return type, where T is the data type constructor, and
1775 u_1, ..., u_p are the universally quantified type variables.
1776
1777 In the ConVar case, the coverage algorithm will have in hand the constructor
1778 K as well as a pattern variable (pv :: T PV_1 ... PV_p), where PV_1, ..., PV_p
1779 are some types that instantiate u_1, ... u_p. The idea is that we should
1780 substitute PV_1 for u_1, ..., and PV_p for u_p when forming a PmCon (the
1781 mkOneConFull function accomplishes this) and then hand this PmCon off to the
1782 ConCon case.
1783
1784 The presence of existentially quantified type variables adds a significant
1785 wrinkle. We always grab e_1, ..., e_m from the definition of K to begin with,
1786 but we don't want them to appear in the final PmCon, because then
1787 calling (mkOneConFull K) for other pattern variables might reuse the same
1788 existential tyvars, which is certainly wrong.
1789
1790 Previously, GHC's solution to this wrinkle was to always create fresh names
1791 for the existential tyvars and put them into the PmCon. This works well for
1792 many cases, but it can break down if you nest GADT pattern matches in just
1793 the right way. For instance, consider the following program:
1794
1795 data App f a where
1796 App :: f a -> App f (Maybe a)
1797
1798 data Ty a where
1799 TBool :: Ty Bool
1800 TInt :: Ty Int
1801
1802 data T f a where
1803 C :: T Ty (Maybe Bool)
1804
1805 foo :: T f a -> App f a -> ()
1806 foo C (App TBool) = ()
1807
1808 foo is a total program, but with the previous approach to handling existential
1809 tyvars, GHC would mark foo's patterns as non-exhaustive.
1810
1811 When foo is desugared to Core, it looks roughly like so:
1812
1813 foo @f @a (C co1 _co2) (App @a1 _co3 (TBool |> co1)) = ()
1814
1815 (Where `a1` is an existential tyvar.)
1816
1817 That, in turn, is processed by the coverage checker to become:
1818
1819 foo @f @a (C co1 _co2) (App @a1 _co3 (pmvar123 :: f a1))
1820 | TBool <- pmvar123 |> co1
1821 = ()
1822
1823 Note that the type of pmvar123 is `f a1`—this will be important later.
1824
1825 Now, we proceed with coverage-checking as usual. When we come to the
1826 ConVar case for App, we create a fresh variable `a2` to represent its
1827 existential tyvar. At this point, we have the equality constraints
1828 `(a ~ Maybe a2, a ~ Maybe Bool, f ~ Ty)` in scope.
1829
1830 However, when we check the guard, it will use the type of pmvar123, which is
1831 `f a1`. Thus, when considering if pmvar123 can match the constructor TInt,
1832 it will generate the constraint `a1 ~ Int`. This means our final set of
1833 equality constraints would be:
1834
1835 f ~ Ty
1836 a ~ Maybe Bool
1837 a ~ Maybe a2
1838 a1 ~ Int
1839
1840 Which is satisfiable! Freshening the existential tyvar `a` to `a2` doomed us,
1841 because GHC is unable to relate `a2` to `a1`, which really should be the same
1842 tyvar.
1843
1844 Luckily, we can avoid this pitfall. Recall that the ConVar case was where we
1845 generated a PmCon with too-fresh existentials. But after ConVar, we have the
1846 ConCon case, which considers whether each constructor of a particular data type
1847 can be matched on in a particular spot.
1848
1849 In the case of App, when we get to the ConCon case, we will compare our
1850 original App PmCon (from the source program) to the App PmCon created from the
1851 ConVar case. In the former PmCon, we have `a1` in hand, which is exactly the
1852 existential tyvar we want! Thus, we can force `a1` to be the same as `a2` here
1853 by emitting an additional `a1 ~ a2` constraint. Now our final set of equality
1854 constraints will be:
1855
1856 f ~ Ty
1857 a ~ Maybe Bool
1858 a ~ Maybe a2
1859 a1 ~ Int
1860 a1 ~ a2
1861
1862 Which is unsatisfiable, as we desired, since we now have that
1863 Int ~ a1 ~ a2 ~ Bool.
1864
1865 In general, App might have more than one constructor, in which case we
1866 couldn't reuse the existential tyvar for App for a different constructor. This
1867 means that we can only use this trick in ConCon when the constructors are the
1868 same. But this is fine, since this is the only scenario where this situation
1869 arises in the first place!
1870 -}
1871
1872 -- ----------------------------------------------------------------------------
1873 -- * Utilities for main checking
1874
1875 updateVsa :: (ValSetAbs -> ValSetAbs) -> (PartialResult -> PartialResult)
1876 updateVsa f p@(PartialResult { presultUncovered = old })
1877 = p { presultUncovered = f old }
1878
1879
1880 -- | Initialise with default values for covering and divergent information.
1881 usimple :: ValSetAbs -> PartialResult
1882 usimple vsa = mempty { presultUncovered = vsa }
1883
1884 -- | Take the tail of all value vector abstractions in the uncovered set
1885 utail :: PartialResult -> PartialResult
1886 utail = updateVsa upd
1887 where upd vsa = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ]
1888
1889 -- | Prepend a value abstraction to all value vector abstractions in the
1890 -- uncovered set
1891 ucon :: ValAbs -> PartialResult -> PartialResult
1892 ucon va = updateVsa upd
1893 where
1894 upd vsa = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ]
1895
1896 -- | Given a data constructor of arity `a` and an uncovered set containing
1897 -- value vector abstractions of length `(a+n)`, pass the first `n` value
1898 -- abstractions to the constructor (Hence, the resulting value vector
1899 -- abstractions will have length `n+1`)
1900 kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
1901 -> PartialResult -> PartialResult
1902 kcon con arg_tys ex_tvs dicts
1903 = let n = conLikeArity con
1904 upd vsa =
1905 [ ValVec (va:vva) delta
1906 | ValVec vva' delta <- vsa
1907 , let (args, vva) = splitAt n vva'
1908 , let va = PmCon { pm_con_con = con
1909 , pm_con_arg_tys = arg_tys
1910 , pm_con_tvs = ex_tvs
1911 , pm_con_dicts = dicts
1912 , pm_con_args = args } ]
1913 in updateVsa upd
1914
1915 -- | Get the union of two covered, uncovered and divergent value set
1916 -- abstractions. Since the covered and divergent sets are represented by a
1917 -- boolean, union means computing the logical or (at least one of the two is
1918 -- non-empty).
1919
1920 mkUnion :: PartialResult -> PartialResult -> PartialResult
1921 mkUnion = mappend
1922
1923 -- | Add a value vector abstraction to a value set abstraction (uncovered).
1924 mkCons :: ValVec -> PartialResult -> PartialResult
1925 mkCons vva = updateVsa (vva:)
1926
1927 -- | Set the divergent set to not empty
1928 forces :: PartialResult -> PartialResult
1929 forces pres = pres { presultDivergent = Diverged }
1930
1931 -- | Set the divergent set to non-empty if the flag is `True`
1932 force_if :: Bool -> PartialResult -> PartialResult
1933 force_if True pres = forces pres
1934 force_if False pres = pres
1935
1936 set_provenance :: Provenance -> PartialResult -> PartialResult
1937 set_provenance prov pr = pr { presultProvenance = prov }
1938
1939 -- ----------------------------------------------------------------------------
1940 -- * Propagation of term constraints inwards when checking nested matches
1941
1942 {- Note [Type and Term Equality Propagation]
1943 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1944 When checking a match it would be great to have all type and term information
1945 available so we can get more precise results. For this reason we have functions
1946 `addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
1947 term constraints (respectively) as we go deeper.
1948
1949 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1950 in HsPat.hs. This handles bug #4139 ( see example
1951 https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
1952 where this is needed.
1953
1954 For term equalities we do less, we just generate equalities for HsCase. For
1955 example we accurately give 2 redundancy warnings for the marked cases:
1956
1957 f :: [a] -> Bool
1958 f x = case x of
1959
1960 [] -> case x of -- brings (x ~ []) in scope
1961 [] -> True
1962 (_:_) -> False -- can't happen
1963
1964 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1965 (_:_) -> True
1966 [] -> False -- can't happen
1967
1968 Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
1969 these constraints.
1970 -}
1971
1972 -- | Generate equalities when checking a case expression:
1973 -- case x of { p1 -> e1; ... pn -> en }
1974 -- When we go deeper to check e.g. e1 we record two equalities:
1975 -- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
1976 -- and (x ~ p1).
1977 genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
1978 -> [Pat GhcTc] -- LHS (should have length 1)
1979 -> [Id] -- MatchVars (should have length 1)
1980 -> DsM (Bag SimpleEq)
1981 genCaseTmCs2 Nothing _ _ = return emptyBag
1982 genCaseTmCs2 (Just scr) [p] [var] = do
1983 fam_insts <- dsGetFamInstEnvs
1984 [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
1985 let scr_e = lhsExprToPmExpr scr
1986 return $ listToBag [(var, e), (var, scr_e)]
1987 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
1988
1989 -- | Generate a simple equality when checking a case expression:
1990 -- case x of { matches }
1991 -- When checking matches we record that (x ~ y) where y is the initial
1992 -- uncovered. All matches will have to satisfy this equality.
1993 genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag SimpleEq
1994 genCaseTmCs1 Nothing _ = emptyBag
1995 genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
1996 genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
1997
1998 {- Note [Literals in PmPat]
1999 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2000 Instead of translating a literal to a variable accompanied with a guard, we
2001 treat them like constructor patterns. The following example from
2002 "./libraries/base/GHC/IO/Encoding.hs" shows why:
2003
2004 mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
2005 mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
2006 "UTF8" -> return $ UTF8.mkUTF8 cfm
2007 "UTF16" -> return $ UTF16.mkUTF16 cfm
2008 "UTF16LE" -> return $ UTF16.mkUTF16le cfm
2009 ...
2010
2011 Each clause gets translated to a list of variables with an equal number of
2012 guards. For every guard we generate two cases (equals True/equals False) which
2013 means that we generate 2^n cases to feed the oracle with, where n is the sum of
2014 the length of all strings that appear in the patterns. For this particular
2015 example this means over 2^40 cases. Instead, by representing them like with
2016 constructor we get the following:
2017 1. We exploit the common prefix with our representation of VSAs
2018 2. We prune immediately non-reachable cases
2019 (e.g. False == (x == "U"), True == (x == "U"))
2020
2021 Note [Translating As Patterns]
2022 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2023 Instead of translating x@p as: x (p <- x)
2024 we instead translate it as: p (x <- coercePattern p)
2025 for performance reasons. For example:
2026
2027 f x@True = 1
2028 f y@False = 2
2029
2030 Gives the following with the first translation:
2031
2032 x |> {x == False, x == y, y == True}
2033
2034 If we use the second translation we get an empty set, independently of the
2035 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
2036 used as an expression. That's why we call `coercePatVec' to drop the guard and
2037 `vaToPmExpr' to transform the value abstraction to an expression in the
2038 guard pattern (value abstractions are a subset of expressions). We keep the
2039 guards in the first pattern `p' though.
2040
2041
2042 %************************************************************************
2043 %* *
2044 Pretty printing of exhaustiveness/redundancy check warnings
2045 %* *
2046 %************************************************************************
2047 -}
2048
2049 -- | Check whether any part of pattern match checking is enabled (does not
2050 -- matter whether it is the redundancy check or the exhaustiveness check).
2051 isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
2052 isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
2053 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
2054
2055 instance Outputable ValVec where
2056 ppr (ValVec vva delta)
2057 = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
2058 vector = substInValAbs subst vva
2059 in ppr_uncovered (vector, residual_eqs)
2060
2061 -- | Apply a term substitution to a value vector abstraction. All VAs are
2062 -- transformed to PmExpr (used only before pretty printing).
2063 substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
2064 substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
2065
2066 -- | Wrap up the term oracle's state once solving is complete. Drop any
2067 -- information about unhandled constraints (involving HsExprs) and flatten
2068 -- (height 1) the substitution.
2069 wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
2070 wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
2071
2072 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
2073 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
2074 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
2075 = when (flag_i || flag_u) $ do
2076 let exists_r = flag_i && notNull redundant && onlyBuiltin
2077 exists_i = flag_i && notNull inaccessible && onlyBuiltin && not is_rec_upd
2078 exists_u = flag_u && (case uncovered of
2079 TypeOfUncovered _ -> True
2080 UncoveredPatterns u -> notNull u)
2081
2082 when exists_r $ forM_ redundant $ \(L l q) -> do
2083 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
2084 (pprEqn q "is redundant"))
2085 when exists_i $ forM_ inaccessible $ \(L l q) -> do
2086 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
2087 (pprEqn q "has inaccessible right hand side"))
2088 when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
2089 case uncovered of
2090 TypeOfUncovered ty -> warnEmptyCase ty
2091 UncoveredPatterns candidates -> pprEqns candidates
2092 where
2093 PmResult
2094 { pmresultProvenance = prov
2095 , pmresultRedundant = redundant
2096 , pmresultUncovered = uncovered
2097 , pmresultInaccessible = inaccessible } = pm_result
2098
2099 flag_i = wopt Opt_WarnOverlappingPatterns dflags
2100 flag_u = exhaustive dflags kind
2101 flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
2102
2103 is_rec_upd = case kind of { RecUpd -> True; _ -> False }
2104 -- See Note [Inaccessible warnings for record updates]
2105
2106 onlyBuiltin = prov == FromBuiltin
2107
2108 maxPatterns = maxUncoveredPatterns dflags
2109
2110 -- Print a single clause (for redundant/with-inaccessible-rhs)
2111 pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
2112
2113 -- Print several clauses (for uncovered clauses)
2114 pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
2115 case qs of -- See #11245
2116 [ValVec [] _]
2117 -> text "Guards do not cover entire pattern space"
2118 _missing -> let us = map ppr qs
2119 in hang (text "Patterns not matched:") 4
2120 (vcat (take maxPatterns us)
2121 $$ dots maxPatterns us)
2122
2123 -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
2124 -- which we only know the type and have no inhabitants at hand)
2125 warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
2126 hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
2127
2128 {- Note [Inaccessible warnings for record updates]
2129 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2130 Consider (Trac #12957)
2131 data T a where
2132 T1 :: { x :: Int } -> T Bool
2133 T2 :: { x :: Int } -> T a
2134 T3 :: T a
2135
2136 f :: T Char -> T a
2137 f r = r { x = 3 }
2138
2139 The desugarer will (conservatively generate a case for T1 even though
2140 it's impossible:
2141 f r = case r of
2142 T1 x -> T1 3 -- Inaccessible branch
2143 T2 x -> T2 3
2144 _ -> error "Missing"
2145
2146 We don't want to warn about the inaccessible branch because the programmer
2147 didn't put it there! So we filter out the warning here.
2148 -}
2149
2150 -- | Issue a warning when the predefined number of iterations is exceeded
2151 -- for the pattern match checker
2152 warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
2153 warnPmIters dflags (DsMatchContext kind loc)
2154 = when (flag_i || flag_u) $ do
2155 iters <- maxPmCheckIterations <$> getDynFlags
2156 putSrcSpanDs loc (warnDs NoReason (msg iters))
2157 where
2158 ctxt = pprMatchContext kind
2159 msg is = fsep [ text "Pattern match checker exceeded"
2160 , parens (ppr is), text "iterations in", ctxt <> dot
2161 , text "(Use -fmax-pmcheck-iterations=n"
2162 , text "to set the maximun number of iterations to n)" ]
2163
2164 flag_i = wopt Opt_WarnOverlappingPatterns dflags
2165 flag_u = exhaustive dflags kind
2166
2167 dots :: Int -> [a] -> SDoc
2168 dots maxPatterns qs
2169 | qs `lengthExceeds` maxPatterns = text "..."
2170 | otherwise = empty
2171
2172 -- | Check whether the exhaustiveness checker should run (exhaustiveness only)
2173 exhaustive :: DynFlags -> HsMatchContext id -> Bool
2174 exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
2175
2176 -- | Denotes whether an exhaustiveness check is supported, and if so,
2177 -- via which 'WarningFlag' it's controlled.
2178 -- Returns 'Nothing' if check is not supported.
2179 exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
2180 exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
2181 exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
2182 exhaustiveWarningFlag IfAlt = Just Opt_WarnIncompletePatterns
2183 exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
2184 exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
2185 exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns
2186 exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
2187 exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
2188 exhaustiveWarningFlag ThPatSplice = Nothing
2189 exhaustiveWarningFlag PatSyn = Nothing
2190 exhaustiveWarningFlag ThPatQuote = Nothing
2191 exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns
2192 -- in list comprehensions, pattern guards
2193 -- etc. They are often *supposed* to be
2194 -- incomplete
2195
2196 -- True <==> singular
2197 pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
2198 pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
2199 = vcat [text txt <+> msg,
2200 sep [ text "In" <+> ppr_match <> char ':'
2201 , nest 4 (rest_of_msg_fun pref)]]
2202 where
2203 txt | singular = "Pattern match"
2204 | otherwise = "Pattern match(es)"
2205
2206 (ppr_match, pref)
2207 = case kind of
2208 FunRhs { mc_fun = L _ fun }
2209 -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
2210 _ -> (pprMatchContext kind, \ pp -> pp)
2211
2212 ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
2213 ppr_pats kind pats
2214 = sep [sep (map ppr pats), matchSeparator kind, text "..."]
2215
2216 ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
2217 ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
2218
2219 ppr_constraint :: (SDoc,[PmLit]) -> SDoc
2220 ppr_constraint (var, lits) = var <+> text "is not one of"
2221 <+> braces (pprWithCommas ppr lits)
2222
2223 ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
2224 ppr_uncovered (expr_vec, complex)
2225 | null cs = fsep vec -- there are no literal constraints
2226 | otherwise = hang (fsep vec) 4 $
2227 text "where" <+> vcat (map ppr_constraint cs)
2228 where
2229 sdoc_vec = mapM pprPmExprWithParens expr_vec
2230 (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
2231
2232 {- Note [Representation of Term Equalities]
2233 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2234 In the paper, term constraints always take the form (x ~ e). Of course, a more
2235 general constraint of the form (e1 ~ e1) can always be transformed to an
2236 equivalent set of the former constraints, by introducing a fresh, intermediate
2237 variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
2238 to #11160 (incredibly bad performance for literal pattern matching). Two are
2239 the main sources of this problem (the actual problem is how these two interact
2240 with each other):
2241
2242 1. Pattern matching on literals generates twice as many constraints as needed.
2243 Consider the following (tests/ghci/should_run/ghcirun004):
2244
2245 foo :: Int -> Int
2246 foo 1 = 0
2247 ...
2248 foo 5000 = 4999
2249
2250 The covered and uncovered set *should* look like:
2251 U0 = { x |> {} }
2252
2253 C1 = { 1 |> { x ~ 1 } }
2254 U1 = { x |> { False ~ (x ~ 1) } }
2255 ...
2256 C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
2257 U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
2258 ...
2259
2260 If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
2261 we get twice as many constraints. Also note that half of them are just the
2262 substitution [x |-> False].
2263
2264 2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
2265 (x ~ e) as substitutions [x |-> e]. More specifically, function
2266 `extendSubstAndSolve` applies such substitutions in the residual constraints
2267 and partitions them in the affected and non-affected ones, which are the new
2268 worklist. Essentially, this gives quadradic behaviour on the number of the
2269 residual constraints. (This would not be the case if the term oracle used
2270 mutable variables but, since we use it to handle disjunctions on value set
2271 abstractions (`Union` case), we chose a pure, incremental interface).
2272
2273 Now the problem becomes apparent (e.g. for clause 300):
2274 * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
2275 constraints that we know that will not reduce (stay in the worklist).
2276 * To check for consistency, we apply the substituting constraints ONE BY ONE
2277 (since `tmOracle` is called incrementally, it does not have all of them
2278 available at once). Hence, we go through the (non-progressing) constraints
2279 over and over, achieving over-quadradic behaviour.
2280
2281 If instead we allow constraints of the form (e ~ e),
2282 * All uncovered sets Ui contain no substituting constraints and i
2283 non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
2284 behaves linearly.
2285 * All covered sets Ci contain exactly (i-1) non-progressing constraints and
2286 a single substituting constraint. So the term oracle goes through the
2287 constraints only once.
2288
2289 The performance improvement becomes even more important when more arguments are
2290 involved.
2291 -}
2292
2293 -- Debugging Infrastructre
2294
2295 tracePm :: String -> SDoc -> PmM ()
2296 tracePm herald doc = liftD $ tracePmD herald doc
2297
2298
2299 tracePmD :: String -> SDoc -> DsM ()
2300 tracePmD herald doc = do
2301 dflags <- getDynFlags
2302 printer <- mkPrintUnqualifiedDs
2303 liftIO $ dumpIfSet_dyn_printer printer dflags
2304 Opt_D_dump_ec_trace (text herald $$ (nest 2 doc))
2305
2306
2307 pprPmPatDebug :: PmPat a -> SDoc
2308 pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
2309 = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
2310 pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
2311 pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
2312 pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
2313 pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv)
2314 <+> ppr ge
2315
2316 pprPatVec :: PatVec -> SDoc
2317 pprPatVec ps = hang (text "Pattern:") 2
2318 (brackets $ sep
2319 $ punctuate (comma <> char '\n') (map pprPmPatDebug ps))
2320
2321 pprValAbs :: [ValAbs] -> SDoc
2322 pprValAbs ps = hang (text "ValAbs:") 2
2323 (brackets $ sep
2324 $ punctuate (comma) (map pprPmPatDebug ps))
2325
2326 pprValVecDebug :: ValVec -> SDoc
2327 pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
2328 parens (pprValAbs vas)