diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/library/Init/Lean/Meta/ExprDefEq.lean
index 7f7a0b0181..4388e0b193 100644
--- a/library/Init/Lean/Meta/ExprDefEq.lean
+++ b/library/Init/Lean/Meta/ExprDefEq.lean
@@ -678,7 +678,8 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
              a type incorrect term. See discussion at A2 -/
           condM (isTypeCorrect v)
             (finalize ())
-            (useFOApprox ())
+            (do trace! `Meta.isDefEq.assignment.typeError (mvar ++ " := " ++ v);
+                useFOApprox ())
         else
           finalize ()