Importing Algebra.DirectSum.Ring avoids unrelated timeouts

Stream: general

[Yaël Dillies]

Consider the following file

import Mathlib.Algebra.DirectSum.Ring -- TODO: Spooky!
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

namespace CategoryTheory.Limits
variable {C : Type*} [Category C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}

@[simp]
def pushoutCocone.toBinaryCofan : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (.mk g) where
  obj c := BinaryCofan.mk (Under.homMk (U := Under.mk f) c.inl rfl)
      (Under.homMk (U := Under.mk g) (V := Under.mk (f ≫ c.inl)) c.inr c.condition.symm)
  map {c1 c2} a := {
    hom := Under.homMk a.hom
    w := by rintro (_|_) <;> aesop_cat
  }

end CategoryTheory.Limits

[Yaël Dillies]

It compiles. but if you remove the first import (which is not used), then the c.inl in obj does not typecheck anymore!

[Yaël Dillies]

You can also replace Mathlib.Algebra.DirectSum.Ring by its imports, and that breaks too

[Yaël Dillies]

Looking at the errors, I was expecting this to come from the fact that Algebra.DirectSum.Ring declares unification hints, but it does not.

[Yaël Dillies]

I am completely stunned. Any ideas?

[Yaël Dillies]

Okay, I have managed to reduce it further:

import Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

section
variable {ι : Type*} [Zero ι] (A : ι → Type*)

class GSemiring where natCast : ℕ → A 0

-- Comment out the next line and `pushoutCocone.toBinaryCofan` breaks
instance [GSemiring A] : NatCast (A 0) := ⟨GSemiring.natCast⟩

end

namespace CategoryTheory.Limits
variable {C : Type*} [Category C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}

@[simp]
def pushoutCocone.toBinaryCofan : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (.mk g) where
  obj c := BinaryCofan.mk (Under.homMk (U := Under.mk f) c.inl rfl)
      (Under.homMk (U := Under.mk g) (V := Under.mk (f ≫ c.inl)) c.inr c.condition.symm)
  map {c1 c2} a := {
    hom := Under.homMk a.hom
    w := by rintro (_|_) <;> aesop_cat
  }

end CategoryTheory.Limits

[Yaël Dillies]

@Eric Wieser, you will be glad to discover more weird consequences of your instance docs#DirectSum.instNatCastOfNat :grinning: