feat: apply app unexpanders for all prefixes of an application

[kmill]

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, 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.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-02-16 22:58:51)
• 💥 Mathlib branch lean-pr-testing-3375 build failed against this PR. (2024-02-18 02:14:28) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d6df1ec32fc26524b12bee8eac2ed45fcb4391ed --onto 88fbe2e5313bb418abdb035c48cae2680ea9bcea. (2024-02-27 06:04:37)

[Kha]

Is there anything we could do against this?

[kmill]

I added a heuristic that if there was a problem computing the ParamKinds, but the universe list is [], then it's likely that the universe list has been intentionally erased and the application has all its implicit arguments erased, so it tells explicit mode that @ is not necessary.

It's doing this in explicit mode because that avoids expanders from applying, and the logic of explicit mode is simpler to reason about.

[Kha]

It looks like in this case we do want the app unexpander for lcErased to apply. But the more reasonable approach here is probably not to reuse the Lean delaborator for IR printing, so this looks satisfactory to me for now.

[Kha]

Ah, there is an explicit pp.explicit in the test, so I suppose this regression is expected

[kmill]

It turns out that match's missing pattern errors also lack universe levels, so this helps with that as well. (Lean.Meta.Match.Example.toMessageData)