Crash encountered when compiling handwrittten recursive descent parser in LEAN4

crash.lean

inductive Maybe (a : Type) : Type where 
| ok: a -> Maybe a
| err: Maybe a

structure P (a: Type) where 
   runP: String -> Maybe (String × a)

def ppure {a: Type} (v: a): P a := { runP :=  λ s => Maybe.ok (s, v) }

def pbind {a b: Type} (pa: P a) (a2pb : a -> P b): P b := 
   { runP := λs => match pa.runP s with 
            | Maybe.ok (s', a) => (a2pb a).runP  s'
            | Maybe.err => Maybe.err 
   }

instance : Monad P := { pure := ppure, bind := pbind }

def pfail : P a := { runP := λ _  => Maybe.err }

instance : Inhabited (P a) where default := pfail

mutual
partial def pregion : P Unit :=  do
  pblock

partial def pop : P Unit := do 
  pregion

partial def pblock : P Unit := do
   pop
end  -- end mutual

def main: IO Unit := do
  return ()

run-log.md

Running

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

GDB log:

(gdb) run
Starting program: /home/bollu/work/2-mlir-verif/crash 
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/usr/lib/libthread_db.so.1".

Program received signal SIGSEGV, Segmentation fault.
0x000055555572b9b2 in lean_mark_persistent ()
(gdb) bt
#0  0x000055555572b9b2 in lean_mark_persistent ()
#1  0x000055555555ceac in initialize_crash ()
#2  0x000055555555cf41 in main ()
(gdb)