HB.instance Definition f Params := ... (outside a section)

[gares]

As of today we can only write

Section Foo.
Variable A : Type.
HB.instance Definition list_m1 := m1.Build (option A) (list nat) (cons 7 nil) None.
End Foo.

If we abstract list_m1 over A we get an assertion in

pred mixin-srcs i:term, i:term, o:list prop.
mixin-srcs T X MSL :- std.do! [
  std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
  if (not (safe-dest-app XTy (global _) _))
     (coq.error "Term:\n" {coq.term->string X}
                "\nhas type:\n" {coq.term->string XTy}
                "\nwhich is not a record")

Instead we should record the abstractions before the record and put them in front of S

pred declare-instances i:term, i:list class.
declare-instances T [class Class Struct MLwP|Rest] :-
  params->holes MLwP Params,
  get-class-constructor Class Params KC,
  list-w-params_list MLwP ML,
  mterm->term (mterm [/*Params already applied to KC*/] T ML KC) KCApp, % we can build it
  not (local-cs? T Struct), % not already built
  !,
  term->gref T TGR,
  coq.gref->id TGR TID,
  Name is TID ^ "_is_a_" ^ {term->modname Struct},

  if-verbose (coq.say "HB: declare canonical instance" Name),

  get-structure-constructor Struct Params KS,
  S = app[KS, T, KCApp],

[gares]

This affects HB in both branches master and parameters