changed 2 years ago  
Linked with GitHub
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

Image Not Showing Possible Reasons
  • The image file may be corrupted
  • The server hosting the image is unavailable
  • The image path is incorrect
  • The image format is not supported
Learn More →

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
Select a repo