diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index f707eb068b..6f8235b51f 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -174,7 +174,8 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
   | some type => pure type
   | none =>
     let type ← inferType
-    modifyInferTypeCache fun c => c.insert e type
+    unless e.hasMVar || type.hasMVar do
+      modifyInferTypeCache fun c => c.insert e type
     pure type
 
 def inferTypeImp (e : Expr) : MetaM Expr :=