Bug: Panicked when getting FullDef from Hax for impl traits with associated types

[ssyram]

This problem should be somehow related to #790 .

Code snippet to reproduce the bug: I simplified the production, and simply have:

trait Internal {
    type IntAssoc;
    fn internal_method(&self) -> Self::IntAssoc;
}

impl Internal for i32 {
    type IntAssoc = i32;
    fn internal_method(&self) -> Self::IntAssoc {
        *self + 1
    }
}

fn main() { }

Then, I run by:

RUST_LOG=trace RUST_BACKTRACE=full ./bin/charon rustc --print-llbc -- --crate-type=rlib charon/tests/ui/vtables.rs

Then, there is a panic reported in Rustc:

thread 'rustc' panicked at compiler/rustc_middle/src/ty/generic_args.rs:54:14:
index out of bounds: the len is 0 but the index is 0

After tracing, I found the problem does not seem to be in Charon, but is in Hax, when we try to get the FullDef of trait impl.

[Nadrieril]

I cannot reproduce this bug

[Nadrieril]

(After private discussion) Closing for now, please reopen if you manage to find a reproducer that triggers the error with make test.

[ssyram]

The issue is still there?

[Nadrieril]

Yep, managed to reproduce in the end: it's a panic that only occurs when tracing is on, it's in the printing routine of a rustc_middle::TraitRefwith no Self.