Merge pull request #712 from hacspec/fstar-uniform-marker-trait

fix(backends/fstar): no `__marker_trait` if parent bounds
hacspec · Jun 13, 2024 · 2db0e69 · 2db0e69
2 parents 6f3325e + ad92b26
commit 2db0e69
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -1324,18 +1324,18 @@ struct
                        parent_bounds)
             items
         in
-        let fields =
-          if List.is_empty fields then
-            [ (F.lid [ "__marker_trait" ], pexpr (U.unit_expr e.span)) ]
-          else fields
-        in
         let parent_bounds_fields =
           List.map
             ~f:(fun (_impl_expr, impl_ident) ->
               (F.lid [ "_super_" ^ impl_ident.name ], F.tc_solve))
             parent_bounds
         in
         let fields = parent_bounds_fields @ fields in
+        let fields =
+          if List.is_empty fields then
+            [ (F.lid [ "__marker_trait" ], pexpr (U.unit_expr e.span)) ]
+          else fields
+        in
         let body = F.term @@ F.AST.Record (None, fields) in
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
         F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ]