Incorrect metadata on pretty-printed signature of String.append

[david-christiansen]

Description

The metadata that's attached to the pretty-printed representation of String.append's signature is incorrect for one of its argument types.

In particular, hovering the second argument's type gives much less information than the first argument's type, and "go to def" doesn't work on it.

Context

[Broader context that the issue occured in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

1. Type #check String.append
2. In the infoview, check the hovers associated with each argument

Expected behavior:
The first argument type and the return type should work consistently with the second argument type.

Actual behavior:
The first argument's type and the return type look like this:

the second argument's type looks like this:

Versions

This can be seen in the latest nightly on live.lean-lang.org: https://live.lean-lang.org/#project=lean-nightly&code=%23check%20String.append%0A

I've also reproduced it in Lean 4.10.

In Lean 4.0 and 4.5, which uses the old format with the inaccessible names, the second one still has the wrong hover:

So this seems to be a fairly old bug.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[david-christiansen]

After a bit more experimentation, this seems to apply to any function argument with a borrow annotation. Here's some examples:

• Both arguments of String.get
• Both arguments of Nat.add, Nat.mul, Nat.pow
• The argument to UInt8.ofNat

[david-christiansen]

This seems to be a general issue with metadata nodes and the delaborator. Here's a minimized failure:

import Lean

open Lean Elab Term Command in
open PrettyPrinter Delaborator in
elab "test" t:term : command => do
  let e ← liftTermElabM <| elabTerm t none
  logInfoAt t m!"{e} {Expr.mdata {} e}"

test String.append

The result is that the first occurrence has a correct hover, while the second doesn't:

I'd expect the annotations here to ignore mdata nodes when figuring out the meaning of some bit of rendered text.