(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.
(some older discussion here: https://hackmd.io/kw8vfb2oSFyQqatCjaFVSw)
Making objects' built-in bounds sound
when proving a predicate for
dyn Traitfrom one of its existential bounds, we need to prove that all of the supertraits of that bound's trait hold fordyn Trait, plus all of the associated types' item bounds hold.For example, given:
For
dyn Trait<Assoc = i32>: Traitto be proven, we must check the item bounds onAssoc.Without any additional work on top of just calling
tcx.item_bounds({Trait::Assoc def-id})and substitutingSelf = 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 Traititself. This would give usi32: 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.