unknown free variable: _kernel_fresh.1210

[nomeata]

Prerequisites

I stumbled upon this while working on lean, this is what I minimized it to so far:

import Lean

open Lean Meta

opaque foo : MetaM Unit

-- unknown free variable: _kernel_fresh.1210
partial def bar : MetaM Unit := do -- doesn't happen with IO here
  let nonIndices : Array Unit := #[].filter (fun i => true) -- doesn't happen without filter here
  for i in nonIndices do
    try
      foo -- needs this foo, pure () is not enough
      return
    catch e => pure () -- needs pure here, return doesnt work

Could be a duplicate of #1415 or #4418, but it is hard to tell without a full investigation, so reporting separately to avoid confusion if a fix ends up fixing one some of these instances.

Versions

4.9.0-rc2, 4.10.0-nightly-2024-06-23,
[Output of #eval Lean.versionString]
[OS version, if not using live.lean-lang.org.]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Ah, adding some mostly unrelated lines to my function makes the error go away. So I'm at least unblocked.

[leodemoura]

We can confirm that is a code generator issue by using noncomputable

[JLimperg]

Probably another instance of this bug, minimised from some Aesop code:

import Lean

open Lean Lean.Parser.Tactic

/-
unknown free variable: _kernel_fresh.134
-/
def foo {m} [Monad m] [MonadQuotation m] (tacs : Array (TSyntax `tactic)) (ns : Array Ident) (b : Bool) : m Syntax := do
  let usedNames : HashSet Name := tacs[1:].foldl (init := sorry) sorry
  for n in ns do
    if usedNames.contains sorry then
      continue
  if b then
    let tacs : TSyntax ``tacticSeq ← `(tacticSeq| $tacs:tactic*)
    sorry
  else
    sorry