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