-
Notifications
You must be signed in to change notification settings - Fork 14k
Closed
Closed
Copy link
Labels
C-bugCategory: This is a bug.Category: This is a bug.F-negative_impls#![feature(negative_impls)]#![feature(negative_impls)]
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
Metadata
Metadata
Assignees
Labels
C-bugCategory: This is a bug.Category: This is a bug.F-negative_impls#![feature(negative_impls)]#![feature(negative_impls)]