diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp
index 6c6bb6615..d431f562e 100644
--- a/src/frontends/lean/placeholder_elaborator.cpp
+++ b/src/frontends/lean/placeholder_elaborator.cpp
@@ -164,7 +164,7 @@ struct placeholder_elaborator : public choice_iterator {
         return cons(c, to_list(cs.begin(), cs.end()));
     }
 
-    void trace(expr const & r) {
+    void trace(expr const & t, expr const & r) {
         if (!m_C->trace_instances())
             return;
         auto out = diagnostic(m_C->env(), m_C->ios());
@@ -181,7 +181,7 @@ struct placeholder_elaborator : public choice_iterator {
             out << " ";
         if (m_depth > 0)
             out << "[" << m_depth << "] ";
-        out << m_meta << " := " << r << endl;
+        out << m_meta << " : " << t << " := " << r << endl;
     }
 
     optional<constraints> try_instance(expr const & inst, expr const & inst_type) {
@@ -216,7 +216,7 @@ struct placeholder_elaborator : public choice_iterator {
                 type = instantiate(binding_body(type), arg);
             }
             r = Fun(locals, r);
-            trace(r);
+            trace(meta_type, r);
             bool relax   = m_C->m_relax;
             constraint c = mk_eq_cnstr(m_meta, r, m_jst, relax);
             return optional<constraints>(mk_constraints(c, cs));
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index aa7db0f1c..c37b209ff 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -25,6 +25,7 @@ definition assump := eassumption
 tactic_hint assump
 
 theorem tst {A B : Type} (H : inh B) : inh (A → B → B)
+set_option elaborator.trace_instances true
 
 theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) :=
 have h1 [visible] : inh A, from inh.intro a,