Skip to content

coherence doesn't permit negative impls to take advantage of implied bounds #93875

Closed
@nikomatsakis

Description

@nikomatsakis

#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.F-negative_impls#![feature(negative_impls)]

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions