-
Notifications
You must be signed in to change notification settings - Fork 13.6k
apply_member_constraints
: fix placeholder check
#142071
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
base: master
Are you sure you want to change the base?
Conversation
@rfcbot fcp merge |
Team member @lcnr has proposed to merge this. The next step is review by the rest of the tagged team members: No concerns currently listed. Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up! See this document for info about what commands tagged team members can give me. |
// This was unnecessary. It is totally acceptable for member regions | ||
// to be able to name placeholders from higher universes, as long as | ||
// they don't actually do so. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This comment is weird: "It is totally acceptable ... as long as they don't actually do so"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
"to be able to" vs "to do"
As in: it's fine for the member region to be an existential region created in a higher universe, as long as it doesn't actually name any placeholder from that higher universe.
How would you restructure this comment? Is the following clearer?
It is totally acceptable for member regions to be able to name placeholders from higher universes, as long as they don't actually refer to a placeholder.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it's fine for the member region to be an existential region created in a higher universe, as long as it doesn't actually name any placeholder from that higher universe.
This is the most clear
🔔 This is now entering its final comment period, as per the review above. 🔔 |
@rfcbot reviewed That example is pretty mind-binding -- the key thing that took me a while to understand was that the universal variable created by proving |
//@ check-pass | ||
|
||
// Unlike `non-root-universe-existential-1.rs` this previously | ||
// compiled as it simnply didn't define the hidden type of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
// compiled as it simnply didn't define the hidden type of | |
// compiled as it simply didn't define the hidden type of |
Checking whether the member region is an existential region from a higher universe is just wrong and I am pretty sure we've added that check by accident as the naming was just horribly confusing before #140466.
I've encountered this issue separately while working on #139587, but feel like it's probably easier to separately FCP this change. This allows the following code to compile
This should not be breaking change, even in theory. Applying member constraints is incomplete in rare circumstances which means that applying them in more cases can cause spurious errors, cc #140569/#142073. However, as we always skipped these member regions in
apply_member_constraints
the skipped region is guaranteed to cause an error incheck_member_constraints
later on.