Elaborating where clauses on traits, structs

[nikomatsakis]

Related to #11, we don't really do anything clever with where clauses on traits/structs. We need to support "elaboration" -- ideally, a richer form than what the current compiler supports. In particular, we should be able to show that e.g. T: Ord => T: PartialOrd (supertrait) but also any other where-clause on traits, and in particular I'd like a better form of support around projections of associated types (e.g., T: Foo<Bar = U> should let us prove about U whatever we can prove about <T as Foo>::Bar).

[nikomatsakis]

We now support a basic form of elaboration, but I am not happy with it. In particular, we have some hard-coded rules that take in the environment and "elaborate" it at various points, much like the compiler does. My ideal would be to find a solution that encodes these relationships "into the logic" as program-clauses. For example, you might imagine:

pub trait Bar: Foo { }

would imply a rule like

(T: Bar) :- (T: Foo).

However, that doesn't quite work. In particular, I also want a program like this to be illegal:

struct X;
impl Bar for X { }
// impl Foo for X { } <-- this impl is missing!

Now the question is, why would this be illegal? If the WF requirements of the impl are that X: Foo, then we can prove that by showing that X: Bar (because the impl exists). That's sort of circular reasoning, clearly. So you could imagine that the impl has an implied where-clause, i.e., it's sort of equivalent to:

impl Bar for X
    where X: Foo
{ }

The only way to prove that would be to have an actual impl of Foo for X so that things terminate. This seems fine, except that I would like to extend elaboration to all where-clauses on a trait, and we currently support circular where-clauses on traits:

trait Foo<T: ?Sized> where T: Bar<Self> { }
trait Bar<T: ?Sized> where T: Foo<Self> { }
impl Foo<i32> for i32 { }
impl Bar<i32> for i32 { }
fn main() { }

Under the approach I proposed, the impls would generate rules like this:

(i32: Foo<i32>) :- (i32: Bar<i32>).
(i32: Bar<i32>) :- (i32: Foo<i32>).

This would clearly never terminate.

I'm not sure yet how properly to think about this.

[withoutboats]

Note the first code block should be pub trait Bar: Foo { }

[withoutboats]

Can we assume all other impls are well formed when checking clauses generated by each impl?

[nikomatsakis]

@withoutboats

Can we assume all other impls are well formed when checking clauses generated by each impl?

I'm not sure what you mean by 'clauses generated by each impl'...

[withoutboats]

@nikomatsakis

trait Foo<T: ?Sized> where T: Foo<Self> { }

struct Bar;
struct Baz;

// impl A
impl Foo<Baz> for Bar { }

// impl B
impl Foo<Bar> for Baz { }

To prove the wellformedness of impl A, we need to prove Baz: Foo<Bar>; currently all we have available is a rule that Baz: Foo<Bar> :- Bar: Foo<Baz>. What if instead clauses carried a context and we had a rule available outside of impl B that Baz: Foo<Bar>, because we assume that impls are well formed when not checking those specific impls?

[withoutboats]

Okay learning a bit more about the internals I think what I mean is:

right now we are talking about translating impl A into (Bar: Foo<Baz>) :- (Baz: Foo<Bar>); I think instead we should translate it into:

• Bar: Foo<Baz>.
• WF(Bar: Foo<Baz>) :- Baz: Foo<Bar>.

That is, we add a fact the impl implies without checking the impl, but also check the impl through a distinct WF check. That avoids cycles.

[nikomatsakis]

Right, so I remember @aturon and I talking about something like this at one point. I thought there was a catch, but perhaps it does work out if we do it just right.

I think the key idea is to distinguish (as you suggest) T: Foo from WF(T: Foo), and then to say that an impl establishes T: Foo but not WF(T: Foo). We then say that:

• an impl can assume that its input types are well-formed, but not its entire trait-reference;
  • to be well-formed, the impl must be able to prove that the trait-reference is well-formed, given its where-clauses and the implied bounds from its input-types.
• every where-clause the user writes like T: Foo is effectively expanded into T: Foo and WF(T: Foo)
• every trait defines rules for what it means for a trait-reference to be well-formed (like you suggested, but we need a few more rules I think)

So let's play out this example a bit more. First, the trait definitions define various rules around well-formedness:

trait Bar { fn bar(&self); }
// WF(?Self: Bar) :-
//     WF(?Self). // input type must be well-formed

trait Foo: Bar { fn foo(&self); }
// WF(?Self: Foo) :-
//     ?Self: Bar,
//     WF(?Self: Bar),
//     WF(?Self).
// ?Self: Bar :-
//     WF(?Self: Foo).
// WF(?Self: Bar) :-
//     WF(?Self: Foo).

You see that I added inverse rules that say "if you know that WF(T: Foo), then you know that T: Bar". I think these rules are necessary, as we'll see later on.

Next, when you have an impl of Foo you get a rule defining T: Foo:

First, a where-clause like T: Foo actually translates into two requirements: WF(T: Foo) and T: Foo.

We create a set of WF(T: Foo) rules based on the trait declaration for Foo:

trait Bar { fn bar(&self) { } }
// WF(?Self: Bar).

trait Foo: Bar { fn foo(&self) { } }
// WF(?Self: Foo) :-
//     ?Self: Bar,
//     WF(?Self: Bar).

When you make an impl of Foo like so, you only get rules for establishing facts T: Foo:

impl Foo for u32 { .. } // impl A
// u32: Foo :-
//     WF(u32). // impl requires its input types are well-formed, along with any explicit where-clauses.

We also have rules that check whether the impl is well-formed. This amounts to showing the WF requirements are met:

// ImplAWellFormed :-
//     WF(u32) => // we get to assume that Self type is well-formed...
//         WF(u32: Foo). // ...we must prove that the trait-ref is well-formed.

Finally, let's imagine some generic code that has a T: Foo bound:

fn foo<T: Foo>(t: T) { ... }

this T: Foo winds up being "lowered" to T: Foo and WF(T: Foo). This is needed because we want the body of foo() to be able to assume that T: Bar. The same applies in other contexts.

Perhaps this all works out nicely, then. Presumably we also have to ensure that we have enough guarantees to ensure that all types that appear (or are inferred) in the fn body are well-formed; from this it should follow that the resulting trait-references only refer to well-formed types.

[withoutboats]

Here's something which today is an unsupported cyclic reference:

trait Relation {
    type Related;
}

trait ToOne: Relation<Related = Option<Self::One>> {
    type One;
}

trait ToMany: Relation<Related = Vec<Self::Many>> {
    type Many;
}

I believe we could support it with the same cycle breaking technique of distinguishing between a T: Trait and WF(T: Trait). Do you think so?

[nikomatsakis]

@withoutboats

Here's something which today is an unsupported cyclic reference...I believe we could support it with the same cycle breaking technique of distinguishing between a T: Trait and WF(T: Trait). Do you think so?

This isn't really unsupported today. What actually happens is that we error out trying to resolve Self::One (and, in particular, to figure out what trait One comes from). If you write out the traits explicitly, it works:

trait Relation {
    type Related;
}

trait ToOne: Relation<Related = Option<<Self as ToOne>::One>> {
    type One;
}

trait ToMany: Relation<Related = Vec<<Self as ToMany>::Many>> {
    type Many;
}

fn main() { }

Chalk kind of sidesteps this problem by not supporting Self::One notation. =)

In any case, I think should work out fine in the setup. I guess the question is whether this setup might help rustc by separating out e.g. the fact that Self: ToOne from the construction of the facts around WF(Self: ToOne). Perhaps so.

[withoutboats]

This strategy should resolve recursive where clauses, I think (see this thread).

Something like this:

trait Foo { }
struct Bar;

impl Foo for Bar where Bar: Foo { }

Currently does not compile. But we should lower it to:

Foo: Bar.
WF(Foo: Bar) :- (Foo: Bar).