Bug: clause value not computed, resulting in LLBC rejected by Aeneas

[maximebuyse]

Code snippet to reproduce the bug:

trait T1 {
    type A;
}
trait T2: T1 {}

impl<I: T1> T2 for I {}

Charon version: 0.1.167

Charon command: charon cargo --preset=aeneas

Charon output:

warning: Could not compute the value of Self::Clause0::A (Some(TraitRef(HashConsed(TraitRefContents { kind: SelfId, trait_decl_ref: RegionBinder { regions: [], skip_binder: TraitDeclRef { id: 1, generics: <@TypeBound(1, 0)> } } })))) needed to update generics <@TypeBound(0, 0)> for item aeneas_test::T2.
         Constraints in scope:
           - ClauseBound(0, 0)::A = @TypeBound(0, 1)
  --> src/main.rs:40:1
   |
40 | impl<I: T1> T2 for I {}
   | ^^^^^^^^^^^^^^^^^^^^^^^

Explain the bug:

Calling Aeneas on the generated LLBC gives the error: Found type error in the output of charon

[Nadrieril]

Beautiful minimization, will look into it