GHC.HsToCore.Pmc

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:

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.

Documentation

pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM Nablas

Check a pattern binding (let, where) for exhaustiveness.

pmcMatches

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 Nablas per Match and GRHS, for long distance info.

Check a list of syntactic Matches (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 Matches 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].

pmcGRHSs

Arguments

:: HsMatchContext GhcTc

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

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

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

isMatchContextPmChecked_SinglePat :: DynFlags -> Origin -> HsMatchContext id -> LPat GhcTc -> Bool

Check whether exhaustivity checks are enabled for this HsMatchContext, when dealing with a single pattern (using the matchSinglePatVar function).

addTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a

Add in-scope type constraints if the coverage checker might run and then run the given action.

addCoreScrutTmCs :: [CoreExpr] -> [Id] -> DsM a -> DsM a

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

addCoreScrutTmCs, but desugars the LHsExprs first.

getLdiNablas :: DsM Nablas

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