category theory import breaks CommRing synthesis

Stream: mathlib4

[Kevin Buzzard]

-- import Mathlib.Algebra.Category.AlgebraCat.Basic -- import this to break #synth
import Mathlib.RingTheory.IntegralClosure

variable (R : Type) (A : Type) [CommRing R] [CommRing A] [Algebra R A]

#synth CommRing (integralClosure R A)
-- breaks if Lean finds `AlgebraCat.of`

Someone had import Mathlib and this #synth was failing, which surprised me, but when I looked at the term I could see why; integralClosure R A is a term of type Subalgebra R A and A is commutative, so this is a commutative ring, but with AlgebraCat imported Lean decides that the best way to make a type out of integralClosure R A is to go via the category of R-algebras (this will be because of this dubious "try most recent instance first" philosophy I guess) and when we're in this category we don't have commutativity in general. Should I decrease the priority of the category theory instance causing the trouble, or increase the priority of the commutative algebra instance, or do something else?

[Riccardo Brasca]

Does it work increasing heartbeats?

[Kevin Buzzard]

The import changes the term from ↥(integralClosure R A) : Type to ↑(AlgebraCat.of R ↥(integralClosure R A)) : Type, and I don't think it's possible to synthesize the instance for the new term however many heartbeats you have.

[Kevin Buzzard]

With the import, the typeclass trace is

[Meta.synthInstance] ✅ CoeT (Subalgebra R A) (integralClosure R A) Type ▼
  [] new goal CoeT (Subalgebra R A) (integralClosure R A) Type ▼
  [instances] #[@instCoeTOfCoeHTCT, @instCoeTOfCoeDep, @instCoeT]
  [] ❌ apply @instCoeT to CoeT (Subalgebra R A) (integralClosure R A) Type ▶
  [] ✅ apply @instCoeTOfCoeDep to CoeT (Subalgebra R A) (integralClosure R A) Type ▶
  [] ✅ apply @instCoeTOfCoeHTCT to CoeT (Subalgebra R A) (integralClosure R A) Type ▶
  [] ❌ apply @instCoeHTCT to CoeHTCT (Subalgebra R A) Type ▶
  [] ✅ apply @instCoeHTCTOfCoeHTC to CoeHTCT (Subalgebra R A) Type ▶
  [] ❌ apply @instCoeHTC to CoeHTC (Subalgebra R A) Type ▶
  [] ✅ apply @instCoeHTCOfCoeOTC to CoeHTC (Subalgebra R A) Type ▶
  [] ❌ apply @instCoeOTC to CoeOTC (Subalgebra R A) Type ▶
  [] ✅ apply @instCoeOTCOfCoeTC to CoeOTC (Subalgebra R A) Type ▶
  [] ❌ apply @instCoeTC to CoeTC (Subalgebra R A) Type ▶
  [] ✅ apply @instCoeTCOfCoe_1 to CoeTC (Subalgebra R A) Type ▶
  [] ✅ apply @instCoeTCOfCoe to CoeTC (Subalgebra R A) Type ▶
  [] ❌ apply boolToProp to Coe ?m.650 Type ▶
  [] ✅ apply @instCoeOTCOfCoeOut to CoeOTC (Subalgebra R A) Type ▶
  [] ✅ apply @instCoeOutSubalgebraAlgebraCat to CoeOut (Subalgebra R A) (AlgebraCat R) ▶
  [resume] propagating CoeOut (Subalgebra R A)
      (AlgebraCat R) to subgoal CoeOut (Subalgebra R A) (AlgebraCat R) of CoeOTC (Subalgebra R A) Type ▶
...

and the problem is that this succeeds, and gives us a circuitous route via AlgebraCat (and things here are not commutative in general).

[Kim Morrison]

@Kevin Buzzard: chore(AlgebraCat): remove bad instance #14804

[Kim Morrison]

No one was using it, so lets just get rid of it.