The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 30 juin 2011 à 16:38, Vladimir Voevodsky a écrit :

> 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 .

Yes, this is a property of the type system due to subtyping:
If Γ |- t : T and t ->* t', Γ |- t' : T' with T' <= T, i.e. 
reduction can lower the universe level. 

It unfortunately makes the substitution of equals principle
more restricted as you point out. You can freely substitute 
convertible terms [t : T] and [u : U] only in contexts that
expect values in the "biggest" type of [T] and [U]. Luo 
discusses that in his paper on ECC.

-- Matthieu

> 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
>> 
>