Type Unification

Type unification is the algorithm used by rustc's type checker (rustc_infer) to solve systems of type equality constraints ($T_1 = T_2$), substituting unknown inference variables (?T, ?Int, ?Float) with concrete types until every expression has a single, consistent type—or reporting a type error if two incompatible types are forced to unify.

How Unification Solves Inference Variables Step by Step

When type-checking a function body, the compiler assigns a fresh inference variable (?0, ?1, ...) to every unannotated binding and generic type parameter, collects equality constraints from operations, and unifies them:

Code:
    let mut v = Vec::new();      // 1. v: Vec<?0>
    let x = 42;                  // 2. x: ?1 (integer variable)
    v.push(x);                   // 3. Unifies Vec<?0>::push(?0) with x: ?1  ==>  ?0 = ?1
    let slice: &[u64] = &v;      // 4. Unifies &Vec<?0> -> &[?0] with &[u64] ==>  ?0 = u64
                                 // 5. By transitivity (?1 = ?0 = u64), both `x` and `v` resolve!
                                 //    v: Vec<u64>, x: u64

fn main() {
    let mut v = Vec::new();
    let x = 42;
    v.push(x);

    // Unifying `&v` with `&[u64]` resolves `?0 = u64` and `x: u64`:
    let slice: &[u64] = &v;
    println!("Resolved slice: {slice:?} (elem size = {} bytes)", size_of_val(&x));
}

Resolved slice: [42] (elem size = 8 bytes)

Structural Decomposition During Unification

When unifying two compound types (such as Result<?A, String> and Result<i32, ?B>), the unification engine checks that the outer type constructors match (Result == Result) and recursively unifies their corresponding type arguments:

• ?A unifies with i32 ($\implies ?A = \text{i32}$)
• String unifies with ?B ($\implies ?B = \text{String}$)
• Resulting unified type: Result<i32, String>

fn operation(succeed: bool) -> Result<i32, String> {
    if succeed {
        // `Ok(10)` has type `Result<i32, ?E>` -> unifies with return type (`?E = String`)
        Ok(10)
    } else {
        // `Err(...)` has type `Result<?T, String>` -> unifies with return type (`?T = i32`)
        Err(String::from("failed"))
    }
}

fn main() {
    println!("{:?}, {:?}", operation(true), operation(false));
}

Ok(10), Err("failed")

Unification Failure and the "Occurs Check" (Infinite Types E0308)

Unification fails in two ways:

1. Constructor mismatch (E0308): Attempting to unify two different concrete types (such as ?0 = u32 from one line and ?0 = &str from another line).
2. Occurs check (infinite type): Attempting to unify an inference variable ?T with a type that contains ?T itself (such as ?T = Vec<?T>), which would require an infinitely nested type Vec<Vec<Vec<...>>>.