Ensure shadowed variables are inaccessible in quotations

[alexkeizer]

Check which variables are shadowed in the meta-context, and make sure they are inaccessible in the quotation context (by making their userName hygienic).

This PR is motivated by the following example (the described behaviour is as it is for master):

import Qq
open Qq

def foo : Q(Nat) :=
  let n : Nat := 1

  -- Qq doesn't realize this is a `Nat`. so it doesn't incorporate it into the quotation context
  let n := 2 
  
  /-
    The context inside q(...) looks like:
      «$n»: Nat := 1
      ⊢ Nat
    Hence, `q($n)` is taken to mean `q(1)`, even though the user probably intended it to mean `q(2)`
  -/
  q($n)

example : foo = q(1) := rfl

After the PR, the context inside the quotation still only has the first version of n, but it's made inaccessible

$n✝: Nat := 1
⊢ Nat

So that the q($n) line will throw an unknown identifier '«$n»' error (which ideally would be an the type of '«$n»' doesn't implement ToExpr error, but that is an orthogonal issue).

[eric-wieser]

This has some slightly odd behavior with set_option pp.sanitizeNames false, which disables the tombstoning generally, but not inside Qq. Maybe @gebner has an opinion on whether this is a good idea.

[alexkeizer]

In a sense, the tombstoning introduced in this PR is not so much about making names inaccessible, as it is about making sure that uses of a shadowing variable don't accidentally become references to the previous, now-shadowed, declaration, so it's defensible that this sanitizeNames option doesn't make these names accessible.

We could change this to rename x to x_shadowed or some other, accessible, name while pp.sanitizeNames is set to false, but there is always the risk of unintended name collisions there. We could also inspect the expression to make sure shadowed variables are not used, and throw an error otherwise, but this seems like a lot of code to implement.

However, I would say sticking with tombstoning in Qq even with this option set is also a valid choice: even though with the option regular shadowed variables are not tombstoned, they are still inaccessible by virtue of the name collision. Thus, I'd say they should remain inaccessible inside the Qq environment as well, even if the shadowing variable does not become a part of this context. Tombstoning is a nice way to achieve this