7

Don't require intercrate mode for negative coherence by compiler-errors · Pull R...

 9 months ago
source link: https://github.com/rust-lang/rust/pull/117992
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

Conversation

Negative coherence needs to be sound, but does not need to be complete, since it's looking for the existence of a negative goal, not the non-existence of a positive goal.

This removes some trivial and annoying ambiguities when a negative impl has region constraints.

r? lcnr idk if this needs an fcp but if it does, pls kick it off

rustbot

added S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.

labels

Nov 16, 2023

compiler-errors

added T-types Relevant to the types team, which will review and decide on the PR/issue.

and removed T-compiler Relevant to the compiler team, which will review and decide on the PR/issue.

labels

Nov 16, 2023

Contributor

don't believe this to require an FCP

@bors r+ rollup

Contributor

📌 Commit ae62ebe has been approved by lcnr

It is now in the queue for this repository.

bors

added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion.

and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties.

labels

Nov 17, 2023

Member

This pull request may have caused this error.

#118041 (comment)

Member

Author

@TaKO8Ki: Also, in the future, please use @bors r- so it doesn't end up in another rollup.
TaKO8Ki reacted with thumbs up emoji

bors

added S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author.

and removed S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion.

labels

Nov 18, 2023

Member

Author

Gonna re-approve this one first

@bors r=lcnr

Contributor

📌 Commit ae62ebe has been approved by lcnr

It is now in the queue for this repository.

bors

added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion.

and removed S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author.

labels

Nov 18, 2023

Comment on lines

400 to 404

// N.B. We don't need to use intercrate mode here because we're trying to prove

// the *existence* of a negative goal, not the non-existence of a positive goal.

// Without this, we over-eagerly register coherence ambiguity candidates when

// impl candidates do exist.

let ref infcx = tcx.infer_ctxt().with_next_trait_solver(true).build();

I believe the intercrate mode must be enabled when equating impl headers in order to not over constrain the common type (e.g. disallow equating alias substs). It can then, and only then, be safely disabled in try_prove_negated_where_clause.

I think this is only a theoretical unsoundness for now because we currently ignore the obligations of equate_impl_headers and because infcx.eq does not have intercrate-specfic behavior (in the new solver mode that is. for the old solver, there is this).

Yeah, that makes sense. I can leave a comment clarifying that next to the line where we currently throw away these obligations.

can't we just disable it in try_prove_negated_where_clause? the fact that we rely on infcx.eq to not have intercrate-specific behavior is a bit scary.

I don't think we have facilities to set the intercrate mode currently, but I guess I could add it to fork, probably the best way to do it.

aliemjay reacted with thumbs up emoji

Member

Author

@bors r- so i dont forget to leave this comment

bors

added S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author.

and removed S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion.

labels

Nov 19, 2023

Member

@aliemjay aliemjay

left a comment

Looks good now. You can r=me unless you want lcnr to review.

Member

Author

Yeah, I'll r=lcnr,aliemjay once #117994 lands. Just fixed up some comments.

Member

Author

19a5e1d is necessary for soundness. We emit region requirements when plugging region inference vars with placeholders, which are necessary to keep around, otherwise code like this passes:

#![feature(negative_impls)]
#![feature(with_negative_coherence)]

trait Foo {}
impl<T> !Foo for &'static T {}

trait Bar {}
impl<T> Bar for T where T: Foo {}
impl<T> Bar for &T {}

@bors r=lcnr,aliemjay

Contributor

📌 Commit 253f502 has been approved by lcnr,aliemjay

It is now in the queue for this repository.

bors

added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion.

and removed S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author.

labels

Nov 20, 2023

bors

merged commit 0270afe into

rust-lang:master

Nov 21, 2023

11 checks passed

rust-timer

added a commit to rust-lang-ci/rust that referenced this pull request

Nov 21, 2023

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Back to tour

aliemjay

aliemjay approved these changes
Assignees

lcnr

Labels
S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. T-types Relevant to the types team, which will review and decide on the PR/issue.
Projects

None yet

Milestone

1.76.0

Development

Successfully merging this pull request may close these issues.

None yet

6 participants

report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK