Some personal notes:

• Last year @stefan-hoeck showed us a very efficient constant-time parser using his library idris2-parser. My personal assessment was that it's essentially the target to hit in term of performance, but re-writing the entire parser with it might be too much work.
• At the beginning of the year I had a chat with @wenkokke about Tree-Sitter, it is undeniable that tree-sitter offers large benefits in terms of ecosystem and accessibility. Because of this, I personally think it is worth investing in a tree-sitter compatible solution. I started working on a prototype to get familiarised with the API but made no progress on the biggest piece of software that we need for an idris2 version: the whitespace lexer.
• Across the years, many contributors, including myself, thought about tackling the problem of partial-evaluation for idris. But nothing materialised yet. At this point the problem is so big and complex it's a project in and of itself, because of that, I don't think we should think of it as a "quick fix for parser performance" but as a genuine research project.
• There might be a way out of this local minimum by developping a solution akin to happy/bison/BNFC where we have a static definition of the grammar and generate idris2-parser code from it, and a tree-sitter grammar for editor support. This solution takes us away from the realm of research and into pure engineering, which might be more achievable given the resources we are given.
• The parser code itself leaves at lot to be desired. Its monolithic architecture makes it hard to test in small fragments. The code is littered with file-tracking code that's unrelated to the parsing itself. The parser performs some desugaring steps before the desugarer, for example in the case of pi-types or sigmas. All this complexity makes any changes to the parser fraught with unexpected challenges. Cleaning this up is going to take some time and we need to be mindful of doing it in a way that enables our other goals.
• While it is not directly related to the parser, the desugaring steps and resugaring steps have their own problems that I think should be adressed as part of any efforts to improve the parser: generating provably parsable code. The issue is that there is no way to prove that a fragment of code can be parsed, desugared and resugared in a way that it can be parsed again. In code, we want to have the following lemma: (code : String) -> parse code >>= desugar >>= resugar >>= print ~~~ code where ~~~ is a notion of parsing equivalence where both sides must both parse or fail with a similar error. Additionally we want the internal trees to be the same: (tree : PTerm) -> tree >>= desugar >>= resugar === Just tree
• One very visible area where parser, desugaring and resugaring fail is in location tracking. Often, location is lost, inaccurate or wrong, essentialy because location tracking needs to be carefully threaded by the programming at each of those steps and as a programmer there is no way to ensure that the assumption we make will hold after multiple passes of tree transformation, least of which are the desugarer and resugarer, but go much deeper with features like proof search, with clauses, elaborator reflection, and more. Because elaborated code is much harder to deal with, and further away from the parser, I think they are out of scope for this specific project. But desugared code should definitely be aware of the parser's capabilities.

Depending on the timeline to re-write the parser (either all at once or in chunks), I feel that it might make the most sense/provide the best return on investment to spend the time/effort to utilize @stefan-hoeck's idris2-parser library. The potential performance improvement alone may be well worth the effort.

There's also an archived attempt at a tree-sitter parser at https://github.com/gwerbin/tree-sitter-idris2 and an active one at https://github.com/kayhide/tree-sitter-idris that seems to be useful for my purposes (program reduction).

I'm most interested in a parser that can produce partial results, in case of an error, and that can produce a concrete syntax tree. I know tree-sitter does the former, but I haven't investigated its ability to do the latter well. These abilities would be useful for a code formatter, too.

I'd love to support a tree-sitter implementation, but this complicated the manner in which Idris is currently bootstrapped, since it would introduce a dependency on a C library.

It might be better to implement a parser library in Idris which produces incremental and streaming results and has error correction.

That said, the implementation effort would be significantly more complicated than simply reusing tree sitter.