From d0f8eb7bd6a2b765354aeb19058fa90836d4c791 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 23 Feb 2026 21:00:36 +0100 Subject: [PATCH] fix: `@[nospecialize]` is never template-like (#12663) This PR avoids false-positive error messages on specialization restrictions under the module system when the declaration is explicitly marked as not specializable. It could also provide some minor public size and rebuild savings. --- src/Lean/Compiler/LCNF/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index aa910edebb..77c085edf2 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -1017,7 +1017,7 @@ Return `true` if `decl` is supposed to be inlined/specialized. -/ def Decl.isTemplateLike (decl : Decl pu) : CoreM Bool := do let env ← getEnv - if ← hasLocalInst decl.type then + if !hasNospecializeAttribute env decl.name && (← hasLocalInst decl.type) then return true -- `decl` applications will be specialized else if (← isImplicitReducible decl.name) then return true -- `decl` is "fuel" for code specialization