Skip to content

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

@strub

Description

@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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions