Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 :: [CoreExpr] -> [Id] -> DsM a -> DsM a
- addHsScrutTmCs :: [LHsExpr GhcTc] -> [Id] -> DsM a -> DsM a
- getLdiNablas :: DsM Nablas
Documentation
pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM () Source #
Check a pattern binding (let, where) for exhaustiveness.
:: 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 function assumes it
checks an -XEmptyCase
with only a single match variable.
See Note [Checking EmptyCase].
:: 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 :: [CoreExpr] -> [Id] -> DsM a -> DsM a Source #
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.
addHsScrutTmCs :: [LHsExpr GhcTc] -> [Id] -> DsM a -> DsM a Source #
addCoreScrutTmCs
, but desugars the LHsExpr
s first.