Open nikomatsakis opened 7 years ago
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.
Note the first code block should be pub trait Bar: Foo { }
Can we assume all other impls are well formed when checking clauses generated by each impl?
@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'...
@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?
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.
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:
T: Foo
is effectively expanded into T: Foo
and WF(T: Foo)
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.
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?
@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.
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).
@scalexm this issue can be closed now, right?
Well I don't know, currently we still have rules of the form WF(T: Trait) :- WF(T)
(i.e. we still require that the input types are well formed), so maybe tweak this + add implied bounds -- I think I have a local branch implementing all this.
@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:
WellFormed(?0 as Foo) :-
WellFormed(?0),
WellFormed(<?0 as Foo>::Assoc as Foo),
<?0 as Foo>::Assoc: Foo.
So now imagine that we try to prove that the impl of Unit
is valid. We have to prove WellFormed(Unit as Foo)
, which means proving WellFormed(<Unit as Foo>::Assoc as Foo)
. That leads us to this clause:
WellFormed(<?0 as Foo>::Assoc as Foo) :- WellFormed(?0 as Foo).
But, applying that here, means that we then have to prove WellFormed(Unit as Foo)
, which is precisely the thing we started out trying to prove. This is a problem.
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:
(SomeType<...>: Foo<...>) :- W1, ..., Wk
SomeType<...> as Foo>::Assoc ==> SomeOtherType<...> :- SomeType<...>: Foo<...>
So these are the same rules as before the WF PR.
Now say that the Foo
trait has the following declaration:
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:
FooImplWF :-
assume that every bound implied by W1, ..., Wk is true,
prove that every bound implied by C1, ..., Cn is true,
(prove that SomeOtherType<...> is WF)
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:
WFco(Self: Trait<...>) :- (Self: Trait<...>), WFco(C1), ..., WFco(Cn)
Of course we introduce such a predicate for each trait. Note that WFco(Self: Trait1)
is a different predicate from WFco(Self: Trait2)
which means that only cycles of the form WFco(Self: Trait1) :- ... :- WFco(Self: Trait1)
are accepted due to co-inductive semantics.
Why does it have a natural co-inductive meaning? Because if we reach a cycle, this means that we have reached a fixed point when computing the set of implied bounds, which means that we have enumerated all the implied bounds.
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 WF(Self: Trait<...>)
associated to the following rules:
Self: Trait<...> :- WF(Self: Trait<...>)
WF(C1) :- WF(Self: Trait<...>)
...
WF(Cn) :- WF(Self: Trait<...>)
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 Foo
impl:
FooImplWF :-
if (WF(W1), ..., WF(Wk)) {
WFco(SomeType<...>: Trait<...>)
}
trait 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 Bar
impl meets its WF requirements, but not the Foo
impl. This can be fixed by adding a where T: Clone
bound on the Foo
impl.
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 <i32 as Foo>::Item ==> i32
then WFco(<i32 as Foo>::Item: Foo)
unifies with WFco(i32: Foo)
and we reach a co-inductive cycle when checking the WF requirements of the Foo
impl.
Inside each function:
fn f<T: Foo>(...) { ... }
just replace the T: Foo
bound by a WF(T: Foo)
bound.
So 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 WFco(Self: Foo)
predicate will run indefinitely since it will enumerate all the implied bounds, never reaching a co-inductive cycle. Of course, the only way to actually use this trait would be to have this impl:
impl<T> Foo for T {}
or at least an impl of the form:
impl<...> Foo for Family<...> {}
where Family<...>
is an infinite family of types such that T
belongs to Family<...>
implies that Box<T>
also belongs to Family<...>
. Hence, the where Box<Self>: Foo
is not needed actually. But this still seems like an actual limitation.
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.
cc @nikomatsakis @arielb1
Inside each function:
fn f<T: Foo>(...) { ... }
just replace the T: Foo
bound by a WF(T: Foo)
bound.
So the caller (actually, the expander of the type-scheme) has to prove that WFco(T: Foo)
? Which they can prove by either enumerating all implied bounds, or by using an i32FooImplWF
-style theorem?
No, the caller just has to prove that T: Foo
holds, because indeed i32FooImplWF
has already been proven.
This is actually related to how I formally defined soundness: let A
be a set of trait bounds and T
a given type. If |- A
and Implied(A) |- T: Trait
, then |- T: Trait
.
In other words, say you have a trait trait Foo: Copy
and that String: Foo
holds (i.e. an impl Foo for String
has been written). And you call f::<String>()
. Then f
will assume that WF(T: Foo)
holds where T = String
(although f
does not know what T
is), hence deduce that T: Copy
i.e. String: Copy
. If you have the soundness property, then you know that |- String: Copy
must hold, i.e. an impl Copy for String
has been written. This means that you cannot trick the type-checker to derive trait bounds for a given type for which an actual impl does not exist. That seems like a good definition of soundness.
If
|- A
andImplied(A) |- T: Trait
, then|- T: 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 |-
is recursive impl search):
Γ, WF(Γ) |- A
Γ, WF(Γ), Implied(A) |- T: Trait
------------
Γ, WF(Γ) |- T: Trait
@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:
trait Foo: Copy {}
impl<T> Foo for T where T: Foo
Then if T
is a given type, let Γ = { T: Foo }
we have:
Γ |- T: Foo
Γ, Implied(T: Foo) |- T: Copy
But we do not have: Γ |- T: Copy
. The point is that, if we had a function:
fn f<T: Foo>()
Then we would not be able to call f
in a non-parametric context.
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:
|- Γ1
Γ1, Implied(Γ1) |- Γ2
...
Γ(N-1), Implied(Γ(N-1)) |- ΓN
- - - - - - - - - -
|- ΓN
Which is a property that is true under my setting (if my soundness theorem is true under this setting), AS SOON AS Implied(Γ(K))
is finite for all K.
@scalexm
That's why I added the WF(Γ)
as a parameter to the parametric definition. We have WF(Γ) |- T: Copy
, so order is restored.
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 ImplWf
rules to get this:
for every impl in the universe, ImplWf
Γ, WF(Γ) |- T: Trait
--------
Γ, WF(Γ) |- WF(T: Trait)
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).
--------
T: Trait |- T: Trait
T2: Trait2 predicate of T: Trait
--------
WF(T: Trait) |- T2: Trait2
T2: Trait2 predicate of T: Trait
--------
WF(T: Trait) |- WF(T2: Trait2)
impl Trait for T where C1...Cn
--------
C1...Cn |- T: Trait
Ah sorry, I responsed to the un-edited message. Is WF(Γ)
the same thing as Implied(Γ)
? If so, I agree.
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:
Implemented(T: Trait)
-- the type T
is known to implement the trait Trait
WellFormed(T: Trait)
-- the type T
implements Trait
and all of the where clauses on Trait
are satisfied
WFco
originallyT: Trait
to be implementedFromEnv(T: Trait)
-- the environment tells us that T: Trait
holds
WF
originallyT: Trait
holds by hypothesis, either directly or indirectly via implied boundsThen for a trait definition:
trait Trait: C1 + .. + Cn { .. }
we lower to the following clauses:
WellFormed(T: Trait) :- Implemented(T: Trait) + WellFormed(C1) + .. + WellFormed(Cn).
Implemented(T: Trait) :- FromEnv(T: Trait).
FromEnv(T: C1) :- FromEnv(T: Trait).
...
FromEnv(T: Cn) :- FromEnv(T: Trait).
Then an impl like:
impl<..> Trait for .. where W1..Wk
lowers to an Implemented
clause:
Implemented(T: Trait) :- Implemented(W1), ..., Implemented(Wk).
and further must prove the following goal to be well-formed:
forall<...> { // impl's type parameters
if (FromEnv(W1) .. FromEnv(Wk)) {
WellFormed(T: Trait)
}
}
Let's walk through this example that @scalexm came up with and is derived from rust-lang/rust#43784:
trait A where Self: B, Self: Copy {}
trait B where Self: A { }
trait Copy { }
impl<T> A for T where T: B {}
impl<T> B for T {}
I believe that using the rules above, we get the following clauses:
// trait A where Self: B, Self: Copy {}
WellFormed(T: A) :- Implemented(T: A), WellFormed(T: B), WellFormed(T: Copy).
Implemented(T: A) :- FromEnv(T: A).
FromEnv(T: B) :- FromEnv(T: A).
FromEnv(T: Copy) :- FromEnv(T: A).
// trait B where Self: A { }
WellFormed(T: B) :- Implemented(T: B), WellFormed(T: A).
Implemented(T: B) :- FromEnv(T: B).
FromEnv(T: A) :- FromEnv(T: B).
// trait Copy { }
WellFormed(T: Copy) :- Implemented(T: Copy).
Implemented(T: Copy) :- FromEnv(T: Copy).
// impl<T> A for T where T: B {}
Implemented(T: A) :- Implemented(T: B).
// impl<T> B for T {}
Implemented(T: B).
And we have the following proof obligations:
// impl<T> A for T where T: B {}
forall<T> {
if (FromEnv(T: B)) {
WellFormed(T: A).
}
}
This one we can prove -- WellFormed(T: A)
requires ultimately proving three things:
Implemented(T: A)
holds from the impl clause (and then hypothesis)Implemented(T: B)
holds by hypothesis (FromEnv(T: B)
) or from the impl clause.Implemented(T: Copy)
holds transitively by hypothesis:
FromEnv(T: B) => FromEnv(T: A) => FromEnv(T: Copy)
However the impl for B
we cannot prove:
// impl<T> B for T {}
forall<T> {
WellFormed(T: B).
}
It too must prove the same set of three things:
Implemented(T: A)
holds from the two impl clauses.Implemented(T: B)
holds from the impl clause.Implemented(T: Copy)
does not have a corresponding impl clause. And there is no FromEnv
in scope so we can't use the implied bounds.Of course the user could have written
impl<T> B for T where T: A { }
In that case, both impls would be well-formed, but neither is usable, because of infinite recursion.
@scalexm
In that case, the WFco(Self: Foo) predicate will run indefinitely since it will enumerate all the implied bounds, never reaching a co-inductive cycle. Of course, the only way to actually use this trait would be to have this impl:
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
OK 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.
We 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).
}
The rule for normalizing is given by:
forall<'a, T> {
Normalize(<SomeType as Foo>::Item<'a, T> -> Value<'a, T>) :- Implemented(Self: Foo), WC
}
The 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)
}
}
First of all, the where clause where T: Foo<Item = U>
in the AST should now lower to two domain goals: Implemented(T: Item)
and ProjectionEq(<T as Foo>::Item = U)
. We would also remove the WellFormed(ProjectionEq)
domain goal.
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)
}
Finally, 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>).
}
Let'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 where Self::Item: blabla
.
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 T: Clone
in order to prove that <Self as Foo>::Item<T>: Clone
(you will need to be able to prove it for all T
without any other conditions).
After some live discussion with @scalexm, it seems like we ought not to need the X: Sized
and T: Clone
bounds here, because knowing that the argument type is WF ought to let us infer them:
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:
FromEnv((Foo::Item)<X, T>)
into the environment used to check the body of foo
FromEnv(WC) :- FromEnv(Foo::Item)<X, T>)
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 Implemented(Self as Foo)
condition ought to be moved from the WellFormed
rule to the fallback rule, as follows:
// 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 <T as Foo>::Item
will unify with (Foo::Item)<T>
only if T: Foo
, our WF clause is correct.
Is there any reason to do it one way or another?
Actually this has been longly discussed :)
If you put it on the fallback clause instead of the WF clause, this allows for a slight inconsistency within implied bounds. That is, let’s say Implemented(Self: Foo)
is on the fallback rule, and consider this function:
trait Foo {
type Item<T>: Clone where T: Clone;
}
fn foo<X, T>(arg: <X as Foo>::Item<T>) {
// let cloned = arg.clone();
}
The foo
function assumes all its inputs are WF. Especially, it assumes that <X as Foo>::Item<T>
is WF (note that this is the projection type and not the skolemized type, which does not really actually exist in rust code). As this point, this function is ok.
But if you uncomment the line, then you have to add a X: Foo
bound on foo
. Indeed, in order to use the fact that <X as Foo>::Item<T>: Clone
, you would like to use the fact that X: Foo
applies, which is in turn implied by WF((Foo::Item<T>)<Self>)
. Seems fine, but in fact the type in the WF
predicate is the skolemized type this time, and in your environment you only have WF(<X as Foo>::Item<T>)
(assumption that your inputs are WF). If you want this predicate to unify with the former, you need to use the fallback rule, which means you need to prove X: Foo
. This is inconsistent and surprising.
This is related with niko’s comment above, when at first we used to have WC
on the fallback rule and not on the WF
rule, and we were dealing with another inconsistency. We were wondering whether we could juste replace every non-skolemized WF
predicates in the environment by their skolemized form; it seemt to work but felt a bit awkward. Hence, we moved to this other design.
Okay, interesting, thanks for the explanation.
As I understand these rules, they're basically saying that <X as Foo>::Item<T>
and (Foo::Item<'a, T>)<Self>
are equivalent representations of the same thing, and so should always be considered equal.
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:
FromEnv(<T as Foo>::Item<‘a, T>: Bounds) :- FromEnv(Self: Foo), FromEnv(WC)
also @LukasKalbertodt raised interesting ergonomic questions and I don’t feel completely at ease with my answers, we should discuss this some more. ———- ÉDIT: I am now at ease with the answers I provided to them :)
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 aboutU
whatever we can prove about<T as Foo>::Bar
).