unsupported pattern in syntax match

Stream: lean4

[Joachim Breitner]

I haven’t played much with Qq yet, so maybe this should be obvious, but why does the following not work?

import Mathlib.Util.Qq

open Lean
open Qq

example (e : Expr) : MetaM Expr := do
  match e : Q(Prop) with
  | ~q(of_eq_true _) => pure e
  | e => pure e

It says

unsupported pattern in syntax match
  ~q(of_eq_true _)

[Joachim Breitner]

Ah, maybe the Q(Prop) is simply a lie

[Joachim Breitner]

This seems to work:

example (e : Expr) : MetaM Expr := do
  let prop : Q(Prop) ← Lean.Meta.inferType e
  let e : Q($prop) ← pure e
  match e with
  | ~q(of_eq_true _) => pure e
  | e => pure e

[Eric Wieser]

of_eq_true _ is not of type Prop so indeed your first match is nonsense

[Joachim Breitner]

Yes, got the levels confused :-)

I am now at the point where I can match some expression, but the value that I am getting out of the match is a metavariable for some reason:
My code

import Lean.Meta.Tactic.Simp
import Mathlib.Tactic.RunCmd
import Std.Tactic.TryThis
import Std.Tactic.ShowTerm
import Mathlib.Tactic.Says
import Mathlib.Util.Qq


open Lean Elab Tactic Meta
open Std.Tactic.TryThis
open Qq

def apply_un_of_eq_true (e : Expr) : MetaM Expr := do
  let prop : Q(Prop) ← Lean.Meta.inferType e
  match prop with
  | ~q($a = ($b : $α)) =>
    let e : Q($a = $b) ← pure e
    match e with
    | ~q(of_eq_true (Eq.trans (congrFun (congrArg Eq $p) _) (eq_self _))) => do
        logInfo m!"a : {a}\nb : {b}\ne: {e}\nh: {p}"
        pure e
    | _ => do
        logInfo m!"Unrecognized term:\n{e}\n"
        pure e

elab (name := calcifyTac) "calcify " t:tacticSeq : tactic => withMainContext do
  let g ← getMainGoal
  evalTactic t
  let expr ← instantiateMVars (mkMVar g)
  let expr2 ← apply_un_of_eq_true expr
  logInfo $ m!"Before simplifying:\n{expr}\n" ++
            m!"After simplifying:\n{expr2}"

set_option pp.rawOnError true

example x : 0 + (0 + x) = x := by
    calcify simp

prints

a : 0 + (0 + x)
b : x
e: of_eq_true
  (Eq.trans (congrFun (congrArg Eq (Eq.trans (congrArg (HAdd.hAdd 0) (Nat.zero_add x)) (Nat.zero_add x))) x)
    (eq_self x))
h: [Error pretty printing expression: unknown metavariable '?_uniq.16571'. Falling back to raw printer.]
?_uniq.16571

and I wonder why h is a metavariable, and not imply the expected subexpression?