Gradualizer icon indicating copy to clipboard operation
Gradualizer copied to clipboard

Checking multi-clause functions against overloaded specs

Open gomoripeti opened this issue 5 years ago • 3 comments

(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:

  1. first ignoring unreachable clause/no pattern match errors
  2. 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.

gomoripeti avatar Apr 17 '19 08:04 gomoripeti

I ran in to this problem today and added a known problem test case in beb5a775dab61813febb90d73800efe43ca8ea54

zuiderkwast avatar Jan 15 '20 17:01 zuiderkwast

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.

zuiderkwast avatar Jan 15 '20 22:01 zuiderkwast

I reverted my commit. There is already a test case for this in test/known_problems/should_pass/intersection.erl.

zuiderkwast avatar Jan 16 '20 08:01 zuiderkwast

Solved by #461 @erszcz?

zuiderkwast avatar Nov 18 '22 09:11 zuiderkwast

It seems so, indeed.

erszcz avatar Nov 18 '22 15:11 erszcz