Goals and clauses
In logic programming terms, a goal is something that you must prove and a clause is something that you know is true. As described in the lowering to logic chapter, Rust's trait solver is based on an extension of hereditary harrop (HH) clauses, which extend traditional Prolog Horn clauses with a few new superpowers.
Goals and clauses meta structure
In Rust's solver, goals and clauses have the following forms (note that the two definitions reference one another):
Goal = DomainGoal // defined in the section below
| Goal && Goal
| Goal || Goal
| exists<K> { Goal } // existential quantification
| forall<K> { Goal } // universal quantification
| if (Clause) { Goal } // implication
| true // something that's trivially true
| ambiguous // something that's never provable
Clause = DomainGoal
| Clause :- Goal // if can prove Goal, then Clause is true
| Clause && Clause
| forall<K> { Clause }
K = <type> // a "kind"
| <lifetime>
The proof procedure for these sorts of goals is actually quite straightforward. Essentially, it's a form of depth-first search. The paper "A Proof Procedure for the Logic of Hereditary Harrop Formulas" gives the details.
In terms of code, these types are defined in
compiler/rustc_middle/src/traits/mod.rs
in rustc, and in
chalk-ir/src/lib.rs
in chalk.
Domain goals
Domain goals are the atoms of the trait logic. As can be seen in the definitions given above, general goals basically consist in a combination of domain goals.
Moreover, flattening a bit the definition of clauses given previously, one can see that clauses are always of the form:
forall<K1, ..., Kn> { DomainGoal :- Goal }
hence domain goals are in fact clauses' LHS. That is, at the most granular level, domain goals are what the trait solver will end up trying to prove.
To define the set of domain goals in our system, we need to first introduce a few simple formulations. A trait reference consists of the name of a trait along with a suitable set of inputs P0..Pn:
TraitRef = P0: TraitName<P1..Pn>
So, for example, u32: Display
is a trait reference, as is Vec<T>: IntoIterator
. Note that Rust surface syntax also permits some extra
things, like associated type bindings (Vec<T>: IntoIterator<Item = T>
), that are not part of a trait reference.
A projection consists of an associated item reference along with its inputs P0..Pm:
Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
Given these, we can define a DomainGoal
as follows:
DomainGoal = Holds(WhereClause)
| FromEnv(TraitRef)
| FromEnv(Type)
| WellFormed(TraitRef)
| WellFormed(Type)
| Normalize(Projection -> Type)
WhereClause = Implemented(TraitRef)
| AliasEq(Projection = Type)
| Outlives(Type: Region)
| Outlives(Region: Region)
WhereClause
refers to a where
clause that a Rust user would actually be able
to write in a Rust program. This abstraction exists only as a convenience as we
sometimes want to only deal with domain goals that are effectively writable in
Rust.
Let's break down each one of these, one-by-one.
Implemented(TraitRef)
e.g. Implemented(i32: Copy)
True if the given trait is implemented for the given input types and lifetimes.
AliasEq(Projection = Type)
e.g. AliasEq<T as Iterator>::Item = u8
The given associated type Projection
is equal to Type
; this can be proved
with either normalization or using placeholder associated types and is handled
as a special kind of type aliases. See
the section on associated types.
Normalize(Projection -> Type)
e.g. Normalize<T as Iterator>::Item -> u8
The given associated type Projection
can be normalized to Type
.
As discussed in the section on associated
types, Normalize
implies AliasEq
,
but not vice versa. In general, proving Normalize(<T as Trait>::Item -> U)
also requires proving Implemented(T: Trait)
.
FromEnv(TraitRef)
e.g. FromEnv(Self: Add<i32>)
True if the inner TraitRef
is assumed to be true,
that is, if it can be derived from the in-scope where clauses.
For example, given the following function:
#![allow(unused)] fn main() { fn loud_clone<T: Clone>(stuff: &T) -> T { println!("cloning!"); stuff.clone() } }
Inside the body of our function, we would have FromEnv(T: Clone)
. In-scope
where clauses nest, so a function body inside an impl body inherits the
impl body's where clauses, too.
This and the next rule are used to implement implied bounds. As we'll see
in the section on lowering, FromEnv(TraitRef)
implies Implemented(TraitRef)
,
but not vice versa. This distinction is crucial to implied bounds.
FromEnv(Type)
e.g. FromEnv(HashSet<K>)
True if the inner Type
is assumed to be well-formed, that is, if it is an
input type of a function or an impl.
For example, given the following code:
struct HashSet<K> where K: Hash { ... }
fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
println!("inserting!");
set.insert(item);
}
HashSet<K>
is an input type of the loud_insert
function. Hence, we assume it
to be well-formed, so we would have FromEnv(HashSet<K>)
inside the body of our
function. As we'll see in the section on lowering, FromEnv(HashSet<K>)
implies
Implemented(K: Hash)
because the
HashSet
declaration was written with a K: Hash
where clause. Hence, we don't
need to repeat that bound on the loud_insert
function: we rather automatically
assume that it is true.
WellFormed(Item)
These goals imply that the given item is well-formed.
We can talk about different types of items being well-formed:
-
Types, like
WellFormed(Vec<i32>)
, which is true in Rust, orWellFormed(Vec<str>)
, which is not (becausestr
is notSized
.) -
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.
Coinductive goals
Most goals in our system are "inductive". In an inductive goal, circular reasoning is disallowed. Consider this example clause:
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:
#![allow(unused)] fn main() { 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
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.