bad instance?

Stream: general

[Yury G. Kudryashov]

It seems that docs#finite_dimensional.proper_is_R_or_C is a bad instance. Since Lean resolves instances right-to-left, it looks for [finite_dimensional ?x F], then tries to find [is_R_or_C k] with k = ?x.

[Yury G. Kudryashov]

Am I right?

[Yury G. Kudryashov]

Found while trying to find the reason for linter failures in #10490

[Gabriel Ebner]

It's bad because it enumerates all finite_dimension ?x F instances, i.e., all base fields for the vector space. In this instance it would indeed be better if is_R_or_C ?x was solved first.

[Yury G. Kudryashov]

Should we turn it into a non-instance?

[Gabriel Ebner]

Could we replace K by \real in that instance?

[Sebastien Gouezel]

We can turn it as a non-instance, and only register it as an instance for $\mathbb{R}$. Hopefully this should also apply automatically in the complex situation, as a complex vector space is also registered automatically as a real vector space.

[Yury G. Kudryashov]

We already have an instance for $\mathbb R$. The proof for is_R_or_C uses it, see src#finite_dimensional.proper_is_R_or_C

[Sebastien Gouezel]

Then I would just make this a lemma instead of an instance. Does it break anything?

[Yury G. Kudryashov]

Yes, it does. I'll try to fix it tonight.