From 9ec9ea61a4ebbcd2672b8905e7c583958113e24e Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 30 May 2023 08:20:57 -0400
Subject: [PATCH] fix: infinite loop in `isClassApp?`

---
 src/Lean/Meta/Basic.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 5a95eabaf5..c7737f4937 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -986,7 +986,7 @@ mutual
 
 
   -- Helper method for isClassExpensive?
-  private partial def isClassApp? (type : Expr) : MetaM (Option Name) := do
+  private partial def isClassApp? (type : Expr) (instantiated := false) : MetaM (Option Name) := do
     match type.getAppFn with
     | .const c _ =>
       let env ← getEnv
@@ -997,7 +997,9 @@ mutual
         match (← whnf type).getAppFn with
         | .const c _ => if isClass env c then return some c else return none
         | _ => return none
-    | .mvar .. => isClassApp? (← instantiateMVars type)
+    | .mvar .. =>
+      if instantiated then return none
+      isClassApp? (← instantiateMVars type) true
     | _ => return none
 
   private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) :=