literal expressions not type-safe

[ericrbg]

mwe:

import Qq
open Qq

def foo (a : Q(Bool)) : Prop := true

example : Prop :=
  let a : Q(Nat) := q(23)
  have := foo a
  have := foo q($a)
  false

the line that says foo a is totally fine, but foo q($a) errors as expected. It'd be nice if I didn't have to requote everything to get the type errors!