import Qq
open Qq Lean

def pairNat₁ (u : Level) (α : Q(Type u)) (a : Q($α)) : MetaM (Q($α × $α)) :=
  match u, α, a with  -- error: Type mismatch `Nat` isn't `Type u`
  | Level.zero, ~q(Nat), ~q($n) => return q(($n, $n))
  | _, _, _ => throwError "only supported for `Nat`"

def pairNat₂ (u : Level) (α : Q(Type u)) (a : Q($α)) : MetaM (Q($α × $α)) :=
  match (generalizing := true) u, α, a with
  | Level.zero, ~q(Nat), ~q($n) => return q(($n, $n))  -- error: invalid pattern
  | _, _, _ => throwError "only supported for `Nat`"

-- works but ugly
def pairNat₃ (u : Level) (α : Q(Type u)) (a : Q($α)) : MetaM (Q($α × $α)) :=
  match (generalizing := true) u with
  | Level.zero =>
    match α, a with
    | ~q(Nat), ~q($n) => return q(($n, $n))
    | _, _ => throwError "only supported for `Nat`"
  | _ => throwError "only supported for `Nat`"