Bug causing stack overflow

Stream: lean4

[Junyan Xu]

The following code crashes Lean:

import Mathlib.Algebra.Algebra.Subalgebra.Basic
example {F E} [CommSemiring F] [Semiring E] [Algebra F E] : Subalgebra F E where
  carrier := _
  add_mem' := _
  mul_mem' := _
  algebraMap_mem' := _

This is a more minimal example (thanks to @Kevin Buzzard) than the original crash:

import Mathlib.FieldTheory.IntermediateField
example {F E} [Field F] [Field E] [Algebra F E] : IntermediateField F E where
  carrier := _
  add_mem' := _
  mul_mem' := _
  inv_mem' := _
  algebraMap_mem' := _

Lean 4 Web reports:

The Lean Server has stopped processing this file:
Server process for file:///LeanProject.lean crashed, likely due to a stack overflow or a bug.

Locally I usually get

Stack overflow detected. Aborting.

but sometimes it's more detailed:

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)

One strange thing: the structure docs#IntermediateField actually has two more fields one_mem' and zero_mem', and if you add both of them then Lean doesn't crash, but it still crashes if you only add one of them. If you remove one of the five fields, it no longer crashes. Strangely, if you don't write any of the field names, Lean's suggestion is missing the zero_mem' and one_mem' fields:

fields missing: 'carrier', 'mul_mem'', 'add_mem'', 'algebraMap_mem'', 'inv_mem''

Reproduced 100% of the time.

[Yury G. Kudryashov]

I reported another crash recently, and I was told that you need to make a Mathlib-free #mwe if you want it to be investigated.

[Kim Morrison]

It doesn't hurt to create an issue on the Lean4 repo to track issues, but realistically the first step of resolving problems like this is to create a Mathlib-free minimisation. We have a label missing mwe on the Lean4 repo that we can tag report bug reports with that still need this.

Creating a Mathlib free minimisation take some effort, but usually isn't super difficult.

If I've got no idea what the cause is and just want to minimise I follow this algorithm:

• Delete anything from the file that isn't necessary to exhibit the problem. It is particularly helpful to remove proofs! Often it's a good idea to remove structure fields too.
• Delete any imports that aren't necessary, or can be replaced with further upstream imports.
• Take an import X, create a new section X at the top of the file, and copy and paste the contents of X into that section (moving imports to the head of the file).
• Repeat these steps until there are no more imports!

In practice one saves lots of time by taking clever shortcuts that circumvent needing some imports completely...

[Kim Morrison]

@Anne Baanen bravely attempted to automate a version of this, but in practice it wasn't efficient enough for use.

[Kevin Buzzard]

I got this far but I need to do other things now:

import Mathlib.Algebra.Ring.Hom.Defs
import Mathlib.GroupTheory.Submonoid.Basic

class Algebra' (R : Type) (A : Type) [CommSemiring R] [Semiring A] extends R →+* A where

def algebraMap' (R : Type) (A : Type) [CommSemiring R] [Semiring A] [Algebra' R A] : R →+* A :=
  Algebra'.toRingHom

structure Subalgebra' (R : Type) (A : Type) [CommSemiring R] [Semiring A] [Algebra' R A] extends
    Submonoid A : Type where
  algebraMap_mem' : ∀ r, algebraMap' R A r ∈ carrier
  one_mem' := (algebraMap' R A).map_one ▸ algebraMap_mem' 1 -- this is the problem

example {F E} [CommSemiring F] [Semiring E] [Algebra' F E] : Subalgebra' F E where
  carrier := _
  mul_mem' := _
  algebraMap_mem' := _

[Kevin Buzzard]

Now it's just a matter (hopefully) of dropping in definitions of ring etc

[Kevin Buzzard]

Actually I just remembered that I made https://github.com/kbuzzard/MweSkeletons -- maybe I'll spend a little more time on this and see if I can get it over the line.

[Kevin Buzzard]

OK so this highly non-minimal but mathlib-free example https://gist.github.com/kbuzzard/931c7ce55d86d9f40e882eb2af2be96c produces the error

Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)

for me on Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release). Sorry it's a bit of a rush job, I just copied and pasted a few files from that repo I linked to, there will be a whole bunch more minimisation which one can do here (e.g. removing all mention of inv and units) but now I really do have to go.

[Kevin Buzzard]

The issue seems to be that in the definition of Subalgebra' the one_mem' field has a default entry which for some reason the example doesn't like.

[Anne Baanen]

I wanted to try the minimizer script anyway and I can't reproduce the stack overflow in either example:

% lake env lean stack-overflow.lean # Kevin's minimized version
deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)
% lake env lean stack-overflow2.lean # Junyan's original version
deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)

My system is:

% lean --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)
% uname -a
Linux McChouffe 6.1.62-1-lts #1 SMP PREEMPT_DYNAMIC Thu, 09 Nov 2023 17:21:17 +0000 x86_64 GNU/Linux
% ulimit -a
-t: cpu time (seconds)              unlimited
-f: file size (blocks)              unlimited
-d: data seg size (kbytes)          unlimited
-s: stack size (kbytes)             8192
-c: core file size (blocks)         unlimited
-m: resident set size (kbytes)      unlimited
-u: processes                       63551
-n: file descriptors                1024
-l: locked-in-memory size (kbytes)  8192
-v: address space (kbytes)          unlimited
-x: file locks                      unlimited
-i: pending signals                 63551
-q: bytes in POSIX msg queues       819200
-e: max nice                        0
-r: max rt priority                 0
-N 15: rt cpu time (microseconds)   unlimited

[Kevin Buzzard]

I get the same error as you when running the same command as you. The thing I cut and pasted was the output I got from VS Code on the same file (which seems to be the same error wrapped in an explanation that it was an uncaught exception)

[Anne Baanen]

Here's a cleaned up version of the autominimizer output on @Kevin Buzzard's results:

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := sorry

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := sorry

class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
  zero_mul : ∀ a : M₀, 0 * a = 0
  mul_zero : ∀ a : M₀, a * 0 = 0

class AddSemigroup (G : Type u) extends Add G where
  add_assoc : ∀ a b c : G, a + b + c = a + (b + c)

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class AddCommSemigroup (G : Type u) extends AddSemigroup G where
  add_comm : ∀ a b : G, a + b = b + a

class SemigroupWithZero (S₀ : Type _) extends Semigroup S₀, MulZeroClass S₀

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class AddZeroClass (M : Type u) extends Zero M, Add M where
  zero_add : ∀ a : M, 0 + a = a
  add_zero : ∀ a : M, a + 0 = a

class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀

class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where

class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀

class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M

class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
  sub a b := sorry

class AddMonoidWithOne (R : Type u) extends AddMonoid R, One R where

class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M

class Distrib (R : Type _) extends Mul R, Add R where
  protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

class NonUnitalNonAssocSemiring (α : Type u) extends AddCommMonoid α, Distrib α, MulZeroClass α

class AddCommMonoidWithOne (R : Type _) extends AddMonoidWithOne R, AddCommMonoid R

class NonAssocSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, MulZeroOneClass α,
    AddCommMonoidWithOne α

class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α, SemigroupWithZero α

class Semiring (α : Type u) extends NonUnitalSemiring α, NonAssocSemiring α, MonoidWithZero α

class CommSemiring (R : Type u) extends Semiring R, CommMonoid R

variable {β : Sort v}

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

variable (F α : Sort _) (β : α → Sort _)

variable {F} [i : FunLike F α β]

instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

structure ZeroHom (M : Type _) (N : Type _) [Zero M] [Zero N] where
  toFun : M → N
  map_zero' : toFun 0 = 0

class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N]
  extends FunLike F M fun _ => N where
  map_zero : ∀ f : F, f 0 = 0

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  toFun : M → N
  map_one' : toFun 1 = 1

class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
  extends FunLike F M fun _ => N where
  map_one : ∀ f : F, f 1 = 1

structure AddHom (M : Type _) (N : Type _) [Add M] [Add N] where
  toFun : M → N
  map_add' : ∀ x y, toFun (x + y) = toFun x + toFun y

class AddHomClass (F : Type _) (M N : outParam (Type _)) [Add M] [Add N]
  extends FunLike F M fun _ => N where
  map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N
  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
  extends FunLike F M fun _ => N where
  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

structure AddMonoidHom (M : Type _) (N : Type _) [AddZeroClass M] [AddZeroClass N] extends
  ZeroHom M N, AddHom M N

infixr:25 " →+ " => AddMonoidHom

class AddMonoidHomClass (F : Type _) (M N : outParam (Type _)) [AddZeroClass M] [AddZeroClass N]
  extends AddHomClass F M N, ZeroHomClass F M N

structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

infixr:25 " →* " => MonoidHom

class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N

structure MonoidWithZeroHom (M : Type _) (N : Type _)
  [MulZeroOneClass M] [MulZeroOneClass N] extends ZeroHom M N, MonoidHom M N

infixr:25 " →*₀ " => MonoidWithZeroHom
structure NonUnitalRingHom (α β : Type _) [NonUnitalNonAssocSemiring α]
  [NonUnitalNonAssocSemiring β] extends α →ₙ* β, α →+ β

class MonoidWithZeroHomClass (F : Type _) (M N : outParam (Type _)) [MulZeroOneClass M]
  [MulZeroOneClass N] extends MonoidHomClass F M N, ZeroHomClass F M N

infixr:25 " →ₙ+* " => NonUnitalRingHom

structure RingHom (α : Type _) (β : Type _) [NonAssocSemiring α] [NonAssocSemiring β] extends
  α →* β, α →+ β, α →ₙ+* β, α →*₀ β

infixr:25 " →+* " => RingHom

class RingHomClass (F : Type _) (α β : outParam (Type _)) [NonAssocSemiring α]
  [NonAssocSemiring β] extends FunLike F α (fun _ => β)

instance instRingHomClass {β : Type _} {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} : RingHomClass (α →+* β) α β where
  coe f := sorry

def Set (α : Type u) := α → Prop

instance : Membership α (Set α) := sorry

structure Subsemigroup (M : Type _) [Mul M] where
  carrier : Set M
  mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier

structure Submonoid (M : Type _) [MulOneClass M] extends Subsemigroup M where
  one_mem' : (1 : M) ∈ carrier

class Algebra' (R : Type) (A : Type) [CommSemiring R] [Semiring A] extends R →+* A where

def algebraMap' (R : Type) (A : Type) [CommSemiring R] [Semiring A] [Algebra' R A] : R →+* A := sorry

protected theorem RingHom.map_one {α β : Type _} [Semiring α] [Semiring β] (f : α →+* β) : f 1 = 1 := sorry

structure Subalgebra' (R : Type) (A : Type) [CommSemiring R] [Semiring A] [Algebra' R A] extends
    Submonoid A : Type where
  algebraMap_mem' : ∀ r, algebraMap' R A r ∈ carrier
  one_mem' := (algebraMap' R A).map_one ▸ algebraMap_mem' 1

example {F E} [CommSemiring F] [Semiring E] [Algebra' F E] : Subalgebra' F E where
  carrier := _
  mul_mem' := _
  algebraMap_mem' := _

Somehow it figured out you can delete some lines in the file and cause Lean to crash before it detects the resulting errors. I fixed that up so there should only be warnings and then the Lean crash.

[Kevin Buzzard]

Nice! I've removed all mentions of 0 and +, and it's now down to this:

class One (α : Type u) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := sorry

class Semigroup (G : Type u) extends Mul G where
  mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)

class CommSemigroup (G : Type u) extends Semigroup G where
  mul_comm : ∀ a b : G, a * b = b * a

class MulOneClass (M : Type u) extends One M, Mul M where
  one_mul : ∀ a : M, 1 * a = a
  mul_one : ∀ a : M, a * 1 = a

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where

class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M

variable {β : Sort v}

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

variable (F α : Sort _) (β : α → Sort _)

variable {F} [i : FunLike F α β]

instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  toFun : M → N
  map_one' : toFun 1 = 1

class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
  extends FunLike F M fun _ => N where
  map_one : ∀ f : F, f 1 = 1

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where
  toFun : M → N
  map_mul' : ∀ x y, toFun (x * y) = toFun x * toFun y

infixr:25 " →ₙ* " => MulHom

class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
  extends FunLike F M fun _ => N where
  map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, M →ₙ* N

infixr:25 " →* " => MonoidHom

class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N

instance instMonoidHomClass {β : Type _} {_ : Monoid α} {_ : Monoid β} : MonoidHomClass (α →* β) α β where
  coe f := sorry
  map_one := sorry
  map_mul := sorry

def Set (α : Type u) := α → Prop

instance : Membership α (Set α) := sorry

structure Subsemigroup (M : Type _) [Mul M] where
  carrier : Set M
  mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier

structure Submonoid (M : Type _) [MulOneClass M] extends Subsemigroup M where
  one_mem' : (1 : M) ∈ carrier

class Algebra' (R : Type) (A : Type) [Monoid R] [Monoid A] extends R →* A where

def algebraMap' (R : Type) (A : Type) [Monoid R] [Monoid A] [Algebra' R A] : R →* A := Algebra'.toMonoidHom

protected theorem MonoidHom.map_one {α β : Type _} [Monoid α] [Monoid β] (f : α →* β) : f 1 = 1 := sorry

structure Subalgebra' (R : Type) (A : Type) [Monoid R] [Monoid A] [Algebra' R A] extends
    Submonoid A : Type where
  algebraMap_mem' : ∀ r, algebraMap' R A r ∈ carrier
  one_mem' := (algebraMap' R A).map_one ▸ algebraMap_mem' 1

example {F E} [Monoid F] [Monoid E] [Algebra' F E] : Subalgebra' F E where
  carrier := _
  mul_mem' := _
  algebraMap_mem' := _

[Anne Baanen]

Here's my final contribution of today: the output of your further minimalization on brutal mode. It reproduces the crash but also has tons of extra errors:

class One (α : Type u) where

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where

class Semigroup (G : Type u) extends Mul G where

class MulOneClass (M : Type u) extends One M, Mul M where

class Monoid (M : Type u) extends Semigroup M, MulOneClass M where

class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

variable {F} [i : FunLike F α β]

instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where

class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
  extends FunLike F M fun _ => N where

structure MulHom (M : Type _) (N : Type _) [Mul M] [Mul N] where

class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]

structure MonoidHom (M : Type _) (N : Type _) [MulOneClass M] [MulOneClass N] extends
  OneHom M N, MulHom M N

class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N

instance instMonoidHomClass {β : Type _} {_ : Monoid α} {_ : Monoid β} : MonoidHomClass (MonoidHom α β) α β where

def Set (α : Type u) := α → Prop

instance : Membership α (Set α) := sorry

structure Subsemigroup (M : Type _) [Mul M] where
  carrier : Set M
  mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier

structure Submonoid (M : Type _) [MulOneClass M] extends Subsemigroup M where
  one_mem' : (1 : M) ∈ carrier

class Algebra' (R : Type) (A : Type) [Monoid R] [Monoid A] extends MonoidHom R A where

def algebraMap' (R : Type) (A : Type) [Monoid R] [Monoid A] [Algebra' R A] : MonoidHom R A := sorry

protected theorem MonoidHom.map_one {α β : Type _} [Monoid α] [Monoid β] (f : MonoidHom α β) : f 1 = 1 := sorry

structure Subalgebra' (R : Type) (A : Type) [Monoid R] [Monoid A] [Algebra' R A] extends
    Submonoid A : Type where
  algebraMap_mem' : ∀ r, algebraMap' R A r ∈ carrier
  one_mem' := (algebraMap' R A).map_one ▸ algebraMap_mem' 1

example {F E} [Monoid F] [Monoid E] [Algebra' F E] : Subalgebra' F E where
  carrier := _
  mul_mem' := _
  algebraMap_mem' := _

[Kevin Buzzard]

I can even remove mul:

class One (α : Type) where
  one : α

instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where
  ofNat := sorry

class FunLike (F : Type) (α : outParam Type) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

variable (F α : Type) (β : α → Type)

variable {F} [i : FunLike F α β]

instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe

structure OneHom (M : Type) (N : Type _) [One M] [One N] where
  toFun : M → N
  map_one' : toFun 1 = 1

class OneHomClass (F : Type) (M N : outParam Type) [One M] [One N]
  extends FunLike F M fun _ => N where
  map_one : ∀ f : F, f 1 = 1

infixr:25 " →1 " => OneHom

instance instOneHomClass {β : Type} {_ : One α} {_ : One β} : OneHomClass (α →1 β) α β where
  coe f := sorry
  map_one := sorry

def Set (α : Type) := α → Prop

instance : Membership α (Set α) := sorry

structure Subone (M : Type) [One M] where
  carrier : Set M
  one_mem' : (1 : M) ∈ carrier

class Algebra' (R : Type) (A : Type) [One R] [One A] extends R →1 A where

def algebraMap' (R : Type) (A : Type) [One R] [One A] [Algebra' R A] : R →1 A := Algebra'.toOneHom

protected theorem OneHom.map_one {α β : Type _} [One α] [One β] (f : α →1 β) : f 1 = 1 := sorry

structure Subalgebra' (R : Type) (A : Type) [One R] [One A] [Algebra' R A] extends
    Subone A : Type where
  algebraMap_mem' : ∀ r, algebraMap' R A r ∈ carrier
  one_mem' := (algebraMap' R A).map_one ▸ algebraMap_mem' 1

example {F E} [One F] [One E] [Algebra' F E] : Subalgebra' F E where
  carrier := _
  algebraMap_mem' := _

[Kevin Buzzard]

I'm not intending on taking this further now; hopefully now this is reasonable enough to start thinking about debugging? Thanks Anne for your help! It inspired me to go further now my workday is over :-)

[Junyan Xu]

Thanks all for the suggestion, diagnosis, and inspirations. I'm now able to reduce it to 20 lines:

class One (α : Type) where
  one : α

variable (R A : Type) [One R] [One A]

class OneHom where
  toFun : R → A
  map_one : toFun One.one = One.one

structure Subone where
  mem : R → Prop
  one_mem : mem One.one

structure Subalgebra [OneHom R A] extends Subone A : Type where
  algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
  one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one

example [OneHom R A] : Subalgebra R A where
  mem := _
  algebraMap_mem := _

[Junyan Xu]

lean4#3150

[Junyan Xu]

It might be helpful to bisect to find out which Lean 4 commit caused this ...

[Mario Carneiro]

Is this actually new?

[Junyan Xu]

It seems anyone who tries to construct a Subalgebra will discover this ...

[Junyan Xu]

Lean only crashes when you put placeholders there, it doesn't crash if you fill the placeholders with something that compiles. So the crash cannot be discovered by compiling mathlib. For example this doesn't crash:

variable {R A : Type} (r : R) (a : A)

structure Subone where
  mem : R → Prop
  one_mem : mem r

variable {f : R → A} (hf : f r = a)

structure Subalgebra extends Subone a : Type where
  algebraMap_mem (r : R) : mem (f r)
  one_mem := cast (congrArg mem hf) (algebraMap_mem r) -- changing ▸ to explicit `cast` has no effect

example : Subalgebra r a hf where
  mem := fun _ ↦ True
  algebraMap_mem := fun _ ↦ trivial

[Yury G. Kudryashov]

I guess, with placeholders it tries to find them by unification, then something breaks.

[Junyan Xu]

It turns out the crash already happens in 4.0.0-m2 (3 years ago)

[Newell Jensen]

I am running into this with linting on #7479

...
info: [68/68] Linking runLinter
libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)

Anyone know how to fix this?

[Jovan Gerbscheid]

I found a much smaller example that crashes with a stack overflow:

def test (a : String) : String :=
  let x : String → String := _
  have : x = 10 := by rfl

(the String types can be replaced with any other type)

From the stack trace we can see the source of the infinite recursion. It is a mutual block in MetavarContext.lean, and has the following pattern of function calls appearing repeatedly:

mkAuxMVarType.abstractRangeAux
mkAuxMVarType
elimMVar
elimApp
visit
Array.mapMUnsafe.map._at._private.src.Lean.MetavarContext.0.Lean.MetavarContext.MkBinding.elimApp._spec_6
elimApp
visit
elimApp
visit
elim

(the top of the list corresponds to the top of the stack, so each function calls the one above it)

This infinite loop is reached via a call to mkLambdaFVars, which calls mkBinding. In particular this call in elabFunValues in MutualDef.lean. So the particular lambda that is trying to be created is

fun a : String =>
  let x : String → String := _
  have : x = 10 := by rfl

Using binary search I found that the stack overflow happens in version 4.9.0 and not in 4.8.0.

[Kim Morrison]

git bisect ... is tricky. :-) Still working on this.

[Kim Morrison]

@Sebastian Ullrich, unfortunately this is an incrementality bug, which appears at lean#3940, commit f97a7d4234bd76bc0f61e43b8c6a78117c1376df

[Kim Morrison]

@Jovan Gerbscheid, would you mind posting your example as new issue, including the fact that it breaks as of lean#3940?

[Jovan Gerbscheid]

lean4#6013

[Jovan Gerbscheid]

I have figured out the cause of the stack overflow. It is a violation of the type occurs check. And the stack overflow in lean#3150 is caused by the same problem.

[Jovan Gerbscheid]

In lean#3150, the problem looks like this:

?m : { α := Nat, a := id ?m }.α

And in lean#6013, the problem looks like this:

?m1 := @OfNat.ofNat (String → String) 10 ?m2
?m2 : let x := ?m1;
  OfNat (String → String) 10

As we can see, both of these type occurs check failures can be made to disappear after a sufficient amount of reducing the type, so they are not inherently bad. But mkLambdaFVars has trouble dealing with them.

[Junyan Xu]

But lean4#3150 occured as early as 4.0.0-m2. So lean4#3940 just made it easier to trigger an old bug?

[Sebastian Ullrich]

yes

[Jovan Gerbscheid]

I can see two ways to fix this:

• change unification/elaboration such that a metavariable type occurrence can't happen. This is tricky, because when assigning metavariables in unification, it explicitly allows some type occurrence to happen, knowing that it will be reduced away later.
• change the free variable elimination procedure so that it can deal with metavariable type occurrences.

I have a fix here that does the latter: lean#6079