Skip to content

Are object bounds sound? #5

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
compiler-errors opened this issue Apr 13, 2023 · 1 comment
Open

Are object bounds sound? #5

compiler-errors opened this issue Apr 13, 2023 · 1 comment

Comments

@compiler-errors
Copy link
Member

(some older discussion here: https://hackmd.io/kw8vfb2oSFyQqatCjaFVSw)

Making objects' built-in bounds sound

when proving a predicate for dyn Trait from one of its existential bounds, we need to prove that all of the supertraits of that bound's trait hold for dyn Trait, plus all of the associated types' item bounds hold.

For example, given:

trait Trait {
    type Assoc: Bound + ?Sized;
}

For dyn Trait<Assoc = i32>: Trait to be proven, we must check the item bounds on Assoc.

If we do no additional work on top of just calling tcx.item_bounds({Trait::Assoc def-id}) and substituting Self = dyn Trait<Assoc = i32>, we get <dyn Trait<Assoc = i32> as Trait>::Assoc: Bound. However, in the new solver, this goal holds trivially via an alias bound candidate from the associated type.

To fix this, rust-lang/rust#108333 folds these object bounds, eagerly replacing projections with the associated types' values that appear in the dyn Trait itself. This would give us i32: Bound, which would fail.

Is this sufficient?

Idk. We probably should find that out before stabilizing the new solver, though.

@lcnr
Copy link
Contributor

lcnr commented Apr 17, 2023

I am pretty sure they are sound once we have fixed #6

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants