WIP on combined Step 1 and 3 for Trees That Grow, HsExpr
[ghc.git] / compiler / deSugar / Check.hs
1 {-
2 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
3
4 Pattern Matching Coverage Checking.
5 -}
6
7 {-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
8 {-# LANGUAGE TupleSections #-}
9
10 module Check (
11 -- Checking and printing
12 checkSingle, checkMatches, isAnyPmCheckEnabled,
13
14 -- See Note [Type and Term Equality Propagation]
15 genCaseTmCs1, genCaseTmCs2,
16
17 -- Pattern-match-specific type operations
18 pmIsClosedType, pmTopNormaliseType_maybe
19 ) where
20
21 #include "HsVersions.h"
22
23 import GhcPrelude
24
25 import TmOracle
26 import Unify( tcMatchTy )
27 import BasicTypes
28 import DynFlags
29 import HsSyn
30 import TcHsSyn
31 import Id
32 import ConLike
33 import Name
34 import FamInstEnv
35 import TysPrim (tYPETyCon)
36 import TysWiredIn
37 import TyCon
38 import SrcLoc
39 import Util
40 import Outputable
41 import FastString
42 import DataCon
43 import HscTypes (CompleteMatch(..))
44
45 import DsMonad
46 import TcSimplify (tcCheckSatisfiability)
47 import TcType (toTcType, isStringTy, isIntTy, isWordTy)
48 import Bag
49 import ErrUtils
50 import Var (EvVar)
51 import TyCoRep
52 import Type
53 import UniqSupply
54 import DsGRHSs (isTrueLHsExpr)
55 import Maybes ( expectJust )
56
57 import Data.List (find)
58 import Data.Maybe (isJust, fromMaybe)
59 import Control.Monad (forM, when, forM_)
60 import Coercion
61 import TcEvidence
62 import IOEnv
63 import qualified Data.Semigroup as Semi
64
65 import ListT (ListT(..), fold, select)
66
67 {-
68 This module checks pattern matches for:
69 \begin{enumerate}
70 \item Equations that are redundant
71 \item Equations with inaccessible right-hand-side
72 \item Exhaustiveness
73 \end{enumerate}
74
75 The algorithm is based on the paper:
76
77 "GADTs Meet Their Match:
78 Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
79
80 http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf
81
82 %************************************************************************
83 %* *
84 Pattern Match Check Types
85 %* *
86 %************************************************************************
87 -}
88
89 -- We use the non-determinism monad to apply the algorithm to several
90 -- possible sets of constructors. Users can specify complete sets of
91 -- constructors by using COMPLETE pragmas.
92 -- The algorithm only picks out constructor
93 -- sets deep in the bowels which makes a simpler `mapM` more difficult to
94 -- implement. The non-determinism is only used in one place, see the ConVar
95 -- case in `pmCheckHd`.
96
97 type PmM a = ListT DsM a
98
99 liftD :: DsM a -> PmM a
100 liftD m = ListT $ \sk fk -> m >>= \a -> sk a fk
101
102 -- Pick the first match complete covered match or otherwise the "best" match.
103 -- The best match is the one with the least uncovered clauses, ties broken
104 -- by the number of inaccessible clauses followed by number of redundant
105 -- clauses.
106 --
107 -- This is specified in the
108 -- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
109 -- users' guide. If you update the implementation of this function, make sure
110 -- to update that section of the users' guide as well.
111 getResult :: PmM PmResult -> DsM PmResult
112 getResult ls
113 = do { res <- fold ls goM (pure Nothing)
114 ; case res of
115 Nothing -> panic "getResult is empty"
116 Just a -> return a }
117 where
118 goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
119 goM mpm dpm = do { pmr <- dpm
120 ; return $ Just $ go pmr mpm }
121
122 -- Careful not to force unecessary results
123 go :: Maybe PmResult -> PmResult -> PmResult
124 go Nothing rs = rs
125 go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
126 | null us && null rs && null is = old
127 | otherwise =
128 let PmResult prov' rs' (UncoveredPatterns us') is' = new
129 in case compareLength us us'
130 `mappend` (compareLength is is')
131 `mappend` (compareLength rs rs')
132 `mappend` (compare prov prov') of
133 GT -> new
134 EQ -> new
135 LT -> old
136 go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
137 = panic "getResult: No inhabitation candidates"
138
139 data PatTy = PAT | VA -- Used only as a kind, to index PmPat
140
141 -- The *arity* of a PatVec [p1,..,pn] is
142 -- the number of p1..pn that are not Guards
143
144 data PmPat :: PatTy -> * where
145 PmCon :: { pm_con_con :: ConLike
146 , pm_con_arg_tys :: [Type]
147 , pm_con_tvs :: [TyVar]
148 , pm_con_dicts :: [EvVar]
149 , pm_con_args :: [PmPat t] } -> PmPat t
150 -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
151 PmVar :: { pm_var_id :: Id } -> PmPat t
152 PmLit :: { pm_lit_lit :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
153 PmNLit :: { pm_lit_id :: Id
154 , pm_lit_not :: [PmLit] } -> PmPat 'VA
155 PmGrd :: { pm_grd_pv :: PatVec
156 , pm_grd_expr :: PmExpr } -> PmPat 'PAT
157
158 -- data T a where
159 -- MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
160 -- or MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r
161
162 type Pattern = PmPat 'PAT -- ^ Patterns
163 type ValAbs = PmPat 'VA -- ^ Value Abstractions
164
165 type PatVec = [Pattern] -- ^ Pattern Vectors
166 data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions
167
168 -- | Term and type constraints to accompany each value vector abstraction.
169 -- For efficiency, we store the term oracle state instead of the term
170 -- constraints. TODO: Do the same for the type constraints?
171 data Delta = MkDelta { delta_ty_cs :: Bag EvVar
172 , delta_tm_cs :: TmState }
173
174 type ValSetAbs = [ValVec] -- ^ Value Set Abstractions
175 type Uncovered = ValSetAbs
176
177 -- Instead of keeping the whole sets in memory, we keep a boolean for both the
178 -- covered and the divergent set (we store the uncovered set though, since we
179 -- want to print it). For both the covered and the divergent we have:
180 --
181 -- True <=> The set is non-empty
182 --
183 -- hence:
184 -- C = True ==> Useful clause (no warning)
185 -- C = False, D = True ==> Clause with inaccessible RHS
186 -- C = False, D = False ==> Redundant clause
187
188 data Covered = Covered | NotCovered
189 deriving Show
190
191 instance Outputable Covered where
192 ppr (Covered) = text "Covered"
193 ppr (NotCovered) = text "NotCovered"
194
195 -- Like the or monoid for booleans
196 -- Covered = True, Uncovered = False
197 instance Semi.Semigroup Covered where
198 Covered <> _ = Covered
199 _ <> Covered = Covered
200 NotCovered <> NotCovered = NotCovered
201
202 instance Monoid Covered where
203 mempty = NotCovered
204 mappend = (Semi.<>)
205
206 data Diverged = Diverged | NotDiverged
207 deriving Show
208
209 instance Outputable Diverged where
210 ppr Diverged = text "Diverged"
211 ppr NotDiverged = text "NotDiverged"
212
213 instance Semi.Semigroup Diverged where
214 Diverged <> _ = Diverged
215 _ <> Diverged = Diverged
216 NotDiverged <> NotDiverged = NotDiverged
217
218 instance Monoid Diverged where
219 mempty = NotDiverged
220 mappend = (Semi.<>)
221
222 -- | When we learned that a given match group is complete
223 data Provenance =
224 FromBuiltin -- ^ From the original definition of the type
225 -- constructor.
226 | FromComplete -- ^ From a user-provided @COMPLETE@ pragma
227 deriving (Show, Eq, Ord)
228
229 instance Outputable Provenance where
230 ppr = text . show
231
232 instance Semi.Semigroup Provenance where
233 FromComplete <> _ = FromComplete
234 _ <> FromComplete = FromComplete
235 _ <> _ = FromBuiltin
236
237 instance Monoid Provenance where
238 mempty = FromBuiltin
239 mappend = (Semi.<>)
240
241 data PartialResult = PartialResult {
242 presultProvenance :: Provenance
243 -- keep track of provenance because we don't want
244 -- to warn about redundant matches if the result
245 -- is contaminated with a COMPLETE pragma
246 , presultCovered :: Covered
247 , presultUncovered :: Uncovered
248 , presultDivergent :: Diverged }
249
250 instance Outputable PartialResult where
251 ppr (PartialResult prov c vsa d)
252 = text "PartialResult" <+> ppr prov <+> ppr c
253 <+> ppr d <+> ppr vsa
254
255
256 instance Semi.Semigroup PartialResult where
257 (PartialResult prov1 cs1 vsa1 ds1)
258 <> (PartialResult prov2 cs2 vsa2 ds2)
259 = PartialResult (prov1 Semi.<> prov2)
260 (cs1 Semi.<> cs2)
261 (vsa1 Semi.<> vsa2)
262 (ds1 Semi.<> ds2)
263
264
265 instance Monoid PartialResult where
266 mempty = PartialResult mempty mempty [] mempty
267 mappend = (Semi.<>)
268
269 -- newtype ChoiceOf a = ChoiceOf [a]
270
271 -- | Pattern check result
272 --
273 -- * Redundant clauses
274 -- * Not-covered clauses (or their type, if no pattern is available)
275 -- * Clauses with inaccessible RHS
276 --
277 -- More details about the classification of clauses into useful, redundant
278 -- and with inaccessible right hand side can be found here:
279 --
280 -- https://ghc.haskell.org/trac/ghc/wiki/PatternMatchCheck
281 --
282 data PmResult =
283 PmResult {
284 pmresultProvenance :: Provenance
285 , pmresultRedundant :: [Located [LPat GhcTc]]
286 , pmresultUncovered :: UncoveredCandidates
287 , pmresultInaccessible :: [Located [LPat GhcTc]] }
288
289 -- | Either a list of patterns that are not covered, or their type, in case we
290 -- have no patterns at hand. Not having patterns at hand can arise when
291 -- handling EmptyCase expressions, in two cases:
292 --
293 -- * The type of the scrutinee is a trivially inhabited type (like Int or Char)
294 -- * The type of the scrutinee cannot be reduced to WHNF.
295 --
296 -- In both these cases we have no inhabitation candidates for the type at hand,
297 -- but we don't want to issue just a wildcard as missing. Instead, we print a
298 -- type annotated wildcard, so that the user knows what kind of patterns is
299 -- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
300 data UncoveredCandidates = UncoveredPatterns Uncovered
301 | TypeOfUncovered Type
302
303 -- | The empty pattern check result
304 emptyPmResult :: PmResult
305 emptyPmResult = PmResult FromBuiltin [] (UncoveredPatterns []) []
306
307 -- | Non-exhaustive empty case with unknown/trivial inhabitants
308 uncoveredWithTy :: Type -> PmResult
309 uncoveredWithTy ty = PmResult FromBuiltin [] (TypeOfUncovered ty) []
310
311 {-
312 %************************************************************************
313 %* *
314 Entry points to the checker: checkSingle and checkMatches
315 %* *
316 %************************************************************************
317 -}
318
319 -- | Check a single pattern binding (let)
320 checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
321 checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
322 tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
323 mb_pm_res <- tryM (getResult (checkSingle' locn var p))
324 case mb_pm_res of
325 Left _ -> warnPmIters dflags ctxt
326 Right res -> dsPmWarn dflags ctxt res
327
328 -- | Check a single pattern binding (let)
329 checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
330 checkSingle' locn var p = do
331 liftD resetPmIterDs -- set the iter-no to zero
332 fam_insts <- liftD dsGetFamInstEnvs
333 clause <- liftD $ translatePat fam_insts p
334 missing <- mkInitialUncovered [var]
335 tracePm "checkSingle: missing" (vcat (map pprValVecDebug missing))
336 -- no guards
337 PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
338 let us' = UncoveredPatterns us
339 return $ case (cs,ds) of
340 (Covered, _ ) -> PmResult prov [] us' [] -- useful
341 (NotCovered, NotDiverged) -> PmResult prov m us' [] -- redundant
342 (NotCovered, Diverged ) -> PmResult prov [] us' m -- inaccessible rhs
343 where m = [L locn [L locn p]]
344
345 -- | Check a matchgroup (case, functions, etc.)
346 checkMatches :: DynFlags -> DsMatchContext
347 -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
348 checkMatches dflags ctxt vars matches = do
349 tracePmD "checkMatches" (hang (vcat [ppr ctxt
350 , ppr vars
351 , text "Matches:"])
352 2
353 (vcat (map ppr matches)))
354 mb_pm_res <- tryM $ getResult $ case matches of
355 -- Check EmptyCase separately
356 -- See Note [Checking EmptyCase Expressions]
357 [] | [var] <- vars -> checkEmptyCase' var
358 _normal_match -> checkMatches' vars matches
359 case mb_pm_res of
360 Left _ -> warnPmIters dflags ctxt
361 Right res -> dsPmWarn dflags ctxt res
362
363 -- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
364 -- list of matches. For empty case expressions, use checkEmptyCase' instead.
365 checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
366 checkMatches' vars matches
367 | null matches = panic "checkMatches': EmptyCase"
368 | otherwise = do
369 liftD resetPmIterDs -- set the iter-no to zero
370 missing <- mkInitialUncovered vars
371 tracePm "checkMatches: missing" (vcat (map pprValVecDebug missing))
372 (prov, rs,us,ds) <- go matches missing
373 return $ PmResult {
374 pmresultProvenance = prov
375 , pmresultRedundant = map hsLMatchToLPats rs
376 , pmresultUncovered = UncoveredPatterns us
377 , pmresultInaccessible = map hsLMatchToLPats ds }
378 where
379 go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
380 -> PmM (Provenance
381 , [LMatch GhcTc (LHsExpr GhcTc)]
382 , Uncovered
383 , [LMatch GhcTc (LHsExpr GhcTc)])
384 go [] missing = return (mempty, [], missing, [])
385 go (m:ms) missing = do
386 tracePm "checMatches': go" (ppr m $$ ppr missing)
387 fam_insts <- liftD dsGetFamInstEnvs
388 (clause, guards) <- liftD $ translateMatch fam_insts m
389 r@(PartialResult prov cs missing' ds)
390 <- runMany (pmcheckI clause guards) missing
391 tracePm "checMatches': go: res" (ppr r)
392 (ms_prov, rs, final_u, is) <- go ms missing'
393 let final_prov = prov `mappend` ms_prov
394 return $ case (cs, ds) of
395 -- useful
396 (Covered, _ ) -> (final_prov, rs, final_u, is)
397 -- redundant
398 (NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
399 -- inaccessible
400 (NotCovered, Diverged ) -> (final_prov, rs, final_u, m:is)
401
402 hsLMatchToLPats :: LMatch id body -> Located [LPat id]
403 hsLMatchToLPats (L l (Match { m_pats = pats })) = L l pats
404
405 -- | Check an empty case expression. Since there are no clauses to process, we
406 -- only compute the uncovered set. See Note [Checking EmptyCase Expressions]
407 -- for details.
408 checkEmptyCase' :: Id -> PmM PmResult
409 checkEmptyCase' var = do
410 tm_css <- map toComplex . bagToList <$> liftD getTmCsDs
411 case tmOracle initialTmState tm_css of
412 Just tm_state -> do
413 ty_css <- liftD getDictsDs
414 fam_insts <- liftD dsGetFamInstEnvs
415 mb_candidates <- inhabitationCandidates fam_insts (idType var)
416 case mb_candidates of
417 -- Inhabitation checking failed / the type is trivially inhabited
418 Left ty -> return (uncoveredWithTy ty)
419
420 -- A list of inhabitant candidates is available: Check for each
421 -- one for the satisfiability of the constraints it gives rise to.
422 Right candidates -> do
423 missing_m <- flip concatMapM candidates $ \(va,tm_ct,ty_cs) -> do
424 let all_ty_cs = unionBags ty_cs ty_css
425 sat_ty <- tyOracle all_ty_cs
426 return $ case (sat_ty, tmOracle tm_state (tm_ct:tm_css)) of
427 (True, Just tm_state') -> [(va, all_ty_cs, tm_state')]
428 _non_sat -> []
429 let mkValVec (va,all_ty_cs,tm_state')
430 = ValVec [va] (MkDelta all_ty_cs tm_state')
431 uncovered = UncoveredPatterns (map mkValVec missing_m)
432 return $ if null missing_m
433 then emptyPmResult
434 else PmResult FromBuiltin [] uncovered []
435 Nothing -> return emptyPmResult
436
437 -- | Returns 'True' if the argument 'Type' is a fully saturated application of
438 -- a closed type constructor.
439 --
440 -- Closed type constructors are those with a fixed right hand side, as
441 -- opposed to e.g. associated types. These are of particular interest for
442 -- pattern-match coverage checking, because GHC can exhaustively consider all
443 -- possible forms that values of a closed type can take on.
444 --
445 -- Note that this function is intended to be used to check types of value-level
446 -- patterns, so as a consequence, the 'Type' supplied as an argument to this
447 -- function should be of kind @Type@.
448 pmIsClosedType :: Type -> Bool
449 pmIsClosedType ty
450 = case splitTyConApp_maybe ty of
451 Just (tc, ty_args)
452 | is_algebraic_like tc && not (isFamilyTyCon tc)
453 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
454 _other -> False
455 where
456 -- This returns True for TyCons which /act like/ algebraic types.
457 -- (See "Type#type_classification" for what an algebraic type is.)
458 --
459 -- This is qualified with \"like\" because of a particular special
460 -- case: TYPE (the underlyind kind behind Type, among others). TYPE
461 -- is conceptually a datatype (and thus algebraic), but in practice it is
462 -- a primitive builtin type, so we must check for it specially.
463 --
464 -- NB: it makes sense to think of TYPE as a closed type in a value-level,
465 -- pattern-matching context. However, at the kind level, TYPE is certainly
466 -- not closed! Since this function is specifically tailored towards pattern
467 -- matching, however, it's OK to label TYPE as closed.
468 is_algebraic_like :: TyCon -> Bool
469 is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon
470
471 pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Type, [DataCon], Type)
472 -- ^ Get rid of *outermost* (or toplevel)
473 -- * type function redex
474 -- * data family redex
475 -- * newtypes
476 --
477 -- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
478 -- coercion, it returns useful information for issuing pattern matching
479 -- warnings. See Note [Type normalisation for EmptyCase] for details.
480 pmTopNormaliseType_maybe env typ
481 = do ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ
482 return (eq_src_ty ty (typ : ty_f [ty]), tm_f [], ty)
483 where
484 -- Find the first type in the sequence of rewrites that is a data type,
485 -- newtype, or a data family application (not the representation tycon!).
486 -- This is the one that is equal (in source Haskell) to the initial type.
487 -- If none is found in the list, then all of them are type family
488 -- applications, so we simply return the last one, which is the *simplest*.
489 eq_src_ty :: Type -> [Type] -> Type
490 eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys)
491
492 is_closed_or_data_family :: Type -> Bool
493 is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty
494
495 -- For efficiency, represent both lists as difference lists.
496 -- comb performs the concatenation, for both lists.
497 comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2)
498
499 stepper = newTypeStepper `composeSteppers` tyFamStepper
500
501 -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
502 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
503 newTypeStepper :: NormaliseStepper ([Type] -> [Type],[DataCon] -> [DataCon])
504 newTypeStepper rec_nts tc tys
505 | Just (ty', _co) <- instNewTyCon_maybe tc tys
506 = case checkRecTc rec_nts tc of
507 Just rec_nts' -> let tyf = ((TyConApp tc tys):)
508 tmf = ((tyConSingleDataCon tc):)
509 in NS_Step rec_nts' ty' (tyf, tmf)
510 Nothing -> NS_Abort
511 | otherwise
512 = NS_Done
513
514 tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
515 tyFamStepper rec_nts tc tys -- Try to step a type/data family
516 = let (_args_co, ntys) = normaliseTcArgs env Representational tc tys in
517 -- NB: It's OK to use normaliseTcArgs here instead of
518 -- normalise_tc_args (which takes the LiftingContext described
519 -- in Note [Normalising types]) because the reduceTyFamApp below
520 -- works only at top level. We'll never recur in this function
521 -- after reducing the kind of a bound tyvar.
522
523 case reduceTyFamApp_maybe env Representational tc ntys of
524 Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
525 _ -> NS_Done
526
527 {- Note [Type normalisation for EmptyCase]
528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
529 EmptyCase is an exception for pattern matching, since it is strict. This means
530 that it boils down to checking whether the type of the scrutinee is inhabited.
531 Function pmTopNormaliseType_maybe gets rid of the outermost type function/data
532 family redex and newtypes, in search of an algebraic type constructor, which is
533 easier to check for inhabitation.
534
535 It returns 3 results instead of one, because there are 2 subtle points:
536 1. Newtypes are isomorphic to the underlying type in core but not in the source
537 language,
538 2. The representational data family tycon is used internally but should not be
539 shown to the user
540
541 Hence, if pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty), then
542 (a) src_ty is the rewritten type which we can show to the user. That is, the
543 type we get if we rewrite type families but not data families or
544 newtypes.
545 (b) dcs is the list of data constructors "skipped", every time we normalise a
546 newtype to it's core representation, we keep track of the source data
547 constructor.
548 (c) core_ty is the rewritten type. That is,
549 pmTopNormaliseType_maybe env ty = Just (src_ty, dcs, core_ty)
550 implies
551 topNormaliseType_maybe env ty = Just (co, core_ty)
552 for some coercion co.
553
554 To see how all cases come into play, consider the following example:
555
556 data family T a :: *
557 data instance T Int = T1 | T2 Bool
558 -- Which gives rise to FC:
559 -- data T a
560 -- data R:TInt = T1 | T2 Bool
561 -- axiom ax_ti : T Int ~R R:TInt
562
563 newtype G1 = MkG1 (T Int)
564 newtype G2 = MkG2 G1
565
566 type instance F Int = F Char
567 type instance F Char = G2
568
569 In this case pmTopNormaliseType_maybe env (F Int) results in
570
571 Just (G2, [MkG2,MkG1], R:TInt)
572
573 Which means that in source Haskell:
574 - G2 is equivalent to F Int (in contrast, G1 isn't).
575 - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
576 -}
577
578 -- | Generate all inhabitation candidates for a given type. The result is
579 -- either (Left ty), if the type cannot be reduced to a closed algebraic type
580 -- (or if it's one trivially inhabited, like Int), or (Right candidates), if it
581 -- can. In this case, the candidates are the signature of the tycon, each one
582 -- accompanied by the term- and type- constraints it gives rise to.
583 -- See also Note [Checking EmptyCase Expressions]
584 inhabitationCandidates :: FamInstEnvs -> Type
585 -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
586 inhabitationCandidates fam_insts ty
587 = case pmTopNormaliseType_maybe fam_insts ty of
588 Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
589 Nothing -> alts_to_check ty ty []
590 where
591 -- All these types are trivially inhabited
592 trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
593 , intTyCon, wordTyCon, word8TyCon ]
594
595 -- Note: At the moment we leave all the typing and constraint fields of
596 -- PmCon empty, since we know that they are not gonna be used. Is the
597 -- right-thing-to-do to actually create them, even if they are never used?
598 build_tm :: ValAbs -> [DataCon] -> ValAbs
599 build_tm = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e])
600
601 -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
602 alts_to_check :: Type -> Type -> [DataCon]
603 -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
604 alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
605 Just (tc, _)
606 | tc `elem` trivially_inhabited -> case dcs of
607 [] -> return (Left src_ty)
608 (_:_) -> do var <- liftD $ mkPmId (toTcType core_ty)
609 let va = build_tm (PmVar var) dcs
610 return $ Right [(va, mkIdEq var, emptyBag)]
611
612 | pmIsClosedType core_ty -> liftD $ do
613 var <- mkPmId (toTcType core_ty) -- it would be wrong to unify x
614 alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
615 return $ Right [(build_tm va dcs, eq, cs) | (va, eq, cs) <- alts]
616 -- For other types conservatively assume that they are inhabited.
617 _other -> return (Left src_ty)
618
619 {- Note [Checking EmptyCase Expressions]
620 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
621 Empty case expressions are strict on the scrutinee. That is, `case x of {}`
622 will force argument `x`. Hence, `checkMatches` is not sufficient for checking
623 empty cases, because it assumes that the match is not strict (which is true
624 for all other cases, apart from EmptyCase). This gave rise to #10746. Instead,
625 we do the following:
626
627 1. We normalise the outermost type family redex, data family redex or newtype,
628 using pmTopNormaliseType_maybe (in types/FamInstEnv.hs). This computes 3
629 things:
630 (a) A normalised type src_ty, which is equal to the type of the scrutinee in
631 source Haskell (does not normalise newtypes or data families)
632 (b) The actual normalised type core_ty, which coincides with the result
633 topNormaliseType_maybe. This type is not necessarily equal to the input
634 type in source Haskell. And this is precicely the reason we compute (a)
635 and (c): the reasoning happens with the underlying types, but both the
636 patterns and types we print should respect newtypes and also show the
637 family type constructors and not the representation constructors.
638
639 (c) A list of all newtype data constructors dcs, each one corresponding to a
640 newtype rewrite performed in (b).
641
642 For an example see also Note [Type normalisation for EmptyCase]
643 in types/FamInstEnv.hs.
644
645 2. Function checkEmptyCase' performs the check:
646 - If core_ty is not an algebraic type, then we cannot check for
647 inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming
648 that the type is inhabited.
649 - If core_ty is an algebraic type, then we unfold the scrutinee to all
650 possible constructor patterns, using inhabitationCandidates, and then
651 check each one for constraint satisfiability, same as we for normal
652 pattern match checking.
653
654 %************************************************************************
655 %* *
656 Transform source syntax to *our* syntax
657 %* *
658 %************************************************************************
659 -}
660
661 -- -----------------------------------------------------------------------
662 -- * Utilities
663
664 nullaryConPattern :: ConLike -> Pattern
665 -- Nullary data constructor and nullary type constructor
666 nullaryConPattern con =
667 PmCon { pm_con_con = con, pm_con_arg_tys = []
668 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
669 {-# INLINE nullaryConPattern #-}
670
671 truePattern :: Pattern
672 truePattern = nullaryConPattern (RealDataCon trueDataCon)
673 {-# INLINE truePattern #-}
674
675 -- | A fake guard pattern (True <- _) used to represent cases we cannot handle
676 fake_pat :: Pattern
677 fake_pat = PmGrd { pm_grd_pv = [truePattern]
678 , pm_grd_expr = PmExprOther (EWildPat noExt) }
679 {-# INLINE fake_pat #-}
680
681 -- | Check whether a guard pattern is generated by the checker (unhandled)
682 isFakeGuard :: [Pattern] -> PmExpr -> Bool
683 isFakeGuard [PmCon { pm_con_con = RealDataCon c }] (PmExprOther (EWildPat _))
684 | c == trueDataCon = True
685 | otherwise = False
686 isFakeGuard _pats _e = False
687
688 -- | Generate a `canFail` pattern vector of a specific type
689 mkCanFailPmPat :: Type -> DsM PatVec
690 mkCanFailPmPat ty = do
691 var <- mkPmVar ty
692 return [var, fake_pat]
693
694 vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
695 -- ADT constructor pattern => no existentials, no local constraints
696 vanillaConPattern con arg_tys args =
697 PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
698 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
699 {-# INLINE vanillaConPattern #-}
700
701 -- | Create an empty list pattern of a given type
702 nilPattern :: Type -> Pattern
703 nilPattern ty =
704 PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
705 , pm_con_tvs = [], pm_con_dicts = []
706 , pm_con_args = [] }
707 {-# INLINE nilPattern #-}
708
709 mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
710 mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
711 , pm_con_arg_tys = [ty]
712 , pm_con_tvs = [], pm_con_dicts = []
713 , pm_con_args = xs++ys }]
714 {-# INLINE mkListPatVec #-}
715
716 -- | Create a (non-overloaded) literal pattern
717 mkLitPattern :: HsLit GhcTc -> Pattern
718 mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
719 {-# INLINE mkLitPattern #-}
720
721 -- -----------------------------------------------------------------------
722 -- * Transform (Pat Id) into of (PmPat Id)
723
724 translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
725 translatePat fam_insts pat = case pat of
726 WildPat ty -> mkPmVars [ty]
727 VarPat _ id -> return [PmVar (unLoc id)]
728 ParPat _ p -> translatePat fam_insts (unLoc p)
729 LazyPat _ _ -> mkPmVars [hsPatType pat] -- like a variable
730
731 -- ignore strictness annotations for now
732 BangPat _ p -> translatePat fam_insts (unLoc p)
733
734 AsPat _ lid p -> do
735 -- Note [Translating As Patterns]
736 ps <- translatePat fam_insts (unLoc p)
737 let [e] = map vaToPmExpr (coercePatVec ps)
738 g = PmGrd [PmVar (unLoc lid)] e
739 return (ps ++ [g])
740
741 SigPat _ty p -> translatePat fam_insts (unLoc p)
742
743 -- See Note [Translate CoPats]
744 CoPat _ wrapper p ty
745 | isIdHsWrapper wrapper -> translatePat fam_insts p
746 | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts p
747 | otherwise -> do
748 ps <- translatePat fam_insts p
749 (xp,xe) <- mkPmId2Forms ty
750 let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
751 return [xp,g]
752
753 -- (n + k) ===> x (True <- x >= k) (n <- x-k)
754 NPlusKPat ty (L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty
755
756 -- (fun -> pat) ===> x (pat <- fun x)
757 ViewPat arg_ty lexpr lpat -> do
758 ps <- translatePat fam_insts (unLoc lpat)
759 -- See Note [Guards and Approximation]
760 case all cantFailPattern ps of
761 True -> do
762 (xp,xe) <- mkPmId2Forms arg_ty
763 let g = mkGuard ps (HsApp noExt lexpr xe)
764 return [xp,g]
765 False -> mkCanFailPmPat arg_ty
766
767 -- list
768 ListPat _ ps ty Nothing -> do
769 foldr (mkListPatVec ty) [nilPattern ty]
770 <$> translatePatVec fam_insts (map unLoc ps)
771
772 -- overloaded list
773 ListPat x lpats elem_ty (Just (pat_ty, _to_list))
774 | Just e_ty <- splitListTyConApp_maybe pat_ty
775 , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty
776 -- elem_ty is frequently something like
777 -- `Item [Int]`, but we prefer `Int`
778 , norm_elem_ty `eqType` e_ty ->
779 -- We have to ensure that the element types are exactly the same.
780 -- Otherwise, one may give an instance IsList [Int] (more specific than
781 -- the default IsList [a]) with a different implementation for `toList'
782 translatePat fam_insts (ListPat x lpats e_ty Nothing)
783 -- See Note [Guards and Approximation]
784 | otherwise -> mkCanFailPmPat pat_ty
785
786 ConPatOut { pat_con = L _ con
787 , pat_arg_tys = arg_tys
788 , pat_tvs = ex_tvs
789 , pat_dicts = dicts
790 , pat_args = ps } -> do
791 groups <- allCompleteMatches con arg_tys
792 case groups of
793 [] -> mkCanFailPmPat (conLikeResTy con arg_tys)
794 _ -> do
795 args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
796 return [PmCon { pm_con_con = con
797 , pm_con_arg_tys = arg_tys
798 , pm_con_tvs = ex_tvs
799 , pm_con_dicts = dicts
800 , pm_con_args = args }]
801
802 NPat ty (L _ ol) mb_neg _eq -> translateNPat fam_insts ol mb_neg ty
803
804 LitPat _ lit
805 -- If it is a string then convert it to a list of characters
806 | HsString src s <- lit ->
807 foldr (mkListPatVec charTy) [nilPattern charTy] <$>
808 translatePatVec fam_insts
809 (map (LitPat noExt . HsChar src) (unpackFS s))
810 | otherwise -> return [mkLitPattern lit]
811
812 PArrPat ty ps -> do
813 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
814 let fake_con = RealDataCon (parrFakeCon (length ps))
815 return [vanillaConPattern fake_con [ty] (concat tidy_ps)]
816
817 TuplePat tys ps boxity -> do
818 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
819 let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
820 return [vanillaConPattern tuple_con tys (concat tidy_ps)]
821
822 SumPat ty p alt arity -> do
823 tidy_p <- translatePat fam_insts (unLoc p)
824 let sum_con = RealDataCon (sumDataCon alt arity)
825 return [vanillaConPattern sum_con ty tidy_p]
826
827 -- --------------------------------------------------------------------------
828 -- Not supposed to happen
829 ConPatIn {} -> panic "Check.translatePat: ConPatIn"
830 SplicePat {} -> panic "Check.translatePat: SplicePat"
831 XPat {} -> panic "Check.translatePat: XPat"
832
833 -- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
834 translateNPat :: FamInstEnvs
835 -> HsOverLit GhcTc -> Maybe (SyntaxExpr GhcTc) -> Type
836 -> DsM PatVec
837 translateNPat fam_insts (OverLit (OverLitTc False ty) val _ ) mb_neg outer_ty
838 | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
839 = translatePat fam_insts (LitPat noExt (HsString src s))
840 | not type_change, isIntTy ty, HsIntegral i <- val
841 = translatePat fam_insts
842 (LitPat noExt $ case mb_neg of
843 Nothing -> HsInt noExt i
844 Just _ -> HsInt noExt (negateIntegralLit i))
845 | not type_change, isWordTy ty, HsIntegral i <- val
846 = translatePat fam_insts
847 (LitPat noExt $ case mb_neg of
848 Nothing -> HsWordPrim (il_text i) (il_value i)
849 Just _ -> let ni = negateIntegralLit i in
850 HsWordPrim (il_text ni) (il_value ni))
851 where
852 type_change = not (outer_ty `eqType` ty)
853
854 translateNPat _ ol mb_neg _
855 = return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) ol }]
856
857 -- | Translate a list of patterns (Note: each pattern is translated
858 -- to a pattern vector but we do not concatenate the results).
859 translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
860 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
861
862 -- | Translate a constructor pattern
863 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
864 -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
865 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
866 = concat <$> translatePatVec fam_insts (map unLoc ps)
867 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
868 = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
869 translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
870 -- Nothing matched. Make up some fresh term variables
871 | null fs = mkPmVars arg_tys
872 -- The data constructor was not defined using record syntax. For the
873 -- pattern to be in record syntax it should be empty (e.g. Just {}).
874 -- So just like the previous case.
875 | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
876 -- Some of the fields appear, in the original order (there may be holes).
877 -- Generate a simple constructor pattern and make up fresh variables for
878 -- the rest of the fields
879 | matched_lbls `subsetOf` orig_lbls
880 = ASSERT(orig_lbls `equalLength` arg_tys)
881 let translateOne (lbl, ty) = case lookup lbl matched_pats of
882 Just p -> translatePat fam_insts p
883 Nothing -> mkPmVars [ty]
884 in concatMapM translateOne (zip orig_lbls arg_tys)
885 -- The fields that appear are not in the correct order. Make up fresh
886 -- variables for all fields and add guards after matching, to force the
887 -- evaluation in the correct order.
888 | otherwise = do
889 arg_var_pats <- mkPmVars arg_tys
890 translated_pats <- forM matched_pats $ \(x,pat) -> do
891 pvec <- translatePat fam_insts pat
892 return (x, pvec)
893
894 let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
895 guards = map (\(name,pvec) -> case lookup name zipped of
896 Just x -> PmGrd pvec (PmExprVar (idName x))
897 Nothing -> panic "translateConPatVec: lookup")
898 translated_pats
899
900 return (arg_var_pats ++ guards)
901 where
902 -- The actual argument types (instantiated)
903 arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
904
905 -- Some label information
906 orig_lbls = map flSelector $ conLikeFieldLabels c
907 matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
908 | L _ x <- fs]
909 matched_lbls = [ name | (name, _pat) <- matched_pats ]
910
911 subsetOf :: Eq a => [a] -> [a] -> Bool
912 subsetOf [] _ = True
913 subsetOf (_:_) [] = False
914 subsetOf (x:xs) (y:ys)
915 | x == y = subsetOf xs ys
916 | otherwise = subsetOf (x:xs) ys
917
918 -- Translate a single match
919 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
920 -> DsM (PatVec,[PatVec])
921 translateMatch fam_insts (L _ (Match { m_pats = lpats, m_grhss = grhss })) = do
922 pats' <- concat <$> translatePatVec fam_insts pats
923 guards' <- mapM (translateGuards fam_insts) guards
924 return (pats', guards')
925 where
926 extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
927 extractGuards (L _ (GRHS gs _)) = map unLoc gs
928
929 pats = map unLoc lpats
930 guards = map extractGuards (grhssGRHSs grhss)
931
932 -- -----------------------------------------------------------------------
933 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
934
935 -- | Translate a list of guard statements to a pattern vector
936 translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
937 translateGuards fam_insts guards = do
938 all_guards <- concat <$> mapM (translateGuard fam_insts) guards
939 return (replace_unhandled all_guards)
940 -- It should have been (return all_guards) but it is too expressive.
941 -- Since the term oracle does not handle all constraints we generate,
942 -- we (hackily) replace all constraints the oracle cannot handle with a
943 -- single one (we need to know if there is a possibility of falure).
944 -- See Note [Guards and Approximation] for all guard-related approximations
945 -- we implement.
946 where
947 replace_unhandled :: PatVec -> PatVec
948 replace_unhandled gv
949 | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
950 | otherwise = gv
951
952 any_unhandled :: PatVec -> Bool
953 any_unhandled gv = any (not . shouldKeep) gv
954
955 shouldKeep :: Pattern -> Bool
956 shouldKeep p
957 | PmVar {} <- p = True
958 | PmCon {} <- p = singleConstructor (pm_con_con p)
959 && all shouldKeep (pm_con_args p)
960 shouldKeep (PmGrd pv e)
961 | all shouldKeep pv = True
962 | isNotPmExprOther e = True -- expensive but we want it
963 shouldKeep _other_pat = False -- let the rest..
964
965 -- | Check whether a pattern can fail to match
966 cantFailPattern :: Pattern -> Bool
967 cantFailPattern p
968 | PmVar {} <- p = True
969 | PmCon {} <- p = singleConstructor (pm_con_con p)
970 && all cantFailPattern (pm_con_args p)
971 cantFailPattern (PmGrd pv _e)
972 = all cantFailPattern pv
973 cantFailPattern _ = False
974
975 -- | Translate a guard statement to Pattern
976 translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
977 translateGuard fam_insts guard = case guard of
978 BodyStmt e _ _ _ -> translateBoolGuard e
979 LetStmt binds -> translateLet (unLoc binds)
980 BindStmt p e _ _ _ -> translateBind fam_insts p e
981 LastStmt {} -> panic "translateGuard LastStmt"
982 ParStmt {} -> panic "translateGuard ParStmt"
983 TransStmt {} -> panic "translateGuard TransStmt"
984 RecStmt {} -> panic "translateGuard RecStmt"
985 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
986
987 -- | Translate let-bindings
988 translateLet :: HsLocalBinds GhcTc -> DsM PatVec
989 translateLet _binds = return []
990
991 -- | Translate a pattern guard
992 translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
993 translateBind fam_insts (L _ p) e = do
994 ps <- translatePat fam_insts p
995 return [mkGuard ps (unLoc e)]
996
997 -- | Translate a boolean guard
998 translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
999 translateBoolGuard e
1000 | isJust (isTrueLHsExpr e) = return []
1001 -- The formal thing to do would be to generate (True <- True)
1002 -- but it is trivial to solve so instead we give back an empty
1003 -- PatVec for efficiency
1004 | otherwise = return [mkGuard [truePattern] (unLoc e)]
1005
1006 {- Note [Guards and Approximation]
1007 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1008 Even if the algorithm is really expressive, the term oracle we use is not.
1009 Hence, several features are not translated *properly* but we approximate.
1010 The list includes:
1011
1012 1. View Patterns
1013 ----------------
1014 A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
1015 oracle does not handle function applications so we know that the generated
1016 constraints will not be handled at the end. Hence, we distinguish between two
1017 cases:
1018 a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
1019 thing*.
1020 b) Pattern @p@ can fail. This means that when checking the guard, we will
1021 generate several cases, with no useful information. E.g.:
1022
1023 h (f -> [a,b]) = ...
1024 h x ([a,b] <- f x) = ...
1025
1026 uncovered set = { [x |> { False ~ (f x ~ []) }]
1027 , [x |> { False ~ (f x ~ (t1:[])) }]
1028 , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
1029
1030 So we have two problems:
1031 1) Since we do not print the constraints in the general case (they may
1032 be too many), the warning will look like this:
1033
1034 Pattern match(es) are non-exhaustive
1035 In an equation for `h':
1036 Patterns not matched:
1037 _
1038 _
1039 _
1040 Which is not short and not more useful than a single underscore.
1041 2) The size of the uncovered set increases a lot, without gaining more
1042 expressivity in our warnings.
1043
1044 Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
1045 @fake_pat@: @True <- _@. That is, we record that there is a possibility
1046 of failure but we minimize it to a True/False. This generates a single
1047 warning and much smaller uncovered sets.
1048
1049 2. Overloaded Lists
1050 -------------------
1051 An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
1052 problem is exactly like above, as its solution. For future reference, the code
1053 below is the *right thing to do*:
1054
1055 ListPat lpats elem_ty (Just (pat_ty, to_list))
1056 otherwise -> do
1057 (xp, xe) <- mkPmId2Forms pat_ty
1058 ps <- translatePatVec (map unLoc lpats)
1059 let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
1060 g = mkGuard pats (HsApp (noLoc to_list) xe)
1061 return [xp,g]
1062
1063 3. Overloaded Literals
1064 ----------------------
1065 The case with literals is a bit different. a literal @l@ should be translated
1066 to @x (True <- x == from l)@. Since we want to have better warnings for
1067 overloaded literals as it is a very common feature, we treat them differently.
1068 They are mainly covered in Note [Undecidable Equality on Overloaded Literals]
1069 in PmExpr.
1070
1071 4. N+K Patterns & Pattern Synonyms
1072 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1073 An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
1074 Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
1075 and has two possible outcomes. Hence, there is no benefit in using a dummy and
1076 we implement the proper thing. Pattern synonyms are simply not implemented yet.
1077 Hence, to be conservative, we generate a dummy pattern, assuming that the
1078 pattern can fail.
1079
1080 5. Actual Guards
1081 ----------------
1082 During translation, boolean guards and pattern guards are translated properly.
1083 Let bindings though are omitted by function @translateLet@. Since they are lazy
1084 bindings, we do not actually want to generate a (strict) equality (like we do
1085 in the pattern bind case). Hence, we safely drop them.
1086
1087 Additionally, top-level guard translation (performed by @translateGuards@)
1088 replaces guards that cannot be reasoned about (like the ones we described in
1089 1-4) with a single @fake_pat@ to record the possibility of failure to match.
1090
1091 Note [Translate CoPats]
1092 ~~~~~~~~~~~~~~~~~~~~~~~
1093 The pattern match checker did not know how to handle coerced patterns `CoPat`
1094 efficiently, which gave rise to #11276. The original approach translated
1095 `CoPat`s:
1096
1097 pat |> co ===> x (pat <- (e |> co))
1098
1099 Instead, we now check whether the coercion is a hole or if it is just refl, in
1100 which case we can drop it. Unfortunately, data families generate useful
1101 coercions so guards are still generated in these cases and checking data
1102 families is not really efficient.
1103
1104 %************************************************************************
1105 %* *
1106 Utilities for Pattern Match Checking
1107 %* *
1108 %************************************************************************
1109 -}
1110
1111 -- ----------------------------------------------------------------------------
1112 -- * Basic utilities
1113
1114 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
1115 -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
1116 pmPatType :: PmPat p -> Type
1117 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
1118 = conLikeResTy con tys
1119 pmPatType (PmVar { pm_var_id = x }) = idType x
1120 pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
1121 pmPatType (PmNLit { pm_lit_id = x }) = idType x
1122 pmPatType (PmGrd { pm_grd_pv = pv })
1123 = ASSERT(patVecArity pv == 1) (pmPatType p)
1124 where Just p = find ((==1) . patternArity) pv
1125
1126 -- | Generate a value abstraction for a given constructor (generate
1127 -- fresh variables of the appropriate type for arguments)
1128 mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
1129 -- * x :: T tys, where T is an algebraic data type
1130 -- NB: in the case of a data family, T is the *representation* TyCon
1131 -- e.g. data instance T (a,b) = T1 a b
1132 -- leads to
1133 -- data TPair a b = T1 a b -- The "representation" type
1134 -- It is TPair, not T, that is given to mkOneConFull
1135 --
1136 -- * 'con' K is a constructor of data type T
1137 --
1138 -- After instantiating the universal tyvars of K we get
1139 -- K tys :: forall bs. Q => s1 .. sn -> T tys
1140 --
1141 -- Results: ValAbs: K (y1::s1) .. (yn::sn)
1142 -- ComplexEq: x ~ K y1..yn
1143 -- [EvVar]: Q
1144 mkOneConFull x con = do
1145 let res_ty = idType x
1146 (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
1147 = conLikeFullSig con
1148 tc_args = tyConAppArgs res_ty
1149 subst1 = case con of
1150 RealDataCon {} -> zipTvSubst univ_tvs tc_args
1151 PatSynCon {} -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty)
1152 -- See Note [Pattern synonym result type] in PatSyn
1153
1154 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
1155
1156 -- Fresh term variables (VAs) as arguments to the constructor
1157 arguments <- mapM mkPmVar (substTys subst arg_tys)
1158 -- All constraints bound by the constructor (alpha-renamed)
1159 let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
1160 evvars <- mapM (nameType "pm") theta_cs
1161 let con_abs = PmCon { pm_con_con = con
1162 , pm_con_arg_tys = tc_args
1163 , pm_con_tvs = ex_tvs'
1164 , pm_con_dicts = evvars
1165 , pm_con_args = arguments }
1166 return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
1167
1168 -- ----------------------------------------------------------------------------
1169 -- * More smart constructors and fresh variable generation
1170
1171 -- | Create a guard pattern
1172 mkGuard :: PatVec -> HsExpr GhcTc -> Pattern
1173 mkGuard pv e
1174 | all cantFailPattern pv = PmGrd pv expr
1175 | PmExprOther {} <- expr = fake_pat
1176 | otherwise = PmGrd pv expr
1177 where
1178 expr = hsExprToPmExpr e
1179
1180 -- | Create a term equality of the form: `(False ~ (x ~ lit))`
1181 mkNegEq :: Id -> PmLit -> ComplexEq
1182 mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
1183 {-# INLINE mkNegEq #-}
1184
1185 -- | Create a term equality of the form: `(x ~ lit)`
1186 mkPosEq :: Id -> PmLit -> ComplexEq
1187 mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
1188 {-# INLINE mkPosEq #-}
1189
1190 -- | Create a term equality of the form: `(x ~ x)`
1191 -- (always discharged by the term oracle)
1192 mkIdEq :: Id -> ComplexEq
1193 mkIdEq x = (PmExprVar name, PmExprVar name)
1194 where name = idName x
1195 {-# INLINE mkIdEq #-}
1196
1197 -- | Generate a variable pattern of a given type
1198 mkPmVar :: Type -> DsM (PmPat p)
1199 mkPmVar ty = PmVar <$> mkPmId ty
1200 {-# INLINE mkPmVar #-}
1201
1202 -- | Generate many variable patterns, given a list of types
1203 mkPmVars :: [Type] -> DsM PatVec
1204 mkPmVars tys = mapM mkPmVar tys
1205 {-# INLINE mkPmVars #-}
1206
1207 -- | Generate a fresh `Id` of a given type
1208 mkPmId :: Type -> DsM Id
1209 mkPmId ty = getUniqueM >>= \unique ->
1210 let occname = mkVarOccFS $ fsLit "$pm"
1211 name = mkInternalName unique occname noSrcSpan
1212 in return (mkLocalId name ty)
1213
1214 -- | Generate a fresh term variable of a given and return it in two forms:
1215 -- * A variable pattern
1216 -- * A variable expression
1217 mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
1218 mkPmId2Forms ty = do
1219 x <- mkPmId ty
1220 return (PmVar x, noLoc (HsVar noExt (noLoc x)))
1221
1222 -- ----------------------------------------------------------------------------
1223 -- * Converting between Value Abstractions, Patterns and PmExpr
1224
1225 -- | Convert a value abstraction an expression
1226 vaToPmExpr :: ValAbs -> PmExpr
1227 vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
1228 = PmExprCon c (map vaToPmExpr ps)
1229 vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
1230 vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
1231 vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
1232
1233 -- | Convert a pattern vector to a list of value abstractions by dropping the
1234 -- guards (See Note [Translating As Patterns])
1235 coercePatVec :: PatVec -> [ValAbs]
1236 coercePatVec pv = concatMap coercePmPat pv
1237
1238 -- | Convert a pattern to a list of value abstractions (will be either an empty
1239 -- list if the pattern is a guard pattern, or a singleton list in all other
1240 -- cases) by dropping the guards (See Note [Translating As Patterns])
1241 coercePmPat :: Pattern -> [ValAbs]
1242 coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
1243 coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
1244 coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
1245 , pm_con_tvs = tvs, pm_con_dicts = dicts
1246 , pm_con_args = args })
1247 = [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
1248 , pm_con_tvs = tvs, pm_con_dicts = dicts
1249 , pm_con_args = coercePatVec args }]
1250 coercePmPat (PmGrd {}) = [] -- drop the guards
1251
1252 -- | Check whether a data constructor is the only way to construct
1253 -- a data type.
1254 singleConstructor :: ConLike -> Bool
1255 singleConstructor (RealDataCon dc) =
1256 case tyConDataCons (dataConTyCon dc) of
1257 [_] -> True
1258 _ -> False
1259 singleConstructor _ = False
1260
1261 -- | For a given conlike, finds all the sets of patterns which could
1262 -- be relevant to that conlike by consulting the result type.
1263 --
1264 -- These come from two places.
1265 -- 1. From data constructors defined with the result type constructor.
1266 -- 2. From `COMPLETE` pragmas which have the same type as the result
1267 -- type constructor.
1268 allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
1269 allCompleteMatches cl tys = do
1270 let fam = case cl of
1271 RealDataCon dc ->
1272 [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
1273 PatSynCon _ -> []
1274
1275 pragmas <- case splitTyConApp_maybe (conLikeResTy cl tys) of
1276 Just (tc, _) -> dsGetCompleteMatches tc
1277 Nothing -> return []
1278 let fams cm = fmap (FromComplete,) $
1279 mapM dsLookupConLike (completeMatchConLikes cm)
1280 from_pragma <- mapM fams pragmas
1281
1282 let final_groups = fam ++ from_pragma
1283 tracePmD "allCompleteMatches" (ppr final_groups)
1284 return final_groups
1285
1286 -- -----------------------------------------------------------------------
1287 -- * Types and constraints
1288
1289 newEvVar :: Name -> Type -> EvVar
1290 newEvVar name ty = mkLocalId name (toTcType ty)
1291
1292 nameType :: String -> Type -> DsM EvVar
1293 nameType name ty = do
1294 unique <- getUniqueM
1295 let occname = mkVarOccFS (fsLit (name++"_"++show unique))
1296 idname = mkInternalName unique occname noSrcSpan
1297 return (newEvVar idname ty)
1298
1299 {-
1300 %************************************************************************
1301 %* *
1302 The type oracle
1303 %* *
1304 %************************************************************************
1305 -}
1306
1307 -- | Check whether a set of type constraints is satisfiable.
1308 tyOracle :: Bag EvVar -> PmM Bool
1309 tyOracle evs
1310 = liftD $
1311 do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
1312 ; case res of
1313 Just sat -> return sat
1314 Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
1315
1316 {-
1317 %************************************************************************
1318 %* *
1319 Sanity Checks
1320 %* *
1321 %************************************************************************
1322 -}
1323
1324 -- | The arity of a pattern/pattern vector is the
1325 -- number of top-level patterns that are not guards
1326 type PmArity = Int
1327
1328 -- | Compute the arity of a pattern vector
1329 patVecArity :: PatVec -> PmArity
1330 patVecArity = sum . map patternArity
1331
1332 -- | Compute the arity of a pattern
1333 patternArity :: Pattern -> PmArity
1334 patternArity (PmGrd {}) = 0
1335 patternArity _other_pat = 1
1336
1337 {-
1338 %************************************************************************
1339 %* *
1340 Heart of the algorithm: Function pmcheck
1341 %* *
1342 %************************************************************************
1343
1344 Main functions are:
1345
1346 * mkInitialUncovered :: [Id] -> PmM Uncovered
1347
1348 Generates the initial uncovered set. Term and type constraints in scope
1349 are checked, if they are inconsistent, the set is empty, otherwise, the
1350 set contains only a vector of variables with the constraints in scope.
1351
1352 * pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1353
1354 Checks redundancy, coverage and inaccessibility, using auxilary functions
1355 `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
1356 common in all three checks (see paper) and calls `pmcheckGuards` when the
1357 whole clause is checked, or `pmcheckHd` when the pattern vector does not
1358 start with a guard.
1359
1360 * pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1361
1362 Processes the guards.
1363
1364 * pmcheckHd :: Pattern -> PatVec -> [PatVec]
1365 -> ValAbs -> ValVec -> PmM PartialResult
1366
1367 Worker: This function implements functions `covered`, `uncovered` and
1368 `divergent` from the paper at once. Slightly different from the paper because
1369 it does not even produce the covered and uncovered sets. Since we only care
1370 about whether a clause covers SOMETHING or if it may forces ANY argument, we
1371 only store a boolean in both cases, for efficiency.
1372 -}
1373
1374 -- | Lift a pattern matching action from a single value vector abstration to a
1375 -- value set abstraction, but calling it on every vector and the combining the
1376 -- results.
1377 runMany :: (ValVec -> PmM PartialResult) -> (Uncovered -> PmM PartialResult)
1378 runMany _ [] = return mempty
1379 runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms
1380
1381 -- | Generate the initial uncovered set. It initializes the
1382 -- delta with all term and type constraints in scope.
1383 mkInitialUncovered :: [Id] -> PmM Uncovered
1384 mkInitialUncovered vars = do
1385 ty_cs <- liftD getDictsDs
1386 tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
1387 sat_ty <- tyOracle ty_cs
1388 let initTyCs = if sat_ty then ty_cs else emptyBag
1389 initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
1390 patterns = map PmVar vars
1391 -- If any of the term/type constraints are non
1392 -- satisfiable then return with the initialTmState. See #12957
1393 return [ValVec patterns (MkDelta initTyCs initTmState)]
1394
1395 -- | Increase the counter for elapsed algorithm iterations, check that the
1396 -- limit is not exceeded and call `pmcheck`
1397 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1398 pmcheckI ps guards vva = do
1399 n <- liftD incrCheckPmIterDs
1400 tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
1401 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1402 $$ pprValVecDebug vva)
1403 res <- pmcheck ps guards vva
1404 tracePm "pmCheckResult:" (ppr res)
1405 return res
1406 {-# INLINE pmcheckI #-}
1407
1408 -- | Increase the counter for elapsed algorithm iterations, check that the
1409 -- limit is not exceeded and call `pmcheckGuards`
1410 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
1411 pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
1412 {-# INLINE pmcheckGuardsI #-}
1413
1414 -- | Increase the counter for elapsed algorithm iterations, check that the
1415 -- limit is not exceeded and call `pmcheckHd`
1416 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1417 -> PmM PartialResult
1418 pmcheckHdI p ps guards va vva = do
1419 n <- liftD incrCheckPmIterDs
1420 tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
1421 $$ pprPatVec ps
1422 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1423 $$ pprPmPatDebug va
1424 $$ pprValVecDebug vva)
1425
1426 res <- pmcheckHd p ps guards va vva
1427 tracePm "pmCheckHdI: res" (ppr res)
1428 return res
1429 {-# INLINE pmcheckHdI #-}
1430
1431 -- | Matching function: Check simultaneously a clause (takes separately the
1432 -- patterns and the list of guards) for exhaustiveness, redundancy and
1433 -- inaccessibility.
1434 pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1435 pmcheck [] guards vva@(ValVec [] _)
1436 | null guards = return $ mempty { presultCovered = Covered }
1437 | otherwise = pmcheckGuardsI guards vva
1438
1439 -- Guard
1440 pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta)
1441 -- short-circuit if the guard pattern is useless.
1442 -- we just have two possible outcomes: fail here or match and recurse
1443 -- none of the two contains any useful information about the failure
1444 -- though. So just have these two cases but do not do all the boilerplate
1445 | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
1446 | otherwise = do
1447 y <- liftD $ mkPmId (pmPatType p)
1448 let tm_state = extendSubst y e (delta_tm_cs delta)
1449 delta' = delta { delta_tm_cs = tm_state }
1450 utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
1451
1452 pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
1453 pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
1454
1455 pmcheck (p:ps) guards (ValVec (va:vva) delta)
1456 = pmcheckHdI p ps guards va (ValVec vva delta)
1457
1458 -- | Check the list of guards
1459 pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1460 pmcheckGuards [] vva = return (usimple [vva])
1461 pmcheckGuards (gv:gvs) vva = do
1462 (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva
1463 (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
1464 return $ PartialResult (prov1 `mappend` prov2)
1465 (cs `mappend` css)
1466 vsas
1467 (ds `mappend` dss)
1468
1469 -- | Worker function: Implements all cases described in the paper for all three
1470 -- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
1471 -- cases which are handled by `pmcheck`
1472 pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1473 -> PmM PartialResult
1474
1475 -- Var
1476 pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
1477 | Just tm_state <- solveOneEq (delta_tm_cs delta)
1478 (PmExprVar (idName x), vaToPmExpr va)
1479 = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
1480 | otherwise = return mempty
1481
1482 -- ConCon
1483 pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
1484 (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
1485 | c1 /= c2 =
1486 return (usimple [ValVec (va:vva) delta])
1487 | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
1488 <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)
1489
1490 -- LitLit
1491 pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
1492 case eqPmLit l1 l2 of
1493 True -> ucon va <$> pmcheckI ps guards vva
1494 False -> return $ ucon va (usimple [vva])
1495
1496 -- ConVar
1497 pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
1498 ps guards
1499 (PmVar x) (ValVec vva delta) = do
1500 (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
1501
1502 cons_cs <- mapM (liftD . mkOneConFull x) complete_match
1503
1504 inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
1505 let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
1506 sat_ty <- if isEmptyBag ty_cs then return True
1507 else tyOracle ty_state
1508 return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
1509 (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
1510 _ty_or_tm_failed -> []
1511
1512 set_provenance prov .
1513 force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1514 runMany (pmcheckI (p:ps) guards) inst_vsa
1515
1516 -- LitVar
1517 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
1518 = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1519 mkUnion non_matched <$>
1520 case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
1521 Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
1522 ValVec vva (delta {delta_tm_cs = tm_state})
1523 Nothing -> return mempty
1524 where
1525 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1526 = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
1527 | otherwise = []
1528
1529 non_matched = usimple us
1530
1531 -- LitNLit
1532 pmcheckHd (p@(PmLit l)) ps guards
1533 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
1534 | all (not . eqPmLit l) lits
1535 , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
1536 -- Both guards check the same so it would be sufficient to have only
1537 -- the second one. Nevertheless, it is much cheaper to check whether
1538 -- the literal is in the list so we check it first, to avoid calling
1539 -- the term oracle (`solveOneEq`) if possible
1540 = mkUnion non_matched <$>
1541 pmcheckHdI p ps guards (PmLit l)
1542 (ValVec vva (delta { delta_tm_cs = tm_state }))
1543 | otherwise = return non_matched
1544 where
1545 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1546 = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
1547 | otherwise = []
1548
1549 non_matched = usimple us
1550
1551 -- ----------------------------------------------------------------------------
1552 -- The following three can happen only in cases like #322 where constructors
1553 -- and overloaded literals appear in the same match. The general strategy is
1554 -- to replace the literal (positive/negative) by a variable and recurse. The
1555 -- fact that the variable is equal to the literal is recorded in `delta` so
1556 -- no information is lost
1557
1558 -- LitCon
1559 pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
1560 = do y <- liftD $ mkPmId (pmPatType va)
1561 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1562 delta' = delta { delta_tm_cs = tm_state }
1563 pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
1564
1565 -- ConLit
1566 pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
1567 = do y <- liftD $ mkPmId (pmPatType p)
1568 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1569 delta' = delta { delta_tm_cs = tm_state }
1570 pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
1571
1572 -- ConNLit
1573 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
1574 = pmcheckHdI p ps guards (PmVar x) vva
1575
1576 -- Impossible: handled by pmcheck
1577 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
1578
1579 -- ----------------------------------------------------------------------------
1580 -- * Utilities for main checking
1581
1582 updateVsa :: (ValSetAbs -> ValSetAbs) -> (PartialResult -> PartialResult)
1583 updateVsa f p@(PartialResult { presultUncovered = old })
1584 = p { presultUncovered = f old }
1585
1586
1587 -- | Initialise with default values for covering and divergent information.
1588 usimple :: ValSetAbs -> PartialResult
1589 usimple vsa = mempty { presultUncovered = vsa }
1590
1591 -- | Take the tail of all value vector abstractions in the uncovered set
1592 utail :: PartialResult -> PartialResult
1593 utail = updateVsa upd
1594 where upd vsa = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ]
1595
1596 -- | Prepend a value abstraction to all value vector abstractions in the
1597 -- uncovered set
1598 ucon :: ValAbs -> PartialResult -> PartialResult
1599 ucon va = updateVsa upd
1600 where
1601 upd vsa = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ]
1602
1603 -- | Given a data constructor of arity `a` and an uncovered set containing
1604 -- value vector abstractions of length `(a+n)`, pass the first `n` value
1605 -- abstractions to the constructor (Hence, the resulting value vector
1606 -- abstractions will have length `n+1`)
1607 kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
1608 -> PartialResult -> PartialResult
1609 kcon con arg_tys ex_tvs dicts
1610 = let n = conLikeArity con
1611 upd vsa =
1612 [ ValVec (va:vva) delta
1613 | ValVec vva' delta <- vsa
1614 , let (args, vva) = splitAt n vva'
1615 , let va = PmCon { pm_con_con = con
1616 , pm_con_arg_tys = arg_tys
1617 , pm_con_tvs = ex_tvs
1618 , pm_con_dicts = dicts
1619 , pm_con_args = args } ]
1620 in updateVsa upd
1621
1622 -- | Get the union of two covered, uncovered and divergent value set
1623 -- abstractions. Since the covered and divergent sets are represented by a
1624 -- boolean, union means computing the logical or (at least one of the two is
1625 -- non-empty).
1626
1627 mkUnion :: PartialResult -> PartialResult -> PartialResult
1628 mkUnion = mappend
1629
1630 -- | Add a value vector abstraction to a value set abstraction (uncovered).
1631 mkCons :: ValVec -> PartialResult -> PartialResult
1632 mkCons vva = updateVsa (vva:)
1633
1634 -- | Set the divergent set to not empty
1635 forces :: PartialResult -> PartialResult
1636 forces pres = pres { presultDivergent = Diverged }
1637
1638 -- | Set the divergent set to non-empty if the flag is `True`
1639 force_if :: Bool -> PartialResult -> PartialResult
1640 force_if True pres = forces pres
1641 force_if False pres = pres
1642
1643 set_provenance :: Provenance -> PartialResult -> PartialResult
1644 set_provenance prov pr = pr { presultProvenance = prov }
1645
1646 -- ----------------------------------------------------------------------------
1647 -- * Propagation of term constraints inwards when checking nested matches
1648
1649 {- Note [Type and Term Equality Propagation]
1650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1651 When checking a match it would be great to have all type and term information
1652 available so we can get more precise results. For this reason we have functions
1653 `addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
1654 term constraints (respectively) as we go deeper.
1655
1656 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1657 in HsPat.hs. This handles bug #4139 ( see example
1658 https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
1659 where this is needed.
1660
1661 For term equalities we do less, we just generate equalities for HsCase. For
1662 example we accurately give 2 redundancy warnings for the marked cases:
1663
1664 f :: [a] -> Bool
1665 f x = case x of
1666
1667 [] -> case x of -- brings (x ~ []) in scope
1668 [] -> True
1669 (_:_) -> False -- can't happen
1670
1671 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1672 (_:_) -> True
1673 [] -> False -- can't happen
1674
1675 Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
1676 these constraints.
1677 -}
1678
1679 -- | Generate equalities when checking a case expression:
1680 -- case x of { p1 -> e1; ... pn -> en }
1681 -- When we go deeper to check e.g. e1 we record two equalities:
1682 -- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
1683 -- and (x ~ p1).
1684 genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
1685 -> [Pat GhcTc] -- LHS (should have length 1)
1686 -> [Id] -- MatchVars (should have length 1)
1687 -> DsM (Bag SimpleEq)
1688 genCaseTmCs2 Nothing _ _ = return emptyBag
1689 genCaseTmCs2 (Just scr) [p] [var] = do
1690 fam_insts <- dsGetFamInstEnvs
1691 [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
1692 let scr_e = lhsExprToPmExpr scr
1693 return $ listToBag [(var, e), (var, scr_e)]
1694 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
1695
1696 -- | Generate a simple equality when checking a case expression:
1697 -- case x of { matches }
1698 -- When checking matches we record that (x ~ y) where y is the initial
1699 -- uncovered. All matches will have to satisfy this equality.
1700 genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag SimpleEq
1701 genCaseTmCs1 Nothing _ = emptyBag
1702 genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
1703 genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
1704
1705 {- Note [Literals in PmPat]
1706 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1707 Instead of translating a literal to a variable accompanied with a guard, we
1708 treat them like constructor patterns. The following example from
1709 "./libraries/base/GHC/IO/Encoding.hs" shows why:
1710
1711 mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
1712 mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
1713 "UTF8" -> return $ UTF8.mkUTF8 cfm
1714 "UTF16" -> return $ UTF16.mkUTF16 cfm
1715 "UTF16LE" -> return $ UTF16.mkUTF16le cfm
1716 ...
1717
1718 Each clause gets translated to a list of variables with an equal number of
1719 guards. For every guard we generate two cases (equals True/equals False) which
1720 means that we generate 2^n cases to feed the oracle with, where n is the sum of
1721 the length of all strings that appear in the patterns. For this particular
1722 example this means over 2^40 cases. Instead, by representing them like with
1723 constructor we get the following:
1724 1. We exploit the common prefix with our representation of VSAs
1725 2. We prune immediately non-reachable cases
1726 (e.g. False == (x == "U"), True == (x == "U"))
1727
1728 Note [Translating As Patterns]
1729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1730 Instead of translating x@p as: x (p <- x)
1731 we instead translate it as: p (x <- coercePattern p)
1732 for performance reasons. For example:
1733
1734 f x@True = 1
1735 f y@False = 2
1736
1737 Gives the following with the first translation:
1738
1739 x |> {x == False, x == y, y == True}
1740
1741 If we use the second translation we get an empty set, independently of the
1742 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
1743 used as an expression. That's why we call `coercePatVec' to drop the guard and
1744 `vaToPmExpr' to transform the value abstraction to an expression in the
1745 guard pattern (value abstractions are a subset of expressions). We keep the
1746 guards in the first pattern `p' though.
1747
1748
1749 %************************************************************************
1750 %* *
1751 Pretty printing of exhaustiveness/redundancy check warnings
1752 %* *
1753 %************************************************************************
1754 -}
1755
1756 -- | Check whether any part of pattern match checking is enabled (does not
1757 -- matter whether it is the redundancy check or the exhaustiveness check).
1758 isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
1759 isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
1760 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
1761
1762 instance Outputable ValVec where
1763 ppr (ValVec vva delta)
1764 = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
1765 vector = substInValAbs subst vva
1766 in ppr_uncovered (vector, residual_eqs)
1767
1768 -- | Apply a term substitution to a value vector abstraction. All VAs are
1769 -- transformed to PmExpr (used only before pretty printing).
1770 substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
1771 substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
1772
1773 -- | Wrap up the term oracle's state once solving is complete. Drop any
1774 -- information about unhandled constraints (involving HsExprs) and flatten
1775 -- (height 1) the substitution.
1776 wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
1777 wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
1778
1779 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
1780 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
1781 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
1782 = when (flag_i || flag_u) $ do
1783 let exists_r = flag_i && notNull redundant && onlyBuiltin
1784 exists_i = flag_i && notNull inaccessible && onlyBuiltin && not is_rec_upd
1785 exists_u = flag_u && (case uncovered of
1786 TypeOfUncovered _ -> True
1787 UncoveredPatterns u -> notNull u)
1788
1789 when exists_r $ forM_ redundant $ \(L l q) -> do
1790 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1791 (pprEqn q "is redundant"))
1792 when exists_i $ forM_ inaccessible $ \(L l q) -> do
1793 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1794 (pprEqn q "has inaccessible right hand side"))
1795 when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
1796 case uncovered of
1797 TypeOfUncovered ty -> warnEmptyCase ty
1798 UncoveredPatterns candidates -> pprEqns candidates
1799 where
1800 PmResult
1801 { pmresultProvenance = prov
1802 , pmresultRedundant = redundant
1803 , pmresultUncovered = uncovered
1804 , pmresultInaccessible = inaccessible } = pm_result
1805
1806 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1807 flag_u = exhaustive dflags kind
1808 flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
1809
1810 is_rec_upd = case kind of { RecUpd -> True; _ -> False }
1811 -- See Note [Inaccessible warnings for record updates]
1812
1813 onlyBuiltin = prov == FromBuiltin
1814
1815 maxPatterns = maxUncoveredPatterns dflags
1816
1817 -- Print a single clause (for redundant/with-inaccessible-rhs)
1818 pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
1819
1820 -- Print several clauses (for uncovered clauses)
1821 pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
1822 case qs of -- See #11245
1823 [ValVec [] _]
1824 -> text "Guards do not cover entire pattern space"
1825 _missing -> let us = map ppr qs
1826 in hang (text "Patterns not matched:") 4
1827 (vcat (take maxPatterns us)
1828 $$ dots maxPatterns us)
1829
1830 -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
1831 -- which we only know the type and have no inhabitants at hand)
1832 warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
1833 hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
1834
1835 {- Note [Inaccessible warnings for record updates]
1836 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1837 Consider (Trac #12957)
1838 data T a where
1839 T1 :: { x :: Int } -> T Bool
1840 T2 :: { x :: Int } -> T a
1841 T3 :: T a
1842
1843 f :: T Char -> T a
1844 f r = r { x = 3 }
1845
1846 The desugarer will (conservatively generate a case for T1 even though
1847 it's impossible:
1848 f r = case r of
1849 T1 x -> T1 3 -- Inaccessible branch
1850 T2 x -> T2 3
1851 _ -> error "Missing"
1852
1853 We don't want to warn about the inaccessible branch because the programmer
1854 didn't put it there! So we filter out the warning here.
1855 -}
1856
1857 -- | Issue a warning when the predefined number of iterations is exceeded
1858 -- for the pattern match checker
1859 warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
1860 warnPmIters dflags (DsMatchContext kind loc)
1861 = when (flag_i || flag_u) $ do
1862 iters <- maxPmCheckIterations <$> getDynFlags
1863 putSrcSpanDs loc (warnDs NoReason (msg iters))
1864 where
1865 ctxt = pprMatchContext kind
1866 msg is = fsep [ text "Pattern match checker exceeded"
1867 , parens (ppr is), text "iterations in", ctxt <> dot
1868 , text "(Use -fmax-pmcheck-iterations=n"
1869 , text "to set the maximun number of iterations to n)" ]
1870
1871 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1872 flag_u = exhaustive dflags kind
1873
1874 dots :: Int -> [a] -> SDoc
1875 dots maxPatterns qs
1876 | qs `lengthExceeds` maxPatterns = text "..."
1877 | otherwise = empty
1878
1879 -- | Check whether the exhaustiveness checker should run (exhaustiveness only)
1880 exhaustive :: DynFlags -> HsMatchContext id -> Bool
1881 exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
1882
1883 -- | Denotes whether an exhaustiveness check is supported, and if so,
1884 -- via which 'WarningFlag' it's controlled.
1885 -- Returns 'Nothing' if check is not supported.
1886 exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
1887 exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
1888 exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
1889 exhaustiveWarningFlag IfAlt = Nothing
1890 exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
1891 exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
1892 exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
1893 exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
1894 exhaustiveWarningFlag ThPatSplice = Nothing
1895 exhaustiveWarningFlag PatSyn = Nothing
1896 exhaustiveWarningFlag ThPatQuote = Nothing
1897 exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns
1898 -- in list comprehensions, pattern guards
1899 -- etc. They are often *supposed* to be
1900 -- incomplete
1901
1902 -- True <==> singular
1903 pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
1904 pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
1905 = vcat [text txt <+> msg,
1906 sep [ text "In" <+> ppr_match <> char ':'
1907 , nest 4 (rest_of_msg_fun pref)]]
1908 where
1909 txt | singular = "Pattern match"
1910 | otherwise = "Pattern match(es)"
1911
1912 (ppr_match, pref)
1913 = case kind of
1914 FunRhs { mc_fun = L _ fun }
1915 -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
1916 _ -> (pprMatchContext kind, \ pp -> pp)
1917
1918 ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
1919 ppr_pats kind pats
1920 = sep [sep (map ppr pats), matchSeparator kind, text "..."]
1921
1922 ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
1923 ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
1924
1925 ppr_constraint :: (SDoc,[PmLit]) -> SDoc
1926 ppr_constraint (var, lits) = var <+> text "is not one of"
1927 <+> braces (pprWithCommas ppr lits)
1928
1929 ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
1930 ppr_uncovered (expr_vec, complex)
1931 | null cs = fsep vec -- there are no literal constraints
1932 | otherwise = hang (fsep vec) 4 $
1933 text "where" <+> vcat (map ppr_constraint cs)
1934 where
1935 sdoc_vec = mapM pprPmExprWithParens expr_vec
1936 (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
1937
1938 {- Note [Representation of Term Equalities]
1939 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1940 In the paper, term constraints always take the form (x ~ e). Of course, a more
1941 general constraint of the form (e1 ~ e1) can always be transformed to an
1942 equivalent set of the former constraints, by introducing a fresh, intermediate
1943 variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
1944 to #11160 (incredibly bad performance for literal pattern matching). Two are
1945 the main sources of this problem (the actual problem is how these two interact
1946 with each other):
1947
1948 1. Pattern matching on literals generates twice as many constraints as needed.
1949 Consider the following (tests/ghci/should_run/ghcirun004):
1950
1951 foo :: Int -> Int
1952 foo 1 = 0
1953 ...
1954 foo 5000 = 4999
1955
1956 The covered and uncovered set *should* look like:
1957 U0 = { x |> {} }
1958
1959 C1 = { 1 |> { x ~ 1 } }
1960 U1 = { x |> { False ~ (x ~ 1) } }
1961 ...
1962 C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
1963 U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
1964 ...
1965
1966 If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
1967 we get twice as many constraints. Also note that half of them are just the
1968 substitution [x |-> False].
1969
1970 2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
1971 (x ~ e) as substitutions [x |-> e]. More specifically, function
1972 `extendSubstAndSolve` applies such substitutions in the residual constraints
1973 and partitions them in the affected and non-affected ones, which are the new
1974 worklist. Essentially, this gives quadradic behaviour on the number of the
1975 residual constraints. (This would not be the case if the term oracle used
1976 mutable variables but, since we use it to handle disjunctions on value set
1977 abstractions (`Union` case), we chose a pure, incremental interface).
1978
1979 Now the problem becomes apparent (e.g. for clause 300):
1980 * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
1981 constraints that we know that will not reduce (stay in the worklist).
1982 * To check for consistency, we apply the substituting constraints ONE BY ONE
1983 (since `tmOracle` is called incrementally, it does not have all of them
1984 available at once). Hence, we go through the (non-progressing) constraints
1985 over and over, achieving over-quadradic behaviour.
1986
1987 If instead we allow constraints of the form (e ~ e),
1988 * All uncovered sets Ui contain no substituting constraints and i
1989 non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
1990 behaves linearly.
1991 * All covered sets Ci contain exactly (i-1) non-progressing constraints and
1992 a single substituting constraint. So the term oracle goes through the
1993 constraints only once.
1994
1995 The performance improvement becomes even more important when more arguments are
1996 involved.
1997 -}
1998
1999 -- Debugging Infrastructre
2000
2001 tracePm :: String -> SDoc -> PmM ()
2002 tracePm herald doc = liftD $ tracePmD herald doc
2003
2004
2005 tracePmD :: String -> SDoc -> DsM ()
2006 tracePmD herald doc = do
2007 dflags <- getDynFlags
2008 printer <- mkPrintUnqualifiedDs
2009 liftIO $ dumpIfSet_dyn_printer printer dflags
2010 Opt_D_dump_ec_trace (text herald $$ (nest 2 doc))
2011
2012
2013 pprPmPatDebug :: PmPat a -> SDoc
2014 pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
2015 = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
2016 pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
2017 pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
2018 pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
2019 pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv)
2020 <+> ppr ge
2021
2022 pprPatVec :: PatVec -> SDoc
2023 pprPatVec ps = hang (text "Pattern:") 2
2024 (brackets $ sep
2025 $ punctuate (comma <> char '\n') (map pprPmPatDebug ps))
2026
2027 pprValAbs :: [ValAbs] -> SDoc
2028 pprValAbs ps = hang (text "ValAbs:") 2
2029 (brackets $ sep
2030 $ punctuate (comma) (map pprPmPatDebug ps))
2031
2032 pprValVecDebug :: ValVec -> SDoc
2033 pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
2034 parens (pprValAbs vas)