Skip to content
  • Sebastian Graf's avatar
    PmCheck: Formulate as translation between Clause Trees · 8038cbd9
    Sebastian Graf authored and Marge Bot's avatar Marge Bot committed
    We used to check `GrdVec`s arising from multiple clauses and guards in
    isolation. That resulted in a split between `pmCheck` and
    `pmCheckGuards`, the implementations of which were similar, but subtly
    different in detail. Also the throttling mechanism described in
    `Note [Countering exponential blowup]` ultimately got quite complicated
    because it had to cater for both checking functions.
    
    This patch realises that pattern match checking doesn't just consider
    single guarded RHSs, but that it's always a whole set of clauses, each
    of which can have multiple guarded RHSs in turn. We do so by
    translating a list of `Match`es to a `GrdTree`:
    
    ```haskell
    data GrdTree
      = Rhs !RhsInfo
      | Guard !PmGrd !GrdTree      -- captures lef-to-right  match semantics
      | Sequence !GrdTree !GrdTree -- captures top-to-bottom match semantics
      | Empty                      -- For -XEmptyCase, neutral element of Sequence
    ```
    
    Then we have a function `checkGrdTree` that matches a given `GrdTree`
    against an incoming set of values, represented by `Deltas`:
    
    ```haskell
    checkGrdTree :: GrdTree -> Deltas -> CheckResult
    ...
    ```
    
    Throttling is isolated to the `Sequence` case and becomes as easy as one
    would expect: When the union of uncovered values becomes too big, just
    return the original incoming `Deltas` instead (which is always a
    superset of the union, thus a sound approximation).
    
    The returned `CheckResult` contains two things:
    
    1. The set of values that were not covered by any of the clauses, for
       exhaustivity warnings.
    2. The `AnnotatedTree` that enriches the syntactic structure of the
       input program with divergence and inaccessibility information.
    
    This is `AnnotatedTree`:
    
    ```haskell
    data AnnotatedTree
      = AccessibleRhs !RhsInfo
      | InaccessibleRhs !RhsInfo
      | MayDiverge !AnnotatedTree
      | SequenceAnn !AnnotatedTree !AnnotatedTree
      | EmptyAnn
    ```
    
    Crucially, `MayDiverge` asserts that the tree may force diverging
    values, so not all of its wrapped clauses can be redundant.
    
    While the set of uncovered values can be used to generate the missing
    equations for warning messages, redundant and proper inaccessible
    equations can be extracted from `AnnotatedTree` by
    `redundantAndInaccessibleRhss`.
    
    For this to work properly, the interface to the Oracle had to change.
    There's only `addPmCts` now, which takes a bag of `PmCt`s. There's a
    whole bunch of `PmCt` variants to replace the different oracle functions
    from before.
    
    The new `AnnotatedTree` structure allows for more accurate warning
    reporting (as evidenced by a number of changes spread throughout GHC's
    code base), thus we fix #17465.
    
    Fixes #17646 on the go.
    
    Metric Decrease:
        T11822
        T9233
        PmSeriesS
        haddock.compiler
    8038cbd9