LocalDecl not recognized in MVar

Stream: metaprogramming / tactics

[nrs]

In the following #mwe, I declare an fvar sig of type Signature, and then a goal of type SigSingleton sig. However, the goal created a dagger name instead of using the sig I declared. What might be causing this? (also, let goal <- mkFreshExprMVar (<- TermElabM.run' do elabTerm (<- ... seems somewhat verbose, is this idiomatic?)

import Mathlib
open Lean Meta Elab Command Term

structure Signature where
  α : Type
  β : α -> Type

inductive SigSingleton (sig : Signature)
| mk : SigSingleton sig

def c : CoreM Unit := do
  let result <- MetaM.run' (α := Unit) do
    withLocalDecl `sig .default (mkConst `Signature) fun _ => do
    let goal <- mkFreshExprMVar (<- TermElabM.run' do elabTerm (<- `(SigSingleton sig)) (Expr.sort levelOne))
    goal.mvarId!.withContext do
      (<- getLCtx).forM fun decl => do
        logInfo f!"localdecl: name: {decl.userName}; type: {<- inferType decl.toExpr}"

#eval c
-- localdecl: name: sig; type: Signature
-- unknown constant 'sig✝'

[nrs]

ah, manually declaring the expr with let goal <- mkFreshExprMVar <| mkApp (.const ``SigSingleton .nil) (.const ``sig .nil) seems to fix the issue. Is the call to TermElabM.run' putting the sig name out of context? If so, is there a way to pass the relevant context?

[Eric Wieser]

Did you mean to write fun sig instead of fun _?

[Eric Wieser]

I think this is a better way to write what you want:

open Qq
def c : CoreM Unit := do
  let result <- MetaM.run' (α := Unit) do
    withLocalDeclQ `sig .default q(Signature) fun sig => do
    let goal <- mkFreshExprMVarQ q(SigSingleton $sig)
    goal.mvarId!.withContext do
      (<- getLCtx).forM fun decl => do
        logInfo m!"localdecl: name: {Expr.fvar decl.fvarId}; type: {<- inferType decl.toExpr}"

[nrs]

Did you mean to write fun sig instead of fun _?

Oh I didn't realize I needed to explicitly pass the Expr variable, I thought it would be recognized through it's LocalDecl name sig, thanks! And thanks a lot for that example, very helpful!!

[Eric Wieser]

nrs said:

I thought it would be recognized through it's LocalDecl name sig,

I think the sig inside `( ) has hygiene considerations, so does not match the variable you asked to be called `sig

[Eric Wieser]

In your version you could have used `(SigSingleton $(sig.toSyntax)) I think

[Kyle Miller]

def c : CoreM Unit := do
  let result <- MetaM.run' (α := Unit) do
    let sig := mkIdent `sig
    withLocalDecl sig.getId .default (mkConst `Signature) fun _ => do
    let goal <- mkFreshExprMVar (<- TermElabM.run' do elabTerm (<- `(SigSingleton $sig)) (Expr.sort levelOne))
    goal.mvarId!.withContext do
      (<- getLCtx).forM fun decl => do
        logInfo f!"localdecl: name: {decl.userName}; type: {<- inferType decl.toExpr}"

#eval c
-- localdecl: name: sig; type: Signature

[nrs]

Eric Wieser

I think the sig inside () has hygiene considerations, so does not match the variable you asked to be called sig

ah makes a lot of sense! thanks a lot! haven't encountered Qq before, am browsing around a bit to see what it's about, thanks for that reference too

[Kyle Miller]

All this Meta.run and TermElabM.run is fairly nonstandard. Why not stick with TermElabM?

def c : TermElabM Unit := do
  let result <- do
    let sig := mkIdent `sig
    withLocalDeclD sig.getId (mkConst `Signature) fun _ => do
    let goal <- mkFreshExprMVar (<- elabTerm (<- `(SigSingleton $sig)) none)
    goal.mvarId!.withContext do
      (<- getLCtx).forM fun decl => do
        logInfo f!"localdecl: name: {decl.userName}; type: {<- inferType decl.toExpr}"

#eval c
-- localdecl: name: sig; type: Signature

[Eric Wieser]

Though using Qq lets you stay in MetaM without needing TermElabM at all!

[Kyle Miller]

Here's the core Lean version of what the Qq version is doing:

def c : MetaM Unit := do
  let result <- do
    withLocalDeclD `sig (mkConst `Signature) fun sig => do
    let goal <- mkFreshExprMVar (<- mkAppM ``SigSingleton #[sig])
    goal.mvarId!.withContext do
      (<- getLCtx).forM fun decl => do
        logInfo f!"localdecl: name: {decl.userName}; type: {<- inferType decl.toExpr}"

#eval c
-- localdecl: name: sig; type: Signature

[nrs]

@Kyle Miller hm right thanks a lot for the examples, these are extremely useful, highly appreciated! I'm debugging why a metavariable is failing to isDefEq by virtue of being unassignable, so I'm trying to simulate the metavar context in MetaM. Should I stick to TermElabM?

[Kyle Miller]

though mkAppM is doing checking at runtime rather than compile time

[Kyle Miller]

If you think you have a strong enough understanding to debug Lean by simulating part of it, and you fully understand that using these run functions means that you're getting some default configuration, then go ahead, but I imagine there are easier ways to figure out what's going on.

[nrs]

hm right... I will instead build a super simplified example with the references provided here for educational purposes and will go back to trying to find a different way to debug that, thanks for the recommendations!