Poor elaboration performance on structure matches

[eric-wieser]

This takes a very long time to elaborate:

import Lean
import Qq

open Lean Qq

def ohNo : MetaM Unit := do
  let xx ← inferTypeQ q(False)
  let res ← match xx with
  | ⟨0, ~q(True), _⟩ => return
  | ⟨0, ~q(True), _⟩ => return
  | ⟨0, ~q(True), _⟩ => return
  | ⟨0, ~q(True), _⟩ => return
  | ⟨0, ~q(True), _⟩ => return
  | ⟨0, ~q(True), _⟩ => return
  | _ => return