checkpoint

This is broken.
We need special treatment during name resolution and declaration
elaboration.
Parts of the code base are making the assumption that private names
and macro scopes are different things.

src/Init/Prelude.lean

@@ -3461,17 +3461,17 @@ instance : BEq Name where
 /--
 Append two hierarchical names. Example:
 ```lean
-`Lean.Meta ++ `Tactic.simp
+appendCore `Lean.Meta `Tactic.simp
 ```
 return `Lean.Meta.Tactic.simp`
--/
-protected def append : Name → Name → Name
-  | n, anonymous => n
-  | n, str p s => Name.mkStr (Name.append n p) s
-  | n, num p d => Name.mkNum (Name.append n p) d
 
-instance : Append Name where
-  append := Name.append
+This function does not have special support for macro scopes.
+See `Name.append`.
+-/
+def appendCore : Name → Name → Name
+  | n, .anonymous => n
+  | n, .str p s => .str (appendCore n p) s
+  | n, .num p d => .num (appendCore n p) d
 
 end Name
 
@@ -3985,8 +3985,10 @@ produce different identifiers.
 abbrev MacroScope := Nat
 /-- Macro scope used internally. It is not available for our frontend. -/
 def reservedMacroScope := 0
-/-- First macro scope available for our frontend -/
-def firstFrontendMacroScope := hAdd reservedMacroScope 1
+/-- Macro scope used to encode private names. -/
+def privateMacroScope := 1
+/-- First macro scope available for our frontend. -/
+def firstFrontendMacroScope := hAdd privateMacroScope 1
 
 /--
 A `MonadRef` is a monad that has a `ref : Syntax` in the read-only state.
@@ -4146,7 +4148,7 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
   match view.scopes with
   | List.nil      => view.name
   | List.cons _ _ =>
-    let base := (Name.mkStr (hAppend (hAppend (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
+    let base := (Name.mkStr (Name.appendCore (Name.appendCore (Name.mkStr view.name "_@") view.imported) view.mainModule) "_hyg")
     view.scopes.foldl Name.mkNum base
 
 private def assembleParts : List Name → Name → Name
@@ -4194,12 +4196,12 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
     | true  => Name.mkNum n scp
     | false =>
       { view with
-        imported   := view.scopes.foldl Name.mkNum (hAppend view.imported view.mainModule)
+        imported   := view.scopes.foldl Name.mkNum (Name.appendCore view.imported view.mainModule)
         mainModule := mainModule
         scopes     := List.cons scp List.nil
       }.review
   | false =>
-    Name.mkNum (Name.mkStr (hAppend (Name.mkStr n "_@") mainModule) "_hyg") scp
+    Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp
 
 /--
 Add a new macro scope onto the name `n`, using the monad state to supply the
@@ -4210,6 +4212,21 @@ main module and current macro scope.
   bind getCurrMacroScope fun scp =>
   pure (Lean.addMacroScope mainModule n scp)
 
+/--
+Append two names that may have macro scopes. The macro scopes in `b` are always erased.
+If `a` has macro scopes, then the are propagated to result of `append a b`
+-/
+def Name.append (a b : Name) : Name :=
+  let b := b.eraseMacroScopes
+  match a.hasMacroScopes with
+  | true =>
+    let view := extractMacroScopes a
+    { view with name := appendCore view.name b }.review
+  | false => appendCore a b
+
+instance : Append Name where
+  append := Name.append
+
 /-- The default maximum recursion depth. This is adjustable using the `maxRecDepth` option. -/
 def defaultMaxRecDepth := 512
 

src/Lean/Elab/Deriving/Util.lean

@@ -119,6 +119,8 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (
       let type         ← `($(mkIdent className) $indType)
       let val          ← if useAnonCtor then `(⟨$(mkIdent auxFunName)⟩) else pure <| mkIdent auxFunName
       let instCmd ← `(instance $binders:implicitBinder* : $type := $val)
+      trace[Meta.debug] "auxFunName: {auxFunName}"
+      trace[Meta.debug] "instCmd: {instCmd}"
       instances := instances.push instCmd
   return instances
 

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -357,9 +357,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
 
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
-  let env ← getEnv
   withOptions (tactic.hygienic.set · false) do
-    let baseName := mkPrivateName env declName
     lambdaTelescope info.value fun xs body => do
       let us := info.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -367,7 +365,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
       mkUnfoldProof declName goal.mvarId!
       let type ← mkForallFVars xs type
       let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := baseName ++ `_unfold
+      let name := mkPrivateName (← getEnv) (declName ++ `_unfold)
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -62,12 +62,11 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
     mkEqnTypes #[info.declName] goal.mvarId!
-  let baseName := mkPrivateName (← getEnv) info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`_eq).appendIndexAfter (i+1)
+    let name := mkPrivateName (← getEnv) (info.declName ++ (`_eq).appendIndexAfter (i+1))
     thmNames := thmNames.push name
     let value ← mkProof info.declName type
     let (type, value) ← removeUnusedEqnHypotheses type value

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -186,7 +186,6 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
 
 def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
-  let baseName := mkPrivateName (← getEnv) declName
   let eqnTypes ← withNewMCtxDepth <| lambdaTelescope info.value fun xs body => do
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -196,7 +195,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
-    let name := baseName ++ (`_eq).appendIndexAfter (i+1)
+    let name := mkPrivateName (← getEnv) (declName ++ (`_eq).appendIndexAfter (i+1))
     thmNames := thmNames.push name
     let value ← mkProof declName info type
     let (type, value) ← removeUnusedEqnHypotheses type value

src/Lean/Meta/Eqns.lean

@@ -66,7 +66,7 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
       let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
       let type  ← mkForallFVars xs (← mkEq lhs body)
       let value ← mkLambdaFVars xs (← mkEqRefl lhs)
-      let name := mkPrivateName (← getEnv) declName ++ `_eq_1
+      let name := mkPrivateName (← getEnv) (declName ++ `_eq_1)
       addDecl <| Declaration.thmDecl {
         name, type, value
         levelParams := info.levelParams

src/Lean/Meta/Match/MatchEqs.lean

@@ -609,7 +609,6 @@ where
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns := withLCtx {} {} do
   trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
   withConfig (fun c => { c with etaStruct := .none }) do
-  let baseName := mkPrivateName (← getEnv) matchDeclName
   let constInfo ← getConstInfo matchDeclName
   let us := constInfo.levelParams.map mkLevelParam
   let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function"
@@ -629,7 +628,7 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
     for i in [:alts.size] do
       let altNumParams := matchInfo.altNumParams[i]!
       let altNonEqNumParams := altNumParams - numDiscrEqs
-      let thmName := baseName ++ ((`eq).appendIndexAfter idx)
+      let thmName := mkPrivateName (← getEnv) (matchDeclName ++ ((`eq).appendIndexAfter idx))
       eqnNames := eqnNames.push thmName
       let (notAlt, splitterAltType, splitterAltNumParam, argMask) ← forallAltTelescope (← inferType alts[i]!) altNonEqNumParams fun ys eqs rhsArgs argMask altResultType => do
         let patterns := altResultType.getAppArgs
@@ -679,7 +678,7 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
       let template ← deltaExpand template (· == constInfo.name)
       let template := template.headBeta
       let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks)
-      let splitterName := baseName ++ `splitter
+      let splitterName := mkPrivateName (← getEnv) (matchDeclName ++ `splitter)
       addAndCompile <| Declaration.defnDecl {
         name        := splitterName
         levelParams := constInfo.levelParams

src/Lean/Modifiers.lean

@@ -17,69 +17,49 @@ def addProtected (env : Environment) (n : Name) : Environment :=
 def isProtected (env : Environment) (n : Name) : Bool :=
   protectedExt.isTagged env n
 
-/-! # Private name support.
+/-!
+# Private name support.
 
-   Suppose the user marks as declaration `n` as private. Then, we create
-   the name: `_private.<module_name>.0 ++ n`.
-   We say `_private.<module_name>.0` is the "private prefix"
-
-   We assume that `n` is a valid user name and does not contain
-   `Name.num` constructors. Thus, we can easily convert from
-   private internal name to the user given name.
+We use a reserved macro scope to encode private names.
 -/
 
-def privateHeader : Name := `_private
-
 def mkPrivateName (env : Environment) (n : Name) : Name :=
-  Name.mkNum (privateHeader ++ env.mainModule) 0 ++ n
+  if n.hasMacroScopes then
+    let view := extractMacroScopes n
+    { view with scopes := privateMacroScope :: view.scopes.erase privateMacroScope }.review
+  else
+    addMacroScope env.mainModule n privateMacroScope
 
-def isPrivateName : Name → Bool
-  | n@(.str p _) => n == privateHeader || isPrivateName p
-  | .num p _     => isPrivateName p
-  | _            => false
+def isPrivateName (declName : Name) : Bool :=
+  if declName.hasMacroScopes then
+    let view := extractMacroScopes declName
+    view.scopes.contains privateMacroScope
+  else
+    false
 
 @[export lean_is_private_name]
 def isPrivateNameExport (n : Name) : Bool :=
   isPrivateName n
 
-/--
-Return `true` if `n` is of the form `_private.<module_name>.0`
-See comment above.
--/
-private def isPrivatePrefix (n : Name) : Bool :=
-  match n with
-  | .num p 0 => go p
-  | _ => false
-where
-  go (n : Name) : Bool :=
-    n == privateHeader ||
-    match n with
-    | .str p _ => go p
-    | _ => false
-
-private def privateToUserNameAux (n : Name) : Name :=
-  match n with
-  | .str p s => .str (privateToUserNameAux p) s
-  | .num p i => if isPrivatePrefix n then .anonymous else .num (privateToUserNameAux p) i
-  | _        => .anonymous
-
 @[export lean_private_to_user_name]
 def privateToUserName? (n : Name) : Option Name :=
-  if isPrivateName n then privateToUserNameAux n
-  else none
+  if n.hasMacroScopes then
+    let view := extractMacroScopes n
+    if view.scopes.contains privateMacroScope then
+      { view with scopes := view.scopes.erase privateMacroScope }.review
+    else
+      none
+  else
+    none
 
 def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
-  match privateToUserName? n with
-  | some userName => mkPrivateName env userName != n
-  | _ => false
-
-private def privatePrefixAux : Name → Name
-  | .str p _ => privatePrefixAux p
-  | n        => n
-
-@[export lean_private_prefix]
-def privatePrefix? (n : Name) : Option Name :=
-  if isPrivateName n then privatePrefixAux n
-  else none
+  if n.hasMacroScopes then
+    let view := extractMacroScopes n
+    if view.scopes.contains privateMacroScope then
+      view.imported == env.mainModule
+    else
+      false
+  else
+    false
 
 end Lean