Closed
Description
#93652 implemented the "negative coherence" rules, but it left one part undone. When we try to prove T: !Trait
for some trait, we ought to include in the environment the "wf" bounds for the input types on the impl; the current logic does not. As a result, tests like src/test/ui/coherence/coherence-negative-outlives-lifetimes.rs
do not compile:
trait MyPredicate<'a> {}
impl<'a, T> !MyPredicate<'a> for &T where T: 'a {}
trait MyTrait<'a> {}
impl<'a, T: MyPredicate<'a>> MyTrait<'a> for T {}
impl<'a, T> MyTrait<'a> for &'a T {}
Here, for MyTrait
to be legal, we would have to be able to prove that T: !MyPredicate<'a>
. There is a negative impl, but it requires that T: 'a
, which we are not able to prove. However, we ought to be able to, because the impl in question is for &'a T
, and that includes a WF bound that T: 'a
.
cc @spastorino