diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml
index 0ead59bd5..0906c846c 100644
--- a/engine/backends/fstar/fstar_ast.ml
+++ b/engine/backends/fstar/fstar_ast.ml
@@ -9,6 +9,7 @@ module Ident = FStar_Ident
 
 let dummyRange = Range.dummyRange
 let id ident = Ident.mk_ident (ident, dummyRange)
+let id_prime (ident : Ident.ident) = id (ident.idText ^ "'")
 
 let lid path =
   let init, last = List.(drop_last_exn path, last_exn path) in
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index f179ffe38..f70275899 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -874,6 +874,26 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
+    let is_opaque =
+      Attrs.find_unique_attr e.attrs
+        ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
+      |> Option.is_some
+    in
+    let opaque_impl name ty attrs =
+      let name' = F.id_prime name in
+
+      [
+        F.decl ~quals:[ Assumption ] ~fsti:false ~attrs
+        @@ F.AST.Assume (name', ty);
+        F.decl ~fsti:false
+        @@ F.AST.TopLevelLet
+             ( NoLetQualifier,
+               [
+                 ( F.pat @@ F.AST.PatVar (name, None, []),
+                   F.term @@ F.AST.Var (F.lid_of_id @@ name') );
+               ] );
+      ]
+    in
     match e.v with
     | Alias { name; item } ->
         (* These should come from bundled items (in the case of cyclic module dependencies).
@@ -938,7 +958,10 @@ struct
         in
 
         let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
-        if interface_mode then [ impl; intf ] else [ full ]
+
+        if is_opaque then intf :: opaque_impl name arrow_typ []
+        else if interface_mode then [ impl; intf ]
+        else [ full ]
     | TyAlias { name; generics; ty } ->
         let pat =
           F.pat
@@ -971,10 +994,7 @@ struct
                             |> List.map ~f:to_pattern) ),
                    ty );
                ] )
-    | Type { name; generics; _ }
-      when Attrs.find_unique_attr e.attrs
-             ~f:([%eq: Types.ha_payload] OpaqueType >> Fn.flip Option.some_if ())
-           |> Option.is_some ->
+    | Type { name; generics; _ } when is_opaque ->
         if not ctx.interface_mode then
           Error.raise
           @@ {
@@ -1471,18 +1491,13 @@ struct
         in
         let body = F.term @@ F.AST.Record (None, fields) in
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
-        let has_type =
-          List.exists items ~f:(fun { ii_v; _ } ->
-              match ii_v with IIType _ -> true | _ -> false)
-        in
-        let impl_val = ctx.interface_mode && not has_type in
         let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
-        if impl_val then
+        if is_opaque then
           let generics_binders = List.map ~f:FStarBinder.to_binder generics in
           let val_type = F.term @@ F.AST.Product (generics_binders, typ) in
           let v = F.AST.Val (name, val_type) in
           (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v)
-          @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl
+          @ opaque_impl name val_type [ tcinst ]
         else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl
     | Quote { quote; _ } ->
         let fstar_opts =
@@ -1529,8 +1544,7 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
               let ctx = ctx
             end) : S)
 
-let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) :
+let strings_of_item (bo : BackendOptions.t) m items (item : item) :
     ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
@@ -1548,8 +1562,7 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
     |> Option.value ~default:(Types.Excluded : Types.inclusion_kind)
   in
   let interface_mode =
-    signature_only
-    || not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
+    not ([%matches? (Types.Excluded : Types.inclusion_kind)] interface_mode')
   in
   let (module Print) =
     make m
@@ -1560,21 +1573,18 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
         line_width = bo.line_width;
       }
   in
-  let mk_impl = if interface_mode then fun i -> `Impl i else fun i -> `Impl i in
+  let mk_impl i = `Impl i in
   let mk_intf = if interface_mode then fun i -> `Intf i else fun i -> `Impl i in
   let no_impl =
-    signature_only
-    || [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
+    [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode'
   in
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
        | `Impl i -> [ (mk_impl (Print.decl_to_string i), `Newline) ]
        | `Intf i -> [ (mk_intf (Print.decl_to_string i), `Newline) ]
-       | `VerbatimIntf (s, nl) ->
-           [ ((if interface_mode then `Intf s else `Impl s), nl) ]
-       | `VerbatimImpl (s, nl) ->
-           [ ((if interface_mode then `Impl s else `Impl s), nl) ]
+       | `VerbatimIntf (s, nl) -> [ (mk_intf s, nl) ]
+       | `VerbatimImpl (s, nl) -> [ (`Impl s, nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
@@ -1582,8 +1592,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
 
 type rec_prefix = NonRec | FirstMutRec | MutRec
 
-let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
-    items : string * string =
+let string_of_items ~mod_name ~bundles (bo : BackendOptions.t) m items :
+    string * string =
   let collect_trait_goal_idents =
     object
       inherit [_] Visitors.reduce as super
@@ -1656,7 +1666,7 @@ let string_of_items ~signature_only ~mod_name ~bundles (bo : BackendOptions.t) m
     List.concat_map
       ~f:(fun item ->
         let recursivity_prefix = get_recursivity_prefix item in
-        let strs = strings_of_item ~signature_only bo m items item in
+        let strs = strings_of_item bo m items item in
         match (recursivity_prefix, item.v) with
         | FirstMutRec, Fn _ ->
             replace_in_strs ~pattern:"let" ~with_:"let rec" strs
@@ -1709,20 +1719,8 @@ let translate_as_fstar m (bo : BackendOptions.t) ~(bundles : AST.item list list)
   U.group_items_by_namespace items
   |> Map.to_alist
   |> List.concat_map ~f:(fun (ns, items) ->
-         let signature_only =
-           let is_dropped_body =
-             Concrete_ident.eq_name Rust_primitives__hax__dropped_body
-           in
-           let contains_dropped_body =
-             U.Reducers.collect_concrete_idents#visit_item ()
-             >> Set.exists ~f:is_dropped_body
-           in
-           List.exists ~f:contains_dropped_body items
-         in
          let mod_name = module_name ns in
-         let impl, intf =
-           string_of_items ~signature_only ~mod_name ~bundles bo m items
-         in
+         let impl, intf = string_of_items ~mod_name ~bundles bo m items in
          let make ~ext body =
            if String.is_empty body then None
            else
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 3b1c6e56b..95778622b 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -630,8 +630,7 @@ module Make (Options : OPTS) : MAKE = struct
               if
                 Attrs.find_unique_attr item.attrs
                   ~f:
-                    ([%eq: Types.ha_payload] OpaqueType
-                    >> Fn.flip Option.some_if ())
+                    ([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
                 |> Option.is_some
               then default_lines
               else default_lines ^^ destructor_lines
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index 944089d01..5695dd087 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -36,14 +36,14 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
             include_clauses
           |> List.last
         in
-        let drop_body =
+        let type_only =
           (* Shall we drop the body? *)
           Option.map
             ~f:(fun clause -> [%matches? Types.SignatureOnly] clause.kind)
             most_precise_clause
           |> Option.value ~default:false
         in
-        Import_thir.import_item ~drop_body item)
+        Import_thir.import_item ~type_only item)
       items
     |> List.map ~f:snd
   in
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index f1f2550db..34f9624a5 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1440,26 +1440,49 @@ let cast_of_enum typ_name generics typ thir_span
   in
   { v; span; ident; attrs = [] }
 
-let rec c_item ~ident ~drop_body (item : Thir.item) : item list =
+let rec c_item ~ident ~type_only (item : Thir.item) : item list =
   try
     Span.with_owner_hint item.owner_id (fun _ ->
-        c_item_unwrapped ~ident ~drop_body item)
+        c_item_unwrapped ~ident ~type_only item)
   with Diagnostics.SpanFreeError.Exn payload ->
     let context, kind = Diagnostics.SpanFreeError.payload payload in
     let error = Diagnostics.pretty_print_context_kind context kind in
     let span = Span.of_thir item.span in
     [ make_hax_error_item span ident error ]
 
-and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
+and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list =
   let open (val make ~krate:item.owner_id.contents.value.krate : EXPR) in
   if should_skip item.attributes then []
   else
     let span = Span.of_thir item.span in
     let attrs = c_item_attrs item.attributes in
+    let erased_by_user =
+      Attr_payloads.payloads attrs
+      |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)])
+    in
+    let erased_by_type_only =
+      type_only
+      &&
+      match item.kind with
+      | Fn _ | Static _ -> true
+      | Impl { of_trait = Some _; items; _ }
+        when List.exists items ~f:(fun item ->
+                 match item.kind with Type _ -> true | _ -> false)
+             |> not ->
+          true
+      | _ -> false
+    in
+    let attrs =
+      if erased_by_type_only && not erased_by_user then
+        Attr_payloads.to_attr Erased span :: attrs
+      else attrs
+    in
+    let erased = erased_by_user || erased_by_type_only in
+
     let mk_one v = { span; v; ident; attrs } in
     let mk v = [ mk_one v ] in
     let drop_body =
-      drop_body
+      erased
       && Attr_payloads.payloads attrs
          |> List.exists
               ~f:(fst >> [%matches? (NeverDropBody : Types.ha_payload)])
@@ -1475,7 +1498,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                name =
                  Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
                generics = c_generics generics;
-               body = c_expr body;
+               body = c_body body;
                params = [];
                safety = Safe;
              }
@@ -1499,6 +1522,12 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                params = c_fn_params item.span params;
                safety = csafety safety;
              }
+    | (Enum (_, generics, _) | Struct (_, generics)) when erased ->
+        let generics = c_generics generics in
+        let is_struct = match item.kind with Struct _ -> true | _ -> false in
+        let def_id = Option.value_exn item.def_id in
+        let name = Concrete_ident.of_def_id Type def_id in
+        mk @@ Type { name; generics; variants = []; is_struct }
     | Enum (variants, generics, repr) ->
         let def_id = Option.value_exn item.def_id in
         let generics = c_generics generics in
@@ -1681,11 +1710,65 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
             ~f:(fun { attributes; _ } -> not (should_skip attributes))
             items
         in
-        let has_type =
-          List.exists items ~f:(fun item ->
-              match item.kind with Type _ -> true | _ -> false)
+        let items =
+          if erased then
+            [
+              {
+                ii_span = Span.of_thir item.span;
+                ii_generics = { params = []; constraints = [] };
+                ii_v =
+                  IIFn
+                    {
+                      body = U.unit_expr span;
+                      params = [ U.make_unit_param span ];
+                    };
+                ii_ident =
+                  Concrete_ident.of_name Value
+                    Rust_primitives__hax__dropped_body;
+                ii_attrs = [];
+              };
+            ]
+          else
+            List.map
+              ~f:(fun (item : Thir.impl_item) ->
+                (* TODO: introduce a Kind.TraitImplItem or
+                   something. Otherwise we have to assume every
+                   backend will see traits and impls as
+                   records. See https://github.com/hacspec/hax/issues/271. *)
+                let ii_ident = Concrete_ident.of_def_id Field item.owner_id in
+                {
+                  ii_span = Span.of_thir item.span;
+                  ii_generics = c_generics item.generics;
+                  ii_v =
+                    (match (item.kind : Thir.impl_item_kind) with
+                    | Fn { body; params; _ } ->
+                        let params =
+                          if List.is_empty params then
+                            [ U.make_unit_param span ]
+                          else List.map ~f:(c_param item.span) params
+                        in
+                        IIFn { body = c_expr body; params }
+                    | Const (_ty, e) -> IIFn { body = c_expr e; params = [] }
+                    | Type { ty; parent_bounds } ->
+                        IIType
+                          {
+                            typ = c_ty item.span ty;
+                            parent_bounds =
+                              List.filter_map
+                                ~f:(fun (clause, impl_expr, span) ->
+                                  let* bound = c_clause span clause in
+                                  match bound with
+                                  | GCType trait_goal ->
+                                      Some
+                                        (c_impl_expr span impl_expr, trait_goal)
+                                  | _ -> None)
+                                parent_bounds;
+                          });
+                  ii_ident;
+                  ii_attrs = c_item_attrs item.attributes;
+                })
+              items
         in
-        let c_e = if has_type then c_expr else c_body in
         mk
         @@ Impl
              {
@@ -1695,49 +1778,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                  ( Concrete_ident.of_def_id Trait of_trait.def_id,
                    List.map ~f:(c_generic_value item.span) of_trait.generic_args
                  );
-               items =
-                 List.map
-                   ~f:(fun (item : Thir.impl_item) ->
-                     (* TODO: introduce a Kind.TraitImplItem or
-                        something. Otherwise we have to assume every
-                        backend will see traits and impls as
-                        records. See https://github.com/hacspec/hax/issues/271. *)
-                     let ii_ident =
-                       Concrete_ident.of_def_id Field item.owner_id
-                     in
-                     {
-                       ii_span = Span.of_thir item.span;
-                       ii_generics = c_generics item.generics;
-                       ii_v =
-                         (match (item.kind : Thir.impl_item_kind) with
-                         | Fn { body; params; _ } ->
-                             let params =
-                               if List.is_empty params then
-                                 [ U.make_unit_param span ]
-                               else List.map ~f:(c_param item.span) params
-                             in
-                             IIFn { body = c_e body; params }
-                         | Const (_ty, e) -> IIFn { body = c_e e; params = [] }
-                         | Type { ty; parent_bounds } ->
-                             IIType
-                               {
-                                 typ = c_ty item.span ty;
-                                 parent_bounds =
-                                   List.filter_map
-                                     ~f:(fun (clause, impl_expr, span) ->
-                                       let* bound = c_clause span clause in
-                                       match bound with
-                                       | GCType trait_goal ->
-                                           Some
-                                             ( c_impl_expr span impl_expr,
-                                               trait_goal )
-                                       | _ -> None)
-                                     parent_bounds;
-                               });
-                       ii_ident;
-                       ii_attrs = c_item_attrs item.attributes;
-                     })
-                   items;
+               items;
                parent_bounds =
                  List.filter_map
                    ~f:(fun (clause, impl_expr, span) ->
@@ -1787,7 +1828,7 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
     | TraitAlias _ ->
         mk NotImplementedYet
 
-let import_item ~drop_body (item : Thir.item) :
+let import_item ~type_only (item : Thir.item) :
     concrete_ident * (item list * Diagnostics.t list) =
   let ident = Concrete_ident.of_def_id Value item.owner_id in
   let r, reports =
@@ -1797,6 +1838,6 @@ let import_item ~drop_body (item : Thir.item) :
       >> U.Reducers.disambiguate_local_idents
     in
     Diagnostics.Core.capture (fun _ ->
-        c_item item ~ident ~drop_body |> List.map ~f)
+        c_item item ~ident ~type_only |> List.map ~f)
   in
   (ident, (r, reports))
diff --git a/engine/lib/import_thir.mli b/engine/lib/import_thir.mli
index 42a5f2184..370af4c05 100644
--- a/engine/lib/import_thir.mli
+++ b/engine/lib/import_thir.mli
@@ -5,6 +5,6 @@ val import_clause :
   Types.span -> Types.clause -> Ast.Rust.generic_constraint option
 
 val import_item :
-  drop_body:bool ->
+  type_only:bool ->
   Types.item_for__decorated_for__expr_kind ->
   Concrete_ident.t * (Ast.Rust.item list * Diagnostics.t list)
diff --git a/hax-lib/macros/src/dummy.rs b/hax-lib/macros/src/dummy.rs
index 5134763c6..8b40ac9b3 100644
--- a/hax-lib/macros/src/dummy.rs
+++ b/hax-lib/macros/src/dummy.rs
@@ -29,6 +29,7 @@ identity_proc_macro_attribute!(
     process_init,
     process_write,
     process_read,
+    opaque,
     opaque_type,
     refinement_type,
     fstar_replace,
diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs
index f71f1891c..4874b1671 100644
--- a/hax-lib/macros/src/implementation.rs
+++ b/hax-lib/macros/src/implementation.rs
@@ -621,9 +621,18 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr
 /// type without revealing its definition.
 #[proc_macro_error]
 #[proc_macro_attribute]
-pub fn opaque_type(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+#[deprecated(note = "Please use 'opaque' instead")]
+pub fn opaque_type(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+    opaque(attr, item)
+}
+
+/// Mark a struct or an enum opaque: the extraction will assume the
+/// type without revealing its definition.
+#[proc_macro_error]
+#[proc_macro_attribute]
+pub fn opaque(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
     let item: Item = parse_macro_input!(item);
-    let attr = AttrPayload::OpaqueType;
+    let attr = AttrPayload::Erased;
     quote! {#attr #item}.into()
 }
 
diff --git a/hax-lib/macros/types/src/lib.rs b/hax-lib/macros/types/src/lib.rs
index bbb1d4575..0b12b90a8 100644
--- a/hax-lib/macros/types/src/lib.rs
+++ b/hax-lib/macros/types/src/lib.rs
@@ -130,8 +130,8 @@ pub enum AttrPayload {
     PVConstructor,
     PVHandwritten,
     TraitMethodNoPrePost,
-    /// Make a type opaque
-    OpaqueType,
+    /// Make something opaque
+    Erased,
 }
 
 pub const HAX_TOOL: &str = "_hax";
diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs
index 866c7cfda..d5f0684a3 100644
--- a/hax-lib/src/proc_macros.rs
+++ b/hax-lib/src/proc_macros.rs
@@ -2,8 +2,8 @@
 //! proc-macro crate cannot export anything but procedural macros.
 
 pub use hax_lib_macros::{
-    attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type,
-    refinement_type, requires, trait_fn_decoration,
+    attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque,
+    opaque_type, refinement_type, requires, trait_fn_decoration,
 };
 
 pub use hax_lib_macros::{