Rust 108 🦀 Mid-Level Intermediate Representation (MIR) Analysis and Borrow Checker Mechanics
The borrow checker does not run on the HIR. It runs on the MIR, a representation that is small enough, explicit enough, and control-flow-based enough to make the borrow checker’s analysis tractable. The MIR is the compiler’s last representation before code generation, and the borrow checker’s phases—dataflow, region inference, and the final error walk—operate on a local copy of it that has been rewritten to expose the lifetimes the checker needs to solve .
This chapter covers the MIR-based borrow checker as it exists in the rustc_borrowck crate. It begins with the reasons the checker moved from the HIR to the MIR—desugaring and non-lexical lifetimes—and the phases that constitute the mir_borrowck query. It then addresses the region uniquification that the MIR type-checker performs to accumulate lifetime constraints, and the move-path analysis that tracks initialization at field granularity. The final sections cover Polonius, the improved borrow checker that resolves the limitations of the current NLL analysis, and the diagnostics that the final error walk produces.
Key point: The borrow checker does not prove that your code is correct. It proves that your code does not violate a specific set of ownership and borrowing rules. The MIR is the representation where those rules are expressible as dataflow and region constraints.
Why the borrow checker runs on the MIR
The desugaring advantage. The HIR still contains the surface syntax that the user wrote. The MIR is radically desugared: for loops, if let, and other constructs are gone, and the control-flow graph is explicit. This simplicity is what the Rust compiler development guide calls the “radical desugaring” that helps prevent bugs in the borrow checker . A checker that operates on a simpler representation has fewer cases to handle and fewer opportunities for unsoundness.
The non-lexical lifetime requirement. The older HIR-based borrow checker used lexical scopes: a borrow lived until the end of the block in which it was created. The MIR-based checker uses non-lexical lifetimes (NLL), which are regions derived from the control-flow graph . A borrow’s lifetime is the set of program points where the borrow may still be used, not the syntactic block that contains it. This is the change that made patterns like conditional borrows and early returns with live references practical.
The move-path granularity. The borrow checker does not track initialization at the level of local variables. It tracks it at the level of move paths, which represent locations that can be initialized, moved, or borrowed. A move path for a and a move path for a.0 are distinct, and the analysis tracks each independently . This granularity is what allows partial moves and field-level initialization to be checked correctly.
The type-check accumulation. The borrow checker needs lifetime constraints, and those constraints come from a second type-checking pass over the MIR. The HIR type-check infers lifetimes, but the MIR type-check erases them and replaces them with fresh inference variables, a process called region uniquification . The purpose is to collect the constraints between regions that the borrow checker will then solve.
a. The phases of the borrow checker
The mir_borrowck query is the entry point, and its phases are documented in the compiler development guide . The sequence is:
- Create a local copy of the MIR. The checker modifies this copy in place, rewriting types and regions to include the inference variables it needs.
- Replace regions in the MIR.
replace_regions_in_mirreplaces every region with a fresh inference variable . - Run dataflow analyses. These compute what data is moved and when, and what borrows are in scope at each program point.
- Perform a second type check. This pass determines all the constraints between different regions .
- Perform region inference. This computes the value of each region—the program points where each lifetime must be valid, according to the constraints .
- Compute borrows in scope. At this point, the checker knows which borrows are live at each point.
- Walk the MIR and report errors. The final walk checks that variables are initialized, that moves do not conflict with borrows, and that mutable access does not overlap with shared access .
The dataflow analyses and the region inference are the computationally heavy parts. The final error walk is where the diagnostics are produced.
b. Region uniquification and user type annotations
The MIR type-checker erases the lifetimes that the HIR inferred and replaces them with fresh, unconstrained inference variables . This is necessary because the borrow checker needs to solve for the lifetimes from scratch, using only the constraints that the MIR exposes. If the HIR’s inferred lifetimes were kept, the borrow checker would be solving a problem that has already been partially solved, and the results would be inconsistent.
The danger of erasing lifetimes is that user-written type annotations can be lost. The HIR type-checker remembers explicit type ascriptions and explicit generic arguments as canonical user type annotations . These are stored in a form that does not depend on the HIR’s inference variables, and the MIR type-checker uses them to constrain the new inference variables. Without this mechanism, a program like let y: &'static u32 = x; would be accepted even when x does not live for 'static, because the erased lifetime would no longer record the user’s intent .
The StatementKind::AscribeUserType in the MIR is the mechanism for constraining the type of a scrutinee expression. The user type is not used directly; it is related to the actual inferred type, and the regions in the actual type are replaced with new inference variables . This is how the borrow checker gets the region constraints that the user’s annotations imply.
c. Move paths and Polonius
The move-path analysis tracks initialization and moves at field granularity. A MovePath represents a location that can be initialized, moved, or borrowed, and the analysis builds a tree of these paths . The tree is indexed by MovePathIndex, and the MoveData structure stores the paths and their relationships. Illegal move paths—paths that cannot be moved from, such as an element of an array or the contents of a borrowed reference—are not created, which reduces the analysis’s overhead .
Polonius is the next-generation borrow checker. The current NLL analysis has known limitations, most notably the “NLL problem case 3” and lending iterator patterns . The Polonius alpha analysis resolves these cases by using a more precise formulation of the borrow-checking problem, based on reachability in a constraint graph rather than the NLL approximation. The alpha analysis is implemented on nightly, passes performance and crater runs, and is targeted for stabilization . The remaining work includes fixing a soundness issue related to opaque types and dead regions, expanding test coverage, and validating performance on real-world code.
The Polonius approach changes the analysis from “compute the lifetimes and check the constraints” to “compute the set of loans that may reach each program point, and check that no conflicting loan is live at the same point” . This is more precise, and it accepts more programs, but it is also more expensive. The performance target is a 10–20% cost for the benefit of the additional expressiveness .
Complete Example Session
// ============================================
// PART 1: THE BORROW CHECK QUERY
// ============================================
// The entry point is mir_borrowck.
// It runs on a local copy of the MIR.
// fn mir_borrowck(tcx, def_id) -> BorrowCheckResult
// // Create local MIR copy
// // replace_regions_in_mir
// // dataflow analyses
// // MIR type check (constraints)
// // region inference
// // borrows in scope
// // error walk
// ============================================
// PART 2: THE MOVE PATH
// ============================================
// Initialization is tracked at field granularity.
// For a local `a: (String, String)`:
// MovePath(a) — the whole tuple
// MovePath(a.0) — the first field
// MovePath(a.1) — the second field
// Moving a.0 does not move a.1.
// The analysis tracks each independently.
// ============================================
// PART 3: ILLEGAL MOVE PATHS
// ============================================
// Not every Place gets a move path.
// let foo: [String; 3];
// foo[1] is not a move path — arrays are not
// movable element-by-element.
// let bar: &String;
// *bar is not a move path — borrowed data
// cannot be moved out.
// ============================================
// PART 4: REGION UNIQUIFICATION
// ============================================
// The MIR type-checker erases HIR lifetimes
// and replaces them with fresh inference variables.
// fn foo<'a>(x: &'a u32) {
// let y: &'static u32 = x; // ERROR
// }
// The user annotation `&'static u32` is preserved
// as a canonical user type, so the constraint
// `'a: 'static` is recorded and the error is reported.
// ============================================
// PART 5: NON-LEXICAL LIFETIMES
// ============================================
// The lifetime of a borrow is the set of points
// where it is live, not the syntactic block.
// let mut x = 0;
// let r = &x;
// println!("{}", r); // r is live here
// x = 1; // OK: r is dead after the println
// The borrow of x ends after its last use,
// not at the end of the block.
// ============================================
// PART 6: THE DATAFLOW ANALYSES
// ============================================
// Computes moves, initializations, and borrows
// at each program point.
// The result is a set of facts:
// - which move paths are moved at which points
// - which move paths are initialized at which points
// - which borrows are in scope at which points
// ============================================
// PART 7: REGION INFERENCE
// ============================================
// Solves for the value of each region.
// The value is the set of program points where
// the lifetime must be valid.
// The constraints come from the MIR type check.
// The solution is a set of points per region.
// ============================================
// PART 8: THE ERROR WALK
// ============================================
// The final pass checks each access against
// the computed facts.
// If a statement reads a place:
// - is the place initialized?
// - is it mutably borrowed?
// If a statement writes a place:
// - is it shared-borrowed?
// If a statement moves a place:
// - is it borrowed at all?
// ============================================
// PART 9: POLONIUS
// ============================================
// The improved analysis.
// Resolves NLL problem case 3 and lending iterators.
// Alpha is on nightly; stabilization is targeted.
// ============================================
// PART 10: THE FULL PICTURE
// ============================================
// MIR is the representation the borrow checker
// needs. The phases are: replace regions,
// dataflow, type check, region inference,
// compute borrows, error walk.
// The result is a proof that the program does not
// violate the ownership and borrowing rules.The ten parts build a conceptual view of the MIR borrow checker: the query, the move paths, region uniquification, non-lexical lifetimes, the dataflow, region inference, the error walk, and Polonius. The pattern is consistent: the MIR exposes the control flow and the regions, and the checker solves the constraints and reports the violations.
Quick Reference
Borrow Checker Phases
| Phase | Purpose |
|---|---|
| Local MIR copy | Isolate the analysis |
replace_regions_in_mir | Replace regions with inference vars |
| Dataflow | Track moves, inits, borrows |
| MIR type check | Collect region constraints |
| Region inference | Solve for region values |
| Borrows in scope | Compute live borrows per point |
| Error walk | Check accesses, report errors |
Move Path Rules
| Place | Move Path? | Reason |
|---|---|---|
a | Yes | Local variable |
a.0 | Yes | Field |
arr[1] | No | Array element not movable |
*ref | No | Cannot move out of borrow |
NLL vs Polonius
| Aspect | NLL | Polonius |
|---|---|---|
| Status | Stable | Alpha, nightly |
| Precision | Conservative | More precise |
| Problem case 3 | Rejected | Accepted |
| Lending iterators | Rejected | Accepted |
| Performance | Baseline | 10–20% cost |
Key Types
| Type | Purpose |
|---|---|
MovePathIndex | Index into move path vector |
MoveData | Stores move paths and facts |
RegionVid | Region inference variable |
BorrowCheckResult | Output of mir_borrowck |
Best Practices
✅ Do This:
// Let the borrow checker see the MIR-level facts.
// Write code that the MIR can analyze precisely.
let r = &x; // ✅
println!("{}", r); // last use
x = 1; // OK: borrow ended
// Use field-level moves when appropriate.
let (a, b) = tuple; // ✅❌ Don’t Do This:
// Don't assume lexical scope determines borrow lifetime.
let r = &x;
x = 1; // ❌ if r is used after
println!("{}", r);
// Don't expect Polonius-level precision from NLL.
// Lending iterators require Polonius. // ❌Common Pitfalls
| Pitfall | Why It Happens | Fix |
|---|---|---|
| NLL problem case 3 | Conditional return of borrow | Polonius (nightly) or restructure |
| Lending iterator rejected | next(&mut self) reborrows | Polonius (nightly) |
| Move path conflict | Partial move then use whole | Use fields independently |
| Region inference error | User annotation conflicts | Check the explicit type |
Real-World Examples
1. Move Path
// MovePath(a) and MovePath(a.0) are distinct.2. NLL
let r = &x;
println!("{}", r); // r live here
x = 1; // OK3. Region Uniquification
// HIR lifetimes erased, MIR inference vars created.4. User Type Annotation
let y: &'static u32 = x; // constraint recorded5. Polonius Alpha
// On nightly; accepts more programs.6. Dataflow
// Computes moves, inits, borrows per point.7. Region Inference
// Solves for lifetime validity points.8. Error Walk
// Checks each access against computed facts.9. MIR Copy
// The checker modifies a local copy.10. Borrows in Scope
// Live borrows at each program point.Visual
The Borrow Check Pipeline
┌─────────────────────────────────────────────────────────┐
│ MIR (from HIR lowering) │
│ │ │
│ ▼ local copy │
│ WORKING MIR │
│ │ │
│ ▼ replace_regions_in_mir │
│ FRESH REGION VARS │
│ │ │
│ ▼ dataflow │
│ MOVES, INITS, BORROWS │
│ │ │
│ ▼ MIR type check │
│ REGION CONSTRAINTS │
│ │ │
│ ▼ region inference │
│ REGION VALUES (points) │
│ │ │
│ ▼ borrows in scope │
│ LIVE BORROWS PER POINT │
│ │ │
│ ▼ error walk │
│ DIAGNOSTICS │
└─────────────────────────────────────────────────────────┘Move Path Tree
┌─────────────────────────────────────────────────────────┐
│ a: (String, String) │
│ │ │
│ ┌────┴────┐ │
│ ▼ ▼ │
│ a.0 a.1 │
│ (move (move │
│ path) path) │
│ │
│ MovePath(a) is the parent. │
│ Moving a.0 does not move a.1. │
│ Each is tracked independently. │
└─────────────────────────────────────────────────────────┘Non-Lexical Lifetimes
┌─────────────────────────────────────────────────────────┐
│ let mut x = 0; │
│ let r = &x; ← borrow created │
│ println!("{}", r); ← borrow live │
│ x = 1; ← borrow dead, write OK │
│ │
│ The borrow ends after the last use, │
│ not at the end of the block. │
└─────────────────────────────────────────────────────────┘Polonius vs NLL
┌─────────────────────────────────────────────────────────┐
│ NLL (stable) │
│ Computes region values, checks constraints. │
│ Conservative: rejects some valid programs. │
│ │
│ POLONIUS (alpha, nightly) │
│ Computes loan reachability in a constraint graph. │
│ More precise: accepts more valid programs. │
│ Cost: 10–20% performance overhead. │
└─────────────────────────────────────────────────────────┘Summary
| Item | Value |
|---|---|
| Crate | rustc_borrowck |
| Query | mir_borrowck |
| Representation | MIR (desugared, control-flow graph) |
| Key phases | Dataflow, region inference, error walk |
| Move tracking | Move paths, field granularity |
| Lifetime model | Non-lexical (NLL) |
| Region uniquification | Erase HIR lifetimes, infer fresh |
| Polonius | Improved analysis, alpha on nightly |
| User annotations | Canonical user types preserve intent |
Key takeaways:
- The borrow checker runs on the MIR because the MIR is simpler. The radical desugaring removes the syntax that the checker does not need, and the control-flow graph makes non-lexical lifetimes possible .
- Region uniquification is the bridge between HIR and MIR lifetimes. The HIR’s inferred lifetimes are erased, and fresh inference variables are created. User type annotations are preserved as canonical types so that the user’s intent is not lost .
- Move paths track initialization at field granularity. A move path exists for a local and for each movable field. Array elements and borrowed data do not get move paths, because they cannot be moved .
- The phases are sequential and dependent. Dataflow feeds the MIR type check, which feeds region inference, which feeds the borrows-in-scope computation, which feeds the error walk .
- Polonius is the next generation. It resolves the NLL limitations—problem case 3 and lending iterators—by using a more precise formulation. The alpha is on nightly, and stabilization is targeted .
- The checker proves the absence of violations, not the presence of correctness. It checks that variables are initialized, that moves do not conflict with borrows, and that mutable and shared access do not overlap. It does not prove that the program does what the programmer intended.
Remember: The borrow checker is a dataflow and constraint solver that operates on the MIR. It creates a local copy of the representation, replaces the regions with inference variables, computes the moves and borrows, solves for the lifetimes, and walks the MIR to check the accesses. The result is a proof that the program does not violate the ownership rules. Polonius improves the precision of that proof, at a performance cost. The MIR is the representation that makes the proof tractable, and the phases are the steps that make it possible.
Stop using slow, ad-bloated tool sites! 🤮
🔎 Search “KandZ Tools” on Google to use many professional utilities for free.
KandZ.me is the ultimate minimalist hub for:
✅ Finance (Mortgage, Interest, Inflation)
✅ Tech (Base64, JSON, Dev Suite, IP)
✅ Health (BMI, BMR, TDEE)
✅ Productivity (Timer, Workspace, QR)
⚡️ Fast & Private
🔒 No data leaves your device
💎 100% Free
🔗 Use it now: https://tools.kandz.me
🔖 Bookmark it—you’ll need it later!