fix(engine/f*): {| ... |} for trait bounds on types

hacspec · Jul 10, 2024 · a17cd49 · a17cd49
1 parent 9f056df
commit a17cd49
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git 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
@@ -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" = '''