fix: app parser

cc @kha

src/Init/Lean/Parser/Parser.lean

@@ -1399,6 +1399,17 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par
         let s := mkTrailingResult s iniSz;
         trailingLoop s
 
+def checkTokenLBPFn : ParserFn :=
+fun c s =>
+  let left := s.stxStack.back;
+  let (s, lbp) := currLbp left c s;
+  if c.rbp < lbp then s
+  else s.mkUnexpectedError "unexpected token"
+
+def checkTokenLBP : Parser :=
+{ info := epsilonInfo,
+  fn   := checkTokenLBPFn }
+
 /--
   Implements a recursive precedence parser according to Pratt's algorithm.
 

src/Init/Lean/Parser/Term.lean

@@ -124,7 +124,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 @[builtinTermParser] def uminus := parser! "-" >> termParser 100
 
 def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
-@[builtinTermParser] def app      := tparser! many1 (namedArgument <|> termParser appPrec)
+@[builtinTermParser] def app      := tparser! many1 (namedArgument <|> (checkTokenLBP >> termParser appPrec))
 
 def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort)
 @[builtinTermParser] def sortApp  := tparser! checkIsSort >> levelParser appPrec

tests/lean/appParserIssue.lean

@@ -0,0 +1,13 @@
+def f (x : Nat) (g : Nat → Nat) := g x
+
+new_frontend
+
+#check f 1 fun x => x   -- should fail
+#check f 1 (fun x => x) -- should work
+#check f 1 $ fun x => x -- should work
+
+syntax "foo" term:max term:max : term
+macro_rules `(foo $x $y) => `(f $x $y)
+
+#check foo 1 fun x => x   -- should fail?
+#check foo 1 (fun x => x) -- should work

tests/lean/appParserIssue.lean.expected.out

@@ -0,0 +1,6 @@
+f 1 : (Nat → Nat) → Nat
+appParserIssue.lean:5:11: error: expected command
+f 1 (λ (x : Nat), x) : Nat
+f 1 (λ (x : Nat), x) : Nat
+f 1 (λ (x : Nat), x) : Nat
+f 1 (λ (x : Nat), x) : Nat