Skip to content
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

are object bounds sound? #10

Closed
compiler-errors opened this issue Feb 24, 2023 · 3 comments
Closed

are object bounds sound? #10

compiler-errors opened this issue Feb 24, 2023 · 3 comments

Comments

@compiler-errors
Copy link

(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.

Without any 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.

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?

It seems to work, but I'm not convinced that it's sufficient... it would be nice to more rigorously convince ourselves about this being a sound approach.

@lcnr

This comment was marked as outdated.

@compiler-errors

This comment was marked as outdated.

@compiler-errors
Copy link
Author

Closing in favor for rust-lang/trait-system-refactor-initiative#5

@compiler-errors compiler-errors closed this as not planned Won't fix, can't repro, duplicate, stale Apr 13, 2023
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