chore: generalize parser kind detection

src/Lean/ParserCompiler.lean

@@ -37,12 +37,17 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
   let e ← whnfCore e
   if e matches Expr.lam .. then
     lambdaLetTelescope e fun _ e => parserNodeKind? e
-  else if e.isAppOfArity ``nodeWithAntiquot 4 || e.isAppOfArity ``withAntiquot 2 || e.isAppOfArity ``withCache 2 then
-    parserNodeKind? (e.getArg! 1)
   else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then
     reduceEval? (e.getArg! 0)
-  else
-    return none
+  else if e.isAppOfArity ``withAntiquot 2 then
+    parserNodeKind? (e.getArg! 1)
+  else forallTelescope (← inferType e.getAppFn) fun params _ => do
+    let lctx ← getLCtx
+    -- if there is exactly one parameter of type `Parser`, search there
+    if let [(i, _)] := params.toList.enum.filter (lctx.getFVar! ·.2 |>.type.isConstOf ``Parser) then
+      parserNodeKind? (e.getArg! i)
+    else
+      return none
 
 section
 open Meta