HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Moduleghc-9.10.3GHC2021

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.

  • 11 values
  • Packageghc-9.10.3
  • Exports11
  • LanguageGHC2021
  • LicenceBSD-3-Clause
  • SourcePmc.hs
valuepmcMatches
  1. :: Origin
  2. -> DsMatchContext

    Match context, for warnings messages

  3. -> [Id]

    Match variables, i.e. x and y above

  4. -> [LMatch GhcTc (LHsExpr GhcTc)]

    List of matches

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

valueaddTyCs :: Origin -> Bag EvVar -> DsM a -> DsM a
#

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

valueaddCoreScrutTmCs :: [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.

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