## Stream: wg-traits

### Topic: alternate implied bounds lowering

nikomatsakis (Nov 07 2018 at 22:13, on Zulip):

The idea is to introduce two things:

• `Implemented(T: Trait)` -- produced by the trait, roughly equivalent to `WellFormed(T: Trait)` today
• `Declared(T: Trait)` -- produced by an impl

So 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).

nikomatsakis (Nov 07 2018 at 22:15, on Zulip):

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 }
```
nikomatsakis (Nov 07 2018 at 22:15, on Zulip):

and similarly if someone were to reference `foo::<X>`, we would produce a proof obligation like `Implemented(X: Ord)`

nikomatsakis (Nov 07 2018 at 22:16, on Zulip):

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.

scalexm (Nov 07 2018 at 22:18, on Zulip):

mmh, I'll try to test this setting on my usual battery of tricky examples

scalexm (Nov 07 2018 at 22:18, on Zulip):

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

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

Indeed I think it is equivalent?

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

It seems to be the same basic idea, but shifting the proof obligation from the impl to the places that reference the impl

scalexm (Nov 07 2018 at 22:19, on Zulip):

we did not have the `Implemented(...)` in the same places so maybe not equivalent

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

(although you also prove it at the impl)

nikomatsakis (Nov 07 2018 at 22:19, on Zulip):

in our current scheme, we are basically saying that impl proves the transitive case once (`WellFormed`), and everybody else relies on that

scalexm (Nov 07 2018 at 22:20, on Zulip):

(I meant maybe not equivalent to the `WF/Implemented`-only setting)

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

oh ok I see, yes, yes

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

and I agree it felt very "familiar"

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

so that was part of why I wanted to run it by you

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

nikomatsakis (Nov 07 2018 at 22:20, on Zulip):

or if it differed in some particular

scalexm (Nov 07 2018 at 22:21, on Zulip):

yes at first sight I can't tell :) I'll look into it tomorrow morning, I'm going to sleep now :p

Alexander Regueiro (Nov 07 2018 at 22:23, on Zulip):

@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)

Alexander Regueiro (Nov 07 2018 at 22:28, on Zulip):

@scalexm thanks. and for the advice as well. good night :-)

scalexm (Nov 08 2018 at 11:26, on Zulip):

scalexm (Nov 08 2018 at 11:27, on Zulip):
```// `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
}
```
scalexm (Nov 08 2018 at 11:27, on Zulip):

first, I think that because of this example, we need `Implemented` to be co-inductive, do you agree?

nikomatsakis (Nov 08 2018 at 16:01, on Zulip):

I agree

nikomatsakis (Nov 08 2018 at 16:01, on Zulip):

However, `Declared` would presumably not be (except for auto traits, perhaps)

scalexm (Nov 08 2018 at 16:05, on Zulip):

Yes but then I have an example that fails :p

scalexm (Nov 08 2018 at 16:05, on Zulip):

I’m on my phone right now, showing you in a few minutes

scalexm (Nov 08 2018 at 16:05, on Zulip):

I think this setup is basically equivalent to our first one `WF/Implemented`-only

scalexm (Nov 08 2018 at 16:06, on Zulip):

Either `WF` is inductive and you have to reject some useful impls, or it is unsound

scalexm (Nov 08 2018 at 16:46, on Zulip):

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
}
```
nikomatsakis (Nov 09 2018 at 16:22, on Zulip):

@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)

scalexm (Nov 09 2018 at 16:24, on Zulip):

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)`

scalexm (Nov 09 2018 at 16:25, on Zulip):

Which in that case is exactly our very first setting

nikomatsakis (Jan 22 2019 at 22:32, on Zulip):

Revisiting this, it's really a fascinating failure. =)

scalexm (Jan 23 2019 at 08:37, on Zulip):

@nikomatsakis for me, the problem with this approach is that it is the same approach as our first one from summer 2017

scalexm (Jan 23 2019 at 08:38, on Zulip):

And we concluded that, we could not soundly handle cyclic things

scalexm (Jan 23 2019 at 08:39, on Zulip):

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 = ();
}
```
scalexm (Jan 23 2019 at 08:41, on Zulip):

So I don’t know

nikomatsakis (Jan 23 2019 at 14:35, on Zulip):

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"

nikomatsakis (Jan 23 2019 at 14:37, on Zulip):

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)

nikomatsakis (Jan 23 2019 at 14:37, on Zulip):

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

nikomatsakis (Jan 23 2019 at 14:37, on Zulip):

I have to revit that soundness failure from `WF(Type)` that you mentioned though

scalexm (Jan 23 2019 at 16:39, on Zulip):

@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

scalexm (Jan 23 2019 at 16:40, on Zulip):

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)

scalexm (Jan 23 2019 at 16:40, on Zulip):

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

Last update: Jun 07 2020 at 08:05UTC