Stream: Coq users

Topic: Unset Printing Universe and new error


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yannick Zakowski (Dec 21 2021 at 09:31):

Ah great, thanks Gaëtan!

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC