#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
#93652 implemented the "negative coherence" rules, but it left one part undone. When we try to prove
T: !Traitfor 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 likesrc/test/ui/coherence/coherence-negative-outlives-lifetimes.rsdo not compile:Here, for
MyTraitto be legal, we would have to be able to prove thatT: !MyPredicate<'a>. There is a negative impl, but it requires thatT: '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 thatT: 'a.cc @spastorino