Universe polymorphism edits

[lastland]

It seems that an edit that makes a definition polymorphic would be helpful. I know that Eric has already been working on this, and I am opening this issue to list a few use cases I found.

The most basic form would be something like set Foo.bar polymorphic where Foo.bar is the qualified name of a definition. The definition can be a record, a type class, a type class instance, a function, an inductive or a coinductive data type, a variant, or a lemma/theorem/axiom (I have found scenarios where I want to make a lemma polymorphic)...

Ideally, when the definition is an instance, we will also want to make all its class methods polymorphic (in Coq translations, they are separate definitions).

When the definition is an inductive or coinductive data type, a variant, or a record type, it would also be useful if a single edit can make it polymorphic and cumulative (maybe something like set Foo.bar polymorphic cumulative?)---the definition would not be cumulative by default otherwise (see: https://coq.inria.fr/refman/addendum/universe-polymorphism.html#cumulative-noncumulative).

In some scenarios, we may also want to use a single edit to make everything in a module universe polymorphic. And in those scenarios, we may also want edits that can make a few definitions monomorphic.

[antalsz]

Sounds like a good plan. I'd recommend polymorphic Mod.val and either cumulative Mod.val or polymorphic cumulative Mod.val to be consistent with the current set of edits. We'll probably need to add a new map from names to their polymorphism status, and then monitor that flag that when translating. (Are polymorphism and cumulativity independent? That probably affects the design.) This should be decently straightforward to add, although it will necessitate modifying the Coq AST to include the Polymorphic and Cumulative tags. I need to focus on my dissertation instead of implementing this, though.

[antalsz]

Actually, another thought: should we always enable universe polymorphism and/or cumulativity? What would be the ramifications of that? (With Universe Polymorphism. and/or Set Polymorphic Inductive Cumulativity.)

[lastland]

Actually, another thought: should we always enable universe polymorphism and/or cumulativity? What would be the ramifications of that?

That is a good question. I have been trying to modify base to make it more polymorphic to see what would happen. At this moment, it seems to me that making everything polymorphic does not work very well (or at least requires more manual intervention), but I have not fully understood why yet. In particular, I am now running into a problem with a Program Fixpoint with a measure. The proof obligations can be solved via lia but Qed fails because Coq somehow runs into a branch that asserts False. :(

[lastland]

Sounds like a good plan. I'd recommend polymorphic Mod.val and either cumulative Mod.val or polymorphic cumulative Mod.val to be consistent with the current set of edits. We'll probably need to add a new map from names to their polymorphism status, and then monitor that flag that when translating. (Are polymorphism and cumulativity independent? That probably affects the design.) This should be decently straightforward to add, although it will necessitate modifying the Coq AST to include the Polymorphic and Cumulative tags.

Good suggestions! Thanks!

[lastland]

In some scenarios, we may also want to use a single edit to make everything in a module universe polymorphic. And in those scenarios, we may also want edits that can make a few definitions monomorphic.

BTW, the first use case can now be simulated by adding Set Universe Polymorphism in a preamble, but edits should look better and we still need the monomorphic flag.

[antalsz]

Ah, good point about the preamble. We could also switch to default polymorphic/edits for monomorphism, but it seems like there's no reason to do that – polymorphism seems to be less necessary.

[lastland]

At this moment, it seems to me that making everything polymorphic does not work very well (or at least requires more manual intervention), but I have not fully understood why yet.

And my plan is to try to understand this part better :)

[lastland]

I have just found another term called "template universe polymorphic". It happened when you define something with explicit universe levels but without the keyword "Polymorphic" in front of the definition. This might also be something we want. In this case, it looks like the edits of declaring something to be polymorphic and the edits of annotating universe levels should be separate edits that can be used together.

I have not found much information about "template universe polymorphic", except for this documentation: https://github.com/coq/coq/blob/master/dev/doc/universes.md
(The term is not in Coq doc. And I do not recall seeing it in their paper 😞 )