1{- 2Author: George Karachalias <george.karachalias@cs.kuleuven.be> 3 4Pattern Matching Coverage Checking. 5-} 6 7{-# LANGUAGE CPP #-} 8{-# LANGUAGE GADTs #-} 9{-# LANGUAGE TupleSections #-} 10{-# LANGUAGE ViewPatterns #-} 11{-# LANGUAGE MultiWayIf #-} 12{-# LANGUAGE LambdaCase #-} 13 14module GHC.HsToCore.PmCheck ( 15 -- Checking and printing 16 checkSingle, checkMatches, checkGuardMatches, 17 needToRunPmCheck, isMatchContextPmChecked, 18 19 -- See Note [Type and Term Equality Propagation] 20 addTyCsDs, addScrutTmCs, addPatTmCs 21 ) where 22 23#include "HsVersions.h" 24 25import GhcPrelude 26 27import GHC.HsToCore.PmCheck.Types 28import GHC.HsToCore.PmCheck.Oracle 29import GHC.HsToCore.PmCheck.Ppr 30import BasicTypes (Origin, isGenerated) 31import CoreSyn (CoreExpr, Expr(Var,App)) 32import FastString (unpackFS, lengthFS) 33import DynFlags 34import GHC.Hs 35import TcHsSyn 36import Id 37import ConLike 38import Name 39import FamInst 40import TysWiredIn 41import SrcLoc 42import Util 43import Outputable 44import DataCon 45import TyCon 46import Var (EvVar) 47import Coercion 48import TcEvidence 49import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr, dsSyntaxExpr) 50import {-# SOURCE #-} DsBinds (dsHsWrapper) 51import DsUtils (selectMatchVar) 52import MatchLit (dsLit, dsOverLit) 53import DsMonad 54import Bag 55import TyCoRep 56import Type 57import DsUtils (isTrueLHsExpr) 58import Maybes 59import qualified GHC.LanguageExtensions as LangExt 60 61import Control.Monad (when, forM_, zipWithM) 62import Data.List (elemIndex) 63import qualified Data.Semigroup as Semi 64 65{- 66This module checks pattern matches for: 67\begin{enumerate} 68 \item Equations that are redundant 69 \item Equations with inaccessible right-hand-side 70 \item Exhaustiveness 71\end{enumerate} 72 73The algorithm is based on the paper: 74 75 "GADTs Meet Their Match: 76 Pattern-matching Warnings That Account for GADTs, Guards, and Laziness" 77 78 http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf 79 80%************************************************************************ 81%* * 82 Pattern Match Check Types 83%* * 84%************************************************************************ 85-} 86 87-- | A very simple language for pattern guards. Let bindings, bang patterns, 88-- and matching variables against flat constructor patterns. 89data PmGrd 90 = -- | @PmCon x K tvs dicts args@ corresponds to a 91 -- @K tvs dicts args <- x@ guard. The @tvs@ and @args@ are bound in this 92 -- construct, the @x@ is just a use. 93 -- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'. 94 PmCon { 95 pm_id :: !Id, 96 pm_con_con :: !PmAltCon, 97 pm_con_tvs :: ![TyVar], 98 pm_con_dicts :: ![EvVar], 99 pm_con_args :: ![Id] 100 } 101 102 -- | @PmBang x@ corresponds to a @seq x True@ guard. 103 | PmBang { 104 pm_id :: !Id 105 } 106 107 -- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually 108 -- /binds/ @x@. 109 | PmLet { 110 pm_id :: !Id, 111 pm_let_expr :: !CoreExpr 112 } 113 114-- | Should not be user-facing. 115instance Outputable PmGrd where 116 ppr (PmCon x alt _con_tvs _con_dicts con_args) 117 = hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x] 118 ppr (PmBang x) = char '!' <> ppr x 119 ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr] 120 121type GrdVec = [PmGrd] 122 123-- | Each 'Delta' is proof (i.e., a model of the fact) that some values are not 124-- covered by a pattern match. E.g. @f Nothing = <rhs>@ might be given an 125-- uncovered set @[x :-> Just y]@ or @[x /= Nothing]@, where @x@ is the variable 126-- matching against @f@'s first argument. 127type Uncovered = [Delta] 128 129-- Instead of keeping the whole sets in memory, we keep a boolean for both the 130-- covered and the divergent set (we store the uncovered set though, since we 131-- want to print it). For both the covered and the divergent we have: 132-- 133-- True <=> The set is non-empty 134-- 135-- hence: 136-- C = True ==> Useful clause (no warning) 137-- C = False, D = True ==> Clause with inaccessible RHS 138-- C = False, D = False ==> Redundant clause 139 140data Covered = Covered | NotCovered 141 deriving Show 142 143instance Outputable Covered where 144 ppr = text . show 145 146-- Like the or monoid for booleans 147-- Covered = True, Uncovered = False 148instance Semi.Semigroup Covered where 149 Covered <> _ = Covered 150 _ <> Covered = Covered 151 NotCovered <> NotCovered = NotCovered 152 153instance Monoid Covered where 154 mempty = NotCovered 155 mappend = (Semi.<>) 156 157data Diverged = Diverged | NotDiverged 158 deriving Show 159 160instance Outputable Diverged where 161 ppr = text . show 162 163instance Semi.Semigroup Diverged where 164 Diverged <> _ = Diverged 165 _ <> Diverged = Diverged 166 NotDiverged <> NotDiverged = NotDiverged 167 168instance Monoid Diverged where 169 mempty = NotDiverged 170 mappend = (Semi.<>) 171 172data Precision = Approximate | Precise 173 deriving (Eq, Show) 174 175instance Outputable Precision where 176 ppr = text . show 177 178instance Semi.Semigroup Precision where 179 Approximate <> _ = Approximate 180 _ <> Approximate = Approximate 181 Precise <> Precise = Precise 182 183instance Monoid Precision where 184 mempty = Precise 185 mappend = (Semi.<>) 186 187-- | A triple <C,U,D> of covered, uncovered, and divergent sets. 188-- 189-- Also stores a flag 'presultApprox' denoting whether we ran into the 190-- 'maxPmCheckModels' limit for the purpose of hints in warning messages to 191-- maybe increase the limit. 192data PartialResult = PartialResult { 193 presultCovered :: Covered 194 , presultUncovered :: Uncovered 195 , presultDivergent :: Diverged 196 , presultApprox :: Precision } 197 198emptyPartialResult :: PartialResult 199emptyPartialResult = PartialResult { presultUncovered = mempty 200 , presultCovered = mempty 201 , presultDivergent = mempty 202 , presultApprox = mempty } 203 204combinePartialResults :: PartialResult -> PartialResult -> PartialResult 205combinePartialResults (PartialResult cs1 vsa1 ds1 ap1) (PartialResult cs2 vsa2 ds2 ap2) 206 = PartialResult (cs1 Semi.<> cs2) 207 (vsa1 Semi.<> vsa2) 208 (ds1 Semi.<> ds2) 209 (ap1 Semi.<> ap2) -- the result is approximate if either is 210 211instance Outputable PartialResult where 212 ppr (PartialResult c unc d pc) 213 = hang (text "PartialResult" <+> ppr c <+> ppr d <+> ppr pc) 2 (ppr_unc unc) 214 where 215 ppr_unc = braces . fsep . punctuate comma . map ppr 216 217instance Semi.Semigroup PartialResult where 218 (<>) = combinePartialResults 219 220instance Monoid PartialResult where 221 mempty = emptyPartialResult 222 mappend = (Semi.<>) 223 224-- | Pattern check result 225-- 226-- * Redundant clauses 227-- * Not-covered clauses (or their type, if no pattern is available) 228-- * Clauses with inaccessible RHS 229-- * A flag saying whether we ran into the 'maxPmCheckModels' limit for the 230-- purpose of suggesting to crank it up in the warning message 231-- 232-- More details about the classification of clauses into useful, redundant 233-- and with inaccessible right hand side can be found here: 234-- 235-- https://gitlab.haskell.org/ghc/ghc/wikis/pattern-match-check 236-- 237data PmResult = 238 PmResult { 239 pmresultRedundant :: [Located [LPat GhcTc]] 240 , pmresultUncovered :: [Delta] 241 , pmresultInaccessible :: [Located [LPat GhcTc]] 242 , pmresultApproximate :: Precision } 243 244instance Outputable PmResult where 245 ppr pmr = hang (text "PmResult") 2 $ vcat 246 [ text "pmresultRedundant" <+> ppr (pmresultRedundant pmr) 247 , text "pmresultUncovered" <+> ppr (pmresultUncovered pmr) 248 , text "pmresultInaccessible" <+> ppr (pmresultInaccessible pmr) 249 , text "pmresultApproximate" <+> ppr (pmresultApproximate pmr) 250 ] 251 252{- 253%************************************************************************ 254%* * 255 Entry points to the checker: checkSingle and checkMatches 256%* * 257%************************************************************************ 258-} 259 260-- | Check a single pattern binding (let) 261checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM () 262checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do 263 tracePm "checkSingle" (vcat [ppr ctxt, ppr var, ppr p]) 264 res <- checkSingle' locn var p 265 dsPmWarn dflags ctxt [var] res 266 267-- | Check a single pattern binding (let) 268checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> DsM PmResult 269checkSingle' locn var p = do 270 fam_insts <- dsGetFamInstEnvs 271 grds <- translatePat fam_insts var p 272 missing <- getPmDelta 273 tracePm "checkSingle': missing" (ppr missing) 274 PartialResult cs us ds pc <- pmCheck grds [] 1 missing 275 dflags <- getDynFlags 276 us' <- getNFirstUncovered [var] (maxUncoveredPatterns dflags + 1) us 277 let plain = PmResult { pmresultRedundant = [] 278 , pmresultUncovered = us' 279 , pmresultInaccessible = [] 280 , pmresultApproximate = pc } 281 return $ case (cs,ds) of 282 (Covered , _ ) -> plain -- useful 283 (NotCovered, NotDiverged) -> plain { pmresultRedundant = m } -- redundant 284 (NotCovered, Diverged ) -> plain { pmresultInaccessible = m } -- inaccessible rhs 285 where m = [cL locn [cL locn p]] 286 287-- | Exhaustive for guard matches, is used for guards in pattern bindings and 288-- in @MultiIf@ expressions. 289checkGuardMatches :: HsMatchContext Name -- Match context 290 -> GRHSs GhcTc (LHsExpr GhcTc) -- Guarded RHSs 291 -> DsM () 292checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do 293 dflags <- getDynFlags 294 let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss) 295 dsMatchContext = DsMatchContext hs_ctx combinedLoc 296 match = cL combinedLoc $ 297 Match { m_ext = noExtField 298 , m_ctxt = hs_ctx 299 , m_pats = [] 300 , m_grhss = guards } 301 checkMatches dflags dsMatchContext [] [match] 302checkGuardMatches _ (XGRHSs nec) = noExtCon nec 303 304-- | Check a matchgroup (case, functions, etc.) 305checkMatches :: DynFlags -> DsMatchContext 306 -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM () 307checkMatches dflags ctxt vars matches = do 308 tracePm "checkMatches" (hang (vcat [ppr ctxt 309 , ppr vars 310 , text "Matches:"]) 311 2 312 (vcat (map ppr matches))) 313 res <- checkMatches' vars matches 314 dsPmWarn dflags ctxt vars res 315 316-- | Check a matchgroup (case, functions, etc.). 317checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM PmResult 318checkMatches' vars matches = do 319 init_delta <- getPmDelta 320 missing <- case matches of 321 -- This must be an -XEmptyCase. See Note [Checking EmptyCase] 322 [] | [var] <- vars -> maybeToList <$> addTmCt init_delta (TmVarNonVoid var) 323 _ -> pure [init_delta] 324 tracePm "checkMatches': missing" (ppr missing) 325 (rs,us,ds,pc) <- go matches missing 326 dflags <- getDynFlags 327 us' <- getNFirstUncovered vars (maxUncoveredPatterns dflags + 1) us 328 return $ PmResult { 329 pmresultRedundant = map hsLMatchToLPats rs 330 , pmresultUncovered = us' 331 , pmresultInaccessible = map hsLMatchToLPats ds 332 , pmresultApproximate = pc } 333 where 334 go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered 335 -> DsM ( [LMatch GhcTc (LHsExpr GhcTc)] 336 , Uncovered 337 , [LMatch GhcTc (LHsExpr GhcTc)] 338 , Precision) 339 go [] missing = return ([], missing, [], Precise) 340 go (m:ms) missing = do 341 tracePm "checkMatches': go" (ppr m) 342 dflags <- getDynFlags 343 fam_insts <- dsGetFamInstEnvs 344 (clause, guards) <- translateMatch fam_insts vars m 345 let limit = maxPmCheckModels dflags 346 n_siblings = length missing 347 throttled_check delta = 348 snd <$> throttle limit (pmCheck clause guards) n_siblings delta 349 350 r@(PartialResult cs missing' ds pc1) <- runMany throttled_check missing 351 352 tracePm "checkMatches': go: res" (ppr r) 353 (rs, final_u, is, pc2) <- go ms missing' 354 return $ case (cs, ds) of 355 -- useful 356 (Covered, _ ) -> (rs, final_u, is, pc1 Semi.<> pc2) 357 -- redundant 358 (NotCovered, NotDiverged) -> (m:rs, final_u, is, pc1 Semi.<> pc2) 359 -- inaccessible 360 (NotCovered, Diverged ) -> (rs, final_u, m:is, pc1 Semi.<> pc2) 361 362 hsLMatchToLPats :: LMatch id body -> Located [LPat id] 363 hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats 364 hsLMatchToLPats _ = panic "checkMatches'" 365 366getNFirstUncovered :: [Id] -> Int -> [Delta] -> DsM [Delta] 367getNFirstUncovered _ 0 _ = pure [] 368getNFirstUncovered _ _ [] = pure [] 369getNFirstUncovered vars n (delta:deltas) = do 370 front <- provideEvidence vars n delta 371 back <- getNFirstUncovered vars (n - length front) deltas 372 pure (front ++ back) 373 374{- Note [Checking EmptyCase] 375~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 376-XEmptyCase is useful for matching on empty data types like 'Void'. For example, 377the following is a complete match: 378 379 f :: Void -> () 380 f x = case x of {} 381 382Really, -XEmptyCase is the only way to write a program that at the same time is 383safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning 384(@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an 385exception into divergence (@f x = f x@). 386 387Semantically, unlike every other case expression, -XEmptyCase is strict in its 388match var x, which rules out ⊥ as an inhabitant. So we add x /~ ⊥ to the 389initial Delta and check if there are any values left to match on. 390-} 391 392{- 393%************************************************************************ 394%* * 395 Transform source syntax to *our* syntax 396%* * 397%************************************************************************ 398-} 399 400-- ----------------------------------------------------------------------- 401-- * Utilities 402 403-- | Smart constructor that eliminates trivial lets 404mkPmLetVar :: Id -> Id -> GrdVec 405mkPmLetVar x y | x == y = [] 406mkPmLetVar x y = [PmLet x (Var y)] 407 408-- | ADT constructor pattern => no existentials, no local constraints 409vanillaConGrd :: Id -> DataCon -> [Id] -> PmGrd 410vanillaConGrd scrut con arg_ids = 411 PmCon { pm_id = scrut, pm_con_con = PmAltConLike (RealDataCon con) 412 , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = arg_ids } 413 414-- | Creates a 'GrdVec' refining a match var of list type to a list, 415-- where list fields are matched against the incoming tagged 'GrdVec's. 416-- For example: 417-- @mkListGrds "a" "[(x, True <- x),(y, !y)]"@ 418-- to 419-- @"[(x:b) <- a, True <- x, (y:c) <- b, seq y True, [] <- c]"@ 420-- where b,c are freshly allocated in @mkListGrds@ and a is the match variable. 421mkListGrds :: Id -> [(Id, GrdVec)] -> DsM GrdVec 422-- See Note [Order of guards matter] for why we need to intertwine guards 423-- on list elements. 424mkListGrds a [] = pure [vanillaConGrd a nilDataCon []] 425mkListGrds a ((x, head_grds):xs) = do 426 b <- mkPmId (idType a) 427 tail_grds <- mkListGrds b xs 428 pure $ vanillaConGrd a consDataCon [x, b] : head_grds ++ tail_grds 429 430-- | Create a 'GrdVec' refining a match variable to a 'PmLit'. 431mkPmLitGrds :: Id -> PmLit -> DsM GrdVec 432mkPmLitGrds x (PmLit _ (PmLitString s)) = do 433 -- We translate String literals to list literals for better overlap reasoning. 434 -- It's a little unfortunate we do this here rather than in 435 -- 'GHC.HsToCore.PmCheck.Oracle.trySolve' and 'GHC.HsToCore.PmCheck.Oracle.addRefutableAltCon', but it's so much 436 -- simpler here. 437 -- See Note [Representation of Strings in TmState] in GHC.HsToCore.PmCheck.Oracle 438 vars <- traverse mkPmId (take (lengthFS s) (repeat charTy)) 439 let mk_char_lit y c = mkPmLitGrds y (PmLit charTy (PmLitChar c)) 440 char_grdss <- zipWithM mk_char_lit vars (unpackFS s) 441 mkListGrds x (zip vars char_grdss) 442mkPmLitGrds x lit = do 443 let grd = PmCon { pm_id = x 444 , pm_con_con = PmAltLit lit 445 , pm_con_tvs = [] 446 , pm_con_dicts = [] 447 , pm_con_args = [] } 448 pure [grd] 449 450-- ----------------------------------------------------------------------- 451-- * Transform (Pat Id) into GrdVec 452 453-- | @translatePat _ x pat@ transforms @pat@ into a 'GrdVec', where 454-- the variable representing the match is @x@. 455translatePat :: FamInstEnvs -> Id -> Pat GhcTc -> DsM GrdVec 456translatePat fam_insts x pat = case pat of 457 WildPat _ty -> pure [] 458 VarPat _ y -> pure (mkPmLetVar (unLoc y) x) 459 ParPat _ p -> translateLPat fam_insts x p 460 LazyPat _ _ -> pure [] -- like a wildcard 461 BangPat _ p -> 462 -- Add the bang in front of the list, because it will happen before any 463 -- nested stuff. 464 (PmBang x :) <$> translateLPat fam_insts x p 465 466 -- (x@pat) ==> Translate pat with x as match var and handle impedance 467 -- mismatch with incoming match var 468 AsPat _ (dL->L _ y) p -> (mkPmLetVar y x ++) <$> translateLPat fam_insts y p 469 470 SigPat _ p _ty -> translateLPat fam_insts x p 471 472 -- See Note [Translate CoPats] 473 -- Generally the translation is 474 -- pat |> co ===> let y = x |> co, pat <- y where y is a match var of pat 475 CoPat _ wrapper p _ty 476 | isIdHsWrapper wrapper -> translatePat fam_insts x p 477 | WpCast co <- wrapper, isReflexiveCo co -> translatePat fam_insts x p 478 | otherwise -> do 479 (y, grds) <- translatePatV fam_insts p 480 wrap_rhs_y <- dsHsWrapper wrapper 481 pure (PmLet y (wrap_rhs_y (Var x)) : grds) 482 483 -- (n + k) ===> let b = x >= k, True <- b, let n = x-k 484 NPlusKPat _pat_ty (dL->L _ n) k1 k2 ge minus -> do 485 b <- mkPmId boolTy 486 let grd_b = vanillaConGrd b trueDataCon [] 487 [ke1, ke2] <- traverse dsOverLit [unLoc k1, k2] 488 rhs_b <- dsSyntaxExpr ge [Var x, ke1] 489 rhs_n <- dsSyntaxExpr minus [Var x, ke2] 490 pure [PmLet b rhs_b, grd_b, PmLet n rhs_n] 491 492 -- (fun -> pat) ===> let y = fun x, pat <- y where y is a match var of pat 493 ViewPat _arg_ty lexpr pat -> do 494 (y, grds) <- translateLPatV fam_insts pat 495 fun <- dsLExpr lexpr 496 pure $ PmLet y (App fun (Var x)) : grds 497 498 -- list 499 ListPat (ListPatTc _elem_ty Nothing) ps -> 500 translateListPat fam_insts x ps 501 502 -- overloaded list 503 ListPat (ListPatTc elem_ty (Just (pat_ty, to_list))) pats -> do 504 dflags <- getDynFlags 505 case splitListTyConApp_maybe pat_ty of 506 Just _e_ty 507 | not (xopt LangExt.RebindableSyntax dflags) 508 -- Just translate it as a regular ListPat 509 -> translateListPat fam_insts x pats 510 _ -> do 511 y <- mkPmId (mkListTy elem_ty) 512 grds <- translateListPat fam_insts y pats 513 rhs_y <- dsSyntaxExpr to_list [Var x] 514 pure $ PmLet y rhs_y : grds 515 516 -- (a) In the presence of RebindableSyntax, we don't know anything about 517 -- `toList`, we should treat `ListPat` as any other view pattern. 518 -- 519 -- (b) In the absence of RebindableSyntax, 520 -- - If the pat_ty is `[a]`, then we treat the overloaded list pattern 521 -- as ordinary list pattern. Although we can give an instance 522 -- `IsList [Int]` (more specific than the default `IsList [a]`), in 523 -- practice, we almost never do that. We assume the `to_list` is 524 -- the `toList` from `instance IsList [a]`. 525 -- 526 -- - Otherwise, we treat the `ListPat` as ordinary view pattern. 527 -- 528 -- See #14547, especially comment#9 and comment#10. 529 530 ConPatOut { pat_con = (dL->L _ con) 531 , pat_arg_tys = arg_tys 532 , pat_tvs = ex_tvs 533 , pat_dicts = dicts 534 , pat_args = ps } -> do 535 translateConPatOut fam_insts x con arg_tys ex_tvs dicts ps 536 537 NPat ty (dL->L _ olit) mb_neg _ -> do 538 -- See Note [Literal short cut] in MatchLit.hs 539 -- We inline the Literal short cut for @ty@ here, because @ty@ is more 540 -- precise than the field of OverLitTc, which is all that dsOverLit (which 541 -- normally does the literal short cut) can look at. Also @ty@ matches the 542 -- type of the scrutinee, so info on both pattern and scrutinee (for which 543 -- short cutting in dsOverLit works properly) is overloaded iff either is. 544 dflags <- getDynFlags 545 core_expr <- case olit of 546 OverLit{ ol_val = val, ol_ext = OverLitTc rebindable _ } 547 | not rebindable 548 , Just expr <- shortCutLit dflags val ty 549 -> dsExpr expr 550 _ -> dsOverLit olit 551 let lit = expectJust "failed to detect OverLit" (coreExprAsPmLit core_expr) 552 let lit' = case mb_neg of 553 Just _ -> expectJust "failed to negate lit" (negatePmLit lit) 554 Nothing -> lit 555 mkPmLitGrds x lit' 556 557 LitPat _ lit -> do 558 core_expr <- dsLit (convertLit lit) 559 let lit = expectJust "failed to detect Lit" (coreExprAsPmLit core_expr) 560 mkPmLitGrds x lit 561 562 TuplePat _tys pats boxity -> do 563 (vars, grdss) <- mapAndUnzipM (translateLPatV fam_insts) pats 564 let tuple_con = tupleDataCon boxity (length vars) 565 pure $ vanillaConGrd x tuple_con vars : concat grdss 566 567 SumPat _ty p alt arity -> do 568 (y, grds) <- translateLPatV fam_insts p 569 let sum_con = sumDataCon alt arity 570 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon 571 pure $ vanillaConGrd x sum_con [y] : grds 572 573 -- -------------------------------------------------------------------------- 574 -- Not supposed to happen 575 ConPatIn {} -> panic "Check.translatePat: ConPatIn" 576 SplicePat {} -> panic "Check.translatePat: SplicePat" 577 XPat n -> noExtCon n 578 579-- | 'translatePat', but also select and return a new match var. 580translatePatV :: FamInstEnvs -> Pat GhcTc -> DsM (Id, GrdVec) 581translatePatV fam_insts pat = do 582 x <- selectMatchVar pat 583 grds <- translatePat fam_insts x pat 584 pure (x, grds) 585 586translateLPat :: FamInstEnvs -> Id -> LPat GhcTc -> DsM GrdVec 587translateLPat fam_insts x = translatePat fam_insts x . unLoc 588 589-- | 'translateLPat', but also select and return a new match var. 590translateLPatV :: FamInstEnvs -> LPat GhcTc -> DsM (Id, GrdVec) 591translateLPatV fam_insts = translatePatV fam_insts . unLoc 592 593-- | @translateListPat _ x [p1, ..., pn]@ is basically 594-- @translateConPatOut _ x $(mkListConPatOuts [p1, ..., pn]>@ without ever 595-- constructing the 'ConPatOut's. 596translateListPat :: FamInstEnvs -> Id -> [LPat GhcTc] -> DsM GrdVec 597translateListPat fam_insts x pats = do 598 vars_and_grdss <- traverse (translateLPatV fam_insts) pats 599 mkListGrds x vars_and_grdss 600 601-- | Translate a constructor pattern 602translateConPatOut :: FamInstEnvs -> Id -> ConLike -> [Type] -> [TyVar] 603 -> [EvVar] -> HsConPatDetails GhcTc -> DsM GrdVec 604translateConPatOut fam_insts x con univ_tys ex_tvs dicts = \case 605 PrefixCon ps -> go_field_pats (zip [0..] ps) 606 InfixCon p1 p2 -> go_field_pats (zip [0..] [p1,p2]) 607 RecCon (HsRecFields fs _) -> go_field_pats (rec_field_ps fs) 608 where 609 -- The actual argument types (instantiated) 610 arg_tys = conLikeInstOrigArgTys con (univ_tys ++ mkTyVarTys ex_tvs) 611 612 -- Extract record field patterns tagged by field index from a list of 613 -- LHsRecField 614 rec_field_ps fs = map (tagged_pat . unLoc) fs 615 where 616 tagged_pat f = (lbl_to_index (getName (hsRecFieldId f)), hsRecFieldArg f) 617 -- Unfortunately the label info is empty when the DataCon wasn't defined 618 -- with record field labels, hence we translate to field index. 619 orig_lbls = map flSelector $ conLikeFieldLabels con 620 lbl_to_index lbl = expectJust "lbl_to_index" $ elemIndex lbl orig_lbls 621 622 go_field_pats tagged_pats = do 623 -- The fields that appear might not be in the correct order. So first 624 -- do a PmCon match, then force according to field strictness and then 625 -- force evaluation of the field patterns in the order given by 626 -- the first field of @tagged_pats@. 627 -- See Note [Field match order for RecCon] 628 629 -- Translate the mentioned field patterns. We're doing this first to get 630 -- the Ids for pm_con_args. 631 let trans_pat (n, pat) = do 632 (var, pvec) <- translateLPatV fam_insts pat 633 pure ((n, var), pvec) 634 (tagged_vars, arg_grdss) <- mapAndUnzipM trans_pat tagged_pats 635 636 let get_pat_id n ty = case lookup n tagged_vars of 637 Just var -> pure var 638 Nothing -> mkPmId ty 639 640 -- 1. the constructor pattern match itself 641 arg_ids <- zipWithM get_pat_id [0..] arg_tys 642 let con_grd = PmCon x (PmAltConLike con) ex_tvs dicts arg_ids 643 644 -- 2. bang strict fields 645 let arg_is_banged = map isBanged $ conLikeImplBangs con 646 bang_grds = map PmBang $ filterByList arg_is_banged arg_ids 647 648 -- 3. guards from field selector patterns 649 let arg_grds = concat arg_grdss 650 651 -- tracePm "ConPatOut" (ppr x $$ ppr con $$ ppr arg_ids) 652 -- 653 -- Store the guards in exactly that order 654 -- 1. 2. 3. 655 pure (con_grd : bang_grds ++ arg_grds) 656 657-- Translate a single match 658translateMatch :: FamInstEnvs -> [Id] -> LMatch GhcTc (LHsExpr GhcTc) 659 -> DsM (GrdVec, [GrdVec]) 660translateMatch fam_insts vars (dL->L _ (Match { m_pats = pats, m_grhss = grhss })) 661 = do 662 pats' <- concat <$> zipWithM (translateLPat fam_insts) vars pats 663 guards' <- mapM (translateGuards fam_insts) guards 664 -- tracePm "translateMatch" (vcat [ppr pats, ppr pats', ppr guards, ppr guards']) 665 return (pats', guards') 666 where 667 extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc] 668 extractGuards (dL->L _ (GRHS _ gs _)) = map unLoc gs 669 extractGuards _ = panic "translateMatch" 670 671 guards = map extractGuards (grhssGRHSs grhss) 672translateMatch _ _ _ = panic "translateMatch" 673 674-- ----------------------------------------------------------------------- 675-- * Transform source guards (GuardStmt Id) to simpler PmGrds 676 677-- | Translate a list of guard statements to a 'GrdVec' 678translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM GrdVec 679translateGuards fam_insts guards = 680 concat <$> mapM (translateGuard fam_insts) guards 681 682-- | Translate a guard statement to a 'GrdVec' 683translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM GrdVec 684translateGuard fam_insts guard = case guard of 685 BodyStmt _ e _ _ -> translateBoolGuard e 686 LetStmt _ binds -> translateLet (unLoc binds) 687 BindStmt _ p e _ _ -> translateBind fam_insts p e 688 LastStmt {} -> panic "translateGuard LastStmt" 689 ParStmt {} -> panic "translateGuard ParStmt" 690 TransStmt {} -> panic "translateGuard TransStmt" 691 RecStmt {} -> panic "translateGuard RecStmt" 692 ApplicativeStmt {} -> panic "translateGuard ApplicativeLastStmt" 693 XStmtLR nec -> noExtCon nec 694 695-- | Translate let-bindings 696translateLet :: HsLocalBinds GhcTc -> DsM GrdVec 697translateLet _binds = return [] 698 699-- | Translate a pattern guard 700-- @pat <- e ==> let x = e; <guards for pat <- x>@ 701translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM GrdVec 702translateBind fam_insts p e = dsLExpr e >>= \case 703 Var y 704 | Nothing <- isDataConId_maybe y 705 -- RHS is a variable, so that will allow us to omit the let 706 -> translateLPat fam_insts y p 707 rhs -> do 708 (x, grds) <- translateLPatV fam_insts p 709 pure (PmLet x rhs : grds) 710 711-- | Translate a boolean guard 712-- @e ==> let x = e; True <- x@ 713translateBoolGuard :: LHsExpr GhcTc -> DsM GrdVec 714translateBoolGuard e 715 | isJust (isTrueLHsExpr e) = return [] 716 -- The formal thing to do would be to generate (True <- True) 717 -- but it is trivial to solve so instead we give back an empty 718 -- GrdVec for efficiency 719 | otherwise = dsLExpr e >>= \case 720 Var y 721 | Nothing <- isDataConId_maybe y 722 -- Omit the let by matching on y 723 -> pure [vanillaConGrd y trueDataCon []] 724 rhs -> do 725 x <- mkPmId boolTy 726 pure $ [PmLet x rhs, vanillaConGrd x trueDataCon []] 727 728{- Note [Field match order for RecCon] 729~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 730The order for RecCon field patterns actually determines evaluation order of 731the pattern match. For example: 732 733 data T = T { a :: !Bool, b :: Char, c :: Int } 734 f :: T -> () 735 f T{ c = 42, b = 'b' } = () 736 737Then 738 * @f (T (error "a") (error "b") (error "c"))@ errors out with "a" because of 739 the strict field. 740 * @f (T True (error "b") (error "c"))@ errors out with "c" because it 741 is mentioned frist in the pattern match. 742 743This means we can't just desugar the pattern match to the PatVec 744@[T !_ 'b' 42]@. Instead we have to generate variable matches that have 745strictness according to the field declarations and afterwards force them in the 746right order. As a result, we get the PatVec @[T !_ b c, 42 <- c, 'b' <- b]@. 747 748Of course, when the labels occur in the order they are defined, we can just use 749the simpler desugaring. 750 751Note [Order of guards matters] 752~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 753Similar to Note [Field match order for RecCon], the order in which the guards 754for a pattern match appear matter. Consider a situation similar to T5117: 755 756 f (0:_) = () 757 f (0:[]) = () 758 759The latter clause is clearly redundant. Yet if we translate the second clause as 760 761 [x:xs' <- xs, [] <- xs', 0 <- x] 762 763We will say that the second clause only has an inaccessible RHS. That's because 764we force the tail of the list before comparing its head! So the correct 765translation would have been 766 767 [x:xs' <- xs, 0 <- x, [] <- xs'] 768 769And we have to take in the guards on list cells into @mkListGrds@. 770 771Note [Countering exponential blowup] 772~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 773Precise pattern match exhaustiveness checking is necessarily exponential in 774the size of some input programs. We implement a counter-measure in the form of 775the -fmax-pmcheck-models flag, limiting the number of Deltas we check against 776each pattern by a constant. 777 778How do we do that? Consider 779 780 f True True = () 781 f True True = () 782 783And imagine we set our limit to 1 for the sake of the example. The first clause 784will be checked against the initial Delta, {}. Doing so will produce an 785Uncovered set of size 2, containing the models {x/~True} and {x~True,y/~True}. 786Also we find the first clause to cover the model {x~True,y~True}. 787 788But the Uncovered set we get out of the match is too huge! We somehow have to 789ensure not to make things worse as they are already, so we continue checking 790with a singleton Uncovered set of the initial Delta {}. Why is this 791sound (wrt. notion of the GADTs Meet their Match paper)? Well, it basically 792amounts to forgetting that we matched against the first clause. The values 793represented by {} are a superset of those represented by its two refinements 794{x/~True} and {x~True,y/~True}. 795 796This forgetfulness becomes very apparent in the example above: By continuing 797with {} we don't detect the second clause as redundant, as it again covers the 798same non-empty subset of {}. So we don't flag everything as redundant anymore, 799but still will never flag something as redundant that isn't. 800 801For exhaustivity, the converse applies: We will report @f@ as non-exhaustive 802and report @f _ _@ as missing, which is a superset of the actual missing 803matches. But soundness means we will never fail to report a missing match. 804 805This mechanism is implemented in the higher-order function 'throttle'. 806 807Note [Combinatorial explosion in guards] 808~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 809Function with many clauses and deeply nested guards like in #11195 tend to 810overwhelm the checker because they lead to exponential splitting behavior. 811See the comments on #11195 on refinement trees. Every guard refines the 812disjunction of Deltas by another split. This no different than the ConVar case, 813but in stark contrast we mostly don't get any useful information out of that 814split! Hence splitting k-fold just means having k-fold more work. The problem 815exacerbates for larger k, because it gets even more unlikely that we can handle 816all of the arising Deltas better than just continue working on the original 817Delta. 818 819We simply apply the same mechanism as in Note [Countering exponential blowup]. 820But we don't want to forget about actually useful info from pattern match 821clauses just because we had one clause with many guards. So we set the limit for 822guards much lower. 823 824Note [Translate CoPats] 825~~~~~~~~~~~~~~~~~~~~~~~ 826The pattern match checker did not know how to handle coerced patterns `CoPat` 827efficiently, which gave rise to #11276. The original approach translated 828`CoPat`s: 829 830 pat |> co ===> x (pat <- (x |> co)) 831 832Why did we do this seemingly unnecessary expansion in the first place? 833The reason is that the type of @pat |> co@ (which is the type of the value 834abstraction we match against) might be different than that of @pat@. Data 835instances such as @Sing (a :: Bool)@ are a good example of this: If we would 836just drop the coercion, we'd get a type error when matching @pat@ against its 837value abstraction, with the result being that pmIsSatisfiable decides that every 838possible data constructor fitting @pat@ is rejected as uninhabitated, leading to 839a lot of false warnings. 840 841But we can check whether the coercion is a hole or if it is just refl, in 842which case we can drop it. 843 844%************************************************************************ 845%* * 846 Utilities for Pattern Match Checking 847%* * 848%************************************************************************ 849-} 850 851-- ---------------------------------------------------------------------------- 852-- * Basic utilities 853 854{- 855Note [Extensions to GADTs Meet Their Match] 856~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 857The GADTs Meet Their Match paper presents the formalism that GHC's coverage 858checker adheres to. Since the paper's publication, there have been some 859additional features added to the coverage checker which are not described in 860the paper. This Note serves as a reference for these new features. 861 862* Value abstractions are severely simplified to the point where they are just 863 variables. The information about the shape of a variable is encoded in 864 the oracle state 'Delta' instead. 865* Handling of uninhabited fields like `!Void`. 866 See Note [Strict argument type constraints] in GHC.HsToCore.PmCheck.Oracle. 867* Efficient handling of literal splitting, large enumerations and accurate 868 redundancy warnings for `COMPLETE` groups through the oracle. 869 870Note [Filtering out non-matching COMPLETE sets] 871~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 872Currently, conlikes in a COMPLETE set are simply grouped by the 873type constructor heading the return type. This is nice and simple, but it does 874mean that there are scenarios when a COMPLETE set might be incompatible with 875the type of a scrutinee. For instance, consider (from #14135): 876 877 data Foo a = Foo1 a | Foo2 a 878 879 pattern MyFoo2 :: Int -> Foo Int 880 pattern MyFoo2 i = Foo2 i 881 882 {-# COMPLETE Foo1, MyFoo2 #-} 883 884 f :: Foo a -> a 885 f (Foo1 x) = x 886 887`f` has an incomplete pattern-match, so when choosing which constructors to 888report as unmatched in a warning, GHC must choose between the original set of 889data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe 890that GHC shouldn't even consider the COMPLETE set as a possibility: the return 891type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since 892there's no substitution `s` such that s(Foo Int) = Foo a. 893 894To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern 895synonym constructor's return type matches the type of the scrutinee, and if one 896doesn't, then we remove the whole COMPLETE set from consideration. 897 898One might wonder why GHC only checks /pattern synonym/ constructors, and not 899/data/ constructors as well. The reason is because that the type of a 900GADT constructor very well may not match the type of a scrutinee, and that's 901OK. Consider this example (from #14059): 902 903 data SBool (z :: Bool) where 904 SFalse :: SBool False 905 STrue :: SBool True 906 907 pattern STooGoodToBeTrue :: forall (z :: Bool). () 908 => z ~ True 909 => SBool z 910 pattern STooGoodToBeTrue = STrue 911 {-# COMPLETE SFalse, STooGoodToBeTrue #-} 912 913 wobble :: SBool z -> Bool 914 wobble STooGoodToBeTrue = True 915 916In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse 917should be matched against, even though its type, SBool False, does not match 918the scrutinee type, SBool z. 919 920SG: Another angle at this is that the implied constraints when we instantiate 921universal type variables in the return type of a GADT will lead to *provided* 922thetas, whereas when we instantiate the return type of a pattern synonym that 923corresponds to a *required* theta. See Note [Pattern synonym result type] in 924PatSyn. Note how isValidCompleteMatches will successfully filter out 925 926 pattern Just42 :: Maybe Int 927 pattern Just42 = Just 42 928 929But fail to filter out the equivalent 930 931 pattern Just'42 :: (a ~ Int) => Maybe a 932 pattern Just'42 = Just 42 933 934Which seems fine as far as tcMatchTy is concerned, but it raises a few eye 935brows. 936-} 937 938{- 939%************************************************************************ 940%* * 941 Heart of the algorithm: Function pmCheck 942%* * 943%************************************************************************ 944 945Main functions are: 946 947* pmCheck :: PatVec -> [PatVec] -> ValVec -> Delta -> DsM PartialResult 948 949 This function implements functions `covered`, `uncovered` and 950 `divergent` from the paper at once. Calls out to the auxilary function 951 `pmCheckGuards` for handling (possibly multiple) guarded RHSs when the whole 952 clause is checked. Slightly different from the paper because it does not even 953 produce the covered and uncovered sets. Since we only care about whether a 954 clause covers SOMETHING or if it may forces ANY argument, we only store a 955 boolean in both cases, for efficiency. 956 957* pmCheckGuards :: [PatVec] -> ValVec -> Delta -> DsM PartialResult 958 959 Processes the guards. 960-} 961 962-- | @throttle limit f n delta@ executes the pattern match action @f@ but 963-- replaces the 'Uncovered' set by @[delta]@ if not doing so would lead to 964-- too many Deltas to check. 965-- 966-- See Note [Countering exponential blowup] and 967-- Note [Combinatorial explosion in guards] 968-- 969-- How many is "too many"? @throttle@ assumes that the pattern match action 970-- will be executed against @n@ similar other Deltas, its "siblings". Now, by 971-- observing the branching factor (i.e. the number of children) of executing 972-- the action, we can estimate how many Deltas there would be in the next 973-- generation. If we find that this number exceeds @limit@, we do 974-- "birth control": We simply don't allow a branching factor of more than 1. 975-- Otherwise we just return the singleton set of the original @delta@. 976-- This amounts to forgetting about the refined facts we got from running the 977-- action. 978throttle :: Int -> (Int -> Delta -> DsM PartialResult) -> Int -> Delta -> DsM (Int, PartialResult) 979throttle limit f n_siblings delta = do 980 res <- f n_siblings delta 981 let n_own_children = length (presultUncovered res) 982 let n_next_gen = n_siblings * n_own_children 983 -- Birth control! 984 if n_next_gen <= limit || n_own_children <= 1 985 then pure (n_next_gen, res) 986 else pure (n_siblings, res { presultUncovered = [delta], presultApprox = Approximate }) 987 988-- | Map a pattern matching action processing a single 'Delta' over a 989-- 'Uncovered' set and return the combined 'PartialResult's. 990runMany :: (Delta -> DsM PartialResult) -> Uncovered -> DsM PartialResult 991runMany f unc = mconcat <$> traverse f unc 992 993-- | Print diagnostic info and actually call 'pmCheck''. 994pmCheck :: GrdVec -> [GrdVec] -> Int -> Delta -> DsM PartialResult 995pmCheck ps guards n delta = do 996 tracePm "pmCheck {" $ vcat [ ppr n <> colon 997 , hang (text "patterns:") 2 (ppr ps) 998 , hang (text "guards:") 2 (ppr guards) 999 , ppr delta ] 1000 res <- pmCheck' ps guards n delta 1001 tracePm "}:" (ppr res) -- braces are easier to match by tooling 1002 return res 1003 1004-- | Lifts 'pmCheck' over a 'DsM (Maybe Delta)'. 1005pmCheckM :: GrdVec -> [GrdVec] -> Int -> DsM (Maybe Delta) -> DsM PartialResult 1006pmCheckM ps guards n m_mb_delta = m_mb_delta >>= \case 1007 Nothing -> pure mempty 1008 Just delta -> pmCheck ps guards n delta 1009 1010-- | Check the list of mutually exclusive guards 1011pmCheckGuards :: [GrdVec] -> Int -> Delta -> DsM PartialResult 1012pmCheckGuards [] _ delta = return (usimple delta) 1013pmCheckGuards (gv:gvs) n delta = do 1014 dflags <- getDynFlags 1015 let limit = maxPmCheckModels dflags `div` 5 1016 (n', PartialResult cs unc ds pc) <- throttle limit (pmCheck gv []) n delta 1017 (PartialResult css uncs dss pcs) <- runMany (pmCheckGuards gvs n') unc 1018 return $ PartialResult (cs `mappend` css) 1019 uncs 1020 (ds `mappend` dss) 1021 (pc `mappend` pcs) 1022 1023-- | Matching function: Check simultaneously a clause (takes separately the 1024-- patterns and the list of guards) for exhaustiveness, redundancy and 1025-- inaccessibility. 1026pmCheck' 1027 :: GrdVec -- ^ Patterns of the clause 1028 -> [GrdVec] -- ^ (Possibly multiple) guards of the clause 1029 -> Int -- ^ Estimate on the number of similar 'Delta's to handle. 1030 -- See 6. in Note [Countering exponential blowup] 1031 -> Delta -- ^ Oracle state giving meaning to the identifiers in the ValVec 1032 -> DsM PartialResult 1033pmCheck' [] guards n delta 1034 | null guards = return $ mempty { presultCovered = Covered } 1035 | otherwise = pmCheckGuards guards n delta 1036 1037-- let x = e: Add x ~ e to the oracle 1038pmCheck' (PmLet { pm_id = x, pm_let_expr = e } : ps) guards n delta = do 1039 tracePm "PmLet" (vcat [ppr x, ppr e]) 1040 -- x is fresh because it's bound by the let 1041 delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e 1042 pmCheck ps guards n delta' 1043 1044-- Bang x: Add x /~ _|_ to the oracle 1045pmCheck' (PmBang x : ps) guards n delta = do 1046 tracePm "PmBang" (ppr x) 1047 pr <- pmCheckM ps guards n (addTmCt delta (TmVarNonVoid x)) 1048 pure (forceIfCanDiverge delta x pr) 1049 1050-- Con: Add x ~ K ys to the Covered set and x /~ K to the Uncovered set 1051pmCheck' (p : ps) guards n delta 1052 | PmCon{ pm_id = x, pm_con_con = con, pm_con_args = args 1053 , pm_con_dicts = dicts } <- p = do 1054 -- E.g f (K p q) = <rhs> 1055 -- <next equation> 1056 -- Split delta into two refinements: 1057 -- * one for <rhs>, binding x to (K p q) 1058 -- * one for <next equation>, recording that x is /not/ (K _ _) 1059 1060 -- Stuff for <rhs> 1061 pr_pos <- pmCheckM ps guards n (addPmConCts delta x con dicts args) 1062 1063 -- The var is forced regardless of whether @con@ was satisfiable 1064 -- See Note [Divergence of Newtype matches] 1065 let pr_pos' = addConMatchStrictness delta x con pr_pos 1066 1067 -- Stuff for <next equation> 1068 pr_neg <- addRefutableAltCon delta x con >>= \case 1069 Nothing -> pure mempty 1070 Just delta' -> pure (usimple delta') 1071 1072 tracePm "PmCon" (vcat [ppr p, ppr x, ppr pr_pos', ppr pr_neg]) 1073 1074 -- Combine both into a single PartialResult 1075 let pr = mkUnion pr_pos' pr_neg 1076 pure pr 1077 1078addPmConCts :: Delta -> Id -> PmAltCon -> [EvVar] -> [Id] -> DsM (Maybe Delta) 1079addPmConCts delta x con dicts fields = runMaybeT $ do 1080 delta_ty <- MaybeT $ addTypeEvidence delta (listToBag dicts) 1081 delta_tm_ty <- MaybeT $ addTmCt delta_ty (TmVarCon x con fields) 1082 pure delta_tm_ty 1083 1084-- ---------------------------------------------------------------------------- 1085-- * Utilities for main checking 1086 1087-- | Initialise with default values for covering and divergent information and 1088-- a singleton uncovered set. 1089usimple :: Delta -> PartialResult 1090usimple delta = mempty { presultUncovered = [delta] } 1091 1092-- | Get the union of two covered, uncovered and divergent value set 1093-- abstractions. Since the covered and divergent sets are represented by a 1094-- boolean, union means computing the logical or (at least one of the two is 1095-- non-empty). 1096 1097mkUnion :: PartialResult -> PartialResult -> PartialResult 1098mkUnion = mappend 1099 1100-- | Set the divergent set to not empty 1101forces :: PartialResult -> PartialResult 1102forces pres = pres { presultDivergent = Diverged } 1103 1104-- | Set the divergent set to non-empty if the variable has not been forced yet 1105forceIfCanDiverge :: Delta -> Id -> PartialResult -> PartialResult 1106forceIfCanDiverge delta x 1107 | canDiverge delta x = forces 1108 | otherwise = id 1109 1110-- | 'forceIfCanDiverge' if the 'PmAltCon' was not a Newtype. 1111-- See Note [Divergence of Newtype matches]. 1112addConMatchStrictness :: Delta -> Id -> PmAltCon -> PartialResult -> PartialResult 1113addConMatchStrictness _ _ (PmAltConLike (RealDataCon dc)) res 1114 | isNewTyCon (dataConTyCon dc) = res 1115addConMatchStrictness delta x _ res = forceIfCanDiverge delta x res 1116 1117-- ---------------------------------------------------------------------------- 1118-- * Propagation of term constraints inwards when checking nested matches 1119 1120{- Note [Type and Term Equality Propagation] 1121~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1122When checking a match it would be great to have all type and term information 1123available so we can get more precise results. For this reason we have functions 1124`addDictsDs' and `addTmVarCsDs' in DsMonad that store in the environment type and 1125term constraints (respectively) as we go deeper. 1126 1127The type constraints we propagate inwards are collected by `collectEvVarsPats' 1128in GHC.Hs.Pat. This handles bug #4139 ( see example 1129 https://gitlab.haskell.org/ghc/ghc/snippets/672 ) 1130where this is needed. 1131 1132For term equalities we do less, we just generate equalities for HsCase. For 1133example we accurately give 2 redundancy warnings for the marked cases: 1134 1135f :: [a] -> Bool 1136f x = case x of 1137 1138 [] -> case x of -- brings (x ~ []) in scope 1139 [] -> True 1140 (_:_) -> False -- can't happen 1141 1142 (_:_) -> case x of -- brings (x ~ (_:_)) in scope 1143 (_:_) -> True 1144 [] -> False -- can't happen 1145 1146Functions `addScrutTmCs' and `addPatTmCs' are responsible for generating 1147these constraints. 1148-} 1149 1150locallyExtendPmDelta :: (Delta -> DsM (Maybe Delta)) -> DsM a -> DsM a 1151locallyExtendPmDelta ext k = getPmDelta >>= ext >>= \case 1152 -- If adding a constraint would lead to a contradiction, don't add it. 1153 -- See @Note [Recovering from unsatisfiable pattern-matching constraints]@ 1154 -- for why this is done. 1155 Nothing -> k 1156 Just delta' -> updPmDelta delta' k 1157 1158-- | Add in-scope type constraints 1159addTyCsDs :: Bag EvVar -> DsM a -> DsM a 1160addTyCsDs ev_vars = 1161 locallyExtendPmDelta (\delta -> addTypeEvidence delta ev_vars) 1162 1163-- | Add equalities for the scrutinee to the local 'DsM' environment when 1164-- checking a case expression: 1165-- case e of x { matches } 1166-- When checking matches we record that (x ~ e) where x is the initial 1167-- uncovered. All matches will have to satisfy this equality. 1168addScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a 1169addScrutTmCs Nothing _ k = k 1170addScrutTmCs (Just scr) [x] k = do 1171 scr_e <- dsLExpr scr 1172 locallyExtendPmDelta (\delta -> addVarCoreCt delta x scr_e) k 1173addScrutTmCs _ _ _ = panic "addScrutTmCs: HsCase with more than one case binder" 1174 1175-- | Add equalities to the local 'DsM' environment when checking the RHS of a 1176-- case expression: 1177-- case e of x { p1 -> e1; ... pn -> en } 1178-- When we go deeper to check e.g. e1 we record (x ~ p1). 1179addPatTmCs :: [Pat GhcTc] -- LHS (should have length 1) 1180 -> [Id] -- MatchVars (should have length 1) 1181 -> DsM a 1182 -> DsM a 1183-- Computes an approximation of the Covered set for p1 (which pmCheck currently 1184-- discards). 1185addPatTmCs ps xs k = do 1186 fam_insts <- dsGetFamInstEnvs 1187 grds <- concat <$> zipWithM (translatePat fam_insts) xs ps 1188 locallyExtendPmDelta (\delta -> computeCovered grds delta) k 1189 1190-- | A dead simple version of 'pmCheck' that only computes the Covered set. 1191-- So it only cares about collecting positive info. 1192-- We use it to collect info from a pattern when we check its RHS. 1193-- See 'addPatTmCs'. 1194computeCovered :: GrdVec -> Delta -> DsM (Maybe Delta) 1195-- The duplication with 'pmCheck' is really unfortunate, but it's simpler than 1196-- separating out the common cases with 'pmCheck', because that would make the 1197-- ConVar case harder to understand. 1198computeCovered [] delta = pure (Just delta) 1199computeCovered (PmLet { pm_id = x, pm_let_expr = e } : ps) delta = do 1200 delta' <- expectJust "x is fresh" <$> addVarCoreCt delta x e 1201 computeCovered ps delta' 1202computeCovered (PmBang{} : ps) delta = do 1203 computeCovered ps delta 1204computeCovered (p : ps) delta 1205 | PmCon{ pm_id = x, pm_con_con = con, pm_con_args = args 1206 , pm_con_dicts = dicts } <- p 1207 = addPmConCts delta x con dicts args >>= \case 1208 Nothing -> pure Nothing 1209 Just delta' -> computeCovered ps delta' 1210 1211{- 1212%************************************************************************ 1213%* * 1214 Pretty printing of exhaustiveness/redundancy check warnings 1215%* * 1216%************************************************************************ 1217-} 1218 1219-- | Check whether any part of pattern match checking is enabled for this 1220-- 'HsMatchContext' (does not matter whether it is the redundancy check or the 1221-- exhaustiveness check). 1222isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool 1223isMatchContextPmChecked dflags origin kind 1224 | isGenerated origin 1225 = False 1226 | otherwise 1227 = wopt Opt_WarnOverlappingPatterns dflags || exhaustive dflags kind 1228 1229-- | Return True when any of the pattern match warnings ('allPmCheckWarnings') 1230-- are enabled, in which case we need to run the pattern match checker. 1231needToRunPmCheck :: DynFlags -> Origin -> Bool 1232needToRunPmCheck dflags origin 1233 | isGenerated origin 1234 = False 1235 | otherwise 1236 = notNull (filter (`wopt` dflags) allPmCheckWarnings) 1237 1238-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility) 1239dsPmWarn :: DynFlags -> DsMatchContext -> [Id] -> PmResult -> DsM () 1240dsPmWarn dflags ctx@(DsMatchContext kind loc) vars pm_result 1241 = when (flag_i || flag_u) $ do 1242 let exists_r = flag_i && notNull redundant 1243 exists_i = flag_i && notNull inaccessible && not is_rec_upd 1244 exists_u = flag_u && notNull uncovered 1245 approx = precision == Approximate 1246 1247 when (approx && (exists_u || exists_i)) $ 1248 putSrcSpanDs loc (warnDs NoReason approx_msg) 1249 1250 when exists_r $ forM_ redundant $ \(dL->L l q) -> do 1251 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns) 1252 (pprEqn q "is redundant")) 1253 when exists_i $ forM_ inaccessible $ \(dL->L l q) -> do 1254 putSrcSpanDs l (warnDs (Reason Opt_WarnOverlappingPatterns) 1255 (pprEqn q "has inaccessible right hand side")) 1256 when exists_u $ putSrcSpanDs loc $ warnDs flag_u_reason $ 1257 pprEqns vars uncovered 1258 where 1259 PmResult 1260 { pmresultRedundant = redundant 1261 , pmresultUncovered = uncovered 1262 , pmresultInaccessible = inaccessible 1263 , pmresultApproximate = precision } = pm_result 1264 1265 flag_i = wopt Opt_WarnOverlappingPatterns dflags 1266 flag_u = exhaustive dflags kind 1267 flag_u_reason = maybe NoReason Reason (exhaustiveWarningFlag kind) 1268 1269 is_rec_upd = case kind of { RecUpd -> True; _ -> False } 1270 -- See Note [Inaccessible warnings for record updates] 1271 1272 maxPatterns = maxUncoveredPatterns dflags 1273 1274 -- Print a single clause (for redundant/with-inaccessible-rhs) 1275 pprEqn q txt = pprContext True ctx (text txt) $ \f -> 1276 f (pprPats kind (map unLoc q)) 1277 1278 -- Print several clauses (for uncovered clauses) 1279 pprEqns vars deltas = pprContext False ctx (text "are non-exhaustive") $ \_ -> 1280 case vars of -- See #11245 1281 [] -> text "Guards do not cover entire pattern space" 1282 _ -> let us = map (\delta -> pprUncovered delta vars) deltas 1283 in hang (text "Patterns not matched:") 4 1284 (vcat (take maxPatterns us) $$ dots maxPatterns us) 1285 1286 approx_msg = vcat 1287 [ hang 1288 (text "Pattern match checker ran into -fmax-pmcheck-models=" 1289 <> int (maxPmCheckModels dflags) 1290 <> text " limit, so") 1291 2 1292 ( bullet <+> text "Redundant clauses might not be reported at all" 1293 $$ bullet <+> text "Redundant clauses might be reported as inaccessible" 1294 $$ bullet <+> text "Patterns reported as unmatched might actually be matched") 1295 , text "Increase the limit or resolve the warnings to suppress this message." ] 1296 1297{- Note [Inaccessible warnings for record updates] 1298~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1299Consider (#12957) 1300 data T a where 1301 T1 :: { x :: Int } -> T Bool 1302 T2 :: { x :: Int } -> T a 1303 T3 :: T a 1304 1305 f :: T Char -> T a 1306 f r = r { x = 3 } 1307 1308The desugarer will (conservatively generate a case for T1 even though 1309it's impossible: 1310 f r = case r of 1311 T1 x -> T1 3 -- Inaccessible branch 1312 T2 x -> T2 3 1313 _ -> error "Missing" 1314 1315We don't want to warn about the inaccessible branch because the programmer 1316didn't put it there! So we filter out the warning here. 1317-} 1318 1319dots :: Int -> [a] -> SDoc 1320dots maxPatterns qs 1321 | qs `lengthExceeds` maxPatterns = text "..." 1322 | otherwise = empty 1323 1324-- | All warning flags that need to run the pattern match checker. 1325allPmCheckWarnings :: [WarningFlag] 1326allPmCheckWarnings = 1327 [ Opt_WarnIncompletePatterns 1328 , Opt_WarnIncompleteUniPatterns 1329 , Opt_WarnIncompletePatternsRecUpd 1330 , Opt_WarnOverlappingPatterns 1331 ] 1332 1333-- | Check whether the exhaustiveness checker should run (exhaustiveness only) 1334exhaustive :: DynFlags -> HsMatchContext id -> Bool 1335exhaustive dflags = maybe False (`wopt` dflags) . exhaustiveWarningFlag 1336 1337-- | Denotes whether an exhaustiveness check is supported, and if so, 1338-- via which 'WarningFlag' it's controlled. 1339-- Returns 'Nothing' if check is not supported. 1340exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag 1341exhaustiveWarningFlag (FunRhs {}) = Just Opt_WarnIncompletePatterns 1342exhaustiveWarningFlag CaseAlt = Just Opt_WarnIncompletePatterns 1343exhaustiveWarningFlag IfAlt = Just Opt_WarnIncompletePatterns 1344exhaustiveWarningFlag LambdaExpr = Just Opt_WarnIncompleteUniPatterns 1345exhaustiveWarningFlag PatBindRhs = Just Opt_WarnIncompleteUniPatterns 1346exhaustiveWarningFlag PatBindGuards = Just Opt_WarnIncompletePatterns 1347exhaustiveWarningFlag ProcExpr = Just Opt_WarnIncompleteUniPatterns 1348exhaustiveWarningFlag RecUpd = Just Opt_WarnIncompletePatternsRecUpd 1349exhaustiveWarningFlag ThPatSplice = Nothing 1350exhaustiveWarningFlag PatSyn = Nothing 1351exhaustiveWarningFlag ThPatQuote = Nothing 1352exhaustiveWarningFlag (StmtCtxt {}) = Nothing -- Don't warn about incomplete patterns 1353 -- in list comprehensions, pattern guards 1354 -- etc. They are often *supposed* to be 1355 -- incomplete 1356 1357-- True <==> singular 1358pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc 1359pprContext singular (DsMatchContext kind _loc) msg rest_of_msg_fun 1360 = vcat [text txt <+> msg, 1361 sep [ text "In" <+> ppr_match <> char ':' 1362 , nest 4 (rest_of_msg_fun pref)]] 1363 where 1364 txt | singular = "Pattern match" 1365 | otherwise = "Pattern match(es)" 1366 1367 (ppr_match, pref) 1368 = case kind of 1369 FunRhs { mc_fun = (dL->L _ fun) } 1370 -> (pprMatchContext kind, \ pp -> ppr fun <+> pp) 1371 _ -> (pprMatchContext kind, \ pp -> pp) 1372 1373pprPats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc 1374pprPats kind pats 1375 = sep [sep (map ppr pats), matchSeparator kind, text "..."] 1376