Option for tactic mode auto-metavar names everywhere?

Stream: lean4

[nrs]

Is there an option to automatically give a friendlier name to automatically generated metavariables, always? e.g. use the argument name from the function from which it arises or something of the sort, instead of their unique IDs. Maybe this doesn't exist but since sometimes automatically named metavariables in tactic mode do use alphabetical names (I think the inaccessible ones always do?) I thought there might be a chance

[Eric Wieser]

Can you give an example of how you introduced the offending metavariables?

[nrs]

I was thinking about this while looking at the trace of #**general>Successful instance search is followed by failure?** , it seems to me that it is not immediate that there are at most four or five candidate unknown metavariables in the entire trace but I thought that, probably, if instead they were given alphabetical names it would be clearer (of course this is probably just me, but also it seems like it would be helpful in cases when you're metagaming the typechecker and hunting for metavariable resolutions instead of thinking more abstractly)