weird hover behavior in vs-code

Stream: general

[Eric Wieser]

Why does hovering over ⋂ give set.Inter : Π {β ι : Type u_2}, (ι → set β) → set β here? Why did β and ι get forced into the same universe, despite docs#set.Inter putting them in different universes?

import algebra.module.basic

variables {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] (S : set (submodule R M))

#check ⋂ s ∈ S, (s : set M)  -- combined universes?
#check (set.Inter $ λ s, set.Inter $ λ (h : s ∈ S), (s : set M))  -- separate universes