Repository: cryspen/hax (language: rust)

Issue:
Cyclic dependency introduced by bundling with `let open`
```rust
pub mod a {
    #[derive(Debug)]
    pub struct S {}
    pub struct Sa(super::b::Sb);
    impl std::fmt::Debug for Sa {
        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
            write!(f, "{:?}", self.0)
        }
    }

}

pub mod b {
    pub struct Sb(super::a::S);
    impl std::fmt::Debug for Sb {
        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
            write!(f, "{:?}", self.0)
        }
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/001a27e207/gist=5c43e496c5fdf2dd5a8f47540b2ba269)

In the situation above, the recursive bundle contains a `let open` for one of the original modules creating a cycle.


Discussion / hints:
Can this be related to https://github.com/hacspec/hax/issues/1068?
> Can this be related to [#1068](https://github.com/hacspec/hax/issues/1068)?

I need to investigate more. This one is about `impl_expr`, I think it is more a problem of not renaming things. The other one is about actually moving definitions to the bundle so I think it is a bit different.
I found a way to minimize even more:

```rust
pub mod a {
    #[derive(Debug)]
    pub struct S {}
   fn f(_x:super::b::Sb) {}

}

pub mod b {
    pub struct Sb(super::a::S);
    impl std::fmt::Debug for Sb {
        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
            write!(f, "{:?}", self.0)
        }
    }
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/001a27e207/gist=8dabf6a7eda9f80401b2b9c4e3b8c3c1)

The problem seems to come from the `impl_expr` for the `derive(Debug)` for `S`
So the problem is that we filter out automatically generated items in `import_thir`, including derived trait impls. Some impl_expr still refer to them but as they don't exist in the engine we don't move them to the bundle, so we don't rename the references to them, thus creating a fake implicit dependency.
After discussing this, we should:
- Change the filtering to replace the method implementations by panics
- Not filter all generated code. We can add some filters (we should at least filter `serde::{Serialize, Deserialize}`). Eventually these filters should be configurable with the cli (with a good default value). 
Related issue: https://github.com/hacspec/hax/issues/108
I am testing my implementation of this. One problem in the case of `Debug` is that `Debug` and `Formatter` both belong to `core::fmt` and have a method `fmt` which means we get https://github.com/hacspec/hax/issues/61. We could rename the method in one of them and also do the same renaming when we translate an implementation. But this is a bit of a hack...
> I am testing my implementation of this. One problem in the case of `Debug` is that `Debug` and `Formatter` both belong to `core::fmt` and have a method `fmt` which means we get [#61](https://github.com/hacspec/hax/issues/61). We could rename the method in one of them and also do the same renaming when we translate an implementation. But this is a bit of a hack...

Apart from that the current implementation works but with the `false` precondition for `panic` it will not be usable for proofs. We can try to find an alternative using `val`s (but it might depend if we want to extract interfaces only, or implementation too.

For some traits like `Clone` we have a custom definition without pre/post conditions which makes the generated code for impls incompatible with the trait definition. We could filter out impls of `Clone` but that would leave the potential problem of creating cyclic dependencies with impl_expr.
> > I am testing my implementation of this. One problem in the case of `Debug` is that `Debug` and `Formatter` both belong to `core::fmt` and have a method `fmt` which means we get [#61](https://github.com/hacspec/hax/issues/61). We could rename the method in one of them and also do the same renaming when we translate an implementation. But this is a bit of a hack...
> 
> Apart from that the current implementation works but with the `false` precondition for `panic` it will not be usable for proofs. We can try to find an alternative using `val`s (but it might depend if we want to extract interfaces only, or implementation too.
> 
> For some traits like `Clone` we have a custom definition without pre/post conditions which makes the generated code for impls incompatible with the trait definition. We could filter out impls of `Clone` but that would leave the potential problem of creating cyclic dependencies with impl_expr.

After discussing this, the solution we should implement is: allow `impl`s (and functions) to be opaque. Add the opaque flag to generated `impl`s. This way we will extract them to `let impl: ... = admit()`
The best solution to solve this right now is to filter out things only with `late_skip` instead of dropping them in `import_thir`. We might need to kill the methods body in `import_thir` to avoid problems, like derived (or at least a list of unsupported traits).

It would also help to rename everything that is directly under the namespace of bundled modules.

Fix patch:
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
index 0e03029fc..c4d0426ba 100644
--- a/engine/backends/coq/coq/coq_backend.ml
+++ b/engine/backends/coq/coq/coq_backend.ml
@@ -407,14 +407,19 @@ struct
       method item'_Impl ~super ~generics ~self_ty ~of_trait ~items
           ~parent_bounds:_ ~safety:_ =
         let name, args = of_trait#v in
-        CoqNotation.instance
-          (name#p ^^ string "_" ^^ string (Int.to_string ([%hash: item] super)))
-          generics#p []
-          (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args)
-          (braces
-             (nest 2
-                (concat_map (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p) items)
-             ^^ break 1))
+        if Attrs.is_erased super.attrs then empty
+        else
+          CoqNotation.instance
+            (name#p ^^ string "_"
+            ^^ string (Int.to_string ([%hash: item] super)))
+            generics#p []
+            (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args)
+            (braces
+               (nest 2
+                  (concat_map
+                     (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p)
+                     items)
+               ^^ break 1))
 
       method item'_NotImplementedYet = string "(* NotImplementedYet *)"
 
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index f77e8fc1f..921f7f424 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -875,11 +875,7 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    let is_erased =
-      Attrs.find_unique_attr e.attrs
-        ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
-      |> Option.is_some
-    in
+    let is_erased = Attrs.is_erased e.attrs in
     let erased_impl name ty attrs binders =
       let name' = F.id_prime name in
       let pat = F.AST.PatVar (name, None, []) in
diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
index 5cce36a06..5b8312274 100644
--- a/engine/lib/attr_payloads.ml
+++ b/engine/lib/attr_payloads.ml
@@ -108,6 +108,11 @@ module MakeBase (Error : Phase_utils.ERROR) = struct
   let late_skip : attrs -> bool =
     status >> [%matches? Types.Included { late_skip = true }]
 
+  let is_erased : attrs -> bool =
+    find_unique_attr
+      ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
+    >> Option.is_some
+
   let uid : attrs -> UId.t option =
     let f = function Types.Uid uid -> Some (UId.of_raw uid) | _ -> None in
     find_unique_attr ~f
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index eb0cd442b..8011d5275 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -1330,17 +1330,9 @@ let is_automatically_derived (attrs : Thir.attribute list) =
       | _ -> false)
     attrs
 
-let is_hax_skip (attrs : Thir.attribute list) =
-  List.exists
-    ~f:(function
-      | { kind = Normal { item = { path; _ }; _ }; _ } ->
-          String.equal path "_hax::skip"
-      | _ -> false)
-    attrs
-
 let should_skip (attrs : Thir.item_attributes) =
   let attrs = attrs.attributes @ attrs.parent_attributes in
-  is_hax_skip attrs || is_automatically_derived attrs
+  is_automatically_derived attrs
 
 (** Converts a generic parameter to a generic value. This assumes the
 parameter is bound. *)
@@ -1452,402 +1444,390 @@ let rec c_item ~ident ~type_only (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
-    (* this is true if the user explicilty requested to erase using the `opaque` macro *)
-    let erased_by_user attrs =
-      Attr_payloads.payloads attrs
-      |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)])
-    in
-    let item_erased_by_user = erased_by_user attrs in
-    let type_only =
-      type_only
-      && Attr_payloads.payloads attrs
-         |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)])
-         |> not
-    in
-    (* This is true if the item should be erased because we are in type-only mode
-       (Only certain kinds of items are erased in this case). *)
-    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
-    (* If the item is erased in type-only mode we need to add the Erased attribute.
-       It is already present if the item is erased by user. *)
-    let attrs_with_erased erased_by_type_only erased_by_user attrs =
-      if erased_by_type_only && not erased_by_user then
-        Attr_payloads.to_attr Erased span :: attrs
-      else attrs
-    in
-    let attrs =
-      attrs_with_erased erased_by_type_only item_erased_by_user attrs
-    in
-    let erased = item_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 =
-      erased
-      && Attr_payloads.payloads attrs
-         |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)])
-         |> not
-    in
-    let c_body = if drop_body then c_expr_drop_body else c_expr in
-    (* TODO: things might be unnamed (e.g. constants) *)
-    match (item.kind : Thir.item_kind) with
-    | Const (_, generics, body) ->
-        mk
-        @@ Fn
-             {
-               name =
-                 Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
-               generics = c_generics generics;
-               body = c_body body;
-               params = [];
-               safety = Safe;
-             }
-    | TyAlias (ty, generics) ->
-        mk
-        @@ TyAlias
-             {
-               name =
-                 Concrete_ident.of_def_id Type (Option.value_exn item.def_id);
-               generics = c_generics generics;
-               ty = c_ty item.span ty;
-             }
-    | Fn (generics, { body; params; header = { safety; _ }; _ }) ->
-        mk
-        @@ Fn
-             {
-               name =
-                 Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
-               generics = c_generics generics;
-               body = c_body body;
-               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
-        let is_struct = false in
-        let kind = Concrete_ident.Kind.Constructor { is_struct } in
-        let discs =
-          (* Each variant might introduce a anonymous constant defining its discriminant integer  *)
-          List.filter_map ~f:(fun v -> v.disr_expr) variants
-          |> List.map ~f:(fun Types.{ def_id; body; _ } ->
-                 let name = Concrete_ident.of_def_id kind def_id in
-                 let generics = { params = []; constraints = [] } in
-                 let body = c_expr body in
-                 {
-                   v = Fn { name; generics; body; params = []; safety = Safe };
-                   span;
-                   ident = name;
-                   attrs = [];
-                 })
-        in
-        let is_primitive =
-          List.for_all
-            ~f:(fun { data; _ } ->
-              match data with
-              | Unit _ | Tuple ([], _, _) | Struct { fields = []; _ } -> true
-              | _ -> false)
-            variants
-        in
-        let variants =
-          List.map
-            ~f:(fun
-                ({ data; def_id = variant_id; attributes; _ } as original) ->
-              let is_record =
-                [%matches? (Struct { fields = _ :: _; _ } : Types.variant_data)]
-                  data
-              in
-              let name = Concrete_ident.of_def_id kind variant_id in
-              let arguments =
-                match data with
-                | Tuple (fields, _, _) | Struct { fields; _ } ->
-                    List.map
-                      ~f:(fun { def_id = id; ty; span; attributes; _ } ->
-                        ( Concrete_ident.of_def_id Field id,
-                          c_ty span ty,
-                          c_attrs attributes ))
-                      fields
-                | Unit _ -> []
-              in
-              let attrs = c_attrs attributes in
-              ({ name; arguments; is_record; attrs }, original))
-            variants
-        in
-        let name = Concrete_ident.of_def_id Type def_id in
-        let cast_fun =
-          cast_of_enum name generics (c_ty item.span repr.typ) item.span
-            variants
-        in
-        let variants, _ = List.unzip variants in
-        let result =
-          mk_one (Type { name; generics; variants; is_struct }) :: discs
-        in
-        if is_primitive then cast_fun :: result else result
-    | Struct (v, generics) ->
-        let generics = c_generics generics in
-        let def_id = Option.value_exn item.def_id in
-        let is_struct = true in
-        (* repeating the attributes of the item in the variant: TODO is that ok? *)
-        let v =
-          let kind = Concrete_ident.Kind.Constructor { is_struct } in
-          let name = Concrete_ident.of_def_id kind def_id in
-          let name = Concrete_ident.Create.move_under name ~new_parent:name in
-          let mk fields is_record =
+  let span = Span.of_thir item.span in
+  let attrs = c_item_attrs item.attributes in
+  (* this is true if the user explicilty requested to erase using the `opaque` macro *)
+  let erased_by_user attrs =
+    Attr_payloads.payloads attrs
+    |> List.exists ~f:(fst >> [%matches? (Erased : Types.ha_payload)])
+  in
+  let item_erased_by_user = erased_by_user attrs in
+  let type_only =
+    type_only
+    && Attr_payloads.payloads attrs
+       |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)])
+       |> not
+  in
+  (* This is true if the item should be erased because we are in type-only mode
+     (Only certain kinds of items are erased in this case). *)
+  let erased_by_hax =
+    should_skip item.attributes
+    || 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
+  (* If the item is erased by hax we need to add the Erased attribute.
+     It is already present if the item is erased by user. *)
+  let attrs_with_erased erased_by_hax erased_by_user attrs =
+    if erased_by_hax && not erased_by_user then
+      Attr_payloads.to_attr Erased span :: attrs
+    else attrs
+  in
+  let attrs = attrs_with_erased erased_by_hax item_erased_by_user attrs in
+  let erased = item_erased_by_user || erased_by_hax in
+
+  let mk_one v = { span; v; ident; attrs } in
+  let mk v = [ mk_one v ] in
+  let drop_body =
+    erased
+    && Attr_payloads.payloads attrs
+       |> List.exists ~f:(fst >> [%matches? (NeverErased : Types.ha_payload)])
+       |> not
+  in
+  let c_body = if drop_body then c_expr_drop_body else c_expr in
+  (* TODO: things might be unnamed (e.g. constants) *)
+  match (item.kind : Thir.item_kind) with
+  | Const (_, generics, body) ->
+      mk
+      @@ Fn
+           {
+             name =
+               Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
+             generics = c_generics generics;
+             body = c_body body;
+             params = [];
+             safety = Safe;
+           }
+  | TyAlias (ty, generics) ->
+      mk
+      @@ TyAlias
+           {
+             name = Concrete_ident.of_def_id Type (Option.value_exn item.def_id);
+             generics = c_generics generics;
+             ty = c_ty item.span ty;
+           }
+  | Fn (generics, { body; params; header = { safety; _ }; _ }) ->
+      mk
+      @@ Fn
+           {
+             name =
+               Concrete_ident.of_def_id Value (Option.value_exn item.def_id);
+             generics = c_generics generics;
+             body = c_body body;
+             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
+      let is_struct = false in
+      let kind = Concrete_ident.Kind.Constructor { is_struct } in
+      let discs =
+        (* Each variant might introduce a anonymous constant defining its discriminant integer  *)
+        List.filter_map ~f:(fun v -> v.disr_expr) variants
+        |> List.map ~f:(fun Types.{ def_id; body; _ } ->
+               let name = Concrete_ident.of_def_id kind def_id in
+               let generics = { params = []; constraints = [] } in
+               let body = c_expr body in
+               {
+                 v = Fn { name; generics; body; params = []; safety = Safe };
+                 span;
+                 ident = name;
+                 attrs = [];
+               })
+      in
+      let is_primitive =
+        List.for_all
+          ~f:(fun { data; _ } ->
+            match data with
+            | Unit _ | Tuple ([], _, _) | Struct { fields = []; _ } -> true
+            | _ -> false)
+          variants
+      in
+      let variants =
+        List.map
+          ~f:(fun ({ data; def_id = variant_id; attributes; _ } as original) ->
+            let is_record =
+              [%matches? (Struct { fields = _ :: _; _ } : Types.variant_data)]
+                data
+            in
+            let name = Concrete_ident.of_def_id kind variant_id in
             let arguments =
-              List.map
-                ~f:(fun Thir.{ def_id = id; ty; span; attributes; _ } ->
-                  ( Concrete_ident.of_def_id Field id,
-                    c_ty span ty,
-                    c_attrs attributes ))
-                fields
+              match data with
+              | Tuple (fields, _, _) | Struct { fields; _ } ->
+                  List.map
+                    ~f:(fun { def_id = id; ty; span; attributes; _ } ->
+                      ( Concrete_ident.of_def_id Field id,
+                        c_ty span ty,
+                        c_attrs attributes ))
+                    fields
+              | Unit _ -> []
             in
-            { name; arguments; is_record; attrs }
+            let attrs = c_attrs attributes in
+            ({ name; arguments; is_record; attrs }, original))
+          variants
+      in
+      let name = Concrete_ident.of_def_id Type def_id in
+      let cast_fun =
+        cast_of_enum name generics (c_ty item.span repr.typ) item.span variants
+      in
+      let variants, _ = List.unzip variants in
+      let result =
+        mk_one (Type { name; generics; variants; is_struct }) :: discs
+      in
+      if is_primitive then cast_fun :: result else result
+  | Struct (v, generics) ->
+      let generics = c_generics generics in
+      let def_id = Option.value_exn item.def_id in
+      let is_struct = true in
+      (* repeating the attributes of the item in the variant: TODO is that ok? *)
+      let v =
+        let kind = Concrete_ident.Kind.Constructor { is_struct } in
+        let name = Concrete_ident.of_def_id kind def_id in
+        let name = Concrete_ident.Create.move_under name ~new_parent:name in
+        let mk fields is_record =
+          let arguments =
+            List.map
+              ~f:(fun Thir.{ def_id = id; ty; span; attributes; _ } ->
+                ( Concrete_ident.of_def_id Field id,
+                  c_ty span ty,
+                  c_attrs attributes ))
+              fields
           in
-          match v with
-          | Tuple (fields, _, _) -> mk fields false
-          | Struct { fields = _ :: _ as fields; _ } -> mk fields true
-          | _ -> { name; arguments = []; is_record = false; attrs }
-        in
-        let variants = [ v ] in
-        let name = Concrete_ident.of_def_id Type def_id in
-        mk @@ Type { name; generics; variants; is_struct }
-    | MacroInvokation { macro_ident; argument; span } ->
-        mk
-        @@ IMacroInvokation
-             {
-               macro = Concrete_ident.of_def_id Macro macro_ident;
-               argument;
-               span = Span.of_thir span;
-               witness = W.macro;
-             }
-    | Trait (No, safety, generics, _bounds, items) ->
-        let items =
-          List.filter
-            ~f:(fun { attributes; _ } -> not (should_skip attributes))
-            items
-        in
-        let name =
-          Concrete_ident.of_def_id Trait (Option.value_exn item.def_id)
-        in
-        let { params; constraints } = c_generics generics in
-        let self =
-          let id = Local_ident.mk_id Typ 0 (* todo *) in
-          let ident = Local_ident.{ name = "Self"; id } in
-          { ident; span; attrs = []; kind = GPType }
+          { name; arguments; is_record; attrs }
         in
-        let params = self :: params in
-        let generics = { params; constraints } in
-        let items = List.map ~f:c_trait_item items in
-        let safety = csafety safety in
-        mk @@ Trait { name; generics; items; safety }
-    | Trait (Yes, _, _, _, _) ->
-        unimplemented ~issue_id:930 [ item.span ] "Auto trait"
-    | Impl { of_trait = None; generics; items; _ } ->
-        let items =
-          List.filter
-            ~f:(fun { attributes; _ } -> not (should_skip attributes))
-            items
-        in
-        List.map
-          ~f:(fun (item : Thir.impl_item) ->
-            let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in
-            let attrs = c_item_attrs item.attributes in
-            let sub_item_erased_by_user = erased_by_user attrs in
-            let sub_item_erased = sub_item_erased_by_user || type_only in
-            let attrs =
-              attrs_with_erased type_only sub_item_erased_by_user attrs
-            in
-            let c_body = if sub_item_erased then c_expr_drop_body else c_body in
-
-            let v =
-              match (item.kind : Thir.impl_item_kind) with
-              | Fn { body; params; header = { safety; _ }; _ } ->
-                  let params =
-                    if List.is_empty params then [ U.make_unit_param span ]
-                    else List.map ~f:(c_param item.span) params
-                  in
-                  Fn
-                    {
-                      name = item_def_id;
-                      generics =
-                        U.concat_generics (c_generics generics)
-                          (c_generics item.generics);
-                      body = c_body body;
-                      params;
-                      safety = csafety safety;
-                    }
-              | Const (_ty, e) ->
-                  Fn
-                    {
-                      name = item_def_id;
-                      generics = c_generics generics;
-                      (* does that make sense? can we have `const<T>`? *)
-                      body = c_body e;
-                      params = [];
-                      safety = Safe;
-                    }
-              | Type _ty ->
-                  assertion_failure [ item.span ]
-                    "Inherent implementations are not supposed to have \
-                     associated types \
-                     (https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations)."
-            in
-            let ident = Concrete_ident.of_def_id Value item.owner_id in
-            { span = Span.of_thir item.span; v; ident; attrs })
+        match v with
+        | Tuple (fields, _, _) -> mk fields false
+        | Struct { fields = _ :: _ as fields; _ } -> mk fields true
+        | _ -> { name; arguments = []; is_record = false; attrs }
+      in
+      let variants = [ v ] in
+      let name = Concrete_ident.of_def_id Type def_id in
+      mk @@ Type { name; generics; variants; is_struct }
+  | MacroInvokation { macro_ident; argument; span } ->
+      mk
+      @@ IMacroInvokation
+           {
+             macro = Concrete_ident.of_def_id Macro macro_ident;
+             argument;
+             span = Span.of_thir span;
+             witness = W.macro;
+           }
+  | Trait (No, safety, generics, _bounds, items) ->
+      let items =
+        List.filter
+          ~f:(fun { attributes; _ } -> not (should_skip attributes))
           items
-    | Impl
-        {
-          of_trait = Some of_trait;
-          generics;
-          self_ty;
-          items;
-          safety;
-          parent_bounds;
-          _;
-        } ->
-        let items =
-          List.filter
-            ~f:(fun { attributes; _ } -> not (should_skip attributes))
-            items
-        in
-        let items =
-          if erased then
-            [
-              (* Dummy associated item *)
+      in
+      let name =
+        Concrete_ident.of_def_id Trait (Option.value_exn item.def_id)
+      in
+      let { params; constraints } = c_generics generics in
+      let self =
+        let id = Local_ident.mk_id Typ 0 (* todo *) in
+        let ident = Local_ident.{ name = "Self"; id } in
+        { ident; span; attrs = []; kind = GPType }
+      in
+      let params = self :: params in
+      let generics = { params; constraints } in
+      let items = List.map ~f:c_trait_item items in
+      let safety = csafety safety in
+      mk @@ Trait { name; generics; items; safety }
+  | Trait (Yes, _, _, _, _) ->
+      unimplemented ~issue_id:930 [ item.span ] "Auto trait"
+  | Impl { of_trait = None; generics; items; _ } ->
+      let items =
+        List.filter
+          ~f:(fun { attributes; _ } -> not (should_skip attributes))
+          items
+      in
+      List.map
+        ~f:(fun (item : Thir.impl_item) ->
+          let item_def_id = Concrete_ident.of_def_id Impl item.owner_id in
+          let attrs = c_item_attrs item.attributes in
+          let sub_item_erased_by_user = erased_by_user attrs in
+          let sub_item_erased = sub_item_erased_by_user || type_only in
+          let attrs =
+            attrs_with_erased type_only sub_item_erased_by_user attrs
+          in
+          let c_body = if sub_item_erased then c_expr_drop_body else c_body in
+
+          let v =
+            match (item.kind : Thir.impl_item_kind) with
+            | Fn { body; params; header = { safety; _ }; _ } ->
+                let params =
+                  if List.is_empty params then [ U.make_unit_param span ]
+                  else List.map ~f:(c_param item.span) params
+                in
+                Fn
+                  {
+                    name = item_def_id;
+                    generics =
+                      U.concat_generics (c_generics generics)
+                        (c_generics item.generics);
+                    body = c_body body;
+                    params;
+                    safety = csafety safety;
+                  }
+            | Const (_ty, e) ->
+                Fn
+                  {
+                    name = item_def_id;
+                    generics = c_generics generics;
+                    (* does that make sense? can we have `const<T>`? *)
+                    body = c_body e;
+                    params = [];
+                    safety = Safe;
+                  }
+            | Type _ty ->
+                assertion_failure [ item.span ]
+                  "Inherent implementations are not supposed to have \
+                   associated types \
+                   (https://doc.rust-lang.org/reference/items/implementations.html#inherent-implementations)."
+          in
+          let ident = Concrete_ident.of_def_id Value item.owner_id in
+          { span = Span.of_thir item.span; v; ident; attrs })
+        items
+  | Impl
+      {
+        of_trait = Some of_trait;
+        generics;
+        self_ty;
+        items;
+        safety;
+        parent_bounds;
+        _;
+      } ->
+      let items =
+        List.filter
+          ~f:(fun { attributes; _ } -> not (should_skip attributes))
+          items
+      in
+      let items =
+        if erased then
+          [
+            (* Dummy associated item *)
+            {
+              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 = { params = []; constraints = [] };
+                ii_generics = c_generics item.generics;
                 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
-        mk
-        @@ Impl
-             {
-               generics = c_generics generics;
-               self_ty = c_ty item.span self_ty;
-               of_trait =
-                 ( Concrete_ident.of_def_id Trait of_trait.def_id,
-                   List.map ~f:(c_generic_value item.span) of_trait.generic_args
-                 );
-               items;
-               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;
-               safety = csafety safety;
-             }
-    | Use ({ span = _; res; segments; rename }, _) ->
-        let v =
-          Use
-            {
-              path = List.map ~f:(fun x -> fst x.ident) segments;
-              is_external =
-                List.exists ~f:(function Err -> true | _ -> false) res;
-              (* TODO: this should represent local/external? *)
-              rename;
-            }
-        in
-        (* ident is supposed to always be an actual item, thus here we need to cheat a bit *)
-        (* TODO: is this DUMMY thing really needed? there's a `Use` segment (see #272) *)
-        let def_id = item.owner_id in
-        let def_id : Types.def_id =
-          let value =
-            {
-              def_id.contents.value with
-              path =
-                def_id.contents.value.path
-                @ [
-                    Types.
-                      {
-                        data = ValueNs "DUMMY";
-                        disambiguator = MyInt64.of_int 0;
-                      };
-                  ];
-            }
-          in
-          { contents = { def_id.contents with value } }
+                  (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
+      mk
+      @@ Impl
+           {
+             generics = c_generics generics;
+             self_ty = c_ty item.span self_ty;
+             of_trait =
+               ( Concrete_ident.of_def_id Trait of_trait.def_id,
+                 List.map ~f:(c_generic_value item.span) of_trait.generic_args
+               );
+             items;
+             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;
+             safety = csafety safety;
+           }
+  | Use ({ span = _; res; segments; rename }, _) ->
+      let v =
+        Use
+          {
+            path = List.map ~f:(fun x -> fst x.ident) segments;
+            is_external =
+              List.exists ~f:(function Err -> true | _ -> false) res;
+            (* TODO: this should represent local/external? *)
+            rename;
+          }
+      in
+      (* ident is supposed to always be an actual item, thus here we need to cheat a bit *)
+      (* TODO: is this DUMMY thing really needed? there's a `Use` segment (see #272) *)
+      let def_id = item.owner_id in
+      let def_id : Types.def_id =
+        let value =
+          {
+            def_id.contents.value with
+            path =
+              def_id.contents.value.path
+              @ [
+                  Types.
+                    { data = ValueNs "DUMMY"; disambiguator = MyInt64.of_int 0 };
+                ];
+          }
         in
-        [ { span; v; ident = Concrete_ident.of_def_id Value def_id; attrs } ]
-    | Union _ ->
-        unimplemented ~issue_id:998 [ item.span ] "Union types: not supported"
-    | ExternCrate _ | Static _ | Macro _ | Mod _ | ForeignMod _ | GlobalAsm _
-    | TraitAlias _ ->
-        mk NotImplementedYet
+        { contents = { def_id.contents with value } }
+      in
+      [ { span; v; ident = Concrete_ident.of_def_id Value def_id; attrs } ]
+  | Union _ ->
+      unimplemented ~issue_id:998 [ item.span ] "Union types: not supported"
+  | ExternCrate _ | Static _ | Macro _ | Mod _ | ForeignMod _ | GlobalAsm _
+  | TraitAlias _ ->
+      mk NotImplementedYet
 
 let import_item ~type_only (item : Thir.item) :
     concrete_ident * (item list * Diagnostics.t list) =


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index e65784071..f52788a03 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -92,6 +92,18 @@ open FStar.Mul
 
 unfold type t_Int = int
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_1': Core.Clone.t_Clone t_Int
+
+let impl_1 = impl_1'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl': Core.Marker.t_Copy t_Int
+
+let impl = impl'
+
 unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
   {
     f_Output = t_Int;
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index f2da7be00..4ef4fb981 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap
@@ -132,6 +132,12 @@ Definition patterns (_ : unit) : unit :=
   end in
   tt.
 
+
+
+
+
+
+
 Definition panic_with_msg (_ : unit) : unit :=
   never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))).
 
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index f3bb80621..0ce6219db 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
@@ -179,6 +179,24 @@ let patterns (_: Prims.unit) : Prims.unit =
   in
   ()
 
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl': Core.Marker.t_StructuralPartialEq t_Foo
+
+let impl = impl'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_1': Core.Cmp.t_PartialEq t_Foo t_Foo
+
+let impl_1 = impl_1'
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+assume
+val impl_2': Core.Cmp.t_Eq t_Foo
+
+let impl_2 = impl_2'
+
 let panic_with_msg (_: Prims.unit) : Prims.unit =
   Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1)
             (let list = ["with msg"] in