Stream: wg-traits

Topic: implied-bounds-flaw


scalexm (Jan 09 2019 at 21:39, on Zulip):

@nikomatsakis For a moment I thought the world was tearing apart, but that's ok

scalexm (Jan 09 2019 at 21:40, on Zulip):

we just overlooked something with implied bounds

scalexm (Jan 09 2019 at 21:40, on Zulip):

I mean I overlooked something, with my "optimization" that if you have say a function fn foo<T: Foo>(), and you call it with e.g. foo::<SomeType>, the caller only has to prove Implemented(SomeType: Foo) while the function can rely on FromEnv(T: Foo)

scalexm (Jan 09 2019 at 21:40, on Zulip):

well guess what, this optimization is wrong

scalexm (Jan 09 2019 at 21:41, on Zulip):

the caller should be proving the full WellFormed(SomeType: Foo)

scalexm (Jan 09 2019 at 21:41, on Zulip):

trivial example of why this optimization is wrong:

#![feature(trivial_bounds)]

trait Bar {
    fn foo();
}
trait Foo: Bar { }

// `WF(S) :- Implemented(S: Foo).` ok
// and the implied bound:
// `FromEnv(S: Foo) :- FromEnv(S)`
struct S where S: Foo;

impl Foo for S {
// We have `FromEnv(S)` which implies `Implemented(S: Foo)` and `Implemented(S: Bar)`,
// so we can prove `WellFormed(S: Foo)`.
}

fn bar<T: Bar>() {
    // Well `T = S` here and we never wrote a `Bar` impl for `S` actually.
    T::foo();
}

fn foo<T: Foo>() {
    // I can rely on `FromEnv(T: Foo)`, hence I can prove `Implemented(T: Bar)`.
    bar::<T>()
}

fn main() {
    // Ok I can prove `Implemented(S: Foo)` because of the impl
    foo::<S>()
}
nikomatsakis (Jan 09 2019 at 21:45, on Zulip):

makes sense

nikomatsakis (Jan 09 2019 at 21:45, on Zulip):

amazing how subtle this can be :)

scalexm (Jan 09 2019 at 21:45, on Zulip):

I guess we won't lose a lot without this optimization thanks to caching

nikomatsakis (Jan 09 2019 at 21:45, on Zulip):

I don't even remember this optimization, I have to admit

nikomatsakis (Jan 09 2019 at 21:45, on Zulip):

yep

nikomatsakis (Jan 14 2019 at 19:54, on Zulip):

@scalexm should I be putting this on some list of "things we need to follow up on"?

scalexm (Jan 14 2019 at 19:55, on Zulip):

@nikomatsakis yes

scalexm (Jan 23 2019 at 20:20, on Zulip):

@nikomatsakis

We can see that we have this asymmetry between well-formedness check, which only verifies that the direct superbounds hold, and implied bounds which gives access to all bounds transitively implied by the where clauses. In that case this is ok because as we said, we don't use FromEnv(Type<...>) to deduce other FromEnv(OtherType<...>) things, nor do we use FromEnv(Type: Trait) to deduce FromEnv(OtherType<...>) things. So in that sense type definitions are "less recursive" than traits, and we saw in a previous subsection that it was the combination of asymmetry and recursive trait / impls that led to unsoundness. As such, the WellFormed(Type<...>) predicate does not need to be co-inductive.

Last update: Nov 18 2019 at 02:00UTC