The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Indeed, that's how it works: the "template" part is about instantiating the type of the template polymorphic inductive so that its conclusion depends on the levels of the actual parameters, and can hence get lower than the original declared universe. However the constraints are not touched at all and we hence must add constraints between the actual parameters and the declared ones in case the constructors introduce constraints on them. What you describe is what the "full" universe polymorphism mechanism does, instantiating the constraints. Example why it is necessary:

Set Printing Universes.

Polymorphic Definition lt@{i j} := let X := Type@{i} : Type@{j} in unit.

Universe k.

Inductive foo@{l} (A : Type@{l}) : Type :=

| bar (B : lt@{l k}) : A -> foo A.

Print foo.

(* Inductive foo (A : Type@{l}) : Type@{max(Set, l)} :=  bar : lt@{l k} -> A -> foo A

  (* l |= l < k *)  *)

Variables B : Type@{k}.

Fail Definition baz' := foo B.

The term "B" has type "Type@{k}" while it is expected to have type "Type@{Top.75}"

(universe inconsistency: Cannot enforce k <= Top.75 because Top.75 < k).

(* Top.75 is l *)

Hope this helps,

-- Matthieu

On Wed, Sep 6, 2017 at 11:20 AM Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org> wrote:

Ok, I see that.

But then my question is : why is this even called "polymorphism"?

Perhaps, what I am asking for is some sort of explanation of what is
template universe polymorphism, actually.

--
JH

Le 06/09/2017 à 10:51, Guillaume Melquiond a écrit :
> On 06/09/2017 10:42, Jacques-Henri Jourdan wrote:
>> My naive understanding is that it would create a fresh (set of) universe
>> variable, and copy all the edges of the existing universe variable of
>> the list inductive type. But there should not be any direct constraint
>> between the fresh universe to the one of the original list definition.
> I don't think it has ever worked that way. (That said, I never
> understood why it was called "template", so maybe it was meant to work
> that way). For instance, if you type
>
>   Check (fun T : Type => list T).
>
> you get a constraint between the Type type here and the one from the
> definition of list:
>
>   Top.1 |= Top.1 <= Coq.Init.Datatypes.44
>
> Best regards,
>
> Guillaume