fix: correct matching on sigma types

[eric-wieser]

No description provided.

[gebner]

Oh wow, this must've been broken since the removal of the implicit pure coercion... Thank you so much for fixing this!

[eric-wieser]

It would be cool if

/-- Given `x + y` of Nat, returns `(x, y)`. Otherwise fail. -/
def getNatAdd (e : Expr) : MetaM (Option (Q(Nat) × Q(Nat))) := do
  let ⟨_, ~q(Nat), ~q($a + $b)⟩ ← inferTypeQ e | return none
  return some (a, b)

worked, but that would need a more cooperative elaboration order