ICE: Can't cast

[matthiaskrgr]

I tried this code:

// Test for specific details of how we handle higher-ranked subtyping to make
// sure that any changes are made deliberately.
//
// - `let y = x` creates a `Subtype` obligation that is deferred for later.
// - `w = a` sets the type of `x` to `Option<for<'a> fn(&'a ())>` and generalizes
//   `z` first to `Option<_>` and then to `Option<fn(&'0 ())>`.
//  - The various subtyping obligations are then processed.
//
// This requires that
// 1. the `Subtype` obligation from `y = x` isn't processed while the types of
//    `w` and `a` are being unified.
// 2. the pending subtype obligation isn't considered when determining the type
//    to generalize `z` to first (when related to the type of `y`).
//
// Found when considering fixes to #117151
// check-pass

#[kani::proof]
fn main() {
    let mut x = None;
    let y = x;
    let z = Default::default();
    let mut w = (&mut x, z, z);
    let a = (&mut None::<fn(&())>, y, None::<fn(&'static ())>);
    w = a;
}

using the following command line invocation:

kani file.rs

with Kani version: 0.46.0

I expected to see this happen: explanation

Instead, this happened: explanation

Kani Rust Verifier 0.46.0 (standalone)
warning: variable `w` is assigned to, but never used
  --> generalize-subtyped-variables.rs:23:13
   |
23 |     let mut w = (&mut x, z, z);
   |             ^
   |
   = note: consider using `_w` instead
   = note: `#[warn(unused_variables)]` on by default

warning: value assigned to `w` is never read
  --> generalize-subtyped-variables.rs:25:5
   |
25 |     w = a;
   |     ^
   |
   = help: maybe it is overwritten before being read?
   = note: `#[warn(unused_assignments)]` on by default

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:517:13:
Can't cast

Expr { value: Symbol { identifier: "main::1::var_6::a" }, typ: StructTag("tag-_322056111968276457747727895819404471275"), location: None, size_of_annotation: None } (StructTag("tag-_322056111968276457747727895819404471275"))

StructTag("tag-_258072409371656006281506298450555494557")
stack backtrace:
   0: rust_begin_unwind
             at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:647:5
   1: core::panicking::panic_fmt
             at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:72:14
   2: cprover_bindings::goto_program::expr::Expr::cast_to
   3: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection
   4: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_stable
   5: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand_stable
   6: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_stable
   7: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
   8: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
   9: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
  10: scoped_tls::ScopedKey<T>::set
  11: rustc_smir::rustc_internal::init
  12: stable_mir::compiler_interface::run
  13: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
  14: rustc_interface::passes::start_codegen
  15: <rustc_interface::queries::Queries>::codegen_and_build_linker
  16: 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.

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
main
[Kani] current codegen location: Loc { file: "generalize-subtyped-variables.rs", function: None, start_line: 19, start_col: Some(1), end_line: 19, end_col: Some(10) }
warning: 2 warnings emitted

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