Use Local Type Inference approach to typecheck polymorphic calls

[xxdavid]

Hi!

After months of working on this, I finally come up with a PR that implements the ideas captured in #553. It behaves in the same way as I described in https://github.com/josefs/Gradualizer/issues/553#issuecomment-1934551242, I only changed the second error message a tiny bit.

The main changes are in the commit b00cadd2. It implements the new approach to typechecking polymorphic calls based on Local Type Inference. I think it is quite straightforward but I already know the algorithm well so I am probably biased. However, it should be at least much simpler than the original constraint solver. I tried to document it in the wiki (together with the rigid type variables), so you may read it as documentation to the code. I'm also writing a thesis about this change, so I will link it to the wiki when it's out, to provide another source of documentation.

The main benefit of this change should be error messages that are understandable even when polymorphism is involved. Only in a few cases, a more complex error message shows up but even then, it should be clear what's going on. I think that if this new approach proves successful, we can even enable --solve_constraints by default in the future.

As a byproduct, all the "shape limitations" of the original constraint solver are gone (this could have been also solved by fixing the constraint generation). A type variable can now be instantiated to both a tuple and an atom without any problems.

Other big changes are in a3029e1a. In this commit, I remove the constraints and clauses for flexible type variables from most of the code. Constraints are now generated and propagated only in functions related to typechecking polymorphic calls and functions related to subtyping. This should make the code simpler and easier to read. It also trivially solves all but one "don't drop the constraints" TODOs because constraints are now combined only in the subtyping functions and in type_check_poly_call/4. (Please do not squash commits when merging the PR as this commit would make the resulting commit unreadable.)

I also fixed some things along the way (fc432f2c, 2323f102, e9a0afa4) and added a lot of tests.

While the new approach is better in some cases (like the minus/1 in poly_fail.erl), it is also weaker in some other cases. I see the biggest limitation in that the type of anonymous functions passed to polymorphic functions is now inferred via type_check_expr/2 and not type_check_expr_in/2 as before, and thus some errors may not be discovered. This can, however, be solved in the future by solving the constraints gathered from all other arguments first and then typechecking the anonymous function using the information from the solved constraints. But I think it is better to have understandable errors than just more of them. Once we have this, let's then focus on inferring the type of anonymous functions passed to polymorphic functions.

[xxdavid]

@zuiderkwast @erszcz I know you're busy, but do you think you'll have time for a code review?

[erszcz]

@xxdavid Sorry for the lack of responsiveness. Life got surprisingly busy the last few months. I can imagine it being quite frustrating given the terrific effort you've put into this work.

That being said, I've just gone through the wiki description - it's excellent! I'll also go over the code of the PR, in the next 1-2 days, and try it out on some examples. Please bear with me.

[xxdavid]

No need to apologize! :) It's a volunteer project after all and I can imagine life getting busy.

Thank you for your kind words and for planning to go over it. I'll stay tuned.

[xxdavid]

Thank you very much for the review! :) I've fixed all the issues and resolved the threads.

Can I merge this pull request now? Or would you also like to take a look, @zuiderkwast?

[erszcz]

I think it's good to merge now 👍

BTW, @xxdavid, it was great to see you in person on Lambda Days!

[xxdavid]

@erszcz Thanks for merging the PR, and it was really nice to see you, too!