Issue #1206: Lowering: an argument that reads the list whose element is changed (w[0].push(w[1][1])) is refused by rustc (E0502)

Open and answer this issue on GitHub.

ready · opened 2026-11-03 · updated 2026-11-03 · 0 comments

Found while probing the forms a CDCL(T) solver needs in Nikaia (ADR-270 D8 steps 3-5, D13; probed on target/fast/nikaia at 31e2ea7, language 0.0.1341).

Probe

fn main() {
    let mut w: Vec[Vec[u32]] = [[], [5, 6]]
    w[0].push(w[1][1])
    println(f"{w[0].len()} {w[0][0]}")
}

nikaia check accepts it; nikaia run fails in rustc: Cannot borrow w as immutable because it is also borrowed as mutable. Expected: 1 6.

The same happens on a field of ref mut self (self.w[a].push(self.w[b][1])), the form a watch list or an occurrence list takes in a solver. The argument is a u32 that copies, so nothing in Nikaia’s rules is in the way: the lowering hands w[0] to push as &mut before it evaluates w[1][1], and Rust’s two-phase borrows do not cover an IndexMut receiver.

To build

1. A test tests/compiler/tests/an_argument_reads_the_list_whose_element_it_changes.nika with the probe and 1 6 as its .stdout, and a second case on ref mut self (self.w[a].push(self.w[b][1])).
2. In the lowering of a method call whose receiver is a place reached through an index (IndexMut), evaluate every argument that reads the same root into a temporary before the receiver is borrowed (let __a = w[1][1]; w[0].push(__a);). Only where an argument reads the receiver’s root; elsewhere the emitted Rust stays as it is.

Back to Open Issues