diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 645671ac0b..3d0d54ce1a 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -141,7 +141,7 @@ instance : AddMessageContext MetaM := {
   pure (a, sCore, s)
 
 instance [MetaEval α] : MetaEval (MetaM α) :=
-  ⟨fun env opts x _ => MetaEval.eval env opts (x.run' : CoreM _) true⟩ -- TODO: check why we need type ascription here
+  ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩
 
 protected def throwIsDefEqStuck {α} : MetaM α :=
   throw $ Exception.internal isDefEqStuckExceptionId