Elaborating binder with a pattern

Stream: lean4

[Tomas Skrivan]

I'm having trouble with elaborating a binder that contains a pattern e.g. (h : FunProp (λ (x,y) => f x y)). Elaborating (h : FunProp (λ p : Nat×Nat => f p.1 p.2)) works fine, but the λ (x,y) => trips elaboration for some reason.

I do not know how this pattern matching works internally so I'm a bit lost on what to do about this. What am I doing wrong here?

mwe:

import Lean

open Lean Elab Meta

syntax "#check_binders" bracketedBinder* : command

elab_rules : command
| `(#check_binders $xs*) => do

  Command.liftTermElabM  do

    Term.elabBinders xs λ contextVars => do
      for x in contextVars do
        if x.hasMVar || (← instantiateMVars (←inferType x)).hasMVar then
          throwError s!"({← ppExpr x} : {← ppExpr (← inferType x)}) contains meta variables!"

      let vars ← contextVars.mapM λ x => do pure s!"{← ppExpr x} : {← ppExpr (← instantiateMVars (← inferType x))}"
      IO.println s!"binders: {vars}"

set_option linter.unusedVariables false

def FunProp (f : α → β) : Prop := True

#check_binders (f : Nat → Nat) -- binders: #[f : Nat → Nat]
#check_binders (f : Nat → Nat) (h : FunProp f) -- binders: #[f : Nat → Nat, h : FunProp f]
#check_binders (f : Nat → Nat → Nat) (h : FunProp (λ p : Nat×Nat => f p.1 p.2)) -- binders: #[f : Nat → Nat → Nat, h : FunProp fun p => f p.fst p.snd]

#check_binders (f : Nat → Nat → Nat) (h : FunProp (λ (x,y) => f x y)) -- Error: (h : FunProp fun x => ?m.6569 x) contains meta variables!