liftCommandElabM breaking namespace resolution?

Stream: metaprogramming / tactics

[Jozef Mikušinec]

Hi! I discovered that when I use liftCommandElabM with elab and resolveGlobalConstNoOverload, it seems to break namespace resolution. It looks like a bug to me, but my knowledge of metaprogramming is very shallow, so I wanted to ask here before reporting an issue in GitHub. Is the following expected?

import Lean

def Foo.ExampleDL := 42

elab "s3(" dl:ident ")" : term => do
  -- remove the `Lean.liftCommandElabM` to remove error below
  let _ ← Lean.liftCommandElabM (Lean.resolveGlobalConstNoOverload dl)
  return .const ``Nat []

#check s3(Foo.ExampleDL)

namespace Foo
-- "Unknown constant `ExampleDL`". Reproducible in https://live.lean-lang.org/
#check s3(ExampleDL)

[Robin Arnez]

That seems unintended, so please create an issue.

[Jozef Mikušinec]

Thanks. Reported here