Don't drop region constraints that come from plugging infer regions with placeholders

This commit is contained in:
Michael Goulet 2023-11-20 18:39:44 +00:00
parent 46ecc10c69
commit 19a5e1dfc6
4 changed files with 13 additions and 9 deletions

View File

@ -415,13 +415,6 @@ 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.
@ -429,6 +422,13 @@ fn impl_intersection_has_negative_obligation(
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))
}

View File

@ -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))]

View File

@ -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

View File

@ -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