{-# LANGUAGE CPP               #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE LambdaCase        #-}

-- | This module coverage checks pattern matches. It finds
--
--     * Uncovered patterns, certifying non-exhaustivity
--     * Redundant equations
--     * Equations with an inaccessible right-hand-side
--
-- The algorithm is based on the paper
-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989)
--
-- There is an overview Figure 2 in there that's probably helpful.
-- Here is an overview of how it's implemented, which follows the structure of
-- the entry points such as 'pmcMatches':
--
--  1. Desugar source syntax (like 'LMatch') to guard tree variants (like
--     'GrdMatch'), with one of the desugaring functions (like 'desugarMatch').
--     See "GHC.HsToCore.Pmc.Desugar".
--     Follows Section 3.1 in the paper.
--  2. Coverage check guard trees (with a function like 'checkMatch') to get a
--     'CheckResult'. See "GHC.HsToCore.Pmc.Check".
--     The normalised refinement types 'Nabla' are tested for inhabitants by
--     "GHC.HsToCore.Pmc.Solver".
--  3. Collect redundancy information into a 'CIRB' with a function such
--     as 'cirbsMatch'. Follows the R function from Figure 6 of the paper.
--  4. Format and report uncovered patterns and redundant equations ('CIRB')
--     with 'formatReportWarnings'. Basically job of the G function, plus proper
--     pretty printing of the warnings (Section 5.4 of the paper).
--  5. Return 'Nablas' reaching syntactic sub-components for
--     Note [Long-distance information]. Collected by functions such as
--     'ldiMatch'. See Section 4.1 of the paper.
module GHC.HsToCore.Pmc (
        -- Checking and printing
        pmcPatBind, pmcMatches, pmcGRHSs,
        isMatchContextPmChecked,

        -- See Note [Long-distance information]
        addTyCs, addCoreScrutTmCs, addHsScrutTmCs
    ) where

#include "GhclibHsVersions.h"

import GHC.Prelude

import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Utils
import GHC.HsToCore.Pmc.Desugar
import GHC.HsToCore.Pmc.Check
import GHC.HsToCore.Pmc.Solver
import GHC.HsToCore.Pmc.Ppr
import GHC.Types.Basic (Origin(..))
import GHC.Core (CoreExpr)
import GHC.Driver.Session
import GHC.Driver.Env
import GHC.Hs
import GHC.Types.Id
import GHC.Types.SrcLoc
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Types.Var (EvVar)
import GHC.Tc.Types
import GHC.Tc.Utils.TcType (evVarPred)
import {-# SOURCE #-} GHC.HsToCore.Expr (dsLExpr)
import GHC.HsToCore.Monad
import GHC.Data.Bag
import GHC.Data.IOEnv (updEnv, unsafeInterleaveM)
import GHC.Data.OrdList
import GHC.Utils.Monad (mapMaybeM)

import Control.Monad (when, forM_)
import qualified Data.Semigroup as Semi
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import Data.Coerce

--
-- * Exported entry points to the checker
--

-- | A non-empty delta that is initialised from the ambient refinement type
-- capturing long-distance information, or the trivially habitable 'Nablas' if
-- the former is uninhabited.
-- See Note [Recovering from unsatisfiable pattern-matching constraints].
getLdiNablas :: DsM Nablas
getLdiNablas :: DsM Nablas
getLdiNablas = do
  Nablas
nablas <- DsM Nablas
getPmNablas
  Nablas -> DsM Bool
isInhabited Nablas
nablas DsM Bool -> (Bool -> DsM Nablas) -> DsM Nablas
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
True  -> Nablas -> DsM Nablas
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nablas
nablas
    Bool
False -> Nablas -> DsM Nablas
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nablas
initNablas

-- | We need to call the Hs desugarer to get the Core of a let-binding or where
-- clause. We don't want to run the coverage checker when doing so! Efficiency
-- is one concern, but also a lack of properly set up long-distance information
-- might trigger warnings that we normally wouldn't emit.
noCheckDs :: DsM a -> DsM a
noCheckDs :: DsM a -> DsM a
noCheckDs DsM a
k = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let dflags' :: DynFlags
dflags' = (DynFlags -> WarningFlag -> DynFlags)
-> DynFlags -> [WarningFlag] -> DynFlags
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' DynFlags -> WarningFlag -> DynFlags
wopt_unset DynFlags
dflags [WarningFlag]
allPmCheckWarnings
  (Env DsGblEnv DsLclEnv -> Env DsGblEnv DsLclEnv) -> DsM a -> DsM a
forall env env' a. (env -> env') -> IOEnv env' a -> IOEnv env a
updEnv (\Env DsGblEnv DsLclEnv
env -> Env DsGblEnv DsLclEnv
env{env_top :: HscEnv
env_top = (Env DsGblEnv DsLclEnv -> HscEnv
forall gbl lcl. Env gbl lcl -> HscEnv
env_top Env DsGblEnv DsLclEnv
env) {hsc_dflags :: DynFlags
hsc_dflags = DynFlags
dflags'} }) DsM a
k

-- | Check a pattern binding (let, where) for exhaustiveness.
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
-- See Note [pmcPatBind only checks PatBindRhs]
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
pmcPatBind ctxt :: DsMatchContext
ctxt@(DsMatchContext HsMatchContext GhcRn
PatBindRhs SrcSpan
loc) Id
var Pat GhcTc
p = do
  !Nablas
missing <- DsM Nablas
getLdiNablas
  PmPatBind Pre
pat_bind <- DsM (PmPatBind Pre) -> DsM (PmPatBind Pre)
forall a. DsM a -> DsM a
noCheckDs (DsM (PmPatBind Pre) -> DsM (PmPatBind Pre))
-> DsM (PmPatBind Pre) -> DsM (PmPatBind Pre)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Id -> Pat GhcTc -> DsM (PmPatBind Pre)
desugarPatBind SrcSpan
loc Id
var Pat GhcTc
p
  String -> SDoc -> DsM ()
tracePm String
"pmcPatBind {" ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt, Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
var, Pat GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr Pat GhcTc
p, PmPatBind Pre -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmPatBind Pre
pat_bind, Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
missing])
  CheckResult (PmPatBind Post)
result <- CheckAction (PmPatBind Post)
-> Nablas -> DsM (CheckResult (PmPatBind Post))
forall a. CheckAction a -> Nablas -> DsM (CheckResult a)
unCA (PmPatBind Pre -> CheckAction (PmPatBind Post)
checkPatBind PmPatBind Pre
pat_bind) Nablas
missing
  String -> SDoc -> DsM ()
tracePm String
"}: " (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CheckResult (PmPatBind Post) -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult (PmPatBind Post)
result))
  (PmPatBind Post -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult (PmPatBind Post) -> DsM ()
forall ann.
(ann -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings PmPatBind Post -> DsM CIRB
cirbsPatBind DsMatchContext
ctxt [Id
var] CheckResult (PmPatBind Post)
result
pmcPatBind DsMatchContext
_ Id
_ Pat GhcTc
_ = () -> DsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions. Returns the 'Nablas' covered by the RHSs.
pmcGRHSs
  :: HsMatchContext GhcRn         -- ^ Match context, for warning messages
  -> GRHSs GhcTc (LHsExpr GhcTc)  -- ^ The GRHSs to check
  -> DsM (NonEmpty Nablas)        -- ^ Covered 'Nablas' for each RHS, for long
                                  --   distance info
pmcGRHSs :: HsMatchContext GhcRn
-> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty Nablas)
pmcGRHSs HsMatchContext GhcRn
hs_ctxt guards :: GRHSs GhcTc (LHsExpr GhcTc)
guards@(GRHSs XCGRHSs GhcTc (LHsExpr GhcTc)
_ [LGRHS GhcTc (LHsExpr GhcTc)]
grhss HsLocalBinds GhcTc
_) = do
  let combined_loc :: SrcSpan
combined_loc = (SrcSpan -> SrcSpan -> SrcSpan) -> [SrcSpan] -> SrcSpan
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SrcSpan -> SrcSpan -> SrcSpan
combineSrcSpans ((GenLocated
   SrcSpan (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
 -> SrcSpan)
-> [GenLocated
      SrcSpan (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
-> [SrcSpan]
forall a b. (a -> b) -> [a] -> [b]
map GenLocated
  SrcSpan (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
-> SrcSpan
forall l e. GenLocated l e -> l
getLoc [GenLocated
   SrcSpan (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
[LGRHS GhcTc (LHsExpr GhcTc)]
grhss)
      ctxt :: DsMatchContext
ctxt = HsMatchContext GhcRn -> SrcSpan -> DsMatchContext
DsMatchContext HsMatchContext GhcRn
hs_ctxt SrcSpan
combined_loc
  !Nablas
missing <- DsM Nablas
getLdiNablas
  PmGRHSs Pre
matches  <- DsM (PmGRHSs Pre) -> DsM (PmGRHSs Pre)
forall a. DsM a -> DsM a
noCheckDs (DsM (PmGRHSs Pre) -> DsM (PmGRHSs Pre))
-> DsM (PmGRHSs Pre) -> DsM (PmGRHSs Pre)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SDoc -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (PmGRHSs Pre)
desugarGRHSs SrcSpan
combined_loc SDoc
empty GRHSs GhcTc (LHsExpr GhcTc)
guards
  String -> SDoc -> DsM ()
tracePm String
"pmcGRHSs" (SDoc -> Int -> SDoc -> SDoc
hang ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt
                                , String -> SDoc
text String
"Guards:"])
                                Int
2
                                (HsMatchContext GhcRn
-> GRHSs GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)) -> SDoc
forall (idR :: Pass) body passL.
(OutputableBndrId idR, Outputable body) =>
HsMatchContext passL -> GRHSs (GhcPass idR) body -> SDoc
pprGRHSs HsMatchContext GhcRn
hs_ctxt GRHSs GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc))
GRHSs GhcTc (LHsExpr GhcTc)
guards SDoc -> SDoc -> SDoc
$$ Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
missing))
  CheckResult (PmGRHSs Post)
result <- CheckAction (PmGRHSs Post)
-> Nablas -> DsM (CheckResult (PmGRHSs Post))
forall a. CheckAction a -> Nablas -> DsM (CheckResult a)
unCA (PmGRHSs Pre -> CheckAction (PmGRHSs Post)
checkGRHSs PmGRHSs Pre
matches) Nablas
missing
  String -> SDoc -> DsM ()
tracePm String
"}: " (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CheckResult (PmGRHSs Post) -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult (PmGRHSs Post)
result))
  (PmGRHSs Post -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult (PmGRHSs Post) -> DsM ()
forall ann.
(ann -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings PmGRHSs Post -> DsM CIRB
cirbsGRHSs DsMatchContext
ctxt [] CheckResult (PmGRHSs Post)
result
  NonEmpty Nablas -> DsM (NonEmpty Nablas)
forall (m :: * -> *) a. Monad m => a -> m a
return (PmGRHSs Post -> NonEmpty Nablas
ldiGRHSs (CheckResult (PmGRHSs Post) -> PmGRHSs Post
forall a. CheckResult a -> a
cr_ret CheckResult (PmGRHSs Post)
result))

-- | Check a list of syntactic 'Match'es (part of case, functions, etc.), each
-- with a 'Pat' and one or more 'GRHSs':
--
-- @
--   f x y | x == y    = 1   -- match on x and y with two guarded RHSs
--         | otherwise = 2
--   f _ _             = 3   -- clause with a single, un-guarded RHS
-- @
--
-- Returns one non-empty 'Nablas' for 1.) each pattern of a 'Match' and 2.)
-- each of a 'Match'es 'GRHS' for Note [Long-distance information].
--
-- Special case: When there are /no matches/, then the functionassumes it
-- checks and @-XEmptyCase@ with only a single match variable.
-- See Note [Checking EmptyCase].
pmcMatches
  :: DsMatchContext                  -- ^ Match context, for warnings messages
  -> [Id]                            -- ^ Match variables, i.e. x and y above
  -> [LMatch GhcTc (LHsExpr GhcTc)]  -- ^ List of matches
  -> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and
                                     --   GRHS, for long distance info.
pmcMatches :: DsMatchContext
-> [Id]
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM [(Nablas, NonEmpty Nablas)]
pmcMatches DsMatchContext
ctxt [Id]
vars [LMatch GhcTc (LHsExpr GhcTc)]
matches = do
  -- We have to force @missing@ before printing out the trace message,
  -- otherwise we get interleaved output from the solver. This function
  -- should be strict in @missing@ anyway!
  !Nablas
missing <- DsM Nablas
getLdiNablas
  String -> SDoc -> DsM ()
tracePm String
"pmcMatches {" (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$
          SDoc -> Int -> SDoc -> SDoc
hang ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt, [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
vars, String -> SDoc
text String
"Matches:"])
               Int
2
               ([SDoc] -> SDoc
vcat ((GenLocated
   SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
 -> SDoc)
-> [GenLocated
      SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
-> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map GenLocated
  SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
-> SDoc
forall a. Outputable a => a -> SDoc
ppr [GenLocated
   SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
[LMatch GhcTc (LHsExpr GhcTc)]
matches) SDoc -> SDoc -> SDoc
$$ Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nablas
missing)
  case [GenLocated
   SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
-> Maybe
     (NonEmpty
        (GenLocated
           SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))))
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [GenLocated
   SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
[LMatch GhcTc (LHsExpr GhcTc)]
matches of
    Maybe
  (NonEmpty
     (GenLocated
        SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))))
Nothing -> do
      -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
      let var :: Id
var = [Id] -> Id
forall a. [a] -> a
only [Id]
vars
      PmEmptyCase
empty_case <- DsM PmEmptyCase -> DsM PmEmptyCase
forall a. DsM a -> DsM a
noCheckDs (DsM PmEmptyCase -> DsM PmEmptyCase)
-> DsM PmEmptyCase -> DsM PmEmptyCase
forall a b. (a -> b) -> a -> b
$ Id -> DsM PmEmptyCase
desugarEmptyCase Id
var
      CheckResult PmEmptyCase
result <- CheckAction PmEmptyCase -> Nablas -> DsM (CheckResult PmEmptyCase)
forall a. CheckAction a -> Nablas -> DsM (CheckResult a)
unCA (PmEmptyCase -> CheckAction PmEmptyCase
checkEmptyCase PmEmptyCase
empty_case) Nablas
missing
      String -> SDoc -> DsM ()
tracePm String
"}: " (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CheckResult PmEmptyCase -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult PmEmptyCase
result))
      (PmEmptyCase -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult PmEmptyCase -> DsM ()
forall ann.
(ann -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings PmEmptyCase -> DsM CIRB
cirbsEmptyCase DsMatchContext
ctxt [Id]
vars CheckResult PmEmptyCase
result
      [(Nablas, NonEmpty Nablas)] -> DsM [(Nablas, NonEmpty Nablas)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Just NonEmpty
  (GenLocated
     SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc))))
matches -> do
      PmMatchGroup Pre
matches <- DsM (PmMatchGroup Pre) -> DsM (PmMatchGroup Pre)
forall a. DsM a -> DsM a
noCheckDs (DsM (PmMatchGroup Pre) -> DsM (PmMatchGroup Pre))
-> DsM (PmMatchGroup Pre) -> DsM (PmMatchGroup Pre)
forall a b. (a -> b) -> a -> b
$ [Id]
-> NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
-> DsM (PmMatchGroup Pre)
desugarMatches [Id]
vars NonEmpty
  (GenLocated
     SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc))))
NonEmpty (LMatch GhcTc (LHsExpr GhcTc))
matches
      CheckResult (PmMatchGroup Post)
result <- CheckAction (PmMatchGroup Post)
-> Nablas -> DsM (CheckResult (PmMatchGroup Post))
forall a. CheckAction a -> Nablas -> DsM (CheckResult a)
unCA (PmMatchGroup Pre -> CheckAction (PmMatchGroup Post)
checkMatchGroup PmMatchGroup Pre
matches) Nablas
missing
      String -> SDoc -> DsM ()
tracePm String
"}: " (Nablas -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CheckResult (PmMatchGroup Post) -> Nablas
forall a. CheckResult a -> Nablas
cr_uncov CheckResult (PmMatchGroup Post)
result))
      (PmMatchGroup Post -> DsM CIRB)
-> DsMatchContext
-> [Id]
-> CheckResult (PmMatchGroup Post)
-> DsM ()
forall ann.
(ann -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings PmMatchGroup Post -> DsM CIRB
cirbsMatchGroup DsMatchContext
ctxt [Id]
vars CheckResult (PmMatchGroup Post)
result
      [(Nablas, NonEmpty Nablas)] -> DsM [(Nablas, NonEmpty Nablas)]
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (Nablas, NonEmpty Nablas) -> [(Nablas, NonEmpty Nablas)]
forall a. NonEmpty a -> [a]
NE.toList (PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
ldiMatchGroup (CheckResult (PmMatchGroup Post) -> PmMatchGroup Post
forall a. CheckResult a -> a
cr_ret CheckResult (PmMatchGroup Post)
result)))

{- Note [pmcPatBind only checks PatBindRhs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@pmcPatBind@'s sole purpose is to check vanilla pattern bindings, like
@x :: Int; Just x = e@, which is in a @PatBindRhs@ context.
But its caller is also called for individual pattern guards in a @StmtCtxt@.
For example, both pattern guards in @f x y | True <- x, False <- y = ...@ will
go through this function. It makes no sense to do coverage checking there:
  * Pattern guards may well fail. Fall-through is not an unrecoverable panic,
    but rather behavior the programmer expects, so inexhaustivity should not be
    reported.
  * Redundancy is already reported for the whole GRHS via one of the other
    exported coverage checking functions. Also reporting individual redundant
    guards is... redundant. See #17646.
Note that we can't just omit checking of @StmtCtxt@ altogether (by adjusting
'isMatchContextPmChecked'), because that affects the other checking functions,
too.
-}

--
-- * Collecting long-distance information
--

ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
ldiMatchGroup (PmMatchGroup NonEmpty (PmMatch Post)
matches) = PmMatch Post -> (Nablas, NonEmpty Nablas)
ldiMatch (PmMatch Post -> (Nablas, NonEmpty Nablas))
-> NonEmpty (PmMatch Post) -> NonEmpty (Nablas, NonEmpty Nablas)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (PmMatch Post)
matches

ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas)
ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas)
ldiMatch (PmMatch { pm_pats :: forall p. PmMatch p -> p
pm_pats = Post
red, pm_grhss :: forall p. PmMatch p -> PmGRHSs p
pm_grhss = PmGRHSs Post
grhss }) =
  (Post -> Nablas
rs_cov Post
red, PmGRHSs Post -> NonEmpty Nablas
ldiGRHSs PmGRHSs Post
grhss)

ldiGRHSs :: PmGRHSs Post -> NonEmpty Nablas
ldiGRHSs :: PmGRHSs Post -> NonEmpty Nablas
ldiGRHSs (PmGRHSs { pgs_grhss :: forall p. PmGRHSs p -> NonEmpty (PmGRHS p)
pgs_grhss = NonEmpty (PmGRHS Post)
grhss }) = PmGRHS Post -> Nablas
ldiGRHS (PmGRHS Post -> Nablas)
-> NonEmpty (PmGRHS Post) -> NonEmpty Nablas
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (PmGRHS Post)
grhss

ldiGRHS :: PmGRHS Post -> Nablas
ldiGRHS :: PmGRHS Post -> Nablas
ldiGRHS (PmGRHS { pg_grds :: forall p. PmGRHS p -> p
pg_grds = Post
red }) = Post -> Nablas
rs_cov Post
red

--
-- * Collecting redundancy information
--

-- | The result of redundancy checking:
--    * RHSs classified as /C/overed, /I/naccessible and /R/edundant
--    * And redundant /B/ang patterns. See Note [Dead bang patterns].
data CIRB
  = CIRB
  { CIRB -> OrdList SrcInfo
cirb_cov   :: !(OrdList SrcInfo) -- ^ Covered clauses
  , CIRB -> OrdList SrcInfo
cirb_inacc :: !(OrdList SrcInfo) -- ^ Inaccessible clauses
  , CIRB -> OrdList SrcInfo
cirb_red   :: !(OrdList SrcInfo) -- ^ Redundant clauses
  , CIRB -> OrdList SrcInfo
cirb_bangs :: !(OrdList SrcInfo) -- ^ Redundant bang patterns
  }

instance Semigroup CIRB where
  CIRB OrdList SrcInfo
a OrdList SrcInfo
b OrdList SrcInfo
c OrdList SrcInfo
d <> :: CIRB -> CIRB -> CIRB
<> CIRB OrdList SrcInfo
e OrdList SrcInfo
f OrdList SrcInfo
g OrdList SrcInfo
h = OrdList SrcInfo
-> OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo -> CIRB
CIRB (OrdList SrcInfo
a OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
<> OrdList SrcInfo
e) (OrdList SrcInfo
b OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
<> OrdList SrcInfo
f) (OrdList SrcInfo
c OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
<> OrdList SrcInfo
g) (OrdList SrcInfo
d OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
<> OrdList SrcInfo
h)
    where <> :: OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
(<>) = OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
forall a. Semigroup a => a -> a -> a
(Semi.<>)

instance Monoid CIRB where
  mempty :: CIRB
mempty = OrdList SrcInfo
-> OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo -> CIRB
CIRB OrdList SrcInfo
forall a. Monoid a => a
mempty OrdList SrcInfo
forall a. Monoid a => a
mempty OrdList SrcInfo
forall a. Monoid a => a
mempty OrdList SrcInfo
forall a. Monoid a => a
mempty

-- See Note [Determining inaccessible clauses]
ensureOneNotRedundant :: CIRB -> CIRB
ensureOneNotRedundant :: CIRB -> CIRB
ensureOneNotRedundant CIRB
ci = case CIRB
ci of
  CIRB { cirb_cov :: CIRB -> OrdList SrcInfo
cirb_cov = OrdList SrcInfo
NilOL, cirb_inacc :: CIRB -> OrdList SrcInfo
cirb_inacc = OrdList SrcInfo
NilOL, cirb_red :: CIRB -> OrdList SrcInfo
cirb_red = ConsOL SrcInfo
r OrdList SrcInfo
rs }
    -> CIRB
ci { cirb_inacc :: OrdList SrcInfo
cirb_inacc = SrcInfo -> OrdList SrcInfo
forall a. a -> OrdList a
unitOL SrcInfo
r, cirb_red :: OrdList SrcInfo
cirb_red = OrdList SrcInfo
rs }
  CIRB
_ -> CIRB
ci

-- | Only adds the redundant bangs to the @CIRB@ if there is at least one
-- non-redundant 'SrcInfo'. There is no point in remembering a redundant bang
-- if the whole match is redundant!
addRedundantBangs :: OrdList SrcInfo -> CIRB -> CIRB
addRedundantBangs :: OrdList SrcInfo -> CIRB -> CIRB
addRedundantBangs OrdList SrcInfo
_red_bangs cirb :: CIRB
cirb@CIRB { cirb_cov :: CIRB -> OrdList SrcInfo
cirb_cov = OrdList SrcInfo
NilOL, cirb_inacc :: CIRB -> OrdList SrcInfo
cirb_inacc = OrdList SrcInfo
NilOL } =
  CIRB
cirb
addRedundantBangs OrdList SrcInfo
red_bangs  CIRB
cirb =
  CIRB
cirb { cirb_bangs :: OrdList SrcInfo
cirb_bangs = CIRB -> OrdList SrcInfo
cirb_bangs CIRB
cirb OrdList SrcInfo -> OrdList SrcInfo -> OrdList SrcInfo
forall a. Semigroup a => a -> a -> a
Semi.<> OrdList SrcInfo
red_bangs }

-- | Checks the 'Nablas' in a 'RedSets' for inhabitants and returns
--    1. Whether the Covered set was inhabited
--    2. Whether the Diverging set was inhabited
--    3. All source bangs whose 'Nablas' were empty, which means they are
--       redundant.
testRedSets :: RedSets -> DsM (Bool, Bool, OrdList SrcInfo)
testRedSets :: Post -> DsM (Bool, Bool, OrdList SrcInfo)
testRedSets RedSets { rs_cov :: Post -> Nablas
rs_cov = Nablas
cov, rs_div :: Post -> Nablas
rs_div = Nablas
div, rs_bangs :: Post -> OrdList (Nablas, SrcInfo)
rs_bangs = OrdList (Nablas, SrcInfo)
bangs } = do
  Bool
is_covered  <- Nablas -> DsM Bool
isInhabited Nablas
cov
  Bool
may_diverge <- Nablas -> DsM Bool
isInhabited Nablas
div
  [SrcInfo]
red_bangs   <- (((Nablas, SrcInfo)
  -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo))
 -> [(Nablas, SrcInfo)] -> IOEnv (Env DsGblEnv DsLclEnv) [SrcInfo])
-> [(Nablas, SrcInfo)]
-> ((Nablas, SrcInfo)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo))
-> IOEnv (Env DsGblEnv DsLclEnv) [SrcInfo]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Nablas, SrcInfo)
 -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo))
-> [(Nablas, SrcInfo)] -> IOEnv (Env DsGblEnv DsLclEnv) [SrcInfo]
forall (m :: * -> *) a b.
Applicative m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM (OrdList (Nablas, SrcInfo) -> [(Nablas, SrcInfo)]
forall a. OrdList a -> [a]
fromOL OrdList (Nablas, SrcInfo)
bangs) (((Nablas, SrcInfo)
  -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo))
 -> IOEnv (Env DsGblEnv DsLclEnv) [SrcInfo])
-> ((Nablas, SrcInfo)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo))
-> IOEnv (Env DsGblEnv DsLclEnv) [SrcInfo]
forall a b. (a -> b) -> a -> b
$ \(Nablas
nablas, SrcInfo
bang) ->
    Nablas -> DsM Bool
isInhabited Nablas
nablas DsM Bool
-> (Bool -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo))
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True  -> Maybe SrcInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe SrcInfo
forall a. Maybe a
Nothing
      Bool
False -> Maybe SrcInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe SrcInfo)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SrcInfo -> Maybe SrcInfo
forall a. a -> Maybe a
Just SrcInfo
bang)
  (Bool, Bool, OrdList SrcInfo) -> DsM (Bool, Bool, OrdList SrcInfo)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
is_covered, Bool
may_diverge, [SrcInfo] -> OrdList SrcInfo
forall a. [a] -> OrdList a
toOL [SrcInfo]
red_bangs)

cirbsMatchGroup :: PmMatchGroup Post -> DsM CIRB
cirbsMatchGroup :: PmMatchGroup Post -> DsM CIRB
cirbsMatchGroup (PmMatchGroup NonEmpty (PmMatch Post)
matches) =
  NonEmpty CIRB -> CIRB
forall a. Semigroup a => NonEmpty a -> a
Semi.sconcat (NonEmpty CIRB -> CIRB)
-> IOEnv (Env DsGblEnv DsLclEnv) (NonEmpty CIRB) -> DsM CIRB
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmMatch Post -> DsM CIRB)
-> NonEmpty (PmMatch Post)
-> IOEnv (Env DsGblEnv DsLclEnv) (NonEmpty CIRB)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PmMatch Post -> DsM CIRB
cirbsMatch NonEmpty (PmMatch Post)
matches

cirbsMatch :: PmMatch Post -> DsM CIRB
cirbsMatch :: PmMatch Post -> DsM CIRB
cirbsMatch PmMatch { pm_pats :: forall p. PmMatch p -> p
pm_pats = Post
red, pm_grhss :: forall p. PmMatch p -> PmGRHSs p
pm_grhss = PmGRHSs Post
grhss } = do
  (Bool
_is_covered, Bool
may_diverge, OrdList SrcInfo
red_bangs) <- Post -> DsM (Bool, Bool, OrdList SrcInfo)
testRedSets Post
red
  -- Don't look at is_covered: If it is True, all children are redundant anyway,
  -- unless there is a 'considerAccessible', which may break that rule
  -- intentionally. See Note [considerAccessible] in "GHC.HsToCore.Pmc.Check".
  CIRB
cirb <- PmGRHSs Post -> DsM CIRB
cirbsGRHSs PmGRHSs Post
grhss
  CIRB -> DsM CIRB
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CIRB -> DsM CIRB) -> CIRB -> DsM CIRB
forall a b. (a -> b) -> a -> b
$ OrdList SrcInfo -> CIRB -> CIRB
addRedundantBangs OrdList SrcInfo
red_bangs
       -- See Note [Determining inaccessible clauses]
       (CIRB -> CIRB) -> CIRB -> CIRB
forall a b. (a -> b) -> a -> b
$ Bool -> (CIRB -> CIRB) -> CIRB -> CIRB
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
may_diverge CIRB -> CIRB
ensureOneNotRedundant
       (CIRB -> CIRB) -> CIRB -> CIRB
forall a b. (a -> b) -> a -> b
$ CIRB
cirb

cirbsGRHSs :: PmGRHSs Post -> DsM CIRB
cirbsGRHSs :: PmGRHSs Post -> DsM CIRB
cirbsGRHSs (PmGRHSs { pgs_grhss :: forall p. PmGRHSs p -> NonEmpty (PmGRHS p)
pgs_grhss = NonEmpty (PmGRHS Post)
grhss }) = NonEmpty CIRB -> CIRB
forall a. Semigroup a => NonEmpty a -> a
Semi.sconcat (NonEmpty CIRB -> CIRB)
-> IOEnv (Env DsGblEnv DsLclEnv) (NonEmpty CIRB) -> DsM CIRB
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PmGRHS Post -> DsM CIRB)
-> NonEmpty (PmGRHS Post)
-> IOEnv (Env DsGblEnv DsLclEnv) (NonEmpty CIRB)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PmGRHS Post -> DsM CIRB
cirbsGRHS NonEmpty (PmGRHS Post)
grhss

cirbsGRHS :: PmGRHS Post -> DsM CIRB
cirbsGRHS :: PmGRHS Post -> DsM CIRB
cirbsGRHS PmGRHS { pg_grds :: forall p. PmGRHS p -> p
pg_grds = Post
red, pg_rhs :: forall p. PmGRHS p -> SrcInfo
pg_rhs = SrcInfo
info } = do
  (Bool
is_covered, Bool
may_diverge, OrdList SrcInfo
red_bangs) <- Post -> DsM (Bool, Bool, OrdList SrcInfo)
testRedSets Post
red
  let cirb :: CIRB
cirb | Bool
is_covered  = CIRB
forall a. Monoid a => a
mempty { cirb_cov :: OrdList SrcInfo
cirb_cov   = SrcInfo -> OrdList SrcInfo
forall a. a -> OrdList a
unitOL SrcInfo
info }
           | Bool
may_diverge = CIRB
forall a. Monoid a => a
mempty { cirb_inacc :: OrdList SrcInfo
cirb_inacc = SrcInfo -> OrdList SrcInfo
forall a. a -> OrdList a
unitOL SrcInfo
info }
           | Bool
otherwise   = CIRB
forall a. Monoid a => a
mempty { cirb_red :: OrdList SrcInfo
cirb_red   = SrcInfo -> OrdList SrcInfo
forall a. a -> OrdList a
unitOL SrcInfo
info }
  CIRB -> DsM CIRB
forall (f :: * -> *) a. Applicative f => a -> f a
pure (OrdList SrcInfo -> CIRB -> CIRB
addRedundantBangs OrdList SrcInfo
red_bangs CIRB
cirb)

cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
cirbsEmptyCase PmEmptyCase
_ = CIRB -> DsM CIRB
forall (f :: * -> *) a. Applicative f => a -> f a
pure CIRB
forall a. Monoid a => a
mempty

cirbsPatBind :: PmPatBind Post -> DsM CIRB
cirbsPatBind :: PmPatBind Post -> DsM CIRB
cirbsPatBind = (PmGRHS Post -> DsM CIRB) -> PmPatBind Post -> DsM CIRB
coerce PmGRHS Post -> DsM CIRB
cirbsGRHS

{- Note [Determining inaccessible clauses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  f _  True = ()
  f () True = ()
  f _  _    = ()
Is f's second clause redundant? The perhaps surprising answer is, no, it isn't!
@f (error "boom") False@ will force the error with clause 2, but will return
() if it was deleted, so clearly not redundant. Yet for now combination of
arguments we can ever reach clause 2's RHS, so we say it has inaccessible RHS
(as opposed to being completely redundant).

We detect an inaccessible RHS simply by pretending it's redundant, until we see
-}

--
-- * Formatting and reporting warnings
--

-- | Given a function that collects 'CIRB's, this function will emit warnings
-- for a 'CheckResult'.
formatReportWarnings :: (ann -> DsM CIRB) -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings :: (ann -> DsM CIRB)
-> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings ann -> DsM CIRB
collect DsMatchContext
ctx [Id]
vars cr :: CheckResult ann
cr@CheckResult { cr_ret :: forall a. CheckResult a -> a
cr_ret = ann
ann } = do
  CIRB
cov_info <- ann -> DsM CIRB
collect ann
ann
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
reportWarnings DynFlags
dflags DsMatchContext
ctx [Id]
vars CheckResult ann
cr{cr_ret :: CIRB
cr_ret=CIRB
cov_info}

-- | Issue all the warnings
-- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
reportWarnings :: DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
reportWarnings :: DynFlags -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
reportWarnings DynFlags
dflags ctx :: DsMatchContext
ctx@(DsMatchContext HsMatchContext GhcRn
kind SrcSpan
loc) [Id]
vars
  CheckResult { cr_ret :: forall a. CheckResult a -> a
cr_ret    = CIRB { cirb_inacc :: CIRB -> OrdList SrcInfo
cirb_inacc = OrdList SrcInfo
inaccessible_rhss
                                 , cirb_red :: CIRB -> OrdList SrcInfo
cirb_red   = OrdList SrcInfo
redundant_rhss
                                 , cirb_bangs :: CIRB -> OrdList SrcInfo
cirb_bangs = OrdList SrcInfo
redundant_bangs }
              , cr_uncov :: forall a. CheckResult a -> Nablas
cr_uncov  = Nablas
uncovered
              , cr_approx :: forall a. CheckResult a -> Precision
cr_approx = Precision
precision }
  = Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
flag_i Bool -> Bool -> Bool
|| Bool
flag_u Bool -> Bool -> Bool
|| Bool
flag_b) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ do
      [Nabla]
unc_examples <- [Id] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered [Id]
vars (Int
maxPatterns Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Nablas
uncovered
      let exists_r :: Bool
exists_r = Bool
flag_i Bool -> Bool -> Bool
&& OrdList SrcInfo -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull OrdList SrcInfo
redundant_rhss
          exists_i :: Bool
exists_i = Bool
flag_i Bool -> Bool -> Bool
&& OrdList SrcInfo -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull OrdList SrcInfo
inaccessible_rhss
          exists_u :: Bool
exists_u = Bool
flag_u Bool -> Bool -> Bool
&& [Nabla] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull [Nabla]
unc_examples
          exists_b :: Bool
exists_b = Bool
flag_b Bool -> Bool -> Bool
&& OrdList SrcInfo -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull OrdList SrcInfo
redundant_bangs
          approx :: Bool
approx   = Precision
precision Precision -> Precision -> Bool
forall a. Eq a => a -> a -> Bool
== Precision
Approximate

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
approx Bool -> Bool -> Bool
&& (Bool
exists_u Bool -> Bool -> Bool
|| Bool
exists_i)) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
loc (DiagnosticReason -> SDoc -> DsM ()
diagnosticDs DiagnosticReason
WarningWithoutFlag SDoc
approx_msg)

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_b (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ OrdList SrcInfo -> (SrcInfo -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ OrdList SrcInfo
redundant_bangs ((SrcInfo -> DsM ()) -> DsM ()) -> (SrcInfo -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(SrcInfo (L SrcSpan
l SDoc
q)) ->
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (DiagnosticReason -> SDoc -> DsM ()
diagnosticDs (WarningFlag -> DiagnosticReason
WarningWithFlag WarningFlag
Opt_WarnRedundantBangPatterns)
                                     (SDoc -> String -> SDoc
pprEqn SDoc
q String
"has redundant bang"))

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_r (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ OrdList SrcInfo -> (SrcInfo -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ OrdList SrcInfo
redundant_rhss ((SrcInfo -> DsM ()) -> DsM ()) -> (SrcInfo -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(SrcInfo (L SrcSpan
l SDoc
q)) ->
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (DiagnosticReason -> SDoc -> DsM ()
diagnosticDs (WarningFlag -> DiagnosticReason
WarningWithFlag WarningFlag
Opt_WarnOverlappingPatterns)
                                     (SDoc -> String -> SDoc
pprEqn SDoc
q String
"is redundant"))
      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_i (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ OrdList SrcInfo -> (SrcInfo -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ OrdList SrcInfo
inaccessible_rhss ((SrcInfo -> DsM ()) -> DsM ()) -> (SrcInfo -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(SrcInfo (L SrcSpan
l SDoc
q)) ->
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (DiagnosticReason -> SDoc -> DsM ()
diagnosticDs (WarningFlag -> DiagnosticReason
WarningWithFlag WarningFlag
Opt_WarnOverlappingPatterns)
                                     (SDoc -> String -> SDoc
pprEqn SDoc
q String
"has inaccessible right hand side"))

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_u (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
loc (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ DiagnosticReason -> SDoc -> DsM ()
diagnosticDs DiagnosticReason
flag_u_reason (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$
        [Id] -> [Nabla] -> SDoc
pprEqns [Id]
vars [Nabla]
unc_examples
  where
    flag_i :: Bool
flag_i = DynFlags -> HsMatchContext GhcRn -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
overlapping DynFlags
dflags HsMatchContext GhcRn
kind
    flag_u :: Bool
flag_u = DynFlags -> HsMatchContext GhcRn -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext GhcRn
kind
    flag_b :: Bool
flag_b = DynFlags -> Bool
redundantBang DynFlags
dflags
    flag_u_reason :: DiagnosticReason
flag_u_reason = DiagnosticReason
-> (WarningFlag -> DiagnosticReason)
-> Maybe WarningFlag
-> DiagnosticReason
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DiagnosticReason
WarningWithoutFlag WarningFlag -> DiagnosticReason
WarningWithFlag (HsMatchContext GhcRn -> Maybe WarningFlag
forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag HsMatchContext GhcRn
kind)

    maxPatterns :: Int
maxPatterns = DynFlags -> Int
maxUncoveredPatterns DynFlags
dflags

    -- Print a single clause (for redundant/with-inaccessible-rhs)
    pprEqn :: SDoc -> String -> SDoc
pprEqn SDoc
q String
txt = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext Bool
True DsMatchContext
ctx (String -> SDoc
text String
txt) (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \SDoc -> SDoc
f ->
      SDoc -> SDoc
f (SDoc
q SDoc -> SDoc -> SDoc
<+> HsMatchContext GhcRn -> SDoc
forall p. HsMatchContext p -> SDoc
matchSeparator HsMatchContext GhcRn
kind SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"...")

    -- Print several clauses (for uncovered clauses)
    pprEqns :: [Id] -> [Nabla] -> SDoc
pprEqns [Id]
vars [Nabla]
nablas = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext Bool
False DsMatchContext
ctx (String -> SDoc
text String
"are non-exhaustive") (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \SDoc -> SDoc
_ ->
      case [Id]
vars of -- See #11245
           [] -> String -> SDoc
text String
"Guards do not cover entire pattern space"
           [Id]
_  -> let us :: [SDoc]
us = (Nabla -> SDoc) -> [Nabla] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (\Nabla
nabla -> Nabla -> [Id] -> SDoc
pprUncovered Nabla
nabla [Id]
vars) [Nabla]
nablas
                     pp_tys :: SDoc
pp_tys = [Kind] -> SDoc
forall a. Outputable a => [a] -> SDoc
pprQuotedList ([Kind] -> SDoc) -> [Kind] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Id -> Kind) -> [Id] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Kind
idType [Id]
vars
                 in  SDoc -> Int -> SDoc -> SDoc
hang
                       (String -> SDoc
text String
"Patterns of type" SDoc -> SDoc -> SDoc
<+> SDoc
pp_tys SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"not matched:")
                       Int
4
                       ([SDoc] -> SDoc
vcat (Int -> [SDoc] -> [SDoc]
forall a. Int -> [a] -> [a]
take Int
maxPatterns [SDoc]
us) SDoc -> SDoc -> SDoc
$$ Int -> [SDoc] -> SDoc
forall a. Int -> [a] -> SDoc
dots Int
maxPatterns [SDoc]
us)

    approx_msg :: SDoc
approx_msg = [SDoc] -> SDoc
vcat
      [ SDoc -> Int -> SDoc -> SDoc
hang
          (String -> SDoc
text String
"Pattern match checker ran into -fmax-pmcheck-models="
            SDoc -> SDoc -> SDoc
<> Int -> SDoc
int (DynFlags -> Int
maxPmCheckModels DynFlags
dflags)
            SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
" limit, so")
          Int
2
          (  SDoc
bullet SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Redundant clauses might not be reported at all"
          SDoc -> SDoc -> SDoc
$$ SDoc
bullet SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Redundant clauses might be reported as inaccessible"
          SDoc -> SDoc -> SDoc
$$ SDoc
bullet SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"Patterns reported as unmatched might actually be matched")
      , String -> SDoc
text String
"Increase the limit or resolve the warnings to suppress this message." ]

getNFirstUncovered :: [Id] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered :: [Id] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered [Id]
vars Int
n (MkNablas Bag Nabla
nablas) = Int -> [Nabla] -> DsM [Nabla]
go Int
n (Bag Nabla -> [Nabla]
forall a. Bag a -> [a]
bagToList Bag Nabla
nablas)
  where
    go :: Int -> [Nabla] -> DsM [Nabla]
go Int
0 [Nabla]
_              = [Nabla] -> DsM [Nabla]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go Int
_ []             = [Nabla] -> DsM [Nabla]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go Int
n (Nabla
nabla:[Nabla]
nablas) = do
      [Nabla]
front <- [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
vars Int
n Nabla
nabla
      [Nabla]
back <- Int -> [Nabla] -> DsM [Nabla]
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Nabla] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Nabla]
front) [Nabla]
nablas
      [Nabla] -> DsM [Nabla]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Nabla]
front [Nabla] -> [Nabla] -> [Nabla]
forall a. [a] -> [a] -> [a]
++ [Nabla]
back)

dots :: Int -> [a] -> SDoc
dots :: Int -> [a] -> SDoc
dots Int
maxPatterns [a]
qs
    | [a]
qs [a] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
maxPatterns = String -> SDoc
text String
"..."
    | Bool
otherwise                      = SDoc
empty

pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pprContext Bool
singular (DsMatchContext HsMatchContext GhcRn
kind SrcSpan
_loc) SDoc
msg (SDoc -> SDoc) -> SDoc
rest_of_msg_fun
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
txt SDoc -> SDoc -> SDoc
<+> SDoc
msg,
          [SDoc] -> SDoc
sep [ String -> SDoc
text String
"In" SDoc -> SDoc -> SDoc
<+> SDoc
ppr_match SDoc -> SDoc -> SDoc
<> Char -> SDoc
char Char
':'
              , Int -> SDoc -> SDoc
nest Int
4 ((SDoc -> SDoc) -> SDoc
rest_of_msg_fun SDoc -> SDoc
pref)]]
  where
    txt :: String
txt | Bool
singular  = String
"Pattern match"
        | Bool
otherwise = String
"Pattern match(es)"

    (SDoc
ppr_match, SDoc -> SDoc
pref)
        = case HsMatchContext GhcRn
kind of
             FunRhs { mc_fun :: forall p. HsMatchContext p -> LIdP p
mc_fun = L _ fun }
                  -> (HsMatchContext GhcRn -> SDoc
forall p.
(Outputable (IdP p), UnXRec p) =>
HsMatchContext p -> SDoc
pprMatchContext HsMatchContext GhcRn
kind, \ SDoc
pp -> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
fun SDoc -> SDoc -> SDoc
<+> SDoc
pp)
             HsMatchContext GhcRn
_    -> (HsMatchContext GhcRn -> SDoc
forall p.
(Outputable (IdP p), UnXRec p) =>
HsMatchContext p -> SDoc
pprMatchContext HsMatchContext GhcRn
kind, \ SDoc
pp -> SDoc
pp)

--
-- * Adding external long-distance information
--

-- | Locally update 'dsl_nablas' with the given action, but defer evaluation
-- with 'unsafeInterleaveM' in order not to do unnecessary work.
locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a
locallyExtendPmNablas :: (Nablas -> DsM Nablas) -> DsM a -> DsM a
locallyExtendPmNablas Nablas -> DsM Nablas
ext DsM a
k = do
  Nablas
nablas <- DsM Nablas
getLdiNablas
  Nablas
nablas' <- DsM Nablas -> DsM Nablas
forall env a. IOEnv env a -> IOEnv env a
unsafeInterleaveM (DsM Nablas -> DsM Nablas) -> DsM Nablas -> DsM Nablas
forall a b. (a -> b) -> a -> b
$ Nablas -> DsM Nablas
ext Nablas
nablas
  Nablas -> DsM a -> DsM a
forall a. Nablas -> DsM a -> DsM a
updPmNablas Nablas
nablas' DsM a
k

-- | Add in-scope type constraints if the coverage checker might run and then
-- run the given action.
addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
addTyCs :: Origin -> Bag Id -> DsM a -> DsM a
addTyCs Origin
origin Bag Id
ev_vars DsM a
m = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  Bool -> (DsM a -> DsM a) -> DsM a -> DsM a
forall a. Bool -> (a -> a) -> a -> a
applyWhen (DynFlags -> Origin -> Bool
needToRunPmCheck DynFlags
dflags Origin
origin)
            ((Nablas -> DsM Nablas) -> DsM a -> DsM a
forall a. (Nablas -> DsM Nablas) -> DsM a -> DsM a
locallyExtendPmNablas ((Nablas -> DsM Nablas) -> DsM a -> DsM a)
-> (Nablas -> DsM Nablas) -> DsM a -> DsM a
forall a b. (a -> b) -> a -> b
$ \Nablas
nablas ->
              Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas (Kind -> PhiCt
PhiTyCt (Kind -> PhiCt) -> (Id -> Kind) -> Id -> PhiCt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Kind
evVarPred (Id -> PhiCt) -> Bag Id -> PhiCts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bag Id
ev_vars))
            DsM a
m

-- | Add equalities for the 'CoreExpr' scrutinee to the local 'DsM' environment
-- when checking a case expression:
--     case e of x { matches }
-- When checking matches we record that (x ~ e) where x is the initial
-- uncovered. All matches will have to satisfy this equality.
addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs Maybe CoreExpr
Nothing    [Id]
_   DsM a
k = DsM a
k
addCoreScrutTmCs (Just CoreExpr
scr) [Id
x] DsM a
k =
  ((Nablas -> DsM Nablas) -> DsM a -> DsM a)
-> DsM a -> (Nablas -> DsM Nablas) -> DsM a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Nablas -> DsM Nablas) -> DsM a -> DsM a
forall a. (Nablas -> DsM Nablas) -> DsM a -> DsM a
locallyExtendPmNablas DsM a
k ((Nablas -> DsM Nablas) -> DsM a)
-> (Nablas -> DsM Nablas) -> DsM a
forall a b. (a -> b) -> a -> b
$ \Nablas
nablas ->
    Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas (PhiCt -> PhiCts
forall a. a -> Bag a
unitBag (Id -> CoreExpr -> PhiCt
PhiCoreCt Id
x CoreExpr
scr))
addCoreScrutTmCs Maybe CoreExpr
_   [Id]
_   DsM a
_ = String -> DsM a
forall a. String -> a
panic String
"addCoreScrutTmCs: scrutinee, but more than one match id"

-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr' first.
addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
addHsScrutTmCs Maybe (LHsExpr GhcTc)
Nothing    [Id]
_    DsM a
k = DsM a
k
addHsScrutTmCs (Just LHsExpr GhcTc
scr) [Id]
vars DsM a
k = do
  CoreExpr
scr_e <- LHsExpr GhcTc -> DsM CoreExpr
dsLExpr LHsExpr GhcTc
scr
  Maybe CoreExpr -> [Id] -> DsM a -> DsM a
forall a. Maybe CoreExpr -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs (CoreExpr -> Maybe CoreExpr
forall a. a -> Maybe a
Just CoreExpr
scr_e) [Id]
vars DsM a
k

{- Note [Long-distance information]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  data Color = R | G | B
  f :: Color -> Int
  f R = …
  f c = … (case c of
          G -> True
          B -> False) …

Humans can make the "long-distance connection" between the outer pattern match
and the nested case pattern match to see that the inner pattern match is
exhaustive: @c@ can't be @R@ anymore because it was matched in the first clause
of @f@.

To achieve similar reasoning in the coverage checker, we keep track of the set
of values that can reach a particular program point (often loosely referred to
as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas'.
We fill that set with Covered Nablas returned by the exported checking
functions, which the call sites put into place with
'GHC.HsToCore.Monad.updPmNablas'.
Call sites also extend this set with facts from type-constraint dictionaries,
case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
and 'addHsScrutTmCs'.

Note [Recovering from unsatisfiable pattern-matching constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following code (see #12957 and #15450):

  f :: Int ~ Bool => ()
  f = case True of { False -> () }

We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
used not to do this; in fact, it would warn that the match was /redundant/!
This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
coverage checker deems any matches with unsatisfiable constraint sets to be
unreachable.

We make sure to always start from an inhabited 'Nablas' by calling
'getLdiNablas', which falls back to the trivially inhabited 'Nablas' if the
long-distance info returned by 'GHC.HsToCore.Monad.getPmNablas' is empty.
-}