Internal error in option.rs

[UlrikBuchholtz]

trafficstars

Forgive me if this is naive: I was trying out aeneas on some rust code, and hit internal errors. I've managed to minimize the example to the following:

pub fn get<T>(v: &Vec<Option<T>>, i: u32) -> Option<&T> {
    if i == u32::MAX {
        return None;
    }
    let i_usize = usize::try_from(i).ok()?;
    v.get(i_usize)?.as_ref()
}

This results in:

Error] Internal error, please file an issue Source: '/rustc/library/core/src/option.rs', lines 2546:4-2546:64

[sonmarcho]

Thanks for the report! This is definitely not naïve: we simply don't handle well instantiating type variables with types containing borrows when calling functions. In the present case, ok()? desugars to an expression which introduces Option::from_residual::<&T>(...), where as you can see the type variable gets substituted for &T. This is a long-standing issue that I intend to lift soon - I'm working on improving our handling of fixed-points and loops, and this is the next item on my list. Also note that the error message should be better: this error should have been detected before the assert that triggered the failure.

As a temporary workaround the following version of the code with explicit matches does go through the translation:

pub fn get<T>(v: &Vec<Option<T>>, i: u32) -> Option<&T> {
    if i == u32::MAX {
        return None;
    }

    if let Some(i_usize) = usize::try_from(i).ok() {
        if let Option::Some(x) = v.get(i_usize) {
            x.as_ref()
        }
        else {
            None
        }
    }
    else {
        None
    }
}

The resulting Lean code:

... -- omitted axioms (there misses definitions for TryFrom in the standard library

def get
  {T : Type} (v : alloc.vec.Vec (Option T)) (i : U32) : Result (Option T) :=
  if i = core.num.U32.MAX
  then ok none
  else
    do
    let r ←
      core.convert.num.ptr_try_from_impls.TryFromUsizeU32corenumerrorTryFromIntError.try_from
        i
    let o ← core.result.Result.ok r
    match o with
    | none => ok none
    | some i_usize =>
      do
      let s := alloc.vec.Vec.deref v
      let o1 ←
        core.slice.Slice.get (core.slice.index.SliceIndexUsizeSliceInst (Option
          T)) s i_usize
      match o1 with
      | none => ok none
      | some x => core.option.Option.as_ref x