Update hax

charon/src/bin/charon-driver/translate/translate_trait_objects.rs

@@ -225,7 +225,7 @@ impl ItemTransCtx<'_, '_> {
         )?;
         let hax::FullDefKind::AssocFn {
             sig,
-            vtable_safe: true,
+            vtable_sig: Some(_),
             ..
         } = item_def.kind()
         else {
@@ -234,7 +234,7 @@ impl ItemTransCtx<'_, '_> {
 
         let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?;
         // It's ok to translate the method signature in the context of the trait because
-        // `vtable_safe: true` ensures the method has no generics of its own.
+        // `vtable_sig: Some(_)` ensures the method has no generics of its own.
         let sig = self.translate_fun_sig(span, sig)?;
         let ty = TyKind::FnPtr(sig).into_ty();
 
@@ -535,7 +535,8 @@ impl ItemTransCtx<'_, '_> {
         // Exit if the item isn't a vtable safe method.
         match self.poly_hax_def(&item.decl_def_id)?.kind() {
             hax::FullDefKind::AssocFn {
-                vtable_safe: true, ..
+                vtable_sig: Some(_),
+                ..
             } => {}
             _ => return Ok(()),
         }

charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out

@@ -0,0 +1,49 @@
+# Final LLBC before serialization:
+
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
+fn UNIT_METADATA()
+{
+    let @0: (); // return
+
+    @0 := ()
+    return
+}
+
+const UNIT_METADATA: () = @Fun0()
+
+struct test_crate::Trait::{vtable} {
+  size: usize,
+  align: usize,
+  drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_)),
+  method_foo: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_))),
+  super_trait_0: &'static (core::marker::MetaSized::{vtable}),
+}
+
+// Full name: test_crate::Trait
+trait Trait<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    fn foo<'a, '_1, Self : 'a> = test_crate::Trait::foo<'a, '_0_1, Self>[Self]
+    vtable: test_crate::Trait::{vtable}
+}
+
+fn test_crate::Trait::foo<'a, '_1, Self>(@1: &'_1 (Self))
+where
+    [@TraitClause0]: Trait<Self>,
+    Self : 'a,
+
+fn test_crate::foo<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_0)))
+{
+    let @0: (); // return
+    let x@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_)); // arg #1
+
+    @0 := ()
+    @0 := ()
+    return
+}
+
+
+

charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.rs

@@ -0,0 +1,7 @@
+trait Trait {
+    fn foo<'a>(&self)
+    where
+        Self: 'a;
+}
+
+fn foo(x: &dyn Trait) {}