Unsound to use fresh KVar for generics with bound

[ranjitjhala]

The code below currently verifies, but shouldn't (maybe we're generating fresh kvars for the Self at the call to x.foo ?)

pub trait MyTrait {
    fn foo(&self) -> Self;
}

// This "verifies" unsoundly due to the parametricity of `T`.
#[flux::sig(fn<T as base, refine q: T -> bool> (&T{v:q(v)}) -> T{v: q(v)})]
pub fn bar<T: MyTrait>(x: &T) -> T {
    x.foo() //~ ERROR refinement type
}

[nilehmann]

Another example. The following code verifies because collect has type forall B: FromIterator. fn(Self) -> B and we are generating an unconstrained kvar for B

#[flux::sig(fn(Vec<i32>) -> Vec<i32[0]>)]
pub fn test(x: Vec<i32>) -> Vec<i32> {
    x.into_iter().collect()
}

[nilehmann]

This was fixed in https://github.com/flux-rs/flux/pull/623 and a test was added in https://github.com/flux-rs/flux/commit/3869e7f3263d922a46a2755305fd8a9885c80345