The Coq mailing list

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

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