Unification and meta-variables in mkAppM'

Stream: lean4

[Siddhartha Gadgil]

I have been experimenting with various meta stuff using elaboration, and I do not understand why the following does not work (though many variants work). I would be grateful if this can be explained.

Firstly, stuff that works (which I use)

def self {α : Type}(a: α ) : α  := a

def selfAppM : MetaM Expr :=
  do
    let e ← mkAppM' (mkConst `self) #[mkConst `Nat.zero]
    return e

#eval selfAppM

Now I try to call this with some syntax to allow input of terms (without implicit variables this works fine).

syntax (name := tryapp) term ">>>>>" term : term

@[termElab tryapp] def tryappImpl : TermElab :=
fun stx expectedType? =>
  match stx with
  | `($s >>>>> $t) =>
    do
      let f <- elabTerm s none
      let x <- elabTerm t none
      let expr : Expr ←  mkAppM' f #[x]
      return expr
  | _ => Elab.throwIllFormedSyntax

def one := Nat.succ >>>>> Nat.zero
#eval one  -- gives 1 as expected

However, the following does not work

#eval self >>>>> Nat.zero

giving the error

Egs2.lean:69:6
application type mismatch
  self zero
argument
  zero
has type
  Nat : Type
but is expected to have type
  ?m.2597 : Type
Egs2.lean:69:0
failed to synthesize
  MetaEval ?α

My question is why is the meta-variable not being unified with Nat? Is it that there is already an error when self needs a meta-variable, or is it that a meta-variable is generated but is of a type that is not unified?

Thanks.

[Siddhartha Gadgil]

I checked that if I return x after generating f but not the application, there is no error. So it seems to be unification that fails.

[Leonardo de Moura]

It is great to see you trying to write your own elaborators. We don't have documentation for the internal APIs yet. The elaborators that come with Lean are the best "documentation" so far.

We use themkAppM functions in the AppBuilder module for constructing auxiliary applications in meta code. For example, we use them in the simplifier for constructing funext applications, congruence proofs, etc. The mkAppM functions provide the following functionality for us: infer implicit arguments using typing constraints and type class inference. Moreover, they guarantee that no new metavariable is introduced in the resulting expression. They also do not assign metavariables that were created before we invoke mkAppM. The mkAppM functions are not elaboration functions, and they don't implement a lot of the functionality that is expected during elaboration: coercions, default parameter values, auto parameters (with tactics), etc.

Your example fails because when you elaborate s, the term @self ?m is produced, and mkAppM' will not assign the metavariable ?m since it was created before you invoked it.

In the elaborator, you can use the elabAppArgs function when you want to control the elaboration order in an application.
The file src/Lean/Elab/Extra.lean contains a few examples. In your example, you could write

@[termElab tryapp] def tryappImpl : TermElab :=
fun stx expectedType? =>
  match stx with
  | `($s >>>>> $t) =>
    do
      let f <- elabTerm s none
      let x <- elabTerm t none
      let expr ← elabAppArgs f #[] #[Arg.expr x] expectedType? (explicit := false) (ellipsis := false)
      return expr
  | _ => Elab.throwIllFormedSyntax

The elabAppArgs can take named arguments, arguments that have not been elaborated yet (i.e., Syntax), etc.