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.
This commit is contained in:
Cameron Zwarich 2025-02-03 19:43:18 -08:00 committed by GitHub
parent 8b2a9cd74d
commit cb6adb0259
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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").