fix: two functions with the same name in a where/let rec block (#…

…4562)

closes #4547

src/Lean/Elab/LetRec.lean

@@ -30,20 +30,24 @@ structure LetRecView where
 
 /-  group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
 private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
-  let decls ← letRec[1][0].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
+  let mut decls : Array LetRecDeclView := #[]
+  for attrDeclStx in letRec[1][0].getSepArgs do
     let docStr? ← expandOptDocComment? attrDeclStx[0]
     let attrOptStx := attrDeclStx[1]
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
-    else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
+    else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
+      if decls.any fun decl => decl.declName == declName then
+        withRef declId do
+          throwError "'{declName}' has already been declared"
       checkNotAlreadyDeclared declName
       applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
       addDocString' declName docStr?
@@ -62,8 +66,10 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       else
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
       let termination ← WF.elabTerminationHints ⟨attrDeclStx[3]⟩
-      pure { ref := declId, attrs, shortDeclName, declName, binderIds, type, mvar, valStx,
-             termination : LetRecDeclView }
+      decls := decls.push {
+        ref := declId, attrs, shortDeclName, declName,
+        binderIds, type, mvar, valStx, termination
+      }
     else
       throwUnsupportedSyntax
   return { decls, body := letRec[3] }

tests/lean/run/4547.lean

@@ -0,0 +1,19 @@
+/--
+error: 'f.go' has already been declared
+-/
+#guard_msgs in
+def f (x : Nat) : Nat :=
+  go x
+where
+  go (x : Nat) : Nat := x
+  go (x : Nat) : Nat := x + 1
+
+/--
+error: 'g.go' has already been declared
+-/
+#guard_msgs in
+def g (x : Nat) : Nat :=
+  go x
+where
+  go (x : Nat) : Nat := x
+  go (x : Nat) (y : Nat) : Nat := x + 1