Why can I coerce
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
[nat : Type] is elaborated to
@cons Type nat (@nil Type) which is a
Right, I guess my question is; what are the coercion rules? Obviously a coercion happens in
foo' but not in
foo. I assumed it is standard covariance rules but maybe I am wrong?
this is cumulativity not coercion
the rules are at https://coq.github.io/doc/master/refman/language/cic.html#subtyping-rules
see also https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Difference.20between.20Set.20and.20Type
Last updated: Jan 28 2023 at 07:30 UTC