Repository: cryspen/hax (language: rust)

Issue:
Generated F* with two type-class arguments named `i4`
```rust
struct Test();

impl Test {
    fn set_ciphersuites<S>(&self, ciphers: impl IntoIterator<Item = S>) -> Result<(), ()>
    where
        S: AsRef<str>, {
            Ok(())
        }

    fn set_alpn_protocols<S>(&self, _protocols: impl IntoIterator<Item = S>) -> Result<(), ()>
    where
    S: AsRef<str>,
    {
        Ok(())
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/de59826b83/gist=bac89b5a8752a73fcec9d867e6135a3a)

In this example, the generated F* for `set_alpn_protocols` has the following two arguments with a name clash:
```
(#[FStar.Tactics.Typeclasses.tcresolve
            ()]
          i4:
          Core.Convert.t_AsRef v_S string)
 (#[FStar.Tactics.Typeclasses.tcresolve
            ()]
          i4:
          Core.Iter.Traits.Collect.t_IntoIterator
          impl_995885649_)
```
Note that this doesn't happen if `set_ciphersuites` is removed.


Discussion / hints:
I understood how this happens. The root of the bug is [here](https://github.com/hacspec/hax/blob/main/engine/lib/ast_utils.ml#L230) where we rename generic type constraints (we get them with an identifier). We assume that these identifiers are unique, but in the case of impls, two different methods can have the same generic constraints with the same identifier. This means we insert a second binding for the same key in the hashmap, so the hashmap length doesn't increase and the next `iN` name we generate is the same.

I think it is quite straightforward to fix. We should check if the identifier is already present in the hashmap. And if it is return the same name. This means the same constraints in two different methods of the same impl will get the same name but they won't collide because they belong to different scopes.

Fix patch:
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 1c149404f..34c37f867 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -226,9 +226,11 @@ module Make (F : Features.T) = struct
             ((enabled, s) : bool * (string, string) Hashtbl.t) gc =
           match gc with
           | GCType { goal; name } when enabled ->
-              let data = "i" ^ Int.to_string (Hashtbl.length s) in
-              let _ = Hashtbl.add s ~key:name ~data in
-              GCType { goal; name = data }
+              let new_name =
+                Hashtbl.find_or_add s name ~default:(fun () ->
+                    "i" ^ Int.to_string (Hashtbl.length s))
+              in
+              GCType { goal; name = new_name }
           | _ -> super#visit_generic_constraint (enabled, s) gc
 
         method! visit_trait_item (_, s) = super#visit_trait_item (true, s)


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index fa558e443..26fe6fce5 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -37,6 +37,36 @@ type t_Defaults (v_T: Type0) (v_N: usize) = | Defaults : t_Array v_T v_N -> t_De
 
 let f (_: t_Defaults Prims.unit (sz 2)) : Prims.unit = ()
 '''
+"Generics.Impl_generics.fst" = '''
+module Generics.Impl_generics
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Test = | Test : t_Test
+
+let impl__Test__set_alpn_protocols
+      (#v_S #impl_995885649_: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Convert.t_AsRef v_S string)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Core.Iter.Traits.Collect.t_IntoIterator impl_995885649_)
+      (self: t_Test)
+      (v__protocols: impl_995885649_)
+    : Core.Result.t_Result Prims.unit Prims.unit =
+  Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
+
+let impl__Test__set_ciphersuites
+      (#v_S #impl_995885649_: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Convert.t_AsRef v_S string)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i3:
+          Core.Iter.Traits.Collect.t_IntoIterator impl_995885649_)
+      (self: t_Test)
+      (ciphers: impl_995885649_)
+    : Core.Result.t_Result Prims.unit Prims.unit =
+  Core.Result.Result_Ok (() <: Prims.unit) <: Core.Result.t_Result Prims.unit Prims.unit
+'''
 "Generics.fst" = '''
 module Generics
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/generics/src/lib.rs b/tests/generics/src/lib.rs
index cb14662fd..131c8da89 100644
--- a/tests/generics/src/lib.rs
+++ b/tests/generics/src/lib.rs
@@ -51,3 +51,24 @@ mod defaults_generics {
     struct Defaults<T = (), const N: usize = 2>([T; N]);
     fn f(_: Defaults) {}
 }
+
+/// See https://github.com/hacspec/hax/issues/1176
+mod impl_generics {
+    struct Test();
+
+    impl Test {
+        fn set_ciphersuites<S>(&self, ciphers: impl IntoIterator<Item = S>) -> Result<(), ()>
+        where
+            S: AsRef<str>,
+        {
+            Ok(())
+        }
+
+        fn set_alpn_protocols<S>(&self, _protocols: impl IntoIterator<Item = S>) -> Result<(), ()>
+        where
+            S: AsRef<str>,
+        {
+            Ok(())
+        }
+    }
+}