From 7308fa0e7d7ec9596b4c624e4dcd30ca1cbbc343 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Oct 2022 16:35:55 -0700
Subject: [PATCH] feat: ensure lambda lifter is creating unused names

---
 src/Lean/Compiler/LCNF/LambdaLifting.lean | 16 ++++++++++++----
 tests/lean/run/lcnf1.lean                 |  1 -
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/LambdaLifting.lean b/src/Lean/Compiler/LCNF/LambdaLifting.lean
index 06ee20382d..e17ce9fecc 100644
--- a/src/Lean/Compiler/LCNF/LambdaLifting.lean
+++ b/src/Lean/Compiler/LCNF/LambdaLifting.lean
@@ -35,6 +35,10 @@ structure State where
   New auxiliary declarations
   -/
   decls  : Array Decl := #[]
+  /--
+  Next index for generating auxiliary declaration name.
+  -/
+  nextIdx := 0
 
 /-- Monad for applying lambda lifting. -/
 abbrev LiftM := ReaderT Context (StateRefT State (ScopeT CompilerM))
@@ -55,16 +59,20 @@ def shouldLift (decl : FunDecl) : LiftM Bool := do
   else
     return true
 
+partial def mkAuxDeclName : LiftM Name := do
+  let nextIdx ← modifyGet fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1})
+  let nameNew := (← read).mainDecl.name ++ (← read).suffix.appendIndexAfter nextIdx
+  if (← getDecl? nameNew).isNone then return nameNew
+  mkAuxDeclName
+
 open Internalize in
 /--
 Create a new auxiliary declaration. The array `closure` contains all free variables
 occurring in `decl`.
 -/
 def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
-  let mainDecl := (← read).mainDecl
-  let nextIdx := (← get).decls.size
-  let nameNew := mainDecl.name ++ (← read).suffix.appendIndexAfter nextIdx
-  let auxDecl ← go nameNew mainDecl.safe |>.run' {}
+  let nameNew ← mkAuxDeclName
+  let auxDecl ← go nameNew (← read).mainDecl.safe |>.run' {}
   let us := auxDecl.levelParams.map mkLevelParam
   let auxDeclName ← match (← cacheAuxDecl auxDecl) with
   | .new =>
diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean
index fd1bc4e68c..e487ca8c4f 100644
--- a/tests/lean/run/lcnf1.lean
+++ b/tests/lean/run/lcnf1.lean
@@ -44,7 +44,6 @@ def Vec.head : Vec α (n+1) → α
 #eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]
 
 set_option profiler true
-set_option trace.Compiler.simp true
 #eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]
 
 def foo (a b : Nat) :=