From 249fed3e93c6041c3b86392597b0e3e97cbd9e15 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Tue, 7 Jan 2025 10:49:50 +0100
Subject: [PATCH] Visit trait goals to rename impl expr they may contain.

---
 engine/lib/ast_utils.ml                         |  1 +
 .../snapshots/toolchain__traits into-fstar.snap | 17 +++++++++++++++++
 tests/traits/src/lib.rs                         | 11 +++++++++++
 3 files changed, 29 insertions(+)

diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 9c7f2984e..899221e21 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -230,6 +230,7 @@ module Make (F : Features.T) = struct
                 Hashtbl.find_or_add s name ~default:(fun () ->
                     "i" ^ Int.to_string (Hashtbl.length s))
               in
+              let goal = super#visit_trait_goal (enabled, s) goal in
               GCType { goal; name = new_name }
           | _ -> super#visit_generic_constraint (enabled, s) gc
 
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index aa66a93db..9e505d3a1 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -157,6 +157,23 @@ let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X
   let _:u8 = f_to_t #v_X #u8 #FStar.Tactics.Typeclasses.solve x in
   ()
 '''
+"Traits.Impl_expr_in_goal.fst" = '''
+module Traits.Impl_expr_in_goal
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_T2 (v_Self: Type0) = { __marker_trait_t_T2:Prims.unit }
+
+class t_T1 (v_Self: Type0) = { f_Assoc:Type0 }
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl
+      (#v_U: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_T1 v_U)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: t_T2 i1.f_Assoc)
+    : t_T2 v_U = { __marker_trait = () }
+'''
 "Traits.Implicit_dependencies_issue_667_.Define_type.fst" = '''
 module Traits.Implicit_dependencies_issue_667_.Define_type
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs
index 9fea11184..1e38b06f0 100644
--- a/tests/traits/src/lib.rs
+++ b/tests/traits/src/lib.rs
@@ -295,3 +295,14 @@ mod default_traits_parameters {
     }
     trait Bar<T = <Self as Foo>::U> {}
 }
+
+// issue 1218
+mod impl_expr_in_goal {
+    trait T1 {
+        type Assoc;
+    }
+
+    trait T2 {}
+
+    impl<U: T1> T2 for U where U::Assoc: T2 {}
+}