#[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]

hierarchy-builder/HB/structure.elpi

Lines 201 to 237 in 7d4f095

	% const Po : forall p1 .. pm T m1 .. mn, Extra (Eg Extra = forall x y, x + y = y + z)
	% const C : forall p1 .. pm s, Extra
	% Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs
	pred clean-op-ty i:list prop, i:term, i:term, o:term.
	clean-op-ty [] _ T1 T2 :- copy T1 T2.
	clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
	gref-deps (const Po) MLwP,
	w-params.nparams MLwP NParams,
	std.length {list-w-params_list MLwP} NMixins,
	(pi L L1 L2 Params Rest PoArgs\
	copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
	std.split-at NParams L Params [_|Rest],
	std.drop NMixins Rest PoArgs,
	std.append Params [S|PoArgs] L1,
	std.map L1 copy L2) =>
	clean-op-ty Ops S T1 T2.
	pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
	i:list term, i:term, i:w-args A, o:pair term term.
	operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ ParamsOp _) (pr Bo Ty) :- std.do! [
	mk-app (global Struct) Params StructType,
	mk-app Psort Params PsortP,
	mk-app Pclass Params PclassP,
	Bo = fun `s` StructType Body,
	Ty = prod `s` StructType BodyTy,
	(@pi-decl `s` StructType s\ sigma Carrier Class\ std.do! [
	mk-app PsortP [s] Carrier,
	mk-app PclassP [s] Class,
	synthesis.under-mixin-src-from-factory.do! Carrier Class [
	% just in case..
	synthesis.infer-all-gref-deps ParamsOp Carrier (const Poperation) (Body s),
	std.assert-ok! (coq.typecheck (Body s) (DirtyTy s)) "export-1-operation: Body illtyped",
	clean-op-ty EXI s (DirtyTy s) (BodyTy s),
	],
	]),
	].

[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.

[proux01]

We should probably merge #423 that fixes it?