From 484a3a4e7c3d97f53d010d988ee972a0219d588f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 11 Apr 2021 19:02:39 -0700
Subject: [PATCH] fix: should only cache inferred type when there are no
 metavars

---
 src/Lean/Meta/InferType.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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 :=