From 929aafa4c807943f9fbcf92cc53fd1775c4eaf6c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Jan 2022 12:06:28 -0800
Subject: [PATCH] fix: generate an error if declaration name clashes with
 variable name

closes #799
---
 src/Lean/Elab/Command.lean       |  6 +++++-
 src/Lean/Elab/MutualDef.lean     |  2 +-
 src/Lean/Elab/Term.lean          |  8 ++++++++
 tests/lean/799.lean              | 13 +++++++++++++
 tests/lean/799.lean.expected.out |  5 +++++
 5 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/799.lean
 create mode 100644 tests/lean/799.lean.expected.out

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 65a7836e58..0798af61fa 100644
--- a/src/Lean/Elab/Command.lean
+++ b/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
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 814dfa9feb..84e8b9741b 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/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 <|
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 1c8e813172..8233b3ba8c 100644
--- a/src/Lean/Elab/Term.lean
+++ b/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
diff --git a/tests/lean/799.lean b/tests/lean/799.lean
new file mode 100644
index 0000000000..ec606bb1a8
--- /dev/null
+++ b/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
diff --git a/tests/lean/799.lean.expected.out b/tests/lean/799.lean.expected.out
new file mode 100644
index 0000000000..1f0068ad78
--- /dev/null
+++ b/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