Case with same var exhaustiveness

[FrankBro]

-module(test2).

-spec test1(integer()) -> integer() | zero.
test1(0) -> zero;
test1(I) -> I.

-spec test2(integer()) -> integer() | zero.
test2(I) ->
    case I of
        0 -> zero;
        I -> I
    end.

I would say both are equivalent but the second fail with this

Nonexhaustive patterns on line 10 at column 9
Example values which are not covered: [-1]

Probably need a special case for matching on the same variable, which would always be true.

[zuiderkwast]

The difference is in the pattern-matching. In the case example, the variable in the pattern in the 2nd case clause is already bound.

The function clause example (test1) is equivalent (typechecker-implementation wise) to a case with a new, free variable, e.g.

test2(I) ->
    case I of
        0 -> zero;
        J -> J
    end.

[FrankBro]

But should it work? I know this is a work around, I've used similar in the past like this #290

-spec nth3([integer()]) -> integer().
nth3(Xs) ->
    case Xs of
        [] -> 0;
        _ -> lists:nth(1, Xs)
    end.

because we would refine the Xs arg to be [integer(), ...]

[zuiderkwast]

Isn't it the same as https://github.com/josefs/Gradualizer/blob/master/test/known_problems/should_pass/refine_bound_var_on_mismatch.erl#L10 ?

-spec refined_var_not_matching_itself(x | y | z) -> ok.
refined_var_not_matching_itself(Var) ->
    case Var of
        x   -> ok;
        Var -> ok
    end.

The comment on the line above is wrong though. The actual error you get is

Nonexhaustive patterns on line 13 at column 9 Example values which are not covered: [y]

[FrankBro]

Ah I think you are right. It might tackle both of my open PRs then. Will try to compare output and close if needed.

[erszcz]

I'll close this PR since there's been no activity here for a while. Please let me know if we should reopen it.