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