The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> 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?

That specific inductive is not allowed.

The rules for inductives 
https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions
basically every argument of a constructor must be at a smaller or equal 
universe to the output universe of the inductive. The first argument of cons 
fails this.

Gaëtan Gilbert

On 16/11/2022 22:32, Helmut Brandl wrote:
> > On 16 Nov 2022, at 22:06, Helmut Brandl <helmut.brandl AT gmx.net 
> > <mailto:helmut.brandl AT gmx.net>> wrote:
> >
> >
> >
> > > On 16 Nov 2022, at 21:23, Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net 
> > > <mailto: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