Yannick Zakowski (Dec 21 2021 at 09:05): Yannick Zakowski (Dec 21 2021 at 09:05):Hello,
I have some Universe Inconsistencies showing up when importing files from two libraries (itrees and RelationalAlgebra fwiw).
Because Holiday time is no time to deal with this hell, I innocently decided to postpone the pain of figuring out a solution by setting Unset Universe Checking.
However when I do so, the following definition that usually goes through now fails:
Variant foo : Type -> Type :=
| Foo : unit -> foo unit.
With the error Error: Ill-formed template inductive declaration: not polymorphic on any universe. (on 8.14.1)
Is that expected? Is there a way to beg Coq to really forget about the Universes and let me keep going by any chance?
Gaëtan Gilbert (Dec 21 2021 at 09:23):Unset Auto Template Polymorphism.
template poly is useless if you're in unset univ checking mode so it should be fine
Yannick Zakowski (Dec 21 2021 at 09:31):Ah great, thanks Gaëtan!
Gaëtan Gilbert (Dec 21 2021 at 10:08):looks like the kernel gets a different result than predicted by the higher layers because Evd.set_eq_sort (called from ComInductive.inductive_levels) does nothing when unset univ checking
Last updated: Oct 13 2024 at 01:02 UTC