fix: generate an error if declaration name clashes with variable name

closes #799

src/Lean/Elab/Command.lean

@@ -435,7 +435,11 @@ def addUnivLevel (idStx : Syntax) : CommandElabM Unit := withRef idStx do
 def expandDeclId (declId : Syntax) (modifiers : Modifiers) : CommandElabM ExpandDeclIdResult := do
   let currNamespace ← getCurrNamespace
   let currLevelNames ← getLevelNames
-  Lean.Elab.expandDeclId currNamespace currLevelNames declId modifiers
+  let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
+  for id in (← getScope).varDecls.concatMap getBracketedBinderIds do
+    if id == r.shortName then
+      throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
+  return r
 
 end Elab.Command
 

src/Lean/Elab/MutualDef.lean

@@ -102,7 +102,7 @@ private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHe
   let mut headers := #[]
   for view in views do
     let newHeader ← withRef view.ref do
-      let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
+      let ⟨shortDeclName, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
       addDeclarationRanges declName view.ref
       applyAttributesAt declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration
       withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|

src/Lean/Elab/Term.lean

@@ -12,6 +12,7 @@ import Lean.Meta.CollectMVars
 import Lean.Meta.Coe
 import Lean.Hygiene
 import Lean.Util.RecDepth
+
 import Lean.Elab.Log
 import Lean.Elab.Config
 import Lean.Elab.Level
@@ -20,6 +21,7 @@ import Lean.Elab.AutoBound
 import Lean.Elab.InfoTree
 import Lean.Elab.Open
 import Lean.Elab.SetOption
+import Lean.Elab.DeclModifiers
 
 namespace Lean.Elab.Term
 structure Context where
@@ -1574,6 +1576,12 @@ def withoutPostponingUniverseConstraints (x : TermElabM α) : TermElabM α := do
     setPostponed postponed
     throw ex
 
+def expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) : TermElabM ExpandDeclIdResult := do
+  let r ← Elab.expandDeclId currNamespace currLevelNames declId modifiers
+  if (← read).sectionVars.contains r.shortName then
+    throwError "invalid declaration name '{r.shortName}', there is a section variable with the same name"
+  return r
+
 end Term
 
 open Term in

tests/lean/799.lean

@@ -0,0 +1,13 @@
+section
+variable (p : Prop)
+def p := 10 -- Error
+#check p
+
+namespace Foo
+def p := true -- Error
+#check p
+end Foo
+end
+
+def p := 10
+#check p

tests/lean/799.lean.expected.out

@@ -0,0 +1,5 @@
+799.lean:3:0-3:11: error: invalid declaration name 'p', there is a section variable with the same name
+p : Prop
+799.lean:7:0-7:13: error: invalid declaration name 'p', there is a section variable with the same name
+p : Prop
+p : Nat