universe resolutions

Stream: general

[Kenny Lau]

universes u v

variables {α : Type u} {β : Type v}
#check (ulift α = ulift β)

[Kenny Lau]

error:

type mismatch at application
  ulift α = ulift β
term
  ulift β
has type
  Type (max v ?) : Type ((max v ?)+1)
but is expected to have type
  Type (max u ?) : Type ((max u ?)+1)

[Kenny Lau]

is there a way to get Lean solve this automatically?

[Kenny Lau]

or is this generally undecidable?

[Kenny Lau]

see e.g. https://github.com/leanprover-community/mathlib/blob/1b85e3c213f57dc4675a821721f51c6c46c9b65a/src/set_theory/cardinal.lean#L881-L882

lemma mk_range_eq_lift {α : Type u} {β : Type v} {f : α → β} (hf : injective f) :
  lift.{v (max u w)} (# (range f)) = lift.{u (max v w)} (# α) :=

[Reid Barton]

Is this the solution (introduce an extra universe parameter) you want it to automatically find?