RFC: Make the delab attribute resolve the name

[jthulhu]

Proposal

This proposal's purpose is to improve user experience when writing delaborators. More specifically, the delaborator attribute currently assumes that the name given as argument matches the name internally generated by the delaborator, which means that no name resolution occurs. Not only this may go against the expectations of a user not acknowledged with the delabotor's internals, but this is currently not documented. The Metaprogramming in Lean 4 book (which, AFAIK, is the only available documentation on this topic) does not explicitly mention this detail, and all the examples happen in the root namespace, so this issue never occurs. Even worse, there is no feedback at all that the name is not resolved: if the user does the wrong thing by expecting the name to be resolved, at no point will a warning or an error appear. Rather, nothing happens, which is poor UX.

The proposal is that the delaborator attribute (ie. @[delab app.foobar]) should resolve the name of the constant being delaborated. For instance, in the following situation

namespace Foo.Bar
def foobar : Nat → Nat := ...

@[delab app.foobar]
def delab_foobar : Delab := do ...
end Foo.Bar

the current behavior is to do nothing, not even trigger a warning. Instead, it should resolve the name foobar so that the actual delaborator key that is registered is app.Foo.Bar.foobar. If the name cannot be resolved in the local namespace, the current behavior is preserved.

The following alternatives are also possible to improve the user experience:

• the delaborator key that is registered is always the one provided by the user, but, in case it could be resolved to a name existing in the local namespace, a warning is emitted, so that, in case the user is not aware that the name is not resolved, they still get feedback.
• the delaborator key is resolved as proposed, and in the case that it is not resolved, a warning is emitted.
• the syntax of the delab property is changed to be consistent with how names are resolved in metaprogramming in general @[delab app.foobar] would become @[delab app `foobar] if the user doesn't want the name to be resolved, and @[delab app ``foobar] if the user wants the name to be resolved.

Finally, once this RFC is closed and a decision has been made about whether to implement the proposal (or one of its variants) or not, the documentation should be changed to mention this point.

Community Feedback

Zulip thread.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[kmill]

I think there's an issue with having @[delab app.foo] itself resolve foo (what if a metaprogram wants to be sure it's adding a delaborator with a specific delaboration key?), but maybe it would be worth having a separate @[app_delab foo] that does resolution. This attribute would be an analogue to @[app_unexpander foo], which also does resolution.

[nomeata]

Silently doing nothing is indeed not great design, thanks for raising this.

I'm sceptical of app.foobar resolving after the app, though.

I like your third alternative, i.e. a syntax that has the function to delab as an ident of it's own. Maybe @[app_delab foobar]. Not sure if there is a use case for not resolving names?

[nomeata]

Ha, jinx'ed with kmill. Good to see that we agree here :-)