Merge remote-tracking branch 'github/pr/83'
[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 }
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 SigPatOut p _ty -> 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 (L _ _n) _k1 _k2 _ge _minus ty -> mkCanFailPmPat ty
755
756 -- (fun -> pat) ===> x (pat <- fun x)
757 ViewPat lexpr lpat arg_ty -> 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 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 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 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 (L _ ol) mb_neg _eq ty -> 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 (map (LitPat . HsChar src) (unpackFS s))
809 | otherwise -> return [mkLitPattern lit]
810
811 PArrPat ps ty -> do
812 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
813 let fake_con = RealDataCon (parrFakeCon (length ps))
814 return [vanillaConPattern fake_con [ty] (concat tidy_ps)]
815
816 TuplePat ps boxity tys -> do
817 tidy_ps <- translatePatVec fam_insts (map unLoc ps)
818 let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
819 return [vanillaConPattern tuple_con tys (concat tidy_ps)]
820
821 SumPat p alt arity ty -> do
822 tidy_p <- translatePat fam_insts (unLoc p)
823 let sum_con = RealDataCon (sumDataCon alt arity)
824 return [vanillaConPattern sum_con ty tidy_p]
825
826 -- --------------------------------------------------------------------------
827 -- Not supposed to happen
828 ConPatIn {} -> panic "Check.translatePat: ConPatIn"
829 SplicePat {} -> panic "Check.translatePat: SplicePat"
830 SigPatIn {} -> panic "Check.translatePat: SigPatIn"
831
832 -- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
833 translateNPat :: FamInstEnvs
834 -> HsOverLit GhcTc -> Maybe (SyntaxExpr GhcTc) -> Type
835 -> DsM PatVec
836 translateNPat fam_insts (OverLit val False _ ty) mb_neg outer_ty
837 | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
838 = translatePat fam_insts (LitPat (HsString src s))
839 | not type_change, isIntTy ty, HsIntegral i <- val
840 = translatePat fam_insts
841 (LitPat $ case mb_neg of
842 Nothing -> HsInt def i
843 Just _ -> HsInt def (negateIntegralLit i))
844 | not type_change, isWordTy ty, HsIntegral i <- val
845 = translatePat fam_insts
846 (LitPat $ case mb_neg of
847 Nothing -> HsWordPrim (il_text i) (il_value i)
848 Just _ -> let ni = negateIntegralLit i in
849 HsWordPrim (il_text ni) (il_value ni))
850 where
851 type_change = not (outer_ty `eqType` ty)
852
853 translateNPat _ ol mb_neg _
854 = return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) ol }]
855
856 -- | Translate a list of patterns (Note: each pattern is translated
857 -- to a pattern vector but we do not concatenate the results).
858 translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
859 translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
860
861 -- | Translate a constructor pattern
862 translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
863 -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
864 translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
865 = concat <$> translatePatVec fam_insts (map unLoc ps)
866 translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
867 = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
868 translateConPatVec fam_insts univ_tys ex_tvs c (RecCon (HsRecFields fs _))
869 -- Nothing matched. Make up some fresh term variables
870 | null fs = mkPmVars arg_tys
871 -- The data constructor was not defined using record syntax. For the
872 -- pattern to be in record syntax it should be empty (e.g. Just {}).
873 -- So just like the previous case.
874 | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
875 -- Some of the fields appear, in the original order (there may be holes).
876 -- Generate a simple constructor pattern and make up fresh variables for
877 -- the rest of the fields
878 | matched_lbls `subsetOf` orig_lbls
879 = ASSERT(orig_lbls `equalLength` arg_tys)
880 let translateOne (lbl, ty) = case lookup lbl matched_pats of
881 Just p -> translatePat fam_insts p
882 Nothing -> mkPmVars [ty]
883 in concatMapM translateOne (zip orig_lbls arg_tys)
884 -- The fields that appear are not in the correct order. Make up fresh
885 -- variables for all fields and add guards after matching, to force the
886 -- evaluation in the correct order.
887 | otherwise = do
888 arg_var_pats <- mkPmVars arg_tys
889 translated_pats <- forM matched_pats $ \(x,pat) -> do
890 pvec <- translatePat fam_insts pat
891 return (x, pvec)
892
893 let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
894 guards = map (\(name,pvec) -> case lookup name zipped of
895 Just x -> PmGrd pvec (PmExprVar (idName x))
896 Nothing -> panic "translateConPatVec: lookup")
897 translated_pats
898
899 return (arg_var_pats ++ guards)
900 where
901 -- The actual argument types (instantiated)
902 arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
903
904 -- Some label information
905 orig_lbls = map flSelector $ conLikeFieldLabels c
906 matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
907 | L _ x <- fs]
908 matched_lbls = [ name | (name, _pat) <- matched_pats ]
909
910 subsetOf :: Eq a => [a] -> [a] -> Bool
911 subsetOf [] _ = True
912 subsetOf (_:_) [] = False
913 subsetOf (x:xs) (y:ys)
914 | x == y = subsetOf xs ys
915 | otherwise = subsetOf (x:xs) ys
916
917 -- Translate a single match
918 translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
919 -> DsM (PatVec,[PatVec])
920 translateMatch fam_insts (L _ (Match { m_pats = lpats, m_grhss = grhss })) = do
921 pats' <- concat <$> translatePatVec fam_insts pats
922 guards' <- mapM (translateGuards fam_insts) guards
923 return (pats', guards')
924 where
925 extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
926 extractGuards (L _ (GRHS gs _)) = map unLoc gs
927
928 pats = map unLoc lpats
929 guards = map extractGuards (grhssGRHSs grhss)
930
931 -- -----------------------------------------------------------------------
932 -- * Transform source guards (GuardStmt Id) to PmPats (Pattern)
933
934 -- | Translate a list of guard statements to a pattern vector
935 translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
936 translateGuards fam_insts guards = do
937 all_guards <- concat <$> mapM (translateGuard fam_insts) guards
938 return (replace_unhandled all_guards)
939 -- It should have been (return all_guards) but it is too expressive.
940 -- Since the term oracle does not handle all constraints we generate,
941 -- we (hackily) replace all constraints the oracle cannot handle with a
942 -- single one (we need to know if there is a possibility of falure).
943 -- See Note [Guards and Approximation] for all guard-related approximations
944 -- we implement.
945 where
946 replace_unhandled :: PatVec -> PatVec
947 replace_unhandled gv
948 | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
949 | otherwise = gv
950
951 any_unhandled :: PatVec -> Bool
952 any_unhandled gv = any (not . shouldKeep) gv
953
954 shouldKeep :: Pattern -> Bool
955 shouldKeep p
956 | PmVar {} <- p = True
957 | PmCon {} <- p = singleConstructor (pm_con_con p)
958 && all shouldKeep (pm_con_args p)
959 shouldKeep (PmGrd pv e)
960 | all shouldKeep pv = True
961 | isNotPmExprOther e = True -- expensive but we want it
962 shouldKeep _other_pat = False -- let the rest..
963
964 -- | Check whether a pattern can fail to match
965 cantFailPattern :: Pattern -> Bool
966 cantFailPattern p
967 | PmVar {} <- p = True
968 | PmCon {} <- p = singleConstructor (pm_con_con p)
969 && all cantFailPattern (pm_con_args p)
970 cantFailPattern (PmGrd pv _e)
971 = all cantFailPattern pv
972 cantFailPattern _ = False
973
974 -- | Translate a guard statement to Pattern
975 translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
976 translateGuard fam_insts guard = case guard of
977 BodyStmt e _ _ _ -> translateBoolGuard e
978 LetStmt binds -> translateLet (unLoc binds)
979 BindStmt p e _ _ _ -> translateBind fam_insts p e
980 LastStmt {} -> panic "translateGuard LastStmt"
981 ParStmt {} -> panic "translateGuard ParStmt"
982 TransStmt {} -> panic "translateGuard TransStmt"
983 RecStmt {} -> panic "translateGuard RecStmt"
984 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt"
985
986 -- | Translate let-bindings
987 translateLet :: HsLocalBinds GhcTc -> DsM PatVec
988 translateLet _binds = return []
989
990 -- | Translate a pattern guard
991 translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
992 translateBind fam_insts (L _ p) e = do
993 ps <- translatePat fam_insts p
994 return [mkGuard ps (unLoc e)]
995
996 -- | Translate a boolean guard
997 translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
998 translateBoolGuard e
999 | isJust (isTrueLHsExpr e) = return []
1000 -- The formal thing to do would be to generate (True <- True)
1001 -- but it is trivial to solve so instead we give back an empty
1002 -- PatVec for efficiency
1003 | otherwise = return [mkGuard [truePattern] (unLoc e)]
1004
1005 {- Note [Guards and Approximation]
1006 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1007 Even if the algorithm is really expressive, the term oracle we use is not.
1008 Hence, several features are not translated *properly* but we approximate.
1009 The list includes:
1010
1011 1. View Patterns
1012 ----------------
1013 A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
1014 oracle does not handle function applications so we know that the generated
1015 constraints will not be handled at the end. Hence, we distinguish between two
1016 cases:
1017 a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
1018 thing*.
1019 b) Pattern @p@ can fail. This means that when checking the guard, we will
1020 generate several cases, with no useful information. E.g.:
1021
1022 h (f -> [a,b]) = ...
1023 h x ([a,b] <- f x) = ...
1024
1025 uncovered set = { [x |> { False ~ (f x ~ []) }]
1026 , [x |> { False ~ (f x ~ (t1:[])) }]
1027 , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }
1028
1029 So we have two problems:
1030 1) Since we do not print the constraints in the general case (they may
1031 be too many), the warning will look like this:
1032
1033 Pattern match(es) are non-exhaustive
1034 In an equation for `h':
1035 Patterns not matched:
1036 _
1037 _
1038 _
1039 Which is not short and not more useful than a single underscore.
1040 2) The size of the uncovered set increases a lot, without gaining more
1041 expressivity in our warnings.
1042
1043 Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
1044 @fake_pat@: @True <- _@. That is, we record that there is a possibility
1045 of failure but we minimize it to a True/False. This generates a single
1046 warning and much smaller uncovered sets.
1047
1048 2. Overloaded Lists
1049 -------------------
1050 An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
1051 problem is exactly like above, as its solution. For future reference, the code
1052 below is the *right thing to do*:
1053
1054 ListPat lpats elem_ty (Just (pat_ty, to_list))
1055 otherwise -> do
1056 (xp, xe) <- mkPmId2Forms pat_ty
1057 ps <- translatePatVec (map unLoc lpats)
1058 let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
1059 g = mkGuard pats (HsApp (noLoc to_list) xe)
1060 return [xp,g]
1061
1062 3. Overloaded Literals
1063 ----------------------
1064 The case with literals is a bit different. a literal @l@ should be translated
1065 to @x (True <- x == from l)@. Since we want to have better warnings for
1066 overloaded literals as it is a very common feature, we treat them differently.
1067 They are mainly covered in Note [Undecidable Equality on Overloaded Literals]
1068 in PmExpr.
1069
1070 4. N+K Patterns & Pattern Synonyms
1071 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1072 An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
1073 Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
1074 and has two possible outcomes. Hence, there is no benefit in using a dummy and
1075 we implement the proper thing. Pattern synonyms are simply not implemented yet.
1076 Hence, to be conservative, we generate a dummy pattern, assuming that the
1077 pattern can fail.
1078
1079 5. Actual Guards
1080 ----------------
1081 During translation, boolean guards and pattern guards are translated properly.
1082 Let bindings though are omitted by function @translateLet@. Since they are lazy
1083 bindings, we do not actually want to generate a (strict) equality (like we do
1084 in the pattern bind case). Hence, we safely drop them.
1085
1086 Additionally, top-level guard translation (performed by @translateGuards@)
1087 replaces guards that cannot be reasoned about (like the ones we described in
1088 1-4) with a single @fake_pat@ to record the possibility of failure to match.
1089
1090 Note [Translate CoPats]
1091 ~~~~~~~~~~~~~~~~~~~~~~~
1092 The pattern match checker did not know how to handle coerced patterns `CoPat`
1093 efficiently, which gave rise to #11276. The original approach translated
1094 `CoPat`s:
1095
1096 pat |> co ===> x (pat <- (e |> co))
1097
1098 Instead, we now check whether the coercion is a hole or if it is just refl, in
1099 which case we can drop it. Unfortunately, data families generate useful
1100 coercions so guards are still generated in these cases and checking data
1101 families is not really efficient.
1102
1103 %************************************************************************
1104 %* *
1105 Utilities for Pattern Match Checking
1106 %* *
1107 %************************************************************************
1108 -}
1109
1110 -- ----------------------------------------------------------------------------
1111 -- * Basic utilities
1112
1113 -- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
1114 -- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
1115 pmPatType :: PmPat p -> Type
1116 pmPatType (PmCon { pm_con_con = con, pm_con_arg_tys = tys })
1117 = conLikeResTy con tys
1118 pmPatType (PmVar { pm_var_id = x }) = idType x
1119 pmPatType (PmLit { pm_lit_lit = l }) = pmLitType l
1120 pmPatType (PmNLit { pm_lit_id = x }) = idType x
1121 pmPatType (PmGrd { pm_grd_pv = pv })
1122 = ASSERT(patVecArity pv == 1) (pmPatType p)
1123 where Just p = find ((==1) . patternArity) pv
1124
1125 -- | Generate a value abstraction for a given constructor (generate
1126 -- fresh variables of the appropriate type for arguments)
1127 mkOneConFull :: Id -> ConLike -> DsM (ValAbs, ComplexEq, Bag EvVar)
1128 -- * x :: T tys, where T is an algebraic data type
1129 -- NB: in the case of a data family, T is the *representation* TyCon
1130 -- e.g. data instance T (a,b) = T1 a b
1131 -- leads to
1132 -- data TPair a b = T1 a b -- The "representation" type
1133 -- It is TPair, not T, that is given to mkOneConFull
1134 --
1135 -- * 'con' K is a constructor of data type T
1136 --
1137 -- After instantiating the universal tyvars of K we get
1138 -- K tys :: forall bs. Q => s1 .. sn -> T tys
1139 --
1140 -- Results: ValAbs: K (y1::s1) .. (yn::sn)
1141 -- ComplexEq: x ~ K y1..yn
1142 -- [EvVar]: Q
1143 mkOneConFull x con = do
1144 let res_ty = idType x
1145 (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , arg_tys, con_res_ty)
1146 = conLikeFullSig con
1147 tc_args = tyConAppArgs res_ty
1148 subst1 = case con of
1149 RealDataCon {} -> zipTvSubst univ_tvs tc_args
1150 PatSynCon {} -> expectJust "mkOneConFull" (tcMatchTy con_res_ty res_ty)
1151 -- See Note [Pattern synonym result type] in PatSyn
1152
1153 (subst, ex_tvs') <- cloneTyVarBndrs subst1 ex_tvs <$> getUniqueSupplyM
1154
1155 -- Fresh term variables (VAs) as arguments to the constructor
1156 arguments <- mapM mkPmVar (substTys subst arg_tys)
1157 -- All constraints bound by the constructor (alpha-renamed)
1158 let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
1159 evvars <- mapM (nameType "pm") theta_cs
1160 let con_abs = PmCon { pm_con_con = con
1161 , pm_con_arg_tys = tc_args
1162 , pm_con_tvs = ex_tvs'
1163 , pm_con_dicts = evvars
1164 , pm_con_args = arguments }
1165 return (con_abs, (PmExprVar (idName x), vaToPmExpr con_abs), listToBag evvars)
1166
1167 -- ----------------------------------------------------------------------------
1168 -- * More smart constructors and fresh variable generation
1169
1170 -- | Create a guard pattern
1171 mkGuard :: PatVec -> HsExpr GhcTc -> Pattern
1172 mkGuard pv e
1173 | all cantFailPattern pv = PmGrd pv expr
1174 | PmExprOther {} <- expr = fake_pat
1175 | otherwise = PmGrd pv expr
1176 where
1177 expr = hsExprToPmExpr e
1178
1179 -- | Create a term equality of the form: `(False ~ (x ~ lit))`
1180 mkNegEq :: Id -> PmLit -> ComplexEq
1181 mkNegEq x l = (falsePmExpr, PmExprVar (idName x) `PmExprEq` PmExprLit l)
1182 {-# INLINE mkNegEq #-}
1183
1184 -- | Create a term equality of the form: `(x ~ lit)`
1185 mkPosEq :: Id -> PmLit -> ComplexEq
1186 mkPosEq x l = (PmExprVar (idName x), PmExprLit l)
1187 {-# INLINE mkPosEq #-}
1188
1189 -- | Create a term equality of the form: `(x ~ x)`
1190 -- (always discharged by the term oracle)
1191 mkIdEq :: Id -> ComplexEq
1192 mkIdEq x = (PmExprVar name, PmExprVar name)
1193 where name = idName x
1194 {-# INLINE mkIdEq #-}
1195
1196 -- | Generate a variable pattern of a given type
1197 mkPmVar :: Type -> DsM (PmPat p)
1198 mkPmVar ty = PmVar <$> mkPmId ty
1199 {-# INLINE mkPmVar #-}
1200
1201 -- | Generate many variable patterns, given a list of types
1202 mkPmVars :: [Type] -> DsM PatVec
1203 mkPmVars tys = mapM mkPmVar tys
1204 {-# INLINE mkPmVars #-}
1205
1206 -- | Generate a fresh `Id` of a given type
1207 mkPmId :: Type -> DsM Id
1208 mkPmId ty = getUniqueM >>= \unique ->
1209 let occname = mkVarOccFS $ fsLit "$pm"
1210 name = mkInternalName unique occname noSrcSpan
1211 in return (mkLocalId name ty)
1212
1213 -- | Generate a fresh term variable of a given and return it in two forms:
1214 -- * A variable pattern
1215 -- * A variable expression
1216 mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
1217 mkPmId2Forms ty = do
1218 x <- mkPmId ty
1219 return (PmVar x, noLoc (HsVar (noLoc x)))
1220
1221 -- ----------------------------------------------------------------------------
1222 -- * Converting between Value Abstractions, Patterns and PmExpr
1223
1224 -- | Convert a value abstraction an expression
1225 vaToPmExpr :: ValAbs -> PmExpr
1226 vaToPmExpr (PmCon { pm_con_con = c, pm_con_args = ps })
1227 = PmExprCon c (map vaToPmExpr ps)
1228 vaToPmExpr (PmVar { pm_var_id = x }) = PmExprVar (idName x)
1229 vaToPmExpr (PmLit { pm_lit_lit = l }) = PmExprLit l
1230 vaToPmExpr (PmNLit { pm_lit_id = x }) = PmExprVar (idName x)
1231
1232 -- | Convert a pattern vector to a list of value abstractions by dropping the
1233 -- guards (See Note [Translating As Patterns])
1234 coercePatVec :: PatVec -> [ValAbs]
1235 coercePatVec pv = concatMap coercePmPat pv
1236
1237 -- | Convert a pattern to a list of value abstractions (will be either an empty
1238 -- list if the pattern is a guard pattern, or a singleton list in all other
1239 -- cases) by dropping the guards (See Note [Translating As Patterns])
1240 coercePmPat :: Pattern -> [ValAbs]
1241 coercePmPat (PmVar { pm_var_id = x }) = [PmVar { pm_var_id = x }]
1242 coercePmPat (PmLit { pm_lit_lit = l }) = [PmLit { pm_lit_lit = l }]
1243 coercePmPat (PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
1244 , pm_con_tvs = tvs, pm_con_dicts = dicts
1245 , pm_con_args = args })
1246 = [PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
1247 , pm_con_tvs = tvs, pm_con_dicts = dicts
1248 , pm_con_args = coercePatVec args }]
1249 coercePmPat (PmGrd {}) = [] -- drop the guards
1250
1251 -- | Check whether a data constructor is the only way to construct
1252 -- a data type.
1253 singleConstructor :: ConLike -> Bool
1254 singleConstructor (RealDataCon dc) =
1255 case tyConDataCons (dataConTyCon dc) of
1256 [_] -> True
1257 _ -> False
1258 singleConstructor _ = False
1259
1260 -- | For a given conlike, finds all the sets of patterns which could
1261 -- be relevant to that conlike by consulting the result type.
1262 --
1263 -- These come from two places.
1264 -- 1. From data constructors defined with the result type constructor.
1265 -- 2. From `COMPLETE` pragmas which have the same type as the result
1266 -- type constructor.
1267 allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
1268 allCompleteMatches cl tys = do
1269 let fam = case cl of
1270 RealDataCon dc ->
1271 [(FromBuiltin, map RealDataCon (tyConDataCons (dataConTyCon dc)))]
1272 PatSynCon _ -> []
1273
1274 pragmas <- case splitTyConApp_maybe (conLikeResTy cl tys) of
1275 Just (tc, _) -> dsGetCompleteMatches tc
1276 Nothing -> return []
1277 let fams cm = fmap (FromComplete,) $
1278 mapM dsLookupConLike (completeMatchConLikes cm)
1279 from_pragma <- mapM fams pragmas
1280
1281 let final_groups = fam ++ from_pragma
1282 tracePmD "allCompleteMatches" (ppr final_groups)
1283 return final_groups
1284
1285 -- -----------------------------------------------------------------------
1286 -- * Types and constraints
1287
1288 newEvVar :: Name -> Type -> EvVar
1289 newEvVar name ty = mkLocalId name (toTcType ty)
1290
1291 nameType :: String -> Type -> DsM EvVar
1292 nameType name ty = do
1293 unique <- getUniqueM
1294 let occname = mkVarOccFS (fsLit (name++"_"++show unique))
1295 idname = mkInternalName unique occname noSrcSpan
1296 return (newEvVar idname ty)
1297
1298 {-
1299 %************************************************************************
1300 %* *
1301 The type oracle
1302 %* *
1303 %************************************************************************
1304 -}
1305
1306 -- | Check whether a set of type constraints is satisfiable.
1307 tyOracle :: Bag EvVar -> PmM Bool
1308 tyOracle evs
1309 = liftD $
1310 do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
1311 ; case res of
1312 Just sat -> return sat
1313 Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
1314
1315 {-
1316 %************************************************************************
1317 %* *
1318 Sanity Checks
1319 %* *
1320 %************************************************************************
1321 -}
1322
1323 -- | The arity of a pattern/pattern vector is the
1324 -- number of top-level patterns that are not guards
1325 type PmArity = Int
1326
1327 -- | Compute the arity of a pattern vector
1328 patVecArity :: PatVec -> PmArity
1329 patVecArity = sum . map patternArity
1330
1331 -- | Compute the arity of a pattern
1332 patternArity :: Pattern -> PmArity
1333 patternArity (PmGrd {}) = 0
1334 patternArity _other_pat = 1
1335
1336 {-
1337 %************************************************************************
1338 %* *
1339 Heart of the algorithm: Function pmcheck
1340 %* *
1341 %************************************************************************
1342
1343 Main functions are:
1344
1345 * mkInitialUncovered :: [Id] -> PmM Uncovered
1346
1347 Generates the initial uncovered set. Term and type constraints in scope
1348 are checked, if they are inconsistent, the set is empty, otherwise, the
1349 set contains only a vector of variables with the constraints in scope.
1350
1351 * pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1352
1353 Checks redundancy, coverage and inaccessibility, using auxilary functions
1354 `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
1355 common in all three checks (see paper) and calls `pmcheckGuards` when the
1356 whole clause is checked, or `pmcheckHd` when the pattern vector does not
1357 start with a guard.
1358
1359 * pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1360
1361 Processes the guards.
1362
1363 * pmcheckHd :: Pattern -> PatVec -> [PatVec]
1364 -> ValAbs -> ValVec -> PmM PartialResult
1365
1366 Worker: This function implements functions `covered`, `uncovered` and
1367 `divergent` from the paper at once. Slightly different from the paper because
1368 it does not even produce the covered and uncovered sets. Since we only care
1369 about whether a clause covers SOMETHING or if it may forces ANY argument, we
1370 only store a boolean in both cases, for efficiency.
1371 -}
1372
1373 -- | Lift a pattern matching action from a single value vector abstration to a
1374 -- value set abstraction, but calling it on every vector and the combining the
1375 -- results.
1376 runMany :: (ValVec -> PmM PartialResult) -> (Uncovered -> PmM PartialResult)
1377 runMany _ [] = return mempty
1378 runMany pm (m:ms) = mappend <$> pm m <*> runMany pm ms
1379
1380 -- | Generate the initial uncovered set. It initializes the
1381 -- delta with all term and type constraints in scope.
1382 mkInitialUncovered :: [Id] -> PmM Uncovered
1383 mkInitialUncovered vars = do
1384 ty_cs <- liftD getDictsDs
1385 tm_cs <- map toComplex . bagToList <$> liftD getTmCsDs
1386 sat_ty <- tyOracle ty_cs
1387 let initTyCs = if sat_ty then ty_cs else emptyBag
1388 initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
1389 patterns = map PmVar vars
1390 -- If any of the term/type constraints are non
1391 -- satisfiable then return with the initialTmState. See #12957
1392 return [ValVec patterns (MkDelta initTyCs initTmState)]
1393
1394 -- | Increase the counter for elapsed algorithm iterations, check that the
1395 -- limit is not exceeded and call `pmcheck`
1396 pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1397 pmcheckI ps guards vva = do
1398 n <- liftD incrCheckPmIterDs
1399 tracePm "pmCheck" (ppr n <> colon <+> pprPatVec ps
1400 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1401 $$ pprValVecDebug vva)
1402 res <- pmcheck ps guards vva
1403 tracePm "pmCheckResult:" (ppr res)
1404 return res
1405 {-# INLINE pmcheckI #-}
1406
1407 -- | Increase the counter for elapsed algorithm iterations, check that the
1408 -- limit is not exceeded and call `pmcheckGuards`
1409 pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
1410 pmcheckGuardsI gvs vva = liftD incrCheckPmIterDs >> pmcheckGuards gvs vva
1411 {-# INLINE pmcheckGuardsI #-}
1412
1413 -- | Increase the counter for elapsed algorithm iterations, check that the
1414 -- limit is not exceeded and call `pmcheckHd`
1415 pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1416 -> PmM PartialResult
1417 pmcheckHdI p ps guards va vva = do
1418 n <- liftD incrCheckPmIterDs
1419 tracePm "pmCheckHdI" (ppr n <> colon <+> pprPmPatDebug p
1420 $$ pprPatVec ps
1421 $$ hang (text "guards:") 2 (vcat (map pprPatVec guards))
1422 $$ pprPmPatDebug va
1423 $$ pprValVecDebug vva)
1424
1425 res <- pmcheckHd p ps guards va vva
1426 tracePm "pmCheckHdI: res" (ppr res)
1427 return res
1428 {-# INLINE pmcheckHdI #-}
1429
1430 -- | Matching function: Check simultaneously a clause (takes separately the
1431 -- patterns and the list of guards) for exhaustiveness, redundancy and
1432 -- inaccessibility.
1433 pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
1434 pmcheck [] guards vva@(ValVec [] _)
1435 | null guards = return $ mempty { presultCovered = Covered }
1436 | otherwise = pmcheckGuardsI guards vva
1437
1438 -- Guard
1439 pmcheck (p@(PmGrd pv e) : ps) guards vva@(ValVec vas delta)
1440 -- short-circuit if the guard pattern is useless.
1441 -- we just have two possible outcomes: fail here or match and recurse
1442 -- none of the two contains any useful information about the failure
1443 -- though. So just have these two cases but do not do all the boilerplate
1444 | isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
1445 | otherwise = do
1446 y <- liftD $ mkPmId (pmPatType p)
1447 let tm_state = extendSubst y e (delta_tm_cs delta)
1448 delta' = delta { delta_tm_cs = tm_state }
1449 utail <$> pmcheckI (pv ++ ps) guards (ValVec (PmVar y : vas) delta')
1450
1451 pmcheck [] _ (ValVec (_:_) _) = panic "pmcheck: nil-cons"
1452 pmcheck (_:_) _ (ValVec [] _) = panic "pmcheck: cons-nil"
1453
1454 pmcheck (p:ps) guards (ValVec (va:vva) delta)
1455 = pmcheckHdI p ps guards va (ValVec vva delta)
1456
1457 -- | Check the list of guards
1458 pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
1459 pmcheckGuards [] vva = return (usimple [vva])
1460 pmcheckGuards (gv:gvs) vva = do
1461 (PartialResult prov1 cs vsa ds) <- pmcheckI gv [] vva
1462 (PartialResult prov2 css vsas dss) <- runMany (pmcheckGuardsI gvs) vsa
1463 return $ PartialResult (prov1 `mappend` prov2)
1464 (cs `mappend` css)
1465 vsas
1466 (ds `mappend` dss)
1467
1468 -- | Worker function: Implements all cases described in the paper for all three
1469 -- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
1470 -- cases which are handled by `pmcheck`
1471 pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
1472 -> PmM PartialResult
1473
1474 -- Var
1475 pmcheckHd (PmVar x) ps guards va (ValVec vva delta)
1476 | Just tm_state <- solveOneEq (delta_tm_cs delta)
1477 (PmExprVar (idName x), vaToPmExpr va)
1478 = ucon va <$> pmcheckI ps guards (ValVec vva (delta {delta_tm_cs = tm_state}))
1479 | otherwise = return mempty
1480
1481 -- ConCon
1482 pmcheckHd ( p@(PmCon {pm_con_con = c1, pm_con_args = args1})) ps guards
1483 (va@(PmCon {pm_con_con = c2, pm_con_args = args2})) (ValVec vva delta)
1484 | c1 /= c2 =
1485 return (usimple [ValVec (va:vva) delta])
1486 | otherwise = kcon c1 (pm_con_arg_tys p) (pm_con_tvs p) (pm_con_dicts p)
1487 <$> pmcheckI (args1 ++ ps) guards (ValVec (args2 ++ vva) delta)
1488
1489 -- LitLit
1490 pmcheckHd (PmLit l1) ps guards (va@(PmLit l2)) vva =
1491 case eqPmLit l1 l2 of
1492 True -> ucon va <$> pmcheckI ps guards vva
1493 False -> return $ ucon va (usimple [vva])
1494
1495 -- ConVar
1496 pmcheckHd (p@(PmCon { pm_con_con = con, pm_con_arg_tys = tys }))
1497 ps guards
1498 (PmVar x) (ValVec vva delta) = do
1499 (prov, complete_match) <- select =<< liftD (allCompleteMatches con tys)
1500
1501 cons_cs <- mapM (liftD . mkOneConFull x) complete_match
1502
1503 inst_vsa <- flip concatMapM cons_cs $ \(va, tm_ct, ty_cs) -> do
1504 let ty_state = ty_cs `unionBags` delta_ty_cs delta -- not actually a state
1505 sat_ty <- if isEmptyBag ty_cs then return True
1506 else tyOracle ty_state
1507 return $ case (sat_ty, solveOneEq (delta_tm_cs delta) tm_ct) of
1508 (True, Just tm_state) -> [ValVec (va:vva) (MkDelta ty_state tm_state)]
1509 _ty_or_tm_failed -> []
1510
1511 set_provenance prov .
1512 force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1513 runMany (pmcheckI (p:ps) guards) inst_vsa
1514
1515 -- LitVar
1516 pmcheckHd (p@(PmLit l)) ps guards (PmVar x) (ValVec vva delta)
1517 = force_if (canDiverge (idName x) (delta_tm_cs delta)) <$>
1518 mkUnion non_matched <$>
1519 case solveOneEq (delta_tm_cs delta) (mkPosEq x l) of
1520 Just tm_state -> pmcheckHdI p ps guards (PmLit l) $
1521 ValVec vva (delta {delta_tm_cs = tm_state})
1522 Nothing -> return mempty
1523 where
1524 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1525 = [ValVec (PmNLit x [l] : vva) (delta { delta_tm_cs = tm_state })]
1526 | otherwise = []
1527
1528 non_matched = usimple us
1529
1530 -- LitNLit
1531 pmcheckHd (p@(PmLit l)) ps guards
1532 (PmNLit { pm_lit_id = x, pm_lit_not = lits }) (ValVec vva delta)
1533 | all (not . eqPmLit l) lits
1534 , Just tm_state <- solveOneEq (delta_tm_cs delta) (mkPosEq x l)
1535 -- Both guards check the same so it would be sufficient to have only
1536 -- the second one. Nevertheless, it is much cheaper to check whether
1537 -- the literal is in the list so we check it first, to avoid calling
1538 -- the term oracle (`solveOneEq`) if possible
1539 = mkUnion non_matched <$>
1540 pmcheckHdI p ps guards (PmLit l)
1541 (ValVec vva (delta { delta_tm_cs = tm_state }))
1542 | otherwise = return non_matched
1543 where
1544 us | Just tm_state <- solveOneEq (delta_tm_cs delta) (mkNegEq x l)
1545 = [ValVec (PmNLit x (l:lits) : vva) (delta { delta_tm_cs = tm_state })]
1546 | otherwise = []
1547
1548 non_matched = usimple us
1549
1550 -- ----------------------------------------------------------------------------
1551 -- The following three can happen only in cases like #322 where constructors
1552 -- and overloaded literals appear in the same match. The general strategy is
1553 -- to replace the literal (positive/negative) by a variable and recurse. The
1554 -- fact that the variable is equal to the literal is recorded in `delta` so
1555 -- no information is lost
1556
1557 -- LitCon
1558 pmcheckHd (PmLit l) ps guards (va@(PmCon {})) (ValVec vva delta)
1559 = do y <- liftD $ mkPmId (pmPatType va)
1560 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1561 delta' = delta { delta_tm_cs = tm_state }
1562 pmcheckHdI (PmVar y) ps guards va (ValVec vva delta')
1563
1564 -- ConLit
1565 pmcheckHd (p@(PmCon {})) ps guards (PmLit l) (ValVec vva delta)
1566 = do y <- liftD $ mkPmId (pmPatType p)
1567 let tm_state = extendSubst y (PmExprLit l) (delta_tm_cs delta)
1568 delta' = delta { delta_tm_cs = tm_state }
1569 pmcheckHdI p ps guards (PmVar y) (ValVec vva delta')
1570
1571 -- ConNLit
1572 pmcheckHd (p@(PmCon {})) ps guards (PmNLit { pm_lit_id = x }) vva
1573 = pmcheckHdI p ps guards (PmVar x) vva
1574
1575 -- Impossible: handled by pmcheck
1576 pmcheckHd (PmGrd {}) _ _ _ _ = panic "pmcheckHd: Guard"
1577
1578 -- ----------------------------------------------------------------------------
1579 -- * Utilities for main checking
1580
1581 updateVsa :: (ValSetAbs -> ValSetAbs) -> (PartialResult -> PartialResult)
1582 updateVsa f p@(PartialResult { presultUncovered = old })
1583 = p { presultUncovered = f old }
1584
1585
1586 -- | Initialise with default values for covering and divergent information.
1587 usimple :: ValSetAbs -> PartialResult
1588 usimple vsa = mempty { presultUncovered = vsa }
1589
1590 -- | Take the tail of all value vector abstractions in the uncovered set
1591 utail :: PartialResult -> PartialResult
1592 utail = updateVsa upd
1593 where upd vsa = [ ValVec vva delta | ValVec (_:vva) delta <- vsa ]
1594
1595 -- | Prepend a value abstraction to all value vector abstractions in the
1596 -- uncovered set
1597 ucon :: ValAbs -> PartialResult -> PartialResult
1598 ucon va = updateVsa upd
1599 where
1600 upd vsa = [ ValVec (va:vva) delta | ValVec vva delta <- vsa ]
1601
1602 -- | Given a data constructor of arity `a` and an uncovered set containing
1603 -- value vector abstractions of length `(a+n)`, pass the first `n` value
1604 -- abstractions to the constructor (Hence, the resulting value vector
1605 -- abstractions will have length `n+1`)
1606 kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
1607 -> PartialResult -> PartialResult
1608 kcon con arg_tys ex_tvs dicts
1609 = let n = conLikeArity con
1610 upd vsa =
1611 [ ValVec (va:vva) delta
1612 | ValVec vva' delta <- vsa
1613 , let (args, vva) = splitAt n vva'
1614 , let va = PmCon { pm_con_con = con
1615 , pm_con_arg_tys = arg_tys
1616 , pm_con_tvs = ex_tvs
1617 , pm_con_dicts = dicts
1618 , pm_con_args = args } ]
1619 in updateVsa upd
1620
1621 -- | Get the union of two covered, uncovered and divergent value set
1622 -- abstractions. Since the covered and divergent sets are represented by a
1623 -- boolean, union means computing the logical or (at least one of the two is
1624 -- non-empty).
1625
1626 mkUnion :: PartialResult -> PartialResult -> PartialResult
1627 mkUnion = mappend
1628
1629 -- | Add a value vector abstraction to a value set abstraction (uncovered).
1630 mkCons :: ValVec -> PartialResult -> PartialResult
1631 mkCons vva = updateVsa (vva:)
1632
1633 -- | Set the divergent set to not empty
1634 forces :: PartialResult -> PartialResult
1635 forces pres = pres { presultDivergent = Diverged }
1636
1637 -- | Set the divergent set to non-empty if the flag is `True`
1638 force_if :: Bool -> PartialResult -> PartialResult
1639 force_if True pres = forces pres
1640 force_if False pres = pres
1641
1642 set_provenance :: Provenance -> PartialResult -> PartialResult
1643 set_provenance prov pr = pr { presultProvenance = prov }
1644
1645 -- ----------------------------------------------------------------------------
1646 -- * Propagation of term constraints inwards when checking nested matches
1647
1648 {- Note [Type and Term Equality Propagation]
1649 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1650 When checking a match it would be great to have all type and term information
1651 available so we can get more precise results. For this reason we have functions
1652 `addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
1653 term constraints (respectively) as we go deeper.
1654
1655 The type constraints we propagate inwards are collected by `collectEvVarsPats'
1656 in HsPat.hs. This handles bug #4139 ( see example
1657 https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
1658 where this is needed.
1659
1660 For term equalities we do less, we just generate equalities for HsCase. For
1661 example we accurately give 2 redundancy warnings for the marked cases:
1662
1663 f :: [a] -> Bool
1664 f x = case x of
1665
1666 [] -> case x of -- brings (x ~ []) in scope
1667 [] -> True
1668 (_:_) -> False -- can't happen
1669
1670 (_:_) -> case x of -- brings (x ~ (_:_)) in scope
1671 (_:_) -> True
1672 [] -> False -- can't happen
1673
1674 Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
1675 these constraints.
1676 -}
1677
1678 -- | Generate equalities when checking a case expression:
1679 -- case x of { p1 -> e1; ... pn -> en }
1680 -- When we go deeper to check e.g. e1 we record two equalities:
1681 -- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
1682 -- and (x ~ p1).
1683 genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
1684 -> [Pat GhcTc] -- LHS (should have length 1)
1685 -> [Id] -- MatchVars (should have length 1)
1686 -> DsM (Bag SimpleEq)
1687 genCaseTmCs2 Nothing _ _ = return emptyBag
1688 genCaseTmCs2 (Just scr) [p] [var] = do
1689 fam_insts <- dsGetFamInstEnvs
1690 [e] <- map vaToPmExpr . coercePatVec <$> translatePat fam_insts p
1691 let scr_e = lhsExprToPmExpr scr
1692 return $ listToBag [(var, e), (var, scr_e)]
1693 genCaseTmCs2 _ _ _ = panic "genCaseTmCs2: HsCase"
1694
1695 -- | Generate a simple equality when checking a case expression:
1696 -- case x of { matches }
1697 -- When checking matches we record that (x ~ y) where y is the initial
1698 -- uncovered. All matches will have to satisfy this equality.
1699 genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag SimpleEq
1700 genCaseTmCs1 Nothing _ = emptyBag
1701 genCaseTmCs1 (Just scr) [var] = unitBag (var, lhsExprToPmExpr scr)
1702 genCaseTmCs1 _ _ = panic "genCaseTmCs1: HsCase"
1703
1704 {- Note [Literals in PmPat]
1705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1706 Instead of translating a literal to a variable accompanied with a guard, we
1707 treat them like constructor patterns. The following example from
1708 "./libraries/base/GHC/IO/Encoding.hs" shows why:
1709
1710 mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
1711 mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
1712 "UTF8" -> return $ UTF8.mkUTF8 cfm
1713 "UTF16" -> return $ UTF16.mkUTF16 cfm
1714 "UTF16LE" -> return $ UTF16.mkUTF16le cfm
1715 ...
1716
1717 Each clause gets translated to a list of variables with an equal number of
1718 guards. For every guard we generate two cases (equals True/equals False) which
1719 means that we generate 2^n cases to feed the oracle with, where n is the sum of
1720 the length of all strings that appear in the patterns. For this particular
1721 example this means over 2^40 cases. Instead, by representing them like with
1722 constructor we get the following:
1723 1. We exploit the common prefix with our representation of VSAs
1724 2. We prune immediately non-reachable cases
1725 (e.g. False == (x == "U"), True == (x == "U"))
1726
1727 Note [Translating As Patterns]
1728 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1729 Instead of translating x@p as: x (p <- x)
1730 we instead translate it as: p (x <- coercePattern p)
1731 for performance reasons. For example:
1732
1733 f x@True = 1
1734 f y@False = 2
1735
1736 Gives the following with the first translation:
1737
1738 x |> {x == False, x == y, y == True}
1739
1740 If we use the second translation we get an empty set, independently of the
1741 oracle. Since the pattern `p' may contain guard patterns though, it cannot be
1742 used as an expression. That's why we call `coercePatVec' to drop the guard and
1743 `vaToPmExpr' to transform the value abstraction to an expression in the
1744 guard pattern (value abstractions are a subset of expressions). We keep the
1745 guards in the first pattern `p' though.
1746
1747
1748 %************************************************************************
1749 %* *
1750 Pretty printing of exhaustiveness/redundancy check warnings
1751 %* *
1752 %************************************************************************
1753 -}
1754
1755 -- | Check whether any part of pattern match checking is enabled (does not
1756 -- matter whether it is the redundancy check or the exhaustiveness check).
1757 isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
1758 isAnyPmCheckEnabled dflags (DsMatchContext kind _loc)
1759 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind
1760
1761 instance Outputable ValVec where
1762 ppr (ValVec vva delta)
1763 = let (residual_eqs, subst) = wrapUpTmState (delta_tm_cs delta)
1764 vector = substInValAbs subst vva
1765 in ppr_uncovered (vector, residual_eqs)
1766
1767 -- | Apply a term substitution to a value vector abstraction. All VAs are
1768 -- transformed to PmExpr (used only before pretty printing).
1769 substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
1770 substInValAbs subst = map (exprDeepLookup subst . vaToPmExpr)
1771
1772 -- | Wrap up the term oracle's state once solving is complete. Drop any
1773 -- information about unhandled constraints (involving HsExprs) and flatten
1774 -- (height 1) the substitution.
1775 wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
1776 wrapUpTmState (residual, (_, subst)) = (residual, flattenPmVarEnv subst)
1777
1778 -- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
1779 dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
1780 dsPmWarn dflags ctx@(DsMatchContext kind loc) pm_result
1781 = when (flag_i || flag_u) $ do
1782 let exists_r = flag_i && notNull redundant && onlyBuiltin
1783 exists_i = flag_i && notNull inaccessible && onlyBuiltin && not is_rec_upd
1784 exists_u = flag_u && (case uncovered of
1785 TypeOfUncovered _ -> True
1786 UncoveredPatterns u -> notNull u)
1787
1788 when exists_r $ forM_ redundant $ \(L l q) -> do
1789 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1790 (pprEqn q "is redundant"))
1791 when exists_i $ forM_ inaccessible $ \(L l q) -> do
1792 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns)
1793 (pprEqn q "has inaccessible right hand side"))
1794 when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $
1795 case uncovered of
1796 TypeOfUncovered ty -> warnEmptyCase ty
1797 UncoveredPatterns candidates -> pprEqns candidates
1798 where
1799 PmResult
1800 { pmresultProvenance = prov
1801 , pmresultRedundant = redundant
1802 , pmresultUncovered = uncovered
1803 , pmresultInaccessible = inaccessible } = pm_result
1804
1805 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1806 flag_u = exhaustive dflags kind
1807 flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind)
1808
1809 is_rec_upd = case kind of { RecUpd -> True; _ -> False }
1810 -- See Note [Inaccessible warnings for record updates]
1811
1812 onlyBuiltin = prov == FromBuiltin
1813
1814 maxPatterns = maxUncoveredPatterns dflags
1815
1816 -- Print a single clause (for redundant/with-inaccessible-rhs)
1817 pprEqn q txt = pp_context True ctx (text txt) $ \f -> ppr_eqn f kind q
1818
1819 -- Print several clauses (for uncovered clauses)
1820 pprEqns qs = pp_context False ctx (text "are non-exhaustive") $ \_ ->
1821 case qs of -- See #11245
1822 [ValVec [] _]
1823 -> text "Guards do not cover entire pattern space"
1824 _missing -> let us = map ppr qs
1825 in hang (text "Patterns not matched:") 4
1826 (vcat (take maxPatterns us)
1827 $$ dots maxPatterns us)
1828
1829 -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
1830 -- which we only know the type and have no inhabitants at hand)
1831 warnEmptyCase ty = pp_context False ctx (text "are non-exhaustive") $ \_ ->
1832 hang (text "Patterns not matched:") 4 (underscore <+> dcolon <+> ppr ty)
1833
1834 {- Note [Inaccessible warnings for record updates]
1835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1836 Consider (Trac #12957)
1837 data T a where
1838 T1 :: { x :: Int } -> T Bool
1839 T2 :: { x :: Int } -> T a
1840 T3 :: T a
1841
1842 f :: T Char -> T a
1843 f r = r { x = 3 }
1844
1845 The desugarer will (conservatively generate a case for T1 even though
1846 it's impossible:
1847 f r = case r of
1848 T1 x -> T1 3 -- Inaccessible branch
1849 T2 x -> T2 3
1850 _ -> error "Missing"
1851
1852 We don't want to warn about the inaccessible branch because the programmer
1853 didn't put it there! So we filter out the warning here.
1854 -}
1855
1856 -- | Issue a warning when the predefined number of iterations is exceeded
1857 -- for the pattern match checker
1858 warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
1859 warnPmIters dflags (DsMatchContext kind loc)
1860 = when (flag_i || flag_u) $ do
1861 iters <- maxPmCheckIterations <$> getDynFlags
1862 putSrcSpanDs loc (warnDs NoReason (msg iters))
1863 where
1864 ctxt = pprMatchContext kind
1865 msg is = fsep [ text "Pattern match checker exceeded"
1866 , parens (ppr is), text "iterations in", ctxt <> dot
1867 , text "(Use -fmax-pmcheck-iterations=n"
1868 , text "to set the maximun number of iterations to n)" ]
1869
1870 flag_i = wopt Opt_WarnOverlappingPatterns dflags
1871 flag_u = exhaustive dflags kind
1872
1873 dots :: Int -> [a] -> SDoc
1874 dots maxPatterns qs
1875 | qs `lengthExceeds` maxPatterns = text "..."
1876 | otherwise = empty
1877
1878 -- | Check whether the exhaustiveness checker should run (exhaustiveness only)
1879 exhaustive :: DynFlags -> HsMatchContext id -> Bool
1880 exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag
1881
1882 -- | Denotes whether an exhaustiveness check is supported, and if so,
1883 -- via which 'WarningFlag' it's controlled.
1884 -- Returns 'Nothing' if check is not supported.
1885 exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
1886 exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns
1887 exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns
1888 exhaustiveWarningFlag IfAlt = Nothing
1889 exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns
1890 exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns
1891 exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns
1892 exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd
1893 exhaustiveWarningFlag ThPatSplice = Nothing
1894 exhaustiveWarningFlag PatSyn = Nothing
1895 exhaustiveWarningFlag ThPatQuote = Nothing
1896 exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns
1897 -- in list comprehensions, pattern guards
1898 -- etc. They are often *supposed* to be
1899 -- incomplete
1900
1901 -- True <==> singular
1902 pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
1903 pp_context singular (DsMatchContext kind _loc) msg rest_of_msg_fun
1904 = vcat [text txt <+> msg,
1905 sep [ text "In" <+> ppr_match <> char ':'
1906 , nest 4 (rest_of_msg_fun pref)]]
1907 where
1908 txt | singular = "Pattern match"
1909 | otherwise = "Pattern match(es)"
1910
1911 (ppr_match, pref)
1912 = case kind of
1913 FunRhs { mc_fun = L _ fun }
1914 -> (pprMatchContext kind, \ pp -> ppr fun <+> pp)
1915 _ -> (pprMatchContext kind, \ pp -> pp)
1916
1917 ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
1918 ppr_pats kind pats
1919 = sep [sep (map ppr pats), matchSeparator kind, text "..."]
1920
1921 ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
1922 ppr_eqn prefixF kind eqn = prefixF (ppr_pats kind (map unLoc eqn))
1923
1924 ppr_constraint :: (SDoc,[PmLit]) -> SDoc
1925 ppr_constraint (var, lits) = var <+> text "is not one of"
1926 <+> braces (pprWithCommas ppr lits)
1927
1928 ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
1929 ppr_uncovered (expr_vec, complex)
1930 | null cs = fsep vec -- there are no literal constraints
1931 | otherwise = hang (fsep vec) 4 $
1932 text "where" <+> vcat (map ppr_constraint cs)
1933 where
1934 sdoc_vec = mapM pprPmExprWithParens expr_vec
1935 (vec,cs) = runPmPprM sdoc_vec (filterComplex complex)
1936
1937 {- Note [Representation of Term Equalities]
1938 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1939 In the paper, term constraints always take the form (x ~ e). Of course, a more
1940 general constraint of the form (e1 ~ e1) can always be transformed to an
1941 equivalent set of the former constraints, by introducing a fresh, intermediate
1942 variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
1943 to #11160 (incredibly bad performance for literal pattern matching). Two are
1944 the main sources of this problem (the actual problem is how these two interact
1945 with each other):
1946
1947 1. Pattern matching on literals generates twice as many constraints as needed.
1948 Consider the following (tests/ghci/should_run/ghcirun004):
1949
1950 foo :: Int -> Int
1951 foo 1 = 0
1952 ...
1953 foo 5000 = 4999
1954
1955 The covered and uncovered set *should* look like:
1956 U0 = { x |> {} }
1957
1958 C1 = { 1 |> { x ~ 1 } }
1959 U1 = { x |> { False ~ (x ~ 1) } }
1960 ...
1961 C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
1962 U10 = { x |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
1963 ...
1964
1965 If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
1966 we get twice as many constraints. Also note that half of them are just the
1967 substitution [x |-> False].
1968
1969 2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
1970 (x ~ e) as substitutions [x |-> e]. More specifically, function
1971 `extendSubstAndSolve` applies such substitutions in the residual constraints
1972 and partitions them in the affected and non-affected ones, which are the new
1973 worklist. Essentially, this gives quadradic behaviour on the number of the
1974 residual constraints. (This would not be the case if the term oracle used
1975 mutable variables but, since we use it to handle disjunctions on value set
1976 abstractions (`Union` case), we chose a pure, incremental interface).
1977
1978 Now the problem becomes apparent (e.g. for clause 300):
1979 * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
1980 constraints that we know that will not reduce (stay in the worklist).
1981 * To check for consistency, we apply the substituting constraints ONE BY ONE
1982 (since `tmOracle` is called incrementally, it does not have all of them
1983 available at once). Hence, we go through the (non-progressing) constraints
1984 over and over, achieving over-quadradic behaviour.
1985
1986 If instead we allow constraints of the form (e ~ e),
1987 * All uncovered sets Ui contain no substituting constraints and i
1988 non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
1989 behaves linearly.
1990 * All covered sets Ci contain exactly (i-1) non-progressing constraints and
1991 a single substituting constraint. So the term oracle goes through the
1992 constraints only once.
1993
1994 The performance improvement becomes even more important when more arguments are
1995 involved.
1996 -}
1997
1998 -- Debugging Infrastructre
1999
2000 tracePm :: String -> SDoc -> PmM ()
2001 tracePm herald doc = liftD $ tracePmD herald doc
2002
2003
2004 tracePmD :: String -> SDoc -> DsM ()
2005 tracePmD herald doc = do
2006 dflags <- getDynFlags
2007 printer <- mkPrintUnqualifiedDs
2008 liftIO $ dumpIfSet_dyn_printer printer dflags
2009 Opt_D_dump_ec_trace (text herald $$ (nest 2 doc))
2010
2011
2012 pprPmPatDebug :: PmPat a -> SDoc
2013 pprPmPatDebug (PmCon cc _arg_tys _con_tvs _con_dicts con_args)
2014 = hsep [text "PmCon", ppr cc, hsep (map pprPmPatDebug con_args)]
2015 pprPmPatDebug (PmVar vid) = text "PmVar" <+> ppr vid
2016 pprPmPatDebug (PmLit li) = text "PmLit" <+> ppr li
2017 pprPmPatDebug (PmNLit i nl) = text "PmNLit" <+> ppr i <+> ppr nl
2018 pprPmPatDebug (PmGrd pv ge) = text "PmGrd" <+> hsep (map pprPmPatDebug pv)
2019 <+> ppr ge
2020
2021 pprPatVec :: PatVec -> SDoc
2022 pprPatVec ps = hang (text "Pattern:") 2
2023 (brackets $ sep
2024 $ punctuate (comma <> char '\n') (map pprPmPatDebug ps))
2025
2026 pprValAbs :: [ValAbs] -> SDoc
2027 pprValAbs ps = hang (text "ValAbs:") 2
2028 (brackets $ sep
2029 $ punctuate (comma) (map pprPmPatDebug ps))
2030
2031 pprValVecDebug :: ValVec -> SDoc
2032 pprValVecDebug (ValVec vas _d) = text "ValVec" <+>
2033 parens (pprValAbs vas)