While on vacation, I’ve been working on an alternate type inference scheme for rustc. (Actually, I got it 99% working on the plane, and have been slowly poking at it ever since.) This scheme simplifies the code of the type inferencer dramatically and (I think) helps to meet our intutions (as I will explain). It is however somewhat less flexible than the existing inference scheme, though all of rustc and all the libraries compile without any changes. The scheme will (I believe) make it much simpler to implement to proper one-way matching for traits (explained later).

*Note:* Changing the type inference scheme doesn’t really mean much to
end users. Roughly the same set of Rust code still compiles. So this
post is really mostly of interest to rustc implementors.

### The new scheme in a nutshell

The new scheme is fairly simple. It is based on the observation that
most subtyping in Rust arises from lifetimes (though the scheme is
extensible to other possible kinds of subtyping, e.g. virtual
structs). It abandons unification and the H-M infrastructure and takes
a different approach: when a type variable `V`

is first related to
some type `T`

, we don’t set the value of `V`

to `T`

directly. Instead,
we say that `V`

is equal to some type `U`

where `U`

is derived by
replacing all lifetimes in `T`

with lifetime variables. We then relate
`T`

and `U`

appropriately.

Let me give an example. Here are two variables whose type must be inferred:

```
'a: { // 'a --> name of block's lifetime
let x = 3;
let y = &x;
...
}
```

Let’s say that the type of `x`

is `$X`

and the type of `y`

is `$Y`

,
where `$X`

and `$Y`

are both inference variables. In that case, the
first assignment generates the constraint that `int <: $X`

and the
second generates the constraint that `&'a $X <: $Y`

. To resolve the
first constraint, we would set `$X`

directly to `int`

. This is because
there are no lifetimes in the type `int`

. To resolve the second
constraint, we would set `$Y`

to `&'0 int`

– here `'0`

represents a
fresh lifetime variable. We would then say that `&'a int <: &'0 int`

,
which in turn implies that `'0 <= 'a`

. After lifetime inference is
complete, the types of `x`

and `y`

would be `int`

and `&'a int`

as
expected.

Without unification, you might wonder what happens when two type variables are related that have not yet been associated with any concrete type. This is actually somewhat challenging to engineer, but it certainly does happen. For example, there might be some code like:

```
let mut x; // type: $X
let mut y = None; // type: Option<$0>
loop {
if y.is_some() {
x = y.unwrap();
...
}
...
}
```

Here, at the point where we process `x = y.unwrap()`

, we do not yet
know the values of either `$X`

or `$0`

. We can say that the type of
`y.unwrap()`

will be `$0`

but we must now process the constrint that
`$0 <: $X`

. We do this by simply keeping a list of outstanding
constraints. So neither `$0`

nor `$X`

would (yet) be assigned a
specific type, but we’d remember that they were related. Then, later,
when either `$0`

or `$X`

*is* set to some specific type `T`

, we can go
ahead and instantiate the other with `U`

, where `U`

is again derived
from `T`

by replacing all lifetimes with lifetime variables. Then we
can relate `T`

and `U`

appropriately.

If we wanted to extend the scheme to handle more kinds of inference beyond lifetimes, it can be done by adding new kinds of inference variables. For example, if we wanted to support subtyping between structs, we might add struct variables.

### What advantages does this scheme have to offer?

The primary advantage of this scheme is that it is easier to think
about for us compiler engineers. Every type variable is either *set*
– in which case its type is known precisely – or *unset* – in which
case its type is not known at all. In the current scheme, we track a
lower- and upper-bound over time. This makes it hard to know just how
much is really known about a type. Certainly I know that when I think
about inference I still think of the state of a variable as a binary
thing, even though I know that really it’s something which evolves.

What prompted me to consider this redesign was the need to support
*one-way matching* as part of trait resolution. One-way matching is
basically a way of saying: is there any substitution `S`

such that ```
T
<: S(U)
```

(whereas normal matching searches for a substitution applied
to both sides, like `S(T) <: S(U)`

).

One-way matching is very complicated to support in the current
inference scheme: after all, if there are type variables that appear
in `T`

or `U`

which are partially constrained, we only know *bounds*
on their eventual type. In practice, these bounds actually tell us a
lot: for example, if a type variable has a lower bound of `int`

, it
actually tells us that the type variable *is* `int`

, since in Rust’s
type system there are no super- of sub-types of `int`

. However,
encoding this sort of knowledge is rather complex – and ultimately
amounts to precisely the same thing as this *new* inference scheme.

Another advantage is that there are various places in the Rust’s type
checker whether we query the current state of a type variable and make
decisions as a result. For example, when processing `*x`

, if the type
of `x`

is a type variable `T`

, we would want to know the current state
of `T`

– is `T`

known to be something inherent derefable (like `&U`

or `&mut U`

) or a struct that must implement the `Deref`

trait? The
current APIs for doing this bother me because they expose the bounds
of `U`

– but those bounds can change over time. This seems risky

to
me, since it’s only sound for us to examine those bounds if we either
(a) freeze the type of `T`

or (b) are certain that we examine
properties of the bound that will not change. This problem does not
exist in the new inference scheme: anything that might change over
time is abstracted into a new inference variable of its own.

### What are the disadvantages?

One form of subtyping that exists in Rust is not amenable to this
inference. It has to do with universal quantification and function
types. Function types that are more polymorphic

can be subtypes of
functions that are less polymorphic

. For example, if I have a
function type like `<'a> fn(&'a T) -> &'a uint`

, this indicates a
function that takes a reference to `T`

with any lifetime `'a`

and
returns a reference to a uint with that same lifetime. This is a
*subtype* of the function type `fn(&'b T) -> &'b uint`

. While these
two function types look similar, they are quite different: the former
accepts a reference with *any* lifetime but the latter accepts only a
reference with the specific lifetime `'b`

.

What this means is that today if you have a variable that is assigned many times from functions with varying amounts of polymorphism, we will generally infer its type correctly:

```
fn example<'b>(..) {
let foo: <'a> |&'a T| -> &'a int = ...;
let bar: |&'b T| -> &'b int = ...;
let mut v;
v = foo;
v = bar;
// type of v is inferred to be |&'b T| -> &'b int
}
```

However, this will not work in the newer scheme. Type ascription of some form would be required. As you can imagine, this is not a very .common problem, and it did not arise in any existing code.

(I believe that there are situations which the newer scheme infers correct types and the older scheme will fail to compile; however, I was unable to come up with a good example.)

### How does it perform?

I haven’t done extensive measurements. The newer scheme creates a lot of region variables. It seems to perform roughly the same as the older scheme, perhaps a bit slower – optimizing region inference may be able to help.