The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

On 16 Nov 2022, at 22:06, Helmut Brandl <helmut.brandl AT gmx.net> wrote:

On 16 Nov 2022, at 21:23, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

I.e. the argument type of a function type can live in a higher universe than the result type.

Yes, but "lst" is an _inhabitant_ of the function type, it's not the function type itself.

Similarly "(fun A:Type@{u+1} => A) : Type@{u+1} -> Type@{u}" is rejected

In that case the rejection is clear to me. The term ‘A’ has type ’Type@{u+1}’. Therefore the function returns a result of type ’Type@{u+1}’ and not ’Type@{u}’ as required by the type annotation. I.e. the function on the left hand side of the colon is not an inhabitant of the type on the right hand side of the colon. The compiler must reject it.

Are you saying that the type ’Type@{u+1} -> Type@{u}’ is not allowed to be inhabited? Is there such a typing rule? If there is such a typing rule, I would like to understand why it is there. Does the violation of such a typing rule create any inconsistencies like an inhabitant of the type ‘forall A: Type, A’?

According to coq the type ’Type@{u+1} -> Type@{u}’ can have inhabitants. E.g. the following is accepted by coq:

Check (fun A: Type@{u+1} => nat): Type@{u+1} -> Type@{u}.

However my construction of the inductive type ‘lst’ which is an inhabitant of exactly that type is rejected. Why is it possible to construct a function of that type but not an inductive definition?

— Helmut

On 16/11/2022 21:02, Helmut Brandl wrote:

I’d like to understand universes and universe polymorphism better. Therefore I have some questions:
The following term is well typed in coq:
  Universe u.
  Check forall A:Type@{u+1}, Type@{u}.
I.e. the argument type of a function type can live in a higher universe than the result type. If I try the same with an inductive type, I get an error.
  Inductive lst (A: Type@{u+1}): Type@{u} :=
  | nil: lst A
  | cons: A -> lst A -> lst A.
  *Error:*Universe inconsistency. Cannot enforce u = max(Set, u+1).
What is the theoretical background of this consistency error. The type of ‘lst’ is exactly the type I have checked above as well typed. I suspect that if it were well typed, then I could ‘hide’ an object from the universe ‘u+1’ in the list which resides in the universe ‘u’. Can anybody help to give a more precise explanation.
Regards
Helmut