Bug leading to stack overflow

[alreadydone]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The following code (web editor link) crashes Lean:

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 := _

with the message

Server process for file:///LeanProject.lean crashed, likely due to a stack overflow or a bug.

Locally I sometimes get a more detailed message:

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)

The automatically filled field one_mem in Subalgebra inherited from Subone is apparently causing the trouble.

Thanks to @Vierkantor and @kbuzzard for the minimization efforts on Zulip.

Context

The problem occurs and was discovered in real life:

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' := _

Steps to Reproduce

Click the web editor link above, or paste into your own editor.

Expected behavior: : Lean should not crash

Actual behavior: Lean crashes

Versions

Lean: 4.5.0-rc1
Web editor: unknown OS
Local OS: MacOS Sonoma 14.2.1 / Windows 11

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[alreadydone]

Further minimized, class-free:

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 := _
  algebraMap_mem := _

[alreadydone]

I believe this is a recently introduced problem. I never saw Lean crash when I tried build a Subalgebra until yesterday. Lean doesn't crash if you fill the placeholders with something that compiles (e.g. the following), and that's why the crash can't be discovered by compiling mathlib.

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

[alreadydone]

Two examples that don't crash

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

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

example : Subalgebra r a hf where
  mem := _
  algebraMap_mem := _

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

structure Subone where
  eq_self : r = r

structure Subalgebra extends Subone a : Type where
  map_eq (r : R) : f r = a
  eq_self := (map_eq r).symm.trans (map_eq r)

example : Subalgebra r a f where
  map_eq := _

So it seems for the crash to occur, there needs to be two classes A and B, such that A has at least two fields, B extends A with an extra field, and B auto-fills one field of A with a term that refers to both the new field in B as well as another field of A.

[nomeata]

I believe this is a recently introduced problem

Could you try old daily release to confirm and narrow down when it was introduced? With

elan run --install some-toolchain lean file.lean

(Untested, on the phone) you can download and test a certain toolchain in one command?

[alreadydone]

It turns out the issue occurs much earlier than I expected: it's already present in 4.0.0-m2 (3 years ago), while 4.0.0-m1 can't compile this file.

> elan run --install 4.0.0-m2 lean crash.lean
Stack overflow detected. Aborting.
Abort trap: 6

> elan run --install 4.0.0-m1 lean crash.lean
crash.lean:1:22: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
crash.lean:5:16: error: unknown identifier 'r'
crash.lean:7:21: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
crash.lean:9:29: error: function expected at
  Subone
term has type
  Type
crash.lean:9:29: error: 'sorryAx' is not a structure
crash.lean:13:10: error: unknown identifier 'Subalgebra'
crash.lean:13:28: error: invalid {...} notation, 'sorryAx' is not a structure

And I confirm that since 4.0.0-rc1 (5 months ago), if you leave out the last two lines then Lean will not ask you to include the one_mem field:

> elan run --install 4.0.0-rc1 lean crash.lean
crash.lean:13:28: error: fields missing: 'mem', 'algebraMap_mem'

Maybe people who constructed new Subalgebras somehow all followed something else (e.g. mathlib docs) rather than Lean's suggestion? It's really hard to explain why this is only discovered now ... (One explanation: people usually build Subalgebra from weaker subobjects that already include the one_mem and zero_mem fields, and only supply algebraMap_mem themselves.)

[JovanGerb]

I minimized the example further:
First define

structure A where
  α : Type
  a : α

structure B (f : (α : Type) → α → α) extends A where
  b : α
  a := f α b

Then this fails as expected:

/-
don't know how to synthesize placeholder
context:

⊢ { α := Nat, a := id ?m.795 }.α
-/
example : B @id where
  α := Nat
  b := _

And this has a stack overflow:

-- stack overflow
example (x : Nat) : B @id where
  α := Nat
  b := _

In the non-stack overflow case, hovering over the metavariable shows that

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

So just like in #6013, the stack overflow comes from the mkLambdaFVars call that abstracts x. And just like in #6013, the problem is a violation of the type occurs check.