ReVars from outer InferCtxt crash try_normalize

[rgwohlbold]

In try_normalize, types may contain region variables (ReVars) from an outer InferCtxt. However, try_normalize creates a fresh InferCtxt which means these cannot be resolved in this context. This manifests as an index out of bounds error and shows up when resolving alias types of types with region variables.

Consider the following example:

trait MyTrait {
    type MyType;

    fn foo(self: Self) -> Self::MyType;
}

struct S<E> { e: E }

impl<E> MyTrait for S<E> {
    type MyType = E;

    fn foo(self: Self) -> Self::MyType {
        self.e
    }
}

fn main() {
    let s: S<&'_ str> = S { e: "abc" };
    let k = s.foo();
}

Prusti crashes on this snippet with the following stack trace:

thread 'rustc' (1216222) panicked at /rust/deps/ena-0.14.3/src/snapshot_vec.rs:199:10:
index out of bounds: the len is 0 but the index is 5
stack backtrace:
   0:     0x7fca0edadb93 - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::hf3fc14c10e517ebe
   1:     0x7fca0f401998 - core::fmt::write::h60a8fe1fb572c912
   2:     0x7fca0ed628f1 - std::io::Write::write_fmt::h04f6f73f48cbbad0
   3:     0x7fca0ed73a72 - std::sys::backtrace::BacktraceLock::print::h90e3d87c9a5140eb
   4:     0x7fca0ed799f9 - std::panicking::default_hook::{{closure}}::h5fd5162b51244d27
   5:     0x7fca0ed79523 - std::panicking::default_hook::h72c168565d86eae1
   6:     0x7fca0dddc125 - std[57c1393ad41bbbfd]::panicking::update_hook::<alloc[7d9612ffe8b8ee55]::boxed::Box<rustc_driver_impl[902c67247d8c741]::install_ice_hook::{closure#1}>>::{closure#0}
   7:     0x7fca0ed79e1f - std::panicking::panic_with_hook::ha6b5140b25841651
   8:     0x7fca0ed79bda - std::panicking::panic_handler::{{closure}}::h0dee07c74bc57a6d
   9:     0x7fca0ed73bb9 - std::sys::backtrace::__rust_end_short_backtrace::hf5c7a0ee0072f6ae
  10:     0x7fca0ed5445d - __rustc[4dd267c369f14767]::rust_begin_unwind
  11:     0x7fca0b4cae30 - core::panicking::panic_fmt::h61140a6577667985
  12:     0x7fca0d4f92a3 - core::panicking::panic_bounds_check::h179101727ed356ff
  13:     0x7fca0f4fdfa1 - rustc_type_ir[ca44605ae549d8be]::relate::structurally_relate_tys::<rustc_middle[5b615cc8729d8cf8]::ty::context::TyCtxt, rustc_infer[20c7ea76d6543cc7]::infer::relate::generalize::Generalizer>::{closure#0}
  14:     0x7fca0f4f3469 - <rustc_infer[20c7ea76d6543cc7]::infer::relate::generalize::Generalizer as rustc_type_ir[ca44605ae549d8be]::relate::TypeRelation<rustc_middle[5b615cc8729d8cf8]::ty::context::TyCtxt>>::tys::{closure#0}
  15:     0x7fca0f4de29e - <rustc_infer[20c7ea76d6543cc7]::infer::relate::type_relating::TypeRelating as rustc_type_ir[ca44605ae549d8be]::relate::TypeRelation<rustc_middle[5b615cc8729d8cf8]::ty::context::TyCtxt>>::tys
  16:     0x7fca0f4e0c72 - rustc_type_ir[ca44605ae549d8be]::relate::structurally_relate_tys::<rustc_middle[5b615cc8729d8cf8]::ty::context::TyCtxt, rustc_infer[20c7ea76d6543cc7]::infer::relate::type_relating::TypeRelating>::{closure#0}
  17:     0x7fca0f4de026 - <rustc_infer[20c7ea76d6543cc7]::infer::relate::type_relating::TypeRelating as rustc_type_ir[ca44605ae549d8be]::relate::TypeRelation<rustc_middle[5b615cc8729d8cf8]::ty::context::TyCtxt>>::tys
  18:     0x7fca0f4b695c - <rustc_trait_selection[3bc5ae364c14853a]::traits::select::SelectionContext>::confirm_candidate
  19:     0x7fca0f6ee39d - rustc_trait_selection[3bc5ae364c14853a]::traits::project::normalize_projection_term
  20:     0x7fca0f6ec2f0 - <rustc_trait_selection[3bc5ae364c14853a]::traits::normalize::AssocTypeNormalizer as rustc_type_ir[ca44605ae549d8be]::fold::TypeFolder<rustc_middle[5b615cc8729d8cf8]::ty::context::TyCtxt>>::fold_ty
  21:     0x55d985c7a932 - rustc_middle::ty::structural_impls::<impl rustc_type_ir::fold::TypeFoldable<rustc_middle::ty::context::TyCtxt> for rustc_middle::ty::Ty>::fold_with::h185f833bf2655664
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_middle/src/ty/structural_impls.rs:373:16
  22:     0x55d9851193d0 - <rustc_type_ir::binder::Binder<I,T> as rustc_type_ir::fold::TypeSuperFoldable<I>>::super_fold_with::{{closure}}::h65ddde53f8877cf7
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_type_ir/src/binder.rs:141:30
  23:     0x55d9851193d0 - rustc_type_ir::binder::Binder<I,T>::map_bound::hf90d4570d89ffdc6
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_type_ir/src/binder.rs:196:21
  24:     0x55d9851193d0 - <rustc_type_ir::binder::Binder<I,T> as rustc_type_ir::fold::TypeSuperFoldable<I>>::super_fold_with::he73d9d55dfd09de1
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_type_ir/src/binder.rs:141:14
  25:     0x55d9851193d0 - <rustc_trait_selection::traits::normalize::AssocTypeNormalizer as rustc_type_ir::fold::TypeFolder<rustc_middle::ty::context::TyCtxt>>::fold_binder::hb9783e071ec0c61b
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:357:19
  26:     0x55d984f07968 - <rustc_type_ir::binder::Binder<I,T> as rustc_type_ir::fold::TypeFoldable<I>>::fold_with::hce37a5c34e021fe2
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_type_ir/src/binder.rs:122:16
  27:     0x55d9851195be - rustc_trait_selection::traits::normalize::AssocTypeNormalizer::fold::hd329570916cd90d9
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:177:82
  28:     0x55d98511a538 - rustc_trait_selection::traits::normalize::normalize_with_depth_to::{{closure}}::hfae741c07f783a89
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:121:45
  29:     0x55d98511a324 - stacker::maybe_grow::hbb09c32580fc4819
                               at /rust/deps/stacker-0.1.21/src/lib.rs:57:9
  30:     0x55d98511a324 - rustc_data_structures::stack::ensure_sufficient_stack::hb3456431c4ad381b
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_data_structures/src/stack.rs:21:5
  31:     0x55d98511a324 - rustc_trait_selection::traits::normalize::normalize_with_depth_to::h8f9ecb6f5f4b2b67
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:121:18
  32:     0x55d985119759 - rustc_trait_selection::traits::normalize::normalize_with_depth::ha9741a988bf0e6f9
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:103:17
  33:     0x55d985045e85 - <rustc_infer::infer::at::At as rustc_trait_selection::traits::normalize::NormalizeExt>::normalize::h5ae23c25c3dcdf8d
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:36:17
  34:     0x55d985045703 - <rustc_infer::infer::at::At as rustc_trait_selection::traits::normalize::NormalizeExt>::deeply_normalize::h246b6811e4db31b5
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_trait_selection/src/traits/normalize.rs:74:18
  35:     0x55d985044b89 - prusti_encoder::encoders::ty::generics::params::GParams::try_normalize::{{closure}}::h4899b74d9b19dc66
                               at /home/richard/progs/prusti-dev/prusti-encoder/src/encoders/ty/generics/params.rs:128:18
  36:     0x55d984fa4cfb - vir::context::with_vcx::{{closure}}::h2b7ff8572774d4ff
                               at /home/richard/progs/prusti-dev/vir/src/context.rs:189:9
  37:     0x55d9850841aa - std::thread::local::LocalKey<core::cell::RefCell<T>>::with_borrow::{{closure}}::h319a3def20efc545
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:526:26
  38:     0x55d98507c792 - std::thread::local::LocalKey<T>::try_with::hf9148efd73e7877d
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:315:12
  39:     0x55d98504a82a - std::thread::local::LocalKey<T>::with::h4f4572b4cc6f3129
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:279:20
  40:     0x55d98507fbe6 - std::thread::local::LocalKey<core::cell::RefCell<T>>::with_borrow::he8df11924d00c60e
                               at /home/richard/.rustup/toolchains/nightly-2025-09-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/local.rs:526:14
  41:     0x55d984fa1b4d - vir::context::with_vcx::h9095e04cfab3166e
                               at /home/richard/progs/prusti-dev/vir/src/context.rs:183:10
  42:     0x55d9852cc35f - prusti_encoder::encoders::ty::generics::params::GParams::try_normalize::h4d1105114abcef02
                               at /home/richard/progs/prusti-dev/prusti-encoder/src/encoders/ty/generics/params.rs:105:9

In particular, the following type causes this issue, note the ReVar '?5:

Alias(Projection, AliasTy { args: [S<&'?5 str>], def_id: DefId(0:4 ~ abc[9888]::MyTrait::MyType), .. })

This PR changes all region variables to 'erased for normalization. In my manual tests, this made this crash disappear and I did not find that files where this fix didn't work/caused another issue. This is supported by the data in https://prusti-stdlib-support.rgwohlbold.de/

[ThomasMayerl]

Hey @rgwohlbold do you by chance know if the crash during the following code snippet could be related to the issue mentioned here?

fn foo<X, Y: MyTrait<X, Z>, Z>(x: Y::SomeType<SomeWrapper<X>>, y: Y::SomeOtherType, z: Y) {
    let res: X = z.gen();
}

trait MyTrait<T, T2> {
    type SomeType<A>;
    type SomeOtherType;

    fn gen(self) -> T;
}

struct St1<T> {
    x: T,
}
struct St2<T> {
    y: T,
}

impl<T, T2> MyTrait<T, T2> for St1<T> {
    type SomeType<A> = A;
    type SomeOtherType = T2;

    fn gen(self) -> T {
        self.x
    }
}

impl<T> MyTrait<T, T> for St2<T> {
    type SomeType<A> = T;
    type SomeOtherType = SomeWrapper<T>;

    fn gen(self) -> T {
        self.y
    }
}

fn bar() {
    foo::<f32, St1<f32>, u32>(SomeWrapper { val: 5.5 }, 6, St1 { x: 5.5 });
    foo::<bool, St2<bool>, bool>(true, SomeWrapper { val: false }, St2 { y: true });
}

struct SomeWrapper<T> {
    val: T,
}

[ThomasMayerl]

lgtm

[Aurel300]

Does rustc no longer have methods that erase regions?

[rgwohlbold]

@ThomasMayerl I looked into this and this seems to be a separate issue, it also shows up for the doctests. I created a draft PR here (want to verify with the doctest pipeline): #171

[rgwohlbold]

Does rustc no longer have methods that erase regions?

I tried to use vcx.tcx().erase_regions(ty), but this led to issues in PCG, for example for this snippet:

use std::any::Any;

fn foo(s: &mut dyn Any) {
    let _ = s.downcast_mut::<u32>();
}

Other than this method, I did not find a method that erases region variables in the way we'd like.

[Aurel300]

In principle we can merge this if it fixes something, but I actually wonder why we need this at all and whether we are not just hiding a bug.

In try_normalize, types may contain region variables (ReVars) from an outer InferCtxt.

But why? We are not doing anything during the actual type inference, so we should by default not observe any ReVars in the MIR we consume. The docs say:

A region variable. Should not exist outside of type inference.

And our usage of the inference context is not somehow recursive, right? How come we hit this case then?

[rgwohlbold]

I investigated a bit. I found that there are at least a couple of spots where the ReVars show up, even if the comment indicates otherwise:

• Constants: In ConstEnc in encode_const_val_ty, ty can constain ReVars. In the test case, I get that the string slice has type &'?2 str.
• Method signatures: Within MethodCallEnc, we get the type Alias(Projection, AliasTy { args: [S<&'?5 str>], def_id: DefId(0:4 ~ associated_types[b583]::MyTrait::MyType), .. }) with context GParams { params: [], env: ParamEnv { caller_bounds: [] }, is_trait_extern_spec: false } containing a ReVar

What should we do here? Erase at these sources or keep the erase where it is now?