partial+mutual crash again

Stream: lean4

[Siddharth Bhat]

After the discussion on this LEAN4 issue about mutual constants, I modified the program discussed in the issue, and I now have another crash:

inductive Foo
| mk: (Int -> Foo) -> Foo
| terminal: Foo
deriving Inhabited

mutual
  partial def even (_: Unit) : Foo :=
     Foo.mk (fun i => odd () )
  partial def odd (_: Unit) : Foo :=
    Foo.mk (fun i => even ())
end

def hasLayer (f: Foo) : Bool :=
 match f with
 | Foo.mk _ => true
 | Foo.terminal => false

def main : IO Unit := do
  IO.println (if hasLayer (odd ()) then "LAYER" else "TERMINAL")
  return ()

I expect the program to print "LAYER" on being run. The program crashes:

$ make crash && ./crash
lean4-contrib/build/stage1/bin/lean --version
Lean (version 4.0.0, commit db5df69db460, Release)
lean4-contrib/build/stage1/bin/lean crash.lean -c crash.c
lean4-contrib/build/stage1/bin/leanc crash.c -o crash
zsh: segmentation fault (core dumped)  ./crash

GDB claims the crash is at lean_mark_persistent

Reading symbols from ./crash...
(No debugging symbols found in ./crash)
(gdb) run
...
Program received signal SIGSEGV, Segmentation fault.
0x000055555572b1a2 in lean_mark_persistent ()
(gdb) bt
#0  0x000055555572b1a2 in lean_mark_persistent ()
#1  0x000055555555c5f6 in initialize_crash ()
#2  0x000055555555c72f in main ()
(gdb)

• Is this expected behaviour, or a bug?
• Also, is it easier if I ask these types of questions on the issue tracker, or here on zulip?

[Leonardo de Moura]

Is this expected behaviour, or a bug?

Sorry, the compiler is eliminating the unused argument, and is reducing your code to the mutually recursive constants issue you hit before.
You should write.

mutual
  partial def even (u : Unit) : Foo :=
     Foo.mk (fun i => odd u)
  partial def odd (u : Unit) : Foo :=
    Foo.mk (fun i => even u)
end