-
Notifications
You must be signed in to change notification settings - Fork 183
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Generalize program clause for AliasEq
goal with nested alias
#792
Generalize program clause for AliasEq
goal with nested alias
#792
Conversation
019e12e
to
db746e0
Compare
@bors r+ |
🔒 Merge conflict This pull request and the master branch diverged in a way that cannot be automatically merged. Please rebase on top of the latest master branch, and let the reviewer approve again. How do I rebase?Assuming
You may also read Git Rebasing to Resolve Conflicts by Drew Blessing for a short tutorial. Please avoid the "Resolve conflicts" button on GitHub. It uses Sometimes step 4 will complete without asking for resolution. This is usually due to difference between how Error message
|
☔ The latest upstream changes (presumably #780) made this pull request unmergeable. Please resolve the merge conflicts. |
db746e0
to
91c24e3
Compare
@bors r+ |
☀️ Test successful - checks-actions |
Consider a goal:
AliasEq(<<?0 as X>::A as Y>::B = <<?1 as X>::A as Y>::B)
. This is expected to (eventually) flounder when the traits are non-enumerable and the variables are yet to be known, but it's currently disproven:forall<T, U> AliasEq(<<T as X>::A as Y>::B = <<U as X>::A as Y>::B)
ProgramClause
that could match:forall<T, U, ..> AliasEq(<<T as X>::A as Y>::B = <<U as X>::A as Y>::B) :- AliasEq(..), AliasEq(..)
AliasEq(<<?0 as X>::A as Y>::B = <<?1 as X>::A as Y>::B)
AliasEq
, we see twoAliasTy
s that we cannot unify structurally, forcing us to produce the subgoalThe problem is that because we're reusing the original goal as the consequence of the program clause we expect them to unify structurally, however we cannot unify aliases structurally in general (e.g.
<?0 as X>::A = <?1 as X>::A
does not imply?0 = ?1
).This PR solves it by placing a fresh variable in rhs of the consequence
AliasEq
instead of reusing the original term. This ensures that rhs of the originalAliasEq
goal is preserved via unification without producing subgoals even if it's an alias.See rust-lang/rust-analyzer#14369 for a real world case where this issue arises.