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

-- | 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, pmcRecSel,
        isMatchContextPmChecked, isMatchContextPmChecked_SinglePat,

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

import GHC.Prelude

import GHC.HsToCore.Errors.Types
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.Types.Basic (Origin(..), isDoExpansionGenerated)
import GHC.Core
import GHC.Driver.DynFlags
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, Var (..))
import GHC.Types.Id.Info
import GHC.Tc.Utils.TcType (evVarPred)
import {-# SOURCE #-} GHC.HsToCore.Expr (dsLExpr)
import GHC.HsToCore.Monad
import GHC.Data.Bag
import GHC.Data.OrdList

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

--
-- * 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 <- DsM Nablas
getPmNablas
  isInhabited nablas >>= \case
    Bool
True  -> Nablas -> DsM Nablas
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nablas
nablas
    Bool
False -> Nablas -> DsM Nablas
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
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 :: forall a. DsM a -> DsM a
noCheckDs = (DynFlags -> DynFlags)
-> TcRnIf DsGblEnv DsLclEnv a -> TcRnIf DsGblEnv DsLclEnv a
forall gbl lcl a.
(DynFlags -> DynFlags) -> TcRnIf gbl lcl a -> TcRnIf gbl lcl a
updTopFlags (\DynFlags
dflags -> (DynFlags -> WarningFlag -> DynFlags)
-> DynFlags -> [WarningFlag] -> DynFlags
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' DynFlags -> WarningFlag -> DynFlags
wopt_unset DynFlags
dflags [WarningFlag]
allPmCheckWarnings)

-- | Check a pattern binding (let, where) for exhaustiveness.
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM Nablas
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM Nablas
pmcPatBind ctxt :: DsMatchContext
ctxt@(DsMatchContext HsMatchContextRn
match_ctxt SrcSpan
loc) Id
var Pat GhcTc
p
  = DsM Nablas -> DsM Nablas
mb_discard_warnings (DsM Nablas -> DsM Nablas) -> DsM Nablas -> DsM Nablas
forall a b. (a -> b) -> a -> b
$ do
      !missing <- DsM Nablas
getLdiNablas
      pat_bind <- noCheckDs $ desugarPatBind loc var p
      tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
      result <- unCA (checkPatBind pat_bind) missing
      let ldi = PmGRHS Post -> Nablas
ldiGRHS (PmGRHS Post -> Nablas) -> PmGRHS Post -> Nablas
forall a b. (a -> b) -> a -> b
$ ( \ PmPatBind Post
pb -> case PmPatBind Post
pb of PmPatBind PmGRHS Post
grhs -> PmGRHS Post
grhs) (PmPatBind Post -> PmGRHS Post) -> PmPatBind Post -> PmGRHS Post
forall a b. (a -> b) -> a -> b
$ CheckResult (PmPatBind Post) -> PmPatBind Post
forall a. CheckResult a -> a
cr_ret CheckResult (PmPatBind Post)
result
      tracePm "pmcPatBind }: " $
        vcat [ text "cr_uncov:" <+> ppr (cr_uncov result)
             , text "ldi:" <+> ppr ldi ]
      formatReportWarnings ReportPatBind ctxt [var] result
      return ldi
  where
    -- See Note [pmcPatBind doesn't warn on pattern guards]
    mb_discard_warnings :: DsM Nablas -> DsM Nablas
mb_discard_warnings
      = if HsMatchContext (GenLocated SrcSpanAnnN Name) -> Bool
forall {fn}. HsMatchContext fn -> Bool
want_pmc HsMatchContextRn
HsMatchContext (GenLocated SrcSpanAnnN Name)
match_ctxt
        then DsM Nablas -> DsM Nablas
forall a. a -> a
id
        else DsM Nablas -> DsM Nablas
forall a. DsM a -> DsM a
discardWarningsDs
    want_pmc :: HsMatchContext fn -> Bool
want_pmc HsMatchContext fn
PatBindRhs = Bool
True
    want_pmc HsMatchContext fn
LazyPatCtx = Bool
True
    want_pmc (StmtCtxt HsStmtContext fn
stmt_ctxt) =
      case HsStmtContext fn
stmt_ctxt of
        PatGuard {} -> Bool
False
        HsStmtContext fn
_           -> Bool
True
    want_pmc HsMatchContext fn
_ = Bool
False

-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions. Returns the 'Nablas' covered by the RHSs.
pmcGRHSs
  :: HsMatchContextRn             -- ^ 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 :: HsMatchContextRn
-> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty Nablas)
pmcGRHSs HsMatchContextRn
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 a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SrcSpan -> SrcSpan -> SrcSpan
combineSrcSpans ((GenLocated
   EpAnnCO (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
 -> SrcSpan)
-> [GenLocated
      EpAnnCO (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
-> [SrcSpan]
forall a b. (a -> b) -> [a] -> [b]
map GenLocated
  EpAnnCO (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))
-> SrcSpan
forall a e. HasLoc a => GenLocated a e -> SrcSpan
getLocA [LGRHS GhcTc (LHsExpr GhcTc)]
[GenLocated
   EpAnnCO (GRHS GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc)))]
grhss)
      ctxt :: DsMatchContext
ctxt = HsMatchContextRn -> SrcSpan -> DsMatchContext
DsMatchContext HsMatchContextRn
hs_ctxt SrcSpan
combined_loc
  !missing <- DsM Nablas
getLdiNablas
  matches  <- noCheckDs $ desugarGRHSs combined_loc empty guards
  tracePm "pmcGRHSs" (hang (vcat [ppr ctxt
                                , text "Guards:"])
                                2
                                (pprGRHSs hs_ctxt guards $$ ppr missing))
  result <- unCA (checkGRHSs matches) missing
  tracePm "}: " (ppr (cr_uncov result))
  formatReportWarnings ReportGRHSs ctxt [] result
  return (ldiGRHSs (cr_ret 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 function assumes it
-- checks an @-XEmptyCase@ with only a single match variable.
-- See Note [Checking EmptyCase].
pmcMatches
  :: Origin
  -> 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 :: Origin
-> DsMatchContext
-> [Id]
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM [(Nablas, NonEmpty Nablas)]
pmcMatches Origin
origin DsMatchContext
ctxt [Id]
vars [LMatch GhcTc (LHsExpr GhcTc)]
matches = {-# SCC "pmcMatches" #-} 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!
  !missing <- DsM Nablas
getLdiNablas
  tracePm "pmcMatches {" $
          hang (vcat [ppr origin, ppr ctxt, ppr vars, text "Matches:"])
               2
               ((ppr matches) $$ (text "missing:" <+> ppr missing))
  case NE.nonEmpty 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
      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
      result <- unCA (checkEmptyCase empty_case) missing
      tracePm "}: " (ppr (cr_uncov result))
      formatReportWarnings ReportEmptyCase ctxt vars result
      return []
    Just NonEmpty
  (GenLocated
     SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc))))
matches -> do
      matches <- {-# SCC "desugarMatches" #-}
                 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 (LMatch GhcTc (LHsExpr GhcTc))
NonEmpty
  (GenLocated
     SrcSpanAnnA (Match GhcTc (GenLocated SrcSpanAnnA (HsExpr GhcTc))))
matches
      tracePm "desugared matches" (ppr matches)
      result  <- {-# SCC "checkMatchGroup" #-}
                 unCA (checkMatchGroup matches) missing
      tracePm "}: " (ppr (cr_uncov result))
      unless (isDoExpansionGenerated origin) -- Do expansion generated code shouldn't emit overlapping warnings
        ({-# SCC "formatReportWarnings" #-}
        formatReportWarnings ReportMatchGroup ctxt vars result)
      return (NE.toList (ldiMatchGroup (cr_ret result)))

{-
Note [Detecting incomplete record selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This Note describes the implementation of
GHC proposal 516 "Add warning for incomplete record selectors".

A **partial field** is a field that does not belong to every constructor of the
corresponding datatype.
A **partial selector occurrence** is a use of a record selector for a partial
field, either as a selector function in an expression, or as the solution to a
HasField constraint.

Partial selector occurrences desugar to case expressions which may crash at
runtime:

  data T a where
    T1 :: T Int
    T2 {sel :: Int} :: T Bool

  urgh :: T a -> Int
  urgh x = sel x
  ===>
  urgh x = case x of
    T1 -> error "no record field sel"
    T2 f -> f

As such, it makes sense to warn about such potential crashes.
We do so whenever -Wincomplete-record-selectors is present, and we utilise
the pattern-match coverage checker for precise results, because there are many
uses of selectors for partial fields which are in fact dynamically safe.

Pmc can detect two very common safe uses for which we will not warn:

 (LDI) Ambient pattern-matches unleash Note [Long-distance information] that
       render a naively flagged partial selector occurrence safe, as in
         ldi :: T a -> Int
         ldi T1  = 0
         ldi arg = sel arg
       We should not warn here, because `arg` cannot be `T1`.

 (RES) Constraining the result type of a GADT such as T might render
       naively flagged partial selector occurrences safe, as in
         resTy :: T Bool -> Int
         resTy = sel
       Here, `T1 :: T Int` is ruled out because it has the wrong result type.

Additionally, we want to support incomplete -XOverloadedRecordDot access as
well, in either the (LDI) use case or the (RES) use case:

  data Dot = No | Yes { sel2 :: Int }
  dot d = d.sel2      -- should warn
  ldiDot No = 0
  ldiDot d  = d.sel2  -- should not warn
  resTyDot :: T Bool -> Int
  resTyDot x = x.sel  -- should not warn

From a user's point of view, function `ldiDot` looks very like example `ldi` and
`resTyDot` looks very like `resTy`. But from an /implementation/ point of view
they are very different: both `ldiDot` and `resTyDot` simply emit `HasField`
constraints, and it is those constraints that the implementation must use to
determine incompleteness.

Furthermore, HasField constraints allow to delay the completeness check from
the field access site to a caller, as in test cases TcIncompleteRecSel and T24891:

  accessDot :: HasField "sel2" t Int => t -> Int
  accessDot x = x.sel2   -- getField @Symbol @"sel2" @t @Int x
  solveDot :: Dot -> Int
  solveDot = accessDot

We should warn in `solveDot`, but not in `accessDot`.

Here is how we achieve all this in the implementation:

(IRS1) When renaming a record selector in `mkOneRecordSelector`,
    we precompute the constructors the selector succeeds on.
    That would be `T2` for `sel` because `sel (T2 42)` succeeds,
    and `Yes` for `sel2` because `sel2 (Yes 13)` succeeds.
    We store this information in the `sel_cons` field of `RecSelId`.
    (Remember, the same field may occur in several constructors of the data
    type; hence the selector may succeed on more than one constructor.)

We generate warnings for incomplete record selectors in two places:
* Mainly: in GHC.HsToCore.Expr.ds_app (see (IRS2-5) below)
* Plus: in GHC.Tc.Instance.Class.matchHassField (see (IRS6-7) below)

(IRS2) In function `ldi`, we have a record selector application `sel arg`.
    This situation is detected `GHC.HsToCore.Expr.ds_app_rec_sel`, when the
    record selector is applied to at least one argument. We call out to the
    pattern-match checker to determine whether use of the selector is safe,
    by calling GHC.HsToCore.Pmc.pmcRecSel, passing the `RecSelId` `sel` as
    well as `arg`.

    The pattern-match checker reduces the partial-selector-occurrence problem to
    a complete-match problem by adding a negative constructor constraint such as
    `arg /~ T2` for every constructor in the precomputed `rsi_def . sel_cons` of
    `sel`. (Recall that these were exactly the constructors which define a field
    `sel`.) `pmcRecSel` then tests
      case arg of {}
    for completeness. Any incomplete match, such as in the original `urgh`, must
    reference a constructor that does not have field `sel`, such as `T1`.

    In case of `urgh`, `T1` is indeed the case that we report as inexhaustive.

    However, in function `ldi`, we have *both* the result type of
    `arg::T a` (boring, but see (IRS3)) as well as Note [Long-distance information]
    about `arg` from the ambient match, and the latter lists the constraint
    `arg /~ T1`. Consequently, since `arg` is neither `T1` nor `T2` in the
    reduced problem, the match is exhaustive and the use of the record selector
    safe.

(IRS3) In function `resTy`, the record selector is unsaturated, but the result type
    ensures a safe use of the selector.

    This situation is also detected in `GHC.HsToCore.Expr.ds_app_rec_sel`.
    THe selector is elaborated with its type arguments; we simply match on
    desugared Core `sel @Bool :: T Bool -> Int` to learn the result type `T Bool`.
    We again call `pmcRecSel`, but this time with a fresh dummy Id `ds::T Bool`.

(IRS4) In case of an unsaturated record selector that is *not* applied to any type
  argument after elaboration (e.g. in `urgh2 = sel2 :: Dot -> Int`), we simply
  produce a warning about all `sel_cons`; no need to call `pmcRecSel`.
  This happens in `ds_app_rec_sel`

Finally, there are two more items addressing -XOverloadedRecordDot:

(IRS5) With -XOverloadedDot, all occurrences of (r.x), such as in `ldiDot` and
  `accessDot` above, are warned about as follows.  `r.x` is parsed as
  `HsGetField` in `HsExpr`; which is then expanded (in `rnExpr`) to a call to
  `getField`.  For example, consider:
         ldiDot No = 0
         ldiDot x  = x.sel2  -- should not warn
  The `d.sel2` in the RHS generates
      getField @GHC.Types.Symbol @"sel2" @Dot @Int
               ($dHasField :: HasField "sel2" Dot Int) x
  where
      $dHasField = sel2 |> (co :: Dot -> Int ~R# HasField "sel2" Dot Int)
  We spot this `getField` application in `GHC.HsToCore.Expr.ds_app_var`,
  and treat it exactly like (IRS2) and (IRS3).

  Note carefully that doing this in the desugarer allows us to account for the
  long-distance info about `x`; even though `sel2` is partial, we don't want
  to warn about `x.sel2` in this example.

(IRS6) Finally we have
          solveDot :: Dot -> Int
          solveDot = accessDot
  No field-accesses or selectors in sight!  From the RHS we get the constraint
      [W] HasField @"sel2" @Dot @Int`
  The only time we can generate a warning is when we solve this constraint,
  in `GHC.Tc.Instance.Class.matchHasField`, generating a call to the (partial)
  selector.  We have no hope of exploiting long-distance info here.

(IRS7) BUT, look back at `ldiDot`.  Doesn't `matchHasField` /also/ generate a
  warning for the `HasField` constraint arising from `x.sel2`?  We don't
  want that, because the desugarer will catch it: see (IRS5).  So we suppress
  the (IRS6) warning in the typechecker for a `HasField` constraint that
  arises from a record-dot HsGetField occurrence.  Happily, this is easy to do
  by looking at its `CtOrigin`. Tested in T24891.
-}

pmcRecSel :: Id       -- ^ Id of the selector
          -> CoreExpr -- ^ Core expression of the argument to the selector
          -> DsM ()
-- See (IRS2,3) in Note [Detecting incomplete record selectors]
pmcRecSel :: Id -> CoreExpr -> DsM ()
pmcRecSel Id
sel_id CoreExpr
arg
  | RecSelId{ sel_cons :: IdDetails -> RecSelInfo
sel_cons = RecSelInfo
rec_sel_info } <- Id -> IdDetails
idDetails Id
sel_id
  , RSI { rsi_def :: RecSelInfo -> [ConLike]
rsi_def = [ConLike]
cons_w_field, rsi_undef :: RecSelInfo -> [ConLike]
rsi_undef = [ConLike]
cons_wo_field } <- RecSelInfo
rec_sel_info
  , Bool -> Bool
not ([ConLike] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConLike]
cons_wo_field)
  = do { !missing <- DsM Nablas
getLdiNablas

       ; tracePm "pmcRecSel {" (ppr sel_id)
       ; CheckResult{ cr_ret = PmRecSel{ pr_arg_var = arg_id }, cr_uncov = uncov_nablas }
           <- unCA (checkRecSel (PmRecSel () arg cons_w_field)) missing
       ; tracePm "}: " $ ppr uncov_nablas

       ; inhabited <- isInhabited uncov_nablas
       ; when inhabited $ warn_incomplete arg_id uncov_nablas }

  | Bool
otherwise
  = () -> DsM ()
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  where
     sel_name :: Name
sel_name = Id -> Name
varName Id
sel_id
     warn_incomplete :: Id -> Nablas -> DsM ()
warn_incomplete Id
arg_id Nablas
uncov_nablas = do
       dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       let maxPatterns = DynFlags -> Int
maxUncoveredPatterns DynFlags
dflags
       unc_examples <- getNFirstUncovered MinimalCover [arg_id] (maxPatterns + 1) uncov_nablas
       let cons = [ConLike
con | Nabla
unc_example <- [Nabla]
unc_examples
                 , Just (PACA (PmAltConLike ConLike
con) [Id]
_ [Id]
_) <- [Nabla -> Id -> Maybe PmAltConApp
lookupSolution Nabla
unc_example Id
arg_id]]
       tracePm "unc-ex" (ppr cons $$ ppr unc_examples)
       diagnosticDs $ DsIncompleteRecordSelector sel_name cons maxPatterns


{- Note [pmcPatBind doesn't warn on pattern guards]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@pmcPatBind@'s main 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 report pattern match warnings
for these pattern guards:

  * 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.

However, we should not skip pattern-match checking altogether, as it may reveal
important long-distance information. One example is described in
Note [Long-distance information in do notation] in GHC.HsToCore.Expr.

Instead, we simply discard warnings when in pattern-guards, by using the function
discardWarningsDs.
-}

--
-- * 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 = unitOL r, cirb_red = 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 = cirb_bangs cirb Semi.<> 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
  is_covered  <- Nablas -> DsM Bool
isInhabited Nablas
cov
  may_diverge <- isInhabited div
  red_bangs   <- flip mapMaybeM (fromOL bangs) $ \(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 a b.
IOEnv (Env DsGblEnv DsLclEnv) a
-> (a -> IOEnv (Env DsGblEnv DsLclEnv) b)
-> IOEnv (Env DsGblEnv DsLclEnv) b
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 a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
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 a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SrcInfo -> Maybe SrcInfo
forall a. a -> Maybe a
Just SrcInfo
bang)
  pure (is_covered, may_diverge, toOL 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty 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
  (_is_covered, may_diverge, 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 <- cirbsGRHSs grhss
  pure $ addRedundantBangs red_bangs
       -- See Note [Determining inaccessible clauses]
       $ applyWhen may_diverge ensureOneNotRedundant
       $ 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty 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
  (is_covered, may_diverge, red_bangs) <- Post -> DsM (Bool, Bool, OrdList SrcInfo)
testRedSets Post
red
  let cirb | Bool
is_covered  = CIRB
forall a. Monoid a => a
mempty { cirb_cov   = unitOL info }
           | Bool
may_diverge = CIRB
forall a. Monoid a => a
mempty { cirb_inacc = unitOL info }
           | Bool
otherwise   = CIRB
forall a. Monoid a => a
mempty { cirb_red   = unitOL info }
  pure (addRedundantBangs red_bangs cirb)

cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
cirbsEmptyCase :: PmEmptyCase -> DsM CIRB
cirbsEmptyCase PmEmptyCase
_ = CIRB -> DsM CIRB
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
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
forall a b. Coercible a b => a -> b
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
--

-- | A datatype to accommodate the different call sites of
-- 'formatReportWarnings'. Used for extracting 'CIRB's from a concrete 'ann'
-- through 'collectInMode'. Since this is only possible for a couple of
-- well-known 'ann's, this is a GADT.
data FormatReportWarningsMode ann where
  ReportPatBind :: FormatReportWarningsMode (PmPatBind Post)
  ReportGRHSs   :: FormatReportWarningsMode (PmGRHSs Post)
  ReportMatchGroup:: FormatReportWarningsMode (PmMatchGroup Post)
  ReportEmptyCase:: FormatReportWarningsMode PmEmptyCase

deriving instance Eq (FormatReportWarningsMode ann)

-- | A function collecting 'CIRB's for each of the different
-- 'FormatReportWarningsMode's.
collectInMode :: FormatReportWarningsMode ann -> ann -> DsM CIRB
collectInMode :: forall ann. FormatReportWarningsMode ann -> ann -> DsM CIRB
collectInMode FormatReportWarningsMode ann
ReportPatBind    = ann -> DsM CIRB
PmPatBind Post -> DsM CIRB
cirbsPatBind
collectInMode FormatReportWarningsMode ann
ReportGRHSs      = ann -> DsM CIRB
PmGRHSs Post -> DsM CIRB
cirbsGRHSs
collectInMode FormatReportWarningsMode ann
ReportMatchGroup = ann -> DsM CIRB
PmMatchGroup Post -> DsM CIRB
cirbsMatchGroup
collectInMode FormatReportWarningsMode ann
ReportEmptyCase  = ann -> DsM CIRB
PmEmptyCase -> DsM CIRB
cirbsEmptyCase

-- | Given a 'FormatReportWarningsMode', this function will emit warnings
-- for a 'CheckResult'.
formatReportWarnings :: FormatReportWarningsMode ann -> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings :: forall ann.
FormatReportWarningsMode ann
-> DsMatchContext -> [Id] -> CheckResult ann -> DsM ()
formatReportWarnings FormatReportWarningsMode ann
report_mode DsMatchContext
ctx [Id]
vars cr :: CheckResult ann
cr@CheckResult { cr_ret :: forall a. CheckResult a -> a
cr_ret = ann
ann } = do
  cov_info <- FormatReportWarningsMode ann -> ann -> DsM CIRB
forall ann. FormatReportWarningsMode ann -> ann -> DsM CIRB
collectInMode FormatReportWarningsMode ann
report_mode ann
ann
  dflags <- getDynFlags
  reportWarnings dflags report_mode ctx vars cr{cr_ret=cov_info}

-- | Issue all the warnings
-- (redundancy, inaccessibility, exhaustiveness, redundant bangs).
reportWarnings :: DynFlags -> FormatReportWarningsMode ann -> DsMatchContext -> [Id] -> CheckResult CIRB -> DsM ()
reportWarnings :: forall ann.
DynFlags
-> FormatReportWarningsMode ann
-> DsMatchContext
-> [Id]
-> CheckResult CIRB
-> DsM ()
reportWarnings DynFlags
dflags FormatReportWarningsMode ann
report_mode (DsMatchContext HsMatchContextRn
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
      unc_examples <- GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered GenerateInhabitingPatternsMode
gen_mode [Id]
vars (Int
maxPatterns Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Nablas
uncovered
      let 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
flag_i Bool -> Bool -> Bool
&& OrdList SrcInfo -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull OrdList SrcInfo
inaccessible_rhss
          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
flag_b Bool -> Bool -> Bool
&& OrdList SrcInfo -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull OrdList SrcInfo
redundant_bangs
          approx   = Precision
precision Precision -> Precision -> Bool
forall a. Eq a => a -> a -> Bool
== Precision
Approximate

      when (approx && (exists_u || exists_i)) $
        putSrcSpanDs loc (diagnosticDs (DsMaxPmCheckModelsReached (maxPmCheckModels dflags)))

      when exists_b $ forM_ redundant_bangs $ \(SrcInfo (L SrcSpan
l SDoc
q)) ->
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (DsMessage -> DsM ()
diagnosticDs (HsMatchContextRn -> SDoc -> DsMessage
DsRedundantBangPatterns HsMatchContextRn
kind SDoc
q))

      when exists_r $ forM_ redundant_rhss $ \(SrcInfo (L SrcSpan
l SDoc
q)) ->
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (DsMessage -> DsM ()
diagnosticDs (HsMatchContextRn -> SDoc -> DsMessage
DsOverlappingPatterns HsMatchContextRn
kind SDoc
q))
      when exists_i $ forM_ inaccessible_rhss $ \(SrcInfo (L SrcSpan
l SDoc
q)) ->
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (DsMessage -> DsM ()
diagnosticDs (HsMatchContextRn -> SDoc -> DsMessage
DsInaccessibleRhs HsMatchContextRn
kind SDoc
q))

      when exists_u $
        putSrcSpanDs loc (diagnosticDs (DsNonExhaustivePatterns kind check_type maxPatterns vars unc_examples))
  where
    flag_i :: Bool
flag_i = DynFlags -> HsMatchContext (GenLocated SrcSpanAnnN Name) -> Bool
forall fn. DynFlags -> HsMatchContext fn -> Bool
overlapping DynFlags
dflags HsMatchContextRn
HsMatchContext (GenLocated SrcSpanAnnN Name)
kind
    flag_u :: Bool
flag_u = DynFlags -> HsMatchContext (GenLocated SrcSpanAnnN Name) -> Bool
forall fn. DynFlags -> HsMatchContext fn -> Bool
exhaustive DynFlags
dflags HsMatchContextRn
HsMatchContext (GenLocated SrcSpanAnnN Name)
kind
    flag_b :: Bool
flag_b = DynFlags -> Bool
redundantBang DynFlags
dflags
    check_type :: ExhaustivityCheckType
check_type = Maybe WarningFlag -> ExhaustivityCheckType
ExhaustivityCheckType (HsMatchContext (GenLocated SrcSpanAnnN Name) -> Maybe WarningFlag
forall fn. HsMatchContext fn -> Maybe WarningFlag
exhaustiveWarningFlag HsMatchContextRn
HsMatchContext (GenLocated SrcSpanAnnN Name)
kind)
    gen_mode :: GenerateInhabitingPatternsMode
gen_mode = case FormatReportWarningsMode ann
report_mode of -- See Note [Case split inhabiting patterns]
      FormatReportWarningsMode ann
ReportEmptyCase -> GenerateInhabitingPatternsMode
CaseSplitTopLevel
      FormatReportWarningsMode ann
_               -> GenerateInhabitingPatternsMode
MinimalCover

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

getNFirstUncovered :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered :: GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nablas -> DsM [Nabla]
getNFirstUncovered GenerateInhabitingPatternsMode
mode [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 a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go Int
_ []             = [Nabla] -> DsM [Nabla]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go Int
n (Nabla
nabla:[Nabla]
nablas) = do
      front <- GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode [Id]
vars Int
n Nabla
nabla
      back <- go (n - length front) nablas
      pure (front ++ back)

--
-- * 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 :: DsM a -> (Nablas -> DsM Nablas) -> DsM a
locallyExtendPmNablas :: forall a. DsM a -> (Nablas -> DsM Nablas) -> DsM a
locallyExtendPmNablas DsM a
k Nablas -> DsM Nablas
ext = do
  nablas <- DsM Nablas
getLdiNablas
  nablas' <- unsafeInterleaveM $ ext nablas
  updPmNablas nablas' 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 :: forall a. Origin -> Bag Id -> DsM a -> DsM a
addTyCs Origin
origin Bag Id
ev_vars DsM a
thing_inside
  | Bag Id -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Id
ev_vars
  = DsM a
thing_inside  -- Very common fast path
  | Bool
otherwise
  = do { dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; if needToRunPmCheck dflags origin
         then locallyExtendPmNablas thing_inside $ \Nablas
nablas ->
              Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas (PredType -> PhiCt
PhiTyCt (PredType -> PhiCt) -> (Id -> PredType) -> Id -> PhiCt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> PredType
evVarPred (Id -> PhiCt) -> Bag Id -> PhiCts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bag Id
ev_vars)
         else thing_inside }

-- | Add equalities for the 'CoreExpr' scrutinees to the local 'DsM' environment,
-- e.g. 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.
-- This is also used for the Arrows \cases command, where these equalities have
-- to be added for multiple scrutinees rather than just one.
addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs :: forall a. [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs []         [Id]
_      DsM a
k = DsM a
k
addCoreScrutTmCs (CoreExpr
scr:[CoreExpr]
scrs) (Id
x:[Id]
xs) DsM a
k
  = DsM a -> (Nablas -> DsM Nablas) -> DsM a
forall a. DsM a -> (Nablas -> DsM Nablas) -> DsM a
locallyExtendPmNablas ([CoreExpr] -> [Id] -> DsM a -> DsM a
forall a. [CoreExpr] -> [Id] -> DsM a -> DsM a
addCoreScrutTmCs [CoreExpr]
scrs [Id]
xs 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 [CoreExpr]
_   [Id]
_   DsM a
_ = String -> DsM a
forall a. HasCallStack => String -> a
panic String
"addCoreScrutTmCs: numbers of scrutinees and match ids differ"

-- | 'addCoreScrutTmCs', but desugars the 'LHsExpr's first.
addHsScrutTmCs :: [LHsExpr GhcTc] -> [Id] -> DsM a -> DsM a
addHsScrutTmCs :: forall a. [LHsExpr GhcTc] -> [Id] -> DsM a -> DsM a
addHsScrutTmCs [LHsExpr GhcTc]
scrs [Id]
vars DsM a
k = do
  scr_es <- (GenLocated SrcSpanAnnA (HsExpr GhcTc)
 -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr)
-> [GenLocated SrcSpanAnnA (HsExpr GhcTc)]
-> IOEnv (Env DsGblEnv DsLclEnv) [CoreExpr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse LHsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
GenLocated SrcSpanAnnA (HsExpr GhcTc)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsLExpr [LHsExpr GhcTc]
[GenLocated SrcSpanAnnA (HsExpr GhcTc)]
scrs
  addCoreScrutTmCs scr_es vars 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.
-}