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