perf: fatal typeclass inference should short-circuit unification

src/Lean/Meta/Basic.lean

@@ -25,6 +25,7 @@ They are packed into the MetaM monad.
 namespace Lean.Meta
 
 builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck
+builtin_initialize synthFailedExceptionId : InternalExceptionId ← registerInternalExceptionId `synthFailed
 
 /--
 Configuration flags for the `MetaM` monad.
@@ -420,7 +421,7 @@ but may contain subexpressions which have not been reduced. -/
 @[extern 6 "lean_infer_type"] opaque inferType : Expr → MetaM Expr
 @[extern 7 "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool
 @[extern 7 "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool
-@[extern 6 "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM Bool
+@[extern 6 "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM (LOption Unit)
 
 def whnfForall (e : Expr) : MetaM Expr := do
   let e' ← whnf e
@@ -1646,6 +1647,10 @@ def isLevelDefEq (u v : Level) : MetaM Bool :=
 /-- See `isDefEq`. -/
 def isExprDefEq (t s : Expr) : MetaM Bool :=
   withReader (fun ctx => { ctx with defEqCtx? := some { lhs := t, rhs := s, lctx := ctx.lctx, localInstances := ctx.localInstances } }) do
+    -- the scope of this exception could be extended into other subsystems where synthesis
+    -- is either not backtracked or exceptions are backtracked (e.g. the elaborator proper),
+    -- but that is not true for e.g. `synthInstance` itself, so would require further adjustments
+    catchInternalId synthFailedExceptionId (h := fun _ => pure false) do
     checkpointDefEq (mayPostpone := true) <| Meta.isExprDefEqAux t s
 
 /--

src/Lean/Meta/ExprDefEq.lean

@@ -138,7 +138,10 @@ def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
 private def trySynthPending (e : Expr) : MetaM Bool := do
   let mvarId? ← getStuckMVar? e
   match mvarId? with
-  | some mvarId => Meta.synthPending mvarId
+  | some mvarId => match (← Meta.synthPending mvarId) with
+    | .none => throw <| Exception.internal synthFailedExceptionId
+    | .some _ => pure true
+    | .undef => pure false
   | none        => pure false
 
 /--
@@ -1627,7 +1630,7 @@ end
   match (← getStuckMVar? e) with
   | some mvarId =>
     trace[Meta.isDefEq.stuckMVar] "found stuck MVar {mkMVar mvarId} : {← inferType (mkMVar mvarId)}"
-    if (← Meta.synthPending mvarId) then
+    if (← trySynthPending e) then  -- HACK, restructure code to avoid double `getStuckMVar?`
       let e ← instantiateMVars e
       successK e
     else

src/Lean/Meta/SynthInstance.lean

@@ -749,35 +749,34 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
     (fun _ => throwError "failed to synthesize{indentExpr type}")
 
 @[export lean_synth_pending]
-private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
+private def synthPendingImp (mvarId : MVarId) : MetaM (LOption Unit) := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl
   match mvarDecl.kind with
   | MetavarKind.syntheticOpaque =>
-    return false
+    return .undef
   | _ =>
     /- Check whether the type of the given metavariable is a class or not. If yes, then try to synthesize
        it using type class resolution. We only do it for `synthetic` and `natural` metavariables. -/
     match (← isClass? mvarDecl.type) with
     | none   =>
-      return false
+      return .undef
     | some _ =>
       /- TODO: use a configuration option instead of the hard-coded limit `1`. -/
       if (← read).synthPendingDepth > 1 then
         trace[Meta.synthPending] "too many nested synthPending invocations"
-        return false
+        return .undef
       else
         withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) do
           trace[Meta.synthPending] "synthPending {mkMVar mvarId}"
-          let val? ← catchInternalId isDefEqStuckExceptionId (synthInstance? mvarDecl.type (maxResultSize? := none)) (fun _ => pure none)
-          match val? with
-          | none     =>
-            return false
-          | some val =>
+          match (← trySynthInstance mvarDecl.type) with
+          | .some val =>
             if (← mvarId.isAssigned) then
-              return false
+              return .none
             else
               mvarId.assign val
-              return true
+              return .some ()
+          | .none => return .none
+          | .undef => return .undef
 
 builtin_initialize
   registerTraceClass `Meta.synthPending

src/Lean/Meta/WHNF.lean

@@ -597,7 +597,7 @@ where
     | ReduceMatcherResult.stuck e' =>
       let mvarId ← getStuckMVar? e'
       /- Try to "unstuck" by resolving pending TC problems -/
-      if (← Meta.synthPending mvarId) then
+      if (← Meta.synthPending mvarId) matches .some _ then
         goMatch e
       else
         failure