Improve error messages when overloads+coercions do not work

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

src/frontends/lean/lean_elaborator.cpp

@@ -230,6 +230,7 @@ class elaborator::imp {
                         args[0]  = f_choices[j];
                         types[0] = f_choice_types[j];
                         good_choices.clear();
+                        best_num_coercions = num_coercions;
                     }
                     good_choices.push_back(j);
                 }
@@ -239,14 +240,20 @@ class elaborator::imp {
             }
         }
         if (good_choices.size() == 0) {
-            // TODO add information to the exception
+            throw no_overload_exception(*m_owner, ctx, src, f_choices.size(), f_choices.data(), f_choice_types.data(),
-            throw exception("none of the overloads are good");
+                                        args.size() - 1, args.data() + 1, types.data() + 1);
         } else if (good_choices.size() == 1) {
             // found overload
             return;
         } else {
-            // TODO add information to the exception
+            buffer<expr> good_f_choices;
-            throw exception("ambiguous overload");
+            buffer<expr> good_f_choice_types;
+            for (unsigned j : good_choices) {
+                good_f_choices.push_back(f_choices[j]);
+                good_f_choice_types.push_back(f_choice_types[j]);
+            }
+            throw ambiguous_overload_exception(*m_owner, ctx, src, good_f_choices.size(), good_f_choices.data(), good_f_choice_types.data(),
+                                               args.size() - 1, args.data() + 1, types.data() + 1);
         }
     }
 

src/frontends/lean/lean_elaborator_exception.cpp

@@ -8,14 +8,37 @@ Author: Leonardo de Moura
 #include "lean_elaborator.h"
 
 namespace lean {
+format pp(formatter fmt, context const & ctx, std::vector<expr> const & exprs, std::vector<expr> const & types, options const & opts) {
+    unsigned indent = get_pp_indent(opts);
+    lean_assert(exprs.size() == types.size());
+    auto it1 = exprs.begin();
+    auto it2 = types.begin();
+    format r;
+    for (; it1 != exprs.end(); ++it1, ++it2) {
+        r += nest(indent, compose(line(), group(format{fmt(ctx, *it1, false, opts), space(), colon(),
+                                                       nest(indent, format{line(), fmt(ctx, *it2, false, opts)})})));
+    }
+    return r;
+}
+
 format pp(formatter fmt, elaborator_exception const & ex, options const & opts) {
     unsigned indent = get_pp_indent(opts);
-    format expr_f = fmt(ex.get_context(), ex.get_expr(), false, opts);
+    context const & ctx = ex.get_context();
-    format elb_f  = ex.get_elaborator().pp(fmt, opts);
+    if (overload_exception const * _ex = dynamic_cast<overload_exception const *>(&ex)) {
-    return format({format(ex.what()), space(), format("at term"),
+        format r;
-                nest(indent, compose(line(), expr_f)),
+        r += format{format(ex.what()), line(), format("Candidates:")};
-                line(), format("Elaborator state"),
+        r += pp(fmt, ctx, _ex->get_fs(), _ex->get_f_types(), opts);
-                nest(indent, compose(line(), elb_f))});
+        r += format{line(), format("Arguments:")};
+        r += pp(fmt, ctx, _ex->get_args(), _ex->get_arg_types(), opts);
+        return r;
+    } else {
+        format expr_f = fmt(ctx, ex.get_expr(), false, opts);
+        format elb_f  = ex.get_elaborator().pp(fmt, opts);
+        return format({format(ex.what()), space(), format("at term"),
+                    nest(indent, compose(line(), expr_f)),
+                    line(), format("Elaborator state"),
+                    nest(indent, compose(line(), elb_f))});
+    }
 }
 
 regular const & operator<<(regular const & out, elaborator_exception const & ex) {

src/frontends/lean/lean_elaborator_exception.h

@@ -55,6 +55,46 @@ public:
     virtual char const * what() const noexcept { return "type mismatch during term elaboration"; }
 };
 
+class overload_exception : public elaborator_exception {
+    std::vector<expr> m_fs;
+    std::vector<expr> m_f_types;
+    std::vector<expr> m_args;
+    std::vector<expr> m_arg_types;
+public:
+    overload_exception(elaborator const & elb, context const & ctx, expr const & s,
+                          unsigned num_fs, expr const * fs, expr const * ftypes,
+                          unsigned num_args, expr const * args, expr const * argtypes):
+        elaborator_exception(elb, ctx, s),
+        m_fs(fs, fs + num_fs),
+        m_f_types(ftypes, ftypes + num_fs),
+        m_args(args, args + num_args),
+        m_arg_types(argtypes, argtypes + num_args) {
+    }
+    virtual ~overload_exception() {}
+    std::vector<expr> const & get_fs() const { return m_fs; }
+    std::vector<expr> const & get_f_types() const { return m_f_types; }
+    std::vector<expr> const & get_args() const { return m_args; }
+    std::vector<expr> const & get_arg_types() const { return m_arg_types; }
+};
+
+class no_overload_exception : public overload_exception {
+public:
+    no_overload_exception(elaborator const & elb, context const & ctx, expr const & s,
+                          unsigned num_fs, expr const * fs, expr const * ftypes,
+                          unsigned num_args, expr const * args, expr const * argtypes):
+        overload_exception(elb, ctx, s, num_fs, fs, ftypes, num_args, args, argtypes) {}
+    virtual char const * what() const noexcept { return "application type mismatch, none of the overloads can be used"; }
+};
+
+class ambiguous_overload_exception : public overload_exception {
+public:
+    ambiguous_overload_exception(elaborator const & elb, context const & ctx, expr const & s,
+                                 unsigned num_fs, expr const * fs, expr const * ftypes,
+                                 unsigned num_args, expr const * args, expr const * argtypes):
+        overload_exception(elb, ctx, s, num_fs, fs, ftypes, num_args, args, argtypes) {}
+    virtual char const * what() const noexcept { return "ambiguous overloads"; }
+};
+
 format pp(formatter fmt, elaborator_exception const & ex, options const & opts);
 regular const & operator<<(regular const & out, elaborator_exception const & ex);
 diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex);

src/frontends/lean/lean_notation.cpp

@@ -31,6 +31,8 @@ void init_builtin_notation(frontend & f) {
     f.add_infixr("\u21D4", 25, mk_iff_fn());     // "⇔"
 
     f.add_infixl("+", 65, mk_nat_add_fn());
+    f.add_infixl("-", 65, mk_nat_sub_fn());
+    f.add_prefix("-", 75, mk_nat_neg_fn());
     f.add_infixl("*", 70, mk_nat_mul_fn());
     f.add_infix("<=", 50, mk_nat_le_fn());
     f.add_infix("\u2264", 50, mk_nat_le_fn());  // ≤

src/frontends/lean/lean_pp.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "lean_pp.h"
 #include "lean_frontend.h"
 #include "lean_coercion.h"
+#include "lean_elaborator.h"
 
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
 #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()
@@ -922,6 +923,22 @@ class pp_fn {
         return mk_result(r_format, p_arg.second + p_v.second + 1);
     }
 
+    result pp_choice(expr const & e, unsigned depth) {
+        lean_assert(is_choice(e));
+        unsigned num = get_num_choices(e);
+        format r_format;
+        unsigned r_weight;
+        for (unsigned i = 0; i < num; i++) {
+            if (i > 0)
+                r_format += format{space(), format("|"), line()};
+            expr const & c = get_choice(e, i);
+            result p_c     = pp_child(c, depth);
+            r_weight      += p_c.second;
+            r_format      += p_c.first;
+        }
+        return mk_result(r_format, r_weight+1);
+    }
+
     result pp(expr const & e, unsigned depth, bool main = false) {
         check_interrupted(m_interrupted);
         if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) {
@@ -934,7 +951,9 @@ class pp_fn {
                     return mk_result(format(it->second), 1);
             }
             result r;
-            if (is_lower(e)) {
+            if (is_choice(e)) {
+                return pp_choice(e, depth);
+            } if (is_lower(e)) {
                 r = pp_lower(e, depth);
             } else if (is_lift(e)) {
                 r = pp_lift(e, depth);

src/kernel/arith/arith.cpp

@@ -126,6 +126,8 @@ MK_BUILTIN(nat_le_fn, nat_le_value);
 MK_CONSTANT(nat_ge_fn, name({"Nat", "ge"}));
 MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"}));
 MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"}));
+MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
+MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
 // =======================================
 
 // =======================================
@@ -461,6 +463,9 @@ void add_arith_theory(environment & env) {
     env.add_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
     env.add_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
 
+    env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
+    env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
+
     env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(mk_real_value(-1), y))));
     env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(mk_real_value(-1), x)));
     env.add_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));

src/kernel/arith/arith.h

@@ -22,21 +22,35 @@ inline expr nVal(unsigned v) { return mk_nat_value(v); }
 bool is_nat_value(expr const & e);
 mpz const & nat_value_numeral(expr const & e);
 
+/** \brief Nat::add : Nat -> Nat -> Nat */
 expr mk_nat_add_fn();
 inline expr nAdd(expr const & e1, expr const & e2) { return mk_app(mk_nat_add_fn(), e1, e2); }
 
+/** \brief Nat::sub : Nat -> Nat -> Int */
+expr mk_nat_sub_fn();
+inline expr nSub(expr const & e1, expr const & e2) { return mk_app(mk_nat_sub_fn(), e1, e2); }
+
+/** \brief Nat::neg : Nat -> Int */
+expr mk_nat_neg_fn();
+inline expr nNeg(expr const & e1, expr const & e2) { return mk_app(mk_nat_neg_fn(), e1, e2); }
+
+/** \brief Nat::mul : Nat -> Nat -> Nat */
 expr mk_nat_mul_fn();
 inline expr nMul(expr const & e1, expr const & e2) { return mk_app(mk_nat_mul_fn(), e1, e2); }
 
+/** \brief Nat::le : Nat -> Nat -> Bool */
 expr mk_nat_le_fn();
 inline expr nLe(expr const & e1, expr const & e2) { return mk_app(mk_nat_le_fn(), e1, e2); }
 
+/** \brief Nat::ge : Nat -> Nat -> Bool */
 expr mk_nat_ge_fn();
 inline expr nGe(expr const & e1, expr const & e2) { return mk_app(mk_nat_ge_fn(), e1, e2); }
 
+/** \brief Nat::lt : Nat -> Nat -> Bool */
 expr mk_nat_lt_fn();
 inline expr nLt(expr const & e1, expr const & e2) { return mk_app(mk_nat_lt_fn(), e1, e2); }
 
+/** \brief Nat::gt : Nat -> Nat -> Bool */
 expr mk_nat_gt_fn();
 inline expr nGt(expr const & e1, expr const & e2) { return mk_app(mk_nat_gt_fn(), e1, e2); }
 

src/library/formatter.cpp

@@ -56,12 +56,12 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
         }
         format arg_type_msg;
         if (arg_types.size() > 2)
-            arg_type_msg = format("arguments types");
+            arg_type_msg = format("Arguments types:");
         else
-            arg_type_msg = format("argument type");
+            arg_type_msg = format("Argument type:");
         return format({format("type mismatch at application"),
                     nest(indent, compose(line(), app_f)),
-                    line(), format("function type"),
+                    line(), format("Function type:"),
                     nest(indent, compose(line(), f_type_fmt)),
                     line(), arg_type_msg,
                     arg_types_fmt});
@@ -82,7 +82,7 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
         format value_f = operator()(_ex->get_value_type(), opts);
         return format({format("type mismatch at definition '"), name_f, format("', expected type"),
                     nest(indent, compose(line(), type_f)),
-                    line(), format("given type"),
+                    line(), format("Given type:"),
                     nest(indent, compose(line(), value_f))});
     } else {
         return format(ex.what());

tests/lean/arith1.lean

@@ -1,3 +1,4 @@
+Set pp::colors false
 Check 10 + 20
 Check 10
 Check 10 - 20

tests/lean/arith1.lean.expected.out

@@ -1,3 +1,4 @@
+  Set: pp::colors
 Nat
 Nat
 Int

tests/lean/arith3.lean

@@ -1,3 +1,4 @@
+Set pp::colors false
 Eval 8 mod 3
 Eval 8 div 4
 Eval 7 div 3

tests/lean/arith3.lean.expected.out

@@ -1,9 +1,10 @@
+  Set: pp::colors
 2
 2
 2
 1
 - 8 mod 3
   Set: lean::pp::notation
-Int::mod (Int::neg 8) 3
+Int::mod (Nat::neg 8) 3
 -2
 -8

tests/lean/ex2.lean.expected.out

@@ -9,9 +9,9 @@ and a b
   Assumed: A
 Error (line: 12, pos: 11) type mismatch at application
     and a A
-function type
+Function type:
     Bool -> Bool -> Bool
-arguments types
+Arguments types:
     Bool
     Type
 Variable A : Type

tests/lean/ex3.lean.expected.out

@@ -5,9 +5,9 @@ myeq Bool ⊤ ⊥
   Assumed: a
 Error (line: 6, pos: 6) type mismatch at application
     myeq Bool ⊤ a
-function type
+Function type:
     Π (A : Type) (_ _ : A), Bool
-arguments types
+Arguments types:
     Type
     Bool
     T
@@ -15,9 +15,9 @@ arguments types
   Set: lean::pp::implicit
 Error (line: 10, pos: 15) type mismatch at application
     myeq2::explicit Bool ⊤ a
-function type
+Function type:
     Π (A : Type) (a b : A), Bool
-arguments types
+Arguments types:
     Type
     Bool
     T

tests/lean/overload2.lean

@@ -0,0 +1,20 @@
+Show 1 + true
+
+Variable R : Type
+Variable T : Type
+Variable r2t : R -> T
+Coercion r2t
+Variable t2r : T -> R
+Coercion t2r
+Variable f : T -> R -> T
+Variable a : T
+Variable b : R
+Set lean::pp::coercion true
+Set lean::pp::notation false
+Show f a b
+Show f b a
+Variable g : R -> T -> R
+Infix 10 ++ : f
+Infix 10 ++ : g
+Show a ++ b
+Show b ++ a

tests/lean/overload2.lean.expected.out

@@ -0,0 +1,30 @@
+Error (line: 1, pos: 10) application type mismatch, none of the overloads can be used
+Candidates:
+    Real::add : Real → Real → Real
+    Int::add : Int → Int → Int
+    Nat::add : Nat → Nat → Nat
+Arguments:
+    1 : Nat
+    ⊤ : Bool
+  Assumed: R
+  Assumed: T
+  Assumed: r2t
+  Coercion r2t
+  Assumed: t2r
+  Coercion t2r
+  Assumed: f
+  Assumed: a
+  Assumed: b
+  Set: lean::pp::coercion
+  Set: lean::pp::notation
+f a b
+f (r2t b) (t2r a)
+  Assumed: g
+f a b
+Error (line: 20, pos: 10) ambiguous overloads
+Candidates:
+    g : R -> T -> R
+    f : T -> R -> T
+Arguments:
+    b : R
+    a : T

tests/lean/tst9.lean.expected.out

@@ -5,8 +5,8 @@
   Assumed: a
 Error (line: 6, pos: 6) type mismatch at application
     g ⊤ (f _ a a)
-function type
+Function type:
     N → N → Bool
-arguments types
+Arguments types:
     Bool
     ?M0