fix: free variable collision at LCNF/Specialize.lean

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -119,6 +119,10 @@ def eraseCodeDecl (decl : CodeDecl) : CompilerM Unit := do
   | .let decl => eraseLetDecl decl
   | .jp decl | .fun decl => eraseFunDecl decl
 
+def eraseDecl (decl : Decl) : CompilerM Unit := do
+  eraseParams decl.params
+  eraseCode decl.value
+
 /--
 A free variable substitution.
 We use these substitutions when inlining definitions and "internalizing" LCNF code into `CompilerM`.

src/Lean/Compiler/LCNF/Specialize.lean

@@ -295,9 +295,19 @@ Specialize `decl` using
 -/
 def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Expr)) (params : Array Param) (decls : Array CodeDecl) (levelParamsNew : List Name) : SpecializeM Decl := do
   let nameNew := decl.name ++ `_at_ ++ (← read).declName ++ (`spec).appendIndexAfter (← get).decls.size
-  go nameNew |>.run' {}
+  /-
+  Recall that we have just retrieved `decl` using `getDecl?`, and it may have free variable identifiers that overlap with the free-variables
+  in `params` and `decls` (i.e., the "closure").
+  Recall that `params` and `decls` are internalized, but `decl` is not.
+  Thus, we internalize `decl` before glueing these "pieces" together. We erase the internalized information after we are done.
+  -/
+  let decl ← decl.internalize
+  try
+    go decl nameNew |>.run' {}
+  finally
+    eraseDecl decl
 where
-  go (nameNew : Name) : InternalizeM Decl := do
+  go (decl : Decl) (nameNew : Name) : InternalizeM Decl := do
     let mut params ← params.mapM internalizeParam
     let decls ← decls.mapM internalizeCodeDecl
     for param in decl.params, arg in argMask do

tests/lean/run/simp1.lean

@@ -29,8 +29,6 @@ axiom aux {α} (f : List α → List α) (xs ys : List α) : f (xs ++ ys) ++ []
 open Lean
 open Lean.Meta
 
-#eval 1 -- TODO: remove, this is a workaround to make sure then next eval works.
-
 def tst1 : MetaM Unit := do
   let thms  ← Meta.getSimpTheorems
   trace[Meta.debug] "{thms.pre}\n-----\n{thms.post}"