Type annotation prevents elaboration of universe level

Stream: lean4

[Jakob von Raumer]

I have a strange case where adding the exact type signature prevents it from being elaborated:

section
variable (A : Type) (B : A → Prop)

def foo := PSigma B -- succeeds

def bar : Type := PSigma B -- fails
end

Do you think this can be fixed?