Bug when accessing fields of elements of Vector / HashMap

[nokunish]

Prusti has some issues detecting the types of parameters, and this seems to only occur when accessing fields of elements in a Vector / HashMap from inside a while loop.

#[derive(Clone, Eq, PartialEq, Hash)]
struct Val(usize);

pub struct MapVal
{
    map: HashMap<usize, Val>
}

impl MapVal
{
    // 1. Prusti doesn't tell us to specify 'V'
    #[ensures(forall(|u: usize| u < 10 ==> result.map.get(&u).is_some() && (*result.map.get(&u).unwrap()).0 === init.0))]

    fn new(init: Val) -> Self {
        let mut map = HashMap::new();
        let mut i = 0;

        while i < 10 {
            body_invariant!(i < 10);

            //2. Error msg:
            //      [E0282] type annotations needed for `std::collections::HashMap<K, V>`.
            //      [Note] type must be known at this point
            //      consider giving `map` an explicit type, where the type for type parameter `V` is specified
            prusti_assert!(forall(|u: usize| u < i ==> map.get(&u).is_some() && (*map.get(&u).unwrap()).0 === init.0));

            // 3. Prusti doesn't tell us to specify 'V' if we don't access the field of struct Val
            prusti_assert!(forall(|u: usize| u < i ==> map.get(&u).is_some() && *(map.get(&u).unwrap()) === init));

            map.insert(i, init.clone());

            i += 1;
        }

         // 4. Prusti doesn't tell us to specify 'V' when assertion is called from outside the while loop
        prusti_assert!(map.get(&i).is_some() && (*map.get(&i).unwrap()).0 === init.0);

        Self {map}
    }
}

Prusti complains that that the type parameter for the value type must be specified when the field of struct Val is accessed in an assertion called from inside the loop (2). However, when that field is accessed from assertions / specifications called from outside the loop(1, 4), or if it's not accessed (3) , then it doesn't give that complaint.

Possible solutions that seem to fix this problem are

1. explicitly indicate let mut map:HashMap<usize, Val> = HashMap::new(), although the compiler in general seems to deduce this automatically
2. verify / assume that the Value object is equal, i.e. *map.get(&i).unwrap() === init before asserting that the fields of those objects are the same (assertion 2).
3. Insert a key-val pair once before entering the loop