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