fix(library/unifier): fix cryptic error message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/unifier.cpp

@@ -431,11 +431,7 @@ struct unifier_fn {
         }
         if (in_conflict())
             return false;
-        justification j1 = mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
-                substitution s(subst);
-                return pp_type_mismatch(fmt, s.instantiate(m_type), s.instantiate(v_type));
-            });
-        if (!is_def_eq(m_type, v_type, mk_composite1(j1, j)))
+        if (!is_def_eq(m_type, v_type, j))
             return false;
         auto it = m_mvar_occs.find(mlocal_name(m));
         if (it) {

tests/lean/empty.lean

@@ -0,0 +1,5 @@
+import logic hilbert
+
+definition v1 : Prop := epsilon (λ x, true)
+inductive Empty : Type
+definition v2 : Empty := epsilon (λ x, true)

tests/lean/empty.lean.expected.out

@@ -0,0 +1,2 @@
+empty.lean:5:25: error: empty.lean:5:25: failed to synthesize placeholder
+ ⊢ inhabited Empty