Skip to content

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information