why no universe inference in theorems?

Stream: lean4

[Michael Jam]

On nightly-2021-08-29, this fails:
theorem f (l0 : Σ α, List α) (h : (l : Σ α, List α) → True) : True := h l0
It fails because lean assigns a different universe to α in l0 and h.
But if I change that theorem into a def it works:
def f (l0 : Σ α, List α) (h : (l : Σ α, List α) → True) : True := h l0
It succeeds because lean assigns the same universe to both (my guess is that some universe inference must be happening).
I don't really know whether universe inference is desirable here, but what I really don't understand is why the behavior depends on if I use theorem/def keyword. theorem actually seems more flexible as it doesn't have to generate code... Is it a bug, or do I misunderstand something?

[Reid Barton]

In Lean 3 the type of a def is inferred taking the body of the definition into account, while the type of a theorem is not. Don't know if it is the same in Lean 4, but it looks like it.

[Michael Jam]

Thanks, I think you're right... If I sorry the def and hover on the alphas they are in different universes