chore: simplify isExprDefEqStuck and isLevelDefEqStuck

src/Lean/Meta/Check.lean

@@ -113,7 +113,7 @@ def isTypeCorrect (e : Expr) : MetaM Bool :=
 catch
   (traceCtx `Meta.check $ do checkAux e; pure true)
   (fun ex => do
-    trace! `Meta.typeError ex.toTraceMessageData;
+    trace! `Meta.typeError ex.toMessageData;
     pure false)
 
 @[init] private def regTraceClasses : IO Unit := do

src/Lean/Meta/Exception.lean

@@ -15,9 +15,8 @@ namespace Meta
 abbrev ExceptionContext := MessageDataContext
 
 inductive Exception
-| isLevelDefEqStuck (u v : Level) (ctx : ExceptionContext)
-| isExprDefEqStuck  (t s : Expr) (ctx : ExceptionContext)
-| core              (ex : Core.Exception)
+| isDefEqStuck
+| core          (ex : Core.Exception)
 
 namespace Exception
 instance : Inhabited Exception := ⟨core $ arbitrary _⟩
@@ -29,16 +28,9 @@ def getRef : Exception → Syntax
 def mkCtx (ctx : ExceptionContext) (m : MessageData) : MessageData :=
 MessageData.withContext ctx m
 
-/-- Generate trace message that is suitable for tracing crawlers -/
-def toTraceMessageData : Exception → MessageData
-| isLevelDefEqStuck u v ctx       => mkCtx ctx $ `isLevelDefEqStuck ++ " " ++ u ++ " =?= " ++ v
-| isExprDefEqStuck t s ctx        => mkCtx ctx $ `isExprDefEqStuck ++ " " ++ t ++ " =?= " ++ s
-| core ex                         => ex.toMessageData
-
 def toMessageData : Exception → MessageData
-| isLevelDefEqStuck u v ctx       => mkCtx ctx $ `isLevelDefEqStuck ++ " " ++ u ++ " =?= " ++ v
-| isExprDefEqStuck t s ctx        => mkCtx ctx $ `isExprDefEqStuck ++ " " ++ t ++ " =?= " ++ s
-| core ex                         => ex.toMessageData
+| isDefEqStuck => "<isDefEqStuck>"
+| core ex      => ex.toMessageData
 
 end Exception
 

src/Lean/Meta/ExprDefEq.lean

@@ -966,7 +966,7 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
        ctx ← read;
        if ctx.config.isDefEqStuckEx then do
          trace! `Meta.isDefEq.stuck (t ++ " =?= " ++ s);
-         throwEx $ Exception.isExprDefEqStuck t s
+         throw Exception.isDefEqStuck
        else pure LBool.false
      else pure LBool.undef) $ do
   -- Both `t` and `s` are terms of the form `?m ...`

src/Lean/Meta/LevelDefEq.lean

@@ -109,7 +109,7 @@ partial def isLevelDefEqAux : Level → Level → MetaM Bool
         ctx ← read;
         if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
           trace! `Meta.isLevelDefEq.stuck (lhs ++ " =?= " ++ rhs);
-          throwEx $ Exception.isLevelDefEqStuck lhs rhs
+          throw Exception.isDefEqStuck
         else
           pure false
       else do

src/Lean/Meta/SynthInstance.lean

@@ -583,9 +583,8 @@ adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with isDef
   catch
     (toLOptionM $ synthInstance? type)
     (fun ex => match ex with
-      | Exception.isExprDefEqStuck _ _ _  => pure LOption.undef
-      | Exception.isLevelDefEqStuck _ _ _ => pure LOption.undef
-      | _                                 => throw ex)
+      | Exception.isDefEqStuck => pure LOption.undef
+      | _                      => throw ex)
 
 def synthInstance (type : Expr) : MetaM Expr := do
 result? ← synthInstance? type;