From 52a0de00e4aa6d9cc4cb755f49308186da7fe27a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2022 09:55:39 -0700
Subject: [PATCH] feat: report error on ambiguous `export` and `open` commands

This commit improves the fix for issue #1224
---
 src/Lean/Elab/BuiltinCommand.lean             | 10 +----
 src/Lean/Elab/Open.lean                       | 37 ++++++++++++++-----
 tests/lean/ambiguousOpenExport.lean           | 11 ++++++
 .../ambiguousOpenExport.lean.expected.out     |  2 +
 4 files changed, 42 insertions(+), 18 deletions(-)
 create mode 100644 tests/lean/ambiguousOpenExport.lean
 create mode 100644 tests/lean/ambiguousOpenExport.lean.expected.out

diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index e49648db2d..acaea509d3 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -128,14 +128,8 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   let mut aliases := #[]
   for idStx in ids do
     let id := idStx.getId
-    let mut exs := #[]
-    for ns in nss do
-      try
-        let declName ← resolveOpenDeclId ns idStx
-        aliases := aliases.push (currNamespace ++ id, declName)
-      catch ex => exs := exs.push ex
-    if exs.size == nss.length then
-      withRef idStx do if exs.size == 1 then throw exs[0] else throwErrorWithNestedErrors "failed to export" exs
+    let declName ← resolveNameUsingNamespaces nss idStx
+    aliases := aliases.push (currNamespace ++ id, declName)
   modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 }
 
 @[builtinCommandElab «open»] def elabOpen : CommandElab := fun n => do
diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean
index 5eda17c77c..f77c61edab 100644
--- a/src/Lean/Elab/Open.lean
+++ b/src/Lean/Elab/Open.lean
@@ -46,19 +46,32 @@ private def elabOpenScoped (n : Syntax) : M (m:=m) Unit :=
     for ns in (← resolveNamespace ns.getId) do
     activateScoped ns
 
+private def resolveNameUsingNamespacesCore (nss : List Name) (idStx : Syntax) : M (m:=m) Name := do
+  let mut exs := #[]
+  let mut result := #[]
+  for ns in nss do
+    try
+      let declName ← resolveId ns idStx
+      result := result.push declName
+    catch ex =>
+      exs := exs.push ex
+  if exs.size == nss.length then
+    withRef idStx do
+      if exs.size == 1 then
+        throw exs[0]
+      else
+        throwErrorWithNestedErrors "failed to open" exs
+  if result.size == 1 then
+    return result[0]
+  else
+    withRef idStx do throwError "ambiguous identifier '{idStx.getId}', possible interpretations: {result.map mkConst}"
+
 -- `open` id `(` id+ `)`
 private def elabOpenOnly (n : Syntax) : M (m:=m) Unit := do
   let nss ← resolveNamespace n[0].getId
   for idStx in n[2].getArgs do
-    let mut exs := #[]
-    for ns in nss do
-      try
-        let declName ← resolveId ns idStx
-        addOpenDecl (OpenDecl.explicit idStx.getId declName)
-      catch ex =>
-        exs := exs.push ex
-    if exs.size == nss.length then
-      withRef idStx do if exs.size == 1 then throw exs[0] else throwErrorWithNestedErrors "failed to open" exs
+    let declName ← resolveNameUsingNamespacesCore nss idStx
+    addOpenDecl (OpenDecl.explicit idStx.getId declName)
 
 -- `open` id `hiding` id+
 private def elabOpenHiding (n : Syntax) : M (m:=m) Unit := do
@@ -97,8 +110,12 @@ def resolveOpenDeclId [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name
   StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
     OpenDecl.resolveId ns idStx
 
+def resolveNameUsingNamespaces [MonadResolveName m] (nss : List Name) (idStx : Syntax) : m Name := do
+  StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
+    resolveNameUsingNamespacesCore nss idStx
+
 end OpenDecl
 
-export OpenDecl (elabOpenDecl resolveOpenDeclId)
+export OpenDecl (elabOpenDecl resolveOpenDeclId resolveNameUsingNamespaces)
 
 end Lean.Elab
diff --git a/tests/lean/ambiguousOpenExport.lean b/tests/lean/ambiguousOpenExport.lean
new file mode 100644
index 0000000000..905b2484e8
--- /dev/null
+++ b/tests/lean/ambiguousOpenExport.lean
@@ -0,0 +1,11 @@
+inductive Foo.C where
+  | mk
+
+inductive Bla.C where
+  | mk
+
+open Foo Bla
+
+open C (mk) -- Error
+
+export C (mk) -- Error
diff --git a/tests/lean/ambiguousOpenExport.lean.expected.out b/tests/lean/ambiguousOpenExport.lean.expected.out
new file mode 100644
index 0000000000..55a371aeab
--- /dev/null
+++ b/tests/lean/ambiguousOpenExport.lean.expected.out
@@ -0,0 +1,2 @@
+ambiguousOpenExport.lean:9:8-9:10: error: ambiguous identifier 'mk', possible interpretations: [Bla.C.mk, Foo.C.mk]
+ambiguousOpenExport.lean:11:10-11:12: error: ambiguous identifier 'mk', possible interpretations: [Bla.C.mk, Foo.C.mk]