Tactic quotations may pick up implicit abstraction names

[Kha]

#check _ → a -- unknown identifier 'a'
run_cmd tactic.to_expr ```(_ → a) >>= tactic.trace -- Π (a : Sort ?), a

In my specific case, the implicit a actually shadowed an outer variable of the same name, which led to a quite confusing error message.

Similarly, not distinguishing non-dependent functions from dependent ones pre-elaboration may introduce unnecessary delayed abstractions:

run_cmd tactic.to_expr ```(bool → _) >>= tactic.trace -- Π (a : bool), ?m_2[a]

I suppose this is just one more item to throw onto the stack of #1674 -- presumably, → would be a macro there that would be unfolded by simpler metaprograms that want to handle both cases uniformly, but would be handled directly by e.g. the elaborator. On top of that, I would expect a user-input Pi never to be pretty-printed as →, which preservers some semantic information in form of the binding names.