diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index 50eafd39e1..f8e70bc558 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -222,7 +222,7 @@ def mkCast (x : VarId) (xType : IRType) (expectedType : IRType) : M Expr := do
   | Arg.var x => castVarIfNeeded x expected (fun x => k (Arg.var x))
   | _         => k x
 
-@[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) := do
+def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) := do
   let mut xs' := #[]
   let mut bs  := #[]
   let mut i   := 0
diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean
index 81f74e1211..6f8f53a8aa 100644
--- a/src/Lean/Compiler/IR/FreeVars.lean
+++ b/src/Lean/Compiler/IR/FreeVars.lean
@@ -30,7 +30,7 @@ private def collectArg : Arg → Collector
   | Arg.var x  => collectVar x
   | irrelevant => skip
 
-@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
+private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
   fun m => as.foldl (fun m a => f a m) m
 
 private def collectArgs (as : Array Arg) : Collector := collectArray as collectArg
@@ -127,7 +127,7 @@ private def collectArg : Arg → Collector
   | Arg.var x  => collectVar x
   | irrelevant => skip
 
-@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
+private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector :=
   fun bv fv => as.foldl (fun fv a => f a bv fv) fv
 
 private def collectArgs (as : Array Arg) : Collector :=
diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean
index 1ef00ff116..363045c21e 100644
--- a/src/Lean/Compiler/IR/LiveVars.lean
+++ b/src/Lean/Compiler/IR/LiveVars.lean
@@ -98,7 +98,7 @@ private def collectArg : Arg → Collector
   | Arg.var x  => collectVar x
   | irrelevant => skip
 
-@[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun s =>
+private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun s =>
   as.foldl (fun s a => f a s) s
 
 private def collectArgs (as : Array Arg) : Collector :=
diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean
index 5a22dbe70c..151977efeb 100644
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/src/Lean/Compiler/IR/NormIds.lean
@@ -131,10 +131,10 @@ namespace MapVars
   | Arg.var x => Arg.var (f x)
   | a         => a
 
-@[specialize] def mapArgs (f : VarId → VarId) (as : Array Arg) : Array Arg :=
+def mapArgs (f : VarId → VarId) (as : Array Arg) : Array Arg :=
   as.map (mapArg f)
 
-@[specialize] def mapExpr (f : VarId → VarId) : Expr → Expr
+def mapExpr (f : VarId → VarId) : Expr → Expr
   | Expr.ctor c ys      => Expr.ctor c (mapArgs f ys)
   | Expr.reset n x      => Expr.reset n (f x)
   | Expr.reuse x c u ys => Expr.reuse (f x) c u (mapArgs f ys)
@@ -150,7 +150,7 @@ namespace MapVars
   | Expr.isTaggedPtr x  => Expr.isTaggedPtr (f x)
   | e@(Expr.lit v)      =>  e
 
-@[specialize] partial def mapFnBody (f : VarId → VarId) : FnBody → FnBody
+partial def mapFnBody (f : VarId → VarId) : FnBody → FnBody
   | FnBody.vdecl x t v b         => FnBody.vdecl x t (mapExpr f v) (mapFnBody f b)
   | FnBody.jdecl j ys v b        => FnBody.jdecl j ys (mapFnBody f v) (mapFnBody f b)
   | FnBody.set x i y b           => FnBody.set (f x) i (mapArg f y) (mapFnBody f b)
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index a715be72d5..a291a392b5 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -81,7 +81,6 @@ private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool :=
 
 /- Return true if `x` also occurs in `ys` in a position that is not consumed.
    That is, it is also passed as a borrow reference. -/
-@[specialize]
 private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool :=
   ys.size.any fun i =>
     let y := ys[i]
@@ -97,7 +96,6 @@ Return `n`, the number of times `x` is consumed.
 - `ys` is a sequence of instruction parameters where we search for `x`.
 - `consumeParamPred i = true` if parameter `i` is consumed.
 -/
-@[specialize]
 private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Nat :=
   ys.size.fold (init := 0) fun i n =>
     let y := ys[i]
@@ -105,7 +103,6 @@ private def getNumConsumptions (x : VarId) (ys : Array Arg) (consumeParamPred :
     | Arg.irrelevant => n
     | Arg.var y      => if x == y && consumeParamPred i then n+1 else n
 
-@[specialize]
 private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : Nat → Bool) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody :=
   xs.size.fold (init := b) fun i b =>
     let x := xs[i]
diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean
index 89f1eaada5..8bc9ab0837 100644
--- a/src/Lean/Data/Json/Printer.lean
+++ b/src/Lean/Data/Json/Printer.lean
@@ -44,7 +44,7 @@ def renderString (s : String) : String :=
   "\"" ++ escape s ++ "\""
 
 section
-@[specialize]
+
 partial def render : Json → Format
   | null       => "null"
   | bool true  => "true"
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 502d3addc8..c8d32f357b 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -182,7 +182,7 @@ private partial def isDefEqArgsFirstPass
       pure (some postponed)
   loop 0 #[]
 
-@[specialize] private def trySynthPending (e : Expr) : MetaM Bool := do
+private def trySynthPending (e : Expr) : MetaM Bool := do
   let mvarId? ← getStuckMVar? e
   match mvarId? with
   | some mvarId => Meta.synthPending mvarId
diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean
index 48086e85db..e52895984b 100644
--- a/src/Lean/Util/FindExpr.lean
+++ b/src/Lean/Util/FindExpr.lean
@@ -28,7 +28,7 @@ unsafe def visited (e : Expr) (size : USize) : FindM Bool := do
     modify fun s => { keys := s.keys.uset i e lcProof }
     pure false
 
-@[specialize] unsafe def findM? (p : Expr → Bool) (size : USize) (e : Expr) : OptionT FindM Expr :=
+unsafe def findM? (p : Expr → Bool) (size : USize) (e : Expr) : OptionT FindM Expr :=
   let rec visit (e : Expr) := do
     if (← visited e size)  then
       failure
@@ -48,7 +48,7 @@ unsafe def visited (e : Expr) (size : USize) : FindM Bool := do
 unsafe def initCache : State :=
   { keys    := mkArray cacheSize.toNat (cast lcProof ()) }
 
-@[inline] unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
+unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
   Id.run <| findM? p cacheSize e |>.run' initCache
 
 end FindImpl
diff --git a/src/Lean/Util/FindLevelMVar.lean b/src/Lean/Util/FindLevelMVar.lean
index 291e8d2766..06bc4e7ff9 100644
--- a/src/Lean/Util/FindLevelMVar.lean
+++ b/src/Lean/Util/FindLevelMVar.lean
@@ -15,7 +15,6 @@ mutual
   partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
     if s.isSome || !e.hasLevelMVar then s else main p e s
 
-  @[specialize]
   partial def main (p : MVarId → Bool) : Expr → Visitor
     | Expr.sort l _        => visitLevel p l
     | Expr.const _ ls _    => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
@@ -30,7 +29,6 @@ mutual
   partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s =>
     if s.isSome || !l.hasMVar then s else mainLevel p l s
 
-  @[specialize]
   partial def mainLevel (p : MVarId → Bool) : Level → Visitor
     | Level.zero _        => id
     | Level.succ l _      => visitLevel p l
diff --git a/src/Lean/Util/FindMVar.lean b/src/Lean/Util/FindMVar.lean
index 4d18130a1f..c135f28c93 100644
--- a/src/Lean/Util/FindMVar.lean
+++ b/src/Lean/Util/FindMVar.lean
@@ -15,7 +15,6 @@ mutual
   partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
     if s.isSome || !e.hasMVar then s else main p e s
 
-  @[specialize]
   partial def main (p : MVarId → Bool) : Expr → Visitor
     | Expr.proj _ _ e _    => visit p e
     | Expr.forallE _ d b _ => visit p b ∘ visit p d
diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean
index 8364a12428..eeef6fcde2 100644
--- a/src/Lean/Util/FoldConsts.lean
+++ b/src/Lean/Util/FoldConsts.lean
@@ -18,7 +18,6 @@ structure State where
 
 abbrev FoldM := StateM State
 
-@[inline]
 unsafe def visited (e : Expr) (size : USize) : FoldM Bool := do
   let s ← get
   let h := ptrAddrUnsafe e
@@ -29,7 +28,6 @@ unsafe def visited (e : Expr) (size : USize) : FoldM Bool := do
     modify $ fun s => { s with visitedTerms := s.visitedTerms.uset i e lcProof }
     pure false
 
-@[specialize]
 unsafe def fold {α : Type} (f : Name → α → α) (size : USize) (e : Expr) (acc : α) : FoldM α :=
   let rec visit (e : Expr) (acc : α) : FoldM α := do
     if (← visited e size) then
diff --git a/src/Lean/Util/ForEachExpr.lean b/src/Lean/Util/ForEachExpr.lean
index efd97b5947..7ebdb2dd49 100644
--- a/src/Lean/Util/ForEachExpr.lean
+++ b/src/Lean/Util/ForEachExpr.lean
@@ -15,7 +15,7 @@ addresses. Note that the following code is parametric in a monad `m`.
 
 variable {ω : Type} {m : Type → Type} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m]
 namespace ForEachExpr
-@[specialize] partial def visit (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Unit :=
+partial def visit (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Unit :=
   checkCache e fun _ => do
     if (← g e) then
       match e with
diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean
index 152cb9dcb2..bae633c964 100644
--- a/src/Lean/Util/ReplaceExpr.lean
+++ b/src/Lean/Util/ReplaceExpr.lean
@@ -18,12 +18,12 @@ structure State where
 
 abbrev ReplaceM := StateM State
 
-@[inline] unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
+unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
   modify fun ⟨keys, results⟩ => { keys := keys.uset i key lcProof, results := results.uset i result lcProof };
   pure result
 
-@[inline] unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) (e : Expr) : ReplaceM Expr := do
-  let rec @[specialize] visit (e : Expr) := do
+unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) (e : Expr) : ReplaceM Expr := do
+  let rec visit (e : Expr) := do
     let c ← get
     let h := ptrAddrUnsafe e
     let i := h % size
@@ -45,7 +45,7 @@ unsafe def initCache : State :=
   { keys    := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
     results := mkArray cacheSize.toNat default }
 
-@[inline] unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
+unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
   (replaceUnsafeM f? cacheSize e).run' initCache
 
 end ReplaceImpl
diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean
index d7de7dd948..10629e4b45 100644
--- a/src/Lean/Util/ReplaceLevel.lean
+++ b/src/Lean/Util/ReplaceLevel.lean
@@ -31,11 +31,11 @@ structure State where
 
 abbrev ReplaceM := StateM State
 
-@[inline] unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
+unsafe def cache (i : USize) (key : Expr) (result : Expr) : ReplaceM Expr := do
   modify fun s => { keys := s.keys.uset i key lcProof, results := s.results.uset i result lcProof };
   pure result
 
-@[specialize] unsafe def replaceUnsafeM (f? : Level → Option Level) (size : USize) (e : Expr) : ReplaceM Expr := do
+unsafe def replaceUnsafeM (f? : Level → Option Level) (size : USize) (e : Expr) : ReplaceM Expr := do
   let rec visit (e : Expr) := do
     let c ← get
     let h := ptrAddrUnsafe e
@@ -58,7 +58,7 @@ unsafe def initCache : State :=
   { keys    := mkArray cacheSize.toNat (cast lcProof ()), -- `()` is not a valid `Expr`
     results := mkArray cacheSize.toNat default }
 
-@[inline] unsafe def replaceUnsafe (f? : Level → Option Level) (e : Expr) : Expr :=
+unsafe def replaceUnsafe (f? : Level → Option Level) (e : Expr) : Expr :=
   (replaceUnsafeM f? cacheSize e).run' initCache
 
 end ReplaceLevelImpl
diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean
index 887e2926d9..b5de260964 100644
--- a/src/Lean/Util/SCC.lean
+++ b/src/Lean/Util/SCC.lean
@@ -79,7 +79,7 @@ private def addSCC (a : α) : M α Unit := do
         modify fun s => { s with stack := bs, sccs := newSCC :: s.sccs }
   add (← get).stack []
 
-@[specialize] private partial def sccAux (successorsOf : α → List α) (a : α) : M α Unit := do
+private partial def sccAux (successorsOf : α → List α) (a : α) : M α Unit := do
   push a
   (successorsOf a).forM fun b => do
     let bData ← getDataOf b;
@@ -98,7 +98,7 @@ private def addSCC (a : α) : M α Unit := do
   if aData.lowlink? == aData.index? then
     addSCC a
 
-@[specialize] def scc (vertices : List α) (successorsOf : α → List α) : List (List α) :=
+def scc (vertices : List α) (successorsOf : α → List α) : List (List α) :=
   let main : M α Unit := vertices.forM fun a => do
     let aData ← getDataOf a
     if aData.index?.isNone then sccAux successorsOf a