The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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 ?

We have similar problems in HoTT/HoTT.  We have one definition with upwards of 2000 universe variables, and this seems to be a primary cause of performance problems in this file.

I should note that there are occasional cases where removing the universe variables is the wrong behavior, at least when the body is transparent (corresponding, say, to when the variables are explicitly names in the body).  See, for example, some definitions we use to add universe constraints.  These are also essential in being able to specify module type interfaces with universe parameters that appear in a transparent body and are relevant, but don't appear in the type.  (It's possible that these are to be considered hacks, and that a better replacement should be found.)

 

On Sun Nov 30 2014 at 1:56:24 PM Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 30/11/2014 15:08, jlottes AT gmail.com wrote:
> 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?

I somehow remember having spoken about this precise point with Matthieu,
but I can't remember the result of the discussion...

But well, I agree that your proposition seems sensible!

PMP