Gradualizer
Gradualizer copied to clipboard
Checking multi-clause functions against overloaded specs
(thanks for @tim2CF for reporting this issue. This is a very common problem in Elixir where using any protocol generates code that is affected)
example:
-spec num(1) -> one;
(2) -> two.
num(1) -> one;
num(2) -> two.
Currently the function is checked against each part of the intersection spec one by one and fails with an error "The [second] clause cannot be reached" because 1
in the first clause completely covers the arg type 1
. If it wouldn't stop here it would also fail while checking the first clause against the second part of the spec: "The pattern 1 cannot match the arg type of 2"
My first naive approach to fix this was to check the function two times:
- first ignoring unreachable clause/no pattern match errors
- second checking only unreachability against some union type in the arguments
(1 | 2) -> any()
The union is a bit problematic (overestimates) in case of multiple args
(a, b) -> ok; (c, d) -> ok
=> (a | c, b | d) -> any()
What should be the algorithm?
Ideally it could be something like instead of `for each spec element check the whole function" do "for each clause check it against the whole spec" and refining the argstype of every spec. If all the RefinedArgsTypes become none, a clause is only then unreachable.
I ran in to this problem today and added a known problem test case in beb5a775dab61813febb90d73800efe43ca8ea54
Sorry for the commit message and the filename mentioning "exhaustiveness", which the issue is not about. Unreachable clauses is similar though, in a way. I'll rename the file one day soon.
I reverted my commit. There is already a test case for this in test/known_problems/should_pass/intersection.erl
.
Solved by #461 @erszcz?
It seems so, indeed.