From 56e85cd20493af05a1e8f2f22cef3accda0c8bb6 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Thu, 4 Jun 2026 11:50:10 +0200
Subject: [PATCH 1/9] wip

---
 HB/factory.elpi   | 5 +++--
 HB/structure.elpi | 9 ++++++++-
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index cd8794b9..f5117820 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -297,6 +297,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "start module Exports"),
 
   log.coq.env.begin-module "Exports" none,
+	coq.TC.declare-class R,
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
     factory->constructor (indt R) GRK,
@@ -363,7 +364,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
 
   if (mixin->first-class F _) (PhGRK = PhGRK0)
     (phant.append-fun-unify PhGRK0 PhGRK),
-  GRDepsClauses => phant.add-abbreviation "Build" PhGRK _ _,
+  GRDepsClauses => phant.add-abbreviation "Build" GRK _ _,
 
   GRDepsClauses => mk-factory-abbrev "axioms" (const C) Clauses FactAbbrev,
 
@@ -436,4 +437,4 @@ mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref->deps
 
 
 
-}}
\ No newline at end of file
+}}
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 52036dfd..98bd44bf 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -47,6 +47,7 @@ declare Module BSkel Sort :- std.do! [
   GRDepsClauses =
     [gref->deps (indt ClassInd) NilwP, gref->deps (indc ClassK) MLwP],
   std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
+  Factories => std.map ML (private.mixin-clause Structure) MixinClauses,
   std.filter ML (m\ not (mixin->first-class m _)) NewMixins,
   std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass,
 
@@ -126,7 +127,8 @@ declare Module BSkel Sort :- std.do! [
   std.flatten [
       Factories, [is-structure Structure],
       NewJoins, [class-def CurrentClass], GRDepsClauses,
-      [gref->deps GRPack MLwP], MixinMems, [StructKeyClause]
+      [gref->deps GRPack MLwP], MixinMems, [StructKeyClause],
+      MixinClauses
     ]
     NewClauses,
   acc-clauses current NewClauses,
@@ -195,6 +197,11 @@ namespace private {
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
+func mixin-clause structure, mixinname -> prop.
+mixin-clause Structure M Clause :-
+  factory->nparams M NP,
+  coq.error "STOP".
+
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra
 % Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs

From cc23d4ce77982a092aaf8944fca9be2162dbafbc Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Thu, 4 Jun 2026 16:40:48 +0200
Subject: [PATCH 2/9] wip

---
 HB/common/database.elpi |  4 ++--
 HB/common/stdpp.elpi    |  2 +-
 HB/factory.elpi         | 15 +++++++-----
 HB/structure.elpi       | 53 ++++++++++++++++++++++++++++++++++++-----
 HB/structures.v         | 30 ++++++++++++++++++++++-
 5 files changed, 88 insertions(+), 16 deletions(-)

diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 2ecaf7ae..29940537 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -433,9 +433,9 @@ has-CS-instance? TyTerm (indt Struct) :-
   coq.CS.db-for (const Proj) Pat L,
   not(L = []).
 
-pred structure-nparams i:structure, o:int.
+func structure-nparams structure -> int.
 structure-nparams Structure NParams :-
-  class-def (class Class Structure _),
+  class-def (class Class Structure _), !,
   factory->nparams Class NParams.
 
 func factory? term -> w-args factoryname.
diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 1d56dac1..8b440586 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -364,4 +364,4 @@ constraint seen? seen! purge-seen!  {
   rule purge-seen! \ (seen! _ _).
   rule \ purge-seen!.
 }
-}
\ No newline at end of file
+}
diff --git a/HB/factory.elpi b/HB/factory.elpi
index f5117820..92691fc1 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -283,8 +283,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   if-verbose (coq.say {header} "declare notation Build"),
 
-  GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
-  GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst BuildAbbrev,
+  coq.say "Hello, world!",
+  GRDepsClauses => coq.notation.add-abbreviation "Build" 0 (global GRK) tt _,
 
   if-verbose (coq.say {header} "declare notation axioms"),
 
@@ -297,12 +297,12 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "start module Exports"),
 
   log.coq.env.begin-module "Exports" none,
-	coq.TC.declare-class R,
+  coq.say "Declaring mixin as typeclass",
+	coq.TC.declare-class (indt R),
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
     factory->constructor (indt R) GRK,
     factory->nparams (indt R) NParams,
-    phant-abbrev GRK (const BuildConst) BuildAbbrev,
     % gref->deps GRFSort MLwP,
     % factory-sort FactorySortCoe,
   ]] NewClauses,
@@ -310,8 +310,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   list-w-params_list MLwP MLwoP,
   std.map MLwoP (_\ r\ r = maximal) Implicits,
+  std.map {std.iota NParams} (_\ r\ r = explicit) Explicits,
   /* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */
-  @global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],
+  @global! => log.coq.arguments.set-implicit GRK [[explicit|{std.append Explicits Implicits}]],
   % @global! => log.coq.coercion.declare FactorySortCoe,
 
   log.coq.env.end-module-name "Exports" Exports,
@@ -352,6 +353,7 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
 
   log.coq.env.end-section-name Module,
 
+  % TODO: make the mixins implicit.
   @global! => log.coq.arguments.set-implicit GRK [[]],
 
   factories-provide GRFSwP MLwP,
@@ -364,7 +366,8 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
 
   if (mixin->first-class F _) (PhGRK = PhGRK0)
     (phant.append-fun-unify PhGRK0 PhGRK),
-  GRDepsClauses => phant.add-abbreviation "Build" GRK _ _,
+  @global! => log.coq.arguments.set-implicit GRK [[]],
+  GRDepsClauses => coq.notation.add-abbreviation "Build" 0 (global GRK) tt _,
 
   GRDepsClauses => mk-factory-abbrev "axioms" (const C) Clauses FactAbbrev,
 
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 98bd44bf..5a02db76 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -47,7 +47,7 @@ declare Module BSkel Sort :- std.do! [
   GRDepsClauses =
     [gref->deps (indt ClassInd) NilwP, gref->deps (indc ClassK) MLwP],
   std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
-  Factories => std.map ML (private.mixin-clause Structure) MixinClauses,
+  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => Factories => std.map-i ML (private.mixin-clause Structure) MixinClauses,
   std.filter ML (m\ not (mixin->first-class m _)) NewMixins,
   std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass,
 
@@ -128,10 +128,11 @@ declare Module BSkel Sort :- std.do! [
       Factories, [is-structure Structure],
       NewJoins, [class-def CurrentClass], GRDepsClauses,
       [gref->deps GRPack MLwP], MixinMems, [StructKeyClause],
-      MixinClauses
     ]
     NewClauses,
   acc-clauses current NewClauses,
+  std.map MixinClauses (c\ r\ r = clause _ _ c) MixinClauses0,
+  coq.elpi.accumulate-clauses _ "tc.db" MixinClauses0,
 
   if-verbose (coq.say {header} "stop module Exports"),
   log.coq.env.end-module-name "Exports" Exports,
@@ -197,10 +198,50 @@ namespace private {
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
-func mixin-clause structure, mixinname -> prop.
-mixin-clause Structure M Clause :-
-  factory->nparams M NP,
-  coq.error "STOP".
+func clause.mk-n-pis int, list term, (func list term -> prop) -> prop.
+clause.mk-n-pis 0 RArgs P Clause :- !, std.rev RArgs Args, P Args Clause.
+clause.mk-n-pis N Args P (pi x\ Clause x) :-
+  calc (N - 1) N0,
+  pi x\ clause.mk-n-pis N0 [x|Args] P (Clause x).
+
+func mixin-clause structure, int, mixinname -> prop.
+mixin-clause S I M Clause :-
+  structure-key SortProj _ S, !,
+  get-constructor S KS,
+  class-def (class (indt Class) S CMLwP), !,
+  get-constructor (indt Class) KC,
+  tc.gref->pred-name M PredName,
+  gref->deps M MDeps,
+  
+% tc-...-NModule_isLSemiModule.tc-axioms_ R T isNModule Inst :-
+%   coq.unify-eq T (Sort R ST) ok,
+%   coq.unify-eq ST (S.Pack R T CT) ok,
+%   coq.unify-eq CT (C.Axioms_ R T isNModule NModule_isLSemiModule),
+%   std.nth 1 [isNModule, NModule_isLSemiModule] Inst.
+  clause.mk-n-pis {structure-nparams S} [] (Params\ clause\
+  clause.mk-n-pis {factory->nparams M} [] (MParams\ clause\
+  clause.mk-n-pis {std.length {list-w-params_list CMLwP}} [] (MIL\ clause\
+  clause.mk-n-pis {std.length {list-w-params_list MDeps}} [] (MHDeps\ clause\
+    sigma Clause' MILI\
+    std.take I MIL MILI,
+    clause = (pi T ST CT Inst\ Clause' T ST CT Inst),
+    pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C\
+    std.append Params [ST] ParamsST,
+    coq.mk-app (global (const SortProj)) ParamsST SortParamsST,
+    coq.mk-app (global KS) {std.append Params [T, CT]} KSParamsC,
+    coq.mk-app (global KC) {std.append Params [T | MIL]} CBody,
+    coq.elpi.predicate PredName {std.append MParams {std.append [T | MHDeps] [Inst]}} C,
+    Clause' T ST CT Inst = (C :-
+      coq.unify-eq T SortParamsST ok,
+      coq.unify-eq ST KSParamsC ok,
+      coq.unify-eq CT CBody ok,
+      std.nth I MIL Inst)
+  ) clause) clause) clause) Clause,
+  coq.say "Clause for " M " is " Clause.
+      
+      
+
+
 
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra
diff --git a/HB/structures.v b/HB/structures.v
index 90fcb358..583854d9 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -20,7 +20,12 @@ Definition ignore {T} (x: T) := x.
 Definition ignore_disabled {T T'} (x : T) (x' : T') := x'.
 
 (* ********************* structures ****************************** *)
-From elpi Require Import elpi.
+From elpi Require Import elpi tc.
+
+From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
+
+TC.AddAllClasses.
+TC.AddAllInstances.
 
 Register unify as hb.unify.
 Register id_phant as hb.id.
@@ -306,6 +311,7 @@ Elpi Export HB.locate.
 
 #[arguments(raw)] Elpi Command HB.about.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
@@ -340,6 +346,7 @@ Elpi Export HB.about.
 
 #[arguments(raw)] Elpi Command HB.howto.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -382,6 +389,7 @@ Elpi Export HB.howto.
 
 #[arguments(raw)] Elpi Command HB.status.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -412,6 +420,7 @@ tred file.dot | xdot -
 
 #[arguments(raw)] Elpi Command HB.graph.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -461,6 +470,8 @@ HB.mixin Record MixinName T & Factory1 T & … & FactoryN T := {
 
 #[arguments(raw)] Elpi Command HB.mixin.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -543,6 +554,7 @@ Elpi Export HB.mixin.
 
 Elpi Tactic HB.pack_for.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -566,6 +578,7 @@ Elpi Export HB.pack_for.
 
 Elpi Tactic HB.pack.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -642,6 +655,8 @@ HB.structure Definition StructureName params :=
 
 #[arguments(raw)] Elpi Command HB.structure.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -725,6 +740,8 @@ Elpi Export HB.structure.
 
 #[arguments(raw)] Elpi Command HB.saturate.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -775,6 +792,7 @@ HB.instance Definition N Params := Factory.Build Params T …
 
 #[arguments(raw)] Elpi Command HB.instance.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -817,6 +835,8 @@ Elpi Export HB.instance.
 
 #[arguments(raw)] Elpi Command HB.factory.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -900,6 +920,8 @@ HB.end.
 
 #[arguments(raw)] Elpi Command HB.builders.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -941,6 +963,7 @@ Elpi Export HB.builders.
 
 #[arguments(raw)] Elpi Command HB.end.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -1015,6 +1038,7 @@ Export Algebra.Exports.
 
 #[arguments(raw)] Elpi Command HB.export.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -1061,6 +1085,7 @@ Elpi Export HB.export.
 
 #[arguments(raw)] Elpi Command HB.reexport.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -1144,6 +1169,8 @@ HB.instance Definition _ : Ml ... T := ml.
 
 #[arguments(raw)] Elpi Command HB.declare.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -1180,6 +1207,7 @@ Elpi Export HB.declare.
 
 #[arguments(raw)] Elpi Command HB.check.
 Elpi Accumulate Db hb.db.
+Elpi Accumulate Db tc.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".

From 9c85b360b3bf28d29b023f5d65a64e26e0acb961 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Fri, 5 Jun 2026 10:57:58 +0200
Subject: [PATCH 3/9] use projection instead of unification to extract the
 mixin from the class

---
 HB/structure.elpi | 25 +++++++++----------------
 1 file changed, 9 insertions(+), 16 deletions(-)

diff --git a/HB/structure.elpi b/HB/structure.elpi
index 5a02db76..a13c1526 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -47,7 +47,7 @@ declare Module BSkel Sort :- std.do! [
   GRDepsClauses =
     [gref->deps (indt ClassInd) NilwP, gref->deps (indc ClassK) MLwP],
   std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
-  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => Factories => std.map-i ML (private.mixin-clause Structure) MixinClauses,
+  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => Factories => std.map ML (private.mixin-clause Structure) MixinClauses,
   std.filter ML (m\ not (mixin->first-class m _)) NewMixins,
   std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass,
 
@@ -204,14 +204,14 @@ clause.mk-n-pis N Args P (pi x\ Clause x) :-
   calc (N - 1) N0,
   pi x\ clause.mk-n-pis N0 [x|Args] P (Clause x).
 
-func mixin-clause structure, int, mixinname -> prop.
-mixin-clause S I M Clause :-
+func mixin-clause structure, mixinname -> prop.
+mixin-clause S M Clause :-
   structure-key SortProj _ S, !,
   get-constructor S KS,
   class-def (class (indt Class) S CMLwP), !,
-  get-constructor (indt Class) KC,
   tc.gref->pred-name M PredName,
   gref->deps M MDeps,
+  from (indt Class) M CMP, !,
   
 % tc-...-NModule_isLSemiModule.tc-axioms_ R T isNModule Inst :-
 %   coq.unify-eq T (Sort R ST) ok,
@@ -222,26 +222,19 @@ mixin-clause S I M Clause :-
   clause.mk-n-pis {factory->nparams M} [] (MParams\ clause\
   clause.mk-n-pis {std.length {list-w-params_list CMLwP}} [] (MIL\ clause\
   clause.mk-n-pis {std.length {list-w-params_list MDeps}} [] (MHDeps\ clause\
-    sigma Clause' MILI\
-    std.take I MIL MILI,
+    sigma Clause'\
     clause = (pi T ST CT Inst\ Clause' T ST CT Inst),
-    pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C\
+    pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C MBody\
     std.append Params [ST] ParamsST,
     coq.mk-app (global (const SortProj)) ParamsST SortParamsST,
     coq.mk-app (global KS) {std.append Params [T, CT]} KSParamsC,
-    coq.mk-app (global KC) {std.append Params [T | MIL]} CBody,
+    coq.mk-app (global CMP) {std.append Params [T, CT]} MBody,
     coq.elpi.predicate PredName {std.append MParams {std.append [T | MHDeps] [Inst]}} C,
     Clause' T ST CT Inst = (C :-
       coq.unify-eq T SortParamsST ok,
       coq.unify-eq ST KSParamsC ok,
-      coq.unify-eq CT CBody ok,
-      std.nth I MIL Inst)
-  ) clause) clause) clause) Clause,
-  coq.say "Clause for " M " is " Clause.
-      
-      
-
-
+      Inst = MBody)
+  ) clause) clause) clause) Clause.
 
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra

From b8d2401778595edcb953b99344ba6de6b44b3c98 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Fri, 5 Jun 2026 10:58:28 +0200
Subject: [PATCH 4/9] Revert "use projection instead of unification to extract
 the mixin from the class"

This reverts commit 9c85b360b3bf28d29b023f5d65a64e26e0acb961.
---
 HB/structure.elpi | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

diff --git a/HB/structure.elpi b/HB/structure.elpi
index a13c1526..5a02db76 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -47,7 +47,7 @@ declare Module BSkel Sort :- std.do! [
   GRDepsClauses =
     [gref->deps (indt ClassInd) NilwP, gref->deps (indc ClassK) MLwP],
   std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
-  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => Factories => std.map ML (private.mixin-clause Structure) MixinClauses,
+  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => Factories => std.map-i ML (private.mixin-clause Structure) MixinClauses,
   std.filter ML (m\ not (mixin->first-class m _)) NewMixins,
   std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass,
 
@@ -204,14 +204,14 @@ clause.mk-n-pis N Args P (pi x\ Clause x) :-
   calc (N - 1) N0,
   pi x\ clause.mk-n-pis N0 [x|Args] P (Clause x).
 
-func mixin-clause structure, mixinname -> prop.
-mixin-clause S M Clause :-
+func mixin-clause structure, int, mixinname -> prop.
+mixin-clause S I M Clause :-
   structure-key SortProj _ S, !,
   get-constructor S KS,
   class-def (class (indt Class) S CMLwP), !,
+  get-constructor (indt Class) KC,
   tc.gref->pred-name M PredName,
   gref->deps M MDeps,
-  from (indt Class) M CMP, !,
   
 % tc-...-NModule_isLSemiModule.tc-axioms_ R T isNModule Inst :-
 %   coq.unify-eq T (Sort R ST) ok,
@@ -222,19 +222,26 @@ mixin-clause S M Clause :-
   clause.mk-n-pis {factory->nparams M} [] (MParams\ clause\
   clause.mk-n-pis {std.length {list-w-params_list CMLwP}} [] (MIL\ clause\
   clause.mk-n-pis {std.length {list-w-params_list MDeps}} [] (MHDeps\ clause\
-    sigma Clause'\
+    sigma Clause' MILI\
+    std.take I MIL MILI,
     clause = (pi T ST CT Inst\ Clause' T ST CT Inst),
-    pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C MBody\
+    pi T ST CT Inst\ sigma ParamsST SortParamsST KSParamsC CBody C\
     std.append Params [ST] ParamsST,
     coq.mk-app (global (const SortProj)) ParamsST SortParamsST,
     coq.mk-app (global KS) {std.append Params [T, CT]} KSParamsC,
-    coq.mk-app (global CMP) {std.append Params [T, CT]} MBody,
+    coq.mk-app (global KC) {std.append Params [T | MIL]} CBody,
     coq.elpi.predicate PredName {std.append MParams {std.append [T | MHDeps] [Inst]}} C,
     Clause' T ST CT Inst = (C :-
       coq.unify-eq T SortParamsST ok,
       coq.unify-eq ST KSParamsC ok,
-      Inst = MBody)
-  ) clause) clause) clause) Clause.
+      coq.unify-eq CT CBody ok,
+      std.nth I MIL Inst)
+  ) clause) clause) clause) Clause,
+  coq.say "Clause for " M " is " Clause.
+      
+      
+
+
 
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra

From 48db6fd98bdb2fa5b881d6b6e0b8c2e3672e6ac2 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 8 Jun 2026 09:24:40 +0200
Subject: [PATCH 5/9] fix Build notation, Build implicits, instance elaboration
 and clause accumulation

---
 HB/common/stdpp.elpi |  6 ++++++
 HB/factory.elpi      | 20 ++++++++++++++------
 HB/instance.elpi     | 19 ++++++++++++++++++-
 HB/structure.elpi    |  5 ++---
 4 files changed, 40 insertions(+), 10 deletions(-)

diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index 8b440586..ff15b709 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -150,6 +150,12 @@ constraint print-ctx mixin-src {
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+func coq.mk-n-fun int, (func list term -> term), list term -> term.
+coq.mk-n-fun 0 F L R :- !, F {std.rev L} R.
+coq.mk-n-fun N F L (fun _ _ (x\ R x)) :-
+  calc (N - 1) N1,
+  pi x\ coq.mk-n-fun N1 F [x|L] (R x).
+
 func coq.term-is-gref? term -> gref.
 coq.term-is-gref? (global GR) GR.
 coq.term-is-gref? (pglobal GR _) GR.
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 92691fc1..b456ea2c 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -269,7 +269,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   coq.env.indt R tt _ _ _ [K] _,
   GRK = indc K,
   @global! => log.coq.arguments.set-implicit (indt R) [[]],
-  @global! => log.coq.arguments.set-implicit GRK [[]],
 
   factories-provide GRFSwP MLwP,
   w-params.nparams MLwP NParams,
@@ -283,9 +282,10 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   if-verbose (coq.say {header} "declare notation Build"),
 
-  coq.say "Hello, world!",
-  GRDepsClauses => coq.notation.add-abbreviation "Build" 0 (global GRK) tt _,
-
+  GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
+  GRDepsClauses => phant.add-abbreviation "Build_" PhGRK BuildConst BuildAbbrev,
+  calc (NParams + 1) NParams1,
+  GRDepsClauses => coq.notation.add-abbreviation "Build" NParams1 {coq.mk-n-fun NParams1 (args\ coq.mk-app (global GRK) {std.append args {coq.mk-n-holes {std.length {list-w-params_list MLwP}}}}) []} tt _,
   if-verbose (coq.say {header} "declare notation axioms"),
 
   if (D = asset-mixin)
@@ -297,12 +297,12 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "start module Exports"),
 
   log.coq.env.begin-module "Exports" none,
-  coq.say "Declaring mixin as typeclass",
 	coq.TC.declare-class (indt R),
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
     factory->constructor (indt R) GRK,
     factory->nparams (indt R) NParams,
+    phant-abbrev GRK (const BuildConst) BuildAbbrev,
     % gref->deps GRFSort MLwP,
     % factory-sort FactorySortCoe,
   ]] NewClauses,
@@ -312,7 +312,15 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   std.map MLwoP (_\ r\ r = maximal) Implicits,
   std.map {std.iota NParams} (_\ r\ r = explicit) Explicits,
   /* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */
-  @global! => log.coq.arguments.set-implicit GRK [[explicit|{std.append Explicits Implicits}]],
+
+  NewImplicits = [explicit|{std.append Explicits Implicits}],
+  coq.arguments.set-default-implicit GRK,
+  coq.arguments.implicit GRK [GRKImplicits|_],
+  std.drop {std.length NewImplicits} GRKImplicits RImplicits, 
+
+  if (std.forall RImplicits(x\ x = explicit)) 
+    (@global! => log.coq.arguments.set-implicit GRK [NewImplicits])
+    (@global! => log.coq.arguments.set-implicit GRK [NewImplicits, {std.append NewImplicits RImplicits}]),
   % @global! => log.coq.coercion.declare FactorySortCoe,
 
   log.coq.env.end-module-name "Exports" Exports,
diff --git a/HB/instance.elpi b/HB/instance.elpi
index f7f6eb1a..6b710273 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -18,6 +18,23 @@ declare-existing T0 F0 :- std.do! [
   acc-clauses current Clauses,
 ].
 
+func elaborate-w-tc term -> term, term, diagnostic.
+elaborate-w-tc (fun N BTy Skel) (prod N BTy Ty) (fun N BTy Body) Diag :-
+  @pi-decl N BTy x\ elaborate-w-tc (Skel x) (Ty x) (Body x) Diag.
+elaborate-w-tc (app [KFactory|Args]) Ty Body Diag :-
+  coq.typecheck KFactory TyFactory ok,
+  coq.prod-tgt->gref TyFactory Factory,
+  factory->nparams Factory NParams,
+  std.length {list-w-params_list {gref->deps Factory}} NDeps,
+  calc (NParams + NDeps + 1) N,
+  std.split-at N Args NArgs Rest,
+  std.assert-ok! (coq.elaborate-skeleton (app [KFactory|NArgs]) _ Head) "tc resolution of mixins failed",
+  coq.elaborate-skeleton {coq.mk-app Head Rest} Ty Body Diag.
+  
+
+  
+  
+
 % [declare-const N B Ty CFL CSL] adds a Definition N : Ty := B where Ty is a factory
 % and equips the type the factory is used on with all the canonical structures
 % that can be built using factory instance B. CFL contains the list of
@@ -26,7 +43,7 @@ func declare-const id, term, arity -> list (pair id constant), list (pair id con
 declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
   std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
   coq.arity->term TyWP Ty,
-  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",
+  std.assert-ok! (d\ elaborate-w-tc BodySkel Ty Body d; coq.elaborate-skeleton BodySkel Ty Body d) "Definition illtyped",
 
   % handle parameters via a section -- begin
   if (TyWP = arity SectionTy) (
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 5a02db76..e8410e0c 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -132,7 +132,7 @@ declare Module BSkel Sort :- std.do! [
     NewClauses,
   acc-clauses current NewClauses,
   std.map MixinClauses (c\ r\ r = clause _ _ c) MixinClauses0,
-  coq.elpi.accumulate-clauses _ "tc.db" MixinClauses0,
+  coq.elpi.accumulate-clauses current "tc.db" MixinClauses0,
 
   if-verbose (coq.say {header} "stop module Exports"),
   log.coq.env.end-module-name "Exports" Exports,
@@ -236,8 +236,7 @@ mixin-clause S I M Clause :-
       coq.unify-eq ST KSParamsC ok,
       coq.unify-eq CT CBody ok,
       std.nth I MIL Inst)
-  ) clause) clause) clause) Clause,
-  coq.say "Clause for " M " is " Clause.
+  ) clause) clause) clause) Clause.
       
       
 

From 5ec8c23dc56a3ff9be8327b7f88c0df89d7ed393 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 8 Jun 2026 14:31:11 +0200
Subject: [PATCH 6/9] add alias for Axioms_ with different implicits

---
 HB/factory.elpi | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index b456ea2c..793cf77b 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -282,10 +282,11 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   if-verbose (coq.say {header} "declare notation Build"),
 
+  GRDepsClauses => coq.env.add-const "Axioms" (global GRK) _ ff GRK0,
   GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
   GRDepsClauses => phant.add-abbreviation "Build_" PhGRK BuildConst BuildAbbrev,
   calc (NParams + 1) NParams1,
-  GRDepsClauses => coq.notation.add-abbreviation "Build" NParams1 {coq.mk-n-fun NParams1 (args\ coq.mk-app (global GRK) {std.append args {coq.mk-n-holes {std.length {list-w-params_list MLwP}}}}) []} tt _,
+  GRDepsClauses => coq.notation.add-abbreviation "Build" NParams1 {coq.mk-n-fun NParams1 (args\ coq.mk-app (global (const GRK0)) {std.append args {coq.mk-n-holes {std.length {list-w-params_list MLwP}}}}) []} tt _,
   if-verbose (coq.say {header} "declare notation axioms"),
 
   if (D = asset-mixin)
@@ -312,6 +313,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   std.map MLwoP (_\ r\ r = maximal) Implicits,
   std.map {std.iota NParams} (_\ r\ r = explicit) Explicits,
   /* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */
+  @global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],
+
 
   NewImplicits = [explicit|{std.append Explicits Implicits}],
   coq.arguments.set-default-implicit GRK,
@@ -319,8 +322,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   std.drop {std.length NewImplicits} GRKImplicits RImplicits, 
 
   if (std.forall RImplicits(x\ x = explicit)) 
-    (@global! => log.coq.arguments.set-implicit GRK [NewImplicits])
-    (@global! => log.coq.arguments.set-implicit GRK [NewImplicits, {std.append NewImplicits RImplicits}]),
+    (@global! => log.coq.arguments.set-implicit (const GRK0) [NewImplicits])
+    (@global! => log.coq.arguments.set-implicit (const GRK0) [NewImplicits, {std.append NewImplicits RImplicits}]),
   % @global! => log.coq.coercion.declare FactorySortCoe,
 
   log.coq.env.end-module-name "Exports" Exports,

From 06adff4801949c1ab43c55a1bfcba1e3dbfefee1 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Fri, 12 Jun 2026 15:31:20 +0200
Subject: [PATCH 7/9] override tc solver for mixin's axioms_

---
 HB/factory.elpi | 1 +
 1 file changed, 1 insertion(+)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index 793cf77b..41da8f13 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -299,6 +299,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   log.coq.env.begin-module "Exports" none,
 	coq.TC.declare-class (indt R),
+  coq.TC.override-solver "axioms_",
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
     factory->constructor (indt R) GRK,

From d11186531aab860f141a35f0c890755b5743fec8 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Fri, 12 Jun 2026 16:56:19 +0200
Subject: [PATCH 8/9] fix override

---
 HB/factory.elpi | 2 +-
 HB/structures.v | 9 +++++++--
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index 41da8f13..df9c4373 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -299,7 +299,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   log.coq.env.begin-module "Exports" none,
 	coq.TC.declare-class (indt R),
-  coq.TC.override-solver "axioms_",
+  coq.TC.override-solver ["axioms_"],
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
     factory->constructor (indt R) GRK,
diff --git a/HB/structures.v b/HB/structures.v
index 583854d9..7bfdfc19 100644
--- a/HB/structures.v
+++ b/HB/structures.v
@@ -24,8 +24,7 @@ From elpi Require Import elpi tc.
 
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 
-TC.AddAllClasses.
-TC.AddAllInstances.
+Elpi TC Solver Override TC.Solver None.
 
 Register unify as hb.unify.
 Register id_phant as hb.id.
@@ -469,6 +468,7 @@ HB.mixin Record MixinName T & Factory1 T & … & FactoryN T := {
 *)
 
 #[arguments(raw)] Elpi Command HB.mixin.
+Elpi Accumulate Plugin "tc-builtin.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File tc_aux.
@@ -654,6 +654,7 @@ HB.structure Definition StructureName params :=
 *)
 
 #[arguments(raw)] Elpi Command HB.structure.
+Elpi Accumulate Plugin "tc-builtin.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File tc_aux.
@@ -739,6 +740,7 @@ Elpi Export HB.structure.
 *)
 
 #[arguments(raw)] Elpi Command HB.saturate.
+Elpi Accumulate Plugin "tc-builtin.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File tc_aux.
@@ -834,6 +836,7 @@ Elpi Export HB.instance.
 (** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)
 
 #[arguments(raw)] Elpi Command HB.factory.
+Elpi Accumulate Plugin "tc-builtin.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File tc_aux.
@@ -919,6 +922,7 @@ HB.end.
 *)
 
 #[arguments(raw)] Elpi Command HB.builders.
+Elpi Accumulate Plugin "tc-builtin.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File tc_aux.
@@ -1168,6 +1172,7 @@ HB.instance Definition _ : Ml ... T := ml.
 *)
 
 #[arguments(raw)] Elpi Command HB.declare.
+Elpi Accumulate Plugin "tc-builtin.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File tc_aux.

From 15582e1f06ab2157db291e134f7f37a1a8405456 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Wed, 17 Jun 2026 15:28:05 +0200
Subject: [PATCH 9/9] declare mixin instances only for the first class

---
 HB/factory.elpi   | 2 +-
 HB/instance.elpi  | 1 +
 HB/structure.elpi | 9 ++++++---
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/HB/factory.elpi b/HB/factory.elpi
index df9c4373..85759229 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -299,7 +299,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   log.coq.env.begin-module "Exports" none,
 	coq.TC.declare-class (indt R),
-  coq.TC.override-solver ["axioms_"],
+  coq.TC.override-solver "TC.Solver" ["axioms_"],
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
     factory->constructor (indt R) GRK,
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 6b710273..ef5cc766 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -27,6 +27,7 @@ elaborate-w-tc (app [KFactory|Args]) Ty Body Diag :-
   factory->nparams Factory NParams,
   std.length {list-w-params_list {gref->deps Factory}} NDeps,
   calc (NParams + NDeps + 1) N,
+  N =< {std.length Args},
   std.split-at N Args NArgs Rest,
   std.assert-ok! (coq.elaborate-skeleton (app [KFactory|NArgs]) _ Head) "tc resolution of mixins failed",
   coq.elaborate-skeleton {coq.mk-app Head Rest} Ty Body Diag.
diff --git a/HB/structure.elpi b/HB/structure.elpi
index e8410e0c..a554967d 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -47,9 +47,10 @@ declare Module BSkel Sort :- std.do! [
   GRDepsClauses =
     [gref->deps (indt ClassInd) NilwP, gref->deps (indc ClassK) MLwP],
   std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
-  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => Factories => std.map-i ML (private.mixin-clause Structure) MixinClauses,
   std.filter ML (m\ not (mixin->first-class m _)) NewMixins,
   std.map NewMixins (m\ r\ r = mixin->first-class m ClassName) MixinFirstClass,
+  [class-def CurrentClass, StructKeyClause | GRDepsClauses] => MixinFirstClass => Factories => std.map-i ML (private.mixin-clause Structure) OptMixinClauses,
+  std.map-filter OptMixinClauses (c\c'\ c = some c') MixinClauses,
 
 
   if-verbose (coq.say {header} "structure: new mixins" NewMixins),
@@ -204,11 +205,12 @@ clause.mk-n-pis N Args P (pi x\ Clause x) :-
   calc (N - 1) N0,
   pi x\ clause.mk-n-pis N0 [x|Args] P (Clause x).
 
-func mixin-clause structure, int, mixinname -> prop.
+func mixin-clause structure, int, mixinname -> option prop.
 mixin-clause S I M Clause :-
   structure-key SortProj _ S, !,
   get-constructor S KS,
   class-def (class (indt Class) S CMLwP), !,
+  if (not (mixin->first-class M (indt Class))) (Clause = none) (
   get-constructor (indt Class) KC,
   tc.gref->pred-name M PredName,
   gref->deps M MDeps,
@@ -236,7 +238,8 @@ mixin-clause S I M Clause :-
       coq.unify-eq ST KSParamsC ok,
       coq.unify-eq CT CBody ok,
       std.nth I MIL Inst)
-  ) clause) clause) clause) Clause.
+  ) clause) clause) clause) Clause',
+  Clause = some Clause').