clone: op override (<= / =) drops the type parameters of a polymorphic operator

[strub]

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.

[oskgo]

There's also #1006 (comment), which might be related but uses <-.

op gen ['a,'b]: bool = true.

theory T.
op f = gen<:unit,'a>.
end T.

op g = gen<:'a,unit>.

clone T as T' with
op f <- g.

[oskgo]

Both cases are fixed by providing a parameter for the operator we instantiate with, even if it is abstract (op mk <= Thy1.mk<:'a> and op f <- g<:'a>)