Universe polymorphic local instance

Stream: mathlib4

[Anatole Dedecker]

Do we have any ways to avoid this? For context this is PR #5771

[Eric Wieser]

I'm not sure this is worth worrying about

[Chris Hughes]

I thought Type* was supposed to avoid it by forcing all types to be in different universes whatever happens.

[Eric Wieser]

I don't think that's the question here; the problem is that when you write have := FiniteDimensional.complete 𝕜 it creates a single local bound by a single universe metavariable, which can be only unified once; wherease when you write lemma foo := FiniteDimensional.complete 𝕜 then Lean generates a family of declarations indexed by the universe variable

[Chris Hughes]

I see, so Type* is having the desired effect by not using the instance for both E and F. I agree that's it's not a huge problem probably. It's never come up for me.

[Eric Wieser]

I don't think Type* is relevant here