###### tags: `thoughts`, `solver`

# Problem with `dyn Trait: Trait` in new solver

In order for `dyn Trait: Trait` to be sound, proving the trait goal must additionally prove that:
1. All the supertrait bounds of `Trait` are satisfied by `dyn Trait`
2. All of the item bounds of `Trait`'s associated items are satisfied by `dyn Trait`'s associated item types, `dyn Trait<Assoc = ...>`.

## Where it goes wrong

trait Setup {
    type From: Copy;
}

fn copy<U: Setup + ?Sized>(from: &U::From) -> U::From {
    *from
}

pub fn copy_any<T>(t: &T) -> T {
    copy::<dyn Setup<From=T>>(t)
    //~^ ERROR the trait bound `T: Copy` is not satisfied
}

fn main() {
    let x = String::from("Hello, world");
    let y = copy_any(&x);
    println!("{y}");
}

In this example, when proving that `dyn Setup<From = T>: Setup`, we must also instantiate and evaluate the item bounds for the associated item `From`:
* `<dyn Setup<From = T> as Setup>::From: Copy`
* `<dyn Setup<From = T> as Setup>::From: Sized`

In the old solver, these goals are normalized before being evaluated into `T: Copy` and `T: Sized`. We then can see pretty clearly that `T: Copy` does not hold in the body of `copy_any`!

In the **new** solver, if we try doing the same thing, the goals are **not** normalized before being recursively evaluated. When we try to evaluate the goal `<dyn Setup<From = T> as Setup>::From: Copy`, it's trivially satisfied via `assemble_alias_bound_candidates`.

This allowing the code to compile, which segfaults :skull:

## A smaller example, and thoughts on the issue of trivially satisfied nested goals

Given the code:

trait Trait {
    type Assoc: Bound;
}

How do we solve the problem above, where the nested goals we must prove for soundness are totally "ignored" because they trivially hold?

I think that we should use a folder on these nested goals to eagerly replace projection types present in the object bounds like `<dyn Trait<Assoc = Ty> as Trait>::Assoc` into `Ty`.

To motivate why, let's think of what a "synthetic" impl for `dyn Trait<Assoc = Ty>` would look like--

impl Trait for dyn Trait<Assoc = Ty>
where
    <dyn Trait<Assoc = Ty> as Trait>::Assoc: Bound,
{
    type Assoc = Ty;
}

The bound on line 3 would cause an overflow.

In contrast, consider an "eagerly folded" synthetic impl like:

impl Trait for dyn Trait<Assoc = Ty>
where
    Ty: Bound,
{
    type Assoc = Ty;
}

This would enforce the correct conditions to make sure that `dyn Trait<Assoc = Ty>: Trait` does not hold without cycles!´

### Rigid

struct DynTrait;
struct Ty;

trait Trait {
    type Assoc: Bound;
}

trait Bound {}

impl Trait for DynTrait
where
    <DynTrait as Trait>::Assoc: Bound,
{
    type Assoc = Ty;
}

error[E0283]: type annotations needed: cannot satisfy `<DynTrait as Trait>::Assoc: Bound`
  --> <source>:10:1
   |
10 | impl Trait for DynTrait
   | ^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: cannot satisfy `<DynTrait as Trait>::Assoc: Bound`
note: required for `DynTrait` to implement `Trait`
  --> <source>:10:6
   |
10 | impl Trait for DynTrait
   |      ^^^^^     ^^^^^^^^
11 | where
12 |     <DynTrait as Trait>::Assoc: Bound,
   |                                 ----- unsatisfied trait bound introduced here

error[E0277]: the trait bound `Ty: Bound` is not satisfied
  --> <source>:12:5
   |
12 |     <DynTrait as Trait>::Assoc: Bound,
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Bound` is not implemented for `Ty`
   |
   = help: see issue #48214
   = help: add `#![feature(trivial_bounds)]` to the crate attributes to enable

error[E0283]: type annotations needed: cannot satisfy `<DynTrait as Trait>::Assoc: Bound`
  --> <source>:14:5
   |
14 |     type Assoc = Ty;
   |     ^^^^^^^^^^
   |
   = note: cannot satisfy `<DynTrait as Trait>::Assoc: Bound`
note: required for `DynTrait` to implement `Trait`
  --> <source>:10:6
   |
10 | impl Trait for DynTrait
   |      ^^^^^     ^^^^^^^^
11 | where
12 |     <DynTrait as Trait>::Assoc: Bound,
   |                                 ----- unsatisfied trait bound introduced here

error: aborting due to 3 previous errors

Some errors have detailed explanations: E0277, E0283.
For more information about an error, try `rustc --explain E0277`.
Compiler returned: 1