Type equality and unification
This section covers how the trait system handles equality between associated types. The full system consists of several moving parts, which we will introduce one by one:
- Projection and the
Normalize
predicate - Placeholder associated type projections
- The
AliasEq
predicate - Integration with unification
Associated type projection and normalization
When a trait defines an associated type (e.g.,
the Item
type in the IntoIterator
trait), that
type can be referenced by the user using an associated type
projection like <Option<u32> as IntoIterator>::Item
.
Often, people will use the shorthand syntax
T::Item
. Presently, that syntax is expanded during "type collection" into the explicit form, though that is something we may want to change in the future.
In some cases, associated type projections can be normalized –
that is, simplified – based on the types given in an impl. So, to
continue with our example, the impl of IntoIterator
for Option<T>
declares (among other things) that Item = T
:
impl<T> IntoIterator for Option<T> {
type Item = T;
...
}
This means we can normalize the projection <Option<u32> as IntoIterator>::Item
to just u32
.
In this case, the projection was a "monomorphic" one – that is, it did not have any type parameters. Monomorphic projections are special because they can always be fully normalized.
Often, we can normalize other associated type projections as well. For
example, <Option<?T> as IntoIterator>::Item
, where ?T
is an inference
variable, can be normalized to just ?T
.
In our logic, normalization is defined by a predicate
Normalize
. The Normalize
clauses arise only from
impls. For example, the impl
of IntoIterator
for Option<T>
that
we saw above would be lowered to a program clause like so:
forall<T> {
Normalize(<Option<T> as IntoIterator>::Item -> T) :-
Implemented(Option<T>: IntoIterator)
}
where in this case, the one Implemented
condition is always true.
Since we do not permit quantification over traits, this is really more like a family of program clauses, one for each associated type.
We could apply that rule to normalize either of the examples that we've seen so far.
Placeholder associated types
Sometimes however we want to work with associated types that cannot be normalized. For example, consider this function:
fn foo<T: IntoIterator>(...) { ... }
In this context, how would we normalize the type T::Item
?
Without knowing what T
is, we can't really do so. To represent this case,
we introduce a type called a placeholder associated type projection. This
is written like so: (IntoIterator::Item)<T>
.
You may note that it looks a lot like a regular type (e.g., Option<T>
),
except that the "name" of the type is (IntoIterator::Item)
. This is not an
accident: placeholder associated type projections work just like ordinary
types like Vec<T>
when it comes to unification. That is, they are only
considered equal if (a) they are both references to the same associated type,
like IntoIterator::Item
and (b) their type arguments are equal.
Placeholder associated types are never written directly by the user. They are used internally by the trait system only, as we will see shortly.
In rustc, they correspond to the TyKind::UnnormalizedProjectionTy
enum
variant, declared in compiler/rustc_middle/src/ty/sty.rs
. In chalk, we use an
AssociatedType
.
Projection equality
So far we have seen two ways to answer the question of "When can we consider an associated type projection equal to another type?":
- the
Normalize
predicate could be used to transform projections when we knew which impl applied; - placeholder associated types can be used when we don't. This is also known as lazy normalization.
These two cases are brought together by the AliasEq
predicate introduced
before (where the AliasTy
is Projection
). The instantiated predicate for projection
equality looks then like so:
AliasEq(<T as IntoIterator>::Item = U)
and we will see that it can be proven either via normalization or
via the placeholder type. As part of lowering an associated type declaration from
some trait, we create two program clauses for AliasEq
:
forall<T, U> {
AliasEq(<T as IntoIterator>::Item = U) :-
Normalize(<T as IntoIterator>::Item -> U)
}
forall<T> {
AliasEq(<T as IntoIterator>::Item = (IntoIterator::Item)<T>)
}
These are the only two AliasEq
program clauses we ever make for
any given associated item.
Integration with unification
Now we are ready to discuss how associated type equality integrates with unification. As described in the type inference section, unification is basically a procedure with a signature like this:
Unify(A, B) = Result<Subgoals, NoSolution>
In other words, we try to unify two things A and B. That procedure
might just fail, in which case we get back Err(NoSolution)
. This
would happen, for example, if we tried to unify u32
and i32
.
The key point is that, on success, unification can also give back to us a set of subgoals that still remain to be proven.
Whenever unification encounters a non-placeholder associated type
projection P being equated with some other type T, it always succeeds,
but it produces a subgoal AliasEq(P = T)
that is propagated
back up. Thus it falls to the ordinary workings of the trait system
to process that constraint.
If we unify two projections P1 and P2, then unification produces a variable X and asks us to prove that
AliasEq(P1 = X)
andAliasEq(P2 = X)
. (That used to be needed in an older system to prevent cycles; I rather doubt it still is. -nmatsakis)