Issue #1208: A part of ref mut self, or an element of a mut list, handed to a keeper: NK1131 says “only borrows self”, and on an element rustc refuses it (E0507)

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 (a watch list or a trail taken out and given back). Probed on target/fast/nikaia at 31e2ea7, language 0.0.1341.

Part I 6.5 and ADR-views-1 D1 (#949): a part of a mut parameter handed to something that keeps it is taken, and assigning the part gives it back; “ref mut self is such a parameter too”. #949 built this for a let mut view; two neighbours are not covered.

Probe 1: a field of ref mut self

struct S { trail: Vec[u32], saved: Vec[Vec[u32]] }
fn keep_all(ws: Vec[u32]) -> Vec[u32] { return ws }
impl S {
    fn stash(ref mut self) {
        let t = keep_all(self.trail)
        self.trail = []
        self.saved.push(t)
    }
}
fn main() {
    let mut s = S { trail: [1, 2], saved: [] }
    s.stash()
    println(f"{s.trail.len()} {s.saved[0].len()}")
}

Refused with NK1131: You can’t give away self.trail here: this method only borrows self, with the note ref self borrows the value. The method takes ref mut self; the message is wrong as well as the refusal. Expected: 0 1.

Probe 2: an element of a mut list parameter

fn keep_all(ws: Vec[u32]) -> Vec[u32] { return ws }
fn stash(mut w: Vec[Vec[u32]], mut saved: Vec[Vec[u32]]) {
    let t = keep_all(w[1])
    w[1] = []
    saved.push(t)
}
fn main() {
    let mut w: Vec[Vec[u32]] = [[], [1, 2]]
    let mut saved: Vec[Vec[u32]] = []
    stash(w, saved)
    println(f"{w[1].len()} {saved[0].len()}")
}

nikaia check accepts it; nikaia run fails in rustc: Cannot move out of a shared reference. Expected: 0 1. The same on self.watches[lit] in a ref mut self method.

To build

1. Tests tests/compiler/tests/a_field_of_ref_mut_self_handed_to_a_keeper_is_taken.nika and tests/compiler/tests/an_element_of_a_mut_list_handed_to_a_keeper_is_taken.nika, each with the probe and 0 1 as its .stdout; plus a .stderr case each where the part is not given back before the way out (NK2108, ADR-views-1 D2).
2. Apply D1-D3 to a field of ref mut self and to an indexed element (w[i], self.w[i]) of a mut place: lowered std::mem::take(&mut place) (or mem::replace with D3’s stand-in).
3. NK1131 on ref mut self names ref mut self, not ref self, where it still applies (the whole self given away).

Related: #979 (D6, a let over the part that is kept later), which meets the same receiver.

Back to Open Issues