From cb6adb02594cbaef0394ea7b4f1f2c94aa8b0df2 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Mon, 3 Feb 2025 19:43:18 -0800 Subject: [PATCH] fix: don't strip macro scopes in names of specialized LCNF decls (#6930) This PR changes the name generation of specialized LCNF decls so they don't strip macro scopes. This avoids name collisions for specializations created in distinct macro scopes. Since the normal Name.append function checks for the presence of macro scopes, we need to use appendCore. --- src/Lean/Compiler/LCNF/Specialize.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 390eefb2b7..2c01478708 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -208,7 +208,7 @@ Specialize `decl` using - `levelParamsNew`: the universe level parameters for the new declaration. -/ def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Arg)) (params : Array Param) (decls : Array CodeDecl) (levelParamsNew : List Name) : SpecializeM Decl := do - let nameNew := decl.name ++ `_at_ ++ (← read).declName.eraseMacroScopes ++ (`spec).appendIndexAfter (← get).decls.size + let nameNew := decl.name.appendCore `_at_ |>.appendCore (← read).declName |>.appendCore `spec |>.appendIndexAfter (← get).decls.size /- 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").