universe inequalities

Stream: general

[Reid Barton]

I wonder whether it would be possible to implement a version of universe inequalities as an elaborator feature.
Consider these examples:

universes u v

def mylift : Type u → Type (max u v) := ulift
def mylift' : Type u → Type (max v u) := ulift -- fails
def mylift'' : Type u → Type (max v u) := ulift.{v u}

[Reid Barton]

mylift has the same type as ulift.{v u} so the elaborator doesn't need any help to solve the universe unification problem.
In mylift', the type is written differently and the elaborator doesn't know how to solve max v u =?= max u ?l_2.
We need to help it, as shown in mylift''.

[Reid Barton]

Now maybe the elaborator should just be able to solve this outright, but it also seems like we could help it out a little if we could say: if you get stuck when trying to elaborate the v variable of ulift.{v u}, assume that it will be >= u and use that to simplify the constraints.

[Reid Barton]

Also, now I'm slightly disturbed by the fact that if I write

def mylift''' : Type u → Type (max v u) := ulift.{(max u v) u}

then mylift'' and mylift''' are not definitionally equal.

[Mario Carneiro]

No, those two are entirely different functions that are merely provably isomorphic

[Mario Carneiro]

the relation between them is similar to the relation between two inductive types with the same definition

[Reid Barton]

Right, so I guess I shouldn't be too worried about this.

[Mario Carneiro]

But as a result, the elaborator problem here is literally underdetermined

[Mario Carneiro]

which is a fancy way of saying that max is not injective

[Reid Barton]

Right, so if the problem is underdetermined, maybe we can add constraints to make it determined.

[Reid Barton]

Perhaps the better definition to aim for is actually mylift'''?

[Reid Barton]

since that one's easier to characterize: we say we're only allowed to write ulift.{x y} when x >= y

[Mario Carneiro]

I don't know... universe expressions can get pretty complicated, especially once imax gets involved

[Mario Carneiro]

I agree that it would be easier to find a "maximal assignment", but I'm still not sure that uniquely picks the inputs from the output

[Reid Barton]

I guess a useful thing to do would be to look at some of the actual instances in the category theory library where we have to write universe levels explicitly and see if there's some way we could account automatically for all of them