Missing (polymorphic) refinements for vec set/get
Opened this issue · 1 comments
ranjitjhala commented
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 commented
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
.