From 364d2a4dec4adbeee85abc0e193329193575c17d Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 15 May 2024 08:12:09 +0200
Subject: [PATCH 1/5] refactor(exporter): split `new` into multiple modules

---
 .../types/{new.rs => new/item_attributes.rs}   | 17 -----------------
 frontend/exporter/src/types/new/mod.rs         |  8 ++++++++
 .../src/types/new/typed_constant_kind.rs       | 18 ++++++++++++++++++
 3 files changed, 26 insertions(+), 17 deletions(-)
 rename frontend/exporter/src/types/{new.rs => new/item_attributes.rs} (77%)
 create mode 100644 frontend/exporter/src/types/new/mod.rs
 create mode 100644 frontend/exporter/src/types/new/typed_constant_kind.rs

diff --git a/frontend/exporter/src/types/new.rs b/frontend/exporter/src/types/new/item_attributes.rs
similarity index 77%
rename from frontend/exporter/src/types/new.rs
rename to frontend/exporter/src/types/new/item_attributes.rs
index e67658032..bfaa141d1 100644
--- a/frontend/exporter/src/types/new.rs
+++ b/frontend/exporter/src/types/new/item_attributes.rs
@@ -1,16 +1,5 @@
 use crate::prelude::*;
 
-impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto<S, TypedConstantKind>
-    for rustc_middle::mir::ConstantKind<'tcx>
-{
-    fn sinto(&self, s: &S) -> TypedConstantKind {
-        TypedConstantKind {
-            typ: self.ty().sinto(s),
-            constant_kind: self.sinto(s),
-        }
-    }
-}
-
 #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
 pub struct ItemAttributes {
     attributes: Vec<Attribute>,
@@ -26,12 +15,6 @@ impl ItemAttributes {
     }
 }
 
-#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
-pub struct TypedConstantKind {
-    pub typ: Ty,
-    pub constant_kind: ConstantExpr,
-}
-
 lazy_static::lazy_static! {
     pub static ref CORE_EXTRACTION_MODE: bool =
         std::env::var_os("HAX_CORE_EXTRACTION_MODE") == Some("on".into());
diff --git a/frontend/exporter/src/types/new/mod.rs b/frontend/exporter/src/types/new/mod.rs
new file mode 100644
index 000000000..53b88f8c9
--- /dev/null
+++ b/frontend/exporter/src/types/new/mod.rs
@@ -0,0 +1,8 @@
+//! This module contains type definitions that have no equivalent in
+//! Rustc.
+
+mod item_attributes;
+mod typed_constant_kind;
+
+pub use item_attributes::*;
+pub use typed_constant_kind::*;
diff --git a/frontend/exporter/src/types/new/typed_constant_kind.rs b/frontend/exporter/src/types/new/typed_constant_kind.rs
new file mode 100644
index 000000000..734abc240
--- /dev/null
+++ b/frontend/exporter/src/types/new/typed_constant_kind.rs
@@ -0,0 +1,18 @@
+use crate::prelude::*;
+
+#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
+pub struct TypedConstantKind {
+    pub typ: Ty,
+    pub constant_kind: ConstantExpr,
+}
+
+impl<'tcx, S: BaseState<'tcx> + HasOwnerId> SInto<S, TypedConstantKind>
+    for rustc_middle::mir::ConstantKind<'tcx>
+{
+    fn sinto(&self, s: &S) -> TypedConstantKind {
+        TypedConstantKind {
+            typ: self.ty().sinto(s),
+            constant_kind: self.sinto(s),
+        }
+    }
+}

From 153c4967032ac5399bb8bf53a49579bae78b355a Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 15 May 2024 08:21:35 +0200
Subject: [PATCH 2/5] fix(exporter): cargo doc: enable
 `--document-private-items`

---
 cli/default.nix              | 1 +
 frontend/exporter/src/lib.rs | 1 +
 2 files changed, 2 insertions(+)

diff --git a/cli/default.nix b/cli/default.nix
index a90ffb13d..369f2182a 100644
--- a/cli/default.nix
+++ b/cli/default.nix
@@ -58,6 +58,7 @@
   );
   frontend-docs = craneLib.cargoDoc (commonArgs // {
     preBuildPhases = ["addRustcDocs"];
+    cargoDocExtraArgs = "--document-private-items";
     addRustcDocs = ''
       mkdir -p target/doc
       cp --no-preserve=mode -rf ${rustc.passthru.availableComponents.rustc-docs}/share/doc/rust/html/rustc/* target/doc/
diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs
index c79d378aa..f15880286 100644
--- a/frontend/exporter/src/lib.rs
+++ b/frontend/exporter/src/lib.rs
@@ -9,6 +9,7 @@
 #![allow(incomplete_features)]
 #![feature(specialization)]
 #![feature(return_position_impl_trait_in_trait)]
+#![allow(rustdoc::private_intra_doc_links)]
 
 extern crate rustc_abi;
 extern crate rustc_ast;

From a9e63c38b5cd433c26651f214e570211565f0563 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 15 May 2024 08:31:16 +0200
Subject: [PATCH 3/5] feat(exporter): introduce `PredicateId`

---
 frontend/exporter/src/types/new/mod.rs        |  2 +
 .../exporter/src/types/new/predicate_id.rs    | 65 +++++++++++++++++++
 2 files changed, 67 insertions(+)
 create mode 100644 frontend/exporter/src/types/new/predicate_id.rs

diff --git a/frontend/exporter/src/types/new/mod.rs b/frontend/exporter/src/types/new/mod.rs
index 53b88f8c9..ca52e55ac 100644
--- a/frontend/exporter/src/types/new/mod.rs
+++ b/frontend/exporter/src/types/new/mod.rs
@@ -2,7 +2,9 @@
 //! Rustc.
 
 mod item_attributes;
+mod predicate_id;
 mod typed_constant_kind;
 
 pub use item_attributes::*;
+pub use predicate_id::*;
 pub use typed_constant_kind::*;
diff --git a/frontend/exporter/src/types/new/predicate_id.rs b/frontend/exporter/src/types/new/predicate_id.rs
new file mode 100644
index 000000000..04fa8b49d
--- /dev/null
+++ b/frontend/exporter/src/types/new/predicate_id.rs
@@ -0,0 +1,65 @@
+use crate::prelude::*;
+use rustc_middle::ty;
+
+#[derive(
+    Copy, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+#[serde(transparent)]
+/// A `PredicateId` is a unique identifier for a clause or a
+/// predicate. It is computed by hashing predicates and clause in a
+/// uniform and deterministic way.
+pub struct PredicateId(u64);
+
+/// Implemented by anything that can be assimilated to a predicate.
+pub trait IntoPredicateId<'tcx, S: UnderOwnerState<'tcx>> {
+    /// Compute a consistent `PredicateId`
+    fn predicate_id(&self, s: &S) -> PredicateId;
+}
+
+impl<'tcx, S: UnderOwnerState<'tcx>> IntoPredicateId<'tcx, S> for ty::Clause<'tcx> {
+    fn predicate_id(&self, s: &S) -> PredicateId {
+        self.as_predicate().predicate_id(s)
+    }
+}
+
+impl<'tcx, S: UnderOwnerState<'tcx>> IntoPredicateId<'tcx, S> for ty::Predicate<'tcx> {
+    fn predicate_id(&self, s: &S) -> PredicateId {
+        // Here, we need to be careful about not hashing a `crate::Predicate`,
+        // but `crate::Binder<crate::PredicateKind>` instead,
+        // otherwise we would get into a infinite recursion.
+        let poly_kind: Binder<PredicateKind> = self.kind().sinto(s);
+        PredicateId(deterministic_hash(&poly_kind))
+    }
+}
+
+impl<'tcx, S: UnderOwnerState<'tcx>> IntoPredicateId<'tcx, S> for ty::PolyTraitPredicate<'tcx> {
+    fn predicate_id(&self, s: &S) -> PredicateId {
+        use ty::ToPredicate;
+        let predicate: ty::Predicate<'tcx> = (*self).to_predicate(s.base().tcx);
+        predicate.predicate_id(s)
+    }
+}
+
+/// A `PredicateId` can be mapped to itself via SInto. This is useful
+/// for mirroring the type [`traits::search_clause::PathChunk`] as
+/// [`traits::ImplExprPathChunk`].
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, PredicateId> for PredicateId {
+    fn sinto(&self, _s: &S) -> PredicateId {
+        *self
+    }
+}
+
+/// We need identifiers that are stable across different
+/// architectures, different paths (which are observable from
+/// `Span`s), etc.
+/// Rustc's stable hash is not doing what we want here: it is sensible
+/// to the environment. Instead, we first `sinto` and then hash with
+/// `deterministic_hash` below.
+fn deterministic_hash<T: std::hash::Hash>(x: &T) -> u64 {
+    use crate::deterministic_hash::DeterministicHasher;
+    use std::collections::hash_map::DefaultHasher;
+    use std::hash::Hasher;
+    let mut hasher = DeterministicHasher::new(DefaultHasher::new());
+    x.hash(&mut hasher);
+    hasher.finish()
+}

From ade0cfe030108ef4c1ea707eefcdea738a01358f Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 15 May 2024 08:35:05 +0200
Subject: [PATCH 4/5] feat(exporter): drop clause ids, use `PredicateId` both
 on `Predicate`s and `Clause`s

In commit [fca56a], the type `Clause` has been renamed as
`ClauseKind`, then commit [21226e] makes `Clause` a
`Binder<ClauseKind>`, essentially (with an indirection via
`PredicateKind` and an invariant where the predicate kind has to be a
`ty::PredicateKind::Clause(ClauseKind)`).

That means that now, Rustc always provides `Clause` with
binders. Thus, it now makes sense to systematically compute clause
identifiers with binders.

Since clauses are a subset of predicates, we now always lift clauses
to predicates before computing identifiers. This was not possible
before, since we lacked binder information to properly lift clauses to
predicates

[fca56a]: https://github.com/rust-lang/rust/commit/fca56a8d2c6f803aeec51167dd4dd22529f8bdd7
[21226e]: https://github.com/rust-lang/rust/commit/21226eefb2e2465b9730c37e7d08655865610d90
---
 engine/lib/concrete_ident/impl_infos.ml | 17 +++---
 engine/lib/import_thir.ml               | 39 ++++++-------
 engine/lib/import_thir.mli              |  4 +-
 frontend/exporter/src/state.rs          | 10 +---
 frontend/exporter/src/traits.rs         | 74 +++++--------------------
 frontend/exporter/src/types/copied.rs   | 59 ++++++++------------
 6 files changed, 71 insertions(+), 132 deletions(-)

diff --git a/engine/lib/concrete_ident/impl_infos.ml b/engine/lib/concrete_ident/impl_infos.ml
index da1257d4e..57a6a915c 100644
--- a/engine/lib/concrete_ident/impl_infos.ml
+++ b/engine/lib/concrete_ident/impl_infos.ml
@@ -6,8 +6,8 @@ type t = {
          [impl] block is an {{: https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations } inherent [impl]}.
         *)
   typ : Ast.Rust.ty;  (** The type implemented by the [impl] block. *)
-  predicates : Ast.Rust.trait_goal list;
-      (** The predicates that constraint this [impl] block. *)
+  clauses : Ast.Rust.trait_goal list;
+      (** The clauses that constraint this [impl] block. *)
 }
 (** metadata of an [impl] block *)
 
@@ -20,17 +20,18 @@ issue 363}, when looking up certain identifiers generated by the
 engine, this function may return [None] even though the supplied
 identifier points to an [Impl] block. *)
 let lookup span (impl : Concrete_ident.t) : t option =
-  let* Types.{ generics = _; predicates; typ; trait_ref } =
+  let* Types.{ generics = _; clauses; typ; trait_ref } =
     Concrete_ident.lookup_raw_impl_info impl
   in
   let trait_goal =
     Option.map ~f:(Import_thir.import_trait_ref span) trait_ref
   in
   let typ = Import_thir.import_ty span typ in
-  let predicates =
-    let f (binder : Types.binder_for__predicate_kind) =
-      Import_thir.import_predicate_kind span binder.value
+  let clauses =
+    let f ((binder : Types.clause), span) =
+      Import_thir.import_clause span binder
     in
-    List.filter_map ~f predicates
+    List.filter_map ~f clauses
+    |> List.map ~f:(fun (i : Ast.Rust.impl_ident) -> i.goal)
   in
-  Some { trait_goal; typ; predicates }
+  Some { trait_goal; typ; clauses }
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 77bb64069..8f92693bc 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -225,7 +225,6 @@ module type EXPR = sig
   val c_param : Thir.span -> Thir.param -> param
   val c_trait_item' : Thir.trait_item -> Thir.trait_item_kind -> trait_item'
   val c_trait_ref : Thir.span -> Thir.trait_ref -> trait_goal
-  val c_predicate_kind : Thir.span -> Thir.predicate_kind -> trait_goal option
   val c_impl_expr : Thir.span -> Thir.impl_expr -> impl_expr
   val c_clause : Thir.span -> Thir.clause -> impl_ident option
 end
@@ -968,15 +967,21 @@ end) : EXPR = struct
     let browse_path (impl : impl_expr) (chunk : Thir.impl_expr_path_chunk) =
       match chunk with
       | AssocItem
-          { item; predicate = { value = { trait_ref; _ }; _ }; clause_id; _ } ->
-          let ident = { goal = c_trait_ref span trait_ref; name = clause_id } in
+          { item; predicate = { value = { trait_ref; _ }; _ }; predicate_id; _ }
+        ->
+          let ident =
+            { goal = c_trait_ref span trait_ref; name = predicate_id }
+          in
           let kind : Concrete_ident.Kind.t =
             match item.kind with Const | Fn -> Value | Type -> Type
           in
           let item = Concrete_ident.of_def_id kind item.def_id in
           Projection { impl; ident; item }
-      | Parent { predicate = { value = { trait_ref; _ }; _ }; clause_id; _ } ->
-          let ident = { goal = c_trait_ref span trait_ref; name = clause_id } in
+      | Parent { predicate = { value = { trait_ref; _ }; _ }; predicate_id; _ }
+        ->
+          let ident =
+            { goal = c_trait_ref span trait_ref; name = predicate_id }
+          in
           Parent { impl; ident }
     in
     match ie with
@@ -984,8 +989,8 @@ end) : EXPR = struct
         let trait = Concrete_ident.of_def_id Impl id in
         let args = List.map ~f:(c_generic_value span) generics in
         Concrete { trait; args }
-    | LocalBound { clause_id; path; _ } ->
-        let init = LocalBound { id = clause_id } in
+    | LocalBound { predicate_id; path; _ } ->
+        let init = LocalBound { id = predicate_id } in
         List.fold ~init ~f:browse_path path
     | Dyn -> Dyn
     | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path
@@ -1042,8 +1047,7 @@ end) : EXPR = struct
     let attrs = c_attrs param.attributes in
     { ident; span; attrs; kind }
 
-  let c_clause span (p : Thir.clause) : impl_ident option =
-    let ({ kind; id } : Thir.clause) = p in
+  let c_clause_kind span id (kind : Thir.clause_kind) : impl_ident option =
     match kind with
     | Trait { is_positive = true; is_const = _; trait_ref } ->
         let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in
@@ -1051,11 +1055,9 @@ end) : EXPR = struct
         Some { goal = { trait; args }; name = id }
     | _ -> None
 
-  let c_predicate_kind' span (p : Thir.predicate_kind) : impl_ident option =
-    match p with Clause clause -> c_clause span clause | _ -> None
-
-  let c_predicate_kind span (p : Thir.predicate_kind) : trait_goal option =
-    c_predicate_kind' span p |> Option.map ~f:(fun (x : impl_ident) -> x.goal)
+  let c_clause span (p : Thir.clause) : impl_ident option =
+    let ({ kind; id } : Thir.clause) = p in
+    c_clause_kind span id kind.value
 
   let list_dedup (equal : 'a -> 'a -> bool) : 'a list -> 'a list =
     let rec aux (seen : 'a list) (todo : 'a list) : 'a list =
@@ -1069,7 +1071,7 @@ end) : EXPR = struct
 
   let c_generics (generics : Thir.generics) : generics =
     let bounds =
-      List.filter_map ~f:(c_predicate_kind' generics.span) generics.bounds
+      List.filter_map ~f:(c_clause generics.span) generics.bounds
       |> List.map ~f:(fun impl_ident -> GCType impl_ident)
     in
     {
@@ -1098,7 +1100,7 @@ end) : EXPR = struct
         in
         TIFn (TArrow (inputs, output))
     | Type (bounds, None) ->
-        let bounds = List.filter_map ~f:(c_predicate_kind' span) bounds in
+        let bounds = List.filter_map ~f:(c_clause span) bounds in
         TIType bounds
     | Type (_, Some _) ->
         unimplemented [ span ]
@@ -1115,9 +1117,8 @@ include struct
   let import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal =
     c_trait_ref
 
-  let import_predicate_kind :
-      Types.span -> Types.predicate_kind -> Ast.Rust.trait_goal option =
-    c_predicate_kind
+  let import_clause : Types.span -> Types.clause -> Ast.Rust.impl_ident option =
+    c_clause
 end
 
 (** Instantiate the functor for translating expressions. The crate
diff --git a/engine/lib/import_thir.mli b/engine/lib/import_thir.mli
index 2ab0c3e5e..2d0374a63 100644
--- a/engine/lib/import_thir.mli
+++ b/engine/lib/import_thir.mli
@@ -1,8 +1,6 @@
 val import_ty : Types.span -> Types.ty -> Ast.Rust.ty
 val import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal
-
-val import_predicate_kind :
-  Types.span -> Types.predicate_kind -> Ast.Rust.trait_goal option
+val import_clause : Types.span -> Types.clause -> Ast.Rust.impl_ident option
 
 val import_item :
   drop_body:bool ->
diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs
index 6cec3638e..26e1fc4f6 100644
--- a/frontend/exporter/src/state.rs
+++ b/frontend/exporter/src/state.rs
@@ -236,7 +236,7 @@ pub trait UnderOwnerState<'tcx> = BaseState<'tcx> + HasOwnerId;
 #[derive(Clone, Debug, Serialize, Deserialize, JsonSchema)]
 pub struct ImplInfos {
     pub generics: TyGenerics,
-    pub predicates: Vec<Predicate>,
+    pub clauses: Vec<(Clause, Span)>,
     pub typ: Ty,
     pub trait_ref: Option<TraitRef>,
 }
@@ -246,17 +246,11 @@ impl ImplInfos {
         let tcx = base.tcx;
         let s = &with_owner_id(base, (), (), did);
 
-        let predicates = tcx
-            .predicates_defined_on(did)
-            .predicates
-            .iter()
-            .map(|(clause, _)| clause.as_predicate().sinto(s))
-            .collect();
         Self {
             generics: tcx.generics_of(did).sinto(s),
             typ: tcx.type_of(did).subst_identity().sinto(s),
             trait_ref: tcx.impl_trait_ref(did).sinto(s),
-            predicates,
+            clauses: tcx.predicates_defined_on(did).predicates.sinto(s),
         }
     }
 }
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 8492ce736..fab6f50a4 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -9,12 +9,12 @@ pub enum ImplExprPathChunk {
     AssocItem {
         item: AssocItem,
         predicate: Binder<TraitPredicate>,
-        clause_id: u64,
+        predicate_id: PredicateId,
         index: usize,
     },
     Parent {
         predicate: Binder<TraitPredicate>,
-        clause_id: u64,
+        predicate_id: PredicateId,
         index: usize,
     },
 }
@@ -32,7 +32,7 @@ pub enum ImplExprAtom {
     },
     /// A context-bound clause like `where T: Trait`.
     LocalBound {
-        clause_id: u64,
+        predicate_id: PredicateId,
         r#trait: Binder<TraitRef>,
         path: Vec<ImplExprPathChunk>,
     },
@@ -70,9 +70,11 @@ pub struct ImplExpr {
     pub args: Vec<ImplExpr>,
 }
 
-mod search_clause {
+// FIXME: this has visibility `pub(crate)` only because of https://github.com/rust-lang/rust/issues/83049
+pub(crate) mod search_clause {
     use crate::prelude::UnderOwnerState;
     use crate::rustc_utils::*;
+    use crate::{IntoPredicateId, PredicateId};
     use rustc_middle::ty::*;
 
     fn predicates_to_poly_trait_predicates<'tcx>(
@@ -90,12 +92,12 @@ mod search_clause {
         AssocItem {
             item: AssocItem,
             predicate: PolyTraitPredicate<'tcx>,
-            clause_id: u64,
+            predicate_id: PredicateId,
             index: usize,
         },
         Parent {
             predicate: PolyTraitPredicate<'tcx>,
-            clause_id: u64,
+            predicate_id: PredicateId,
             index: usize,
         },
     }
@@ -224,10 +226,7 @@ mod search_clause {
                         cons(
                             PathChunk::Parent {
                                 predicate: p,
-                                clause_id: {
-                                    use rustc_middle::ty::ToPredicate;
-                                    crate::clause_id_of_predicate(s, p.to_predicate(s.base().tcx))
-                                },
+                                predicate_id: p.predicate_id(s),
                                 index,
                             },
                             path,
@@ -244,13 +243,7 @@ mod search_clause {
                                     cons(
                                         PathChunk::AssocItem {
                                             item,
-                                            clause_id: {
-                                                use rustc_middle::ty::ToPredicate;
-                                                crate::clause_id_of_predicate(
-                                                    s,
-                                                    p.to_predicate(s.base().tcx),
-                                                )
-                                            },
+                                            predicate_id: p.predicate_id(s),
                                             predicate: p,
                                             index,
                                         },
@@ -374,7 +367,7 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> {
                         .with_args(impl_exprs(s, &nested), trait_ref)
                 } else {
                     ImplExprAtom::LocalBound {
-                        clause_id: clause_id_of_predicate(s, apred.predicate),
+                        predicate_id: apred.predicate.predicate_id(s),
                         r#trait,
                         path,
                     }
@@ -410,59 +403,22 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>(
     let impl_trait_ref = tcx
         .impl_trait_ref(impl_did)
         .map(|binder| rustc_middle::ty::Binder::dummy(binder.subst_identity()))?;
-    let original_clause_id = {
+    let original_predicate_id = {
         // We don't want the id of the substituted clause id, but the
         // original clause id (with, i.e., `Self`)
         let s = &with_owner_id(s.base(), (), (), impl_trait_ref.def_id());
-        // We compute the id of the clause without binder.
-        let clause: Clause = clause.kind().skip_binder().sinto(s);
-        clause.id
+        clause.predicate_id(s)
     };
     let new_clause = clause.subst_supertrait(tcx, &impl_trait_ref);
     let impl_expr = new_clause
         .as_predicate()
         .to_opt_poly_trait_pred()?
         .impl_expr(s, get_param_env(s));
-    // Build the new clause, again without binder.
-    let mut new_clause_no_binder: Clause = new_clause.kind().skip_binder().sinto(s);
-    new_clause_no_binder.id = original_clause_id;
+    let mut new_clause_no_binder = new_clause.sinto(s);
+    new_clause_no_binder.id = original_predicate_id;
     Some((new_clause_no_binder, impl_expr, span.sinto(s)))
 }
 
-fn deterministic_hash<T: std::hash::Hash>(x: &T) -> u64 {
-    use crate::deterministic_hash::DeterministicHasher;
-    use std::collections::hash_map::DefaultHasher;
-    use std::hash::Hasher;
-    let mut hasher = DeterministicHasher::new(DefaultHasher::new());
-    x.hash(&mut hasher);
-    hasher.finish()
-}
-
-/// Crafts a unique identifier for a predicate by hashing it. The hash
-/// is non-trivial because we need stable identifiers: two hax
-/// extraction of a same predicate should result in the same
-/// identifier. Rustc's stable hash is not doing what we want here: it
-/// is sensible to the environment. Instead, we convert the (rustc)
-/// predicate to `crate::Predicate` and hash from there.
-#[tracing::instrument(level = "trace", skip(s))]
-pub fn clause_id_of_predicate<'tcx, S: UnderOwnerState<'tcx>>(
-    s: &S,
-    predicate: rustc_middle::ty::Predicate<'tcx>,
-) -> u64 {
-    let predicate = predicate.sinto(s);
-    match &predicate.value {
-        // Instead of recursively hashing the clause, we reuse the already-computed id.
-        PredicateKind::Clause(clause) => clause.id,
-        _ => deterministic_hash(&(1u8, predicate)),
-    }
-}
-
-/// Used when building a `crate::Clause`. See [`clause_id_of_predicate`] for what we're doing here.
-#[tracing::instrument(level = "trace")]
-pub fn clause_id_of_bound_clause_kind(binder: &Binder<ClauseKind>) -> u64 {
-    deterministic_hash(&(0u8, binder))
-}
-
 #[tracing::instrument(level = "trace", skip(s))]
 pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index 51008319b..8a2b1ce26 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -3275,35 +3275,39 @@ pub enum ClauseKind {
     TypeWellFormedFromEnv(Ty),
 }
 
-/// Reflects [`rustc_middle::ty::ClauseKind`] and adds a hash-consed clause identifier.
+/// Reflects [`rustc_middle::ty::Clause`] and adds a hash-consed predicate identifier.
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
 pub struct Clause {
-    pub kind: ClauseKind,
-    pub id: u64,
+    pub kind: Binder<ClauseKind>,
+    pub id: PredicateId,
 }
 
-impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause>
-    for rustc_middle::ty::Binder<'tcx, rustc_middle::ty::ClauseKind<'tcx>>
-{
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for rustc_middle::ty::Clause<'tcx> {
     fn sinto(&self, s: &S) -> Clause {
-        // FIXME: `ClauseKind::sinto` uses a dummy binder. We need it because `Predicate::sinto()`
-        // doesn't propagate the binder to the `ClauseKind`. This might cause inconsistencies. It
-        // might be that we don't want to hash the binder at all.
-        let binder: Binder<ClauseKind> = self.sinto(s);
-        let id = clause_id_of_bound_clause_kind(&binder);
         Clause {
-            kind: binder.value,
-            id,
+            kind: self.kind().sinto(s),
+            id: self.predicate_id(s),
         }
     }
 }
 
-impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for rustc_middle::ty::ClauseKind<'tcx> {
-    fn sinto(&self, s: &S) -> Clause {
-        // FIXME: this is dangerous.
-        rustc_middle::ty::Binder::dummy(self.clone()).sinto(s)
+/// Reflects [`rustc_middle::ty::Predicate`] and adds a hash-consed predicate identifier.
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub struct Predicate {
+    pub kind: Binder<PredicateKind>,
+    pub id: PredicateId,
+}
+
+impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Predicate> for rustc_middle::ty::Predicate<'tcx> {
+    fn sinto(&self, s: &S) -> Predicate {
+        Predicate {
+            kind: self.kind().sinto(s),
+            id: self.predicate_id(s),
+        }
     }
 }
 
@@ -3341,9 +3345,6 @@ pub struct GenericPredicates {
     pub predicates: Vec<(Predicate, Span)>,
 }
 
-/// Reflects [`rustc_middle::ty::Predicate`]
-pub type Predicate = Binder<PredicateKind>;
-
 impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto<S, Binder<T2>>
     for rustc_middle::ty::Binder<'tcx, T1>
 where
@@ -3356,12 +3357,6 @@ where
     }
 }
 
-impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Predicate> for rustc_middle::ty::Predicate<'tcx> {
-    fn sinto(&self, s: &S) -> Predicate {
-        self.kind().sinto(s)
-    }
-}
-
 /// Reflects [`rustc_middle::ty::SubtypePredicate`]
 #[derive(AdtInto)]
 #[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_middle::ty::SubtypePredicate<'tcx>, state: S as tcx)]
@@ -3415,7 +3410,7 @@ pub enum ClosureKind {
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
 pub enum PredicateKind {
-    Clause(Clause),
+    Clause(ClauseKind),
     ObjectSafe(DefId),
     ClosureKind(DefId, Vec<GenericArg>, ClosureKind),
     Subtype(SubtypePredicate),
@@ -3426,7 +3421,7 @@ pub enum PredicateKind {
 }
 
 /// Reflects [`rustc_hir::GenericBounds`]
-type GenericBounds = Vec<PredicateKind>;
+type GenericBounds = Vec<Clause>;
 
 /// Compute the bounds for the owner registed in the state `s`
 fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> GenericBounds {
@@ -3467,13 +3462,7 @@ fn region_bounds_at_current_owner<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> Gene
             .copied()
             .collect()
     };
-    clauses
-        .iter()
-        .map(|clause| {
-            tcx.erase_late_bound_regions(clause.as_predicate().kind())
-                .sinto(s)
-        })
-        .collect()
+    clauses.sinto(s)
 }
 
 impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericBounds> for rustc_hir::GenericBounds<'tcx> {

From e259b1799561068b19e034cb2fab85c256259f09 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 15 May 2024 08:54:55 +0200
Subject: [PATCH 5/5] chore: refresh test snapshots

---
 .../src/snapshots/toolchain__traits into-fstar.snap    | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 703fd638b..b3f7449b3 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -62,7 +62,7 @@ class t_Lang (v_Self: Type0) = {
 }
 
 class t_SuperTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4075428158603710007:Core.Clone.t_Clone v_Self;
+  [@@@ FStar.Tactics.Typeclasses.no_method]_super_10391689928755043351:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> bool;
   f_function_of_super_trait_post:v_Self -> u32 -> bool;
   f_function_of_super_trait:x0: v_Self
@@ -74,7 +74,7 @@ class t_SuperTrait (v_Self: Type0) = {
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_SuperTrait_for_i32: t_SuperTrait i32 =
   {
-    _super_4075428158603710007 = FStar.Tactics.Typeclasses.solve;
+    _super_10391689928755043351 = FStar.Tactics.Typeclasses.solve;
     f_function_of_super_trait_pre = (fun (self: i32) -> true);
     f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
@@ -82,8 +82,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 =
 
 class t_Foo (v_Self: Type0) = {
   f_AssocType:Type0;
-  f_AssocType_12975176671554111340:t_SuperTrait f_AssocType;
-  f_AssocType_15292246028710717365:Core.Clone.t_Clone f_AssocType;
+  f_AssocType_1566547207180513319:t_SuperTrait f_AssocType;
+  f_AssocType_18427724250319916167:Core.Clone.t_Clone f_AssocType;
   f_N:usize;
   f_assoc_f_pre:Prims.unit -> bool;
   f_assoc_f_post:Prims.unit -> Prims.unit -> bool;
@@ -130,7 +130,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
 let impl_Foo_for_tuple_: t_Foo Prims.unit =
   {
     f_AssocType = i32;
-    f_AssocType_12975176671554111340 = FStar.Tactics.Typeclasses.solve;
+    f_AssocType_1566547207180513319 = FStar.Tactics.Typeclasses.solve;
     f_N = sz 32;
     f_assoc_f_pre = (fun (_: Prims.unit) -> true);
     f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);