False positive with usize cast from &mut [T; n] to &mut [T]

[nilehmann]

The following code fails to verify

pub fn test() -> [u8; 4] {
    let mut b = [1, 2, 3, 4];
    b.reverse();
    b
}

The problem is that the default signature we generate for reverse is fn(&mut ∃v. [T][v]) which cannot guarantee the length of the slice doesn't change (the length of a slice cannot change but the type can't guarantee it). Since we are casting &mut [T; n] to &mut [T][n] the call to reverse fails because &mut [T][n] is not a subtype of &mut ∃v. [T][v].

[ranjitjhala]

(editing title as FP is more commonly used for things that are safe but reported as unsafe; FN would be if we missed a bug...)