diff --git a/Changelog.md b/Changelog.md
index 76ab679f..246a3c99 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -3,6 +3,7 @@
 ## Unreleased
 
 - **Removed** the `#[primitive_class]` attribute, making it the default.
+- **New** `HB.saturate` to saturate instances w.r.t. the current hierarchy
 
 ## [1.6.0] - 2023-09-20
 
diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index 05182baf..d583b4c3 100644
--- a/HB/common/database.elpi
+++ b/HB/common/database.elpi
@@ -133,6 +133,38 @@ factories-provide FLwP MLwP :- std.do! [
   w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
 ].
 
+pred undup-grefs  i:list gref, o:list gref.
+undup-grefs  L UL :- std.do! [
+  coq.gref.list->set L S, 
+  coq.gref.set.elements S UL,
+].
+
+pred undup-sorts i:list sort, o:list sort.
+undup-sorts L R :- std.do! [
+  
+  if (std.mem L prop) (R1 = [prop]) (R1 = []),
+  if (std.mem L sprop) (R2 = [sprop]) (R2 = []),
+  if (std.mem L (typ _)) (R3 = [typ _]) (R3 = []),
+  
+  std.flatten [R1, R2, R3] R,
+].
+
+% also prunes cs-default
+pred undup-cs-patterns  i:list cs-pattern, o:list cs-pattern.
+undup-cs-patterns L R :- std.do! [
+  std.map-filter L (x\r\ x = cs-gref r) LGR,
+  undup-grefs LGR ULGR,
+  std.map ULGR (x\r\ r = cs-gref x) R1,
+
+  std.map-filter L (x\r\ x = cs-sort r) LS,
+  undup-sorts LS ULS,
+  std.map ULS (x\r\ r = cs-sort x) R2,
+
+  if (std.mem L cs-prod) (R3 = [cs-prod]) (R3 = []),
+
+  std.flatten [R1, R2, R3] R,
+].
+
 % Mixins can be topologically sorted according to their dependencies
 pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
 toposort-mixins In Out :- std.do! [
@@ -192,6 +224,13 @@ findall-builders LFIL :-
   std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted,
   std.bubblesort LFILunsorted leq-builder LFIL.
 
+pred findall-has-mixin-instance o:list prop.
+findall-has-mixin-instance CL :-
+   std.findall (has-mixin-instance  _ _ _) CL.
+
+pred has-mixin-instance_key i:prop, o:cs-pattern.
+has-mixin-instance_key (has-mixin-instance P _ _) P.
+
 pred findall-mixin-src i:term, o:list mixinname.
 findall-mixin-src T ML :-
   std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.
@@ -299,7 +338,7 @@ get-constructor (indt R) (indc K) :- !,
  if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" R).
 get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
-%% finding for locally defined structures
+% finding for locally defined structures
 pred get-cs-structure i:cs-instance, o:structure.
 get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [
   coq.env.typeof (const Inst) InstTy,
@@ -313,17 +352,64 @@ get-cs-instance (cs-instance _ _ (const Inst)) Inst.
 pred has-cs-instance i:gref, i:cs-instance.
 has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
-pred term->cs-pattern i:term, o:cs-pattern.
-term->cs-pattern (prod _ _ _) cs-prod.
-term->cs-pattern (sort U) (cs-sort U).
-term->cs-pattern T (cs-gref GR) :- term->gref T GR.
-term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
-
-pred cs-pattern->name i:cs-pattern, o:string.
-cs-pattern->name cs-prod "prod".
-cs-pattern->name (cs-sort _) "sort".
-cs-pattern->name cs-default "default".
-cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
+
+pred mixin-src->has-mixin-instance i:prop, o:prop.
+mixin-src->has-mixin-instance  (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
+  term->gref I IHd.
+
+mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
+  term->gref I IHd.
+  
+mixin-src->has-mixin-instance (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd):-
+  term->gref I IHd.
+
+mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
+  term->gref I IHd.
+
+% this auxiliary function iterates over the list of arguments of an application,
+% and create the necessary unify condition for each arguments 
+% and at the end returns the mixin-src clause with all the conditions
+pred mixin-instance-type->mixin-src.aux 
+  i:list term, % list of arguments
+  i:term, % head of the original application
+  i:mixinname, % name of mixin
+  i:term, % instance body
+  i:list prop, % Cond list
+  o:prop.
+mixin-instance-type->mixin-src.aux [] T M I Cond (mixin-src T M I :- Cond).
+mixin-instance-type->mixin-src.aux [A|Args] T M I Cond  (pi a \ C a) :-
+  pi a \
+  sigma Ta\
+    coq.mk-app T [a] Ta,
+    mixin-instance-type->mixin-src.aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a).
+
+
+% transforms the type of a mixin instance into a
+% mixin-src clause with eventual conditions regarding its parameters
+pred mixin-instance-type->mixin-src
+  i:term, % type of the instance Ty
+  i:mixinname, % name of mixin
+  i:term, % instance body I of type Ty
+  i:list prop, % Cond list
+  o:prop.
+
+mixin-instance-type->mixin-src (app _ as F) M I Cond C :-
+  factory? F (triple _ _ Subject),
+  safe-dest-app Subject Hd Args,
+  mixin-instance-type->mixin-src.aux Args Hd M I Cond C.
+
+mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :-
+  pi a\
+  sigma  Ia \
+  coq.mk-app I [a] Ia,
+    mixin-instance-type->mixin-src (F a) M Ia Cond (C a).
+
+pred has-mixin-instance->mixin-src i:prop, o:prop.
+has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![
+  T = global IHd,
+  coq.env.typeof IHd Ty,
+  mixin-instance-type->mixin-src Ty M T [] C,
+].
 
 pred get-canonical-structures i:term, o:list structure.
 get-canonical-structures TyTrm StructL :- std.do! [
diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
index cd1ffaa4..fac753e4 100644
--- a/HB/common/stdpp.elpi
+++ b/HB/common/stdpp.elpi
@@ -123,6 +123,12 @@ pred coq.env.current-library o:string.
 coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
+pred coq.term-is-gref? i:term, o:gref.
+coq.term-is-gref? (global GR) GR :- !.
+coq.term-is-gref? (pglobal GR _) GR :- !.
+coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR.
+coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR.
+
 pred coq.prod-tgt->gref i:term, o:gref.
 coq.prod-tgt->gref T GR :- whd1 T T1, !, coq.prod-tgt->gref T1 GR.
 coq.prod-tgt->gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ coq.prod-tgt->gref (Tgt x) GR.
@@ -245,3 +251,86 @@ coq.fold-map (primitive _ as C) A C A :- !.
 coq.fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A coq.fold-map L1 A1, coq.mk-app-uvar M L1 W.
 % when used in CHR rules
 coq.fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A coq.fold-map L1 A1.
+
+pred cs-pattern->term i:cs-pattern, o:term.
+cs-pattern->term (cs-gref GR) T :- coq.env.global GR T.
+cs-pattern->term (cs-sort prop) (sort prop).
+cs-pattern->term (cs-sort sprop) (sort sprop).
+cs-pattern->term (cs-sort _) T :- coq.elaborate-skeleton {{ Type }} _ T ok.
+cs-pattern->term cs-prod T :- coq.elaborate-skeleton (prod `x` Ty_ x\ Bo_ x) _ T ok.
+
+pred term->cs-pattern i:term, o:cs-pattern.
+term->cs-pattern (prod _ _ _) cs-prod.
+term->cs-pattern (sort U) (cs-sort U).
+term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR.
+term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
+
+pred cs-pattern->name i:cs-pattern, o:string.
+cs-pattern->name cs-prod "prod".
+cs-pattern->name (cs-sort _) "sort".
+cs-pattern->name cs-default "default".
+cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
+
+% ---------------------------------------------------------------------
+% kit for closing a term by abstracting evars with lambdas
+% we use constraints to attach to holes a number
+% and replace them by a special node, to later be bound
+% via a lambda
+
+namespace abstract-holes {
+
+% we add a new constructor to terms to represent terms to be abstracted
+type abs int -> term.
+
+% bind back abstracted subterms
+pred bind i:int, i:int, i:term, o:term.
+bind I M T T1 :- M > I, !,
+  T1 = {{ fun x => lp:(B x) }},   
+  N is I + 1,
+  pi x\                           % we allocate the fresh symbol for (abs M)
+    (copy (abs N) x :- !) =>      % we schedule the replacement (abs M) -> x
+    bind N M T (B x).
+bind M M T T1 :- copy T T1.         % we perform all the replacements
+
+% for a term with M holes, returns a term with M variables to fill these holes
+% the clause see is only generated for a term if it hasn't been seen before
+% the term might need to be typechecked first or main generates extra holes for the
+% type of the parameters
+pred main i:term, o:term.
+main T1 T3 :- std.do! [
+  % we put (abs N) in place of each occurrence of the same hole
+  (pi T Ty N N' M \ fold-map T N (abs M) M :- var T, not (seen? T _), !, coq.typecheck T Ty ok, fold-map Ty N _ N', M is N' + 1, seen! T M) =>
+  (pi T N M \ fold-map T N (abs M) N :- var T, seen? T M, !) =>
+    fold-map T1 0 T2 M,
+  % we abstract M holes (M abs nodes)
+  bind 0 M T2 T3,
+  % cleanup constraint store
+  purge-seen!,
+].
+
+% all constraints are also on _ so that they share
+% a variable with the constraint to purge the store
+
+% we query if the hole was seen before, and if so
+% we fetch its number
+pred seen? i:term, o:int.
+seen? X Y :- declare_constraint (seen? X Y) [X,_].  
+
+% we declare it is now seen and label it with a number
+pred seen! i:term, i:int.
+seen! X Y :- declare_constraint (seen! X Y) [X,_].
+
+% to empty the store
+pred purge-seen!.
+purge-seen! :- declare_constraint purge-seen! [_].
+
+constraint seen? seen! purge-seen!  {
+  % a succesful query, give the label back via M
+  rule (seen! X N) \ (seen? X M) <=> (M = N).
+  % an unsuccesful query
+  rule             \ (seen? X _) <=> false.
+
+  rule purge-seen! \ (seen! _ _).
+  rule \ purge-seen!.
+}
+}
\ No newline at end of file
diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi
index 3f94a7ed..fa7552b0 100644
--- a/HB/common/utils.elpi
+++ b/HB/common/utils.elpi
@@ -374,4 +374,11 @@ prod-last X X :- !.
 
 pred prod-last-gref i:term, o:gref.
 prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR.
-prod-last-gref X GR :- coq.term->gref X GR.
\ No newline at end of file
+prod-last-gref X GR :- coq.term->gref X GR.
+
+% saturate a type constructor with holes
+pred saturate-type-constructor i:term, o:term .
+saturate-type-constructor T ET :- 
+  coq.typecheck T TH ok,
+  coq.count-prods TH N,
+  coq.mk-app T {coq.mk-n-holes N} ET.
diff --git a/HB/factory.elpi b/HB/factory.elpi
index 6fe74186..8ff72665 100644
--- a/HB/factory.elpi
+++ b/HB/factory.elpi
@@ -53,7 +53,7 @@ argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
 pred argument-name i:argument, o:string.
 argument-name (const-decl Id _ _) Id :- !.
 argument-name (indt-decl (parameter _ _ _ R)) Id :- !,
-  argument-name (indt-decl (R (sort prop))) Id.
+argument-name (indt-decl (R (sort prop))) Id.
 argument-name (indt-decl (record Id _ _ _)) Id :- !.
 argument-name (indt-decl (inductive Id _ _ _)) Id :- !.
 argument-name (ctx-decl _) "_" :- !.
@@ -231,7 +231,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-  % coq.say RDecl RDeclClosed,
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 0b793248..7e931d49 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -15,7 +15,7 @@ declare-existing T0 F0 :- std.do! [
      "The type of the instance is not a factory",
   factory-alias->gref FactoryAlias Factory,
   private.declare-instance Factory T F Clauses _,
-  acc-clauses current Clauses
+  acc-clauses current Clauses,
 ].
 
 % [declare-const N B Ty] adds a Definition N : Ty := B where Ty is a factory
@@ -86,6 +86,44 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
 % Each mixin used in order to fulfill a class is returned together with its name.
 pred declare-all i:term, i:list class, o:list (pair id constant).
 declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
+
+  infer-class T Class Struct MLwP S Name STy Clauses,
+
+  !,
+
+  decl-const-in-struct Name S STy CS,
+
+  Clauses => declare-all T Rest L.
+
+declare-all T [_|Rest] L :- declare-all T Rest L.
+declare-all _ [] [].
+
+% for generic types, we need first to instantiate them by giving them holes,
+% so they can be used to instantiate the classes
+pred declare-all-on-type-constructor i:term, i:list class, o:list (pair id constant).
+declare-all-on-type-constructor T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
+
+  %TODO: compute the arity of the Class subject and saturate up to that point
+  %      there may even be more than one possibility
+  saturate-type-constructor T Ty,
+
+  infer-class Ty Class Struct MLwP S Name _STy Clauses,
+
+  !,
+
+  abstract-holes.main S SC,
+  std.assert-ok! (coq.typecheck SC SCTy) "declare-all-on-type-constructor: badly closed",
+  
+  decl-const-in-struct Name SC SCTy CS,
+
+  Clauses => declare-all-on-type-constructor T Rest L.
+
+declare-all-on-type-constructor T [_|Rest] L :- declare-all-on-type-constructor T Rest L.
+declare-all-on-type-constructor _ [] [].
+
+pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop.
+infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
+
   if (not(has-CS-instance? T Struct))
      true % we build it
      (if-verbose (coq.say {header} "skipping already existing"
@@ -101,8 +139,6 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
         {coq.term->string T}))
      fail,
 
-  !,
-
   Name is {cs-pattern->name {term->cs-pattern T}}
     ^ "__canonical__" ^ {gref->modname Struct 2 "_" },
 
@@ -113,18 +149,18 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
   private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses,
   coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S,
   if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),
-  std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped",
+  std.assert-ok! (coq.typecheck S STy) "infer-class: S illtyped",
+].
+
+pred decl-const-in-struct i:string, i:term, i:term, i:constant.
+decl-const-in-struct Name S STy CS:- std.do![
 
   log.coq.env.add-const-noimplicits Name S STy @transparent! CS, % Bug coq/coq#11155, could be a Let
   with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
-
   acc-clause current (local-canonical CS),
-
   if-verbose (coq.say {header} "structure instance" Name "declared"),
+].
 
-  Clauses => declare-all T Rest L.
-declare-all T [_|Rest] L :- declare-all T Rest L.
-declare-all _ [] [].
 
 pred declare-factory-sort-deps i:gref.
 declare-factory-sort-deps  GR :- std.do! [
@@ -189,6 +225,29 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
   declare-const "_" GCF (arity FGCF) CSL
 ].
 
+% create instances for all possible combinations of types and structure compatible 
+pred saturate-instances.
+saturate-instances :- std.do! [
+  findall-has-mixin-instance ClausesHas,
+
+  std.map ClausesHas has-mixin-instance_key KL,
+  undup-cs-patterns KL UKL,
+  std.map UKL cs-pattern->term TL,
+
+  findall-classes AllClasses,
+
+  std.map ClausesHas has-mixin-instance->mixin-src Clauses,
+  
+  Clauses => std.forall2 TL UKL (t\k\sigma Classes\
+    std.filter AllClasses (no-instance-for k) Classes,
+    declare-all-on-type-constructor t Classes _),
+].
+
+pred no-instance-for i:cs-pattern, i:class.
+no-instance-for K (class _ S _) :-
+  get-structure-sort-projection S (global Proj),
+  coq.CS.db-for Proj K [].
+
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */
 /* ------------------------------------------------------------------------- */
@@ -208,11 +267,12 @@ declare-instance Factory T F Clauses CSL :-
   declare-canonical-instances-from-factory-and-local-builders Factory
     T F TheFactory FGR Clauses CSL.
 declare-instance Factory T F Clauses CSL :-
-  declare-canonical-instances-from-factory Factory T F CSL,
+  declare-canonical-instances-from-factory Factory T F Clauses1 CSL,
   if (get-option "export" tt)
      (coq.env.current-library File,
-      std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses)
-     (Clauses = []).
+      std.map CSL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
+     (Clauses2 = []),
+     std.append Clauses1 Clauses2 Clauses.
 
 % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type
 % T built from factory F
@@ -271,6 +331,7 @@ postulate-arity (arity Ty) ArgsRev X T Ty :-
   hd-beta X {std.rev ArgsRev} X1 Stack1,
   unwind X1 Stack1 T.
 
+
 % We find the new mixins that F build, we build them and shedule them
 % for becoming builders at section closing time. We also declare
 % all canonical instances these new mixins allow for, so that the user
@@ -284,7 +345,7 @@ declare-canonical-instances-from-factory-and-local-builders
       add-all-mixins T FGR NewMixins ff Clauses MCSL,
   ]),
   list-w-params_list {factory-provides Factory} ML,
-  Clauses => instance.declare-all T {findall-classes-for ML} CCSL,
+  Clauses => declare-all T {findall-classes-for ML} CCSL,
   std.append MCSL CCSL CSL
 ].
 
@@ -292,8 +353,8 @@ declare-canonical-instances-from-factory-and-local-builders
 % it uses all known builders to declare canonical instances of structures
 % on T
 pred declare-canonical-instances-from-factory
-  i:factoryname, i:term, i:term, o:list (pair id constant).
-declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
+  i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant).
+declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [
   % The order of the following two "under...do!"  is crucial,
   % priority must be given to canonical mixins
   % as they are the ones which guarantee forgetful inheritance
@@ -301,8 +362,9 @@ declare-canonical-instances-from-factory Factory T F CSL :- std.do! [
   synthesis.under-mixin-src-from-factory.do! T F [
     synthesis.under-local-canonical-mixins-of.do! T [
       list-w-params_list {factory-provides Factory} ML,
-      add-all-mixins T Factory ML tt _ MCSL,
-      instance.declare-all T {findall-classes-for ML} CCSL,
+      add-all-mixins T Factory ML tt Clauses MCSL,
+      std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas,
+      ClausesHas => declare-all T {findall-classes-for ML} CCSL, % declare-all-on-type-constructor doesn't work here
     ]
   ],
   std.append MCSL CCSL CSL
diff --git a/HB/structure.elpi b/HB/structure.elpi
index 2fd1132d..89bf3313 100644
--- a/HB/structure.elpi
+++ b/HB/structure.elpi
@@ -187,7 +187,10 @@ declare Module BSkel Sort :- std.do! [
   NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName),
 
   NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport
-    {w-params.nparams MLwP} ClassProjection GRPack)
+    {w-params.nparams MLwP} ClassProjection GRPack),
+
+% Automatic saturation disabled since it is expensive
+%  NewClauses => instance.saturate-instances,
 ].
 
 /* ------------------------------------------------------------------------- */
@@ -346,8 +349,8 @@ declare-coercion SortProjection ClassProjection
 
   w-params.then FMLwP mk-fun mk-fun
     (mk-coe-class-body FC TC TMLwP) CoeBody,
-
-  std.assert-ok! (coq.elaborate-skeleton CoeBody Ty CoeBody') "declare-coercion: CoeBody illtyped",
+  ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized",
+  std.assert-ok! (coq.elaborate-skeleton CoeBody Ty CoeBody') ErrorMessage,
 
   if-verbose (coq.say {header} "declare coercion hint" CName),
 
@@ -359,7 +362,8 @@ declare-coercion SortProjection ClassProjection
     (mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection)
     SCoeBody,
 
-  std.assert-ok! (coq.elaborate-skeleton SCoeBody STy SCoeBody') "declare-coercion: SCoeBody illtyped",
+ ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized",
+  std.assert-ok! (coq.elaborate-skeleton SCoeBody STy SCoeBody') ErrorMessage,
 
   if-verbose (coq.say {header} "declare unification hint" SName),
 
diff --git a/Makefile b/Makefile
index 2b86211f..14cfc4a9 100644
--- a/Makefile
+++ b/Makefile
@@ -141,5 +141,5 @@ endif
 structures.vo : %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
 
-$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v)): __always__ config build Makefile.test-suite.coq
+$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq
 	+$(COQMAKE_TESTSUITE) $@
diff --git a/README.md b/README.md
index df51bc7e..38b2bf8e 100644
--- a/README.md
+++ b/README.md
@@ -134,6 +134,8 @@ opam install coq-hierarchy-builder
   - `HB.builders` and `HB.end` declare a set of builders,
   - `HB.instance` declares a structure instance,
   - `HB.declare` declares a context with parameters, key and mixins.
+  - `HB.saturate` reconsiders all mixin instances to see if some newly declared
+    structure can be inhabited
 
 - HB core tactic-in-term:
   - `HB.pack` to synthesize a structure instance in the middle of a term.
diff --git a/_CoqProject b/_CoqProject
index b8cf8cf7..057e9001 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,3 +1,7 @@
 structures.v
 -arg -w -arg -elpi.accumulate-syntax
--Q . HB
\ No newline at end of file
+-arg -w -arg +elpi.typecheck
+-Q . HB
+
+-R tests HB.tests
+-R examples HB.examples
\ No newline at end of file
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index 98c20167..391e6c39 100644
--- a/_CoqProject.test-suite
+++ b/_CoqProject.test-suite
@@ -3,6 +3,7 @@
 -arg -w -arg -abstract-large-number
 -arg -w -arg -disj-pattern-notation
 -arg -w -arg -notation-overridden
+-arg -w -arg +elpi.typecheck
 
 examples/readme.v
 examples/hulk.v
@@ -52,6 +53,8 @@ examples/Coq2020_material/CoqWS_abstract.v
 examples/Coq2020_material/CoqWS_expansion/withHB.v
 examples/Coq2020_material/CoqWS_expansion/withoutHB.v
 
+# examples/cat/cat.v
+
 tests/type_of_exported_ops.v
 tests/duplicate_structure.v
 tests/instance_params_no_type.v
@@ -72,6 +75,7 @@ tests/not_same_key.v
 tests/hb_pack.v
 tests/declare.v
 tests/short.v
+tests/instance_before_structure.v
 tests/primitive_records.v
 tests/non_forgetful_inheritance.v
 tests/fix_loop.v
@@ -80,6 +84,16 @@ tests/hnf.v
 tests/fun_instance.v
 tests/issue284.v
 tests/issue287.v
+tests/two_hier.v
+tests/instance_merge_with_param.v
+tests/instance_merge_with_distinct_param.v
+tests/instance_merge.v
+
+tests/unit/enrich_type.v
+tests/unit/mixin_src_has_mixin_instance.v
+tests/unit/mk_src_map.v
+tests/unit/close_hole_term.v
+tests/unit/struct.v
 
 -R tests HB.tests
 -R examples HB.examples
diff --git a/structures.v b/structures.v
index be0c29fa..ca6ae584 100644
--- a/structures.v
+++ b/structures.v
@@ -193,6 +193,11 @@ pred mixin-class o:mixinname, o:classname.
 % Coq's CS database (which is just for structures).
 pred mixin-src o:term, o:mixinname, o:term.
 
+% [has-mixin-instance P M G] states that G is a reference to an instance
+% which can be used to reconstruct an instance 
+% of the form [M P …] with eventually some parameters for P.
+pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref.
+
 %% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % [builder N TheFactory TheMixin S] is used to
@@ -604,9 +609,10 @@ Elpi Accumulate File "HB/structure.elpi".
 Elpi Accumulate lp:{{
 
 main [const-decl N (some B) Arity] :- !, std.do! [
+  % compute the universe for the structure (default )
   prod-last {coq.arity->term Arity} Ty,
-  if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort,
-  with-attributes (with-logging (structure.declare N B Univ))
+  if (ground_term Ty) (Sort = Ty) (Sort = {{Type}}), sort Univ = Sort, 
+  with-attributes (with-logging (structure.declare N B Univ)),
 ].
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 
@@ -618,6 +624,41 @@ Elpi Export HB.structure.
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 
+(* [HB.saturate] saturates all instances w.r.t. the current hierarchy.
+
+   When two (unrelated) files are imported it might be that the instances
+   declared in one file are sufficient to instantiate structures declared
+   in the other file.
+
+   This command reconsiders all types with a canonical structure instance
+   and see if the they are also equipped with new ones.
+*)
+
+#[arguments(raw)] Elpi Command HB.saturate.
+Elpi Accumulate Db hb.db.
+Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/database.elpi".
+#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
+#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
+Elpi Accumulate File "HB/common/log.elpi".
+Elpi Accumulate File "HB/common/synthesis.elpi".
+Elpi Accumulate File "HB/common/phant-abbreviation.elpi".
+Elpi Accumulate File "HB/export.elpi".
+Elpi Accumulate File "HB/instance.elpi".
+Elpi Accumulate File "HB/context.elpi".
+Elpi Accumulate File "HB/factory.elpi".
+Elpi Accumulate lp:{{
+main [] :- !, with-attributes (with-logging (instance.saturate-instances)).
+main _ :- coq.error "Usage: HB.saturate".
+}}.
+Elpi Typecheck.
+Elpi Export HB.saturate.
+
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
 (** [HB.instance] associates to a type all the structures that can be
     obtained from the provided factory inhabitant.
 
diff --git a/tests/instance_before_structure.v b/tests/instance_before_structure.v
new file mode 100644
index 00000000..e8e3cb22
--- /dev/null
+++ b/tests/instance_before_structure.v
@@ -0,0 +1,37 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.mixin Record m3 T := { default3 : T }.
+
+HB.structure Definition s1  := { T of m1 T }.
+
+HB.instance Definition _ : m1 nat := m1.Build nat 1.
+
+HB.about nat.
+
+(* too early *)
+HB.instance Definition _ : m2 nat := m2.Build nat 2.
+
+HB.about nat. (* only s1 on nat *)
+
+HB.instance Definition _ : m3 nat := m3.Build nat 3.
+
+HB.structure Definition s2 := { T of m1 T & m2 T }.
+HB.about nat. (* s2 is not there yet *)
+
+HB.structure Definition s3 := { T of m3 T }.
+HB.about nat. (* s2 has been instanciated but not s3 *)
+
+
+(* here it works *)
+HB.saturate.
+HB.about nat. (* all there *)
+
+Check @default1 nat.
+Check @default2 nat.
+Check @default3 nat.
+
+
diff --git a/tests/instance_merge.v b/tests/instance_merge.v
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/instance_merge_with_distinct_param.v b/tests/instance_merge_with_distinct_param.v
new file mode 100644
index 00000000..413b5834
--- /dev/null
+++ b/tests/instance_merge_with_distinct_param.v
@@ -0,0 +1,45 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+(* since s1 only requires m1 there is a 1:1 correspondence 
+between the structure s1 and the mixin m1 *)
+HB.structure Definition s1 := { T of m1 T }.
+HB.structure Definition s2 := { T of m2 T }.
+
+HB.instance Definition nat_m1 := m1.Build nat 0.
+HB.instance Definition nat_m2 := m2.Build nat 1.
+
+(* with the following example we want to show that list
+preserves the s1 structure ie. if x:s1.type then (list x):s1.type,
+in practice we can use this for the type of polynomials *)
+HB.instance Definition list_m1 (X : s1.type) : m1 (list X) :=
+  m1.Build (list X) (cons default1 nil).
+(* similarly list preserves s2 structure *)
+HB.instance Definition list_m2 (X : s2.type) : m2 (list X) :=
+  m2.Build (list X) (cons default2 nil).
+
+
+HB.structure Definition s3 := { T of m1 T & m2 T }.
+(* since we can preserve m1 and m2 with list, we can preserve s3 as well ! *)
+
+(* 
+if we have a file A with definitions of S1 and S2,
+file B importing Awith definitions of instance nat_m1 and nat_m2
+file C importing A with the definition of s3
+in a file D that imports B and C if we call saturate_instance, we create the instance for s3.
+this example shows the need for a separate command
+*)
+
+Fail Check nat : s3.type.
+HB.saturate.
+Check nat : s3.type.
+(* since nat satisfies s3.type, so does list nat *)
+Check list nat : s3.type.
+Check list (list nat) : s3.type.
+
+Fail Check fun t : s1.type => (list t : s3.type).
+Fail Check fun t : s2.type => (list t : s3.type).
+Check fun t : s3.type => (list t : s3.type).
diff --git a/tests/instance_merge_with_param.v b/tests/instance_merge_with_param.v
new file mode 100644
index 00000000..9fbc0759
--- /dev/null
+++ b/tests/instance_merge_with_param.v
@@ -0,0 +1,26 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.structure Definition s1 := { T of m1 T }.
+HB.structure Definition s2 := { T of m2 T }.
+
+HB.instance Definition _ (X : s1.type) : m1 (list X) :=
+  m1.Build (list X) (cons default1 nil).
+HB.instance Definition list_m2 (X : s1.type) : m2 (list X) :=
+  m2.Build (list X) nil.
+
+HB.structure Definition s3 := { T of m1 T & m2 T }.
+
+HB.about list. (* should have s3 *)
+
+(* The s3 instance on list should be synthetized automatically, *)
+(* But since it's defined afterwards, it's not taken into account. *)
+(* The subtelty now is that there is a parameter, but it's always the same *)
+(* A simple recall suffices: *)
+HB.instance Definition _ (X : s1.type) := list_m2 X.
+HB.about list.
+
+
diff --git a/tests/instance_params_no_type.v b/tests/instance_params_no_type.v
index 5220be11..07087457 100644
--- a/tests/instance_params_no_type.v
+++ b/tests/instance_params_no_type.v
@@ -1,7 +1,41 @@
 From HB Require Import structures.
 
 HB.mixin Record is_foo P A := { op : P -> A -> A }.
+
+HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x).
+HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x).
+HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x).
+
+About list_foo'.
+
 HB.structure Definition foo P := { A of is_foo P A }.
 
-Axiom f : forall T, T -> nat -> nat.
-HB.instance Definition bar P := is_foo.Build P nat (f P).
\ No newline at end of file
+(* .... list A ....
+
+(fun A =>   {|
+    foo.sort := list..;
+    foo.class :=
+      {| foo.instance_params_no_type_is_foo_mixin := list_foo A |}
+  |} ).
+
+
+HB.about foo. *)
+
+(* Elpi Trace Browser. *)
+Check nat_foo.
+Check list_foo.
+HB.mixin Record is_b A:= { default : A }.
+Check foo.type.
+Print foo.type.
+Print Module foo.
+Print foo.axioms_.
+(*Elpi Trace Browser. *)
+HB.structure Definition b := { A of is_b A}.
+HB.instance Definition nat_b := is_b.Build nat 0.
+
+HB.mixin Record is_bar (P : b.type) A := { test : P -> A -> A }.
+
+HB.structure Definition bar P := { A of is_bar P A}.
+HB.instance Definition list_bar P := is_bar.Build P (list P)  (fun _ x => x).
+Check list_bar.
+
diff --git a/tests/two_hier.v b/tests/two_hier.v
new file mode 100644
index 00000000..9d4881f6
--- /dev/null
+++ b/tests/two_hier.v
@@ -0,0 +1,75 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+
+HB.mixin Record m2 T := { default2 : T }.
+
+(* since s1 only requires m1 there is a 1:1 correspondence 
+between the structure s1 and the mixin m1 *)
+HB.structure Definition s1 := { T of m1 T }.
+HB.structure Definition s2 := { T of m2 T }.
+
+HB.instance Definition nat_m1 := m1.Build nat 0.
+HB.instance Definition nat_m2 := m2.Build nat 1.
+
+(* with the following example we want to show that list
+preserves the s1 structure ie. if x:s1.type then (list x):s1.type,
+in practice we can use this for the type of polynomials *)
+HB.instance Definition list_m1 (X : s1.type) : m1 (list X) :=
+  m1.Build (list X) (cons default1 nil).
+(* similarly list preserves s2 structure *)
+HB.instance Definition list_m2 (X : s2.type) : m2 (list X) :=
+  m2.Build (list X) (cons default2 nil).
+
+
+HB.structure Definition s3 := { T of m1 T & m2 T }.
+(* since we can preserve m1 and m2 with list, we can preserve s3 as well ! *)
+
+(* 
+if we have a file A with definitions of S1 and S2,
+file B importing Awith definitions of instance nat_m1 and nat_m2
+file C importing A with the definition of s3
+in a file D that imports B and C if we call saturate_instance, we create the instance for s3.
+this example shows the need for a separate command
+*)
+Fail Check nat : s3.type.
+HB.saturate.
+Check nat : s3.type.
+(* since nat satisfies s3.type, so does list nat *)
+Check list nat : s3.type.
+Check list (list nat) : s3.type.
+
+Fail Check fun t : s1.type => (list t : s3.type).
+Fail Check fun t : s2.type => (list t : s3.type).
+Check fun t : s3.type => (list t : s3.type).
+
+HB.mixin Record m1' (P : s1.type) T := { f1 : P -> T }.
+
+HB.mixin Record m2' (P : s2.type) T := { f2 : P -> T }.
+
+(* since s1 only requires m1 there is a 1:1 correspondence 
+between the structure s1 and the mixin m1 *)
+HB.structure Definition s1' P := { T of m1' P T }.
+HB.structure Definition s2' P := { T of m2' P T }.
+
+HB.instance Definition nat_m1' := m1'.Build nat nat (fun _ => 0).
+HB.instance Definition nat_m2' := m2'.Build nat nat (fun _ => 1).
+
+(* with the following example we want to show that list
+preserves the s1 structure ie. if x:s1.type then (list x):s1.type,
+in practice we can use this for the type of polynomials *)
+HB.instance Definition list_m1' (P : s1.type) (X : s1'.type P) : m1' P (list X) :=
+m1'.Build P (list X) (fun x => cons (f1 x) nil).
+(* similarly list preserves s2 structure *)
+HB.instance Definition list_m2' (P : s2.type) (X : s2'.type P) : m2' P (list X) :=
+  m2'.Build P (list X) (fun x => cons (f2 x) nil).
+
+
+HB.structure Definition s3' (P : s3.type) := { T of m1' P T & m2' P T }.
+Fail Check nat : s3'.type _.
+HB.saturate.
+Check nat : s3'.type _.
+(* since nat satisfies s3'.type, so does list nat *)
+Check list nat : s3'.type _.
+Check Datatypes_list__canonical__two_hier_s3'.
+Check list (list nat) : s3'.type _.
\ No newline at end of file
diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v
new file mode 100644
index 00000000..4b63a08a
--- /dev/null
+++ b/tests/unit/close_hole_term.v
@@ -0,0 +1,29 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+From Coq Require Export Setoid.
+
+Elpi Query HB.instance lp:{{
+    X = app [{{list}}, Y],
+    % X needs to be typechecked here to get rid of the hole for the type of Y
+    coq.typecheck X _ ok,
+    abstract-holes.main X Z,
+    std.assert! (Z = {{fun x => list x}}) "term badly closed"
+}}.
+
+Elpi Query HB.instance lp:{{
+    abstract-holes.main {{nat}} Z,
+    std.assert! (Z = {{nat}}) "term badly closed"
+}}.
+
+
+Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
+inj x y : S (f x) (f y) -> R x y.
+
+Elpi Query HB.structure lp:{{
+    Y = {{Inj}}, %Inj has 5 implicit arguments
+    saturate-type-constructor Y X,
+    % X needs to be typechecked here to get rid of the holes of the types of its arguments
+    coq.typecheck X _ ok,
+    abstract-holes.main X Z,
+    std.assert! (Z = {{ fun a b c d e => @Inj a b c d e }}) "term badly closed"
+}}.
\ No newline at end of file
diff --git a/tests/unit/enrich_type.v b/tests/unit/enrich_type.v
new file mode 100644
index 00000000..72947365
--- /dev/null
+++ b/tests/unit/enrich_type.v
@@ -0,0 +1,27 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+From Coq Require Export Setoid.
+
+Elpi Query HB.structure lp:{{
+    saturate-type-constructor {{nat}} X,
+    std.assert! (X = {{nat}}) "wrong enriched type"
+}}.
+
+Elpi Query HB.structure lp:{{
+    saturate-type-constructor {{list}} X,
+    std.assert! (X = app [{{list}}, Y]) "wrong enriched type"
+}}.
+
+Elpi Query HB.structure lp:{{
+    Y = (x \ (y \ {{(prod (list lp:x) (list lp:y))}})),
+    saturate-type-constructor (Y _ _) X,
+    std.assert! (X = (app [{{prod}}, (app[{{list}},X1]), app[{{list}},C]])) "wrong enriched type"
+}}.
+
+Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
+inj x y : S (f x) (f y) -> R x y.
+
+Elpi Query HB.structure lp:{{
+    saturate-type-constructor {{Inj}} X,
+    std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type"
+}}.
diff --git a/tests/unit/mixin_src_has_mixin_instance.v b/tests/unit/mixin_src_has_mixin_instance.v
new file mode 100644
index 00000000..0694875f
--- /dev/null
+++ b/tests/unit/mixin_src_has_mixin_instance.v
@@ -0,0 +1,30 @@
+From HB Require Import structures.
+From elpi Require Import elpi.
+
+HB.mixin Record m1 T := { default1 : T }.
+HB.mixin Record m2 T := { default2 : T }.
+
+HB.structure Definition s1 := { T of m1 T }.
+HB.instance Definition i1 (X : s1.type) : m1 (list X) :=
+m1.Build (list X) (cons default1 nil).
+
+HB.instance Definition nat_m1 : m1 nat := m1.Build nat 1.
+HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1.
+
+
+Elpi Query HB.instance lp:{{
+mixin-src->has-mixin-instance (mixin-src {{nat}} M1 {{nat_m1}}) Y,
+Y = has-mixin-instance (cs-gref {{:gref nat}}) {{:gref m1.phant_axioms}} {{:gref nat_m1}}.
+
+}}.
+
+Section Test.
+Variable X:s1.type.
+
+Elpi Query HB.instance lp:{{
+mixin-src->has-mixin-instance (mixin-src {{list X}} M1 {{i1 X}}) Y,
+Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}}.
+
+}}.
+End Test.
+
diff --git a/tests/unit/mk_src_map.v b/tests/unit/mk_src_map.v
new file mode 100644
index 00000000..2be9718a
--- /dev/null
+++ b/tests/unit/mk_src_map.v
@@ -0,0 +1,26 @@
+From HB Require Import structures.
+
+HB.mixin Record is_foo P A := { op : P -> A -> A }.
+HB.mixin Record is_foo' P A := { op : P -> A -> A }.
+
+HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x).
+
+HB.instance Definition list_foo' P A := is_foo.Build P (list A) (fun _ x => x).
+Check list_foo'.
+Check list_foo.
+
+Elpi Query HB.structure lp:{{
+
+has-mixin-instance->mixin-src (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo}}) MS,
+    MS = (pi a b \ 
+        mixin-src (app [{{list}}, b]) ({{:gref is_foo.axioms_}}) (app [{{list_foo}}, a]) 
+            :- [coq.unify-eq a b ok])
+}}.
+
+Elpi Query HB.structure lp:{{
+
+has-mixin-instance->mixin-src (has-mixin-instance (cs-gref{{:gref list}}) {{:gref is_foo.axioms_}} {{:gref list_foo'}}) MS',
+MS' = (pi p a b \ 
+    mixin-src (app [{{list}}, b]) {{:gref is_foo.axioms_}} (app [{{list_foo'}}, p,a])
+        :- [coq.unify-eq  a b ok]).
+}}.
\ No newline at end of file
diff --git a/tests/unit/struct.v b/tests/unit/struct.v
new file mode 100644
index 00000000..16e6afd1
--- /dev/null
+++ b/tests/unit/struct.v
@@ -0,0 +1,36 @@
+From HB Require Import structures.
+
+HB.mixin Record m1 T := { default1 : T }.
+HB.mixin Record m2 T := { default2 : T }.
+HB.mixin Record is_foo P A := { op : P -> A -> A }.
+HB.structure Definition foo P := { A  of is_foo P A}.
+HB.structure Definition foo1 := { A of is_foo (option nat) A & m1 A}.
+
+
+Elpi Query HB.structure lp:{{
+std.findall (has-mixin-instance _ _ _) H
+}}.
+
+(* here we don't have any declared instances but a clause is still created by the system  : 
+has-mixin-instance (cs-gref (const «eta»)) (indt «is_foo.axioms_») (const «struct_foo1__to__struct_is_foo»)
+struct_foo1__to__struct_is_foo is an instance created by the system upon structure declaration to allow 
+coercions from foo1 to other structures with the mixin is_foo.
+*)
+Print struct_foo1__to__struct_foo.
+
+(* its type is
+forall A : foo1.type, is_foo.axioms_ (option nat) (eta A))
+which means it can't serve as a coercion for foo2 or foo3,
+
+however foo3 can still be declared because it has another mixin,
+while foo2 can't because it has the exact same mixins than foo
+
+*)
+
+
+Fail HB.structure Definition foo2 := { A of is_foo bool A}.
+
+
+HB.structure Definition foo3 := { A of is_foo bool A & m2 A}.
+
+Fail HB.structure Definition fooj := { A of foo1 A & foo3 A}.