Elaborator and @

Stream: lean4

[Leni Aniva]

Suppose we have

  let e ← match Parser.runParserCategory
    (env := <- MonadEnv.getEnv)
    (catName := `term)
    (input := "Nat.brecOn")
    (fileName := "<stdin>") with
    | .ok syn => pure syn
    | .error error => throwError error
  let e <- Elab.elabTerm e .none

The inferred type of e is a metavariable, but if I replace Nat.brecOn with @Nat.brecOn, the inferred type becomes the full type of Nat.brecOn. How can I enforce this effect during elaboration? I remember in one of the tactics this @ effect is enforced, but I forgot which one

[Leni Aniva]

According to the documentation:

/--
  Main function for elaborating terms.
  It extracts the elaboration methods from the environment using the node kind.
  Recall that the environment has a mapping from `SyntaxNodeKind` to `TermElab` methods.
  It creates a fresh macro scope for executing the elaboration method.
  All unlogged trace messages produced by the elaboration method are logged using
  the position information at `stx`. If the elaboration method throws an `Exception.error` and `errToSorry == true`,
  the error is logged and a synthetic sorry expression is returned.
  If the elaboration throws `Exception.postpone` and `catchExPostpone == true`,
  a new synthetic metavariable of kind `SyntheticMVarKind.postponed` is created, registered,
  and returned.
  The option `catchExPostpone == false` is used to implement `resumeElabTerm`
  to prevent the creation of another synthetic metavariable when resuming the elaboration.

  If `implicitLambda == false`, then disable implicit lambdas feature for the given syntax, but not for its subterms.
  We use this flag to implement, for example, the `@` modifier. If `Context.implicitLambda == false`, then this parameter has no effect.
  -/
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
  withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx

I tried to pass in implicitLambda := true/false but the result is the same. The elaboration generates a metavariable when there is no @.

[Kyle Miller]

implicitLambda is for @fun ... vs fun ...

Do you know about Elab.elabAppArgs?

[Leni Aniva]

Kyle Miller said:

implicitLambda is for @fun ... vs fun ...

Do you know about Elab.elabAppArgs?

yes, but I don't know how to use it in this case

[Leni Aniva]

If I run the elaboration monad in withoutHeedElabAsElim

/--
  Execute `x` without heeding the `elab_as_elim` attribute. Useful when there is
  no expected type (so `elabAppArgs` would fail), but expect that the user wants
  to use such constants.
-/
def withoutHeedElabAsElim [MonadFunctorT TermElabM m] : m α → m α :=
  monadMap (m := TermElabM) withoutHeedElabAsElimImp

The type of the elaborated symbol becomes

(t : Nat) → ((t : Nat) → Nat.below t → ?m.67 t) → ?m.67 t

which is almost correct except for that the motive argument is missing. The documentation of this function says without expected type (which is my use caes),elabAppArgs would fail, but I still can't replicate the behaviour of @Nat.brecOn

[Leni Aniva]

Kyle Miller said:

implicitLambda is for @fun ... vs fun ...

Do you know about Elab.elabAppArgs?

I don't think I can use this function since I in this use case I don't have the arguments to Nat.brecOn when I'm calling it. I just want to determine the type of this expression in context

[Leni Aniva]

This is a MWE. I read in Elab/Term.lean that the automatic insertion of metavariables is related to autoBoundImplicit but disabling it in the elaboration context did not do anything:

import Lean
open Lean

def parseTerm (s: String): CoreM Syntax := do
  match Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := s)
    (fileName := "<stdin>") with
  | .ok s => return s
  | .error e => throwError e

def termElabM : Elab.TermElabM Unit := do
  let expr := "Nat.brecOn"
  let expr  ← Elab.Term.elabTerm (← parseTerm expr) (expectedType? := .none)
  let type ← Meta.inferType expr
  IO.println s!"{← Meta.ppExpr expr}"
  IO.println s!"  : {← Meta.ppExpr type}"

  let unassigned ← Elab.Term.collectUnassignedMVars type
  for mvarId in unassigned do
    let mvarType ← Meta.inferType mvarId
    IO.println s!"{← Meta.ppExpr mvarId}: {← Meta.ppExpr mvarType}"

def main : IO Unit := do
  let options: Options := {}
  let options := options.setNat `pp.deepTerms.threshold 100
  let options := options.setNat `pp.proofs.threshold 100
  let env: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  let termElabContext: Elab.Term.Context :=  {
    heedElabAsElim := false,
    declName? := `sandbox,
    errToSorry := false
  }
  let coreM := Meta.MetaM.run' <| Elab.Term.TermElabM.run' (ctx := termElabContext) termElabM
  let coreContext: Lean.Core.Context := {
    options,
    currNamespace := `Example
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0] }
  }
  match ← (coreM.run' coreContext { env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok _ => return ()

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I guess you are not in a situation where you can simply prepend @ to whatever your input is?

[Leni Aniva]

Wojciech Nawrocki said:

I guess you are not in a situation where you can simply prepend @ to whatever your input is?

The input is user supplied so I don't have control over it

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

What kinds of inputs are allowed? If the input is someConstant, you could prepend @. Is someConstant arg allowed? In that case, should Lean also not put in any metavariables in the inferred type? For instance if someConstant (a : Nat) {b : Nat} (c : Nat) : a = b := sorry, do you expect someConstant arg : ∀ {b : Nat}, Nat → 2 = b (which you'd normally get from @someConstant arg?

[Leni Aniva]

Wojciech Nawrocki said:

What kinds of inputs are allowed? If the input is someConstant, you could prepend @. Is someConstant arg allowed? In that case, should Lean also not put in any metavariables in the inferred type? For instance if someConstant (a : Nat) {b : Nat} (c : Nat) : a = b := sorry, do you expect someConstant arg : ∀ {b : Nat}, Nat → 2 = b (which you'd normallly get from @someConstant arg?

Yes. The goal here is to not generate any metavariables and infer the type signature of the input

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

There might be an option in the elaborator that achieves this exact behavior, but I'm not sure what it is. How about traversing the Term's syntax and prepending the @ to the head function symbol that way?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

To be sure, this would break on any custom syntax like infix operators.

[Robert Maxton]

Leni Aniva said:

Suppose we have

  let e ← match Parser.runParserCategory
    (env := <- MonadEnv.getEnv)
    (catName := `term)
    (input := "Nat.brecOn")
    (fileName := "<stdin>") with
    | .ok syn => pure syn
    | .error error => throwError error
  let e <- Elab.elabTerm e .none

The inferred type of e is a metavariable, but if I replace Nat.brecOn with @Nat.brecOn, the inferred type becomes the full type of Nat.brecOn. How can I enforce this effect during elaboration? I remember in one of the tactics this @ effect is enforced, but I forgot which one

As a side note, if all you want is to a real type instead of a metavariable, you can also use docs#Lean.instantiateMVars or docs#Qq.instantiateMVarsQ as needed.

[Leni Aniva]

Robert Maxton said:

Leni Aniva said:

Suppose we have

  let e ← match Parser.runParserCategory
    (env := <- MonadEnv.getEnv)
    (catName := `term)
    (input := "Nat.brecOn")
    (fileName := "<stdin>") with
    | .ok syn => pure syn
    | .error error => throwError error
  let e <- Elab.elabTerm e .none

The inferred type of e is a metavariable, but if I replace Nat.brecOn with @Nat.brecOn, the inferred type becomes the full type of Nat.brecOn. How can I enforce this effect during elaboration? I remember in one of the tactics this @ effect is enforced, but I forgot which one

As a side note, if all you want is to a real type instead of a metavariable, you can also use docs#Lean.instantiateMVars or docs#Qq.instantiateMVarsQ as needed.

I tried calling instantiateMVars on the mvar produced by elabTerm but it had no effect