`Stack overflow detected. Aborting.` on macro

[srghma]

Prerequisites

• https://live.lean-lang.org/ errors too, but nightly - dont know, didnt wait for Waiting for Lean server to start...

Description

minimal code is

-- inductive FileTree where
--   | file : String → FileTree
--   | dir : String → List FileTree → FileTree
--   deriving Repr

-- open Lean Elab Macro Term

declare_syntax_cat file_tree
-- syntax str : file_tree
-- syntax ident " {" file_tree* "}" : file_tree
syntax file_tree* : file_tree

macro_rules
| `(file_tree| $name:str) => `(FileTree.file $name)

--- | `(file_tree| $name:ident { $fs:file_tree* }) =>
---     `(FileTree.dir $(quote name.getId.toString) [ $[$fs],* ])
---
--- -- Example usage
--- #eval (file_tree|
---   src {
---     "Main.lean"
---     "Utils.lean"
---   }
---   test {
---     "MainTest.lean"
---   }
---   "README.md"
--- )

Versions

Lean 4.20.0-rc5
Target: x86_64-unknown-linux-gnu

Impact

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

[Rob23oba]

Well file_tree* : file_tree means that the empty string is a filetree and one filetree is another filetree node which can be infinitely nested -- in other words this is simply not good grammar because it can always continue parsing empty strings. A better syntax would be filetree file_tree+ : filetree. Maybe this kind of syntax should be forbidden though...?