From a17cd49f0dc109063ed7cac7b0b4191213bffffd Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 10 Jul 2024 11:06:40 +0200
Subject: [PATCH] fix(engine/f*): `{| ... |}` for trait bounds on types

---
 engine/backends/fstar/fstar_backend.ml                 | 10 ++++++----
 .../src/snapshots/toolchain__traits into-fstar.snap    |  2 +-
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index db89c2435..b9d4185b5 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -640,7 +640,9 @@ struct
     type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term }
 
     let make_explicit x = { x with kind = Explicit }
-    let make_implicit x = { x with kind = Implicit }
+
+    let implicit_to_explicit x =
+      if [%matches? Tcresolve] x.kind then x else make_explicit x
 
     let of_generic_param span (p : generic_param) : t =
       let ident = plocal_ident p.ident in
@@ -1034,7 +1036,7 @@ struct
                  F.AST.TyconRecord
                    ( F.id @@ U.Concrete_ident_view.to_definition_name name,
                      FStarBinder.of_generics e.span generics
-                     |> List.map ~f:FStarBinder.make_explicit
+                     |> List.map ~f:FStarBinder.implicit_to_explicit
                      |> List.map ~f:FStarBinder.to_binder,
                      None,
                      [],
@@ -1101,7 +1103,7 @@ struct
                  F.AST.TyconVariant
                    ( F.id @@ U.Concrete_ident_view.to_definition_name name,
                      FStarBinder.of_generics e.span generics
-                     |> List.map ~f:FStarBinder.make_explicit
+                     |> List.map ~f:FStarBinder.implicit_to_explicit
                      |> List.map ~f:FStarBinder.to_binder,
                      None,
                      constructors );
@@ -1299,7 +1301,7 @@ struct
             List.map
               ~f:
                 FStarBinder.(
-                  of_generic_param e.span >> make_explicit >> to_binder)
+                  of_generic_param e.span >> implicit_to_explicit >> to_binder)
               generics.params
           in
           F.AST.TyconRecord (name_id, bds, None, [], fields)
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 13c1c318a..81f7fa2f2 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -432,7 +432,7 @@ module Traits.Type_alias_bounds_issue_707_
 open Core
 open FStar.Mul
 
-type t_StructWithGenericBounds (v_T: Type0) (i1: Core.Clone.t_Clone v_T) =
+type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} =
   | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T
 '''
 "Traits.Unconstrainted_types_issue_677_.fst" = '''