From 675bebb446295263cf706d430204e136a04d0d75 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 Apr 2021 10:27:14 -0700
Subject: [PATCH] fix: `isLevelDefEq` missing case

---
 src/Lean/Meta/LevelDefEq.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 17d734a08a..66b738bdd9 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -84,6 +84,7 @@ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
   let ref ← getRef
   let ctx ← read
+  trace[Meta.isLevelDefEq.stuck] "{lhs} =?= {rhs}"
   modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs, ref := ref, ctx? := ctx.defEqCtx? }
 
 mutual
@@ -107,7 +108,9 @@ mutual
       Bool.toLBool <$> isLevelDefEqAux levelZero v₂
     | Level.zero _, Level.succ .. => return LBool.false
     | Level.succ u _, v =>
-      if u.isMVar && u.occurs v then
+      if v.isParam then
+        return LBool.false
+      else if u.isMVar && u.occurs v then
         return LBool.undef
       else
         match (← Meta.decLevel? v) with