unknown constant '_obj'

[nomeata]

I just ran into this. I fear this is yet another code generator bug (if so, maybe it’s at least useful to test the completeness of the fixes once we fix them.)

import Lean

open Lean Meta

def go : MetaM Unit := do
  for (_name, ci) in (← getEnv).constants do
    if ci.isTheorem then continue

    forallTelescope ci.type fun _xs _r => do
    --   -- unless r.isApp do return
    --   -- unless r.appFn!.isFVar do return
    --   -- dbg_trace f!"{name}"
      pure ()

/-- error: unknown constant '_obj' -/
#guard_msgs in
run_meta go

Version

Lean 4.16.0-nightly-2025-01-06

[nomeata]

Hmm, or maybe it’s another issue; if I add

    if name.isInternal then continue

after the for it seems to help.