fix(exporter): improve predicate_equality

When `try_normalize_erasing_regions` fails, regions are not
erased. When comparing predicates, regions never matter: we need to
make sure they are erased (an erased lifetime will show up as `&`
instead of `&'named`).

Also, erased regions still show up in the binder: whence we skip it.

This commit does a last thing: instead of dealing with constness by
replacing in strings, we call `without_const`.

frontend/exporter/src/traits.rs

@@ -127,12 +127,13 @@ pub(crate) mod search_clause {
         s: &S,
     ) -> bool {
         let tcx = s.base().tcx;
-        let x = tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x);
-        let y = tcx.try_normalize_erasing_regions(param_env, y).unwrap_or(y);
-        // Below: "~const " may appear in the string, and comes from the way the
-        // trait ref is internalized by rustc. We remove such occurrences (yes, this is sad).
-        let sx = format!("{:?}", x).replace("~const ", "");
-        let sy = format!("{:?}", y).replace("~const ", "");
+        let erase_and_norm =
+            |x| tcx.erase_regions(tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x));
+        // Lifetime and constantness are irrelevant when resolving instances
+        let x = erase_and_norm(x).without_const(tcx);
+        let y = erase_and_norm(y).without_const(tcx);
+        let sx = format!("{:?}", x.kind().skip_binder());
+        let sy = format!("{:?}", y.kind().skip_binder());
         let result = sx == sy;
         const DEBUG: bool = false;
         if DEBUG && result {

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

@@ -29,6 +29,23 @@ Compiling traits v0.1.0 (WORKSPACE_ROOT/traits)
 diagnostics = []
 
 [stdout.files]
+"Traits.For_clauses.fst" = '''
+module Traits.For_clauses
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_Foo (v_Self: Type0) (v_T: Type0) = {
+  f_to_t_pre:v_Self -> bool;
+  f_to_t_post:v_Self -> v_T -> bool;
+  f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result)
+}
+
+let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X)
+    : Prims.unit =
+  let _:u8 = f_to_t x in
+  ()
+'''
 "Traits.fst" = '''
 module Traits
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

tests/traits/src/lib.rs

@@ -77,3 +77,13 @@ impl Error {
         || Self::Fail
     }
 }
+
+mod for_clauses {
+    trait Foo<T> {
+        fn to_t(&self) -> T;
+    }
+
+    fn _f<X: for<'a> Foo<&'a u8>>(x: X) {
+        x.to_t();
+    }
+}