HB.instance: read the factory from the type rather than the body

hb.elpi

@@ -1075,13 +1075,13 @@ main-mixin-requires Str GR GRFS [From|PO] SN :- !, std.do! [
 % corresponding to parameters in arity A. TS is T applied
 % to all section variables (and hd-beta reduced). Acc should
 % be [] at call site.
-pred postulate-arity i:arity, i:list term, i:term, o:term.
-postulate-arity (parameter ID _ S A) Acc T T1 :-
+pred postulate-arity i:arity, i:list term, i:term, o:term, o:term.
+postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
   if-verbose (coq.say "HB: postulating" ID),
   @local! => coq.env.add-const ID _ S @opaque! C,
   Var = global (const C),
-  postulate-arity (A Var) [Var|Acc] T T1.
-postulate-arity (arity _) ArgsRev X T :-
+  postulate-arity (A Var) [Var|Acc] T T1 Ty.
+postulate-arity (arity Ty) ArgsRev X T Ty :-
   hd-beta X {std.rev ArgsRev} X1 Stack1,
   unwind X1 Stack1 T.
 

structures.v

@@ -305,7 +305,7 @@ main [const-decl Name (some BodySkel) TyWPSkel] :- !, 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",
-  if (TyWP = arity _) (
+  if (TyWP = arity SectionTy) (
      % Do not open a section when it is not necessary (no parameters)
      % A side effect of opening a section is loosing meta data associated
      % with instances, in particular builder tags are lost
@@ -315,11 +315,12 @@ main [const-decl Name (some BodySkel) TyWPSkel] :- !, std.do! [
     with-attributes (if-verbose (coq.say  "opening instance section" TyWP)),
     SectionName is "hb_instance_" ^ {term_to_string {new_int} },
     coq.env.begin-section SectionName,
-    postulate-arity TyWP [] Body SectionBody
+    postulate-arity TyWP [] Body SectionBody SectionTy
   ),
 
-  std.assert! (coq.safe-dest-app SectionBody (global (const Builder)) Args) "Not an application of a builder, use a section if you have parameters",
-  std.assert! (factory-builder-nparams Builder NParams) "Not a factory builder synthesized by HB",
+  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
+  factory-alias->gref FactoryAlias Factory,
+  std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",
   coq.env.add-const Name SectionBody _ @transparent! C,
   std.appendR {coq.mk-n-holes NParams} [T|_] Args,
   with-attributes (main-declare-canonical-instances T (global (const C))),