The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

It does seem to be related to nil but also to the return type of the 
match. Below are some tests. N (n) stands for explicit (implicit) nil 
argument. M (m) stands for explicit (implicit) return type. Only the 
fully implicit version seems to introduce the new universe which does 
not appear anywhere in the term. Is this related to matches using 
functions internally?

Janno


From Coq Require List.
Set Printing Universes.
Set Printing All.
Definition tl_NM (A : Type) (l : list A) :=
match l return list A with
| nil => @nil A
| cons _ m => m
end.
Print tl_NM.

Definition tl_Nm (A : Type) (l : list A) :=
match l with
| nil => @nil A
| cons _ m => m
end.
Print tl_Nm.

Definition tl_nM (A : Type) (l : list A) :=
match l return list A with
| nil => @nil _
| cons _ m => m
end.
Print tl_nM.

Definition tl_nm (A : Type) (l : list A) :=
match l with
| nil => @nil _
| cons _ m => m
end.
Print tl_nm.


On 09/06/2017 07:49 AM, Guillaume Melquiond wrote:
> On 06/09/2017 01:14, Jan-Oliver Kaiser wrote:
> > Hey everyone,
> >
> > List.tl and List.repeat are outliers in the List module as they
> > introduce new universes which upper-bound list's own universe variable
> > in the global graph. Why is that?
>
> Good catch. They are created because of the implicit argument of nil,
> which is of type Type. I have no idea whether this deficiency of Coq is
> easily fixed, but we can at least remove these superfluous universes by
> explicit setting the argument of nil in the definitions of tl and repeat.
>
> Best regards,
>
> Guillaume