From 5bef45b1fd5725122c8b77b4fb442a8ed92c3ba9 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 13 Aug 2015 21:11:39 -0700 Subject: [PATCH] feat(library/coercion): improve error message when target is unacceptable --- src/library/coercion.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 9b7f4c43d..1b3bcdc49 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -341,8 +341,9 @@ static environment add_coercion(environment const & env, name const & f, name co check_levels(const_levels(C_fn), d.get_univ_params())) { optional cls = type_to_coercion_class(binding_body(t)); if (!cls) - throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" - << C << "'"); + throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from source '" + << C << "', since target does not match any of the acceptable forms\n" + << "D t_1 ... t_m\n" << "Type\n" << "Pi x : A, B x\n"); else if (is_user_class(*cls) && *cls == C) throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); return add_coercion_core(env, C, f, num, *cls, persistent);