More improvements to trait resolution

engine/hax-engine.opam

@@ -1,5 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+version: "0.1.0-alpha.1"
 synopsis: "The engine of hax, a Rust verification tool"
 description:
   "Hax is divided in two: a frontend (written in Rust) and an engine (written in OCaml). This is the engine."

frontend/exporter/src/constant_utils.rs

@@ -374,7 +374,7 @@ mod rustc {
         let name = assoc.name.to_string();
 
         // Retrieve the trait information
-        let impl_expr = get_trait_info(s, generics, assoc);
+        let impl_expr = self_clause_for_item(s, assoc, generics).unwrap();
 
         ConstantExprKind::TraitConst { impl_expr, name }
     }

frontend/exporter/src/rustc_utils.rs

@@ -12,17 +12,6 @@ impl<'tcx, T: ty::TypeFoldable<ty::TyCtxt<'tcx>>> ty::Binder<'tcx, T> {
     }
 }
 
-// TODO: this seems to be constructing a `Self: Trait` clause. Document what it does exactly.
-pub fn poly_trait_ref<'tcx, S: UnderOwnerState<'tcx>>(
-    s: &S,
-    assoc: &ty::AssocItem,
-    generics: ty::GenericArgsRef<'tcx>,
-) -> Option<ty::PolyTraitRef<'tcx>> {
-    let tcx = s.base().tcx;
-    let r#trait = tcx.trait_of_item(assoc.def_id)?;
-    Some(ty::Binder::dummy(ty::TraitRef::new(tcx, r#trait, generics)))
-}
-
 #[tracing::instrument(skip(s))]
 pub(crate) fn arrow_of_sig<'tcx, S: UnderOwnerState<'tcx>>(sig: &ty::PolyFnSig<'tcx>, s: &S) -> Ty {
     Ty::Arrow(Box::new(sig.sinto(s)))