Allow opaque types even without interface mode.

cryspen · Nov 28, 2024 · eb63300 · eb63300
1 parent 7f28b35
commit eb63300
Showing 1 changed file with 8 additions and 21 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -995,27 +995,14 @@ struct
                    ty );
                ] )
     | Type { name; generics; _ } when is_erased ->
-        if not ctx.interface_mode then
-          Error.raise
-          @@ {
-               kind =
-                 AttributeRejected
-                   {
-                     reason =
-                       "a type cannot be opaque if its module is not extracted \
-                        as an interface";
-                   };
-               span = e.span;
-             }
-        else
-          let generics = FStarBinder.of_generics e.span generics in
-          let ty = F.type0_term in
-          let arrow_typ =
-            F.term
-            @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
-          in
-          let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
-          [ F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) ]
+        let generics = FStarBinder.of_generics e.span generics in
+        let ty = F.type0_term in
+        let arrow_typ =
+          F.term
+          @@ F.AST.Product (List.map ~f:FStarBinder.to_binder generics, ty)
+        in
+        let name = F.id @@ U.Concrete_ident_view.to_definition_name name in
+        [ F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) ]
     | Type
         {
           name;