Add an explicit Self: Trait clause to trait assoc items

frontend/exporter/src/state.rs

@@ -357,7 +357,7 @@ impl ImplInfos {
                 .impl_trait_ref(did)
                 .map(|trait_ref| trait_ref.instantiate_identity())
                 .sinto(s),
-            clauses: predicates_defined_on(tcx, did).predicates.sinto(s),
+            clauses: predicates_defined_on(tcx, did).as_ref().sinto(s),
         }
     }
 }

frontend/exporter/src/traits.rs

@@ -7,7 +7,7 @@ mod utils;
 #[cfg(feature = "rustc")]
 pub use utils::{
     erase_and_norm, implied_predicates, predicates_defined_on, required_predicates, self_predicate,
-    ToPolyTraitRef,
+    Predicates, ToPolyTraitRef,
 };
 
 #[cfg(feature = "rustc")]
@@ -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 {
@@ -358,12 +360,11 @@ pub fn solve_item_implied_traits<'tcx, S: UnderOwnerState<'tcx>>(
 fn solve_item_traits_inner<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     generics: ty::GenericArgsRef<'tcx>,
-    predicates: ty::GenericPredicates<'tcx>,
+    predicates: utils::Predicates<'tcx>,
 ) -> Vec<ImplExpr> {
     let tcx = s.base().tcx;
     let typing_env = s.typing_env();
     predicates
-        .predicates
         .iter()
         .map(|(clause, _span)| *clause)
         .filter_map(|clause| clause.as_trait_clause())
@@ -387,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

@@ -11,9 +11,10 @@ use rustc_middle::traits::CodegenObligationError;
 use rustc_middle::ty::{self, *};
 use rustc_trait_selection::traits::ImplSource;
 
-use crate::{self_predicate, traits::utils::erase_and_norm};
-
-use super::utils::{implied_predicates, normalize_bound_val, required_predicates, ToPolyTraitRef};
+use super::utils::{
+    self, erase_and_norm, implied_predicates, normalize_bound_val, required_predicates,
+    self_predicate, ToPolyTraitRef,
+};
 
 #[derive(Debug, Clone)]
 pub enum PathChunk<'tcx> {
@@ -153,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,
     ) {
@@ -164,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,
@@ -179,7 +192,6 @@ fn initial_search_predicates<'tcx>(
         }
         predicates.extend(
             required_predicates(tcx, def_id, add_drop)
-                .predicates
                 .iter()
                 .map(|(clause, _span)| *clause)
                 .filter_map(|clause| {
@@ -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
 }
 
@@ -204,7 +216,6 @@ fn parents_trait_predicates<'tcx>(
 ) -> Vec<PolyTraitPredicate<'tcx>> {
     let self_trait_ref = pred.to_poly_trait_ref();
     implied_predicates(tcx, pred.def_id(), add_drop)
-        .predicates
         .iter()
         .map(|(clause, _span)| *clause)
         // Substitute with the `self` args so that the clause makes sense in the
@@ -342,8 +353,8 @@ impl<'tcx> PredicateSearcher<'tcx> {
         };
 
         // The bounds that hold on the associated type.
-        let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.add_drop)
-            .predicates
+        let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.add_drop);
+        let item_bounds = item_bounds
             .iter()
             .map(|(clause, _span)| *clause)
             .filter_map(|pred| pred.as_trait_clause())
@@ -642,13 +653,12 @@ impl<'tcx> PredicateSearcher<'tcx> {
     pub fn resolve_predicates(
         &mut self,
         generics: GenericArgsRef<'tcx>,
-        predicates: GenericPredicates<'tcx>,
+        predicates: utils::Predicates<'tcx>,
         // Call back into hax-related code to display a nice warning.
         warn: &impl Fn(&str),
     ) -> Result<Vec<ImplExpr<'tcx>>, String> {
         let tcx = self.tcx;
         predicates
-            .predicates
             .iter()
             .map(|(clause, _span)| *clause)
             .filter_map(|clause| clause.as_trait_clause())

frontend/exporter/src/traits/utils.rs

@@ -29,23 +29,21 @@
 use rustc_hir::def::DefKind;
 use rustc_middle::ty::*;
 use rustc_span::def_id::DefId;
-use rustc_span::DUMMY_SP;
+use rustc_span::{Span, DUMMY_SP};
+use std::borrow::Cow;
+
+pub type Predicates<'tcx> = Cow<'tcx, [(Clause<'tcx>, Span)]>;
 
 /// Returns a list of type predicates for the definition with ID `def_id`, including inferred
 /// lifetime constraints. This is the basic list of predicates we use for essentially all items.
-pub fn predicates_defined_on(tcx: TyCtxt<'_>, def_id: DefId) -> GenericPredicates<'_> {
-    let mut result = tcx.explicit_predicates_of(def_id);
+pub fn predicates_defined_on(tcx: TyCtxt<'_>, def_id: DefId) -> Predicates<'_> {
+    let mut result = Cow::Borrowed(tcx.explicit_predicates_of(def_id).predicates);
     let inferred_outlives = tcx.inferred_outlives_of(def_id);
     if !inferred_outlives.is_empty() {
-        let inferred_outlives_iter = inferred_outlives
-            .iter()
-            .map(|(clause, span)| ((*clause).upcast(tcx), *span));
-        result.predicates = tcx.arena.alloc_from_iter(
-            result
-                .predicates
-                .into_iter()
-                .copied()
-                .chain(inferred_outlives_iter),
+        result.to_mut().extend(
+            inferred_outlives
+                .iter()
+                .map(|(clause, span)| ((*clause).upcast(tcx), *span)),
         );
     }
     result
@@ -66,7 +64,7 @@ pub fn required_predicates<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: DefId,
     add_drop: bool,
-) -> GenericPredicates<'tcx> {
+) -> Predicates<'tcx> {
     use DefKind::*;
     let def_kind = tcx.def_kind(def_id);
     let mut predicates = match def_kind {
@@ -88,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`.
@@ -103,9 +106,7 @@ pub fn required_predicates<'tcx>(
                 .map(|ty| Binder::dummy(TraitRef::new(tcx, drop_trait, [ty])))
                 .map(|tref| tref.upcast(tcx))
                 .map(|clause| (clause, DUMMY_SP));
-            predicates.predicates = tcx
-                .arena
-                .alloc_from_iter(predicates.predicates.iter().copied().chain(extra_bounds));
+            predicates.to_mut().extend(extra_bounds);
         }
     }
     predicates
@@ -134,36 +135,26 @@ pub fn implied_predicates<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: DefId,
     add_drop: bool,
-) -> GenericPredicates<'tcx> {
+) -> Predicates<'tcx> {
     use DefKind::*;
     let parent = tcx.opt_parent(def_id);
     match tcx.def_kind(def_id) {
         // We consider all predicates on traits to be outputs
         Trait | TraitAlias => predicates_defined_on(tcx, def_id),
         AssocTy if matches!(tcx.def_kind(parent.unwrap()), Trait) => {
-            let mut predicates = GenericPredicates {
-                parent,
-                // `skip_binder` is for the GAT `EarlyBinder`
-                predicates: tcx.explicit_item_bounds(def_id).skip_binder(),
-                ..GenericPredicates::default()
-            };
+            // `skip_binder` is for the GAT `EarlyBinder`
+            let mut predicates = Cow::Borrowed(tcx.explicit_item_bounds(def_id).skip_binder());
             if add_drop {
                 // Add a `Drop` bound to the assoc item.
                 let drop_trait = tcx.lang_items().drop_trait().unwrap();
                 let ty =
                     Ty::new_projection(tcx, def_id, GenericArgs::identity_for_item(tcx, def_id));
                 let tref = Binder::dummy(TraitRef::new(tcx, drop_trait, [ty]));
-                predicates.predicates = tcx.arena.alloc_from_iter(
-                    predicates
-                        .predicates
-                        .iter()
-                        .copied()
-                        .chain([(tref.upcast(tcx), DUMMY_SP)]),
-                );
+                predicates.to_mut().push((tref.upcast(tcx), DUMMY_SP));
             }
             predicates
         }
-        _ => GenericPredicates::default(),
+        _ => Predicates::default(),
     }
 }
 

frontend/exporter/src/types/hir.rs

@@ -830,7 +830,6 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene
             .instantiate_identity()
     } else {
         predicates_defined_on(tcx, s.owner_id())
-            .predicates
             .iter()
             .map(|(x, _span)| x)
             .copied()

frontend/exporter/src/types/ty.rs

@@ -1337,6 +1337,17 @@ pub struct GenericPredicates {
     pub predicates: Vec<(Clause, Span)>,
 }
 
+#[cfg(feature = "rustc")]
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericPredicates>
+    for crate::traits::Predicates<'tcx>
+{
+    fn sinto(&self, s: &S) -> GenericPredicates {
+        GenericPredicates {
+            predicates: self.as_ref().sinto(s),
+        }
+    }
+}
+
 #[cfg(feature = "rustc")]
 impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto<S, Binder<T2>> for ty::Binder<'tcx, T1>
 where

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 =