From 5901fef43abe90a3ce659f028cf905e7a2b100ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 27 Jun 2022 13:56:14 -0700
Subject: [PATCH] feat: protected aliases

See message: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/287633118
---
 RELEASES.md                                 | 13 +++++++++++++
 src/Lean/Elab/App.lean                      |  3 ++-
 src/Lean/ResolveName.lean                   | 17 +++++++++++++----
 tests/lean/protectedAlias.lean              |  9 +++++++++
 tests/lean/protectedAlias.lean.expected.out |  2 ++
 5 files changed, 39 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/protectedAlias.lean
 create mode 100644 tests/lean/protectedAlias.lean.expected.out

diff --git a/RELEASES.md b/RELEASES.md
index 3605ded476..f09f9517fd 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,19 @@
 Unreleased
 ---------
 
+* Aliases of protected definitions are protected too. Example:
+  ```lean
+  protected def Nat.double (x : Nat) := 2*x
+
+  namespace Ex
+  export Nat (double) -- Add alias Ex.double for Nat.double
+  end Ex
+
+  open Ex
+  #check Ex.double -- Ok
+  #check double -- Error, `Ex.double` is alias for `Nat.double` which is protected
+  ```
+
 * Use `IO.getRandomBytes` to initialize random seed for `IO.rand`. See discussion at [this PR](https://github.com/leanprover/lean4-samples/pull/2).
 
 * Improve dot notation and aliases interaction. See discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185) for additional details.
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index f88a37e971..ca43debd92 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -552,7 +552,8 @@ private partial def findMethod? (env : Environment) (structName fieldName : Name
 -/
 private def findMethodAlias? (env : Environment) (structName fieldName : Name) : Option (Name × Name) :=
   let fullName := structName ++ fieldName
-  let aliasesCandidates := getAliases env fullName |>.filterMap fun alias =>
+  -- We never skip `protected` aliases when resolving dot-notation.
+  let aliasesCandidates := getAliases env fullName (skipProtected := false) |>.filterMap fun alias =>
     match alias.eraseSuffix? fieldName with
     | none => none
     | some structName' => some (structName', alias)
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 84525a46cd..a713d9c7c7 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -36,10 +36,18 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia
 def getAliasState (env : Environment) : AliasState :=
   aliasExtension.getState env
 
-def getAliases (env : Environment) (a : Name) : List Name :=
+/-
+  Retrieve aliases for `a`. If `skipProtected` is `true`, then the resulting list only includes
+  declarations that are not marked as `proctected`.
+-/
+def getAliases (env : Environment) (a : Name) (skipProtected : Bool) : List Name :=
   match aliasExtension.getState env |>.find? a with
   | none    => []
-  | some es => es
+  | some es =>
+    if skipProtected then
+      es.filter (!isProtected env ·)
+    else
+      es
 
 -- slower, but only used in the pretty printer
 def getRevAliases (env : Environment) (e : Name) : List Name :=
@@ -51,7 +59,8 @@ namespace ResolveName
 /- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/
 private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name :=
   let resolvedId    := ns ++ id
-  let resolvedIds   := getAliases env resolvedId
+  -- We ignore protected aliases if `id` is atomic.
+  let resolvedIds   := getAliases env resolvedId (skipProtected := id.isAtomic)
   if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then
     resolvedId :: resolvedIds
   else
@@ -122,7 +131,7 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
           let idPrv       := mkPrivateName env id
           let resolvedIds := if env.contains idPrv then [idPrv] ++ resolvedIds else resolvedIds
           let resolvedIds := resolveOpenDecls env id openDecls resolvedIds
-          let resolvedIds := getAliases env id ++ resolvedIds
+          let resolvedIds := getAliases env id (skipProtected := id.isAtomic) ++ resolvedIds
           match resolvedIds with
           | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
           | []     => loop p (s::projs)
diff --git a/tests/lean/protectedAlias.lean b/tests/lean/protectedAlias.lean
new file mode 100644
index 0000000000..cd2781c720
--- /dev/null
+++ b/tests/lean/protectedAlias.lean
@@ -0,0 +1,9 @@
+protected def Nat.double (x : Nat) := 2*x
+
+namespace Ex
+export Nat (double) -- Add alias Ex.double for Nat.double
+end Ex
+
+open Ex
+#check Ex.double -- Ok
+#check double -- Error, `Ex.double` is alias for `Nat.double` which is protected
diff --git a/tests/lean/protectedAlias.lean.expected.out b/tests/lean/protectedAlias.lean.expected.out
new file mode 100644
index 0000000000..81af85f7d8
--- /dev/null
+++ b/tests/lean/protectedAlias.lean.expected.out
@@ -0,0 +1,2 @@
+Ex.double : Nat → Nat
+protectedAlias.lean:9:7-9:13: error: unknown identifier 'double'