Question about unused variable linter

Stream: metaprogramming / tactics

[Jannis Limperg]

I'm looking at the unused variable linter because I'd like to implement a similar analysis in a tool for proof optimisation/cleanup. The docs say:

The main complication is that it can be difficult to
determine what constitutes a "use" apart from direct references to a variable
that we can easily find in the info tree. For example, we would like this to be
considered a use of x:

def foo (x : Nat) : Nat := by assumption

The final proof term is fun x => x so clearly x was used, but we can't make
use of this because the final proof term is after we have abstracted over the
original fvar for x. [...]

If we [...] look further into the tactic state, we can see
the fvar show up in the instantiation to the original goal metavariable
?m : Nat := x, but it is not always the case that we can follow metavariable
instantiations to determine what happened after the fact, because tactics might
skip the goal metavariable and instantiate some other metavariable created prior
to it instead.

I don't quite understand what the corner case described here would look like. Could someone enlighten me? CC @Mario Carneiro and @Sebastian Ullrich since you're listed as authors of the linter.

[Mario Carneiro]

(the last rewrite of the linter was Sebastian Ullrich 's)