Missing (polymorphic) refinements for vec set/get

[ranjitjhala]

The following should pass but do not.

#![feature(allocator_api)]
#![feature(associated_type_bounds)]

use std::ops::Index;

#[path = "../lib/vec.rs"]
mod vec;

#[flux::sig(fn(xs: &Vec<i32{v: v > 55}>[100]) -> i32{v:v > 55})]
fn test_get(xs: &Vec<i32>) -> i32 {
    xs[0]
}

#[flux::sig(fn(xs: &mut Vec<i32{v: v > 55}>[100]) )]
fn test_set(xs: &mut Vec<i32>)  {
    xs[0] = 66
}

[nilehmann]

Did some digging. The reason for this is that in the signature of index (and index_mut) the type variable T (of items) appears in a bound so we don't generate refinements when instantiating it. More specifically, the signature of index is

fn index<T, I, A>(z: &Vec<T, A>, idx: I) -> <I as SliceIndex<T>>::Output
where 
    I: SliceIndex<[T]>,
    A: Allocator

Since T appears under I: SliceIndex<[T]> we don't generate refinements for the instantiation.

Unclear if there's an easy workaround. Contrary to other traits where we can make an exception based on the trait definition, in this case, the "parametricity" of T comes from the implementation of SliceIndex<[T]> for usize.