Bring `AnnotatedTree` structure in line with Lower Your Guards
Currently, we check Deltas for inhabitants before generating annotated trees:
data AnnotatedTree
= ...
| MayDiverge !AnnotatedTree
-- ^ Asserts that the tree may force diverging values, so not all of its
-- clauses can be redundant.
| ...
checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
...
-- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
checkGrdTree' (Guard (PmBang x) tree) deltas = do
has_diverged <- addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
deltas' <- addPmCtDeltas deltas (PmNotBotCt x)
res <- checkGrdTree' tree deltas'
pure res{ cr_clauses = applyWhen has_diverged MayDiverge (cr_clauses res) }
...
In Lower Your Guards, we found that it's more elegant to postpone all isInhabited checks to generation of warnings, what is currently redunantAndInaccessibleRhss. That would correspond to the following AnnotatedTree/checkGrdTree' impl:
data AnnotatedTree
= ...
| Banged !Deltas !AnnotatedTree
| ...
checkGrdTree' :: GrdTree -> Deltas -> DsM CheckResult
...
-- Bang x: Diverge on x ~ ⊥, refine with x /~ ⊥
checkGrdTree' (Guard (PmBang x) tree) deltas = do
has_diverged <- addPmCtDeltas deltas (PmBotCt x) >>= isInhabited
deltas' <- addPmCtDeltas deltas (PmNotBotCt x)
res <- checkGrdTree' tree deltas'
pure res{ cr_clauses = applyWhen has_diverged MayDiverge (cr_clauses res) }
...
Banged ds t matches like t, but must be "kept alive" (may not be deleted) if ds is inhabited, even if t doesn't match anything. In other words: If ds is inhabited, there must be at least one RHS of t that is not redundant. (See the paper.)
Similarly for what is currently InaccessibleRhs/AccessibleRhs; keep RhsAnn !Deltas !RhsInfo instead and postpone the isInhabited check.