Description
Right now, we have this hokey thing where it walks the tree at the end, but sometimes (to help with inference) does resolution eagerly, and it's all a big mess. Besides being hard to understand and inefficient, this also means that inference often fails where it could succeed. An example is the overloading example I gave in my blog post, where the result type often fails to be inferred (at least according to some folk on IRC, I haven't experimented much with this myself, so I don't have a precise test case).
I want to have it work something like this:
- There is a list in the fn_ctxt of pending type-trait pairs that need to be resolved
- We add new pairs to this list as we do our type check, assigning each pair an index.
- We can then create a mapping from the expr.id and probably some other stuff to this index so we can uncover the result in trans, this is tied up a bit in Make
a.b()
always a method call, refactor how methods are represented in the compiler #3446
- We can then create a mapping from the expr.id and probably some other stuff to this index so we can uncover the result in trans, this is tied up a bit in Make
- When we add a new pair to the list, we can try to eagerly resolve it at that time, which helps with type inference
- Actually, we are free to try and resolve whenever we like, so we can even wait to try and resolve when we encounter types whose structure is not known but needs to be
- At the end, we walk the list and make sure all pairs are resolvable
These pairs more-or-less correspond to Haskell's type contexts. "Eager resolution" is context simplification. The only reason it's reasonable to use pairs is if we decide to enforce overload freedom, as I described in my blog post.
Also, to ensure termination, it may be necessary to add a depth to these pairs, unless we decide to enforce something like Haskell's Paterson or Basic conditions (which I am not sure how I feel about).