diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean
index 574f11c86f87..ea81d1699684 100644
--- a/library/Init/Lean/TypeClass/Context.lean
+++ b/library/Init/Lean/TypeClass/Context.lean
@@ -282,7 +282,9 @@ partial def uAlphaNormalizeCore : Level → StateM AlphaNormData Level
 
 partial def eAlphaNormalizeCore : Expr → StateM AlphaNormData Expr
 | e =>
-  if e.isConst then pure e
+  if e.isConst then do
+    ls ← e.constLevels!.mapM uAlphaNormalizeCore;
+    pure $ Expr.updateConst! e ls
   else if e.isFVar then pure e
   else if !e.hasMVar then pure e
   else match e with