diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp
index d57702eec..22e28a8e7 100644
--- a/src/kernel/error_msgs.cpp
+++ b/src/kernel/error_msgs.cpp
@@ -41,7 +41,7 @@ format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const &
 }
 
 format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type) {
-    format r("type mismatch, expected type");
+    format r("type mismatch, expected type:");
     r += ::lean::pp_indent_expr(fmt, expected_type);
     r += compose(line(), format("given type:"));
     r += ::lean::pp_indent_expr(fmt, given_type);
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index ea2d6733a..43ae5cfb3 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/error_msgs.h"
 #include "library/occurs.h"
 #include "library/unifier.h"
 #include "library/opaque_hints.h"
@@ -431,7 +432,10 @@ struct unifier_fn {
         }
         if (in_conflict())
             return false;
-        if (!is_def_eq(m_type, v_type, j))
+        justification j1 = mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
+                return pp_type_mismatch(fmt, subst.instantiate(m_type), subst.instantiate(v_type));
+            });
+        if (!is_def_eq(m_type, v_type, mk_composite1(j1, j)))
             return false;
         auto it = m_mvar_occs.find(mlocal_name(m));
         if (it) {