fix: stack overflow at mkBinding if type occurs check fails

src/Lean/MetavarContext.lean

@@ -910,6 +910,15 @@ structure Context where
   binderInfoForMVars : BinderInfo := BinderInfo.implicit
   /-- Set of unassigned metavariables being abstracted. -/
   mvarIdsToAbstract  : MVarIdSet := {}
+  /--
+  Map of metavariable assignments that haven't yet been added to the metavariable context.
+  This is necessary to deal with metavariables that contain themselves in their own type.
+  Without this, such a situation would lead to infinite recursion. (see #6013 and #3150)
+
+  We claim it is not necessary to run `elim` on this cached value again, because the
+  dependencies on the free variables are already eliminated. This stops the infinite recursion.
+  -/
+  mvarIdsInProgress  : AssocList MVarId Expr := {}
 
 abbrev MCore := EStateM Exception State
 abbrev M     := ReaderT Context MCore
@@ -1129,15 +1138,15 @@ mutual
       let newMVarLCtx   := reduceLocalContext mvarLCtx toRevert
       let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
       -- Remark: we must reset the cache before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
-      let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
       let newMVarId    := { name := (← get).ngen.curr }
+      modify fun s => { s with ngen := s.ngen.next }
       let newMVar      := mkMVar newMVarId
       let result       := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
+      let newMVarType ← withReader (fun ctx => { ctx with mvarIdsInProgress := ctx.mvarIdsInProgress.insert mvarId result }) do
+        withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
       let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs
       modify fun s => { s with
-          mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs,
-          ngen := s.ngen.next
-        }
+        mctx := s.mctx.addExprMVarDecl newMVarId Name.anonymous newMVarLCtx newLocalInsts newMVarType newMVarKind numScopeArgs }
       if !mvarDecl.kind.isSyntheticOpaque then
         mvarId.assign result
       else
@@ -1170,7 +1179,10 @@ mutual
         if (← read).mvarIdsToAbstract.contains mvarId then
           return mkAppN f (← args.mapM (visit xs))
         else
-          return (← elimMVar xs mvarId args).1
+          if let some result := (← read).mvarIdsInProgress.find? mvarId then
+            return result
+          else
+            return (← elimMVar xs mvarId args).1
     | _ =>
       return mkAppN (← visit xs f) (← args.mapM (visit xs))
 

tests/lean/run/6013.lean

@@ -0,0 +1,77 @@
+
+/--
+error: failed to synthesize
+  OfNat (String → String) 10
+numerals are polymorphic in Lean, but the numeral `10` cannot be used in a context where the expected type is
+  String → String
+due to the absence of the instance above
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+example (a : String) : String :=
+  let x : String → String := _
+  have : x = 10 := by rfl
+  "tested"
+
+
+
+
+structure A where
+  α : Type
+  a : α
+
+structure B (f : (α : Type) → α → α) extends A where
+  b : α
+  a := f α b
+
+/--
+error: don't know how to synthesize placeholder
+context:
+⊢ { α := Nat, a := id ?m }.α
+-/
+#guard_msgs in
+example : B @id where
+  α := Nat
+  b := _
+
+
+
+
+class One (α : Type) where
+  one : α
+
+variable (R A : Type) [One R] [One A]
+
+class OneHom where
+  toFun : R → A
+  map_one : toFun One.one = One.one
+
+structure Subone where
+  mem : R → Prop
+  one_mem : mem One.one
+
+structure Subalgebra [OneHom R A] extends Subone A : Type where
+  algebraMap_mem : ∀ r : R, mem (OneHom.toFun r)
+  one_mem := OneHom.map_one (R := R) (A := A) ▸ algebraMap_mem One.one
+
+/--
+error: don't know how to synthesize placeholder
+context:
+R A : Type
+inst✝² : One R
+inst✝¹ : One A
+inst✝ : OneHom R A
+⊢ ∀ (r : R), { mem := ?m R A _example, one_mem := ⋯ }.mem (OneHom.toFun r)
+---
+error: don't know how to synthesize placeholder
+context:
+R A : Type
+inst✝² : One R
+inst✝¹ : One A
+inst✝ : OneHom R A
+⊢ A → Prop
+-/
+#guard_msgs in
+example [OneHom R A] : Subalgebra R A where
+  mem := _
+  algebraMap_mem := _