Overriding a polymorphic operator during cloning fails, claiming the body has
no type parameters.
MRE
theory Thy.
op mk (x : 'a) = (x, x).
end Thy.
clone Thy as Thy1.
clone Thy as Thy2 with
op mk <= Thy1.mk.
Result:
operator `mk' body contains 0 type parameter instead of 1
Reproduces on main with both op mk <= Thy1.mk and op mk = Thy1.mk.
Notes
This is orthogonal to datatypes (the MRE above uses none) and to #989. It
concerns how operator overrides carry the overridden operator's type
parameters. Surfaced while investigating #989 / PR #1045.
Overriding a polymorphic operator during cloning fails, claiming the body has
no type parameters.
MRE
Result:
Reproduces on
mainwith bothop mk <= Thy1.mkandop mk = Thy1.mk.Notes
This is orthogonal to datatypes (the MRE above uses none) and to #989. It
concerns how operator overrides carry the overridden operator's type
parameters. Surfaced while investigating #989 / PR #1045.