From ce12ecfe13bdeeb04734060ebec03f6acd6f27cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Sep 2022 18:50:49 -0700
Subject: [PATCH] fix: free variable collision at `LCNF/Specialize.lean`

---
 src/Lean/Compiler/LCNF/CompilerM.lean  |  4 ++++
 src/Lean/Compiler/LCNF/Specialize.lean | 14 ++++++++++++--
 tests/lean/run/simp1.lean              |  2 --
 3 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean
index 2c87157ead..6c4c26b9e6 100644
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/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`.
diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean
index 1918d3b348..77973e81d2 100644
--- a/src/Lean/Compiler/LCNF/Specialize.lean
+++ b/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
diff --git a/tests/lean/run/simp1.lean b/tests/lean/run/simp1.lean
index 88604e2257..559bf93981 100644
--- a/tests/lean/run/simp1.lean
+++ b/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}"