Potential unhygienic use of functions in `Lean` namespace

[Vtec234]

Consider the following example. A universe level and a typeclass instance that depends on it are only antiquoted correctly if the Lean namespace is open in the enclosing scope. This suggests that some function there is not used hygienically. I would expect the example to work regardless of whether Lean is open.

import Qq

open Qq

class Foo.{v} (α : Type) : Type v where
class Bar.{v} (α : Type) [Foo.{v} α] where

structure FooBar₁ where
  v : Level
  T : Q(Type)
  fooT : Q(Foo.{v} $T)
  /- failed to synthesize instance
    Foo «$T» -/
  barT : Q(Bar.{v} $T) -- $v and $fooT are not in the local context

open Lean

structure FooBar₂ where
  v : Level
  T : Q(Type)
  fooT : Q(Foo.{v} $T)
  barT : Q(Bar.{v} $T) -- works, $v and $fooT are in the local context

[gebner]

I'm not at a computer right now, but I'm pretty sure the first Level is an autoimplicit.

[Vtec234]

Oops! Sorry about that.