Polymorphic extensions

[cqc-alec]

"Polymorphic" is a scary word and I'm not sure if it's the right one. But I want to be able to define, in one place, a family of extensions (parametrized, say, by a natural number $k$). Any given $k$ gives me a fixed set of operations and types.

Currently, as far as I can see the only way is to define a single extension whose operations and types are polymorphic in $k$. But then there is nothing to stop people from mixing operations with different $k$, which shouldn't be allowed.

Use case: defining an extension to capture the logical operations of the iceberg $[[k+2, k, 2]]$ code.

[ss2165]

to express k+2 you need dependent types too... (see Quantinuum/guppylang#785)