The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I guess you are right. I checked again and for [ x : X ] , [ X : UU1 ]  and 
the value of [ test1 x ] is [ X ] but [ X ] moved into the universe [ UU3 ] .

It is weird because it means that from the point of view of Coq there are 
*two different* types with the name [ X ] one in [ UU1 ] and another one in [ 
UU3 ] .  A function [ F : UU1 -> UU1 ] can be applied to the first one but 
not to the second .

Vladimir. 



 On Jun 30, 2011, at 7:11 PM, Matthieu Sozeau wrote:

> 
> Le 30 juin 2011 à 13:18, Vladimir Voevodsky a écrit :
> 
>> Consider the following code:
>> 
>> Definition UU1 := Type .
>> Definition UU2 := Type .
>> Definition UU3 := Type .
>> 
>> (* The following two lines establish that UU1 : UU2 *)
>> 
>> Variable F : UU2 -> UU2 .
>> Variable a : F ( UU1 ) .
>> 
>> (* The following two lines establish that UU2 : UU3 and UU2 is a subtype 
>> of UU3 *)
>> 
>> Definition subuu2uu3 : UU2 -> UU3 := fun X : UU2 => X . 
>> Definition inuu2uu3 : UU3 := ( fun X0 : UU3 => X0 ) UU2 . 
>> 
>> (* The following code produces universe inconsistency by failing to 
>> recognize that the type of [ t ] is [ UU1 ] . *)
>> 
>> Definition test1 { T : UU3 } ( t : T ) := T .
>> Variable t : UU1 .
>> Variable b : F ( test1 t ) .
> 
> Hi Vladimir,
> 
>  You are thinking of test1 as being polymorphic on the universe level of T, 
> so that
> if T is instantiated by UU1, then [test1 t : UU1 + 1]. This works if you 
> set 
> definitions to be universe polymorphic when no type constraint is given, 
> but wouldn't
> work if you defined instead:
> 
> Definition test1 { T : UU3 } ( t : T ) : UU3 := T. 
> 
> The discrepancy is clear if you use an inductive definition of test1, which 
> automatically supports universe polymorphism:
> 
> Inductive itest1 {T:UU3} (t : T) :=
>  intro_test1 : T -> itest1 t.
> 
> Then the [Variable b : F (itest1 t)] typechecks.
> 
>> I think in this situation the inference algorithm should either complain 
>> that there is an ambiguity or infer UU1 as the type of t ( in general it 
>> should choose the lowest universe to which is known to t belong ) .
> 
> I agree the type inference should find the lowest level possible, there's 
> been a few improvements in this respect recently, by making unification 
> actually aware of the sort
> variables. It is however a different problem from making definitions 
> polymorphic.
> I have a tentative patch for the later [1] (mainly the kernel/*.ml changes 
> are necessary), 
> and it seems not to cause any problem. It is also justified by Harper and 
> Pollack's 
> version of typical ambiguity with definitions.
> 
> [1] 
> https://github.com/mattam82/Coq-misc/commit/d98dfbcae463f8d699765e2d7004becd7714d6cf#diff-6
> 
> Hope this helps,
> -- Matthieu
>