[Agda] Level constraints

[Christian Sattler]

Hi all,

Sometimes, you want to define a module/record/some structure over two 
universe indices i ≤ j.Just two examples are lifting and defining types 
of type constructors with large elimination. The current way of doing 
this is to have two parameters i j' and defining j' = i ⊔ j'. This works 
just fine, but there are certain scenarios where you will always have to 
explicitly specify j', even though it seems redundant, like in the 
following example:

open import Agda.Prim

record Lift {i j'} (A : Set i) : Set (i ⊔ j') where
field
lift : A → Lift {j' = j'} A -- (same issue as below)

module _ {u v} (X : Set u) where
Y : Set (u ⊔ v)
Y = Lift {j' = {!!}} X -- both v and u ⊔ v fit the hole

As a programmer, I only care about the final level of Lift X, not about 
the value of j' used to compute i ⊔ j'. But the constraint u ⊔ _1= v 
does not have a unique solution (both u and u ⊔ v fit the metavar). It 
does have, however, a unique solution *up to join with u*, i.e. a unique 
solution _1 ≥ u, and this could be inferred algorithmically if there was 
a way of specifying constraints like that (_1 ⊔ u = u) in the source 
file. One could think of several ways of extending the syntax, either by 
a dependent type

Level≥ : Level → Level

or (more generally) by some kind of constraint type

_Level.≤_ : Level → Level → LevelConstraint

where LevelConstraint gives an explicit way of specifying relationships 
between universe levels and can either be an abstract type, meaning the 
system would always have to infer its value by level constraint solving, 
or could have actual constructors like _Nat.≤_, enabling the user to 
prove constraints by hand (personally, I think this goes too far).

Except for this syntactical addition, the type checking and constraint 
solving would mostly stay the same. What do you think?

Cheers,
Christian