Index out of bounds panic

[jprider63]

I get the following panic at 2aecd0d366dfbaa0677d5d9791e164034391502e:

thread 'rustc' panicked at crates/flux-middle/src/rty/mod.rs:607:16:
index out of bounds: the len is 0 but the index is 0

From the following example:

#![allow(unused)]
#![flux::cfg(scrape_quals = true)]

#[path = "../lib/rvec.rs"]
pub mod rvec;
use rvec::RVec;

#[flux::sig(fn(xs:RVec<T>[@xl], ys:RVec<T>[@yl]) -> RVec<T>[xl + yl])]
fn merge<T:Copy + PartialOrd>(xs:RVec<T>, ys:RVec<T>) -> RVec<T> {
    let mut r = RVec::new();
    let mut i = 0;
    let mut j = 0;
    while i + j < xs.len() + ys.len() {
        if i == xs.len() {
            r.push(ys[j]);
            j += 1;
        } else if j == ys.len() {
            r.push(xs[i]);
            i += 1;
        } else {
            if xs[i] < ys[j] {
                r.push(xs[i]);
                i += 1;
            } else {
                r.push(ys[j]);
                j += 1;
            }
        }
    }
    r
}

[nilehmann]

@jprider63 I looked a bit into this. This is a minimal reproduction.

fn test<T: PartialOrd>(x: T, y: T) -> bool {
    x < y
}

The issue is related to PartialOrd<Rhs = Self> having a generic type with a default which we don't handle properly.

More specifically, when using a definition in an external crate (PartialOrd in this case), we generate a default refined version that Flux can understand. That logic is implemented in refining.rs.

When refining a definition, we need the list of generic parameters in the item containing the definition. For example, when refining Vec<T> inside fn foo<T>(x: Vec<T>) we need to know that T is a parameter of the containing item (the function foo in this case).

The issue here arises because when we refine Self in PartialOrd<Rhs = Self> we use the wrong list of generic parameters. Concretely, we are calling the function type_of with the DefId of the generic parameter Rhs. The generic parameter is not an item so it doesn't make sense to ask for its generic parameters in this line. What we should do instead is to find the containing item (PartialOrd in this case) and ask for its generic parameters.