ICE: failed to resolve instance for <dyn ThriftService as ThriftService>::foo

[matthiaskrgr]

I tried this code:

use std::future::Future;

pub trait Service {
    type Response;
    type Future: Future<Output = Self::Response>;
}

pub trait ThriftService: Service<Future = Box<dyn Future<Output = i32>>, Response = i32> {
    fn foo(&self) {}
}


#[kani::proof]
fn main() {
    let x: &dyn ThriftService = todo!();
}

using the following command line invocation:

RUST_BACKTRACE=1 kani 102933-2.rs

with Kani version:

I expected to see this happen: explanation

Kani Rust Verifier 0.55.0 (standalone)
warning: unused variable: `x`
  --> 102933-2.rs:15:9
   |
15 |     let x: &dyn ThriftService = todo!();
   |         ^ help: if this is intentional, prefix it with an underscore: `_x`
   |
   = note: `#[warn(unused_variables)]` on by default

error: internal compiler error: compiler/rustc_middle/src/ty/instance.rs:587:21: failed to resolve instance for <dyn ThriftService as ThriftService>::foo
 --> 102933-2.rs:9:5
  |
9 |     fn foo(&self) {}
  |     ^^^^^^^^^^^^^

thread 'rustc' panicked at compiler/rustc_middle/src/ty/instance.rs:587:21:
Box<dyn Any>
stack backtrace:
   0:     0x7fc82d9d9f1a - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::h31dc88f6577e8818
   1:     0x7fc82e203317 - core::fmt::write::h1296d08387b85208
   2:     0x7fc82f48d9d1 - std::io::Write::write_fmt::h60f3b4e20fc7812f
   3:     0x7fc82d9d9d72 - std::sys::backtrace::BacktraceLock::print::h12f30b474946a668
   4:     0x7fc82d9dc291 - std::panicking::default_hook::{{closure}}::hcd71afd9479200e3
   5:     0x7fc82d9dc0c4 - std::panicking::default_hook::hd0f9dbf29aa65768
   6:     0x64571a97e495 - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h07e74ae1e803cf7a
   7:     0x64571a97c1ea - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hc19532aa8f4b5bfb
   8:     0x7fc82d9dc9b8 - std::panicking::rust_panic_with_hook::ha2e90e1b96f5d037
   9:     0x7fc82cb7b581 - std[3955799ea844ceb3]::panicking::begin_panic::<rustc_errors[f28b20d2cb2c50ae]::ExplicitBug>::{closure#0}
  10:     0x7fc82cb6eb76 - std[3955799ea844ceb3]::sys::backtrace::__rust_end_short_backtrace::<std[3955799ea844ceb3]::panicking::begin_panic<rustc_errors[f28b20d2cb2c50ae]::ExplicitBug>::{closure#0}, !>
  11:     0x7fc82cb6a299 - std[3955799ea844ceb3]::panicking::begin_panic::<rustc_errors[f28b20d2cb2c50ae]::ExplicitBug>
  12:     0x7fc82cb84701 - <rustc_errors[f28b20d2cb2c50ae]::diagnostic::BugAbort as rustc_errors[f28b20d2cb2c50ae]::diagnostic::EmissionGuarantee>::emit_producing_guarantee
  13:     0x7fc82d0ae51d - <rustc_errors[f28b20d2cb2c50ae]::DiagCtxtHandle>::span_bug::<rustc_span[28cede8597ee1bb4]::span_encoding::Span, alloc[29916fc110380a4b]::string::String>
  14:     0x7fc82d14b0d8 - rustc_middle[84a3b9fea629b5f1]::util::bug::opt_span_bug_fmt::<rustc_span[28cede8597ee1bb4]::span_encoding::Span>::{closure#0}
  15:     0x7fc82d130c8a - rustc_middle[84a3b9fea629b5f1]::ty::context::tls::with_opt::<rustc_middle[84a3b9fea629b5f1]::util::bug::opt_span_bug_fmt<rustc_span[28cede8597ee1bb4]::span_encoding::Span>::{closure#0}, !>::{closure#0}
  16:     0x7fc82d130b3b - rustc_middle[84a3b9fea629b5f1]::ty::context::tls::with_context_opt::<rustc_middle[84a3b9fea629b5f1]::ty::context::tls::with_opt<rustc_middle[84a3b9fea629b5f1]::util::bug::opt_span_bug_fmt<rustc_span[28cede8597ee1bb4]::span_encoding::Span>::{closure#0}, !>::{closure#0}, !>
  17:     0x7fc82d14b007 - rustc_middle[84a3b9fea629b5f1]::util::bug::span_bug_fmt::<rustc_span[28cede8597ee1bb4]::span_encoding::Span>
  18:     0x7fc82e63f521 - <rustc_middle[84a3b9fea629b5f1]::ty::instance::Instance>::expect_resolve
  19:     0x7fc82eaa85d7 - <rustc_middle[84a3b9fea629b5f1]::ty::instance::Instance>::expect_resolve_for_vtable
  20:     0x7fc82eaa9505 - rustc_trait_selection[6307f589a1799ac4]::traits::vtable::vtable_entries::{closure#0}
  21:     0x7fc82ebc890d - rustc_trait_selection[6307f589a1799ac4]::traits::vtable::vtable_entries
  22:     0x7fc82ebc8568 - rustc_query_impl[762dd1939c7ece16]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[762dd1939c7ece16]::query_impl::vtable_entries::dynamic_query::{closure#2}::{closure#0}, rustc_middle[84a3b9fea629b5f1]::query::erase::Erased<[u8; 16usize]>>
  23:     0x7fc82ebc8527 - <rustc_query_impl[762dd1939c7ece16]::query_impl::vtable_entries::dynamic_query::{closure#2} as core[420b71e5fcfa1e50]::ops::function::FnOnce<(rustc_middle[84a3b9fea629b5f1]::ty::context::TyCtxt, rustc_type_ir[aa2c6cd7ba9ec25c]::binder::Binder<rustc_middle[84a3b9fea629b5f1]::ty::context::TyCtxt, rustc_type_ir[aa2c6cd7ba9ec25c]::predicate::TraitRef<rustc_middle[84a3b9fea629b5f1]::ty::context::TyCtxt>>)>>::call_once
  24:     0x7fc82ebc5d37 - rustc_query_system[1704d0a4bf762c9]::query::plumbing::try_execute_query::<rustc_query_impl[762dd1939c7ece16]::DynamicConfig<rustc_query_system[1704d0a4bf762c9]::query::caches::DefaultCache<rustc_type_ir[aa2c6cd7ba9ec25c]::binder::Binder<rustc_middle[84a3b9fea629b5f1]::ty::context::TyCtxt, rustc_type_ir[aa2c6cd7ba9ec25c]::predicate::TraitRef<rustc_middle[84a3b9fea629b5f1]::ty::context::TyCtxt>>, rustc_middle[84a3b9fea629b5f1]::query::erase::Erased<[u8; 16usize]>>, false, false, false>, rustc_query_impl[762dd1939c7ece16]::plumbing::QueryCtxt, false>
  25:     0x7fc82ebc5a7d - rustc_query_impl[762dd1939c7ece16]::query_impl::vtable_entries::get_query_non_incr::__rust_end_short_backtrace
  26:     0x64571a897113 - rustc_middle::query::plumbing::query_get_at::h6c7cd22f7a969c6f
  27:     0x64571a8eff89 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty_ref::h189716a911d781af
  28:     0x64571a8eb918 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty::h1f2d96de75db2ae6
  29:     0x64571a8f773f - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h392e8e6c25f3a5aa
  30:     0x64571a9de66c - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h30d4aea3216d5909
  31:     0x64571aa0315f - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}::hb53dafd0a65b2d20
  32:     0x64571a9f3362 - rustc_smir::rustc_internal::run::hdb17e8acd9433354
  33:     0x64571a9e1cf8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h019c2d63e6e51a8f
  34:     0x7fc82f363030 - <rustc_interface[518cb27c8fb52ec1]::queries::Linker>::codegen_and_build_linker
  35:     0x7fc82efb3a27 - rustc_interface[518cb27c8fb52ec1]::interface::run_compiler::<core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>, rustc_driver_impl[d99d56083ab92750]::run_compiler::{closure#0}>::{closure#1}
  36:     0x7fc82f08f150 - std[3955799ea844ceb3]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[518cb27c8fb52ec1]::util::run_in_thread_with_globals<rustc_interface[518cb27c8fb52ec1]::util::run_in_thread_pool_with_globals<rustc_interface[518cb27c8fb52ec1]::interface::run_compiler<core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>, rustc_driver_impl[d99d56083ab92750]::run_compiler::{closure#0}>::{closure#1}, core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>>::{closure#0}, core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>>
  37:     0x7fc82f08f7ba - <<std[3955799ea844ceb3]::thread::Builder>::spawn_unchecked_<rustc_interface[518cb27c8fb52ec1]::util::run_in_thread_with_globals<rustc_interface[518cb27c8fb52ec1]::util::run_in_thread_pool_with_globals<rustc_interface[518cb27c8fb52ec1]::interface::run_compiler<core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>, rustc_driver_impl[d99d56083ab92750]::run_compiler::{closure#0}>::{closure#1}, core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>>::{closure#0}, core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[420b71e5fcfa1e50]::result::Result<(), rustc_span[28cede8597ee1bb4]::ErrorGuaranteed>>::{closure#1} as core[420b71e5fcfa1e50]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  38:     0x7fc82f08fbab - std::sys::pal::unix::thread::Thread::new::thread_start::h4351cd95dc3be91c
  39:     0x7fc83064139d - <unknown>
  40:     0x7fc8306c649c - <unknown>
  41:                0x0 - <unknown>

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: main
_RNvCsl9uD83Fi9mE_8_102933_24main
[Kani] current codegen location: Loc { file: "102933-2.rs", function: None, start_line: 14, start_col: Some(1), end_line: 14, end_col: Some(10), pragmas: [] }
error: aborting due to 1 previous error; 1 warning emitted

error: /home/matthias/.kani/kani-0.55.0/bin/kani-compiler exited with status exit status: 101

[matthiaskrgr]

I've seen similar ICEs in standalone rust, but I could not get this particular code to crash just with rustc and without kani 🤔