From f798507bbf23ef3243c8c597f093fd9f03dbcfad Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 21 Dec 2022 10:46:52 -0800
Subject: [PATCH] chore: tc: only normalize level mvars at current depth

---
 src/Lean/Meta/SynthInstance.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 30d462973c..7d91774629 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -102,7 +102,7 @@ partial def normLevel (u : Level) : M Level := do
     | Level.max v w     => return u.updateMax! (← normLevel v) (← normLevel w)
     | Level.imax v w    => return u.updateIMax! (← normLevel v) (← normLevel w)
     | Level.mvar mvarId =>
-      if !(← isLevelMVarAssignable mvarId) then
+      if (← getMCtx).getLevelDepth mvarId != (← getMCtx).depth then
         return u
       else
         let s ← get