{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -- | Coverage checking step of the -- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989). -- -- Coverage check guard trees (like @'PmMatch' 'Pre'@) to get a -- 'CheckResult', containing -- -- 1. The set of uncovered values, 'cr_uncov' -- 2. And an annotated tree variant (like @'PmMatch' 'Post'@) that captures -- redundancy and inaccessibility information as 'RedSets' annotations -- -- Basically the UA function from Section 5.1, which is an optimised -- interleaving of U and A from Section 3.2 (Figure 5). -- The Normalised Refinement Types 'Nablas' are maintained in -- "GHC.HsToCore.Pmc.Solver". module GHC.HsToCore.Pmc.Check ( CheckAction(..), checkMatchGroup, checkGRHSs, checkPatBind, checkEmptyCase, checkRecSel ) where import GHC.Prelude import GHC.Builtin.Names ( hasKey, considerAccessibleIdKey, trueDataConKey ) import GHC.HsToCore.Monad ( DsM ) import GHC.HsToCore.Pmc.Types import GHC.HsToCore.Pmc.Utils import GHC.HsToCore.Pmc.Solver import GHC.Driver.DynFlags import GHC.Utils.Outputable import GHC.Tc.Utils.TcType (evVarPred) import GHC.Data.OrdList import GHC.Data.Bag import qualified Data.Semigroup as Semi import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.List.NonEmpty as NE import Data.Coerce import GHC.Types.Var import GHC.Core import GHC.Core.Utils -- | Coverage checking action. Can be composed 'leftToRight' or 'topToBottom'. newtype CheckAction a = CA { forall a. CheckAction a -> Nablas -> DsM (CheckResult a) unCA :: Nablas -> DsM (CheckResult a) } deriving (forall a b. (a -> b) -> CheckAction a -> CheckAction b) -> (forall a b. a -> CheckAction b -> CheckAction a) -> Functor CheckAction forall a b. a -> CheckAction b -> CheckAction a forall a b. (a -> b) -> CheckAction a -> CheckAction b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f $cfmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b fmap :: forall a b. (a -> b) -> CheckAction a -> CheckAction b $c<$ :: forall a b. a -> CheckAction b -> CheckAction a <$ :: forall a b. a -> CheckAction b -> CheckAction a Functor -- | A 'CheckAction' representing a successful pattern-match. matchSucceeded :: CheckAction RedSets matchSucceeded :: CheckAction Post matchSucceeded = (Nablas -> DsM (CheckResult Post)) -> CheckAction Post forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a CA ((Nablas -> DsM (CheckResult Post)) -> CheckAction Post) -> (Nablas -> DsM (CheckResult Post)) -> CheckAction Post forall a b. (a -> b) -> a -> b $ \Nablas inc -> -- succeed CheckResult Post -> DsM (CheckResult Post) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure CheckResult { cr_ret :: Post cr_ret = Post emptyRedSets { rs_cov = inc } , cr_uncov :: Nablas cr_uncov = Nablas forall a. Monoid a => a mempty , cr_approx :: Precision cr_approx = Precision Precise } -- | Composes 'CheckAction's top-to-bottom: -- If a value falls through the resulting action, then it must fall through the -- first action and then through the second action. -- If a value matches the resulting action, then it either matches the -- first action or matches the second action. -- Basically the semantics of the LYG branching construct. topToBottom :: ((Nablas -> (Precision, Nablas)) -> top -> bot -> (Precision, ret)) -> CheckAction top -> CheckAction bot -> CheckAction ret topToBottom :: forall top bot ret. ((Nablas -> (Precision, Nablas)) -> top -> bot -> (Precision, ret)) -> CheckAction top -> CheckAction bot -> CheckAction ret topToBottom (Nablas -> (Precision, Nablas)) -> top -> bot -> (Precision, ret) f (CA Nablas -> DsM (CheckResult top) top) (CA Nablas -> DsM (CheckResult bot) bot) = (Nablas -> DsM (CheckResult ret)) -> CheckAction ret forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a CA ((Nablas -> DsM (CheckResult ret)) -> CheckAction ret) -> (Nablas -> DsM (CheckResult ret)) -> CheckAction ret forall a b. (a -> b) -> a -> b $ \Nablas inc -> do t <- Nablas -> DsM (CheckResult top) top Nablas inc b <- bot (cr_uncov t) limit <- maxPmCheckModels <$> getDynFlags -- See Note [Countering exponential blowup] let throttler Nablas cov = Int -> Nablas -> Nablas -> (Precision, Nablas) throttle Int limit Nablas inc Nablas cov let (prec', ret) = f throttler (cr_ret t) (cr_ret b) pure CheckResult { cr_ret = ret , cr_uncov = cr_uncov b , cr_approx = prec' Semi.<> cr_approx t Semi.<> cr_approx b } -- | Composes 'CheckAction's left-to-right: -- If a value falls through the resulting action, then it either falls through the -- first action or through the second action. -- If a value matches the resulting action, then it must match the first action -- and then match the second action. -- Basically the semantics of the LYG guard construct. leftToRight :: (RedSets -> right -> ret) -> CheckAction RedSets -> CheckAction right -> CheckAction ret leftToRight :: forall right ret. (Post -> right -> ret) -> CheckAction Post -> CheckAction right -> CheckAction ret leftToRight Post -> right -> ret f (CA Nablas -> DsM (CheckResult Post) left) (CA Nablas -> DsM (CheckResult right) right) = (Nablas -> DsM (CheckResult ret)) -> CheckAction ret forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a CA ((Nablas -> DsM (CheckResult ret)) -> CheckAction ret) -> (Nablas -> DsM (CheckResult ret)) -> CheckAction ret forall a b. (a -> b) -> a -> b $ \Nablas inc -> do l <- Nablas -> DsM (CheckResult Post) left Nablas inc r <- right (rs_cov (cr_ret l)) limit <- maxPmCheckModels <$> getDynFlags let uncov = CheckResult Post -> Nablas forall a. CheckResult a -> Nablas cr_uncov CheckResult Post l Nablas -> Nablas -> Nablas forall a. Semigroup a => a -> a -> a Semi.<> CheckResult right -> Nablas forall a. CheckResult a -> Nablas cr_uncov CheckResult right r -- See Note [Countering exponential blowup] let (prec', uncov') = throttle limit inc uncov pure CheckResult { cr_ret = f (cr_ret l) (cr_ret r) , cr_uncov = uncov' , cr_approx = prec' Semi.<> cr_approx l Semi.<> cr_approx r } -- | @throttle limit old new@ returns @old@ if the number of 'Nabla's in @new@ -- is exceeding the given @limit@ and the @old@ number of 'Nabla's. -- See Note [Countering exponential blowup]. throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas) throttle :: Int -> Nablas -> Nablas -> (Precision, Nablas) throttle Int limit old :: Nablas old@(MkNablas Bag Nabla old_ds) new :: Nablas new@(MkNablas Bag Nabla new_ds) --- | pprTrace "PmCheck:throttle" (ppr (length old_ds) <+> ppr (length new_ds) <+> ppr limit) False = undefined | Bag Nabla -> Int forall a. Bag a -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length Bag Nabla new_ds Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int -> Int -> Int forall a. Ord a => a -> a -> a max Int limit (Bag Nabla -> Int forall a. Bag a -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length Bag Nabla old_ds) = (Precision Approximate, Nablas old) | Bool otherwise = (Precision Precise, Nablas new) checkAlternatives :: (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) -- The implementation is pretty similar to -- @traverse1 :: Apply f => (a -> f b) -> NonEmpty a -> f (NonEmpty b)@ checkAlternatives :: forall grdtree anntree. (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) checkAlternatives grdtree -> CheckAction anntree act (grdtree t :| []) = (anntree -> [anntree] -> NonEmpty anntree forall a. a -> [a] -> NonEmpty a :| []) (anntree -> NonEmpty anntree) -> CheckAction anntree -> CheckAction (NonEmpty anntree) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> grdtree -> CheckAction anntree act grdtree t checkAlternatives grdtree -> CheckAction anntree act (grdtree t1 :| (grdtree t2:[grdtree] ts)) = ((Nablas -> (Precision, Nablas)) -> anntree -> NonEmpty anntree -> (Precision, NonEmpty anntree)) -> CheckAction anntree -> CheckAction (NonEmpty anntree) -> CheckAction (NonEmpty anntree) forall top bot ret. ((Nablas -> (Precision, Nablas)) -> top -> bot -> (Precision, ret)) -> CheckAction top -> CheckAction bot -> CheckAction ret topToBottom ((anntree -> NonEmpty anntree -> NonEmpty anntree) -> (Nablas -> (Precision, Nablas)) -> anntree -> NonEmpty anntree -> (Precision, NonEmpty anntree) forall {t} {t} {b} {p}. (t -> t -> b) -> p -> t -> t -> (Precision, b) no_throttling anntree -> NonEmpty anntree -> NonEmpty anntree forall a. a -> NonEmpty a -> NonEmpty a (NE.<|)) (grdtree -> CheckAction anntree act grdtree t1) ((grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) forall grdtree anntree. (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) checkAlternatives grdtree -> CheckAction anntree act (grdtree t2grdtree -> [grdtree] -> NonEmpty grdtree forall a. a -> [a] -> NonEmpty a :|[grdtree] ts)) where no_throttling :: (t -> t -> b) -> p -> t -> t -> (Precision, b) no_throttling t -> t -> b f p _throttler t t t b = (Precision Precise, t -> t -> b f t t t b) emptyRedSets :: RedSets -- Semigroup instance would be misleading! emptyRedSets :: Post emptyRedSets = Nablas -> Nablas -> OrdList (Nablas, SrcInfo) -> Post RedSets Nablas forall a. Monoid a => a mempty Nablas forall a. Monoid a => a mempty OrdList (Nablas, SrcInfo) forall a. Monoid a => a mempty checkGrd :: PmGrd -> CheckAction RedSets checkGrd :: PmGrd -> CheckAction Post checkGrd PmGrd grd = (Nablas -> DsM (CheckResult Post)) -> CheckAction Post forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a CA ((Nablas -> DsM (CheckResult Post)) -> CheckAction Post) -> (Nablas -> DsM (CheckResult Post)) -> CheckAction Post forall a b. (a -> b) -> a -> b $ \Nablas inc -> case PmGrd grd of -- let x = e: Refine with x ~ e PmLet Id x CoreExpr e -> do matched <- Nablas -> PhiCt -> DsM Nablas addPhiCtNablas Nablas inc (Id -> CoreExpr -> PhiCt PhiCoreCt Id x CoreExpr e) tracePm "check:Let" (ppr x <+> char '=' <+> ppr e) pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched } , cr_uncov = mempty , cr_approx = Precise } -- Bang x _: Diverge on x ~ ⊥, refine with x ≁ ⊥ PmBang Id x Maybe SrcInfo mb_info -> do div <- Nablas -> PhiCt -> DsM Nablas addPhiCtNablas Nablas inc (Id -> PhiCt PhiBotCt Id x) matched <- addPhiCtNablas inc (PhiNotBotCt x) -- See Note [Dead bang patterns] -- mb_info = Just info <==> PmBang originates from bang pattern in source let bangs | Just SrcInfo info <- Maybe SrcInfo mb_info = (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo) forall a. a -> OrdList a unitOL (Nablas div, SrcInfo info) | Bool otherwise = OrdList (Nablas, SrcInfo) forall a. OrdList a NilOL tracePm "check:Bang" (ppr x <+> ppr div) pure CheckResult { cr_ret = RedSets { rs_cov = matched, rs_div = div, rs_bangs = bangs } , cr_uncov = mempty , cr_approx = Precise } -- See point (3) of Note [considerAccessible] PmCon Id x (PmAltConLike ConLike con) [Id] _ [Id] _ [Id] _ | Id x Id -> Unique -> Bool forall a. Uniquable a => a -> Unique -> Bool `hasKey` Unique considerAccessibleIdKey , ConLike con ConLike -> Unique -> Bool forall a. Uniquable a => a -> Unique -> Bool `hasKey` Unique trueDataConKey -> CheckResult Post -> DsM (CheckResult Post) forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure CheckResult { cr_ret :: Post cr_ret = Post emptyRedSets { rs_cov = initNablas } , cr_uncov :: Nablas cr_uncov = Nablas forall a. Monoid a => a mempty , cr_approx :: Precision cr_approx = Precision Precise } -- Con: Fall through on x ≁ K and refine with x ~ K ys and type info PmCon Id x PmAltCon con [Id] tvs [Id] dicts [Id] args -> do !div <- if PmAltCon -> Bool isPmAltConMatchStrict PmAltCon con then Nablas -> PhiCt -> DsM Nablas addPhiCtNablas Nablas inc (Id -> PhiCt PhiBotCt Id x) else Nablas -> DsM Nablas forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (f :: * -> *) a. Applicative f => a -> f a pure Nablas forall a. Monoid a => a mempty !matched <- addPhiCtNablas inc (PhiConCt x con tvs (map evVarPred dicts) args) !uncov <- addPhiCtNablas inc (PhiNotConCt x con) tracePm "check:Con" $ vcat [ ppr grd , ppr inc , hang (text "div") 2 (ppr div) , hang (text "matched") 2 (ppr matched) , hang (text "uncov") 2 (ppr uncov) ] pure CheckResult { cr_ret = emptyRedSets { rs_cov = matched, rs_div = div } , cr_uncov = uncov , cr_approx = Precise } checkGrdDag :: GrdDag -> CheckAction RedSets checkGrdDag :: Pre -> CheckAction Post checkGrdDag (GdOne PmGrd g) = PmGrd -> CheckAction Post checkGrd PmGrd g checkGrdDag Pre GdEnd = CheckAction Post matchSucceeded checkGrdDag (GdSeq Pre dl Pre dr) = (Post -> Post -> Post) -> CheckAction Post -> CheckAction Post -> CheckAction Post forall right ret. (Post -> right -> ret) -> CheckAction Post -> CheckAction right -> CheckAction ret leftToRight Post -> Post -> Post merge (Pre -> CheckAction Post checkGrdDag Pre dl) (Pre -> CheckAction Post checkGrdDag Pre dr) where -- Note that -- * the incoming set of dr is the covered set of dl -- * the covered set of dr is a subset of the incoming set of dr -- * this is so that the covered set of dr is the covered set of the -- entire sequence -- Hence we merge by returning @rs_cov ri_r@ as the covered set. merge :: Post -> Post -> Post merge Post ri_l Post ri_r = RedSets { rs_cov :: Nablas rs_cov = Post -> Nablas rs_cov Post ri_r , rs_div :: Nablas rs_div = Post -> Nablas rs_div Post ri_l Nablas -> Nablas -> Nablas forall a. Semigroup a => a -> a -> a Semi.<> Post -> Nablas rs_div Post ri_r , rs_bangs :: OrdList (Nablas, SrcInfo) rs_bangs = Post -> OrdList (Nablas, SrcInfo) rs_bangs Post ri_l OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo) forall a. Semigroup a => a -> a -> a Semi.<> Post -> OrdList (Nablas, SrcInfo) rs_bangs Post ri_r } checkGrdDag (GdAlt Pre dt Pre db) = ((Nablas -> (Precision, Nablas)) -> Post -> Post -> (Precision, Post)) -> CheckAction Post -> CheckAction Post -> CheckAction Post forall top bot ret. ((Nablas -> (Precision, Nablas)) -> top -> bot -> (Precision, ret)) -> CheckAction top -> CheckAction bot -> CheckAction ret topToBottom (Nablas -> (Precision, Nablas)) -> Post -> Post -> (Precision, Post) forall {a}. (Nablas -> (a, Nablas)) -> Post -> Post -> (a, Post) merge (Pre -> CheckAction Post checkGrdDag Pre dt) (Pre -> CheckAction Post checkGrdDag Pre db) where -- The intuition here: ri_b is disjoint with ri_t, because db only gets -- fed the "leftover" uncovered set of dt. But for the GrdDag that follows -- to the right of the GdAlt (say), we have to reunite the RedSets. Hence -- component-wise merge. -- After the GdAlt, we unite the covered sets. If they become too large, we -- throttle, continuing with the incoming set. merge :: (Nablas -> (a, Nablas)) -> Post -> Post -> (a, Post) merge Nablas -> (a, Nablas) throttler Post ri_t Post ri_b = let (a prec, Nablas cov) = Nablas -> (a, Nablas) throttler (Post -> Nablas rs_cov Post ri_t Nablas -> Nablas -> Nablas forall a. Semigroup a => a -> a -> a Semi.<> Post -> Nablas rs_cov Post ri_b) in (a prec, RedSets { rs_cov :: Nablas rs_cov = Nablas cov , rs_div :: Nablas rs_div = Post -> Nablas rs_div Post ri_t Nablas -> Nablas -> Nablas forall a. Semigroup a => a -> a -> a Semi.<> Post -> Nablas rs_div Post ri_b , rs_bangs :: OrdList (Nablas, SrcInfo) rs_bangs = Post -> OrdList (Nablas, SrcInfo) rs_bangs Post ri_t OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo) -> OrdList (Nablas, SrcInfo) forall a. Semigroup a => a -> a -> a Semi.<> Post -> OrdList (Nablas, SrcInfo) rs_bangs Post ri_b }) checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post) checkMatchGroup :: PmMatchGroup Pre -> CheckAction (PmMatchGroup Post) checkMatchGroup (PmMatchGroup NonEmpty (PmMatch Pre) matches) = NonEmpty (PmMatch Post) -> PmMatchGroup Post forall p. NonEmpty (PmMatch p) -> PmMatchGroup p PmMatchGroup (NonEmpty (PmMatch Post) -> PmMatchGroup Post) -> CheckAction (NonEmpty (PmMatch Post)) -> CheckAction (PmMatchGroup Post) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> (PmMatch Pre -> CheckAction (PmMatch Post)) -> NonEmpty (PmMatch Pre) -> CheckAction (NonEmpty (PmMatch Post)) forall grdtree anntree. (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) checkAlternatives PmMatch Pre -> CheckAction (PmMatch Post) checkMatch NonEmpty (PmMatch Pre) matches checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post) checkMatch :: PmMatch Pre -> CheckAction (PmMatch Post) checkMatch (PmMatch { pm_pats :: forall p. PmMatch p -> p pm_pats = Pre grds, pm_grhss :: forall p. PmMatch p -> PmGRHSs p pm_grhss = PmGRHSs Pre grhss }) = (Post -> PmGRHSs Post -> PmMatch Post) -> CheckAction Post -> CheckAction (PmGRHSs Post) -> CheckAction (PmMatch Post) forall right ret. (Post -> right -> ret) -> CheckAction Post -> CheckAction right -> CheckAction ret leftToRight Post -> PmGRHSs Post -> PmMatch Post forall p. p -> PmGRHSs p -> PmMatch p PmMatch (Pre -> CheckAction Post checkGrdDag Pre grds) (PmGRHSs Pre -> CheckAction (PmGRHSs Post) checkGRHSs PmGRHSs Pre grhss) checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post) checkGRHSs :: PmGRHSs Pre -> CheckAction (PmGRHSs Post) checkGRHSs (PmGRHSs { pgs_lcls :: forall p. PmGRHSs p -> p pgs_lcls = Pre lcls, pgs_grhss :: forall p. PmGRHSs p -> NonEmpty (PmGRHS p) pgs_grhss = NonEmpty (PmGRHS Pre) grhss }) = (Post -> NonEmpty (PmGRHS Post) -> PmGRHSs Post) -> CheckAction Post -> CheckAction (NonEmpty (PmGRHS Post)) -> CheckAction (PmGRHSs Post) forall right ret. (Post -> right -> ret) -> CheckAction Post -> CheckAction right -> CheckAction ret leftToRight Post -> NonEmpty (PmGRHS Post) -> PmGRHSs Post forall p. p -> NonEmpty (PmGRHS p) -> PmGRHSs p PmGRHSs (Pre -> CheckAction Post checkGrdDag Pre lcls) ((PmGRHS Pre -> CheckAction (PmGRHS Post)) -> NonEmpty (PmGRHS Pre) -> CheckAction (NonEmpty (PmGRHS Post)) forall grdtree anntree. (grdtree -> CheckAction anntree) -> NonEmpty grdtree -> CheckAction (NonEmpty anntree) checkAlternatives PmGRHS Pre -> CheckAction (PmGRHS Post) checkGRHS NonEmpty (PmGRHS Pre) grhss) checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post) checkGRHS :: PmGRHS Pre -> CheckAction (PmGRHS Post) checkGRHS (PmGRHS { pg_grds :: forall p. PmGRHS p -> p pg_grds = Pre grds, pg_rhs :: forall p. PmGRHS p -> SrcInfo pg_rhs = SrcInfo rhs_info }) = (Post -> SrcInfo -> PmGRHS Post) -> SrcInfo -> Post -> PmGRHS Post forall a b c. (a -> b -> c) -> b -> a -> c flip Post -> SrcInfo -> PmGRHS Post forall p. p -> SrcInfo -> PmGRHS p PmGRHS SrcInfo rhs_info (Post -> PmGRHS Post) -> CheckAction Post -> CheckAction (PmGRHS Post) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Pre -> CheckAction Post checkGrdDag Pre grds checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase -- See Note [Checking EmptyCase] checkEmptyCase :: PmEmptyCase -> CheckAction PmEmptyCase checkEmptyCase pe :: PmEmptyCase pe@(PmEmptyCase { pe_var :: PmEmptyCase -> Id pe_var = Id var }) = (Nablas -> DsM (CheckResult PmEmptyCase)) -> CheckAction PmEmptyCase forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a CA ((Nablas -> DsM (CheckResult PmEmptyCase)) -> CheckAction PmEmptyCase) -> (Nablas -> DsM (CheckResult PmEmptyCase)) -> CheckAction PmEmptyCase forall a b. (a -> b) -> a -> b $ \Nablas inc -> do unc <- Nablas -> PhiCt -> DsM Nablas addPhiCtNablas Nablas inc (Id -> PhiCt PhiNotBotCt Id var) pure CheckResult { cr_ret = pe, cr_uncov = unc, cr_approx = mempty } checkPatBind :: (PmPatBind Pre) -> CheckAction (PmPatBind Post) checkPatBind :: PmPatBind Pre -> CheckAction (PmPatBind Post) checkPatBind = (PmGRHS Pre -> CheckAction (PmGRHS Post)) -> PmPatBind Pre -> CheckAction (PmPatBind Post) forall a b. Coercible a b => a -> b coerce PmGRHS Pre -> CheckAction (PmGRHS Post) checkGRHS checkRecSel :: PmRecSel () -> CheckAction (PmRecSel Id) -- See Note [Detecting incomplete record selectors] in GHC.HsToCore.Pmc checkRecSel :: PmRecSel () -> CheckAction (PmRecSel Id) checkRecSel pr :: PmRecSel () pr@(PmRecSel { pr_arg :: forall v. PmRecSel v -> CoreExpr pr_arg = CoreExpr arg, pr_cons :: forall v. PmRecSel v -> [ConLike] pr_cons = [ConLike] cons }) = (Nablas -> DsM (CheckResult (PmRecSel Id))) -> CheckAction (PmRecSel Id) forall a. (Nablas -> DsM (CheckResult a)) -> CheckAction a CA ((Nablas -> DsM (CheckResult (PmRecSel Id))) -> CheckAction (PmRecSel Id)) -> (Nablas -> DsM (CheckResult (PmRecSel Id))) -> CheckAction (PmRecSel Id) forall a b. (a -> b) -> a -> b $ \Nablas inc -> do arg_id <- case CoreExpr arg of Var Id arg_id -> Id -> IOEnv (Env DsGblEnv DsLclEnv) Id forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a forall (m :: * -> *) a. Monad m => a -> m a return Id arg_id CoreExpr _ -> PredType -> IOEnv (Env DsGblEnv DsLclEnv) Id mkPmId (PredType -> IOEnv (Env DsGblEnv DsLclEnv) Id) -> PredType -> IOEnv (Env DsGblEnv DsLclEnv) Id forall a b. (a -> b) -> a -> b $ HasDebugCallStack => CoreExpr -> PredType CoreExpr -> PredType exprType CoreExpr arg let con_cts = (ConLike -> PhiCt) -> [ConLike] -> [PhiCt] forall a b. (a -> b) -> [a] -> [b] map (Id -> PmAltCon -> PhiCt PhiNotConCt Id arg_id (PmAltCon -> PhiCt) -> (ConLike -> PmAltCon) -> ConLike -> PhiCt forall b c a. (b -> c) -> (a -> b) -> a -> c . ConLike -> PmAltCon PmAltConLike) [ConLike] cons arg_ct = Id -> CoreExpr -> PhiCt PhiCoreCt Id arg_id CoreExpr arg phi_cts = [PhiCt] -> Bag PhiCt forall a. [a] -> Bag a listToBag (PhiCt arg_ct PhiCt -> [PhiCt] -> [PhiCt] forall a. a -> [a] -> [a] : [PhiCt] con_cts) unc <- addPhiCtsNablas inc phi_cts pure CheckResult { cr_ret = pr{ pr_arg_var = arg_id }, cr_uncov = unc, cr_approx = mempty } {- Note [Checking EmptyCase] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -XEmptyCase is useful for matching on empty data types like 'Void'. For example, the following is a complete match: f :: Void -> () f x = case x of {} Really, -XEmptyCase is the only way to write a program that at the same time is safe (@f _ = error "boom"@ is not because of ⊥), doesn't trigger a warning (@f !_ = error "inaccessible" has inaccessible RHS) and doesn't turn an exception into divergence (@f x = f x@). Semantically, unlike every other case expression, -XEmptyCase is strict in its match var x, which rules out ⊥ as an inhabitant. So we add x ≁ ⊥ to the initial Nabla and check if there are any values left to match on. Note [Dead bang patterns] ~~~~~~~~~~~~~~~~~~~~~~~~~ Consider f :: Bool -> Int f True = 1 f !x = 2 Whenever we fall through to the second equation, we will already have evaluated the argument. Thus, the bang pattern serves no purpose and should be warned about. We call this kind of bang patterns "dead". Dead bangs are the ones that under no circumstances can force a thunk that wasn't already forced. Dead bangs are a form of redundant bangs; see below. We can detect dead bang patterns by checking whether @x ~ ⊥@ is satisfiable where the PmBang appears in 'checkGrd'. If not, then clearly the bang is dead. So for a source bang, we add the refined Nabla and the source info to the 'RedSet's 'rs_bangs'. When collecting stuff to warn, we test that Nabla for inhabitants. If it's empty, we'll warn that it's redundant. Note that we don't want to warn for a dead bang that appears on a redundant clause. That is because in that case, we recommend to delete the clause wholly, including its leading pattern match. Dead bang patterns are redundant. But there are bang patterns which are redundant that aren't dead, for example f !() = 0 the bang still forces the match variable, before we attempt to match on (). But it is redundant with the forcing done by the () match. We currently don't detect redundant bangs that aren't dead. Note [Countering exponential blowup] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Precise pattern match exhaustiveness checking is necessarily exponential in the size of some input programs. We implement a counter-measure in the form of the -fmax-pmcheck-models flag, limiting the number of Nablas we check against each pattern by a constant. How do we do that? Consider f True True = () f True True = () And imagine we set our limit to 1 for the sake of the example. The first clause will be checked against the initial Nabla, {}. Doing so will produce an Uncovered set of size 2, containing the models {x≁True} and {x~True,y≁True}. Also we find the first clause to cover the model {x~True,y~True}. But the Uncovered set we get out of the match is too large! We somehow have to ensure not to make things worse than they are already, so we continue checking with a singleton Uncovered set of the initial Nabla {}. Why is this sound (wrt. the notion in GADTs Meet Their Match)? Well, it basically amounts to forgetting that we matched against the first clause. The values represented by {} are a superset of those represented by its two refinements {x≁True} and {x~True,y≁True}. This forgetfulness becomes very apparent in the example above: By continuing with {} we don't detect the second clause as redundant, as it again covers the same non-empty subset of {}. So we don't flag everything as redundant anymore, but still will never flag something as redundant that isn't. For exhaustivity, the converse applies: We will report @f@ as non-exhaustive and report @f _ _@ as missing, which is a superset of the actual missing matches. But soundness means we will never fail to report a missing match. This mechanism is implemented in 'throttle'. Guards are an extreme example in this regard, with #11195 being a particularly dreadful example: Since their RHS are often pretty much unique, we split on a variable (the one representing the RHS) that doesn't occur anywhere else in the program, so we don't actually get useful information out of that split! We counter this by throttling *Uncovered* sets in `leftToRight`. Another challenge is posed by or-patterns (see also Note [Implementation of OrPatterns]): Large matches such as `f (LT; GT) (LT; GT) .... True = 1` will desugar into a long sequence of `GdAlt LT GT`. The careless desugaring of `GdAlt` via `topToBottom` would cause ever enlarging *Covered* sets. So we throttle when merging Covered sets from LT and GT, by using the original incoming covered set. The effect is very like replacing (LT; GT) with a wildcard pattern _. Note [considerAccessible] ~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (T18610) f :: Bool -> Int f x = case (x, x) of (True, True) -> 1 (False, False) -> 2 (True, False) -> 3 -- Warning: Redundant The third case is detected as redundant. But it may be the intent of the programmer to keep the dead code, in order for it not to bitrot or to support debugging scenarios. But there is no way to communicate that to the pattern-match checker! The only way is to deactivate pattern-match checking whole-sale, which is quite annoying. Hence, we define in "GHC.Exts": considerAccessible = True 'considerAccessible' is treated specially by the pattern-match checker in that a guard with it as the scrutinee expression will keep its parent clause alive: g :: Bool -> Int g x = case (x, x) of (True, True) -> 1 (False, False) -> 2 (True, False) | GHC.Exts.considerAccessible -> 3 -- No warning The key bits of the implementation are: 1. Its definition is recognised as known-key (see "GHC.Builtin.Names"). 2. After "GHC.HsToCore.Pmc.Desugar", the guard will end up as a 'PmCon', where the match var is the known-key 'considerAccessible' and the constructor against which it matches is 'True'. 3. We recognise the 'PmCon' in 'GHC.HsToCore.Check.checkGrd' and inflate the incoming set of values for all guards downstream to the unconstrained 'initNablas' set, e.g. /all/ values. (The set of values that falls through that particular guard is empty, as matching 'considerAccessible' against 'True' can't fail.) Note that 'considerAccessible' breaks the invariant that incoming sets of values reaching syntactic children are subsets of that of the syntactic ancestor: A whole match, like that of the third clause of the example, might have no incoming value, but its single RHS has incoming values because of (3). That means the 'is_covered' flag computed in 'GHC.HsToCore.Pmc.cirbsMatch' is irrelevant and should not be used to flag all children as redundant (which is what we used to do). We achieve great benefits with a very simple implementation. There are caveats, though: (A) Putting potentially failing guards /after/ the 'considerAccessible' guard might lead to weird check results, e.g., h :: Bool -> Int h x = case (x, x) of (True, True) -> 1 (False, False) -> 2 (True, False) | GHC.Exts.considerAccessible, False <- x -> 3 -- Warning: Not matched: (_, _) That *is* fixable, although we would pay with a much more complicated implementation. (B) If the programmer puts a 'considerAccessible' marker on an accessible clause, the checker doesn't warn about it. E.g., f :: Bool -> Int f True | considerAccessible = 0 f False = 1 will not emit any warning whatsoever. We could implement code that warns here, but it wouldn't be as simple as it is now. -}