Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Checking multi-clause functions against overloaded specs #183

Closed
gomoripeti opened this issue Apr 17, 2019 · 5 comments · Fixed by #486
Closed

Checking multi-clause functions against overloaded specs #183

gomoripeti opened this issue Apr 17, 2019 · 5 comments · Fixed by #486

Comments

@gomoripeti
Copy link
Collaborator

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

@zuiderkwast
Copy link
Collaborator

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

@zuiderkwast
Copy link
Collaborator

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
Copy link
Collaborator

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

@zuiderkwast
Copy link
Collaborator

Solved by #461 @erszcz?

@erszcz
Copy link
Collaborator

erszcz commented Nov 18, 2022

It seems so, indeed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
3 participants