diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml
index 0ead59bd5..5c0120883 100644
--- a/engine/backends/fstar/fstar_ast.ml
+++ b/engine/backends/fstar/fstar_ast.ml
@@ -32,6 +32,7 @@ let pat (pat : AST.pattern') = AST.{ pat; prange = dummyRange }
 
 module Attrs = struct
   let no_method = term @@ AST.Var FStar_Parser_Const.no_method_lid
+  let tcinstance = term @@ AST.Var FStar_Parser_Const.tcinstance_lid
 end
 
 let tcresolve = term @@ AST.Var FStar_Parser_Const.tcresolve_lid
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 6430fc633..8a86b7a57 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -1365,7 +1365,7 @@ struct
                  | GCType { goal = bound; name = id } ->
                      let name = "_super_" ^ id in
                      let typ = pgeneric_constraint_type e.span c in
-                     Some (F.id name, None, [ F.Attrs.no_method ], typ)
+                     Some (F.id name, None, [ F.Attrs.tcinstance ], typ)
                  | GCProjection _ ->
                      (* TODO: Not yet implemented, see https://github.com/hacspec/hax/issues/785 *)
                      None
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 75062d160..8baf9477a 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -35,11 +35,11 @@ open FStar.Mul
 class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
 
 class t_ParBlocksSizeUser (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_10960599340086055385:t_BlockSizeUser v_Self
+  [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_10960599340086055385:t_BlockSizeUser v_Self
 }
 
 class t_BlockBackend (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self;
+  [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_15949286759387124191:t_ParBlocksSizeUser v_Self;
   f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
   f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
   f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
@@ -329,7 +329,7 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg
   }
 
 class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_8779313392680198588:t_Trait v_Self
+  [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_8779313392680198588:t_Trait v_Self
     v_TypeArg
     v_ConstArg;
   f_AssocType:Type0;
@@ -458,7 +458,7 @@ class t_Trait1 (v_Self: Type0) = {
 }
 
 class t_Trait2 (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_4567617955834163411:t_Trait1 v_Self;
+  [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_4567617955834163411:t_Trait1 v_Self;
   f_U:Type0
 }
 '''
@@ -541,7 +541,7 @@ class t_Lang (v_Self: Type0) = {
 }
 
 class t_SuperTrait (v_Self: Type0) = {
-  [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self;
+  [@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9442900250278684536:Core.Clone.t_Clone v_Self;
   f_function_of_super_trait_pre:v_Self -> Type0;
   f_function_of_super_trait_post:v_Self -> u32 -> Type0;
   f_function_of_super_trait:x0: v_Self