a bit unsure about this, it looks too smart in some cases

we should juggle with the section or infer by hand...

Author: gares

HB/common/utils.elpi

@@ -367,6 +367,25 @@ re-enable-id-phant T T1 :-
   (pi f1 f2 t v\ copy {{lib:@hb.ignore_disabled lp:t lp:f1 lp:v lp:f2}} {{lib:@hb.ignore lp:t lp:v}} :- !) =>
   copy T T1.
 
+pred failsafe-structure-inference i:term, o:term.
+failsafe-structure-inference T T1 :-
+  (pi OP Args Args1\
+    copy (app [global (const OP)|Args]) (app [global (const OP)| Args1]) :-
+      exported-op _ _ OP, !, eta-structure-record OP Args Args1) =>
+  copy T T1.
+
+pred eta-structure-record i:constant, i:list term, o:list term.
+eta-structure-record OP L L1 :-
+  exported-op M _ OP, mixin-first-class M Class, factory-nparams Class NP,
+  std.split-at NP L Params [S|Rest],
+  var S,
+  class-def (class Class Structure _),
+  get-constructor Structure K,
+  std.map Params copy Params1,
+  std.map Rest copy Rest1,
+  coq.mk-app {coq.env.global K} {std.append Params1 [_,_]} EtaS,
+  std.append Params1 [EtaS|Rest1] L1.
+
 pred prod-last i:term, o:term.
 prod-last (prod N S X) Y :- !, @pi-decl N S x\ prod-last (X x) Y.
 prod-last X X :- !.

HB/structure.elpi

@@ -9,8 +9,11 @@ pred declare i:string, i:term, i:sort.
 pred declare i:string, i:term, i:universe.
 declare Module BSkel Sort :- std.do! [
   disable-id-phant BSkel BSkelNoId,
-  std.assert-ok! (coq.elaborate-skeleton BSkelNoId _ BNoId) "illtyped structure definition",
+  failsafe-structure-inference BSkelNoId BSkelNoIdX,
+  coq.say BSkelNoIdX,
+  std.assert-ok! (coq.elaborate-skeleton BSkelNoIdX _ BNoId) "illtyped structure definition",
   re-enable-id-phant BNoId B,
+  
   private.sigT->list-w-params B GRFSwP_or_ThingtoBeWrapped ClosureCheck,
 
   % do some work to go back to factories on a single subject

tests/monoid_enriched_cat.v

@@ -52,12 +52,17 @@ HB.mixin Record hom_isMon T of Quiver T :=
     { hom_isMon_private : forall A B, isMon (@hom T A B) }.
 
 
-Fail HB.structure
+Succeed HB.structure
   Definition Monoid_enriched_quiver :=
     { Obj of isQuiver Obj &
               (forall A B : Obj, isMon (hom A B)) }.
 
-(* which one is best? *)
+Succeed HB.structure
+  Definition Monoid_enriched_quiver :=
+    { Obj of (*isQuiver Obj & once we wrap we pull this in as a dep! *)
+              (forall A B : Obj, isMon (hom A B)) }.
+
+                          (* which one is best? *)
 Succeed HB.structure
   Definition Monoid_enriched_quiver :=
     { Obj of isQuiver Obj &