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.