enough_projectives universe issue

Stream: maths

[Kevin Buzzard]

Module.Module_enough_projectives is somehow broken in Lean 3?

import category_theory.preadditive.projective
import algebra.category.Module.projective

namespace category_theory

-- these work
example (R : Type) [ring R] : enough_projectives (Module.{0} R) := Module.Module_enough_projectives
example (R : Type) [ring R] : enough_projectives (Module.{0} R) := infer_instance

universe u

-- these fail
example (R : Type u) [ring R] : enough_projectives (Module.{u} R) := Module.Module_enough_projectives
example (R : Type u) [ring R] : enough_projectives (Module.{u} R) := infer_instance

-- this works
example (R : Type u) [ring R] : enough_projectives (Module.{u} R) := Module.Module_enough_projectives.{u u}

end category_theory

[Eric Wieser]

Module.Module_enough_projectives.{u _} also works, Lean is only stuck on the first argument of docs#Module.Module_enough_projectives

[Joël Riou]

I have also observed this problem, and suggested a fix at #19061: declaring two instances, one for Module.{max u v} R and one for Module.{u} R (my fix is not syntactically optimal though).