From a44a975388fbd844d13145f00528c0a07a94d445 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Jan 2017 08:51:09 -0800
Subject: [PATCH] feat(library/type_context,frontends/lean/elaborator): add
 class_exception (for max depth reached), ignore them during coercion
 resolution (just add a trace message)

---
 src/frontends/lean/elaborator.cpp | 18 +++++++++++++++---
 src/library/type_context.cpp      |  2 +-
 src/library/type_context.h        |  6 ++++++
 3 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d515e0c066..c81533e955 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -434,7 +434,15 @@ optional<expr> elaborator::mk_coercion_core(expr const & e, expr const & e_type,
                                    "('set_option trace.app_builder true' for more information)");
             return none_expr();
         }
-        optional<expr> inst = m_ctx.mk_class_instance_at(m_ctx.lctx(), has_coe_t);
+        optional<expr> inst;
+        try {
+            inst = m_ctx.mk_class_instance_at(m_ctx.lctx(), has_coe_t);
+        } catch (class_exception &) {
+            trace_coercion_failure(e_type, type, ref,
+                                   "failed to synthesize class instance for 'has_coe_t' "
+                                   "('set_option trace.class_instances true' for more information)");
+            return none_expr();
+        }
         if (!inst) {
             trace_coercion_failure(e_type, type, ref,
                                    "failed to synthesize 'has_coe_t' type class instance "
@@ -452,8 +460,12 @@ optional<expr> elaborator::mk_coercion_core(expr const & e, expr const & e_type,
 }
 
 bool elaborator::is_monad(expr const & e) {
-    expr m = mk_app(m_ctx, get_monad_name(), e);
-    return static_cast<bool>(m_ctx.mk_class_instance(m));
+    try {
+        expr m = mk_app(m_ctx, get_monad_name(), e);
+        return static_cast<bool>(m_ctx.mk_class_instance(m));
+    } catch (class_exception &) {
+        return false;
+    }
 }
 
 /*
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index fb161c272a..fbc2c33a6f 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2959,7 +2959,7 @@ optional<name> type_context::is_class(expr const & type) {
     return is_full_class(type);
 }
 
-[[ noreturn ]] static void throw_class_exception(expr const & m, char const * msg) { throw generic_exception(m, msg); }
+[[ noreturn ]] static void throw_class_exception(expr const & m, char const * msg) { throw class_exception(m, msg); }
 
 struct instance_synthesizer {
     struct stack_entry {
diff --git a/src/library/type_context.h b/src/library/type_context.h
index c293276e45..8d2f5e48f3 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -17,8 +17,14 @@ Author: Leonardo de Moura
 #include "library/projection.h"
 #include "library/metavar_context.h"
 #include "library/expr_pair_maps.h"
+#include "library/exception.h"
 
 namespace lean {
+class class_exception : public generic_exception {
+public:
+    class_exception(expr const & m, char const * msg):generic_exception(m, msg) {}
+};
+
 enum class transparency_mode { All, Semireducible, Reducible, None };
 
 /* \brief Cached information for type_context. */