Skip to content

PmCheck: Implement Long-distance information with Covered sets

Sebastian Graf requested to merge wip/pmcheck-ldi into master

Consider

data T = A | B | C

f :: T -> Int
f A = 1
f x = case x of
  A -> 2
  B -> 3
  C -> 4

Clearly, the RHS returning 2 is redundant. But we don't currently see that, because our approximation to the covered set of the inner case expression just picks up the positive information from surrounding pattern matches. It lacks the context sensivity that x can't be A anymore!

Therefore, we adopt the conceptually and practically superior approach of reusing the covered set of a particular GRHS from an outer pattern match. In this case, we begin checking the case expression with the covered set of fs second clause, which encodes the information that x can't be A anymore. After this MR, we will successfully warn about the RHS returning 2 being redundant.

Perhaps surprisingly, this was a great simplification to the code of both the coverage checker and the desugarer.

Edited by Sebastian Graf

Merge request reports