How to match only types using Qq

Stream: lean4

[Vasilii Nesterov]

When matching some type : Q(Prop) with $x = $y how can I filter out the case when x and y are Props?

import Qq
open Qq Lean Elab Meta Tactic

elab "print_eqs" : tactic => withMainContext do
  for ldecl in ← getLCtx do
    let ⟨0, type, expr⟩ := ← inferTypeQ ldecl.toExpr | continue
    match type with
    | ~q(@Eq $α $x $y) =>
      -- Is it possible to filter only α : Q(Type u) here?
      logInfo m!"{x} = {y}"
    | _ => pure ()

example (a b : Nat) (h1 : a = b) : True := by
  have h2 : True = True := rfl
  print_eqs

For example, later I'd like to check whether there is an LE α instance:

let inst ← synthInstanceQ (q(LE $α))

but it is impossible because LE expects α : Type u, not α : Sort u.

[Eric Wieser]

Did you mean to test with trivial = trivial instead?

[Eric Wieser]

Matching against ~q(@Eq.{_ + 1} $α $x $y) seems to work

[Eric Wieser]

As does ~q(@Eq ($α : Type _) $x $y)

[Robin Arnez]

Also, maybe don't inferTypeQ here, there is ldecl.type which should also do what you want.

[Yaël Dillies]

Robin, your suggestion does not provide the correct Qq annotations, right?

[Robin Arnez]

You're right... but I feel like it's silly to do use an inferType when the information already exists somewhere.

[Vasilii Nesterov]

Thank you very much, Eric!

[Eric Wieser]

Note that the let ⟨0, can fail if the universe is a metavariable

[Vasilii Nesterov]

Ah, I see. Is there a better way than

let ⟨u, type, expr⟩ := ← inferTypeQ ldecl.toExpr
if ← isProp type then
  have : u =QL 0 := ⟨⟩
  -- the rest of the code

?