Fix exhaustiveness checking for union types

[xxdavid]

I've looked into issue #477 and traced the issue down to add_type_pat_union/3 . If I understand it correctly, the add_type_pat function computes which parts of type Ty are covered by pattern Pat. add_type_union is a special case when Ty is a union type.

It computes add_type_pat on all "parts of the union" and when one pattern matches more than one "part of the union", it computes the GLB of them. But I think this is not the correct behaviour.

Imagine the following code

case E of
	P1 -> B1
	P2 -> B2
	...
	PN -> BN
end

where E is of type T = (T1 | T2 | … | TM). If for example P1 covers both T1 and T2, add_type_pat_union(T, P1) outputs GLB(T1, T2) . But it does not make much sense to me. It covers both of them, so I think it should be the lowest upper bound (i.e., union) of them instead.

In the example mentioned in #477, add_type_pat_union({error, foo} | {error, bar}, {error, _Sth}) returns GLB({error, foo}. {error, bar}) which is none(). But it should rather be {error, foo} | {error, bar}.

I've fixed it, and apart from the example (test/should_pass/exhaustiveness_union_types.erl ) now passing, three other things happened.

First, this workaround for

ebin/typechecker.beam: Nonexhaustive patterns on line 2172 at column 9
Example values which are not covered:
        {false, {true, #constraints{}}}

is no longer needed.

Second, this false positive is gone as well:

test/known_problems/should_pass/intersection.erl: Nonexhaustive patterns on line 21 at column 1
Example values which are not covered:
        {a, b}

I've moved intersection.erl into test/should_pass/intersection.erl, but it does not satisfy tests either because Gradualizer still outputs

test/should_pass/intersection.erl: None of the types of the function h on line 5 at column 9 matches the call site. Here's the types of the function:
fun((a) -> a)
fun((b) -> b)
test/should_pass/intersection.erl: The type of the functionh, called on line 9 at column 9 doesn't match the surrounding calling context.
It has the following type
fun((a) -> a)
fun((b) -> b)

What should we do in this case? Maybe we can put part of the file into known_problems/should_pass and part into should_pass?

Third, gradualizingtest/should_fail/tuple_union_arg.erl no longer reports an error. However, this is tricky. Until now, it reported

test/known_problems/should_fail/tuple_union_arg.erl: Nonexhaustive patterns on line 12 at column 1
Example values which are not covered:
        {d, b}

and this is the same false positive we've already seen. It should fail with a different error (something like that i cannot be called with d, b and neither with a, e). I've moved it into known problems.

[erszcz]

This is amazing! 🚀
I remember stumbling upon this part of code, but being quite deep down the rabbit hole I didn't want to tinker with one more knob.

If for example P1 covers both T1 and T2, add_type_pat_union(T, P1) outputs GLB(T1, T2) . But it does not make much sense to me. It covers both of them, so I think it should be the lowest upper bound (i.e., union) of them instead.

👍

What should we do in this case? Maybe we can put part of the file into known_problems/should_pass and part into should_pass?

Definitely. I usually split such files and put one with a _should_pass suffix under test/known_problems/should_pass and one with a _pass suffix under test/should_pass. Analogically for _should_fail / _fail.

Great job!

[erszcz]

Thanks again, @xxdavid!

[xxdavid]

Thanks for extracting the tests, I wouldn't get to that until weekend. Happy to see it merged. :)