Automated class inference fault when using `Trocq Use`

[ecranceMERCE]

While writing an example file for Trocq, I got a bug after adding the following lemma to Trocq, relating the length function of lists to itself, so that transfer is possible with goals containing it:

Definition lengthR :
  forall (A A' : Type) (AR : A -> A' -> Type)
         (l : list A) (l' : list A') (lR : listR A A' AR l l'),
    natR (length l) (length l').

As length is not a type former, Trocq will translate it at level $(0,0)$, which does not require more between A and A' than the raw relation, i.e., class $(0,0)$ as well.

However, here is what Trocq prints when accumulating the entry into the Elpi database:

accumulating const «length» @ pc map0 map0 ( [] ) ~ const «length» :. const «lengthR»

The class $(0,0)$ of AR is not properly detected because it is not formatted as ParamXY.Rel A A'. The required type for this lemma is the following:

Definition lengthR :
  forall (A A' : Type) (AR : Param00.Rel A A')
         (l : list A) (l' : list A') (lR : listR A A' AR l l'),
    natR (length l) (length l').

Note that leaving listR with the following type is fine:

listR : forall (A A' : Type) (AR : A -> A' -> Type), list A -> list A' -> Type

It looks like the tool is strict only on relations between values in Type. For any class different from $(0,0)$, anyway we would write it as ParamXY.Rel A A', but for $(0,0)$ it might be less natural.

I do not really know whether it qualifies as a bug, but it might introduce misunderstandings or silent bugs in the user's development when using Trocq. I think it requires either an exception for $(0,0)$ on occurrences of Type, or a line of documentation to make the expected syntax more explicit.