So, @scalexm, I am curious to get your thoughts about this alternate idea for implied bounds lowering.
The idea is to introduce two things:
Implemented(T: Trait)
-- produced by the trait, roughly equivalent to WellFormed(T: Trait)
todayDeclared(T: Trait)
-- produced by an implSo for something like
trait Ord: Eq { }
you would produce
Implemented(T: Ord) :- Declared(T: Ord), Implemented(T: Eq). Implemented(T: Eq) :- Implemented(T: Ord).
and then if you have impl Ord for Foo
that would produce
Declared(Foo: Ord).
along with the proof obligation that Implemented(Foo: Ord)
.
Without a impl Eq for Foo
impl, though, this proof obligation cannot be satisfied.
One nice property of this is that fn foo<T: Ord>()
can simply convert T: Ord
into Implemented(T: Ord)
in all cases, we don't have this "sometimes convert to FromEnv
, sometimes to Implemented
" thing going on.
I've not tried to go through all the examples though -- maybe it falls apart somewhere?
I am particularly interested in coinduction. Presumably Implemented
, like WellFormed
, is coinductive (but Declared
is not).
To expand on the fn foo<T: Ord>
thing, if the "goal" for foo
to be well-formed is G
, the idea is that we would produce a proof-obligation like
forall<G> { Implemented(T: Ord) => G }
and similarly if someone were to reference foo::<X>
, we would produce a proof obligation like Implemented(X: Ord)
One downside is that you are "re-proving" T: Eq
each time you prove T: Ord
(via the impl, anyway). However, we should be caching, so probably that's ok.
mmh, I'll try to test this setting on my usual battery of tricky examples
at first sight, it seems similar to our setting where we only had WellFormed
and Implemented
, and used WellFormed
for both well-formedness checks and implied bounds
Indeed I think it is equivalent?
It seems to be the same basic idea, but shifting the proof obligation from the impl to the places that reference the impl
we did not have the Implemented(...)
in the same places so maybe not equivalent
(although you also prove it at the impl)
in our current scheme, we are basically saying that impl proves the transitive case once (WellFormed
), and everybody else relies on that
(I meant maybe not equivalent to the WF/Implemented
-only setting)
oh ok I see, yes, yes
and I agree it felt very "familiar"
so that was part of why I wanted to run it by you
and see if we had rejected it already for some reason
or if it differed in some particular
yes at first sight I can't tell :) I'll look into it tomorrow morning, I'm going to sleep now :p
@scalexm want to r+ if you're happy then? it will fail to go through in the case a test fails of course (which is unlikely given we've verified locally)
@scalexm thanks. and for the advice as well. good night :-)
Ok @nikomatsakis some thoughts about this alternate encoding
// `Implemented(T: Foo) :- Declared(T: Foo), Implemented(<T as Foo>::Item: Foo).` // `Implemented(<T as Foo>::Item: Foo) :- Implemented(T: Foo).` trait Foo where <Self as Foo>::Item: Foo { type Item; } // `Declared(i32: Foo).` impl Foo for i32 { type Item = i32; // Prove `Implemented(i32: Foo)` --> ok if `Implemented` is co-inductive }
first, I think that because of this example, we need Implemented
to be co-inductive, do you agree?
I agree
However, Declared
would presumably not be (except for auto traits, perhaps)
Yes but then I have an example that fails :p
I’m on my phone right now, showing you in a few minutes
I think this setup is basically equivalent to our first one WF/Implemented
-only
Either WF
is inductive and you have to reject some useful impls, or it is unsound
ok @nikomatsakis, what do you think of this example:
// `Implemented(T: Copy) :- Declared(T: Copy).` trait Copy { } // `Implemented(T: Partial) :- Declared(T: Partial), Implemented(T: Copy).` // `Implemented(T: Copy) :- Implemented(T: Partial).` (*) trait Partial where Self: Copy { } // `Declared(T: Partial)`. impl<T> Partial for T { // Prove `Implemented(T: Partial)`: // true if `Declared(T: Partial)`, --> ok // `Implemented(T: Copy) // // Prove `Implemented(T: Copy)`: // true if `Implemented(T: Partial)` because of (*) // --> co-inductive cycle }
@scalexm hmm. So this is precisely the example I was thinking of. I'm trying to remember why I thought it would be ok. It may be that in relaying the idea I errored somewhere.
The plan was that trait Partial: Copy
lowes to this:
Implemented(T: Partial) iff Declared(T: Partial), Implemented(T: Copy).
which of course means that
Implemented(T: Partial) :- Declared(T: Partial), Implemented(T: Copy).
but I have to think about the reverse rule... honestly my brain does not seem to be functioning right now. It seems though that from this iff
we should be able to conclude that Implemented(T: Copy) => Implemented(T: Partial)
, as I wrote, right? I'll think about it when I'm a bit less worn out perhaps though (or look up the standard handling for iff
:P)
If this is an iff
, there should definitely be two reverse rules
Declared(T: Partial) :- Implemented(T: Partial)
and Implemented(T: Copy) :- Implemented(T: Partial)
Which in that case is exactly our very first setting
Revisiting this, it's really a fascinating failure. =)
@nikomatsakis for me, the problem with this approach is that it is the same approach as our first one from summer 2017
And we concluded that, we could not soundly handle cyclic things
Basically, if Implemented
in this setup is not co-inductive, you cannot handle decls like:
trait Foo where Self::Item: Foo { type Item; } impl Foo for () { type Item = (); }
So I don’t know
yeah I mean I agree it's wrong, @scalexm, I'm just trying to kind of dig a bit into why it's wrong. The core problem I think is that the co-inductive Implemented
predicate is used as more than a "carrier"
and co-induction without some guarantee of "productivity" (I think this is the term, iirc) is problematic -- (basically, the existence of cycles without some "step" in between)
anyway, I'm going to try and sketch some sort of "diagram-like thing" for the implied bounds to see if I can capture my intuition for what it was aiming at
I have to revit that soundness failure from WF(Type)
that you mentioned though
@nikomatsakis my own intuition for implied bounds is that they happen in two steps:
first we compute the full « graph » of impls, this is where we translate all the impls into rules of the form Implemented(...) :- Implemented(...)
** here we only have Implemented
goals and no WF
at all because we are just stating relations between impls
only when the impls graph is built, we check that all impls are legal: this is where we do generate WF
goals and try to prove them
Of course in practice these two steps happen in parallel, where we « discover » the impls graph lazily while checking legality: this works because WellFormed(TraitRef)
is co-inductive and hence can handle cycles
Then the difference between FromEnv
and WellFormed
is that WellFormed
serves as a graph traversal; while FromEnv
serves as finding a path in an oriented graph (going from one goal to prove to a possible clause in our environment)
So this is why the two are somehow unrelated, and also why WellFormed
should not have any reverse rules: it is somehow incompatible with its « graph traversal » semantics