feat: add isLevelDefEqStuck exception

src/Init/Lean/Meta/Exception.lean

@@ -29,7 +29,8 @@ inductive Exception
 | invalidProjection    (structName : Name) (idx : Nat) (s : Expr) (ctx : ExceptionContext)
 | revertFailure        (toRevert : Array Expr) (decl : LocalDecl) (ctx : ExceptionContext)
 | readOnlyMVar         (mvarId : MVarId) (ctx : ExceptionContext)
-| isDefEqStuck         (t s : Expr) (ctx : ExceptionContext)
+| isLevelDefEqStuck    (u v : Level) (ctx : ExceptionContext)
+| isExprDefEqStuck     (t s : Expr) (ctx : ExceptionContext)
 | letTypeMismatch      (fvarId : FVarId) (ctx : ExceptionContext)
 | appTypeMismatch      (f a : Expr) (ctx : ExceptionContext)
 | bug                  (b : Bug) (ctx : ExceptionContext)
@@ -51,7 +52,8 @@ def toStr : Exception → String
 | invalidProjection _ _ _ _     => "invalid projection"
 | revertFailure _ _ _           => "revert failure"
 | readOnlyMVar _ _              => "try to assign read only metavariable"
-| isDefEqStuck _ _ _            => "isDefEq is stuck"
+| isLevelDefEqStuck _ _ _       => "isDefEq is stuck"
+| isExprDefEqStuck _ _ _        => "isDefEq is stuck"
 | letTypeMismatch _ _           => "type mismatch at let-expression"
 | appTypeMismatch _ _ _         => "application type mismatch"
 | bug _ _                       => "bug"
@@ -74,7 +76,8 @@ def toMessageData : Exception → MessageData
 | invalidProjection s i e ctx     => mkCtx ctx $ `invalidProjection ++ " " ++ mkProj s i e
 | revertFailure xs decl ctx       => mkCtx ctx $ `revertFailure -- TODO improve
 | readOnlyMVar mvarId ctx         => mkCtx ctx $ `readOnlyMVar ++ " " ++ mkMVar mvarId
-| isDefEqStuck t s ctx            => mkCtx ctx $ `isDefEqStuck ++ " " ++ t ++ " =?= " ++ s
+| isLevelDefEqStuck u v ctx       => mkCtx ctx $ `isLevelDefEqStuck ++ " " ++ u ++ " =?= " ++ v
+| isExprDefEqStuck t s ctx        => mkCtx ctx $ `isExprDefEqStuck ++ " " ++ t ++ " =?= " ++ s
 | letTypeMismatch fvarId ctx      => mkCtx ctx $ `letTypeMismatch ++ " " ++ mkFVar fvarId
 | appTypeMismatch f a ctx         => mkCtx ctx $ `appTypeMismatch ++ " " ++ mkApp f a
 | bug _ _                         => "internal bug" -- TODO improve

src/Init/Lean/Meta/ExprDefEq.lean

@@ -918,7 +918,7 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
   cond (!tAssign? && !sAssign?)
     (if tFn.isMVar || sFn.isMVar then do
        ctx ← read;
-       if ctx.config.isDefEqStuckEx then throwEx $ Exception.isDefEqStuck t s
+       if ctx.config.isDefEqStuckEx then throwEx $ Exception.isExprDefEqStuck t s
        else pure LBool.false
      else pure LBool.undef) $ do
   -- Both `t` and `s` are terms of the form `?m ...`

src/Init/Lean/Meta/LevelDefEq.lean

@@ -67,8 +67,12 @@ partial def isLevelDefEqAux : Level → Level → MetaM Bool
       isLevelDefEqAux lhs' rhs'
     else do
       mctx ← getMCtx;
-      if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then
-        pure false
+      if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then do
+        ctx ← read;
+        if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then
+          throwEx $ Exception.isLevelDefEqStuck lhs rhs
+        else
+          pure false
       else do
         k ← getLevelConstraintKind lhs rhs;
         match k with