From 5bc62f0ba90cfb1db0089fe3a67d78e82ffbbdc0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Aug 2014 06:59:52 -0700 Subject: [PATCH] fix(library/coercion): error message Signed-off-by: Leonardo de Moura --- src/library/coercion.cpp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 9aee122a9..14a268499 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -109,6 +109,16 @@ static void check_pi(name const & f, expr const & t) { throw exception(sstream() << "invalid coercion, '" << f << "' is not function"); } +// similar to check_pi, but produces a more informative message +static void check_valid_coercion(name const & f, expr const & t) { + if (!is_pi(t)) { + throw exception(sstream() << "invalid coercion, type of '" << f << "' does not match any of the allowed expected types for coercions\n" + << " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), D t_1 ... t_m\n" + << " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), Type\n" + << " Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), A -> B\n"); + } +} + /** \brief Return true iff args contains Var(0), Var(1), ..., Var(args.size() - 1) */ static bool check_var_args(buffer const & args) { for (unsigned i = 0; i < args.size(); i++) { @@ -294,7 +304,7 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc } t = binding_body(t); num++; - check_pi(f, t); + check_valid_coercion(f, t); } }