diff --git a/Changelog.md b/Changelog.md
index c2d0ebe0..d2e196f5 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -12,6 +12,9 @@
 	`T` to `S.type` whenever `T` is not a global type (e.g. a variable). Note
 	that `S.pack` can cast a `t : T` to `S.type` only if an instance of the
 	class `S` on `t` is found by type class inference
+- **New** Attribute `#[typeclass]` to declare the class of a
+	structure (`axioms_`) as a type class on the subject with all arguments in
+	output mode but for the subject that is in input mode.
 
 ## [1.7.0] - 2024-01-10
 
diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils-synterp.elpi
index 73932c1a..82962ad8 100644
--- a/HB/common/utils-synterp.elpi
+++ b/HB/common/utils-synterp.elpi
@@ -24,6 +24,7 @@ with-attributes P :-
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,
+	 att "typeclass" bool,
   ] Opts, !,
   Opts => (save-docstring, P).
 
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 5f396586..e730c787 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -127,6 +127,11 @@ declare Module BSkel Sort :- std.do! [
     ])
     (coq.say "declare:" ClassName "should be an inductive", fail),
 
+  if (get-option "typeclass" tt) (
+	 coq.TC.declare-class ClassName,
+	 coq.hints.add-mode ClassName "typeclass_instances" {std.append {std.map {std.iota {w-params.nparams MLwP}} (_\ r\ r = mode-output)} [mode-input]})
+	 (true),
+
   if-verbose (coq.say {header} "accumulating various props"),
   std.flatten [
       Factories, [ClassAlias], [is-structure Structure],
diff --git a/tests/coercion.v b/tests/coercion.v
index e0faa29a..6eaf1e87 100644
--- a/tests/coercion.v
+++ b/tests/coercion.v
@@ -5,7 +5,7 @@ HB.mixin Record isSigma (T : Type) (P : T -> Prop) (x : T) := {
   _ : P x
 }.
 
-#[short(type="sigType")]
+#[short(type="sigType"), typeclass]
 HB.structure Definition Sig (T : Type) (P : T -> Prop) := {x of isSigma T P x}.
 
 Section Sigma.
@@ -45,7 +45,7 @@ Fail Check x : sigType A P.
 End Sigma.
 
 HB.mixin Record isSigmaT (P : Type -> Prop) (x : Type) := { _ : P x }.
-#[short(type="sigTType")]
+#[short(type="sigTType"), typeclass]
 HB.structure Definition SigT (P : Type -> Prop) := {x of isSigmaT P x}.
 
 Section SigmaT.