Stop implicitly adding template inductive types to Keep Equality table. #17718
Conversation
coqbot-app
bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
🔴 CI failure at commit 8b9a9d1 without any failure in the test-suite ✔️ Corresponding job for the base commit 037233d succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
no-template-keep-inj-equality
branch
from
8b9a9d1
to
e38d637
Compare
coqbot-app
bot
removed
the
request: full CI
| @@ -3,8 +3,12 @@ | |||
|
|
|||
| (* This is also #4560 and #6273 *) | |||
|
|
|||
| #[universes(template)] | |||
| #[warnings="-no-template-universe"] | |||
| Inductive foo := foo_1. | |||
There was a problem hiding this comment.
This is exactly the one reason why the process leading to this PR was really tricky. Basically, it is possible to have a template-poly inductive type that has no bound template poly universe. The urexample is a unit type without an explicit sort annotation (like above, and like the phantom type pattern). This flag is totally useless except for the behaviour of injection / discriminate and the like.
The warning fires as soon as the inductive has no template universes, but here we care about the inductive being effectively template, hence the attribute belly dance.
There was a problem hiding this comment.
This flag is totally useless except for the behaviour of injection / discriminate and the like.
I thought that was only until this PR? After it does it still matter for this test?
There was a problem hiding this comment.
We could indeed remove it, but I think it's also a good idea to have a place to test that there is no regression for weird template corner-cases.
|
@coqbot merge now |
The reason why the flag was introduced was precisely to be able to desynchronize the template status from the equality keeping behaviour. Since the Keep Equality flag has been around since 8.15 it is now time to perform this change.