Don't require intercrate mode for negative coherence #117992

compiler-errors · 2023-11-16T22:26:56Z

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

lcnr · 2023-11-17T09:13:05Z

don't believe this to require an FCP

@bors r+ rollup

bors · 2023-11-17T09:13:08Z

📌 Commit ae62ebe has been approved by lcnr

It is now in the queue for this repository.

…lete, r=lcnr Don't require intercrate mode for negative coherence 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

TaKO8Ki · 2023-11-18T19:46:32Z

This pull request may have caused this error.

#118041 (comment)

compiler-errors · 2023-11-18T19:47:45Z

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

compiler-errors · 2023-11-18T19:55:13Z

Gonna re-approve this one first

@bors r=lcnr

bors · 2023-11-18T19:55:15Z

📌 Commit ae62ebe has been approved by lcnr

It is now in the queue for this repository.

aliemjay · 2023-11-19T02:38:07Z

compiler/rustc_trait_selection/src/traits/coherence.rs

+    // 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.

compiler-errors · 2023-11-19T02:41:07Z

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

aliemjay

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

compiler-errors · 2023-11-20T01:31:42Z

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

…ith placeholders

compiler-errors · 2023-11-20T18:53:45Z

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

bors · 2023-11-20T18:53:48Z

📌 Commit 253f502 has been approved by lcnr,aliemjay

It is now in the queue for this repository.

…iaskrgr Rollup of 8 pull requests Successful merges: - rust-lang#117327 (Add documentation for some queries) - rust-lang#117835 (Note about object lifetime defaults in does not live long enough error) - rust-lang#117851 (Uplift `InferConst` to `rustc_type_ir`) - rust-lang#117973 (test: Add test for async-move in 2015 Rust proc macro) - rust-lang#117992 (Don't require intercrate mode for negative coherence) - rust-lang#118010 (Typeck break expr even if break is illegal) - rust-lang#118026 (Don't consider regions in `deref_into_dyn_supertrait` lint) - rust-lang#118089 (intercrate_ambiguity_causes: handle self ty infer + reservation impls) r? `@ghost` `@rustbot` modify labels: rollup

Rollup merge of rust-lang#117992 - compiler-errors:sound-but-not-complete, r=lcnr,aliemjay Don't require intercrate mode for negative coherence 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 assigned lcnr Nov 16, 2023

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

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

matthiaskrgr mentioned this pull request Nov 17, 2023

Rollup of 7 pull requests #118019

Closed

TaKO8Ki mentioned this pull request Nov 18, 2023

Rollup of 8 pull requests #118041

Closed

compiler-errors mentioned this pull request Nov 18, 2023

Rollup of 9 pull requests #118049

Closed

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

compiler-errors mentioned this pull request Nov 18, 2023

Ignore but do not assume region obligations from unifying headers in negative coherence #117994

Merged

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

aliemjay requested changes Nov 19, 2023

View reviewed changes

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

compiler-errors force-pushed the sound-but-not-complete branch from ae62ebe to 348c9c2 Compare November 19, 2023 19:22

aliemjay approved these changes Nov 20, 2023

View reviewed changes

compiler-errors force-pushed the sound-but-not-complete branch from 348c9c2 to 506ec26 Compare November 20, 2023 01:31

compiler-errors added 2 commits November 20, 2023 18:49

Don't drop region constraints that come from plugging infer regions w…

19a5e1d

…ith placeholders

Don't require intercrate mode for negative coherence

253f502

compiler-errors force-pushed the sound-but-not-complete branch from 506ec26 to 253f502 Compare November 20, 2023 18:50

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

matthiaskrgr mentioned this pull request Nov 20, 2023

Rollup of 8 pull requests #118107

Merged

bors merged commit 0270afe into rust-lang:master Nov 21, 2023
11 checks passed

rustbot added this to the 1.76.0 milestone Nov 21, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Don't require intercrate mode for negative coherence #117992

Don't require intercrate mode for negative coherence #117992

compiler-errors commented Nov 16, 2023

lcnr commented Nov 17, 2023

bors commented Nov 17, 2023

TaKO8Ki commented Nov 18, 2023

compiler-errors commented Nov 18, 2023

compiler-errors commented Nov 18, 2023

bors commented Nov 18, 2023

aliemjay Nov 19, 2023

compiler-errors Nov 19, 2023

aliemjay Nov 19, 2023

compiler-errors Nov 19, 2023

compiler-errors commented Nov 19, 2023

aliemjay left a comment

compiler-errors commented Nov 20, 2023 •

edited

Loading

compiler-errors commented Nov 20, 2023

bors commented Nov 20, 2023

Don't require intercrate mode for negative coherence #117992

Don't require intercrate mode for negative coherence #117992

Conversation

compiler-errors commented Nov 16, 2023

lcnr commented Nov 17, 2023

bors commented Nov 17, 2023

TaKO8Ki commented Nov 18, 2023

compiler-errors commented Nov 18, 2023

compiler-errors commented Nov 18, 2023

bors commented Nov 18, 2023

aliemjay Nov 19, 2023

Choose a reason for hiding this comment

compiler-errors Nov 19, 2023

Choose a reason for hiding this comment

aliemjay Nov 19, 2023

Choose a reason for hiding this comment

compiler-errors Nov 19, 2023

Choose a reason for hiding this comment

compiler-errors commented Nov 19, 2023

aliemjay left a comment

Choose a reason for hiding this comment

compiler-errors commented Nov 20, 2023 • edited Loading

compiler-errors commented Nov 20, 2023

bors commented Nov 20, 2023

compiler-errors commented Nov 20, 2023 •

edited

Loading