`#[primitive] HB.mixin` breaks the types of constants lifting mixin projections

[pi8027]

Example:

From Coq Require Import ssreflect ssrfun.
From HB Require Import structures.

#[primitive]
HB.mixin Record AddMonoid_of_TYPE S := {
  zero : S;
  add : S -> S -> S;
  addrA : associative add;
  add0r : left_id zero add;
  addr0 : right_id zero add;
}.

HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.

Check addrA.
(*
addrA
     : associative (AddMonoid_of_TYPE.add _ (AddMonoid.class ?s))
where
?s : [ |- AddMonoid.type]
*)

The type of addrA should be associative add.

[gares]

Iirc there is a piece of code cleaning up the type. I guess it is broken if the primitive term constructors shows up

[pi8027]

@gares Can you point out the part of the code declaring these constants and synthesizing their types? I have a rough idea of how to fix the issue.

[gares]

clean-op-ty in structure.elpi is what I suspect messes up things.

[gares]

https://github.com/math-comp/hierarchy-builder/blob/7d4f0958c37d6c006569892c742d7c7bb70279e1/HB/structure.elpi#L201-L237

[pi8027]

Thanks. I believe that constructing the types of these constants from the declaration of the record type is much easier than doing so from the types of the projections. While the latter requires some replacements using copy (as we can see in clean-op-ty), the former should be just a matter of substitution.

[pi8027]

I will take a closer look when I have some time.