feat: add pp.safe_shadowing

When `pp.safe_shadowing` is set to true, we still use the
suggested name if the "body" does not contain a free variable with the
suggested name. This is the approach used in Lean 3, and I think it
improved the result in all affected tests.
The implementation was simple. The only nasty case was `delabAppMatch`.

The main motivation for this feature was hovering information such as
```lean
f : {α_1 : Type} → α_1 → α_1
```
when hovering over the `f` at
```lean
def g (α : Type) (a : α) :=
  f a
```
With `safe_shadowing`, we get the nicer
```lean
f : {α : Type} → α → α
```

cc @Kha

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -45,10 +45,12 @@ def getPPUniverses (o : Options) : Bool := o.get `pp.universes (getPPAll o)
 def getPPFullNames (o : Options) : Bool := o.get `pp.full_names (getPPAll o)
 def getPPPrivateNames (o : Options) : Bool := o.get `pp.private_names (getPPAll o)
 def getPPUnicode (o : Options) : Bool := o.get `pp.unicode (!getPPAll o)
+def getPPSafeShadowing (o : Options) : Bool := o.get `pp.safe_shadowing true
 
 builtin_initialize
   registerOption `pp.explicit { defValue := false, group := "pp", descr := "(pretty printer) display implicit arguments" }
   registerOption `pp.structure_instance_type { defValue := false, group := "pp", descr := "(pretty printer) display type of structure instances" }
+  registerOption `pp.safe_shadowing { defValue := true, group := "pp", descr := "(pretty printer) allow variable shadowing if there is no collision" }
   -- TODO: register other options when old pretty printer is removed
   --registerOption `pp.universes { defValue := false, group := "pp", descr := "(pretty printer) display universes" }
 
@@ -213,14 +215,28 @@ def annotateCurPos (stx : Syntax) : Delab := do
   let ctx ← read
   pure $ annotatePos ctx.pos stx
 
-def getUnusedName (suggestion : Name) : DelabM Name := do
+def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
   -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
   let suggestion := if suggestion.isAnonymous then `a else suggestion;
+  let suggestion := suggestion.eraseMacroScopes
   let lctx ← getLCtx
-  pure $ lctx.getUnusedName suggestion
+  if !lctx.usesUserName suggestion then
+    return suggestion
+  else if (← getPPOption getPPSafeShadowing) && !bodyUsesSuggestion lctx suggestion then
+    return suggestion
+  else
+    return lctx.getUnusedName suggestion
+where
+  bodyUsesSuggestion (lctx : LocalContext) (suggestion' : Name) : Bool :=
+    Option.isSome <| body.find? fun
+      | Expr.fvar fvarId _ =>
+        match lctx.find? fvarId with
+        | none      => false
+        | some decl => decl.userName == suggestion'
+      | _ => false
 
 def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
-  let n ← getUnusedName (← getExpr).bindingName!
+  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
   let stxN ← annotateCurPos (mkIdent n)
   withBindingBody n $ d stxN
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -156,21 +156,14 @@ structure AppMatchState where
   params    : Array Expr := #[]
   hasMotive : Bool := false
   discrs    : Array Syntax := #[]
+  varNames  : Array (Array Name) := #[]
   rhss      : Array Syntax := #[]
   -- additional arguments applied to the result of the `match` expression
   moreArgs  : Array Syntax := #[]
-
-/-- Skip `numParams` binders. -/
-private def skippingBinders {α} : (numParams : Nat) → (x : DelabM α) → DelabM α
-  | 0,           x => x
-  | numParams+1, x =>
-    withBindingBodyUnusedName fun _ =>
-      skippingBinders numParams x
-
 /--
   Extract arguments of motive applications from the matcher type.
   For the example below: `#[#[`([])], #[`(a::as)]]` -/
-private def delabPatterns (st : AppMatchState) : DelabM (Array (Array Syntax)) := do
+private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Syntax)) := do
   let ty ← instantiateForall st.matcherTy st.params
   forallTelescope ty fun params _ => do
     -- skip motive and discriminators
@@ -178,8 +171,26 @@ private def delabPatterns (st : AppMatchState) : DelabM (Array (Array Syntax)) :
     alts.mapIdxM fun idx alt => do
       let ty ← inferType alt
       withReader ({ · with expr := ty }) $
-        skippingBinders st.info.altNumParams[idx] do
+        usingNames st.varNames[idx] do
           withAppFnArgs (pure #[]) (fun pats => do pure $ pats.push (← delab))
+where
+  usingNames {α} (varNames : Array Name) (x : DelabM α) : DelabM α :=
+    usingNamesAux 0 varNames x
+  usingNamesAux {α} (i : Nat) (varNames : Array Name) (x : DelabM α) : DelabM α :=
+    if i < varNames.size then
+      withBindingBody varNames[i] <| usingNamesAux (i+1) varNames x
+    else
+      x
+
+/-- Skip `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names. -/
+private def skippingBinders {α} (numParams : Nat) (x : Array Name → DelabM α) : DelabM α :=
+  loop numParams #[]
+where
+  loop : Nat → Array Name → DelabM α
+    | 0,   varNames => x varNames
+    | n+1, varNames =>
+      withBindingBodyUnusedName fun id => do
+        loop n (varNames.push id.getId)
 
 /--
   Delaborate applications of "matchers" such as
@@ -196,7 +207,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
     (do
       let (Expr.const c us _) ← getExpr | failure
       let (some info) ← getMatcherInfo? c | failure
-      { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info, : AppMatchState })
+      { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
     (fun st => do
       if st.params.size < st.info.numParams then
         pure { st with params := st.params.push (← getExpr) }
@@ -206,7 +217,12 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
       else if st.discrs.size < st.info.numDiscrs then
         pure { st with discrs := st.discrs.push (← delab) }
       else if st.rhss.size < st.info.altNumParams.size then
-        pure { st with rhss := st.rhss.push (← skippingBinders st.info.altNumParams[st.rhss.size] delab) }
+        /- We save the variables names here to be able to implemente safe_shadowing.
+           The pattern delaboration must use the names saved here. -/
+        let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size] fun varNames => do
+          let rhs ← delab
+          return (varNames, rhs)
+        pure { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
       else
         pure { st with moreArgs := st.moreArgs.push (← delab) })
 
@@ -347,7 +363,7 @@ def delabForall : Delab :=
 @[builtinDelab letE]
 def delabLetE : Delab := do
   let Expr.letE n t v b _ ← getExpr | unreachable!
-  let n ← getUnusedName n
+  let n ← getUnusedName n b
   let stxT ← descend t 0 delab
   let stxV ← descend v 1 delab
   let stxB ← withLetDecl n t v fun fvar =>
@@ -547,7 +563,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
       | _ => delabAndRet
   else if e.isLet then
     let Expr.letE n t v b _ ← getExpr | unreachable!
-    let n ← getUnusedName n
+    let n ← getUnusedName n b
     let stxT ← descend t 0 delab
     let stxV ← descend v 1 delab
     withLetDecl n t v fun fvar =>

tests/lean/220.lean.expected.out

@@ -2,4 +2,4 @@ def f : List Nat → List Nat :=
 fun (x : List Nat) =>
   match x with 
   | a :: xs@(b :: bs) => xs
-  | x_1 => []
+  | x => []

tests/lean/autoBoundImplicits1.lean.expected.out

@@ -10,6 +10,6 @@ autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β'
 autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n'
 autoBoundImplicits1.lean:25:18-25:23: warning: declaration uses 'sorry'
-f : {α_1 : Type} → {n_1 : Nat} → Vec α_1 n_1 → Vec α_1 n_1
+f : {α : Type} → {n : Nat} → Vec α n → Vec α n
 f mkVec : Vec ?m 0
 f mkVec : Vec Nat 0

tests/lean/match1.lean.expected.out

@@ -34,18 +34,18 @@ fun (x : Nat × Nat) =>
 fun (x x_1 : Option Nat) =>
   match x, x_1 with 
   | some a, some b => some (a + b)
-  | x_2, x_3 => none : Option Nat → Option Nat → Option Nat
+  | x, x => none : Option Nat → Option Nat → Option Nat
 fun (x : Nat) =>
   (match x with 
     | 0 => id
-    | Nat.succ x_1 => id)
+    | Nat.succ x => id)
     x : Nat → Nat
 fun (x : Array Nat) =>
   match x with 
   | #[1, 2] => 2
   | #[] => 0
   | #[3, 4, 5] => 3
-  | x_1 => 4 : Array Nat → Nat
+  | x => 4 : Array Nat → Nat
 g.match_1 : (motive : List ?m → Sort u_2) →
-  (x : List ?m) → ((a : ?m) → motive [a]) → ((x_1 : List ?m) → motive x_1) → motive x
+  (x : List ?m) → ((a : ?m) → motive [a]) → ((x : List ?m) → motive x) → motive x
 fun (e : Empty) => nomatch e : Empty → False

tests/lean/precissues.lean.expected.out

@@ -21,6 +21,6 @@ p ∧ ¬q : Prop
 ¬p = q : Prop
 ¬p = q : Prop
 id ¬p : Prop
-(a a_1 : Nat) → a_1 = a_1 : Prop
+(a a : Nat) → a = a : Prop
 id : ?m → ?m
 precissues.lean:41:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term

tests/lean/safeShadowing.lean

@@ -0,0 +1,22 @@
+def f (x x : Nat) :=
+  match x with
+  | 0          => x + 1
+  | Nat.succ _ => x + 2
+
+variables {α : Type}
+
+#check fun (a : α) => a
+
+#check fun {α} (a : α) => a
+
+#check fun (x x : Nat) => x
+
+#print f
+
+set_option pp.safe_shadowing false
+
+#check fun {α} (a : α) => a
+
+#check fun (x x : Nat) => x
+
+#print f

tests/lean/safeShadowing.lean.expected.out

@@ -0,0 +1,15 @@
+fun (a : α) => a : α → α
+fun {α : Sort u_1} (a : α) => a : {α : Sort u_1} → α → α
+fun (x x : Nat) => x : Nat → Nat → Nat
+def f : Nat → Nat → Nat :=
+fun (x x : Nat) =>
+  match x with 
+  | 0 => x + 1
+  | Nat.succ x_1 => x + 2
+fun {α_1 : Sort u_1} (a : α_1) => a : {α_1 : Sort u_1} → α_1 → α_1
+fun (x x_1 : Nat) => x_1 : Nat → Nat → Nat
+def f : Nat → Nat → Nat :=
+fun (x x_1 : Nat) =>
+  match x_1 with 
+  | 0 => x_1 + 1
+  | Nat.succ x_2 => x_1 + 2

tests/lean/simpcfg.lean.expected.out

@@ -1,6 +1,6 @@
 f : Nat → Nat
 x y z : Nat
-h : x = (fun (x_1 : Nat) => x_1) y
+h : x = (fun (x : Nat) => x) y
 ⊢ f x = f y
 f : Nat → Nat
 x y z : Nat