Compilation hangs when having a type defined inside a trait

[dbsc]

The following code snippet

pub trait Trait1 {
    type T: Trait2;
}

pub trait Trait2: Trait1 {
    type U;
}

makes charon hang. The motivation for this structure can be found in arkworks/ff.

[Nadrieril]

The stack overflow happens in hax; the last bit in charon is: https://github.com/AeneasVerif/charon/blob/fd3f417a7408c137b1a645fb276e3bd77518da78/charon/src/translate_traits.rs?plain=1#L344

Seems pretty innocent; do you think this is something to fix on hax's side?

Marking it as blocked on hax for now.

[sonmarcho]

Yes, let's fix it on hax's side. But maybe wait for the merge of charon_traits_merge?

[Nadrieril]

This fails in hax on THIR too. I filed the issue there: https://github.com/hacspec/hax/issues/692

[Nadrieril]

This was fixed in hax. I'll add a regression test in my next PR.