Lef Ioannidis (Feb 10 2022 at 17:44): Lef Ioannidis (Feb 10 2022 at 17:44):Why can I coerce Set to Type but not list Set to list Type, I thought list was covariant. Am I misunderstanding how universe polymorphism works?
Definition bar : Type := nat.
Fail Definition foo: list Type := [nat; nat].
On the other hand, this works so perhaps this is just a syntactic quirk or some global setting I can use to enable this coercion
Definition foo': list Type := [nat: Type; nat: Type].
Set and Type are arguments, not universe arguments, so univ poly is irrelevant
[nat] is elaborated to @cons Set nat (@nil Set) which is a list Set
[nat : Type] is elaborated to @cons Type nat (@nil Type) which is a list Type
Lef Ioannidis (Feb 10 2022 at 17:51):Right, I guess my question is; what are the coercion rules? Obviously a coercion happens in bar and foo' but not in foo. I assumed it is standard covariance rules but maybe I am wrong?
Gaëtan Gilbert (Feb 10 2022 at 17:51):this is cumulativity not coercion
Gaëtan Gilbert (Feb 10 2022 at 17:55):the rules are at https://coq.github.io/doc/master/refman/language/cic.html#subtyping-rules
Gaëtan Gilbert (Feb 10 2022 at 17:58):Last updated: Sep 23 2023 at 08:01 UTC