Repository: cryspen/hax (language: rust)

Issue:
Naming bug with generic constraint on associated types
```rust
trait T1 {
    type Assoc;
}

trait T2 {}

impl<U: T1> T2 for U where U::Assoc : T2 {}


```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar+tc/f47b2ae440/gist=c23e295f24de541a0e87120618b620f8)



Discussion / hints:

Fix patch:
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
 


Test patch:
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 {}
+}