Verus panicked at rust_verify/src/lifetime_generate.rs:520:30

[y1ca1]

Minimized repro:

use vstd::prelude::*;

verus! {   

trait Foo {                 
    type T<'a>;

    fn foo<'a>() -> Result<Self::T<'a>, ()> {
        Err(())
    }
}

fn main();
}

Verus outputs:

❯ RUST_BACKTRACE=1 verus src/main.rs
thread 'rustc' panicked at rust_verify/src/lifetime_generate.rs:520:30:
expected lifetime param
stack backtrace:
   0: std::panicking::begin_panic
   1: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
   2: alloc::vec::in_place_collect::<impl alloc::vec::spec_from_iter::SpecFromIter<T,I> for alloc::vec::Vec<T>>::from_iter
   3: rust_verify::lifetime_generate::erase_ty
   4: rust_verify::lifetime_generate::mk_typ_args
   5: rust_verify::lifetime_generate::erase_call
   6: rust_verify::lifetime_generate::erase_expr
   7: rust_verify::lifetime_generate::erase_block
   8: rust_verify::lifetime_generate::erase_expr
   9: rust_verify::lifetime_generate::erase_fn_common
  10: rust_verify::lifetime_generate::erase_trait_item
  11: rust_verify::lifetime_generate::gen_check_tracked_lifetimes
  12: rust_verify::lifetime::check_tracked_lifetimes
  13: rustc_middle::ty::context::GlobalCtxt::enter
  14: <rust_verify::verifier::VerifierCallbacksEraseMacro as rustc_driver_impl::Callbacks>::after_expansion
  15: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#0}::{closure#0}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuar
anteed>>
  16: rustc_span::create_session_globals_then::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver
_impl::run_compiler::{closure#0}>::{closure#0}>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

No panic when removing the trait default:

...
    fn foo<'a>() -> Result<Self::T<'a>, ()>;
...

❯ verus src/main.rs
verification results:: 1 verified, 0 errors

Tested on:

❯ verus --version
Verus
  Version: 0.2024.06.09.bf6d637
  Profile: release
  Platform: macos_aarch64
  Toolchain: 1.76.0-aarch64-apple-darwin

[Chris-Hawblitzel]

Can you try the latest commit?

[y1ca1]

Can you try the latest commit?

I tried it and it solved the issue. Thanks a ton!