Unexpected Qq behaviour with match

Stream: mathlib4

[Paul Lezeau]

This morning I came across the following rather unexpected behaviour with Qq - does anyone know what's happening here?

import Mathlib

open Lean Elab Meta Qq

run_meta do -- Error: unknown constant '_eval.match_1'
  let expr : Expr := q({(x, y) : ℕ × ℕ | x + y = 2})
  let expr' : Expr := q({x : ℕ × ℕ | x.fst + x.snd = 2})
  Lean.logInfo m!"{← isExprDefEq expr expr'}"

[Eric Wieser]

Note this works fine as

def foo : MetaM Unit := do
  let expr : Expr := q({(x, y) : ℕ × ℕ | x + y = 2})
  let expr' : Expr := q({x : ℕ × ℕ | x.fst + x.snd = 2})
  Lean.logInfo m!"{← isExprDefEq expr expr'}"

run_meta foo

suggesting that this might be an issue with run_meta instead