HIR "Eager Type Inference" / Expectations dev guide page - #2924
HIR "Eager Type Inference" / Expectations dev guide page#2924fallible-algebra wants to merge 9 commits into
Conversation
|
Thanks for the PR. If you have write access, feel free to merge this PR if it does not need reviews. You can request a review using |
|
|
||
| In reality, we perform it (at least) twice: First, at eager evaluation points, and secondly "at the end" when those constraints have been collected. | ||
|
|
||
| `Expectations` are a piece of type inference state we maintain for the cases where we need to eagerly infer the types of expressions rather than leave them to the end. They allow us to "ask questions" of the form "hey, we're expecting this term to have this type, is this true?" |
There was a problem hiding this comment.
i feel like its more of a we can ask "what are we expecting the type of this expression to be?"
|
|
||
| If we didn't do eager type inference we would instead have closures whose types were filled with [inference variables](../appendix/glossary.md#inf-var). | ||
|
|
||
| This would be able to be solved in some situations, but because we do not have Higher-Ranked Inference Variables[^higher-ranked-inference] this would make the higher-ranked bounds for lifetimes that rust can have unusable without more annotation. |
There was a problem hiding this comment.
the other reason we care about this is that if you have fn(?x) -> ?y as your closure signature then you can't do field accesses/method calls/etc on ?x which is a quite common thing to want to do
There was a problem hiding this comment.
I think more generally we want to talk about how inferring higher ranked things is eager, and there are two main places this happens:
- inferring higher ranked closure signatures
- subtyping of higher ranked types
|
|
||
| [Coercions](./coercions.md) can happen in many places. We check to see if a coercion can happen, and if it can we perform the coercion. | ||
|
|
||
| When we successfully find a coercion, we need to eagerly perform type inference/checking on it as future inference will require or benefit from this information to be known ahead of time. |
There was a problem hiding this comment.
I don't really know what this sentence is saying 🤔 it also feels a bit backwards to me because once we've "successfully found a coercion" then we've already done "eager type inference" because finding a coercion is the thing that cares about the current state of inference :3
|
|
||
| When we successfully find a coercion, we need to eagerly perform type inference/checking on it as future inference will require or benefit from this information to be known ahead of time. | ||
|
|
||
| ### Method calls, Fields, and Indexes. |
There was a problem hiding this comment.
structuring this as
- Closures
- Coercions
- Other stuff
feels slightly off to me as I feel like it places too much importance on the expectation vs non expectation distinction between cases of eager type inference
I feel like I would prefer just a flat list of all the places that are eager type inference spots
|
|
||
| #### Methods | ||
|
|
||
| Maybe Not. Maybe just point to [method lookup](./method-lookup.md). |
There was a problem hiding this comment.
definitely want to talk about methods :3
I think for each item (e.g. coercions, closures, fields, etc) here we want to cover:
- Why it is an eager inference spot
- How we handle it being an eager inference spot (we would probably talk about "hey we use expectations" here if we do)
- Why we handle it the way we do
for methods this is probably:
- method lookup is an eager inference spot because we need to look at the type of the receiver to determine what methods exist
- we handle this by erroring if there are inference variables which prevent us from figuring out all the methods we might be able to call
- we could move this into the trait solver but it'd complicate things quite a lot and hasn't really been necessary to do so (so mostly historical reasons).
|
|
||
| ? Method calls engage in Coercion and therefore need to engage in Eager Type Inference. | ||
|
|
||
| #### Fields? |
There was a problem hiding this comment.
definitely want to talk about field accesses :3 its mostly the same reasoning as methods
| Eager evaluation of the type of a term (type inference) is required at some specific points to either make later type inference more consistent or (in the case of higher-ranked bounds / Higher Ranked Lifetime bounds) make it even possible. | ||
|
|
||
| Eager type inference is when we do type inference earlier than we otherwise would. To do this, we bring in Expectations as an additional piece of context. | ||
|
|
There was a problem hiding this comment.
general structural thing I think it would be nice to talk about like "the ways we can handle places that care about the current inference state" and sort of talk abstractly about:
- we can defer it to arbitrary points during type inference (trait solving works like this)
- we can eagerly error on inference variables
- we can defer it to the end of typeck after everything has been inferred (array repeat expr checks do this)
|
|
||
| Eager type inference is when we do type inference earlier than we otherwise would. To do this, we bring in Expectations as an additional piece of context. | ||
|
|
||
| ### Closures and Higher-Ranked Variables |
There was a problem hiding this comment.
i kind of want to add trait solving to the list of "eager inference points" in that they're still part of the general "sometimes we do things which cares about the current inference state" its just that "trait" solving is how we handle that correctly instead of jankily
Page on "Eager Type Inference" / Expectations. Currently deep in drafts.