Confusing type of Expr inputs in the local context

[Vtec234]

Consider the following program:

def abc : Q(Type) :=
  let e : Expr := Expr.const `abc []
  let f : Q(Type) := Expr.const ``Nat []
  q(sorry)

Then hovering over sorry, we see the following Expected type:

«$e» : Expr := Expr.const `abc []
«$f» : Type
⊢ Type

Here $f has its "internal" type shown properly (Type rather than Q(Type)), whereas $e has its "external" type shown which is quite confusing as the context is now mixing up theories. Could quote4 assume something like e : Q(?), or e : Q(dummy), and show $e : ?mvar, or $e : dummy, in the local context?

UPDATE: This happens because quote4 comes with an auto-quotation feature using the ToExpr typeclass. For example, if we have n : Nat in the external context, we get $n : Nat internally. This is actually mkNatLit n, using the ToExpr Nat instance. Combining this behaviour with the ToExpr Expr instance present in mathlib makes for the confusing situation described here where e gets quoted twice.