search

hydromatic / morel

Standard ML interpreter, with relational extensions, implemented in Java
Apache License 2.0
291 stars 15 forks source link

Pattern that uses nested type-constructors should not be considered redundant #205

Closed julianhyde closed 7 months ago

julianhyde commented 7 months ago

The pattern

fun f (SOME (SOME i)) = i + 1
  | f (SOME NONE) = 0
  | f NONE = ~1

is currently flagged as redundant when it is not. After SOME i has been seen at depth 1 in the first line, the checker incorrectly believes that SOME at depth 0 in the second line has been covered already.

The fix is to generate different variables for the satisfiability checker: 1.SOME for the first (because it occurs within the type constructor number 1 (0- based)), and SOME for the second.