diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 5abec11ab3..56c6678759 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -73,7 +73,7 @@ private def tryCoeFun? (α : Expr) (a : Expr) : TermElabM (Option Expr) := do
   let mvar ← mkFreshExprMVar coeFunInstType MetavarKind.synthetic
   let mvarId := mvar.mvarId!
   try
-    if (← synthesizeInstMVarCore mvarId) then
+    if (← synthesizeCoeInstMVarCore mvarId) then
       pure $ some $ mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar]
     else
       pure none
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 96079fc913..2985cc9c74 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -83,7 +83,7 @@ private def synthesizePendingCoeInstMVar
     (instMVar : MVarId) (errorMsgHeader? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Bool :=
   withMVarContext instMVar do
     try
-      synthesizeInstMVarCore instMVar
+      synthesizeCoeInstMVarCore instMVar
     catch
       | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
       | _                     => unreachable!
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 6d8b60ad11..d0a19c3998 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -525,11 +525,11 @@ def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr)
    Return `true` if the instance was synthesized successfully, and `false` if
    the instance contains unassigned metavariables that are blocking the type class
    resolution procedure. Throw an exception if resolution or assignment irrevocably fails. -/
-def synthesizeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do
+def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none) : TermElabM Bool := do
   let instMVarDecl ← getMVarDecl instMVar
   let type := instMVarDecl.type
   let type ← instantiateMVars type
-  let result ← trySynthInstance type
+  let result ← trySynthInstance type maxResultSize?
   match result with
   | LOption.some val =>
     if (← isExprMVarAssigned instMVar) then
@@ -542,6 +542,15 @@ def synthesizeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do
   | LOption.undef    => pure false -- we will try later
   | LOption.none     => throwError! "failed to synthesize instance{indentExpr type}"
 
+def maxCoeSizeDefault := 16
+builtin_initialize
+  registerOption `maxCoeSize { defValue := maxCoeSizeDefault, group := "", descr := "maximum number of instances used to construct an automatic coercion" }
+private def getCoeMaxSize (opts : Options) : Nat :=
+  opts.getNat `maxCoeSize maxCoeSizeDefault
+
+def synthesizeCoeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do
+  synthesizeInstMVarCore instMVar (getCoeMaxSize (← getOptions))
+
 /-
 The coercion from `α` to `Thunk α` cannot be implemented using an instance because it would
 eagerly evaluate `e` -/
@@ -576,7 +585,7 @@ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eTyp
       let mvarId := mvar.mvarId!
       try
         withoutMacroStackAtErr do
-          unless (← synthesizeInstMVarCore mvarId) do
+          unless (← synthesizeCoeInstMVarCore mvarId) do
             registerSyntheticMVarWithCurrRef mvarId (SyntheticMVarKind.coe errorMsgHeader? expectedType eType e f?)
           pure eNew
       catch
@@ -1023,7 +1032,7 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do
   let mvarId := mvar.mvarId!
   try
     withoutMacroStackAtErr do
-      if (← synthesizeInstMVarCore mvarId) then
+      if (← synthesizeCoeInstMVarCore mvarId) then
         pure $ mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar]
       else
         throwError "type expected"
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 502b1667ce..2982542b85 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -37,8 +37,10 @@ structure ConsumerNode where
   key      : Expr
   mctx     : MetavarContext
   subgoals : List Expr
+  size     : Nat -- instance size so far
 
-instance : Inhabited ConsumerNode := ⟨⟨arbitrary, arbitrary, arbitrary, []⟩⟩
+instance : Inhabited ConsumerNode where
+  default := { mvar := arbitrary, key := arbitrary, mctx := arbitrary, subgoals := [], size := 0 }
 
 inductive Waiter where
   | consumerNode : ConsumerNode → Waiter
@@ -133,13 +135,18 @@ def mkTableKey (mctx : MetavarContext) (e : Expr) : Expr :=
 structure Answer where
   result     : AbstractMVarsResult
   resultType : Expr
+  size       : Nat
 
-instance : Inhabited Answer := ⟨⟨arbitrary, arbitrary⟩⟩
+instance : Inhabited Answer where
+  default := { result := arbitrary, resultType := arbitrary, size := 0 }
 
 structure TableEntry where
   waiters : Array Waiter
   answers : Array Answer := #[]
 
+structure Context where
+  maxResultSize : Nat
+
 /-
   Remark: the SynthInstance.State is not really an extension of `Meta.State`.
   The field `postponed` is not needed, and the field `mctx` is misleading since
@@ -153,13 +160,13 @@ structure State where
   resumeStack    : Array (ConsumerNode × Answer) := #[]
   tableEntries   : HashMap Expr TableEntry       := {}
 
-abbrev SynthM := StateRefT State MetaM
+abbrev SynthM := ReaderT Context $ StateRefT State MetaM
 
 @[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
   monadMap @f
 
-instance {α} : Inhabited (SynthM α) :=
-  ⟨fun _ => arbitrary⟩
+instance {α} : Inhabited (SynthM α) where
+  default := fun _ _ => arbitrary
 
 /-- Return globals and locals instances that may unify with `type` -/
 def getInstances (type : Expr) : MetaM (Array Expr) := do
@@ -311,7 +318,7 @@ def tryResolveCore (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext 
   If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : SynthM (Option (MetavarContext × List Expr)) :=
-  traceCtx `Meta.synthInstance.tryResolve $ withMCtx mctx $ tryResolveCore mvar inst
+  traceCtx `Meta.synthInstance.tryResolve <| withMCtx mctx <| tryResolveCore mvar inst
 
 /--
   Assign a precomputed answer to `mvar`.
@@ -330,7 +337,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
     if answer.result.paramNames.isEmpty && answer.result.numMVars == 0 then
       modify fun s => { s with result := answer.result.expr }
     else
-      let (_, _, answerExpr) ← liftM $ openAbstractMVarsResult answer.result
+      let (_, _, answerExpr) ← openAbstractMVarsResult answer.result
       trace[Meta.synthInstance]! "skip answer containing metavariables {answerExpr}"
       pure ()
   | Waiter.consumerNode cNode =>
@@ -344,25 +351,29 @@ def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
 
 private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
   withMCtx cNode.mctx do
-    traceM `Meta.synthInstance.newAnswer do pure (← inferType cNode.mvar)
+    traceM `Meta.synthInstance.newAnswer do m!"size: {cNode.size}, {← inferType cNode.mvar}"
     let val ← instantiateMVars cNode.mvar
     let result ← abstractMVars val -- assignable metavariables become parameters
     let resultType ← inferType result.expr
-    pure { result := result, resultType := resultType }
+    pure { result := result, resultType := resultType, size := cNode.size + 1 }
 
 /--
   Create a new answer after `cNode` resolved all subgoals.
   That is, `cNode.subgoals == []`.
   And then, store it in the tabled entries map, and wakeup waiters. -/
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
-  let answer ← mkAnswer cNode
-  -- Remark: `answer` does not contain assignable or assigned metavariables.
-  let key := cNode.key
-  let entry ← getEntry key
-  if isNewAnswer entry.answers answer then
-    let newEntry := { entry with answers := entry.answers.push answer }
-    modify fun s => { s with tableEntries := s.tableEntries.insert key newEntry }
-    entry.waiters.forM (wakeUp answer)
+  if cNode.size ≥ (← read).maxResultSize then
+    traceM `Meta.synthInstance.discarded do m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
+    return ()
+  else
+    let answer ← mkAnswer cNode
+    -- Remark: `answer` does not contain assignable or assigned metavariables.
+    let key := cNode.key
+    let entry ← getEntry key
+    if isNewAnswer entry.answers answer then
+      let newEntry := { entry with answers := entry.answers.push answer }
+      modify fun s => { s with tableEntries := s.tableEntries.insert key newEntry }
+      entry.waiters.forM (wakeUp answer)
 
 /-- Process the next subgoal in the given consumer node. -/
 def consume (cNode : ConsumerNode) : SynthM Unit :=
@@ -400,7 +411,7 @@ def generate : SynthM Unit := do
     modifyTop fun gNode => { gNode with currInstanceIdx := idx }
     match (← tryResolve mctx mvar inst) with
     | none                  => pure ()
-    | some (mctx, subgoals) => consume { key := key, mvar := mvar, subgoals := subgoals, mctx := mctx }
+    | some (mctx, subgoals) => consume { key := key, mvar := mvar, subgoals := subgoals, mctx := mctx, size := 0 }
 
 def getNextToResume : SynthM (ConsumerNode × Answer) := do
   let s ← get
@@ -422,8 +433,8 @@ def resume : SynthM Unit := do
       withMCtx mctx <| traceM `Meta.synthInstance.resume do
         let goal    ← inferType cNode.mvar
         let subgoal ← inferType mvar
-        pure m!"{goal} <== {subgoal}"
-      consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx := mctx }
+        pure m!"size: {cNode.size + answer.size}, {goal} <== {subgoal}"
+      consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx := mctx, size := cNode.size + answer.size }
 
 def step : SynthM Bool := do
   let s ← get
@@ -439,21 +450,16 @@ def step : SynthM Bool := do
 def getResult : SynthM (Option Expr) := do
   pure (← get).result
 
-def synth : Nat → SynthM (Option Expr)
-  | 0   => do
-    trace[Meta.synthInstance]! "synthInstance is out of fuel"
+partial def synth : SynthM (Option Expr) := do
+  if (← step) then
+    match (← getResult) with
+    | none        => synth
+    | some result => pure result
+  else
+    trace[Meta.synthInstance]! "failed"
     pure none
-  | fuel+1 => do
-    trace[Meta.synthInstance]! "remaining fuel {fuel}"
-    if (← step) then
-      match (← getResult) with
-      | none        => synth fuel
-      | some result => pure result
-    else
-      trace[Meta.synthInstance]! "failed"
-      pure none
 
-def main (type : Expr) (fuel : Nat) : MetaM (Option Expr) :=
+def main (type : Expr) (maxResultSize : Nat) : MetaM (Option Expr) :=
   traceCtx `Meta.synthInstance do
      trace[Meta.synthInstance]! "main goal {type}"
      let mvar ← mkFreshExprMVar type
@@ -461,8 +467,8 @@ def main (type : Expr) (fuel : Nat) : MetaM (Option Expr) :=
      let key    := mkTableKey mctx type
      let action : SynthM (Option Expr) := do
        newSubgoal mctx key mvar Waiter.root
-       synth fuel
-     action.run' {}
+       synth
+     action.run { maxResultSize := maxResultSize } |>.run' {}
 
 end SynthInstance
 
@@ -524,15 +530,15 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
         mkForallFVars xs (mkAppN c args)
     | _ => pure type
 
-def maxStepsDefault := 1000
+def maxResultSizeDefault := 128
 builtin_initialize
-  registerOption `synthInstance.maxSteps { defValue := maxStepsDefault, group := "", descr := "maximum steps for the type class instance synthesis procedure" }
-private def getMaxSteps (opts : Options) : Nat :=
-  opts.getNat `synthInstance.maxSteps maxStepsDefault
+  registerOption `maxInstSize { defValue := maxResultSizeDefault, group := "", descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure" }
+private def getMaxSize (opts : Options) : Nat :=
+  opts.getNat `maxInstSize maxResultSizeDefault
 
-private def synthInstanceImp? (type : Expr) : MetaM (Option Expr) := profileitM Exception "typeclass inference" ⟨0, 0⟩ do
+private def synthInstanceImp? (type : Expr) (maxResultSize? : Option Nat) : MetaM (Option Expr) := profileitM Exception "typeclass inference" ⟨0, 0⟩ do
   let opts ← getOptions
-  let fuel := getMaxSteps opts
+  let maxResultSize := maxResultSize?.getD (getMaxSize opts)
   let inputConfig ← getConfig
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.reducible,
                                           foApprox := true, ctxApprox := true, constApprox := false }) do
@@ -545,7 +551,7 @@ private def synthInstanceImp? (type : Expr) : MetaM (Option Expr) := profileitM
       let result? ← withNewMCtxDepth do
         let normType ← preprocessOutParam type
         trace[Meta.synthInstance]! "{type} ==> {normType}"
-        match (← SynthInstance.main normType fuel) with
+        match (← SynthInstance.main normType maxResultSize) with
         | none        => pure none
         | some result =>
           trace[Meta.synthInstance]! "FOUND result {result}"
@@ -559,7 +565,7 @@ private def synthInstanceImp? (type : Expr) : MetaM (Option Expr) := profileitM
         | some result => do
           trace[Meta.synthInstance]! "result {result}"
           let resultType ← inferType result
-          if (← withConfig (fun _ => inputConfig) $ isDefEq type resultType) then
+          if (← withConfig (fun _ => inputConfig) <| isDefEq type resultType) then
             let result ← instantiateMVars result
             pure (some result)
           else
@@ -573,28 +579,28 @@ private def synthInstanceImp? (type : Expr) : MetaM (Option Expr) := profileitM
 /--
   Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if
   instance cannot be synthesized right now because `type` contains metavariables. -/
-private def trySynthInstanceImp (type : Expr) : MetaM (LOption Expr) := do
+private def trySynthInstanceImp (type : Expr) (maxResultSize? : Option Nat) : MetaM (LOption Expr) := do
   catchInternalId isDefEqStuckExceptionId
-    (toLOptionM $ synthInstanceImp? type)
+    (toLOptionM $ synthInstanceImp? type maxResultSize?)
     (fun _ => pure LOption.undef)
 
-private def synthInstanceImp (type : Expr) : MetaM Expr :=
+private def synthInstanceImp (type : Expr) (maxResultSize? : Option Nat) : MetaM Expr :=
   catchInternalId isDefEqStuckExceptionId
     (do
-      let result? ← synthInstanceImp? type
+      let result? ← synthInstanceImp? type maxResultSize?
       match result? with
       | some result => pure result
       | none        => throwError! "failed to synthesize{indentExpr type}")
     (fun _ => throwError! "failed to synthesize{indentExpr type}")
 
-private def synthPendingImp (mvarId : MVarId) : MetaM Bool := do
+private def synthPendingImp (mvarId : MVarId) (maxResultSize? : Option Nat) : MetaM Bool := do
   let mvarDecl ← getMVarDecl mvarId
   match mvarDecl.kind with
   | MetavarKind.synthetic =>
     match (← isClass? mvarDecl.type) with
     | none   => pure false
     | some _ => do
-      let val? ← catchInternalId isDefEqStuckExceptionId (synthInstanceImp? mvarDecl.type) (fun _ => pure none)
+      let val? ← catchInternalId isDefEqStuckExceptionId (synthInstanceImp? mvarDecl.type maxResultSize?) (fun _ => pure none)
       match val? with
       | none     => pure false
       | some val =>
@@ -606,7 +612,7 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := do
   | _ => pure false
 
 builtin_initialize
-  synthPendingRef.set synthPendingImp
+  synthPendingRef.set (synthPendingImp · none)
 
 builtin_initialize
   registerTraceClass `Meta.synthInstance
@@ -618,13 +624,18 @@ builtin_initialize
 
 variables {m : Type → Type} [MonadLiftT MetaM m]
 
-def synthInstance? (type : Expr) : m (Option Expr) :=
-  liftMetaM $ synthInstanceImp? type
+/-
+  Remark: when `maxResultSize? == none`, the configuration option `synthInstance.maxResultSize` is used.
+  Remark: we use a different option for controlling the maximum result size for coercions.
+-/
 
-def trySynthInstance (type : Expr) : m (LOption Expr) :=
-  liftMetaM $ trySynthInstanceImp type
+def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : m (Option Expr) :=
+  synthInstanceImp? type maxResultSize?
 
-def synthInstance (type : Expr) : m Expr :=
-  liftMetaM $ synthInstanceImp type
+def trySynthInstance (type : Expr) (maxResultSize? : Option Nat := none) : m (LOption Expr) :=
+  trySynthInstanceImp type maxResultSize?
+
+def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : m Expr :=
+  synthInstanceImp type maxResultSize?
 
 end Lean.Meta
diff --git a/tests/lean/infoFromFailure.lean.expected.out b/tests/lean/infoFromFailure.lean.expected.out
index a71f13aab5..6a64023cbe 100644
--- a/tests/lean/infoFromFailure.lean.expected.out
+++ b/tests/lean/infoFromFailure.lean.expected.out
@@ -4,12 +4,10 @@ foo "hello" : String × String
     [Meta.synthInstance] main goal Add String
     [Meta.synthInstance.newSubgoal] Add String
     [Meta.synthInstance.globalInstances] Add String, []
-    [Meta.synthInstance] remaining fuel 999
     [Meta.synthInstance] failed
 [Meta.synthInstance] Add Bool ==> Add Bool
   [Meta.synthInstance] 
     [Meta.synthInstance] main goal Add Bool
     [Meta.synthInstance.newSubgoal] Add Bool
     [Meta.synthInstance.globalInstances] Add Bool, []
-    [Meta.synthInstance] remaining fuel 999
     [Meta.synthInstance] failed
diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean
index 8346199f0d..b8f411312f 100644
--- a/tests/lean/run/typeclass_coerce.lean
+++ b/tests/lean/run/typeclass_coerce.lean
@@ -70,7 +70,7 @@ axiom Top (α : Type) (n : Nat) : Type
 
 #print "-----"
 
-set_option synthInstance.maxSteps 10000
+set_option maxInstSize 256
 
 #synth HasCoerce (Top Unit Nat.zero)
                  (Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ)