Make Self clause explicit in trait method declarations

charon/src/ast/types_utils.rs

@@ -118,6 +118,19 @@ impl<T> Binder<T> {
     }
 }
 
+impl<T> RegionBinder<T> {
+    /// Wrap the value in an empty region binder, shifting variables appropriately.
+    pub fn empty(x: T) -> Self
+    where
+        T: TyVisitable,
+    {
+        RegionBinder {
+            regions: Default::default(),
+            skip_binder: x.move_under_binder(),
+        }
+    }
+}
+
 impl GenericArgs {
     pub fn len(&self) -> usize {
         let GenericArgs {
@@ -557,6 +570,11 @@ pub trait TyVisitable: Sized + AstVisitable {
         self.drive_mut(&mut SubstVisitor::new(generics));
     }
 
+    /// Move under one binder.
+    fn move_under_binder(self) -> Self {
+        self.move_under_binders(DeBruijnId::one())
+    }
+
     /// Move under `depth` binders.
     fn move_under_binders(mut self, depth: DeBruijnId) -> Self {
         let Continue(()) = self.visit_db_id::<Infallible>(|id| {

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

@@ -333,6 +333,9 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx> {
     pub parent_trait_clauses: Vector<TraitClauseId, TraitClause>,
     /// (For traits only) accumulated trait clauses on associated types.
     pub item_trait_clauses: HashMap<TraitItemName, Vector<TraitClauseId, TraitClause>>,
+    /// (For method declarations only) the clause id corresponding to the explicit `Self` clause.
+    /// If `None`, use `TraitRefKind::Self` instead.
+    pub self_clause_id: Option<TraitClauseId>,
 
     /// The (regular) variables in the current function body.
     pub locals: Locals,
@@ -985,6 +988,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
             binding_levels: Default::default(),
             parent_trait_clauses: Default::default(),
             item_trait_clauses: Default::default(),
+            self_clause_id: Default::default(),
             locals: Default::default(),
             vars_map: Default::default(),
             blocks: Default::default(),
@@ -1169,6 +1173,12 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         span: Span,
         mut id: usize,
     ) -> Result<ClauseDbVar, Error> {
+        if self.self_clause_id.is_some() {
+            // We added an extra first clause which hax doesn't know about, so we adapt the index
+            // accordingly.
+            // TODO: more robust tracking of clause ids between hax and charon.
+            id += 1;
+        }
         // The clause indices returned by hax count clauses in order, starting from the parentmost.
         // While adding clauses to a binding level we already need to translate types and clauses,
         // so the innermost item binder may not have all the clauses yet. Hence for that binder we

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

@@ -255,10 +255,17 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                     trait_ref,
                     path,
                 );
-                // If we are refering to a trait clause, we need to find the
-                // relevant one.
+                // If we are refering to a trait clause, we need to find the relevant one.
                 let mut trait_id = match &impl_source.r#impl {
-                    ImplExprAtom::SelfImpl { .. } => TraitRefKind::SelfId,
+                    ImplExprAtom::SelfImpl { .. } => match self.self_clause_id {
+                        None => TraitRefKind::SelfId,
+                        // An explicit `Self` clause is bound at the top-level; we use it instead
+                        // of the implicit `TraitRefKind::SelfId` one.
+                        Some(id) => TraitRefKind::Clause(DeBruijnVar::bound(
+                            DeBruijnId::new(self.binding_levels.len() - 1),
+                            id,
+                        )),
+                    },
                     ImplExprAtom::LocalBound { index, .. } => {
                         let var = self.lookup_clause_var(span, *index)?;
                         TraitRefKind::Clause(var)

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

@@ -55,7 +55,12 @@ impl BodyTransCtx<'_, '_> {
             error_or_panic!(self, span, &format!("Trait aliases are not supported"));
         }
 
-        let hax::FullDefKind::Trait { items, .. } = &def.kind else {
+        let hax::FullDefKind::Trait {
+            items,
+            self_predicate,
+            ..
+        } = &def.kind
+        else {
             error_or_panic!(self, span, &format!("Unexpected definition: {def:?}"));
         };
         let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
@@ -72,6 +77,12 @@ impl BodyTransCtx<'_, '_> {
         // `self.parent_trait_clauses`.
         // TODO: Distinguish between required and implied trait clauses?
         self.translate_def_generics(span, def)?;
+        let self_trait_ref = TraitRef {
+            kind: TraitRefKind::SelfId,
+            trait_decl_ref: RegionBinder::empty(
+                self.translate_trait_predicate(span, self_predicate)?,
+            ),
+        };
 
         // Translate the associated items
         // We do something subtle here: TODO: explain
@@ -90,19 +101,23 @@ impl BodyTransCtx<'_, '_> {
                     let fun_def = self.t_ctx.hax_def(item_def_id)?;
                     let fn_ref = self.translate_binder_for_def(item_span, &fun_def, |bt_ctx| {
                         let fun_id = bt_ctx.register_fun_decl_id(item_span, item_def_id);
-                        // TODO: there's probably a cleaner way to write this
                         assert_eq!(bt_ctx.binding_levels.len(), 2);
-                        let fun_generics = bt_ctx
-                            .outermost_binder()
-                            .params
-                            .identity_args_at_depth(GenericsSource::item(def_id), DeBruijnId::one())
-                            .concat(
-                                GenericsSource::item(fun_id),
-                                &bt_ctx.innermost_binder().params.identity_args_at_depth(
-                                    GenericsSource::Method(def_id.into(), item_name.clone()),
-                                    DeBruijnId::zero(),
-                                ),
+                        let mut fun_generics =
+                            bt_ctx.outermost_binder().params.identity_args_at_depth(
+                                GenericsSource::item(def_id),
+                                DeBruijnId::one(),
                             );
+                        // Add the necessary explicit `Self` clause at the start.
+                        fun_generics
+                            .trait_refs
+                            .insert(0.into(), self_trait_ref.clone().move_under_binder());
+                        fun_generics = fun_generics.concat(
+                            GenericsSource::item(fun_id),
+                            &bt_ctx.innermost_binder().params.identity_args_at_depth(
+                                GenericsSource::Method(def_id.into(), item_name.clone()),
+                                DeBruijnId::zero(),
+                            ),
+                        );
                         Ok(FunDeclRef {
                             id: fun_id,
                             generics: fun_generics,

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

@@ -551,7 +551,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     ) -> Result<(), Error> {
         assert!(self.binding_levels.len() == 0);
         self.binding_levels.push_front(BindingLevel::new(true));
-        self.push_generics_for_def(span, def, false)?;
+        self.push_generics_for_def(span, def, false, false)?;
         self.innermost_binder_mut().params.check_consistency();
         Ok(())
     }
@@ -563,7 +563,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         def: &hax::FullDef,
     ) -> Result<(), Error> {
         self.binding_levels.push_front(BindingLevel::new(true));
-        self.push_generics_for_def_without_parents(span, def, true, true)?;
+        self.push_generics_for_def_without_parents(span, def, true, true, false)?;
         self.innermost_binder().params.check_consistency();
         Ok(())
     }
@@ -579,24 +579,34 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         span: Span,
         def: &hax::FullDef,
         is_parent: bool,
+        explicit_self_clause: bool,
     ) -> Result<(), Error> {
-        use hax::FullDefKind;
+        use hax::FullDefKind::*;
         // Add generics from the parent item, recursively (recursivity is important for closures,
-        // as they could be nested).
-        match &def.kind {
-            FullDefKind::AssocTy { .. }
-            | FullDefKind::AssocFn { .. }
-            | FullDefKind::AssocConst { .. }
-            | FullDefKind::Closure { .. }
-            | FullDefKind::Ctor { .. }
-            | FullDefKind::Variant { .. } => {
+        // as they can be nested).
+        match def.kind() {
+            AssocTy { .. }
+            | AssocFn { .. }
+            | AssocConst { .. }
+            | Closure { .. }
+            | Ctor { .. }
+            | Variant { .. } => {
                 let parent_def_id = def.parent.as_ref().unwrap();
                 let parent_def = self.t_ctx.hax_def(parent_def_id)?;
-                self.push_generics_for_def(span, &parent_def, true)?;
+                let explicit_self_clause = matches!(def.kind(), AssocFn { .. })
+                    && matches!(parent_def.kind(), Trait { .. });
+                // Add an explicit `Self` clause to trait method declarations.
+                self.push_generics_for_def(span, &parent_def, true, explicit_self_clause)?;
             }
             _ => {}
         }
-        self.push_generics_for_def_without_parents(span, def, !is_parent, !is_parent)?;
+        self.push_generics_for_def_without_parents(
+            span,
+            def,
+            !is_parent,
+            !is_parent,
+            explicit_self_clause,
+        )?;
         Ok(())
     }
 
@@ -608,22 +618,33 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
         def: &hax::FullDef,
         include_late_bound: bool,
         include_assoc_ty_clauses: bool,
+        explicit_self_clause: bool,
     ) -> Result<(), Error> {
         use hax::FullDefKind;
         if let Some((generics, predicates)) = def.generics() {
             // Add the generic params.
             self.push_generic_params(generics)?;
-            // Add the self trait clause.
-            match &def.kind {
-                FullDefKind::TraitImpl {
-                    trait_pred: self_predicate,
-                    ..
-                }
-                | FullDefKind::Trait { self_predicate, .. } => {
-                    self.register_trait_decl_id(span, &self_predicate.trait_ref.def_id);
-                    let _ = self.translate_trait_predicate(span, self_predicate)?;
-                }
-                _ => {}
+            // Add the explicit self trait clause if required.
+            if let FullDefKind::Trait { self_predicate, .. } = &def.kind
+                && explicit_self_clause
+            {
+                // We add an explicit `Self` clause to trait method declarations. Trait method
+                // implementations already don't use the implicit `Self` clause. This way, methods
+                // don't need an implicit `Self` clause: they're normal functions, and the trait
+                // decl/impl takes care to pass the right arguments.
+                let self_predicate =
+                    RegionBinder::empty(self.translate_trait_predicate(span, self_predicate)?);
+                let clause_id =
+                    self.innermost_generics_mut()
+                        .trait_clauses
+                        .push_with(|clause_id| TraitClause {
+                            clause_id,
+                            origin: PredicateOrigin::TraitSelf,
+                            span: Some(span),
+                            trait_: self_predicate,
+                        });
+                // Record the id so we can resolve `ImplExpr::Self`s to it.
+                self.self_clause_id = Some(clause_id);
             }
             // Add the predicates.
             let (origin, location) = match &def.kind {

charon/src/ids/vector.rs

@@ -126,6 +126,12 @@ where
         self.real_len += other.real_len;
     }
 
+    /// Insert a value at that index, shifting all the values with equal or larger indices.
+    pub fn insert(&mut self, id: I, x: T) {
+        self.real_len += 1;
+        self.vector.insert(id, Some(x))
+    }
+
     /// Map each entry to a new one, keeping the same ids.
     pub fn map<U>(self, mut f: impl FnMut(T) -> U) -> Vector<I, U> {
         Vector {

charon/tests/cargo/dependencies.out

@@ -23,7 +23,7 @@ trait core::ops::function::FnOnce<Self, Args>
     parent_clause1 : [@TraitClause1]: core::marker::Tuple<Args>
     parent_clause2 : [@TraitClause2]: core::marker::Sized<Self::Output>
     type Output
-    fn call_once = core::ops::function::FnOnce::call_once<Self, Args>
+    fn call_once = core::ops::function::FnOnce::call_once<Self, Args>[Self]
 }
 
 fn take_mut::take<'_0, T, F>(@1: &'_0 mut (T), @2: F)
@@ -151,7 +151,9 @@ fn test_cargo_dependencies::main()
     return
 }
 
-fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> Self::Output
+fn core::ops::function::FnOnce::call_once<Self, Args>(@1: Self, @2: Args) -> @TraitClause0::Output
+where
+    [@TraitClause0]: core::ops::function::FnOnce<Self, Args>,
 
 
 

charon/tests/crate_data.rs

@@ -222,6 +222,7 @@ fn predicate_origins() -> anyhow::Result<()> {
         (
             "test_crate::Trait::trait_method",
             vec![
+                (TraitSelf, "Trait"),
                 (WhereClauseOnFn, "Sized"),
                 (WhereClauseOnFn, "From"),
                 (WhereClauseOnFn, "From"),

charon/tests/ui/arrays.out

@@ -254,12 +254,12 @@ trait core::slice::index::SliceIndex<Self, T>
 {
     parent_clause0 : [@TraitClause0]: core::slice::index::private_slice_index::Sealed<Self>
     type Output
-    fn get<'_0> = core::slice::index::SliceIndex::get<'_0_0, Self, T>
-    fn get_mut<'_0> = core::slice::index::SliceIndex::get_mut<'_0_0, Self, T>
-    fn get_unchecked = core::slice::index::SliceIndex::get_unchecked<Self, T>
-    fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut<Self, T>
-    fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T>
-    fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T>
+    fn get<'_0> = core::slice::index::SliceIndex::get<'_0_0, Self, T>[Self]
+    fn get_mut<'_0> = core::slice::index::SliceIndex::get_mut<'_0_0, Self, T>[Self]
+    fn get_unchecked = core::slice::index::SliceIndex::get_unchecked<Self, T>[Self]
+    fn get_unchecked_mut = core::slice::index::SliceIndex::get_unchecked_mut<Self, T>[Self]
+    fn index<'_0> = core::slice::index::SliceIndex::index<'_0_0, Self, T>[Self]
+    fn index_mut<'_0> = core::slice::index::SliceIndex::index_mut<'_0_0, Self, T>[Self]
 }
 
 fn core::slice::index::{impl core::ops::index::Index<I> for Slice<T>}::index<'_0, T, I>(@1: &'_0 (Slice<T>), @2: I) -> &'_0 (@TraitClause2::Output)
@@ -405,7 +405,7 @@ fn test_crate::array_to_slice_mut_<'_0>(@1: &'_0 mut (Array<u32, 32 : usize>)) -
 trait core::ops::index::Index<Self, Idx>
 {
     type Output
-    fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>
+    fn index<'_0> = core::ops::index::Index::index<'_0_0, Self, Idx>[Self]
 }
 
 fn core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>}#15::index<'_0, T, I, const N : usize>(@1: &'_0 (Array<T, const N : usize>), @2: I) -> &'_0 (core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>}#15<T, I, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2]::Output)
@@ -456,7 +456,7 @@ fn test_crate::array_subslice_shared_<'_0>(@1: &'_0 (Array<u32, 32 : usize>), @2
 trait core::ops::index::IndexMut<Self, Idx>
 {
     parent_clause0 : [@TraitClause0]: core::ops::index::Index<Self, Idx>
-    fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx>
+    fn index_mut<'_0> = core::ops::index::IndexMut::index_mut<'_0_0, Self, Idx>[Self]
 }
 
 impl<T, I, const N : usize> core::array::{impl core::ops::index::Index<I> for Array<T, const N : usize>}#15<T, I, const N : usize> : core::ops::index::Index<Array<T, const N : usize>, I>
@@ -1874,9 +1874,13 @@ fn test_crate::slice_pattern_4<'_0>(@1: &'_0 (Slice<()>))
     return
 }
 
-fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output)
+fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (@TraitClause0::Output)
+where
+    [@TraitClause0]: core::ops::index::Index<Self, Idx>,
 
-fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (Self::parent_clause0::Output)
+fn core::ops::index::IndexMut::index_mut<'_0, Self, Idx>(@1: &'_0 mut (Self), @2: Idx) -> &'_0 mut (@TraitClause0::parent_clause0::Output)
+where
+    [@TraitClause0]: core::ops::index::IndexMut<Self, Idx>,
 
 impl<T, I, const N : usize> core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>}#16<T, I, const N : usize> : core::ops::index::IndexMut<Array<T, const N : usize>, I>
 where
@@ -1888,17 +1892,29 @@ where
     fn index_mut<'_0> = core::array::{impl core::ops::index::IndexMut<I> for Array<T, const N : usize>}#16::index_mut<'_0_0, T, I, const N : usize>[@TraitClause0, @TraitClause1, @TraitClause2]
 }
 
-fn core::slice::index::SliceIndex::get<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> core::option::Option<&'_0 (Self::Output)>[core::marker::Sized<&'_0 (Self::Output)>]
+fn core::slice::index::SliceIndex::get<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> core::option::Option<&'_0 (@TraitClause0::Output)>[core::marker::Sized<&'_0 (@TraitClause0::Output)>]
+where
+    [@TraitClause0]: core::slice::index::SliceIndex<Self, T>,
 
-fn core::slice::index::SliceIndex::get_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> core::option::Option<&'_0 mut (Self::Output)>[core::marker::Sized<&'_0 mut (Self::Output)>]
+fn core::slice::index::SliceIndex::get_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> core::option::Option<&'_0 mut (@TraitClause0::Output)>[core::marker::Sized<&'_0 mut (@TraitClause0::Output)>]
+where
+    [@TraitClause0]: core::slice::index::SliceIndex<Self, T>,
 
-unsafe fn core::slice::index::SliceIndex::get_unchecked<Self, T>(@1: Self, @2: *const T) -> *const Self::Output
+unsafe fn core::slice::index::SliceIndex::get_unchecked<Self, T>(@1: Self, @2: *const T) -> *const @TraitClause0::Output
+where
+    [@TraitClause0]: core::slice::index::SliceIndex<Self, T>,
 
-unsafe fn core::slice::index::SliceIndex::get_unchecked_mut<Self, T>(@1: Self, @2: *mut T) -> *mut Self::Output
+unsafe fn core::slice::index::SliceIndex::get_unchecked_mut<Self, T>(@1: Self, @2: *mut T) -> *mut @TraitClause0::Output
+where
+    [@TraitClause0]: core::slice::index::SliceIndex<Self, T>,
 
-fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> &'_0 (Self::Output)
+fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> &'_0 (@TraitClause0::Output)
+where
+    [@TraitClause0]: core::slice::index::SliceIndex<Self, T>,
 
-fn core::slice::index::SliceIndex::index_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> &'_0 mut (Self::Output)
+fn core::slice::index::SliceIndex::index_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> &'_0 mut (@TraitClause0::Output)
+where
+    [@TraitClause0]: core::slice::index::SliceIndex<Self, T>,