feat: apply app unexpanders for all prefixes of an application (#3375)

Before, app unexpanders would only be applied to entire applications.
However, some notations produce functions, and these functions can be
given additional arguments. The solution so far has been to write app
unexpanders so that they can take an arbitrary number of additional
arguments. However, as reported in [this Zulip
thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/pretty.20printer.20bug/near/420662236),
this leads to misleading hover information in the Infoview. For example,
while `HAdd.hAdd f g 1` pretty prints as `(f + g) 1`, hovering over `f +
g` shows `f`. There is no way to fix the situation from within an app
unexpander; the expression position for `HAdd.hAdd f g` is absent, and
app unexpanders cannot register TermInfo.

This commit changes the app delaborator to try running app unexpanders
on every prefix of an application, from longest to shortest prefix. For
efficiency, it is careful to only try this when app delaborators do in
fact exist for the head constant, and it also ensures arguments are only
delaborated once. Then, in `(f + g) 1`, the `f + g` gets TermInfo
registered for that subexpression, making it properly hoverable.

The app delaborator is also refactored, and there are some bug fixes:
- app unexpanders only run when `pp.explicit` is false
- trailing parameters in under-applied applications are now only
considered up to reducible & instance transparency, which lets, for
example, optional arguments for `IO`-valued functions to be omitted.
(`IO` is a reader monad, so it's hiding a pi type)
- app unexpanders will no longer run for delaborators that use
`withOverApp`
- auto parameters now always pretty print, since we are not verifying
that the provided argument equals the result of evaluating the tactic

Furthermore, the `notation` command has been modified to generate an app
unexpander that relies on the app delaborator's new behavior.

The change to app unexpanders is reverse-compatible, but it's
recommended to update `@[app_unexpander]`s in downstream projects so
that they no longer handle overapplication themselves.

src/Lean/Elab/Notation.lean

@@ -107,22 +107,10 @@ def mkUnexpander (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Mac
   -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
   let lhs ← `($$f:ident)
   let lhs := Syntax.mkApp lhs (.mk args)
-  -- allow over-application, avoiding nested `app` nodes
-  let lhsWithMoreArgs := flattenApp (← `($lhs $$moreArgs*))
-  let patWithMoreArgs := flattenApp (← `($pat $$moreArgs*))
   `(@[$attrKind app_unexpander $(mkIdent c)]
     aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($lhs)             => withRef f `($pat)
-      -- must be a separate case as the LHS and RHS above might not be `app` nodes
-      | `($lhsWithMoreArgs) => withRef f `($patWithMoreArgs)
       | _                   => throw ())
-where
-  -- NOTE: we consider only one nesting level here
-  flattenApp : Term → Term
-    | stx@`($f $xs*) => match f with
-      | `($f' $xs'*) => Syntax.mkApp f' (xs' ++ xs)
-      | _            => stx
-    | stx            => stx
 
 private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     (doc? : Option (TSyntax ``docComment))

src/Lean/PrettyPrinter/Delaborator/SubExpr.lean

@@ -65,6 +65,16 @@ def withBoundedAppFnArgs (maxArgs : Nat) (xf : m α) (xa : α → m α) : m α :
     withAppArg (xa acc)
   | _, _ => xf
 
+/--
+Runs `xf` in the context of `Lean.Expr.getBoundedAppFn maxArgs`.
+This is equivalent to `withBoundedAppFnArgs maxArgs xf pure`.
+-/
+def withBoundedAppFn (maxArgs : Nat) (xf : m α) : m α := do
+  let e ← getExpr
+  let numArgs := min maxArgs e.getAppNumArgs
+  let newPos := (← getPos).pushNaryFn numArgs
+  withTheReader SubExpr (fun cfg => { cfg with expr := e.getBoundedAppFn numArgs, pos := newPos }) xf
+
 def withBindingDomain (x : m α) : m α := do descend (← getExpr).bindingDomain! 0 x
 
 def withBindingBody (n : Name) (x : m α) : m α := do