Check that impl satisfies trait specs

[ranjitjhala]

Currently, flux happily verifies the below which seems dubious:

pub trait Silly {
    #[flux::sig(fn(&Self) -> i32{v:100 < v})]
    fn bloop(&self) -> i32;
}

impl Silly for i32 {
    fn bloop(&self) -> i32 {
        0
    }
}

Originally posted by @ranjitjhala in #589 (comment)

[nilehmann]

A blocker for this is that we rely on this unsoundness to have index syntax for RVec.

The impl is

impl<T> std::ops::Index<usize> for RVec<T> {
    type Output = T;

    #[flux::trusted]
    #[flux::sig(fn(&RVec<T>[@n], usize{v : v < n}) -> &T)]
    fn index(&self, index: usize) -> &T {
        self.get(index)
    }
}

The problem is flipped in this case: the signature for the impl is "more refined" than the trait declaration.

[ranjitjhala]

hmm not clear why this is a blocker? [ as you point out, the issue in the RVec case is flipped? ] ?

[nilehmann]

It's a blocker because fn(&RVec<T>[@n], usize{v : v < n}) -> &T (the impl) is not a subtype of fn(&RVec<T>, usize) -> &T (the trait). But when I wrote that we didn't have associated refinements which would make it a valid implementation, so it may be less of a blocker now.