22. Borrow Checker: Diagnostics & Errors

The Non-Lexical Lifetimes (NLL) architecture distills borrow checking down to five specific error codes. By maintaining CFG tracking and routing conflicts through the Z3 solver, the compiler can map structural violations directly to errors.

E001: Use of Moved Value

Triggered when a variable is read or written to after a move or reassignment.

p = [1, 2, 3]
q = p
print(p)   
# E001: `p` was moved to `q` on line 2; cannot use `p` here

E002: Conflicting Borrow

Triggered when the Z3 solver returns SAT for overlapping active loans where at least one of the active borrows is a mutable borrow (ActiveMut). Because of NLL, this only triggers if the overlapping loans are genuinely active simultaneously at a specific CFG node.

p = [1, 2, 3]
m = mut ref p
r = ref p
m.append(4)  # Conflict point
print(r[0])
# E002: cannot borrow `p` as mutable because it is also borrowed as immutable by `r`

Note on Disjoint Fields: Borrows on disjoint fields of the same struct (e.g., mut ref p.x and mut ref p.y) do not trigger E002, as the overlap() structural predicate guarantees their memory paths are distinct.

E003: Move While Borrowed

Triggered when a reassignment or move is attempted on a place that currently has an active loan. This generates a loan_killed_at fact that conflicts with the computed liveness range.

p = [1, 2, 3]
r = ref p
q = p        # E003: cannot move `p` while borrowed by `r`
print(r[0])

E004: Borrow Escapes its Scope

While borrows are not strictly bound to lexical blocks, this error triggers if a reference outlives the original owner’s allocation (e.g., returning a reference to a local variable).

def get_ref():
    p = [1, 2, 3]
    return ref p
# E004: `p` does not live long enough to be borrowed here

E005: Use of Uninitialized Variable

Triggered by the forward dataflow analysis when a CFG node reads a variable whose state is strictly uninitialized.

# Assuming `p` is declared but not assigned
print(p)
# E005: `p` is used before being initialized