The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

It's a consequence of a minimization heuristic. See 
https://coq.inria.fr/refman/Reference-Manual032.html#sec807

You can do [Unset Universe Minimization ToSet] as the link says or you 
can make the universe explicit so that it won't be unified with Set.

Gaëtan Gilbert

On 14/07/2017 13:16, Dominik Kirst wrote:
> Hello,
>
> the following code produces some unexpected behaviour:
>
> ——
>
> Set Universe Polymorphism.
> Set Printing Universes.
>
> Inductive Tree : Type :=
> | sup : forall X : Type, (X -> Tree) -> Tree.
>
> Definition pair s t :=
>    @sup bool (fun b => if b then s else t).
>
> About pair.
>
> "pair@{} : Tree@{Set} -> Tree@{Set} -> Tree@{Set}"
>
> ——
>
> Although the function “pair" is inferred to be universe-polymorphic, the 
> input trees and return trees are restricted to Set. This should not be the case 
> since the operation is valid for all universe levels. In fact, other operations 
> such as union and power (that do not refer to explicit types like bool in their 
> definitions) are typed correctly. Is that intended or a bug?
>
> Thanks for your help,
> Dominik Kirst