Consistency Error with nested generics

[JM4ier]

Trying to verify the following (probably minimal) code leads to a consistency error.

// <-- consistency error reported on first line

use prusti_contracts::*;

struct Vector<T>(T);
struct Wrapper<T>(T);

impl<T> Vector<T> {
    #[pure]
    fn len(&self) -> usize {1}

    #[requires(idx < self.len())]
    fn index(&self, idx: usize) {}
}

fn first<T>(vec: &Vector<Wrapper<T>>) {
    vec.index(0)
}

[Prusti internal error] Prusti encountered an unexpected internal error
Details: consistency error in veribetrfs::first: Consistency error: Function m_len__$TY$__struct$m_Wrapper$struct$m_Wrapper$__TYPARAM__$_T$0$__$ with formal arguments List(_1: Snap$struct$m_Vector$struct$m_Wrapper$struct$m_Wrapper$__TYPARAM__$_T$0$__) cannot be applied to provided arguments List(snap$__$TY$__Snap$struct$m_Vector$struct$m_Wrapper$__TYPARAM__$_T$0$__$(_2.val_ref)). (@12.22)