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