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`

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?

this is cumulativity not coercion

the rules are at https://coq.github.io/doc/master/refman/language/cic.html#subtyping-rules

Last updated: Jun 18 2024 at 09:02 UTC