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