Coverage checking step of the Lower Your Guards paper.

Coverage check guard trees (like PmMatch Pre) to get a CheckResult, containing

1. The set of uncovered values, cr_uncov
2. And an annotated tree variant (like PmMatch Post) that captures redundancy and inaccessibility information as RedSets annotations

Basically the UA function from Section 5.1, which is an optimised interleaving of U and A from Section 3.2 (Figure 5). The Normalised Refinement Types Nablas are maintained in GHC.HsToCore.Pmc.Solver.