Description
edit: this issue has been partially fixed in #117088, so any remaining incompleteness (and therefore incorrectly accepted overlap) is a lot harder to trigger. See rust-lang/trait-system-refactor-initiative#8 for a list of known issues with generalization. Keeping this issue open as is to track this, but we should try to write a test which relies on one of the other problems of that issue, now that the problem case 2 has been fixed.
// Using the higher ranked projection hack to prevent us from replacing the projection
// with an inference variable.
trait ToUnit<'a> {
type Unit;
}
struct LocalTy;
impl<'a> ToUnit<'a> for *const LocalTy {
type Unit = ();
}
impl<'a, T: Copy + ?Sized> ToUnit<'a> for *const T {
type Unit = ();
}
trait Overlap<T> {
type Assoc;
}
type Assoc<'a, T> = <*const T as ToUnit<'a>>::Unit;
impl<T> Overlap<T> for T {
type Assoc = usize;
}
impl<T> Overlap<for<'a> fn(&'a (), Assoc<'a, T>)> for T
where
for<'a> *const T: ToUnit<'a>,
{
type Assoc = Box<usize>;
}
fn foo<T: Overlap<U>, U>(x: T::Assoc) -> T::Assoc {
x
}
fn main() {
foo::<for<'a> fn(&'a (), ()), for<'a> fn(&'a (), ())>(3usize);
}
for<'a> fn(&'a (), ())>: Overlap<for<'a> fn(&'a (), ())>>
can be satisfied using both impls, ignoring a deficiency of the current normalization routine which means that right now the second impl pretty much never applies.
Currently inference constraints from equating the self type are not used to normalize the trait argument so we fail when equating ()
with Assoc<'a, for<'a> fn(&'a (), ())>
even those these two are the same type. This will change once deferred projection equality is implemented.
why this currently passes coherence
Coherence does a pairwise check for all relevant impls. It starts by instantiating the impl parameters with inference vars and equating the impl headers. When we do that with Overlap<T> for T
and Overlap<for<'a> fn(&'a (), Assoc<'a, T>)> for T
we have:
eq(?0: Overflap<?0>, ?1: Overlap<for<'a> fn(&'a (), <*const ?1 as ToUnit<'a>>::Unit)>)
eq(?0, ?1)
constrains?1
to be equal to?0
eq(?0, for<'a> fn(&'a (), <*const ?0 as ToUnit<'a>>::Unit)>)
: this now fails the occurs check
The occurs check is necessary to prevent ourselves from creating infinitely large types, e.g. ?0 = Vec<?0>
. But it does mean that coherence considers these two impls to be disjoint. Because the inference var only occurs inside of a projection, there's a way to equate these two types without resulting in an infinitely large type by normalizing the projection.