From 2dad1e0e3347366683ed908a93bb39bc99ed0e69 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Aug 2013 19:24:11 -0700
Subject: [PATCH] Fix type mismatch error message

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/type_check.cpp       |  4 ++--
 src/tests/kernel/type_check.cpp | 15 +++++++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index 01115b9a2..fd91b78c7 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -134,12 +134,12 @@ struct infer_type_fn {
                 expr const & c = arg(e, i);
                 expr c_t       = infer_type(c, ctx);
                 if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx)) {
-                    format msg = format{format("type mismatch at argument "), format(i), format("of"),
+                    format msg = format{format("type mismatch at argument "), format(i), space(), format("of"),
                                         nl_indent(fmt()(e, ctx)), line(),
                                         format("expected type:"),
                                         nl_indent(fmt()(abst_domain(f_t), ctx)), line(),
                                         format("given type:"),
-                                        nl_indent(fmt()(c_t, ctx))};
+                                        nl_indent(fmt()(c_t, ctx)), line()};
                     push_context(msg, ctx);
                     throw_exception(arg(e,i), msg);
                 }
diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp
index fd9dc5b01..c32920ec3 100644
--- a/src/tests/kernel/type_check.cpp
+++ b/src/tests/kernel/type_check.cpp
@@ -115,6 +115,20 @@ static void tst6() {
     }
 }
 
+static void tst7() {
+    environment env = mk_toplevel();
+    expr A = Const(name{"foo", "bla", "bla", "foo"});
+    expr f = Const("f");
+    expr x = Const("x");
+    expr t = Fun({A, Type()}, Fun({f, arrow(Int, arrow(A, arrow(A, arrow(A, arrow(A, arrow(A, A))))))}, Fun({x, Int}, f(x, x))));
+    try {
+        infer_type(t, env);
+        lean_unreachable();
+    } catch (exception & ex) {
+        std::cout << "Error: " << ex.what() << "\n";
+    }
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
@@ -123,5 +137,6 @@ int main() {
     tst4();
     tst5();
     tst6();
+    tst7();
     return has_violations() ? 1 : 0;
 }