feat: report error on ambiguous export and open commands

This commit improves the fix for issue #1224

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

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

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

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]