Why does #synth cause an error somewhere else?

Stream: new members

[Snir Broshi]

import Mathlib

variable {R : Type*} [CommRing R]
variable {K : Type*} [CommRing K]
variable [Algebra R K]
variable [IsFractionRing R K]
instance : Field K := sorry

#synth Field K

This produces a strange error on the IsFractionRing: failed to synthesize Algebra R K
It's trivial to synthesize Algebra R K since it's the variable before it.

Commenting out the synth command makes the error go away somehow, spooky action at a distance.

Adding a [Field K] before the [Algebra R K] gives an error even without the instance and synth:

import Mathlib

variable {R : Type*} [CommRing R]
variable {K : Type*} [CommRing K]
variable [Field K]
variable [Algebra R K]
variable [IsFractionRing R K]

probably because there's now more than one addition and multiplication on K, but either moving the [Field K] below [Algebra R K] or deleting [CommRing K] makes it work fine.

What's going on?

[Eric Wieser]

instance : Field K := sorry says "every type is a field, even things that are already a ring in an unrelated way"

[Eric Wieser]

If you use instance foo : Field K := sorry instead, you can hover over foo and see that the instance is clearly bad

[Snir Broshi]

I agree that instance is bad, but how does #synth trigger an error somewhere far away from it?

[Eric Wieser]

variables are re-elaborated on every command