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