#[primitive_class] makes HB.structure diverging

[pi8027]

Here is a minimal example, but I couldn't identify the reason:

From HB Require Import structures.

HB.mixin Record M A := {}.
#[primitive_class] HB.structure Definition S := { A of M A }.

[gares]

See also #248

[gares]

I did not report it upstream. If you have the time, use #[log] to report a HB independent bug.

[gares]

Maybe it's not the same bug. The other one seems Coq related, this one may be in Coq-Elpi

[pi8027]

I agree that these two are not the same bug.

[gares]

It's a loop in my code doing whd

rid:0 step:5029 gid:5514 user:curgoal = whd
(global (const «fix_loop_M_mixin»)) 
[app
  [global (const «eta»), 
   sort (typ «fix_loop.48»), 
   app
    [global (const «sort»), 
     global (const «A»)]], 
 global
  (const «HB_unnamed_factory_2»)] 
(global (indc _)) X24 


rid:0 step:5044 gid:5529 user:curgoal = whd
(global (const «fix_loop_M_mixin»)) 
[app
  [global (const «eta»), 
   sort (typ «fix_loop.48»), 
   app
    [global (const «sort»), 
     global (const «A»)]], 
 global
  (const «HB_unnamed_factory_2»)] 
(global (indc _)) X24 

[gares]

I found the culprit, I'll fix it but it will take a day or two.

The problem is that I translate to elpi in the same way both the primitive projection and the "compatibility constant". The latter mentions the former, so I build a "cyclic term". I will reuse the primitive term constructor I already have for primitive integers and floats to represent primitive projections.

[pi8027]

I don't see this issue anymore, although now I have another issue with #[primitive] or #[primitive_class]. Shall we close it?