Stream: Coq users

Topic: Difference between Set and Type

Julin S (Jan 08 2022 at 15:32):

Isn't a value of type Set also a value of type Type?

I did

Check nat : Set.
Check nat : Type.

and it ran without errors.

But doing

Require Import List.
Import ListNotations.

Check [nat; bool]%list : list Set. (* ✓ *)


Check [nat; bool]%list : list Type. (* ✗ *)
(*
The term "[nat; bool]" has type "list Set" while it is expected to have type
 "list Type" (universe inconsistency: Cannot enforce Set = tst.2).
*)

Why is the error happening in the last line?

Gaëtan Gilbert (Jan 08 2022 at 15:34):

a value of type list Set is not a value of type list Type
[nat; bool] becomes the kernel term @cons Set nat (@cons Set bool (@nil Set)) which has type list Set

Julin S (Jan 08 2022 at 15:37):

So Set being Set : Type won't reach down to @cons Set nat (@cons Set bool (@nil Set)) being something like a 'subset' of @cons Type nat (@cons Type bool (@nil Type))?

Julin S (Jan 08 2022 at 15:40):

Is there a flag to show implicit args as well while printing terms in coq?

Li-yao (Jan 08 2022 at 15:43):

Set Printing All

Gaëtan Gilbert (Jan 08 2022 at 15:44):

it's not Set : Type that's important, it's Set <= Type
cons Set ... produces a list Set, but list Set isn't <= list Type

Gaëtan Gilbert (Jan 08 2022 at 15:46):

consider also

Arguments cons {_} & _ _.

Check [nat; bool]%list : list Type.

the & is a bidi hint https://coq.github.io/doc/master/refman/language/extensions/arguments-command.html#bidirectionality-hints which makes it infer @cons Type ...

Julin S (Jan 08 2022 at 17:58):

I wasn't sure about the <= but it's mentioned at http://adam.chlipala.net/cpdt/html/Universes.html
So am reading that.

Julin S (Jan 10 2022 at 04:26):

Oh does Set <= Type mean something like Set ⊆ Type?

Paolo Giarrusso (Jan 10 2022 at 10:04):

Intuitively, yes, but <= can be more restrictive

Paolo Giarrusso (Jan 10 2022 at 10:05):

as in the example above where not (list Set <= list Type)

Gaëtan Gilbert (Jan 10 2022 at 10:07):

Julin S said:

Oh does Set <= Type mean something like Set ⊆ Type?

that's what it means
it doesn't go through application

Meven Lennon-Bertrand (Jan 10 2022 at 13:36):

An alternative solution to the bidi hint of Gaëtan is to annotate your terms with types to help the elaboration:

Check [nat : Type; bool : Type] : list Type.

That way the annotation forces both nat and bool to be coerced to Type (which is possible), and so you do not run into the issue of coercing from list Set to list Type (which is not possible).

Last updated: Oct 01 2023 at 18:01 UTC