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

@@ -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.

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)

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)

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

tests/lean/protectedAlias.lean.expected.out

@@ -0,0 +1,2 @@
+Ex.double : Nat → Nat
+protectedAlias.lean:9:7-9:13: error: unknown identifier 'double'