# Implied Bounds

Implied bounds remove the need to repeat where clauses written on a type declaration or a trait declaration. For example, say we have the following type declaration:

```
struct HashSet<K: Hash> {
...
}
```

then everywhere we use `HashSet<K>`

as an "input" type, that is appearing in
the receiver type of an `impl`

or in the arguments of a function, we don't
want to have to repeat the `where K: Hash`

bound, as in:

```
// I don't want to have to repeat `where K: Hash` here.
impl<K> HashSet<K> {
...
}
// Same here.
fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
println!("inserting!");
set.insert(item);
}
```

Note that in the `loud_insert`

example, `HashSet<K>`

is not the type
of the `set`

argument of `loud_insert`

, it only *appears* in the
argument type `&mut HashSet<K>`

: we care about every type appearing
in the function's header (the header is the signature without the return type),
not only types of the function's arguments.

The rationale for applying implied bounds to input types is that, for example,
in order to call the `loud_insert`

function above, the programmer must have
*produced* the type `HashSet<K>`

already, hence the compiler already verified
that `HashSet<K>`

was well-formed, i.e. that `K`

effectively implemented
`Hash`

, as in the following example:

```
fn main() {
// I am producing a value of type `HashSet<i32>`.
// If `i32` was not `Hash`, the compiler would report an error here.
let set: HashSet<i32> = HashSet::new();
loud_insert(&mut set, 5);
}
```

Hence, we don't want to repeat where clauses for input types because that would
sort of duplicate the work of the programmer, having to verify that their types
are well-formed both when calling the function and when using them in the
arguments of their function. The same reasoning applies when using an `impl`

.

Similarly, given the following trait declaration:

```
trait Copy where Self: Clone { // desugared version of `Copy: Clone`
...
}
```

then everywhere we bound over `SomeType: Copy`

, we would like to be able to
use the fact that `SomeType: Clone`

without having to write it explicitly,
as in:

```
fn loud_clone<T: Clone>(x: T) {
println!("cloning!");
x.clone();
}
fn fun_with_copy<T: Copy>(x: T) {
println!("will clone a `Copy` type soon...");
// I'm using `loud_clone<T: Clone>` with `T: Copy`, I know this
// implies `T: Clone` so I don't want to have to write it explicitly.
loud_clone(x);
}
```

The rationale for implied bounds for traits is that if a type implements
`Copy`

, that is, if there exists an `impl Copy`

for that type, there *ought*
to exist an `impl Clone`

for that type, otherwise the compiler would have
reported an error in the first place. So again, if we were forced to repeat the
additional `where SomeType: Clone`

everywhere whereas we already know that
`SomeType: Copy`

hold, we would kind of duplicate the verification work.

Implied bounds are not yet completely enforced in rustc, at the moment it only works for outlive requirements, super trait bounds, and bounds on associated types. The full RFC can be found here. We'll give here a brief view of how implied bounds work and why we chose to implement it that way. The complete set of lowering rules can be found in the corresponding chapter.

## Implied bounds and lowering rules

Now we need to express implied bounds in terms of logical rules. We will start with exposing a naive way to do it. Suppose that we have the following traits:

```
trait Foo {
...
}
trait Bar where Self: Foo { } {
...
}
```

So we would like to say that if a type implements `Bar`

, then necessarily
it must also implement `Foo`

. We might think that a clause like this would
work:

```
forall<Type> {
Implemented(Type: Foo) :- Implemented(Type: Bar).
}
```

Now suppose that we just write this impl:

```
struct X;
impl Bar for X { }
```

Clearly this should not be allowed: indeed, we wrote a `Bar`

impl for `X`

, but
the `Bar`

trait requires that we also implement `Foo`

for `X`

, which we never
did. In terms of what the compiler does, this would look like this:

```
struct X;
impl Bar for X {
// We are in a `Bar` impl for the type `X`.
// There is a `where Self: Foo` bound on the `Bar` trait declaration.
// Hence I need to prove that `X` also implements `Foo` for that impl
// to be legal.
}
```

So the compiler would try to prove `Implemented(X: Foo)`

. Of course it will
not find any `impl Foo for X`

since we did not write any. However, it
will see our implied bound clause:

```
forall<Type> {
Implemented(Type: Foo) :- Implemented(Type: Bar).
}
```

so that it may be able to prove `Implemented(X: Foo)`

if `Implemented(X: Bar)`

holds. And it turns out that `Implemented(X: Bar)`

does hold since we wrote
a `Bar`

impl for `X`

! Hence the compiler will accept the `Bar`

impl while it
should not.

## Implied bounds coming from the environment

So the naive approach does not work. What we need to do is to somehow decouple
implied bounds from impls. Suppose we know that a type `SomeType<...>`

implements `Bar`

and we want to deduce that `SomeType<...>`

must also implement
`Foo`

.

There are two possibilities: first, we have enough information about
`SomeType<...>`

to see that there exists a `Bar`

impl in the program which
covers `SomeType<...>`

, for example a plain `impl<...> Bar for SomeType<...>`

.
Then if the compiler has done its job correctly, there *must* exist a `Foo`

impl which covers `SomeType<...>`

, e.g. another plain
`impl<...> Foo for SomeType<...>`

. In that case then, we can just use this
impl and we do not need implied bounds at all.

Second possibility: we do not know enough about `SomeType<...>`

in order to
find a `Bar`

impl which covers it, for example if `SomeType<...>`

is just
a type parameter in a function:

```
fn foo<T: Bar>() {
// We'd like to deduce `Implemented(T: Foo)`.
}
```

That is, the information that `T`

implements `Bar`

here comes from the
*environment*. The environment is the set of things that we assume to be true
when we type check some Rust declaration. In that case, what we assume is that
`T: Bar`

. Then at that point, we might authorize ourselves to have some kind
of "local" implied bound reasoning which would say
`Implemented(T: Foo) :- Implemented(T: Bar)`

. This reasoning would
only be done within our `foo`

function in order to avoid the earlier
problem where we had a global clause.

We can apply this local reasoning everywhere we can have an environment -- i.e. when we can write where clauses -- that is, inside impls, trait declarations, and type declarations.

## Computing implied bounds with `FromEnv`

The previous subsection showed that it was only useful to compute implied bounds for facts coming from the environment. We talked about "local" rules, but there are multiple possible strategies to indeed implement the locality of implied bounds.

In rustc, the current strategy is to *elaborate* bounds: that is, each time
we have a fact in the environment, we recursively derive all the other things
that are implied by this fact until we reach a fixed point. For example, if
we have the following declarations:

```
trait A { }
trait B where Self: A { }
trait C where Self: B { }
fn foo<T: C>() {
...
}
```

then inside the `foo`

function, we start with an environment containing only
`Implemented(T: C)`

. Then because of implied bounds for the `C`

trait, we
elaborate `Implemented(T: B)`

and add it to our environment. Because of
implied bounds for the `B`

trait, we elaborate `Implemented(T: A)`

and add it
to our environment as well. We cannot elaborate anything else, so we conclude
that our final environment consists of `Implemented(T: A + B + C)`

.

In the new-style trait system, we like to encode as many things as possible
with logical rules. So rather than "elaborating", we have a set of *global*
program clauses defined like so:

```
forall<T> { Implemented(T: A) :- FromEnv(T: A). }
forall<T> { Implemented(T: B) :- FromEnv(T: B). }
forall<T> { FromEnv(T: A) :- FromEnv(T: B). }
forall<T> { Implemented(T: C) :- FromEnv(T: C). }
forall<T> { FromEnv(T: B) :- FromEnv(T: C). }
```

So these clauses are defined globally (that is, they are available from
everywhere in the program) but they cannot be used because the hypothesis
is always of the form `FromEnv(...)`

which is a bit special. Indeed, as
indicated by the name, `FromEnv(...)`

facts can **only** come from the
environment.
How it works is that in the `foo`

function, instead of having an environment
containing `Implemented(T: C)`

, we replace this environment with
`FromEnv(T: C)`

. From here and thanks to the above clauses, we see that we
are able to reach any of `Implemented(T: A)`

, `Implemented(T: B)`

or
`Implemented(T: C)`

, which is what we wanted.

## Implied bounds and well-formedness checking

Implied bounds are tightly related with well-formedness checking. Well-formedness checking is the process of checking that the impls the programmer wrote are legal, what we referred to earlier as "the compiler doing its job correctly".

We already saw examples of illegal and legal impls:

```
trait Foo { }
trait Bar where Self: Foo { }
struct X;
struct Y;
impl Bar for X {
// This impl is not legal: the `Bar` trait requires that we also
// implement `Foo`, and we didn't.
}
impl Foo for Y {
// This impl is legal: there is nothing to check as there are no where
// clauses on the `Foo` trait.
}
impl Bar for Y {
// This impl is legal: we have a `Foo` impl for `Y`.
}
```

We must define what "legal" and "illegal" mean. For this, we introduce another
predicate: `WellFormed(Type: Trait)`

. We say that the trait reference
`Type: Trait`

is well-formed if `Type`

meets the bounds written on the
`Trait`

declaration. For each impl we write, assuming that the where clauses
declared on the impl hold, the compiler tries to prove that the corresponding
trait reference is well-formed. The impl is legal if the compiler manages to do
so.

Coming to the definition of `WellFormed(Type: Trait)`

, it would be tempting
to define it as:

```
trait Trait where WC1, WC2, ..., WCn {
...
}
```

```
forall<Type> {
WellFormed(Type: Trait) :- WC1 && WC2 && .. && WCn.
}
```

and indeed this was basically what was done in rustc until it was noticed that
this mixed badly with implied bounds. The key thing is that implied bounds
allows someone to derive all bounds implied by a fact in the environment, and
this *transitively* as we've seen with the `A + B + C`

traits example.
However, the `WellFormed`

predicate as defined above only checks that the
*direct* superbounds hold. That is, if we come back to our `A + B + C`

example:

```
trait A { }
// No where clauses, always well-formed.
// forall<Type> { WellFormed(Type: A). }
trait B where Self: A { }
// We only check the direct superbound `Self: A`.
// forall<Type> { WellFormed(Type: B) :- Implemented(Type: A). }
trait C where Self: B { }
// We only check the direct superbound `Self: B`. We do not check
// the `Self: A` implied bound coming from the `Self: B` superbound.
// forall<Type> { WellFormed(Type: C) :- Implemented(Type: B). }
```

There is an asymmetry between the recursive power of implied bounds and
the shallow checking of `WellFormed`

. It turns out that this asymmetry
can be exploited. Indeed, suppose that we define the following
traits:

```
trait Partial where Self: Copy { }
// WellFormed(Self: Partial) :- Implemented(Self: Copy).
trait Complete where Self: Partial { }
// WellFormed(Self: Complete) :- Implemented(Self: Partial).
impl<T> Partial for T where T: Complete { }
impl<T> Complete for T { }
```

For the `Partial`

impl, what the compiler must prove is:

```
forall<T> {
if (T: Complete) { // assume that the where clauses hold
WellFormed(T: Partial) // show that the trait reference is well-formed
}
}
```

Proving `WellFormed(T: Partial)`

amounts to proving `Implemented(T: Copy)`

.
However, we have `Implemented(T: Complete)`

in our environment: thanks to
implied bounds, we can deduce `Implemented(T: Partial)`

. Using implied bounds
one level deeper, we can deduce `Implemented(T: Copy)`

. Finally, the `Partial`

impl is legal.

For the `Complete`

impl, what the compiler must prove is:

```
forall<T> {
WellFormed(T: Complete) // show that the trait reference is well-formed
}
```

Proving `WellFormed(T: Complete)`

amounts to proving `Implemented(T: Partial)`

.
We see that the `impl Partial for T`

applies if we can prove
`Implemented(T: Complete)`

, and it turns out we can prove this fact since our
`impl<T> Complete for T`

is a blanket impl without any where clauses.

So both impls are legal and the compiler accepts the program. Moreover, thanks
to the `Complete`

blanket impl, all types implement `Complete`

. So we could
now use this impl like so:

```
fn eat<T>(x: T) { }
fn copy_everything<T: Complete>(x: T) {
eat(x);
eat(x);
}
fn main() {
let not_copiable = vec![1, 2, 3, 4];
copy_everything(not_copiable);
}
```

In this program, we use the fact that `Vec<i32>`

implements `Complete`

, as any
other type. Hence we can call `copy_everything`

with an argument of type
`Vec<i32>`

. Inside the `copy_everything`

function, we have the
`Implemented(T: Complete)`

bound in our environment. Thanks to implied bounds,
we can deduce `Implemented(T: Partial)`

. Using implied bounds again, we deduce
`Implemented(T: Copy)`

and we can indeed call the `eat`

function which moves
the argument twice since its argument is `Copy`

. Problem: the `T`

type was
in fact `Vec<i32>`

which is not copy at all, hence we will double-free the
underlying vec storage so we have a memory unsoundness in safe Rust.

Of course, disregarding the asymmetry between `WellFormed`

and implied bounds,
this bug was possible only because we had some kind of self-referencing impls.
But self-referencing impls are very useful in practice and are not the real
culprits in this affair.

## Co-inductiveness of `WellFormed`

So the solution is to fix this asymmetry between `WellFormed`

and implied
bounds. For that, we need for the `WellFormed`

predicate to not only require
that the direct superbounds hold, but also all the bounds transitively implied
by the superbounds. What we can do is to have the following rules for the
`WellFormed`

predicate:

```
trait A { }
// WellFormed(Self: A) :- Implemented(Self: A).
trait B where Self: A { }
// WellFormed(Self: B) :- Implemented(Self: B) && WellFormed(Self: A).
trait C where Self: B { }
// WellFormed(Self: C) :- Implemented(Self: C) && WellFormed(Self: B).
```

Notice that we are now also requiring `Implemented(Self: Trait)`

for
`WellFormed(Self: Trait)`

to be true: this is to simplify the process of
traversing all the implied bounds transitively. This does not change anything
when checking whether impls are legal, because since we assume
that the where clauses hold inside the impl, we know that the corresponding
trait reference does hold. Thanks to this setup, you can see that we indeed
require to prove the set of all bounds transitively implied by the where
clauses.

However there is still a catch. Suppose that we have the following trait definition:

```
trait Foo where <Self as Foo>::Item: Foo {
type Item;
}
```

so this definition is a bit more involved than the ones we've seen already because it defines an associated item. However, the well-formedness rule would not be more complicated:

```
WellFormed(Self: Foo) :-
Implemented(Self: Foo) &&
WellFormed(<Self as Foo>::Item: Foo).
```

Now we would like to write the following impl:

```
impl Foo for i32 {
type Item = i32;
}
```

The `Foo`

trait definition and the `impl Foo for i32`

are perfectly valid
Rust: we're kind of recursively using our `Foo`

impl in order to show that
the associated value indeed implements `Foo`

, but that's ok. But if we
translate this to our well-formedness setting, the compiler proof process
inside the `Foo`

impl is the following: it starts with proving that the
well-formedness goal `WellFormed(i32: Foo)`

is true. In order to do that,
it must prove the following goals: `Implemented(i32: Foo)`

and
`WellFormed(<i32 as Foo>::Item: Foo)`

. `Implemented(i32: Foo)`

holds because
there is our impl and there are no where clauses on it so it's always true.
However, because of the associated type value we used,
`WellFormed(<i32 as Foo>::Item: Foo)`

simplifies to just
`WellFormed(i32: Foo)`

. So in order to prove its original goal
`WellFormed(i32: Foo)`

, the compiler needs to prove `WellFormed(i32: Foo)`

:
this clearly is a cycle and cycles are usually rejected by the trait solver,
unless... if the `WellFormed`

predicate was made to be co-inductive.

A co-inductive predicate, as discussed in the chapter on
goals and clauses, are predicates
for which the
trait solver accepts cycles. In our setting, this would be a valid thing to do:
indeed, the `WellFormed`

predicate just serves as a way of enumerating all
the implied bounds. Hence, it's like a fixed point algorithm: it tries to grow
the set of implied bounds until there is nothing more to add. Here, a cycle
in the chain of `WellFormed`

predicates just means that there is no more bounds
to add in that direction, so we can just accept this cycle and focus on other
directions. It's easy to prove that under these co-inductive semantics, we
are effectively visiting all the transitive implied bounds, and only these.

## Implied bounds on types

We mainly talked about implied bounds for traits, but implied bounds on types are very similar. Suppose we have the following definition:

```
struct Type<...> where WC1, ..., WCn {
...
}
```

To prove that `Type<...>`

is well-formed, we would need to prove a goal of the
form `WellFormed(Type<...>).`

. The `WellFormed(Type<...>)`

predicate is defined
by the rule:

```
forall<...> {
WellFormed(Type<...>) :- WellFormed(WC1), ..., WellFormed(WCn).
}
```

Conversely, if we know a type is well-formed from our environment (for example because it appears as an argument of one of our functions), we can have implied bounds thanks to the below set of rules:

```
forall<...> {
FromEnv(WC1) :- FromEnv(Type<...>).
...
FromEnv(WCn) :- FromEnv(Type<...>).
}
```

Looking at the above rules, we see that we can never encounter a chain of
deductions of the form `WellFormed(Type<...>) :- ... :- WellFormed(Type<...>)`

.
So in contrast with traits, the `WellFormed(Type<...>)`

predicate does not need
to be co-inductive.