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

[julianhyde]

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.