[Agda] Universe Hierarchy Problem?

[Andreas Abel]

On Dec 7, 2009, at 7:41 PM, Nils Anders Danielsson wrote:
> On 2009-12-07 03:42, kahl at cas.mcmaster.ca wrote:
>> I have managed to get the error message (from Agda-2.2.4):
>>
>>  Set !=< Set1
>>
>> To me, that seems to indicate the claim that Set is not a subtype of
>> Set1, [...]
>
> Set is not a subtype of Set₁.


In Ulf's thesis I read (p. 72)

3.7.3 Universe hierarchy
In the presence of a universe hierarchy the logic has to be extended  
by level
metavariables. This is because when we instantiate a metavariable with
a function type as described above, we do not know what levels the new
metavariables should live at. It is unclear at this point how to  
handle the in-
teraction between universe subtyping and level metavariables, since  
this will
introduce inequality constraints between the variables, rather than  
equal-
ity constraints. The current implementation turns unsolved  
inequalities into
equality constraints, which will necessarily exclude valid solutions.  
The al-
ternative of keeping the inequality constraints and attempting to  
solve them
globally after type checking is potentially very costly.

Which basically points to a lacking theory of unification in the  
presence of inequality constraints.  Research is needed!  Because  
subtyping is a nice thing to have.


Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41