Joshua Grosso (Feb 08 2021 at 18:51): Joshua Grosso (Feb 08 2021 at 18:51):Set Auto Template Polymorphism.
Inductive foo (X : Type) : Type :=
| bar : X -> foo X.
Definition baz : Set := foo nat.
works, but
Set Auto Template Polymorphism.
Section foo.
Variable X : Type.
Inductive foo : Type :=
| bar : X -> foo.
End foo.
Definition baz : Set := foo nat.
gives a universe inconsistency error. (I've fiddled around with things, and it seems like defining X as a Section-local Variable is what introduces the error in the second example.) Is there any way around this (other than not using Section-local Variables)?
Pierre-Marie Pédrot (Feb 08 2021 at 18:52):No, it is a voluntary limitation.
Pierre-Marie Pédrot (Feb 08 2021 at 18:53):It was changed not so long ago to fix a soundness issue of sections + template poly
Joshua Grosso (Feb 08 2021 at 19:05):Hmm, https://github.com/coq/coq/issues/11039 seems to me to imply that universe polymorphism is the preferred approach to template polymorphism anyway—but the docs list it as experimental, so should I avoid using e.g. Set Universe Polymorphism. in modern code?
Joshua Grosso (Feb 08 2021 at 19:06):(or does "experimental" only mean e.g. "unergonomic" rather than "potentially inconsistent")
Théo Zimmermann (Feb 08 2021 at 20:53):"experimental" actually means that it was added as an experimental feature a long time ago and the warning was never removed from the documentation
Théo Zimmermann (Feb 08 2021 at 20:53):But there isn't really any proper definition of what experimental features are in the case of Coq.
Théo Zimmermann (Feb 08 2021 at 20:54):Furthermore, every universe expert will tell you that full universe polymorphism is actually better understood than what is currently implemented and known as template polymorphism in Coq.
Matthieu Sozeau (Feb 11 2021 at 19:24):Rather the former :) The ergonomy is ongoing work as Théo mentions. If you want polymorphism just for parameters in Type@{} (and not Prop) then I would suggest making just this inductive polymorphic (and cumulative, to get a similar effect to template polymorphism)
Joshua Grosso (Feb 11 2021 at 19:44):@Matthieu Sozeau Thanks! Just to make sure I understand: at this point, it's probably better to add#[universes(polymorphic, cumulative)] to the datatype(s) in question rather than to Set Universe Polymorphism globally?
Matthieu Sozeau (Feb 11 2021 at 19:45):Yes. That way you shouldn't get into the trouble of having definitions with many universe binders you certainly have no use of
Matthieu Sozeau (Feb 11 2021 at 19:45):May I ask what kind of inductive you are declaring?
Joshua Grosso (Feb 12 2021 at 04:55):Just a basic (in)finite sequence, inside a Section.
Section seq.
Variable X : Type.
Inductive seq : Type :=
| seq_infinite : (nat -> X) -> seq
| seq_finite : list X -> seq.
(* ... *)
End seq.
when I tried to use it (specifically, from another module) with an argument in Set, it didn't specialize to Set as I had expected.
Joshua Grosso (Feb 12 2021 at 04:59):also I see your point—I just ran into a non-obvious universe binder issue because I I had forgotten to enable universe polymorphism somewhere else :-P
Last updated: Apr 20 2024 at 06:02 UTC