fix: pretty print dot notation for private definitions on public types (#10122)

This PR adds support for pretty printing using generalized field
notation (dot notation) for private definitions on public types. It also
modifies dot notation elaboration to resolve names after removing the
private prefix, which enables using dot notation for private definitions
on private imported types.

It won't pretty print with dot notation for definitions on inaccessible
private types from other modules.

Closes #7297

src/Lean/Elab/App.lean

@@ -1270,7 +1270,7 @@ If it resolves to `name`, returns `(S', name)`.
 private partial def findMethod? (structName fieldName : Name) : MetaM (Option (Name × Name)) := do
   let env ← getEnv
   let find? structName' : MetaM (Option (Name × Name)) := do
-    let fullName := structName' ++ fieldName
+    let fullName := privateToUserName structName' ++ fieldName
     -- We do not want to make use of the current namespace for resolution.
     let candidates := ResolveName.resolveGlobalName (← getEnv) Name.anonymous (← getOpenDecls) fullName
       |>.filter (fun (_, fieldList) => fieldList.isEmpty)

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -44,16 +44,25 @@ private def projInfo (c : Name) : MetaM (Option (Name × Nat × Bool × Bool ×
   else
     return none
 
+/--
+Checks that `e` is an application of a constant that equals `baseName`, taking into consideration private name mangling.
+-/
+private def isAppOfBaseName (env : Environment) (e : Expr) (baseName : Name) : Bool :=
+  if let some c := e.cleanupAnnotations.getAppFn.constName? then
+    privateToUserName c == baseName && !isInaccessiblePrivateName env c
+  else
+    false
+
 /--
 Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types.
 -/
 private partial def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   withReducibleAndInstances do
-    if type.cleanupAnnotations.isAppOf baseName then
+    if isAppOfBaseName (← getEnv) type baseName then
       return true
     else
       let type ← whnfCore type
-      if type.isAppOf baseName then
+      if isAppOfBaseName (← getEnv) type baseName then
         return true
       else
         match ← unfoldDefinition? type with
@@ -66,10 +75,10 @@ returns the field name and the index for the argument to be used as the object o
 Otherwise it fails.
 -/
 private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × Nat) := do
-  let .str _ field := c | failure
-  let field := Name.mkSimple field
-  let baseName := c.getPrefix
+  let .str baseName field := c | failure
+  let baseName := privateToUserName baseName
   guard <| !baseName.isAnonymous
+  let field := Name.mkSimple field
   -- Disallow `Function` since it is used for pi types.
   guard <| baseName != `Function
   let info ← getConstInfo c
@@ -87,7 +96,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
         -- We require an exact match for the base name.
         -- While `Lean.Elab.Term.resolveLValLoop` is able to unfold the type and iterate, we do not attempt to exploit this feature.
         -- (To get it right, we would need to check that each relevant namespace does not contain a declaration named `field`.)
-        guard <| (← instantiateMVars <| ← inferType args[i]!).consumeMData.isAppOf baseName
+        guard <| isAppOfBaseName (← getEnv) (← instantiateMVars <| ← inferType args[i]!) baseName
         return (field, i)
       else
         -- We only use the first explicit argument for field notation.
@@ -107,6 +116,8 @@ returns the field name to use and the argument index for the object of the field
 def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldNotation : Bool) : MetaM (Option (Name × Nat)) := do
   let env ← getEnv
   let .const c .. := f.consumeMData | return none
+  if isInaccessiblePrivateName (← getEnv) c then
+    return none
   if c.getPrefix.isAnonymous then return none
   -- If there is `pp_nodot` on this function, then don't use field notation for it.
   if hasPPNoDotAttribute env c then

tests/lean/private.lean.expected.out

@@ -8,6 +8,6 @@ Boo.Bla.boo == "world" : Bool
 Boo.boo == 100 : Bool
 Boo.Bla.boo == "world" : Bool
 Boo.boo == 100 : Bool
-Nat.mul10 x : Nat
+x.mul10 : Nat
 private.lean:65:12-65:13: error: a non-private declaration `y` has already been declared
 private.lean:68:4-68:5: error: a private declaration `z` has already been declared

tests/lean/run/cleanupTypeAnnotations.lean

@@ -49,7 +49,7 @@ instance i1 (b := 0) : Decidable (a.toNat = b) :=
   have : True := by trace_state; trivial
   inferInstance
 
-/-- info: i1 (a : Bool := true) (b : Nat := 0) : Decidable (Bool.toNat a = b) -/
+/-- info: i1 (a : Bool := true) (b : Nat := 0) : Decidable (a.toNat = b) -/
 #guard_msgs in #check i1
 
 /-!

tests/lean/run/delabProjectionApp.lean

@@ -184,3 +184,36 @@ set_option pp.notation false in
 set_option pp.notation false in set_option pp.fieldNotation.generalized false in
 /-- info: ∀ {α : Type} (s t : MySet α), MySet.MySubset s t : Prop -/
 #guard_msgs in #check ∀ {α : Type} (s t : MySet α), s ⊆⊆ t
+
+/-!
+Private definition on public type.
+-/
+private def Char.MyIsA (c : Char) : Prop := c = 'A'
+
+/-- info: ∀ (c : Char), c.MyIsA : Prop -/
+#guard_msgs in #check ∀ (c : Char), c.MyIsA
+
+/-!
+Public definition on public type.
+-/
+def Char.MyIsA' (c : Char) : Prop := c = 'A'
+
+/-- info: ∀ (c : Char), c.MyIsA' : Prop -/
+#guard_msgs in #check ∀ (c : Char), c.MyIsA'
+
+/-!
+Private definition on private type.
+-/
+private structure Char'
+private def Char'.MyIsA (_ : Char') : Prop := true
+
+/-- info: ∀ (c : Char'), c.MyIsA : Prop -/
+#guard_msgs in #check ∀ (c : Char'), c.MyIsA
+
+/-!
+Public definition on private type.
+-/
+def Char'.MyIsA' (_ : Char') : Prop := true
+
+/-- info: ∀ (c : Char'), c.MyIsA' : Prop -/
+#guard_msgs in #check ∀ (c : Char'), c.MyIsA'

tests/lean/run/grind_9572.lean

@@ -12,7 +12,7 @@ l : List Nat
 h :
   ¬List.Pairwise
       (fun x y =>
-        List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
+        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
           (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
       l
 ⊢ False
@@ -20,13 +20,13 @@ h :
   [facts] Asserted facts
     [prop] ¬List.Pairwise
             (fun x y =>
-              List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
+              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
                 (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
             l
   [eqc] False propositions
     [prop] List.Pairwise
           (fun x y =>
-            List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
+            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
               (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
           l
 -/