trouble matching `∀` in Qq

Stream: lean4

[Jireh Loreaux]

Can someone explain why the second one of these doesn't work, and how to fix it?

-- this is an example in the `Qq` library
example : Q(Prop) → MetaM Q(Prop)
  | ~q(∃ x y, $p x y) => return q(∀ x y, $p x y)
  | e => return e

-- this doesn't work. Note the switch of `∃` and `∀`.
example : Q(Prop) → MetaM Q(Prop)
  | ~q(∀ x y, $p x y) => return q(∃ x y, $p x y) -- cannot quote level mvar ?u.14326
  | e => return e

[Eric Wieser]

Does adding explicit binder types help?

[Thomas Murrills]

Partial answer: I think it has to do with ~q knowing how to handle level mvars when they appear as parameters to a constant, as in Exists.{?u} (possible by not using mvars at all in that case behind the scenes; I'm not sure), but not knowing how to deal with level mvars when they appear in the type of the binder of a forallE, as they do for the types of x and y in ∀ x y, $p x y.

Note also that ∃ elaborates in a special way such that we always wind up with a function $p to match on, no matter the actual form of the body. This isn't the case for ∀, so a different approach should be taken in order to be able to match on any body!

[Thomas Murrills]

Eric Wieser said:

Does adding explicit binder types help?

^It does! :) For the generic case of x y : Sort u, though, I suspect we'd need to resort to bare expr matching.

[Thomas Murrills]

There is one advantage to bare expr matching in general here: you can preserve binder names. Note that in the working example, the x, y in return q(∀ x y, $p x y) are unrelated to the x, y in ~q(∃ x y, $p x y), and you'll wind up with x, y as binder names no matter the names of the binders that you match on. Maybe there's a way to do that with Qq as well? I'm not sure. Naively adding $ to the binders doesn't work.

[Jireh Loreaux]

ah yes, I had been doing some bare expr matching before this, but I was attempting to use Qq to save some hassle. I guess is sort of surprises me there isn't a Qq way to match an arbitrary ∀ though. :thinking: