Tracking Issue for coinductive_overlap_in_coherence lint

[compiler-errors]

This is the summary issue for the coinductive_overlap_in_coherence future-compatibility warning. The goal of this page is describe why this change was made and how you can fix code that is affected by it. It also provides a place to ask questions or register a complaint if you feel the change should not be made. For more information on the policy around future-compatibility warnings, see our breaking change policy guidelines.

What is a inductive cycle, why does it affect coherence?

Rust currently treats trait cycles as errors in the current trait solver. That is, if an impl requires some trait predicate to hold in order to prove that same trait predicate, then we know that it would require solving to depth infinity, and we can cut out the unnecessary work and conclude the predicate must never hold. This is called an inductive cycle.

For example:

trait A {}
impl<T> A for T where T: B {}

trait B {}
impl<T> B for T where T: A {}

fn needs_a<T: A>() {}

fn main() {
    needs_a::<i32>();
}

In order to prove that i32: A, we must prove that i32: B. However, to prove that i32: B, we must show that i32: A, completing the inductive cycle.

During coherence, when a where clause is known to error, we can use it to conclude that two impls do not overlap. We consider two impls to not overlap if unifying their impl headers results in a where-clause of one of the impls to not hold.

For example:

use std::cmp::Ordering;
use std::marker::PhantomData;

#[derive(PartialEq, Default)]
pub(crate) struct Interval<T>(PhantomData<T>);

impl<T, Q> PartialEq<Q> for Interval<T>
where
    Q: PartialOrd,
{
    fn eq(&self, _: &Q) -> bool { todo!() }
}

impl<T, Q> PartialOrd<Q> for Interval<T>
where
    Q: PartialOrd,
{
    fn partial_cmp(&self, _: &Q) -> Option<Ordering> { todo!() }
}

When trying to show that the derive PartialEq and the manual impl don't overlap, we infer that Q = Interval<T>. Then we want to show that Interval<T>: PartialOrd, which is satisfied by the second impl. That then requires that Interval<T>: PartialOrd, leading to an inductive cycle, and we can conclude that the two impls may never overlap.

Why is this a problem?

In the new trait solver (#107374), we currently treat inductive cycles as ambiguity -- we may not assume they never hold, but we don't know that they certainly hold (due to the infinite depth required to prove it). This is to leave room for eventually migrating to coinductive solving, which is allowed to use the fact that we're proving a trait predicate to prove itself, breaking infinite predicate cycles. Unfortunately, this does mean that during coherence, we may no longer be able to prove that two impls overlap.

Tracking

• Initial implementation: Warn on inductive cycle in coherence leading to impls being considered not overlapping #114023
• Bump lint to deny: Bump COINDUCTIVE_OVERLAP_IN_COHERENCE to deny + warn in deps #116493
• Make it a hard error

[lcnr]

has been changed to a hard error in #118649