Compiler Doesn't Understand vector<T> where T doesn't have drop

[PaulFidika]

The following code is correct, but fails to compile:

    public fun create<K: copy, V>(keys: vector<K>, values: vector<V>): VecMap<K, V> {
        assert!(vector::length(&keys) == vector::length(&values), EVEC_LENGTH_MISMATCH);

        vector::reverse(&mut keys);
        vector::reverse(&mut values);

        let result = vec_map::empty();
        while (vector::length(&values) > 0) {
            let key = vector::pop_back(&mut keys);
            let value = vector::pop_back(&mut values);
            vec_map::insert(&mut result, key, value);
        };

        assert!(vector::is_empty(&keys), EVEC_NOT_EMPTY);
        assert!(vector::is_empty(&values), EVEC_NOT_EMPTY);

        result
    }

The compiler gives the incorrect error:

unused value without 'drop'
  ┌─ ./../sui_utils/sources/vec_map2.move:28:9
  │
12 │     public fun create<K: copy, V>(keys: vector<K>, values: vector<V>): VecMap<K, V> {
  │                                                    ------  ---------
  │                                                    │       │      │
  │                                                    │       │      The type 'vector<V>' can have the ability 'drop' but the type argument 'V' does not have the required ability 'drop'
  │                                                    │       The type 'vector<V>' does not have the ability 'drop'
  │                                                    The parameter 'values' still contains a value. The value does not have the 'drop' ability and must be consumed before the function returns
  ·
28 │         result
  │         ^^^^^^ Invalid return

The problem is that K and V do not have drop, but the code above guarantees that vector and vector will both be empty by the end of execution, and hence both vectors will be dropable. The compiler incorrectly thinks that vector or vector may have values that we're dropping, but this is not the case.

I even added the assertions at the end, which didn't help.

The only real solution here is to add an unnecessary 'drop' requirement to K and V.

This limits Move overall; suppose I want to provide a vector of objects that do not have drop as an ability; Move essentially breaks and cannot handle this situation.

[PaulFidika]

Do I need to add some spec or do something with the Move prover perhaps for this code to compile?

[nanne007]

Try vector::destory_empty for your keys,values at the end of your code.

[sblackshear]

@lerencao is correct--emptiness/non-emptiness of a vector is not captured in the type system, so you will always need to explicitly destroy a vector<T> where T does not have drop.