`private` and `protected` interact strangely

[digama0]

import Lean
open Lean
macro "test" x:ident : command => do
  let [(name, _)] ← Macro.resolveGlobalName x.getId | Macro.throwUnsupported
  `(protected theorem $(mkIdent (name.mkStr "ext")):ident : True := trivial)

inductive A : Type
test A
#print A.ext -- ok

private inductive B : Type
test B 
-- invalid scope
-- protected declarations must be in a namespace
-- invalid 'end', insufficient scopes
#print B.ext -- fail

namespace Ns
private inductive C : Type
test C 
-- invalid scope
-- invalid 'end', insufficient scopes
#print C.ext -- fail, but...
#print Ns.ext -- ok

This is a simplified version of an issue with the ext attribute from mathlib, which attempts to create a protected declaration in the same namespace as the input type name. (It would also be nice to implement this as a macro; I think I know how to work around this as an elab.) When the type is private, this essentially amounts to elaborating a command like:

protected theorem _private.Test.0.B.ext : True := trivial

and the declaration parser gets very confused by this identifier. Ideally, this would just work and create a private declaration which is also protected, in the sense that you can refer to it by the name B.ext but not ext. I believe the knock-on error about invalid scope is because the declaration elaborator expanded to a namespace 0 which isn't valid.

[leodemoura]

I have a workaround for this issue (see commits above), but I think we should not merge them into master. It silently ignores the protected annotation and treats it as a private one if isPrivateName name is true. The test command above also looks fishy. For example, suppose we write

namespace Bla.Boo
inductive Foo : Type
test Foo
end Bla.Boo

It will generate the declaration

Bla.Boo.Bla.Boo.Foo.ext

[leodemoura]

We can avoid the issue by writing test as follows

import Lean
open Lean
macro "test" x:ident : command => do
  let [(name, _)] ← Macro.resolveGlobalName x.getId | Macro.throwUnsupported
  let name := privateToUserName? name |>.getD name
  `(protected theorem $(mkIdent (`_root_ ++ (name.mkStr "ext"))):ident : True := trivial)

inductive A : Type
test A
#print A.ext

private inductive B : Type
test B
#print B.ext

namespace Ns
private inductive C : Type
test C
#print C.ext
end Ns

namespace Bla.Boo
inductive Foo : Type
test Foo
#print Foo.ext

[leodemoura]

Note that in the example above B.ext is not a private declaration, but a protected one. If we want to force B.ext to be private when B is private, then we can write test as follows.

import Lean
open Lean
macro "test" x:ident : command => do
  let [(name, _)] ← Macro.resolveGlobalName x.getId | Macro.throwUnsupported
  if let some name := privateToUserName? name then
    `(private theorem $(mkIdent (`_root_ ++ (name.mkStr "ext"))):ident : True := trivial)
  else
    `(protected theorem $(mkIdent (`_root_ ++ (name.mkStr "ext"))):ident : True := trivial)

inductive A : Type
test A
#print A.ext

private inductive B : Type
set_option trace.Elab.definition true in
test B
#print B.ext

namespace Ns
private inductive C : Type
set_option trace.Elab.definition true in
test C
#print Ns.C.ext
end Ns

namespace Bla.Boo
inductive Foo : Type
test Foo
#print Foo.ext

[leodemoura]

@digama0 I am planning to close this issue because the solutions above look satisfactory to me.

[leodemoura]

Dev meeting summary: use macro scopes for encoding private names. We will need to adapt the name resolution.