Merge pull request #1220 from hacspec/fix-1218

Visit trait goals to rename impl expr they may contain.
hacspec · Jan 7, 2025 · 98ded93 · 98ded93
2 parents 4d7cbff + 249fed3
commit 98ded93
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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 {}
+}