feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution

src/frontends/lean/CMakeLists.txt

@@ -7,7 +7,8 @@ begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
 theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp
 extra_info.cpp local_context.cpp choice_iterator.cpp
 placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp
-proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp)
+proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp
+elaborator_exception.cpp)
 
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/elaborator.cpp

@@ -46,6 +46,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/pp_options.h"
 #include "frontends/lean/begin_end_ext.h"
+#include "frontends/lean/elaborator_exception.h"
 
 namespace lean {
 /** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
@@ -1212,9 +1213,7 @@ static expr translate_local_name(environment const & env, list<expr> const & ctx
         if (local_pp_name(local) == local_name)
             return copy(local);
     }
-    // TODO(Leo): we should create an elaborator exception.
-    // Using kernel_exception here is just a dirty hack.
-    throw_kernel_exception(env, sstream() << "unknown identifier '" << local_name << "'", src);
+    throw_elaborator_exception(env, sstream() << "unknown identifier '" << local_name << "'", src);
 }
 
 /** \brief Translated local constants (and undefined constants) occurring in \c e into

src/frontends/lean/elaborator_exception.cpp

@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/kernel_exception.h"
+#include "frontends/lean/elaborator_exception.h"
+
+namespace lean {
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m) {
+    throw_kernel_exception(env, msg, m);
+}
+
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, sstream const & strm, expr const & m) {
+    throw_kernel_exception(env, strm, m);
+}
+
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn) {
+    throw_kernel_exception(env, msg, m, fn);
+}
+
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, expr const & m, pp_fn const & fn) {
+    throw_kernel_exception(env, m, fn);
+}
+}

src/frontends/lean/elaborator_exception.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/environment.h"
+#include "kernel/formatter.h"
+
+namespace lean {
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m);
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, sstream const & strm, expr const & m);
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn);
+[[ noreturn ]] void throw_elaborator_exception(environment const & env, expr const & m, pp_fn const & fn);
+}

src/frontends/lean/placeholder_elaborator.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
+#include "kernel/error_msgs.h"
 #include "library/unifier.h"
 #include "library/reducible.h"
 #include "library/metavar_closure.h"
@@ -18,6 +19,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/class.h"
 #include "frontends/lean/local_context.h"
 #include "frontends/lean/choice_iterator.h"
+#include "frontends/lean/elaborator_exception.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_UNIQUE_CLASS_INSTANCES false
@@ -279,8 +281,14 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
                     cnstrs = p.second;
                     expr next_solution = subst.instantiate(new_meta);
                     if (solution) {
-                        // TODO(Leo): more informative error message
-                        throw exception("ambiguous class-instance resolution, there is more than one solution");
+                        throw_elaborator_exception(env, m, [=](formatter const & fmt) {
+                                format r = format("ambiguous class-instance resolution, "
+                                                  "there is more than one solution");
+                                r += pp_indent_expr(fmt, *solution);
+                                r += compose(line(), format("and"));
+                                r += pp_indent_expr(fmt, next_solution);
+                                return r;
+                            });
                     } else {
                         solution = next_solution;
                     }