Fix replacing supertrait aliases in ReplaceProjectionWith

[compiler-errors]

The new solver has a procedure called predicates_for_object_candidate, which elaborates the super-bounds and item-bounds that are required to hold for a dyn trait to implement something via a built-in object impl.

In that procedure, there is a folder called ReplaceProjectionWith which is responsible for replacing projections that reference Self, so that we don't encounter cycles when we then go on to normalize those projections in the process of proving these super-bounds.

That folder had a few problems: Firstly, it wasn't actually checking that this was a super bound originating from Self. Secondly, it only accounted for a single projection type def id, but trait objects can have multiple (i.e. trait Foo<A, B>: Bar<A, Assoc = A> + Bar<B, Assoc = B>).

To fix the first, it's simple enough to just add an equality check for the self ty. To fix the second, I implemented a matching step that's very similar to the projection_may_match check we have for upcasting, since on top of having multiple choices, we need to deal with both non-structural matches and ambiguity.

This probably lacks a bit of documentation, but I think it works pretty well.

Fixes rust-lang/trait-system-refactor-initiative#171

r? lcnr

[rustbot]

Some changes occurred to the core trait solver

cc @rust-lang/initiative-trait-system-refactor

[compiler-errors]

Ideally we'd use a FallibleTypeFolder here rather than tracking ambiguity on the side. Unfortunately, I think it's impossible to implement a FallibleTypeFolder b/c of the blanket implementation:

impl FallibleTypeFolder<I> for F where F: TypeFolder<I> {}

...causing us to have impl overlap due to downstream impl ambiguity in coherence.

[lcnr]

:skull_emoji:

[lcnr]

would like to block this on #139768 then

[lcnr]

Want to familiarize myself with why exactly this folder is necessary again. A quick look at the comments and the link to lcnr/solver-woes#9 / rust-lang/trait-system-refactor-initiative#6 were not too unhelpful at getting this back into cache.

[compiler-errors]

Yeah, the documentation is lacking in the compiler.

It mentions the need for this folder to prevent unsoundness due to aliases trivially proving their own item bounds, but it doesn't mention that this folder is also required to prevent trivial (in the future -- coinductive, I think) cycles due to the fact that we require alias bounds to hold in the built-in impl.

This is made further interesting by the fact that aliases are allowed to be present in item bounds, for example see:

trait Foo {
    type Assoc: Baz<Self::Assoc>;
}

trait Baz<T> {}
impl Baz<()> for () {}

fn is_foo<T: Foo + ?Sized>() {}

fn main() {
    is_foo::<dyn Foo<Assoc = ()>>();
}

Such a built-in impl conceptually expands to something like:

impl<A> Foo for dyn Foo<Assoc = A>
where
    <Self as Foo>::Assoc: Baz<<Self as Foo>::Assoc>
{
    type Assoc = A;
}

Which I hope is clear that it'll lead to cycles :)

[compiler-errors]

Yeah, the documentation is lacking in the compiler.

Actually, the documentation already mentions a very similar example to the one I gave above:

/// Assemble a list of predicates that would be present on a theoretical
/// user impl for an object type. These predicates must be checked any time
/// we assemble a built-in object candidate for an object type, since they
/// are not implied by the well-formedness of the type.
///
/// For example, given the following traits:
///
/// ```rust,ignore (theoretical code)
/// trait Foo: Baz {
///     type Bar: Copy;
/// }
///
/// trait Baz {}
/// ```
///
/// For the dyn type `dyn Foo<Item = Ty>`, we can imagine there being a
/// pair of theoretical impls:
///
/// ```rust,ignore (theoretical code)
/// impl Foo for dyn Foo<Item = Ty>
/// where
///     Self: Baz,
///     <Self as Foo>::Bar: Copy,
/// {
///     type Bar = Ty;
/// }
///
/// impl Baz for dyn Foo<Item = Ty> {}
/// ```
///
/// However, in order to make such impls non-cyclical, we need to do an
/// additional step of eagerly folding the associated types in the where
/// clauses of the impl. In this example, that means replacing
/// `<Self as Foo>::Bar` with `Ty` in the first impl.

I kinda feel like that is sufficient to motivate the existence of the folder, and I'll just remove the FIXME since it's not necessary anymore.

[lcnr]

gamer

@bors r+ rollup

[bors]

📌 Commit e1936d2 has been approved by lcnr

It is now in the queue for this repository.