will this make typclass inference loop?

Stream: general

[Kevin Buzzard]

A field is an integral domain. The field of fractions of an integral domain is a field. We have an instance discrete_field X -> integral_domain X. But I just noticed that integral_domain X -> discrete_field (quotient_ring X) is a definition and not an instance. Are there problems with making it an instance?

https://github.com/leanprover-community/mathlib/blob/f623d346a09cc7716389a406ee6bb1139fff28da/src/ring_theory/localization.lean#L212

[Johan Commelin]

If I understand things correctly, there shouldn't really be a problem.

[Kevin Buzzard]

I would make a PR changing "def" to "instance" but I don't want to waste people's time if this is a bad idea.

[Kevin Buzzard]

I can see that Lean could now go ahead and prove integral_domain (quotient_ring $ quotient_ring $ quotient_ring $ ... $ X) but I don't understand the system well enough to know whether it would ever be tempted by this lunacy

[Kevin Buzzard]

[example for non-maths folk: the field of fractions of Z is Q, the field of fractions of Q is Q]

[Kevin Buzzard]

[except that in Lean they're not equal, just isomorphic]

[Kenny Lau]

I think I got stuck in a typeclass loop before

[Kevin Buzzard]

If the answer actually _is_ "you might get stuck in a typeclass loop" then this will trigger another of my "typeclass inference is not fit for purpose when it comes to mathematics" rants.

[Kevin Buzzard]

Am I allowed to make it a local instance and just gamble in my one particular file?

[Kenny Lau]

sure?