feat: apply [specialize] before elaboration

This is a workaround. See new comment.
We need it for making aa9080e9e more effective.

library/Init/Lean/Attributes.lean

@@ -253,7 +253,7 @@ structure EnumAttributes (α : Type) :=
 (attrs : List AttributeImpl)
 (ext   : PersistentEnvExtension (Name × α) (NameMap α))
 
-def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) (validate : Environment → Name → α → Except String Unit := fun _ _ _ => Except.ok ()) : IO (EnumAttributes α) :=
+def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) (validate : Environment → Name → α → Except String Unit := fun _ _ _ => Except.ok ()) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO (EnumAttributes α) :=
 do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistentEnvExtension {
      name            := extName,
      addImportedFn   := fun _ => pure {},
@@ -264,9 +264,10 @@ do ext : PersistentEnvExtension (Name × α) (NameMap α) ← registerPersistent
      statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
    };
    let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
-     name  := name,
-     descr := descr,
-     add   := fun env decl args persistent => do
+     name            := name,
+     descr           := descr,
+     applicationTime := applicationTime,
+     add             := fun env decl args persistent => do
        unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
        unless (env.getModuleIdxFor decl).isNone $
          throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));

library/Init/Lean/Compiler/Specialize.lean

@@ -30,7 +30,17 @@ def mkSpecializeAttrs : IO (EnumAttributes SpecializeAttributeKind) :=
 registerEnumAttributes `specializeAttrs
   [(`specialize, "mark definition to always be inlined", SpecializeAttributeKind.specialize),
    (`nospecialize, "mark definition to never be inlined", SpecializeAttributeKind.nospecialize) ]
-  (fun env declName _ => checkIsDefinition env declName)
+  /- TODO: fix the following hack.
+     We need to use the following hack because the equation compiler generates auxiliary
+     definitions that are compiled before we even finish the elaboration of the current command.
+     So, if the current command is a `@[specialize] def foo ...`, we must set the attribute `[specialize]`
+     before we start elaboration, otherwise when we compile the auxiliary definitions we will not be
+     able to test whether `@[specialize]` has been set or not.
+     In the new equation compiler we should pass all attributes and allow it to apply them to auxiliary definitions.
+     In the current implementation, we workaround this issue by using functions such as `hasSpecializeAttrAux`.
+   -/
+  (fun env declName _ => Except.ok ())
+  AttributeApplicationTime.beforeElaboration
 
 @[init mkSpecializeAttrs]
 constant specializeAttrs : EnumAttributes SpecializeAttributeKind := arbitrary _