kernel error caused by metavariables in mkAuxTheorem

Stream: lean4

[Eric Wieser]

Reduced from #lean4 > Kernel error in list index notation :

import Lean
import Qq

open Qq

run_meta do
  have l : Q(True) := ← Lean.Meta.mkFreshExprMVar q(True) (kind := .syntheticOpaque)
  withLocalDeclQ `h default q(True ∧ let := $l; True) fun x => do
    let e : Q(True) := q(($x).2)
    Lean.logInfo m!"before: {e}"
    -- works fine without this line
    let e ← Lean.Meta.mkAuxTheorem q(True) e (zetaDelta := true) -- or false, not really relevant
    Lean.logInfo m!"after: {e}"

gives

info: before: h.right
---
info: after: _proof_2 h ?m.1
---
error: (kernel) declaration has free variables '_private.«external:file:///MathlibDemo/MathlibDemo.lean».0._proof_2'

where the hover info for _proof_2 is

_proof_2 : (True ∧
    let this := _fvar.1002;
    True) →
  True → True

docs#Lean.Meta.mkAuxTheorem doesn't really make any strong promises about this in its docstring, but the module docstring claims:

This module provides functions for "closing" open terms and creating auxiliary definitions. Here, we say a term is "open" if it contains free/meta-variables.

which suggests that the metavariable should be handled

(Edit: filed as lean4#10705)

[Eric Wieser]

(Apologies for the Qq usage, building the term is more annoying without; but I don't think Qq is implicated here)

[Eric Wieser]

My hunch is that:

  let newLocalDecls := s.newLocalDecls.reverse ++ s.newLocalDeclsForMVars
  let newLetDecls   := s.newLetDecls.reverse
  let type  := mkForall newLocalDecls (mkForall newLetDecls type)
  let value := mkLambda newLocalDecls (mkLambda newLetDecls value)

is to blame, and in fact newLocalDeclsForMVars, newLetDecls, and newLocalDecls need to be interlaced in the order they are discovered

[Eric Wieser]

I think lean4#10704 is enough to resolve the notation overloading issue in the other thread, but leaves behind a performance bug in place of the behavior bug