Open PaulFidika opened 1 year ago
Do I need to add some spec or do something with the Move prover perhaps for this code to compile?
Try vector::destory_empty
for your keys
,values
at the end of your code.
@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
.
The following code is correct, but fails to compile:
The compiler gives the incorrect error:
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.