Add an explicit Self: Trait clause to trait assoc items

This way, the special `ImplExpr::SelfImpl` is only valid within a trait
declaration.

Author: Nadrieril

frontend/exporter/src/traits.rs

@@ -290,7 +290,9 @@ pub fn translate_item_ref<'tcx, S: UnderOwnerState<'tcx>>(
         let num_trait_generics = trait_ref.generic_args.len();
         generic_args.drain(0..num_trait_generics);
         let num_trait_trait_clauses = trait_ref.impl_exprs.len();
-        impl_exprs.drain(0..num_trait_trait_clauses);
+        // Associated items take a `Self` clause as first clause, we skip that one too. Note: that
+        // clause is the same as `tinfo`.
+        impl_exprs.drain(0..num_trait_trait_clauses + 1);
     }
 
     let content = ItemRefContents {
@@ -386,15 +388,14 @@ pub fn self_clause_for_item<'tcx, S: UnderOwnerState<'tcx>>(
     def_id: RDefId,
     generics: rustc_middle::ty::GenericArgsRef<'tcx>,
 ) -> Option<ImplExpr> {
-    use rustc_middle::ty::EarlyBinder;
     let tcx = s.base().tcx;
 
     let tr_def_id = tcx.trait_of_item(def_id)?;
     // The "self" predicate in the context of the trait.
     let self_pred = self_predicate(tcx, tr_def_id);
     // Substitute to be in the context of the current item.
     let generics = generics.truncate_to(tcx, tcx.generics_of(tr_def_id));
-    let self_pred = EarlyBinder::bind(self_pred).instantiate(tcx, generics);
+    let self_pred = ty::EarlyBinder::bind(self_pred).instantiate(tcx, generics);
 
     // Resolve
     Some(solve_trait(s, self_pred))

frontend/exporter/src/traits/resolution.rs

@@ -154,6 +154,7 @@ fn initial_search_predicates<'tcx>(
         tcx: TyCtxt<'tcx>,
         def_id: rustc_span::def_id::DefId,
         add_drop: bool,
+        include_self_pred: bool,
         predicates: &mut Vec<AnnotatedTraitPred<'tcx>>,
         pred_id: &mut usize,
     ) {
@@ -165,11 +166,22 @@ fn initial_search_predicates<'tcx>(
         use DefKind::*;
         match tcx.def_kind(def_id) {
             // These inherit some predicates from their parent.
-            AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant => {
+            dk @ (AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant) => {
                 let parent = tcx.parent(def_id);
-                acc_predicates(tcx, parent, add_drop, predicates, pred_id);
+                // Hack: we don't support GATs well so for now we let assoc types refer to the
+                // implicit trait `Self` clause. Other associated items get an explicit `Self:
+                // Trait` clause passed to them so they don't need that.
+                let include_self_pred = include_self_pred && matches!(dk, AssocTy);
+                acc_predicates(
+                    tcx,
+                    parent,
+                    add_drop,
+                    include_self_pred,
+                    predicates,
+                    pred_id,
+                );
             }
-            Trait | TraitAlias => {
+            Trait | TraitAlias if include_self_pred => {
                 let self_pred = self_predicate(tcx, def_id).upcast(tcx);
                 predicates.push(AnnotatedTraitPred {
                     origin: BoundPredicateOrigin::SelfPred,
@@ -192,7 +204,7 @@ fn initial_search_predicates<'tcx>(
     }
 
     let mut predicates = vec![];
-    acc_predicates(tcx, def_id, add_drop, &mut predicates, &mut 0);
+    acc_predicates(tcx, def_id, add_drop, true, &mut predicates, &mut 0);
     predicates
 }
 

frontend/exporter/src/traits/utils.rs

@@ -86,6 +86,11 @@ pub fn required_predicates<'tcx>(
         // `predicates_defined_on` ICEs on other def kinds.
         _ => Default::default(),
     };
+    // For associated items in trait definitions, we add an explicit `Self: Trait` clause.
+    if let Some(trait_def_id) = tcx.trait_of_item(def_id) {
+        let self_clause = self_predicate(tcx, trait_def_id).upcast(tcx);
+        predicates.to_mut().insert(0, (self_clause, DUMMY_SP));
+    }
     if add_drop {
         // Add a `T: Drop` bound for every generic, unless the current trait is `Drop` itself, or
         // `Sized`.

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -661,9 +661,18 @@ class t_Foo (v_Self: Type0) = {
   f_method_f_post:v_Self -> Prims.unit -> Type0;
   f_method_f:x0: v_Self
     -> Prims.Pure Prims.unit (f_method_f_pre x0) (fun result -> f_method_f_post x0 result);
-  f_assoc_type_pre:{| i2: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Type0;
-  f_assoc_type_post:{| i2: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> Type0;
-  f_assoc_type:{| i2: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType
+  f_assoc_type_pre:
+      {| i2: Core.Marker.t_Copy v_5081411602995720689.f_AssocType |} ->
+      v_5081411602995720689.f_AssocType
+    -> Type0;
+  f_assoc_type_post:
+      {| i2: Core.Marker.t_Copy v_5081411602995720689.f_AssocType |} ->
+      v_5081411602995720689.f_AssocType ->
+      Prims.unit
+    -> Type0;
+  f_assoc_type:
+      {| i2: Core.Marker.t_Copy v_5081411602995720689.f_AssocType |} ->
+      x0: v_5081411602995720689.f_AssocType
     -> Prims.Pure Prims.unit
         (f_assoc_type_pre #i2 x0)
         (fun result -> f_assoc_type_post #i2 x0 result)
@@ -672,9 +681,11 @@ class t_Foo (v_Self: Type0) = {
 class t_Lang (v_Self: Type0) = {
   f_Var:Type0;
   f_s_pre:v_Self -> i32 -> Type0;
-  f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> Type0;
+  f_s_post:v_Self -> i32 -> (v_Self & v_178762381425797165.f_Var) -> Type0;
   f_s:x0: v_Self -> x1: i32
-    -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result)
+    -> Prims.Pure (v_Self & v_178762381425797165.f_Var)
+        (f_s_pre x0 x1)
+        (fun result -> f_s_post x0 x1 result)
 }
 
 let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit =