Replace fallback clauses with projection-equality vs normalization #75
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Not really the ideal solution, but helpful. It'd be nice to record all the data and be able to expand after the fact.
scalexm
reviewed
Jan 19, 2018
src/lower/mod.rs
Outdated
| // we generate the 'fallback' rule: | ||
| // | ||
| // forall<T> { | ||
| // proj <T as Foo>::Assoc = Foo::Assoc<T> |
There was a problem hiding this comment.
I’m not sure why we don’t need a :- T: Foo condition here, especially looking at the reverse rule below
There was a problem hiding this comment.
Good point. Although currently I've hacked out that reverse rule, the comment is out of date, and instead made T: Foo part of the "WF" criteria (which I guess is your answer). Still, it seems like otherwise I suppose we would need that.
nikomatsakis
force-pushed
the
de-fallback
branch
from
b4062a1
to
6a1b63d
Compare
|
OK, @scalexm, I changed the fallback rule as you suggested, which doesn't seem to cause any problems (I didn't think it would). I also wrote comments. I didn't really clean up the history that much, not sure that I care enough to do so. Inclined to merge soon. |
nikomatsakis
force-pushed
the
de-fallback
branch
from
6a1b63d
to
2b2685d
Compare
|
ok, I cleaned it up |
Instead of having "fallback clauses" to handle projection, we now
have `ProjectionEq(<T as Trait>::Bar = U)`, which can be proven
either by normalizing *or* by skolemizing.
This required adjusting how we handle elaboration. That is, we now
"expand" a `T: Trait<Bar = U>` (which is the user syntax for projection
equality) into `T: Trait` as well, which in turn expands into `WF(T:
Trait)`. We do this instead of having a clause like:
> `(T: Trait) :- exists<U> { (T: Trait<Bar = U>) }`
This is because that clause caused issues for the recursive solver; in
particular, `exists<U> { (T: Trait<Bar = U>) }` always resolves to an
ambiguous result, since there is no unique `U`.
This PR adjusts the tests appropriately. Mostly we add normalize and
projection. In a few cases, the SLG solver doesn't work yet; those are
tagged with FIXME (and fixed in a later commit).
nikomatsakis
force-pushed
the
de-fallback
branch
from
2b2685d
to
db6be19
Compare
This is not only more efficient, but it also sidesteps the problems that led to the SLG solver recursing infinitely when unifying goals involving projections. This also uncovers a potential flaw with the truncation operation, in that it does not concern itself with internal binders. For example, we might truncate a type like `for<'a> fn(Vec<&'a u32>)` into `for<'a> fn(?X)`. This is problematic because there is no value of `?X` that could reference `'a`. For now, the SLG solver will panic in this scenario, but probably truncation needs to truncate the binder as well.
nikomatsakis
force-pushed
the
de-fallback
branch
from
db6be19
to
4ddc058
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #74
Before merging, I should do a few things:
AnswerSubstitutorcode