The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature