feat: try to improve weird error message

@Kha Before this commit, we were producing the error "expected command" at the `let` token
```lean
check id let x := 1; x
```
The new error is "expected command, but found term; this error may be
due to parsing precedence levels, consider parenthesizing the term".

The example above looks artificial, but it will happen all the time as
users start to define their own notation.

src/Lean/Parser/Basic.lean

@@ -88,6 +88,7 @@ input.get (input.next pos)
    Note that nothing prevents users from using a higher precedence, but we strongly
    discourage them from doing it. -/
 def maxPrec : Nat := 1024
+def leadPrec := maxPrec - 1
 
 abbrev Token := String
 
@@ -351,6 +352,13 @@ instance hasAndthen : HasAndthen Parser :=
 { info := nodeInfo n p.info,
   fn   := nodeFn n p.fn }
 
+def errorFn (msg : String) : ParserFn :=
+fun _ s => s.mkUnexpectedError msg
+
+@[inline] def error (msg : String) : Parser :=
+{ info := epsilonInfo,
+  fn   := errorFn msg }
+
 /- Succeeds if `c.prec <= prec` -/
 def checkPrecFn (prec : Nat) : ParserFn :=
 fun c s =>
@@ -399,14 +407,14 @@ checkPrec prec >> trailingNodeAux n p
 @[inline] def group (p : Parser) : Parser :=
 node nullKind p
 
-def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : Nat) : ParserState :=
+def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : Nat) (mergeErrors : Bool) : ParserState :=
 match s with
 | ⟨stack, pos, cache, some error2⟩ =>
-  if pos == iniPos then ⟨stack, pos, cache, some (error1.merge error2)⟩
+  if pos == iniPos then ⟨stack, pos, cache, some (if mergeErrors then error1.merge error2 else error2)⟩
   else s
 | other => other
 
-@[inline] def orelseFn (p q : ParserFn) : ParserFn
+@[inline] def orelseFnCore (p q : ParserFn) (mergeErrors : Bool) : ParserFn
 | c, s =>
   let iniSz  := s.stackSize;
   let iniPos := s.pos;
@@ -414,11 +422,14 @@ match s with
   match s.errorMsg with
   | some errorMsg =>
     if s.pos == iniPos then
-      mergeOrElseErrors (q c (s.restore iniSz iniPos)) errorMsg iniPos
+      mergeOrElseErrors (q c (s.restore iniSz iniPos)) errorMsg iniPos mergeErrors
     else
       s
   | none => s
 
+@[inline] def orelseFn (p q : ParserFn) : ParserFn :=
+orelseFnCore p q true
+
 @[noinline] def orelseInfo (p q : ParserInfo) : ParserInfo :=
 { collectTokens := p.collectTokens ∘ q.collectTokens,
   collectKinds  := p.collectKinds ∘ q.collectKinds,

src/Lean/Parser/Module.lean

@@ -70,6 +70,12 @@ match s.errorMsg with
 | some _ => pos + 1
 | none   => s.pos
 
+def topLevelCommandParserFn : ParserFn :=
+orelseFnCore
+  commandParser.fn
+  (andthenFn (lookaheadFn termParser.fn) (errorFn "expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term"))
+  false /- do not merge errors -/
+
 partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
 | s@{ pos := pos, recovering := recovering }, messages =>
   if inputCtx.input.atEnd pos then
@@ -78,7 +84,7 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP
     let c  := mkParserContext env inputCtx;
     let s  := { cache := initCacheForInput c.input, pos := pos : ParserState };
     let s  := whitespace c s;
-    let s  := (commandParser : Parser).fn c s;
+    let s  := topLevelCommandParserFn c s;
     match s.errorMsg with
     | none =>
       let stx := s.stxStack.back;

src/Lean/Parser/Term.lean

@@ -41,8 +41,6 @@ checkPrec prec >> unicodeSymbol sym asciiSym >> termParser (prec+1)
 def infixL (sym : String) (prec : Nat) : TrailingParser :=
 checkPrec prec >> symbol sym >> termParser (prec+1)
 
-def leadPrec := maxPrec - 1
-
 /- Built-in parsers -/
 
 @[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.indentedNonEmptySeq
@@ -52,8 +50,8 @@ def leadPrec := maxPrec - 1
 @[builtinTermParser] def num : Parser := checkPrec maxPrec >> numLit
 @[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit
 @[builtinTermParser] def char : Parser := checkPrec maxPrec >> charLit
-@[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
-@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
+@[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> levelParser maxPrec)
+@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> levelParser maxPrec)
 @[builtinTermParser] def prop := parser! "Prop"
 @[builtinTermParser] def hole := parser! "_"
 @[builtinTermParser] def syntheticHole := parser! "?" >> (ident <|> hole)
@@ -135,7 +133,7 @@ def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPre
 def optExprPrecedence := optional (try ":" >> termParser maxPrec)
 @[builtinTermParser] def «parser!»  := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
 @[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser
-@[builtinTermParser] def borrowed   := parser! "@&" >> termParser (maxPrec - 1)
+@[builtinTermParser] def borrowed   := parser! "@&" >> termParser leadPrec
 @[builtinTermParser] def quotedName := parser! nameLit
 -- NOTE: syntax quotations are defined in Init.Lean.Parser.Command
 @[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts

tests/lean/precissues.lean

@@ -14,6 +14,8 @@ def f (x : Nat) (g : Nat → Nat) := g x
 
 #check id have True from ⟨⟩; this -- should fail
 
+#check id let x := 10; x
+
 #check 1
 
 #check id (have True from ⟨⟩; this)

tests/lean/precissues.lean.expected.out

@@ -4,7 +4,9 @@ f 1 fun (x : Nat) => x : Nat
 0 : Nat
 f 1 fun (x : Nat) => x : Nat
 id : ?m → ?m
-precissues.lean:15:10: error: expected command
+precissues.lean:15:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
+id : ?m → ?m
+precissues.lean:17:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
 1 : Nat
 id ((fun (this : True) => this) True.intro) : True
 0 = (fun (this : Nat) => this) 1 : Prop