Universe-related(?) error when renaming type variables

Stream: new members

[Michael Rothgang]

As expressed in the style guide, I tried to rename the type variables in Topology.Homeomorph to match standard mathematics conventions. (I was touching the file anyway, in a different PR.)
Building this, however, yields an error I don't understand. The first error, on line 2506 in Topology.Module.Basic is

application type mismatch
  ↑(Homeomorph.funUnique ι) M
argument
  M
has type
  Type u_3 : Type (u_3 + 1)
but is expected to have type
  ι → ?m.2568875 : Type (max u_1 ?u.2568873)

Code in #7587, build errors also in the files tab.

I have only a vague understanding of universes; no particular idea what could be causing the issue here.

My best guess is that changing Homeomorph.refl is the culprit: but I have no idea why that should cause an issue. To me, the lines look basically identical. Apparently, this is deeper than I anticipated... apologies for inadvertedly causing a mess!

[Michael Rothgang]

Full set of errors, from the build log

Header

Error: ./././Mathlib/Topology/Algebra/Module/Basic.lean:2506:2: error: expected structure
Error: ./././Mathlib/Topology/Algebra/Module/Basic.lean:2506:27: error: application type mismatch
↑(Homeomorph.funUnique ι) M
argument
M
has type
Type u_3 : Type (u_3 + 1)
but is expected to have type
ι → ?m.2568875 : Type (max u_1 ?u.2568873)
Error: ./././Mathlib/Topology/Algebra/Module/Basic.lean:2513:2: error: type mismatch
rfl
has type
↑(funUnique ι R M) = ↑(funUnique ι R M) : Prop
but is expected to have type
↑(funUnique ι R M) = Function.eval default : Prop
Error: ./././Mathlib/Topology/Algebra/Module/Basic.lean:2518:2: error: type mismatch
rfl
has type
↑(ContinuousLinearEquiv.symm (funUnique ι R M)) = ↑(ContinuousLinearEquiv.symm (funUnique ι R M)) : Prop
but is expected to have type
↑(ContinuousLinearEquiv.symm (funUnique ι R M)) = Function.const ι : Prop

[Michael Rothgang]

Never mind: I've found the error. "Re-using" in funUnique caused issues; reverting that fixes things.

[Yaël Dillies]

Sorry, why do we care about the case of variables?