Why is Field.toIsField not an instance?

Stream: mathlib4

[Johan Commelin]

Why is docs#Field.toIsField not an instance?

[Yaël Dillies]

Because IsField is not a class, I would guess

[Johan Commelin]

Never mind... because IsField is not a class

[Johan Commelin]

So.... why... is IsField not a class?

[Yaël Dillies]

I think because most people use ¬ IsField R

[Johan Commelin]

hmm, good point

[Kevin Buzzard]

Maybe we should have class IsntField

[Antoine Chambert-Loir]

I worried for 30 seconds at the prospect that R wouldn't be a field. Ok.

[Adam Topaz]

docs#DiscreteValuationRing

[Adam Topaz]

(I also remember some discussions about making Dedekind domains IsntField)

[Johan Commelin]

I really like it that IsntField vs instField isn't confusing at all :grinning:

[Yaël Dillies]

Can't wait for instIsntField

[Damiano Testa]

If there were an instance : IsntField ℤ, would typeclass inference know not to look for Field ℤ? If it were the case, this could be a way of systematically short-circuiting TC searches that are "obviously" going to fail.

[Kevin Buzzard]

Just to be clear, my comment was made in jest, but it's certainly true that it's annoying that fields are regarded as Dedekind domains in the literature because in practice you actually want a word for "smooth affine curve" and what the literature offers is "smooth affine curve or a point". I remember that Maria Ines had to prove that integers of number fields weren't fields, for example.

[Johan Commelin]

Damiano Testa said:

If there were an instance : IsntField ℤ, would typeclass inference know not to look for Field ℤ? If it were the case, this could be a way of systematically short-circuiting TC searches that are "obviously" going to fail.

I think we'll need some systematic data to decide whether such a feature is a good idea.

[Johan Commelin]

To be more precise:

• how often does TC synth go down a path that will "obviously fail"?
• how quickly does it recover with the current algo?
• in how many of these cases can we reasonably expect the "opposite" TC problem to succeed quickly?
• and vice versa, in how many cases will the "opposite" TC problem be a complete waste of time?