Safe Haskell | None |
---|---|
Language | Haskell2010 |
GHC.HsToCore.Pmc
Description
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"
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
:
- Desugar source syntax (like
LMatch
) to guard tree variants (likeGrdMatch
), with one of the desugaring functions (likedesugarMatch
). See GHC.HsToCore.Pmc.Desugar. Follows Section 3.1 in the paper. - Coverage check guard trees (with a function like
checkMatch
) to get aCheckResult
. See GHC.HsToCore.Pmc.Check. The normalised refinement typesNabla
are tested for inhabitants by GHC.HsToCore.Pmc.Solver. - Collect redundancy information into a
CIRB
with a function such ascirbsMatch
. Follows the R function from Figure 6 of the paper. - Format and report uncovered patterns and redundant equations (
CIRB
) withformatReportWarnings
. Basically job of the G function, plus proper pretty printing of the warnings (Section 5.4 of the paper). - Return
Nablas
reaching syntactic sub-components for Note [Long-distance information]. Collected by functions such asldiMatch
. See Section 4.1 of the paper.
Synopsis
- pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM ()
- pmcMatches :: DsMatchContext -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM [(Nablas, NonEmpty Nablas)]
- pmcGRHSs :: HsMatchContext GhcRn -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM (NonEmpty Nablas)
- isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool
- addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
- addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a
- addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a
Documentation
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM () Source #
Check a pattern binding (let, where) for exhaustiveness.
Arguments
:: 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 |
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].
Arguments
:: HsMatchContext GhcRn | Match context, for warning messages |
-> GRHSs GhcTc (LHsExpr GhcTc) | The GRHSs to check |
-> DsM (NonEmpty Nablas) | Covered |
Exhaustive for guard matches, is used for guards in pattern bindings and
in MultiIf
expressions. Returns the Nablas
covered by the RHSs.
isMatchContextPmChecked :: DynFlags -> Origin -> HsMatchContext id -> Bool Source #
Check whether any part of pattern match checking is enabled for this
HsMatchContext
(does not matter whether it is the redundancy check or the
exhaustiveness check).
addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a Source #
Add in-scope type constraints if the coverage checker might run and then run the given action.
addCoreScrutTmCs :: Maybe CoreExpr -> [Id] -> DsM a -> DsM a Source #
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.
addHsScrutTmCs :: Maybe (LHsExpr GhcTc) -> [Id] -> DsM a -> DsM a Source #
addCoreScrutTmCs
, but desugars the LHsExpr
first.