# Zulip Chat Archive

## Stream: general

### Topic: will this make typclass inference loop?

#### Kevin Buzzard (Feb 08 2019 at 11:27):

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?

#### Johan Commelin (Feb 08 2019 at 11:30):

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

#### Kevin Buzzard (Feb 08 2019 at 11:31):

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 (Feb 08 2019 at 11:32):

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 (Feb 08 2019 at 11:33):

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

#### Kevin Buzzard (Feb 08 2019 at 11:33):

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

#### Kenny Lau (Feb 08 2019 at 11:35):

I think I got stuck in a typeclass loop before

#### Kevin Buzzard (Feb 08 2019 at 11:40):

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 (Feb 08 2019 at 11:41):

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

#### Kenny Lau (Feb 08 2019 at 11:43):

sure?

Last updated: Dec 20 2023 at 11:08 UTC