Elaborating where clauses on traits, structs #12
Comments
|
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 impl Bar for X
where X: Foo
{ }The only way to prove that would be to have an actual impl of 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: This would clearly never terminate. I'm not sure yet how properly to think about this. |
Closes rust-lang#19. I took a slightly different approach from your suggestion. ir::Program and ProgramEnvironment are distinct types with no ownership relationship, but instead of lowering returning a tuple, ir::Program has a method to construct a ProgramEnvironment. In addition to the trait_data, the associated_type_data also needs to be cloned over, and the `split_projection` method is duplicated for both types, because that method is invoked in `elaborated_clauses`. It seems like once we have a new way of solving rust-lang#12, ProgramEnvironment would just be a set of ProgramClauses, and that would be the whole context necessary for the solver to run.
|
Note the first code block should be |
|
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'... |
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 |
|
Okay learning a bit more about the internals I think what I mean is: right now we are talking about translating impl A into
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. |
|
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)
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 Next, when you have an impl of First, a where-clause like We create a set of 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 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 fn foo<T: Foo>(t: T) { ... }this 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. |
|
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 |
This isn't really unsupported today. What actually happens is that we error out trying to resolve 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 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 |
|
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: |
|
@scalexm this issue can be closed now, right? |
|
Well I don't know, currently we still have rules of the form |
|
@scalexm I see. OK, want to open a PR with that branch? |
|
OK, after some discussion with @arielb1 and @scalexm on gitter, it became clear that there is still another problem. This has to do with cycles that arise when trying to deal with associated types and bounds. Consider this setup: struct Unit { }
trait Foo { type Assoc: Foo; }
impl Foo for Unit { type Assoc = Unit; }The actual Chalk syntax for that is as follows: struct Unit { }
trait Foo where <Self as Foo>::Assoc: Foo { type Assoc; }
impl Foo for Unit { type Assoc = Unit; }which gives rise to lowered clauses in this gist, including notably this one: So now imagine that we try to prove that the impl of But, applying that here, means that we then have to prove It's not yet clear to me what step of this chain is wrong. =) |
|
Here is my last take at that. So we need to cleanly separate impls and WF requirements. The following impl block: impl<...> Foo<...> for SomeType<...> where W1, ..., Wk {
type Assoc = SomeOtherType<...>;
}lowers to the following set of rules: So these are the same rules as before the WF PR. Now say that the trait Foo<...> where C1, ..., Cn {
type Assoc;
}Then the WF requirements for the previous impl block we have seen can be informally translated as follows: So the main problem is to be able to compute the set of bounds implied by another set of bounds. Actually, there are two sub-problems.
The first problem (computing all the implied bounds) can be formally described as a least fixed point computation problem. Hence, we introduce the following predicate, which has a natural co-inductive meaning: Of course we introduce such a predicate for each trait. Note that The second problem is just walking up a graph: we start from what we want to prove, and we check if it is implied by something. If it is the case, then we try to know wether this new something is something we know. And so on. So we add an inductive predicate Again, we have such a predicate and rules for each trait. Also, note that within the logic program that we just obtained, we never have cycles which mixes inductive and co-inductive predicates. Now we can reformulate the WF requirements of the previous Some examplestrait Foo where Self: Bar {}
// WFco(Self: Foo) :- (Self: Foo), WFco(Self: Bar)
// (Self: Foo) :- WF(Self: Foo)
// WF(Self: Bar) :- WF(Self: Foo)
trait Bar where Self: Foo {}
// WFco(Self: Bar) :- (Self: Bar), WFco(Self: Foo)
// (Self: Bar) :- WF(Self: Bar)
// WF(Self: Foo) :- WF(Self: Bar)
impl Foo for i32 {}
// i32: Foo.
// i32FooImplWF :- WFco(i32: Foo)
impl Bar for i32 {}
// i32: Bar.
// i32BarImplWF :- WFco(i32: Bar)The two WF requirements hold. trait Clone {}
// WFco(Self: Clone) :- Self: Clone
// (Self: Clone) :- WF(Self: Clone)
trait Foo where Self: Bar, Self: Clone {}
// WFco(Self: Foo) :- (Self: Foo), WFco(Self: Bar), WFco(Self: Clone)
// (Self: Foo) :- WF(Self: Foo)
// WF(Self: Bar) :- WF(Self: Foo)
// WF(Self: Clone) :- WF(Self: Foo)
trait Bar where Self: Foo {}
// WFco(Self: Bar) :- (Self: Bar), WFco(Self: Foo)
// (Self: Bar) :- WF(Self: Bar)
// WF(Self: Foo) :- WF(Self: Bar)
impl<T> Foo for T {}
// T: Foo.
// TFooImplWF :- WFco(T: Foo)
impl<T> Bar for T where T: Foo {}
// T: Bar :- T: Foo.
// TBarImplWF :- if (WF(T: Foo)) { WFco(T: Bar) }The trait Foo where <Self as Foo>::Item: Foo {
type Item;
}
// WFco(Self: Foo) :- (Self: Foo), WFco(<Self as Foo>::Item: Foo)
// (Self: Foo) :- WF(Self: Foo)
// WF(<Self as Foo>::Item: Foo) :- WF(Self: Foo)
impl Foo for i32 {
type Item = i32;
}
// i32: Foo.
// <i32 as Foo>::Item ==> i32 :- (i32: Foo)
// i32FooImplWF :- WFco(i32: Foo)Since in this setting, we have How to use itInside each function: fn f<T: Foo>(...) { ... }just replace the Main problem of this approachSo we saw that this approach correctly handles cyclic impls. However, the problem is that the set of all implied bounds can be infinite, as in: trait Foo where Box<Self>: Foo { }
// WFco(Self: Foo) :- (Self: Foo), WFco(Box<Self>: Foo)In that case, the impl<T> Foo for T {}or at least an impl of the form: impl<...> Foo for Family<...> {}where I think we are close to having something usable, because I wrote a very straightforward implementation in chalk, and I also sketched a formal proof that this setting is sound (where I gave a formal definition of everything used in this setting, in particular a formal definition of “implied bounds” in terms of least fixed point and a formal definition of “soundness”). I hope we could tweak this setting in order to leverage the previous limitation. |
|
Inside each function: just replace the So the caller (actually, the expander of the type-scheme) has to prove that |
|
No, the caller just has to prove that This is actually related to how I formally defined soundness: let In other words, say you have a trait |
This feels like it ignores the parametric context. While this should be enough for translation, rustc also wants the version with arguments: "implication-elimination" theorem (here |
|
@arielb1 Yes I agree with you, and actually I did think about that when I sketched my proof. The thing is that we cannot ask for your definition in an intuitionistic model. Indeed, say we have the following traits and impls: Then if But we do not have: Then we would not be able to call And, in general, if you are inside a parametric function, you can go up the call stack, and at one point you will be in a non-parametric context. So I think what we need is: Which is a property that is true under my setting (if my soundness theorem is true under this setting), AS SOON AS |
|
That's why I added the Also, because impl-trees must be finite (and this should be the only case where we assume that impl trees are finite), we can recurse on them using the So after wf-checking, you can use this meta-theorem to avoid checking well-formedness in a "simple" semantics, and impl trees are restricted to be a finite tree of these forms (note: you can't get a use of WF here except at the root). |
|
Ah sorry, I responsed to the un-edited message. Is |
|
OK, so, @scalexm and I were talking about this. I am going to write up the idea as I understand it -- we ultimately adopted somewhat different terminology that I found helpful -- and then walk through an illustrative example. First, the terminology:
Then for a trait definition: trait Trait: C1 + .. + Cn { .. }we lower to the following clauses: Then an impl like: lowers to an and further must prove the following goal to be well-formed: Let's walk through this example that @scalexm came up with and is derived from rust-lang/rust#43784: I believe that using the rules above, we get the following clauses: And we have the following proof obligations: This one we can prove -- However the impl for It too must prove the same set of three things: Of course the user could have written In that case, both impls would be well-formed, but neither is usable, because of infinite recursion. |
Regarding this limitation, there is some work on recognizing such cycles and creating a richer notion of inductive hypothesis (as you probably recall). But I'm having trouble coming up with what could be a valid impl exactly or scenario where this limitation is problematic -- do you have any ideas? |
|
cc @nikomatsakis, @withoutboats Plan for GATsOK so we still need to figure out how to translate bounds on GATs, especially when it comes to WF requirements and implied bounds. Here's what I've come up with. So let's write a fully general GAT example: trait Foo {
// `'a` and `T` may actually designate multiple parameters
type Item<'a, T>: Bounds where WC;
}
impl Foo for Sometype {
type Item<'a, T> = Value<'a, T>;
// We don't repeat `WC`, and we cannot add more specific where clauses,
// exactly like associated methods.
// This may look like a limitation however, e.g.
// you cannot implement `type Item<T> = HashSet<T>` unless there was a
// `T: Hash` bound initially in the trait declaration, but it seems like a
// necessary one.
}and let us step directly onto the general rules, we'll see a simpler example later. ProjectingWe have two rules for projecting: // Fallback rule
forall<Self, 'a, T> {
ProjectionEq(<Self as Foo>::Item<'a, T> = (Foo::Item<'a, T>)<Self>).
}
forall<Self, 'a, T, U> {
ProjectionEq(<Self as Foo>::Item<'a, T> = U) :-
Normalize(<Self as Foo>::Item<'a, T> -> U).
}NormalizingThe rule for normalizing is given by: forall<'a, T> {
Normalize(<SomeType as Foo>::Item<'a, T> -> Value<'a, T>) :- Implemented(Self: Foo), WC
}WF requirementsThe above impl typechecks only if the following goal can be proven to be true: FooImplWF :-
/* ... normal WF requirements if we add bounds on the impl or on the traits etc ... */
forall<'a, T> {
if (FromEnv(WC)) {
WellFormed(Value<'a, T>), WellFormed(Value<'a, T>: Bounds)
}
}Implied boundsFirst of all, the where clause Then, a new implied bounds rule would deal with (possibly higher-ranked) bounds on the associated type: // New reverse rule
forall<Self, 'a, T, U> {
FromEnv(<T as Foo>::Item<'a, T>: Bounds) :- FromEnv(Self: Foo)
}Well-formedness of projection typesFinally, we add a rule about well-formedness of the skolemized projection type. forall<Self, 'a, T> {
WellFormed((Foo::Item<'a,T>)<Self>) :- WC, Implemented(Self: Foo).
FromEnv(WC) :- FromEnv((Foo::Item<'a,T>)<Self>).
FromEnv(Self: Foo) :- FromEnv((Foo::Item<'a,T>)<Self>).
}Concrete exampleLet's dig into a more concrete example and see how this all mixes up with the other ways of expressing bounds on associated types (i.e. in the trait header like trait Foo {
type Item<T: Clone>: Clone where Self: Sized;
// ^^^^^^^^^ this could be rewritten as `where T: Clone`
}
impl Foo for () {
type Item<T> = Vec<T>;
}Let's see the WF requirements for this impl: FooImplWF :-
forall<T> {
if (FromEnv(T: Clone), FromEnv(Vec<T>: Sized)) {
// ^^^^^^^^^^^^^ trivial bound
WellFormed(Vec<T>: Clone), WellFormed(Vec<T>)
}
}which are indeed satisfiable. Example of usage of implied bounds: fn foo<X: Foo>(arg: <X as Foo>::Item<T>) {
// ^^^^^^^^ no need for `T: Clone` because we assume
// `WellFormed(<X as Foo>::Item<T>)`
let cloned = arg.clone(); // we can rely on the fact that
// `<X as Foo>::Item<T>: Clone` thanks to
// the reverse rule
}The last question is how is this consistent with bounds expressed in the trait header. As long as there are no additional where clauses on the associated type, these two writings are perfectly equivalent when it comes to the rules we have seen before: trait Foo {
type Item<T>: Debug;
}
trait Foo where for<T> <Self as Foo>::Item<T>: Debug {
type Item<T>;
}Now, in the first setting where we have where clauses on the associated type: trait Foo {
type Item<T>: Clone where T: Clone;
}there is no other way to express the bound without adding support for where clauses in HRTBs. I don't really think this is a problem actually. Something you can do however is: trait Foo where for<T> <Self as Foo>::Item<T>: Clone {
type Item<T> where T: Clone;
}but this is probably not what you want since when writing an impl, you won't be able to use the fact that |
|
After some live discussion with @scalexm, it seems like we ought not to need the fn foo<X: Foo + Sized, T: Clone>(arg: <X as Foo>::Item<T>) {
// ^^^^^^^^ `T: Clone` needed for projecting out
let cloned = arg.clone(); // we can rely on the fact that
// `<X as Foo>::Item<T>: Clone` thanks to
// the reverse rule
}but we're not 100% sure how to set that up =) UPDATE: Idea we think works is to:
The idea is that the caller must have been able to unify with skolemized form, so we can use it, which sidesteps infinite recursion that would otherwise occur. |
|
Looking at the current implementation in Chalk, I believe the // Fallback rule
forall<Self, 'a, T> {
ProjectionEq(<Self as Foo>::Item<'a, T> = (Foo::Item<'a, T>)<Self>) :-
Implemented(Self as Foo).
}
forall<Self, 'a, T> {
WellFormed((Foo::Item<'a,T>)<Self>) :- WC.
}Since Is there any reason to do it one way or another? |
|
Actually this has been longly discussed :) trait Foo {
type Item<T>: Clone where T: Clone;
}
fn foo<X, T>(arg: <X as Foo>::Item<T>) {
// let cloned = arg.clone();
}The But if you uncomment the line, then you have to add a This is related with niko’s comment above, when at first we used to have |
|
Okay, interesting, thanks for the explanation. As I understand these rules, they're basically saying that This at least intuitively makes sense, and gives the solver an option to prove facts about our type via normalization or unification on the skolemized type. (I'm not yet 100% understanding of where such equivalences can and cannot be applied, though.) |
|
@nikomatsakis there is a bug in the implied bounds rule for GATs as described above, I think it should be: also @LukasKalbertodt raised interesting ergonomic questions and I don’t feel completely at ease with my answers, we should discuss this some more. |
|
Some comments from discord that someone might want to document permanently: Expand
|
Fix an implied bound related to assoc types according to #12
jackh726
added
needs triage
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 aboutUwhatever we can prove about<T as Foo>::Bar).The text was updated successfully, but these errors were encountered: