The Coq mailing list

[<jlottes AT gmail.com>]

When defining a polymorphic constant, if any universe variables are used in
the definition but do not appear in the type, they will nevertheless become
part of the list of universe parameters for the constant. In this sense,
universe-polymorphic constants are a "leaky" abstraction. I found this
behavior rather counter-intuitive when I first encountered it as I began
trying out universe polymorphism.

A particularly troublesome case of the above is when the constant being
defined is an opaque lemma (let's say, living or mapping to Prop). A "proof-
irrelevant" spirit (any term/tactic that gets the QED is as good as any other)
becomes rather problematic. One needs to be careful about the tactics used, as
they may introduce universe variables that become part of the lemma's
signature. The effect is perniciously cumulative; as future proofs that make
use of this lemma may end up using multiple copies of any of these extra
universe variables.

This creates a tension between using "elegant" but very abstract proof devices
on the one hand, and preferring "clean" direct proofs that do not "pollute"
the lemma's signature with extra universe variables on the other, in order to
avoid ever-growing lists of universe variables.

Now for my question: from what I've managed to grok from the relevant papers
(by Sozeau/Tabareau and Herbelin), it seems to me that it should, in
principle, be possible to remove any universe parameters from an opaque
constant that (1) do not appear in the type of the constant, and (2) have no
upper bound. Doing so may cause other universe parameters to no longer have an
upper bound, and the process could be repeated. In the meta-theory, I think
this should be sound since there is no chance these variables could ever
become bounded from above. After all, the type checker should never encounter
them, as they are not in the type, and opaque terms are not unfolded. It is
also my impression that this could be done fairly simply in the code, without
needing major implementation changes. Am I correct about the metatheory? About
the implementation? Or have I missed something? Perhaps something subtle about
what being "opaque" means?

This change could very well eliminate my problems of growing universe variable
lists completely, as the universes needed by abstract proof techniques all
tend to fall in the above category (no upper bound).

It would be nice to have a general approach to this problem (could the
metatheory be extended to support an "existential" type former for universes?
what would that look like?), although I can see that it is not easy.

Are other people running into these issues? Or is everyone else who is using
universe polymorphism doing HoTT and only interested in carefully constructed,
relevant, Type-sorted "proofs" in which perhaps these problems don't arise ?

In case the tone of this message came across as too critical, let me make it
clear that I am a big fan of the universe polymorphism feature, in general.