declare axioms_ as typeclass and typeclass option for HB.structure

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
 

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).
 

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],

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.