From 365aebfce96663b1ef22cbdd6ffc76a40e03022e Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 15 May 2024 17:59:32 +0200
Subject: [PATCH] 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                 | 13 +++++++------
 .../snapshots/toolchain__traits into-fstar.snap | 17 +++++++++++++++++
 tests/traits/src/lib.rs                         | 10 ++++++++++
 3 files changed, 34 insertions(+), 6 deletions(-)

diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index ff9fef100..ad42e6d98 100644
--- a/frontend/exporter/src/traits.rs
+++ b/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 {
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index b3f7449b3..f1eeafa27 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/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"
diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
index bf6e56704..48d64cb65 100644
--- a/tests/traits/src/lib.rs
+++ b/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();
+    }
+}