From 8d643767979de35ccf26d4978700652c57e16fa0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Nov 2016 16:24:54 -0800
Subject: [PATCH] chore(library/type_context): add more trace messages

---
 src/library/type_context.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index fa9ea66c2c..74ef2d44fb 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2841,6 +2841,7 @@ struct instance_synthesizer {
                              scope_trace_env scope(m_ctx.env(), m_ctx);
                              trace(e.m_depth, mk_app(mvar, locals.as_buffer()), mvar_type, r););
             if (!m_ctx.is_def_eq(mvar_type, type)) {
+                lean_trace_plain("class_instances", tout() << "failed is_def_eq\n";);
                 return false;
             }
             r = locals.mk_lambda(r);
@@ -2852,7 +2853,8 @@ struct instance_synthesizer {
                 m_state.m_stack = cons(stack_entry(new_inst_mvars[i], e.m_depth+1), m_state.m_stack);
             }
             return true;
-        } catch (exception &) {
+        } catch (exception & ex) {
+            lean_trace_plain("class_instances", tout() << "exception: " << ex.what() << "\n";);
             return false;
         }
     }
@@ -3026,6 +3028,8 @@ struct instance_synthesizer {
                     return r;
                 }
             }
+            lean_trace("class_instances",
+                       tout() << "trying next solution, current solution has metavars\n" << *r << "\n";);
             r = next_solution();
         }
     }