#[infer(var = "R", from ="Type")]

[gares]

• after (R : ringType) take a (ph : phant R) in the mixin
• at structure definition, ph are not abstrcted but rather specialized in both the structure type /abbreviation and the operations:
  • Foo.type R := Foo.type_ R (Phant R)
  • Foo.op R x y := ... (Phant R) ...

[pi8027]

IIUC, subtyping functions should preserve phantom arguments and displays. For example, in the master branch of MathComp:

GRing.Algebra.lalgType
     : forall (R : ringType) (phR : phant R), GRing.Algebra.type (R:=R) phR -> GRing.Lalgebra.type (R:=R) phR

Order.Total.porderType
     : forall disp : unit, orderType disp -> porderType disp

In MathComp, these arguments appear only in the argument of structure records, and do not appear in mixins and classes. Displays should not actually appear in mixins and classes. I think we need some special treatments for these points.

[gares]

OK, I'll try something