perf: normalizeLevels

src/Lean/Level.lean

@@ -288,7 +288,7 @@ def normLtAux : Level → Nat → Level → Nat → Bool
 def normLt (l₁ l₂ : Level) : Bool :=
   normLtAux l₁ 0 l₂ 0
 
-private def isAlreadyNormalizedCheap : Level → Bool
+def isAlreadyNormalizedCheap : Level → Bool
   | zero    => true
   | param _ => true
   | mvar _  => true

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -182,10 +182,18 @@ def foldProjs (e : Expr) : MetaM Expr := do
       return .done e
   Meta.transform e (post := post)
 
+/-- Quick filter for checking whether we can skip `normalizeLevels`. -/
+private def levelsAlreadyNormalized (e : Expr) : Bool :=
+  Option.isNone <| e.find? fun
+    | .const _ us => us.any (! ·.isAlreadyNormalizedCheap)
+    | .sort u => !u.isAlreadyNormalizedCheap
+    | _ => false
+
 /--
 Normalizes universe levels in constants and sorts.
 -/
 def normalizeLevels (e : Expr) : CoreM Expr := do
+  if levelsAlreadyNormalized e then return e
   let pre (e : Expr) := do
     match e with
     | .sort u => return .done <| e.updateSort! u.normalize