WellFormed, Outlives, Coinductive Goals, and Auto Traits

We can talk about different types of items being well-formed: * *Types*, like `WellFormed(Vec<i32>)`, which is true in Rust, or `WellFormed(Vec<str>)`, which is not (because `str` is not `Sized`.) * *TraitRefs*, like `WellFormed(Vec<i32>: Clone)`. Well-formedness is important to [implied bounds]. In particular, the reason it is okay to assume `FromEnv(T: Clone)` in the `loud_clone` example is that we _also_ verify `WellFormed(T: Clone)` for each call site of `loud_clone`. Similarly, it is okay to assume `FromEnv(HashSet<K>)` in the `loud_insert` example because we will verify `WellFormed(HashSet<K>)` for each call site of `loud_insert`. #### Outlives(Type: Region), Outlives(Region: Region) e.g. `Outlives(&'a str: 'b)`, `Outlives('a: 'static)` True if the given type or region on the left outlives the right-hand region. <a id="coinductive"></a> ## Coinductive goals Most goals in our system are "inductive". In an inductive goal, circular reasoning is disallowed. Consider this example clause: ```text Implemented(Foo: Bar) :- Implemented(Foo: Bar). ``` Considered inductively, this clause is useless: if we are trying to prove `Implemented(Foo: Bar)`, we would then recursively have to prove `Implemented(Foo: Bar)`, and that cycle would continue ad infinitum (the trait solver will terminate here, it would just consider that `Implemented(Foo: Bar)` is not known to be true). However, some goals are *co-inductive*. Simply put, this means that cycles are OK. So, if `Bar` were a co-inductive trait, then the rule above would be perfectly valid, and it would indicate that `Implemented(Foo: Bar)` is true. *Auto traits* are one example in Rust where co-inductive goals are used. Consider the `Send` trait, and imagine that we have this struct: ```rust struct Foo { next: Option<Box<Foo>> } ``` The default rules for auto traits say that `Foo` is `Send` if the types of its fields are `Send`. Therefore, we would have a rule like ```text Implemented(Foo: Send) :- Implemented(Option<Box<Foo>>: Send). ``` As you can probably imagine, proving that `Option<Box<Foo>>: Send` is going to wind up circularly requiring us to prove that `Foo: Send` again. So this would be an example where we wind up in a cycle – but that's ok, we *do* consider `Foo: Send` to hold, even though it references itself. In general, co-inductive traits are used in Rust trait solving when we want to enumerate a fixed set of possibilities. In the case of auto traits, we are enumerating the set of reachable types from a given starting point (i.e., `Foo` can reach values of type `Option<Box<Foo>>`, which implies it can reach values of type `Box<Foo>`, and then of type `Foo`, and then the cycle is complete). In addition to auto traits, `WellFormed` predicates are co-inductive. These are used to achieve a similar "enumerate all the cases" pattern, as described in the section on [implied bounds]. ## Incomplete chapter Some topics yet to be written: - Elaborate on the proof procedure - SLG solving – introduce negative reasoning

This section discusses `WellFormed(Item)` and its relation to implied bounds, followed by `Outlives`, indicating that a type or region outlives another region. It explains "coinductive" goals, where cycles are permitted (unlike inductive goals). Auto traits, such as `Send`, are examples where co-inductive goals are used to enumerate a fixed set of possibilities. `WellFormed` predicates are also co-inductive. The chapter is incomplete and will be extended.