diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index 1c149404f..42f8ac9fb 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -226,9 +226,14 @@ 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 value = Hashtbl.find s name in + let new_name = + Option.value_or_thunk value ~default:(fun () -> + let data = "i" ^ Int.to_string (Hashtbl.length s) in + let _ = Hashtbl.add s ~key:name ~data in + data) + in + GCType { goal; name = new_name } | _ -> super#visit_generic_constraint (enabled, s) gc method! visit_trait_item (_, s) = super#visit_trait_item (true, s) 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; N]); fn f(_: Defaults) {} } + +/// See https://github.com/hacspec/hax/issues/1176 +mod impl_generics { + struct Test(); + + impl Test { + fn set_ciphersuites(&self, ciphers: impl IntoIterator) -> Result<(), ()> + where + S: AsRef, + { + Ok(()) + } + + fn set_alpn_protocols(&self, _protocols: impl IntoIterator) -> Result<(), ()> + where + S: AsRef, + { + Ok(()) + } + } +}