Handle cycles in overlap with negative impls #109673

spastorino · 2023-03-27T19:28:41Z

Fixes #102678

r? @nikomatsakis

Opened this as a way to start reviewing it.

At the very least we have the following pending things:

Properly handle errors on negative impls
If specialize succeeds in insert loop we still want to run negative_impls_hold. I didn't bother to do that because I wanted to first see the code "doing something useful".
The old checks are still running and the idea is that we were going to replace them with this new logic. We still need to remove those checks.

I'd need to check a bit better to, to see if there's more to cover.

compiler/rustc_trait_selection/src/traits/coherence.rs

compiler-errors · 2023-03-27T22:49:29Z

compiler/rustc_trait_selection/src/traits/coherence.rs

+            trait_pred,
+        ))
+        .expect("Overflow should be caught earlier in standard query mode")
+        .must_apply_modulo_regions()


Why use this over predicate_may_hold? Don't we want to treat treat ambiguity as "yes" instead of "no" for coherence purposes?

Sorry if this question is misunderstanding what this PR is trying to do.

The idea if I got everything correct is that we want to check that there's not a negative impl that applies. This is why I wanted to check for a must. But this is one of the things that I have doubts if using must_apply_module_regions is correct here.

This should be may apply modulo regions, not must apply.

compiler-errors · 2023-03-27T22:52:32Z

tests/ui/coherence/coherence-overlap-negative-cycles.stderr

+   | ^^^^^^^^^^^^^^^^^^^^
+   | |
+   | first implementation here
+   | conflicting implementation


Ideally we'd find the impl that satisfies !MyTrait and highlight it -- can we do that with SelectionContext::select? This could be a follow-up I guess..

Yes, diagnostics are not really handled in the PR yet. Is one of the things that are still not complete.

compiler/rustc_trait_selection/src/traits/specialize/specialization_graph.rs

bors · 2023-03-28T16:19:37Z

☔ The latest upstream changes (presumably #108080) made this pull request unmergeable. Please resolve the merge conflicts.

nikomatsakis · 2023-03-30T14:14:20Z

compiler/rustc_trait_selection/src/traits/specialize/specialization_graph.rs

@@ -226,6 +226,22 @@ fn overlap_check_considering_specialization<'tcx>(
        return Ok(OverlapResult::SpecializeAll(replace_children));


Block: early returns

nikomatsakis · 2023-03-30T14:16:08Z

compiler/rustc_trait_selection/src/traits/specialize/specialization_graph.rs

@@ -226,6 +226,22 @@ fn overlap_check_considering_specialization<'tcx>(
        return Ok(OverlapResult::SpecializeAll(replace_children));
    }

+    if overlap_mode.use_negative_impl()


remove this if, but before you do, let's try to figure out why the src/test/ui/traits/negative-impls/pin-unsound-issue-66544-derefmut.rs test gets an error (assuming it does...)

probably because we didn't remove the old coherence logic

nikomatsakis · 2023-03-30T14:22:20Z

compiler/rustc_trait_selection/src/traits/coherence.rs

@@ -120,6 +120,48 @@ pub fn overlapping_impls(
    Some(overlap(selcx, skip_leak_check, impl1_def_id, impl2_def_id, overlap_mode).unwrap())
 }

+/// Given an impl_def_id that "positively" implement a trait, check if the "negative" holds.


s/implement/implements/

nikomatsakis · 2023-03-30T14:25:14Z

compiler/rustc_trait_selection/src/traits/coherence.rs

@@ -120,6 +120,48 @@ pub fn overlapping_impls(
    Some(overlap(selcx, skip_leak_check, impl1_def_id, impl2_def_id, overlap_mode).unwrap())
 }

+/// Given an impl_def_id that "positively" implement a trait, check if the "negative" holds.
+pub fn negative_impl_holds(tcx: TyCtxt<'_>, impl_def_id: DefId, overlap_mode: OverlapMode) -> bool {


s/negative_impl_holds/negative_impl_may_hold/

nikomatsakis · 2023-03-30T14:25:18Z

compiler/rustc_trait_selection/src/traits/coherence.rs

+            trait_pred,
+        ))
+        .expect("Overflow should be caught earlier in standard query mode")
+        .must_apply_modulo_regions()


This should be may apply modulo regions, not must apply.

nikomatsakis · 2023-03-30T14:30:26Z

compiler/rustc_trait_selection/src/traits/coherence.rs

+    )));
+
+    // Ideally we would use param_env(impl_def_id) but that's unsound today.
+    let param_env = ty::ParamEnv::empty();


To do this properly, what we ought to do is get the parameter environment and then apply the infer_substs above. The idea is that for some impl...

impl<A..Z> SomeTrait<T1..Tn> for T0 where WC

we want to test if...

there exists types A..Z such that...

assuming WC is true (ie., with the param env in scope)...

T0: !SomeTrait<T1..Tn>

this would be an error, because that means that for at least some instance of this positive impl, there exists a negative impl.

Problem is: applying infer_substs to param-env will mean that we have inference variables in the environment, and I think our code doesn't like that.

It should be sound to not assume WC is true, because proving A => X is harder than proving X on its own, but I'm worried we may be overly conservative.

inference variables in the param env generally cause issues, especially in the old solver. Don't remember exactly what breaks but iirc @BoxyUwU encountered a bunch of issues recently when she tried it.

I think a bigger issue is that the way candidate_should_be_dropped_in_favor_of handles param env candidates is incomplete. This means that coherence in the old solver with trait goals in the param env is unsound because inference may incorrectly cause another nested goal to fail, resulting in an incorrect error. My current approach for the new solver is to disable this behavior if we're in coherence: #109724

Dylan-DPC · 2023-05-21T08:32:57Z

@spastorino any updates on this?

spastorino · 2023-05-23T21:51:18Z

@rustbot modify labels -S-waiting-on-review +S-waiting-on-author

bors · 2023-07-14T18:01:34Z

☔ The latest upstream changes (presumably #113591) made this pull request unmergeable. Please resolve the merge conflicts.

spastorino · 2023-10-11T08:21:53Z

This can be closed for now.

rustbot assigned nikomatsakis Mar 27, 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 Mar 27, 2023

This comment has been minimized.

Sign in to view

spastorino force-pushed the handle-cycles-in-overlap-with-negative-impls branch from 8262cf6 to 9443847 Compare March 27, 2023 20:37

compiler-errors reviewed Mar 27, 2023

View reviewed changes

compiler/rustc_trait_selection/src/traits/coherence.rs Show resolved Hide resolved

compiler-errors reviewed Mar 27, 2023

View reviewed changes

spastorino added 2 commits March 28, 2023 16:32

Rename Inserted to OverlapResult

ada058d

Extract overlap_check_considering_specialization from insert

408c732

spastorino force-pushed the handle-cycles-in-overlap-with-negative-impls branch from 9443847 to ba78cb9 Compare March 28, 2023 19:52

Fix coinductive coherence overlap checks

45ac61a

spastorino force-pushed the handle-cycles-in-overlap-with-negative-impls branch from ba78cb9 to 45ac61a Compare March 28, 2023 20:25

nikomatsakis reviewed Mar 30, 2023

View reviewed changes

rustbot 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-review Status: Awaiting review from the assignee but also interested parties. labels May 23, 2023

spastorino closed this Oct 11, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Handle cycles in overlap with negative impls #109673

Handle cycles in overlap with negative impls #109673

spastorino commented Mar 27, 2023

This comment has been minimized.

compiler-errors Mar 27, 2023

spastorino Mar 28, 2023

nikomatsakis Mar 30, 2023

compiler-errors Mar 27, 2023

spastorino Mar 28, 2023

bors commented Mar 28, 2023

nikomatsakis Mar 30, 2023

nikomatsakis Mar 30, 2023

nikomatsakis Mar 30, 2023

nikomatsakis Mar 30, 2023

nikomatsakis Mar 30, 2023

nikomatsakis Mar 30, 2023

nikomatsakis Mar 30, 2023

lcnr Mar 31, 2023 •

edited

Loading

Dylan-DPC commented May 21, 2023

spastorino commented May 23, 2023

bors commented Jul 14, 2023

spastorino commented Oct 11, 2023

		@@ -226,6 +226,22 @@ fn overlap_check_considering_specialization<'tcx>(
		return Ok(OverlapResult::SpecializeAll(replace_children));

Handle cycles in overlap with negative impls #109673

Handle cycles in overlap with negative impls #109673

Conversation

spastorino commented Mar 27, 2023

This comment has been minimized.

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bors commented Mar 28, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lcnr Mar 31, 2023 • edited Loading

Choose a reason for hiding this comment

Dylan-DPC commented May 21, 2023

spastorino commented May 23, 2023

bors commented Jul 14, 2023

spastorino commented Oct 11, 2023

lcnr Mar 31, 2023 •

edited

Loading