Count binders, not variables #360
Conversation
If we have `where for<'a> T: Foo<'a>`, that should generate `for<'a> FromEnv(T: Foo<'a>)` in the environment.
If we are counting binding levels, then this is important to keep the debruijn indices from getting out of whack. In other words, `for ^1.0` is very different from `^1.0`.
The new convention is: * `shift_in` and `shifted_in` assume one level * `shifted_in_by(N)` to shift by N levels `shift_out` is analogous but it also always returns `Option` instead of having an assert.
This is more strongly typed. In the process, rename `shifted_in_by/shifted_out_by` to * `shifted_in_from(D)` -- i.e., we are shifting a value from the binder D into this one * `shifted_out_to(D)` -- i.e., we are shifting a value from this binder into the binder D I at least find those names give me a better intuition for what's going on in most cases. i.e., we are taking a term that was valid from some outer binder D and shifting it *in* to the inner binder.
To some extent it falls out from the approach of counting binders -- it would be possible to remove the binder, but it takes more work. The way the code is now, you never consider at all how many variables appear in a binder, which makes things a bit simpler: you're generally shifting by constant amounts (i.e., by one binding level) and not some variable number of locations. This also tends to be a bit less error-prone: this is why I uncovered a few oversights where we weren't adjusting indices. Since those binders tended to be empty, in the older system those oversights slipped through without being noticed. To see what I mean, consider the term In contrast, the But under the new system, we would represent If we find that there is some sort of efficiency cost, we could consider doing it, although I think there shouldn't really be any cost. We could probably (when solving goals) just notice the "irrelevant" binder and skip over it without doing any folding (but instead just incrementing some counter). |
This explanation helped me a lot, thanks. These changes LGTM with the minor nits and stuff. Name change comments and such are up to your discretion. |
The big change here is counting binders, not variables (rust-lang/chalk#360). We have to adapt to the same scheme for our `Ty::Bound`. It's mostly fine though, even makes some things more clear.
The big change here is counting binders, not variables (rust-lang/chalk#360). We have to adapt to the same scheme for our `Ty::Bound`. It's mostly fine though, even makes some things more clear.
This branch modifies our notion of "bound variable" so that we count binders and not variables. This aligns more closely with how rustc does things.
Side note that along the way, I encountered at least one semi-serious (and pre-existing) problem with the setup of the implied bounds. I left a FIXME but we should open a follow-up issue on the topic.
Side note that I would dearly love to refactor the wf/coherence code that creates goals to introduce a
GoalBuilder, somewhat analogous to theClauseBuilder. The existing logic requires some very "careful coding" in that it makes extensive use of "copying and pasting" where-clauses and types from one context to another -- you can do this is you are very careful with how you setup your binders, but it's fragile and confusing.