mixin-instance-type->mixin-src does not use the typing information

[Tragicus]

mixin-instance-type->mixin-src produces clauses mixin-src clauses that call the unification, without giving the type of the evars it creates. This can lead to a unification of the form S.sort ?a = ?b where S.sort is a primitive projection. However, then Rocq retypes S.sort ?a and since ?a has type ?A which is not an inductive type, it fails.
N.B. Using coq.typecheck feels a bit heavy to do this, when we just have to create the evar with the right type. Is there a better way to do this?

[CohenCyril]

@gares, @Tragicus minimized his first attempt with the following.
(@pi-decl N T x \ (foo x x :- !)) => foo X Y
This fails while (pi x \ (foo x x :- !)) => foo X Y succeeds... is that expected?

(I rebuilt the example from the top of my head without testing it, I hope that I'm not too wrong...)

[Tragicus]

The error in coq-8.19/mathcomp-ssreflect is reproducible by adding an HB.saturate in ssreflect/eqtype.v/l.777 and is the following. After doing

coq.typecheck X870 
    (app
        [global (const «cancel»), 
          app
             [global
                 (const «Equality.sort»), 
               X867], X866, X868, X869]) ok

doing

coq.typecheck X869 
     (prod `x` 
        (app
           [global
               (const «Equality.sort»), 
              X867]) c0 \ X866) ok

fails with an Ill-typed evar instance error. Do we have any idea what could be wrong?

[gares]

Can you invoke coq.sigma.print between the two calls?

[Tragicus]

Yes, I could do it, but X869 still has an evar as its type and I did not see anything wrong, so I am still a bit confused. Nevertheless, I do the typechecks in the wrong order. I assume there is a retyping somewhere that fails for a similar reason that it failed with unifications.