Unexpected Compiler Crash

Stream: general

[Wang Jingting]

I came across the following example, in which the compiler reported "Server process for ... crashed, likely due to a stack overflow or a bug." Does anyone know why that's happening?
A mwe:

import Mathlib

open CategoryTheory

def hello (R : Type u) [CommRing R] : R →+* (End 𝟭 (ModuleCat R)) := by sorry

It seems that a stack overflow is occurring, but I don't really know why.

[Bhavik Mehta]

The same thing happens with just def hello (R : Type u) [CommRing R] : End 𝟭 (ModuleCat R) := by sorry

[Wang Jingting]

Bhavik Mehta said:

The same thing happens with just def hello (R : Type u) [CommRing R] : End 𝟭 (ModuleCat R) := by sorry

Yes, you're right. I also find #check End 𝟭 (ModuleCat R) working fine, #synth Ring (End 𝟭 (ModuleCat R)), #synth Monoid (End 𝟭 (ModuleCat R)) causing stack overflow.

[Notification Bot]

This topic was moved here from #general > Weird Compiler Crash by Wang Jingting.

[Wang Jingting]

Does anyone know why that's happening? I'd really appreciate your help!

[Kevin Buzzard]

Can you try and minimise? Can you get the crash without any imports by just copying definitions from mathlib? If so then you can ask in #lean4 .

[Bhavik Mehta]

My expectation is that this is some dodgy instance resolution using instances in mathlib

[Kevin Buzzard]

import Mathlib.CategoryTheory.Endomorphism

#check CategoryTheory.End -- fine

#check CategoryTheory.Functor.id -- fine

#check CategoryTheory.End CategoryTheory.Functor.id -- stack overflow

[Kevin Buzzard]

--import Mathlib.CategoryTheory.Pi.Basic -- uncomment for stackoverflow
-- these are the imports in `Mathlib.CategoryTheory.Pi.Basic`
import Mathlib.CategoryTheory.EqToHom
import Mathlib.CategoryTheory.NatIso
import Mathlib.CategoryTheory.Products.Basic

universe v u

namespace CategoryTheory

def End {C : Type u} [CategoryStruct.{v} C] (X : C) := X ⟶ X

end CategoryTheory

#check CategoryTheory.End CategoryTheory.Functor.id

[Kevin Buzzard]

OK I need to stop now but here's what I got it down to so far: it's the instance CategoryTheory.pi'. Make it an instance to get a stack overflow. This was on v4.19.0-rc2 (of mathlib and lean) BTW

import Mathlib.CategoryTheory.Functor.Category

namespace CategoryTheory

universe w₀ w₁ w₂ v₁ v₂ v₃ u₁ u₂ u₃

variable {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [∀ i, Category.{v₁} (C i)]

/-- `pi C` gives the cartesian product of an indexed family of categories.
-/
instance pi : Category.{max w₀ v₁} (∀ i, C i) where
  Hom X Y := ∀ i, X i ⟶ Y i
  id X i := 𝟙 (X i)
  comp f g i := f i ≫ g i

/-- This provides some assistance to typeclass search in a common situation,
which otherwise fails. (Without this `CategoryTheory.Pi.has_limit_of_has_limit_comp_eval` fails.)
-/
abbrev pi' {I : Type v₁} (C : I → Type u₁) [∀ i, Category.{v₁} (C i)] : Category.{v₁} (∀ i, C i) :=
  CategoryTheory.pi C

-- uncomment the next line for a stack overflow
--attribute [instance] pi'

universe v u

def End {C : Type u} [CategoryStruct.{v} C] (X : C) := X ⟶ X

end CategoryTheory

#check CategoryTheory.End CategoryTheory.Functor.id

[Kevin Buzzard]

I left the mathlib docstrings but CategoryTheory.Pi.has_limit_of_has_limit_comp_eval doesn't seem to exist any more?

[Bhavik Mehta]

It looks like the docstring wasn't ported, and it refers to docs#CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval

[Kevin Buzzard]

Mathlib seems to compile with pi' deleted. I'll make a PR.

[Kevin Buzzard]

#23812 (let's see what benchmarking says)