Type inference fails on specific reuse of a reference

[jhaye]

I took a look at the all zero exercise. When adding the following loop invariant #[invariant(bounds, @i <= (@*v).len())] while v is also referenced in the already existing invariant, I get the following error:

error[E0282]: type annotations needed
  --> 04_all_zero.rs:13:5
   |
13 |     #[invariant(proph_const, ^v == ^old_v.inner())]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ cannot infer type
   |
   = note: this error originates in the attribute macro `invariant` (in Nightly builds, run with -Z macro-backtrace for more info)

error[creusot]: internal error

Running with -Z macro-backtrace isn't very illuminating and interestingly, other invariants like #[invariant(prev_all_zero, forall<j: Int> 0 <= j && j < @i ==> (@v)[j] == 0u32)] that also use v do not produce this error.

I have tried some variations of the first invariant:

1. #[invariant(bounds, @i <= (@v).len())]
2. #[invariant(bounds, @i <= (@^v).len())]
3. #[invariant(bounds, @i <= @(v.len()))]

They all produce the same outcome.

[xldenis]

This is an unfortunate side-effect of how the contracts are encoded in Rust code, it doesn't play super well with inference. Typically @ is the primary cause of issue, if rust doesn't know the type of i before the invariant expression, it will fail because there multiple types which have a Model instance with ModelTy = Int.

Unfortunately, short of better rustc support, there's not much we can do (that I know of at least).