Rollup merge of #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

Author: matthiaskrgr

compiler/rustc_infer/src/infer/at.rs

@@ -65,8 +65,15 @@ impl<'tcx> InferCtxt<'tcx> {
 
     /// Forks the inference context, creating a new inference context with the same inference
     /// variables in the same state. This can be used to "branch off" many tests from the same
-    /// common state. Used in coherence.
+    /// common state.
     pub fn fork(&self) -> Self {
+        self.fork_with_intercrate(self.intercrate)
+    }
+
+    /// Forks the inference context, creating a new inference context with the same inference
+    /// variables in the same state, except possibly changing the intercrate mode. This can be
+    /// used to "branch off" many tests from the same common state. Used in negative coherence.
+    pub fn fork_with_intercrate(&self, intercrate: bool) -> Self {
         Self {
             tcx: self.tcx,
             defining_use_anchor: self.defining_use_anchor,
@@ -81,7 +88,7 @@ impl<'tcx> InferCtxt<'tcx> {
             tainted_by_errors: self.tainted_by_errors.clone(),
             err_count_on_creation: self.err_count_on_creation,
             universe: self.universe.clone(),
-            intercrate: self.intercrate,
+            intercrate,
             next_trait_solver: self.next_trait_solver,
         }
     }

compiler/rustc_trait_selection/src/traits/coherence.rs

@@ -397,6 +397,8 @@ fn impl_intersection_has_negative_obligation(
 ) -> bool {
     debug!("negative_impl(impl1_def_id={:?}, impl2_def_id={:?})", impl1_def_id, impl2_def_id);
 
+    // N.B. We need to unify impl headers *with* intercrate mode, even if proving negative predicates
+    // do not need intercrate mode enabled.
     let ref infcx = tcx.infer_ctxt().intercrate(true).with_next_trait_solver(true).build();
     let root_universe = infcx.universe();
     assert_eq!(root_universe, ty::UniverseIndex::ROOT);
@@ -415,20 +417,20 @@ fn impl_intersection_has_negative_obligation(
         return false;
     };
 
-    plug_infer_with_placeholders(
-        infcx,
-        root_universe,
-        (impl1_header.impl_args, impl2_header.impl_args),
-    );
-    let param_env = infcx.resolve_vars_if_possible(param_env);
-
     // FIXME(with_negative_coherence): the infcx has constraints from equating
     // the impl headers. We should use these constraints as assumptions, not as
     // requirements, when proving the negated where clauses below.
     drop(equate_obligations);
     drop(infcx.take_registered_region_obligations());
     drop(infcx.take_and_reset_region_constraints());
 
+    plug_infer_with_placeholders(
+        infcx,
+        root_universe,
+        (impl1_header.impl_args, impl2_header.impl_args),
+    );
+    let param_env = infcx.resolve_vars_if_possible(param_env);
+
     util::elaborate(tcx, tcx.predicates_of(impl2_def_id).instantiate(tcx, impl2_header.impl_args))
         .any(|(clause, _)| try_prove_negated_where_clause(infcx, clause, param_env))
 }
@@ -554,7 +556,11 @@ fn try_prove_negated_where_clause<'tcx>(
         return false;
     };
 
-    let ref infcx = root_infcx.fork();
+    // 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 = root_infcx.fork_with_intercrate(false);
     let ocx = ObligationCtxt::new(infcx);
 
     ocx.register_obligation(Obligation::new(

tests/ui/coherence/coherence-negative-outlives-lifetimes.rs

@@ -1,5 +1,9 @@
 // revisions: stock with_negative_coherence
+
 //[with_negative_coherence] known-bug: unknown
+// Ideally this would work, but we don't use `&'a T` to imply that `T: 'a`
+// which is required for `&'a T: !MyPredicate` to hold. This is similar to the
+// test `negative-coherence-placeholder-region-constraints-on-unification.explicit.stderr`
 
 #![feature(negative_impls)]
 #![cfg_attr(with_negative_coherence, feature(with_negative_coherence))]

tests/ui/coherence/coherence-negative-outlives-lifetimes.stock.stderr

@@ -1,5 +1,5 @@
 error[E0119]: conflicting implementations of trait `MyTrait<'_>` for type `&_`
-  --> $DIR/coherence-negative-outlives-lifetimes.rs:14:1
+  --> $DIR/coherence-negative-outlives-lifetimes.rs:18:1
    |
 LL | impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {}
    | ---------------------------------------------- first implementation here

tests/ui/coherence/coherence-negative-outlives-lifetimes.with_negative_coherence.stderr

@@ -1,5 +1,5 @@
 error[E0119]: conflicting implementations of trait `MyTrait<'_>` for type `&_`
-  --> $DIR/coherence-negative-outlives-lifetimes.rs:14:1
+  --> $DIR/coherence-negative-outlives-lifetimes.rs:18:1
    |
 LL | impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {}
    | ---------------------------------------------- first implementation here

tests/ui/coherence/coherence-overlap-with-regions.rs

@@ -1,10 +1,4 @@
-// known-bug: unknown
-
-// This fails because we currently perform negative coherence in coherence mode.
-// This means that when looking for a negative predicate, we also assemble a
-// coherence-unknowable predicate. Since confirming the negative impl has region
-// obligations, we don't prefer the impl over the unknowable predicate
-// unconditionally and instead flounder.
+// check-pass
 
 #![feature(negative_impls)]
 #![feature(rustc_attrs)]

tests/ui/coherence/coherence-overlap-with-regions.stderr

@@ -1,5 +1,5 @@
 error[E0119]: conflicting implementations of trait `Bar` for type `&_`
-  --> $DIR/negative-coherence-considering-regions.rs:22:1
+  --> $DIR/negative-coherence-considering-regions.rs:16:1
    |
 LL | impl<T> Bar for T where T: Foo {}
    | ------------------------------ first implementation here

tests/ui/coherence/negative-coherence-considering-regions.any_lt.stderr

@@ -1,11 +1,5 @@
 // revisions: any_lt static_lt
-//[static_lt] known-bug: unknown
-
-// This fails because we currently perform negative coherence in coherence mode.
-// This means that when looking for a negative predicate, we also assemble a
-// coherence-unknowable predicate. Since confirming the negative impl has region
-// obligations, we don't prefer the impl over the unknowable predicate
-// unconditionally and instead flounder.
+//[static_lt] check-pass
 
 #![feature(negative_impls)]
 #![feature(with_negative_coherence)]