The Coq mailing list

[Dominik Kirst <kirst AT ps.uni-saarland.de>]

Great, that did work, thank you!

Dominik




> On 17. Jul 2017, at 11:12, Gaetan Gilbert 
> <gaetan.gilbert AT ens-lyon.fr>
>  wrote:
> 
> 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
>