Stream: Coq users

Topic: Difference between Set and Type


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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))?

view this post on Zulip Julin S (Jan 08 2022 at 15:40):

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

view this post on Zulip Li-yao (Jan 08 2022 at 15:43):

Set Printing All

view this post on Zulip 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

view this post on Zulip 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 ...

view this post on Zulip 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.

view this post on Zulip Julin S (Jan 10 2022 at 04:26):

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

view this post on Zulip Paolo Giarrusso (Jan 10 2022 at 10:04):

Intuitively, yes, but <= can be more restrictive

view this post on Zulip Paolo Giarrusso (Jan 10 2022 at 10:05):

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

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC