fix: private names

@Kha I tried to fix a few issues with private names. The new test
tries to cover them. If you have more, please create an issue.

1- Scoping. A private declaration should shadow one in a previous scope.
2- We should not be able to define the same `private` in the same
module more than once.
   ```
   private def x := 10
   private def x := "hello" -- should produce error here
   ```
3- Dot-notation should work with private declarations in the module
where they were defined.
4- The following should work
   ```
   namespace N
   private def x := 10
   end N
   #check N.x
   ```
5- The following should **not** work
   ```
   def y := 10
   private def y := "hello" -- produce error

   private def z := 10
   def z := "hello" -- produce error
   ```
   BTW, I am happy to change this behavior. I just mimicked C's
   behavior for `static`.

It is not clear whether the following should work or not.
```
    namespace N
      private def b := 10
    end N
    open N
    #check b
```

src/Init/Lean/Elab/App.lean

@@ -321,8 +321,13 @@ match eType.getAppFn, lval with
   let searchEnv (fullName : Name) : TermElabM LValResolution := do {
     match env.find? fullName with
     | some _ => pure $ LValResolution.const structName fullName
-    | none   => throwLValError ref e eType $
-      "invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ fullName ++ "'"
+    | none   =>
+      let fullNamePrv := mkPrivateName env fullName;
+      match env.find? fullNamePrv with
+      | some _ => pure $ LValResolution.const structName fullNamePrv
+      | none   =>
+        throwLValError ref e eType $
+        "invalid field notation, '" ++ fieldName ++ "' is not a valid \"field\" because environment does not contain '" ++ fullName ++ "'"
   };
   -- search local context first, then environment
   let searchCtx : Unit → TermElabM LValResolution := fun _ => do {

src/Init/Lean/Elab/DeclModifiers.lean

@@ -110,16 +110,22 @@ let declName := currNamespace ++ atomicName;
 match modifiers.visibility with
 | Visibility.private => do
   env ← getEnv;
-  let (env, declName) := mkPrivateName env declName;
-  setEnv env;
-  -- TODO: alias?
-  pure declName
+  pure $ mkPrivateName env declName
 | _                  => pure declName
 
 def checkNotAlreadyDeclared (ref : Syntax) (declName : Name) : CommandElabM Unit := do
 env ← getEnv;
 when (env.contains declName) $
-  throwError ref ("'" ++ declName ++ "' has already been declared")
+  match privateToUserName? declName with
+  | none          => throwError ref ("'" ++ declName ++ "' has already been declared")
+  | some declName => throwError ref ("private declaration '" ++ declName ++ "' has already been declared");
+when (env.contains (mkPrivateName env declName)) $
+  throwError ref ("a private declaration '" ++ declName ++ "' has already been declared");
+match privateToUserName? declName with
+| none => pure ()
+| some declName =>
+  when (env.contains declName) $
+    throwError ref ("a non-private declaration '" ++ declName ++ "' has already been declared")
 
 def applyAttributes (ref : Syntax) (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : CommandElabM Unit :=
 attrs.forM $ fun attr => do

src/Init/Lean/Elab/ResolveName.lean

@@ -34,10 +34,15 @@ n.replacePrefix rootNamespace Name.anonymous
 
 /- 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;
+let resolvedId    := ns ++ id;
+let resolvedIds   := getAliases env resolvedId;
 if env.contains resolvedId && (!id.isAtomic || !isProtected env resolvedId) then resolvedId :: resolvedIds
-else resolvedIds
+else
+  -- Check whether environment contains the private version. That is, `_private.<module_name>.ns.id`.
+  let resolvedIdPrv := mkPrivateName env resolvedId;
+  if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds
+  else resolvedIds
+
 
 /- Check surrounding namespaces -/
 private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name
@@ -52,7 +57,13 @@ private def resolveExact (env : Environment) (id : Name) : Option Name :=
 if id.isAtomic then none
 else
   let resolvedId := id.replacePrefix rootNamespace Name.anonymous;
-  if env.contains resolvedId then some resolvedId else none
+  if env.contains resolvedId then some resolvedId
+  else
+    -- We also allow `_root` when accessing private declarations.
+    -- If we change our minds, we should just replace `resolvedId` with `id`
+    let resolvedIdPrv := mkPrivateName env resolvedId;
+    if env.contains resolvedIdPrv then some resolvedIdPrv
+    else none
 
 /- Check open namespaces -/
 private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name

src/Init/Lean/Modifiers.lean

@@ -43,17 +43,20 @@ constant privateExt : EnvExtension Nat := arbitrary _
 def privateHeader : Name := `_private
 
 @[export lean_mk_private_prefix]
-def mkPrivatePrefix (env : Environment) : Environment × Name :=
+def mkUniquePrivatePrefix (env : Environment) : Environment × Name :=
 let idx := privateExt.getState env;
 let p   := mkNameNum (privateHeader ++ env.mainModule) idx;
 let env := privateExt.setState env (idx+1);
 (env, p)
 
 @[export lean_mk_private_name]
-def mkPrivateName (env : Environment) (n : Name) : Environment × Name :=
-let (env, p) := mkPrivatePrefix env;
+def mkUniquePrivateName (env : Environment) (n : Name) : Environment × Name :=
+let (env, p) := mkUniquePrivatePrefix env;
 (env, p ++ n)
 
+def mkPrivateName (env : Environment) (n : Name) : Name :=
+mkNameNum (privateHeader ++ env.mainModule) 0 ++ n
+
 def isPrivateName : Name → Bool
 | n@(Name.str p _ _) => n == privateHeader || isPrivateName p
 | Name.num p _ _     => isPrivateName p
@@ -68,7 +71,7 @@ private def privateToUserNameAux : Name → Name
 | _              => Name.anonymous
 
 @[export lean_private_to_user_name]
-def privateToUserName (n : Name) : Option Name :=
+def privateToUserName? (n : Name) : Option Name :=
 if isPrivateName n then privateToUserNameAux n
 else none
 

tests/lean/private.lean

@@ -0,0 +1,68 @@
+new_frontend
+
+-- Issue 1
+def foo := 10
+
+def f (x : Nat) := x + x
+
+namespace Bla
+
+private def foo := "hello"
+
+#check foo == "world" -- `foo` resolves to private `Bla.foo`
+
+private def foo : Float := 1.0 -- should produce error like in other programming languages
+
+end Bla
+
+#check foo == 0
+
+#check Bla.foo
+
+-- Issue 2
+namespace Boo
+
+def boo := 100
+
+namespace Bla
+
+private def boo := "hello"
+
+#check boo == "world" -- resolving to `Boo.Bla.boo` as expected
+#check boo ++ "world" -- should work
+
+end Bla
+
+#check Bla.boo == "world"
+#check boo == 100
+
+end Boo
+
+#check Boo.Bla.boo == "world"
+#check Boo.boo == 100
+
+/-
+Should the following work?
+```
+    namespace N
+      private def b := 10
+    end N
+    open N
+    #check b
+```
+-/
+
+-- Issue 3
+private def Nat.mul10 (x : Nat) := x * 10
+def x := 10
+
+#check x.mul10 -- dot-notation should work with local private declarations
+
+
+-- Issue 4
+
+def y := 10
+private def y := "hello" -- produce error
+
+private def z := 10
+def z := "hello" -- produce error

tests/lean/private.lean.expected.out

@@ -0,0 +1,13 @@
+Bla.foo=="world" : Bool
+private.lean:14:8: error: private declaration 'Bla.foo' has already been declared
+foo==0 : Bool
+Bla.foo : String
+Boo.Bla.boo=="world" : Bool
+Boo.Bla.boo++"world" : String
+Boo.Bla.boo=="world" : Bool
+Boo.boo==100 : Bool
+Boo.Bla.boo=="world" : Bool
+Boo.boo==100 : Bool
+Nat.mul10 x : Nat
+private.lean:65:8: error: a non-private declaration 'y' has already been declared
+private.lean:68:0: error: a private declaration 'z' has already been declared