Stack overflow in sorry

Stream: general

[Alex Meiburg]

This (very simple! no mathlib! no tactics!) code causes a stack overflow on the lean server immediately and deterministically. I have no clue why. This is minified, of course, from the actual code I was working on.

structure H where
  a : Nat

def prop1 (M : H) : Prop :=
  sorry

def prop2 (M : H) : Prop :=
  sorry

theorem prop2.prop1 {M : H} (hM : prop2 M) : prop1 M :=
  sorry

structure DataProp1 where
  data : H
  is_prop1 : prop1 data

structure DataProp2 extends DataProp1 where
  is_prop2 : prop2 data
  is_prop1 := is_prop2.prop1

def breakingBug : DataProp2 where
  data := ⟨0⟩
  is_prop2 := by
    sorry

[Alex Meiburg]

It doesn't seem to matter what goes in the sorrys, or the "0" value (or using something other than Nat), or if you make the def noncomputable or not.

[Alex Meiburg]

Oddly -- if I change the "by sorry" at the bottom to "sorry", then it doesn't crash.

[Alex Meiburg]

So I have to conclude that, somehow, there is a bug in the sorry tactic!?

[Kyle Miller]

There's a chance it's a bug in default values in structures that that are for fields from parent structures. I've seen some oddities in it before.

[Kyle Miller]

Evidence pointing toward that is that this avoids the stack overflow:

structure DataProp2 extends DataProp1 where
  is_prop2 : prop2 data
  is_prop1 := sorry

[Alex Meiburg]

@Kyle Miller do you think it could involve _entering tactic mode_ that is triggering it? Because the "sorry" itself shouldn't do anything

[Kevin Buzzard]

Something like this (sorry v by sorry crashing) came up a week or so ago -- I think it might have been Jz Pan when doing algebra but I'm on mobile and can't search. Maybe Floris minimised it and an issue was opened?

[Richard Osborn]

It crashes the moment you type by, so sorry has nothing to do with it. I believe when lean is creating the type for is_prop2 it needs to construct a DataProp1 to get the data field which then tries to use is_prop1 := is_prop2.prop1 and this causes infinite recursion.

[Junyan Xu]

lean4#3150