Open
Description
our current plan to soundly support coinductive traits is to require proving the item bounds of a trait when using an implementation. Afaict this should break the following example:
trait WithSuper<T>: Copy {}
trait WithAliasBound {
type Assoc: Copy;
}
// With our approach to coinduction, using this impl should require
// proving `<T as WithAliasBound>::Assoc: Copy`
impl<T: WithAliasBound> WithSuper<T> for <T as WithAliasBound>::Assoc {}
fn impls_with_super<T: WithSuper<U>, U>() {}
fn item_bounds_not_checked<T: WithAliasBound<Assoc = U>, U>() {
impls_with_super::<U, T>();
// This uses the impl and would fail to prove `U: Copy`.
}