diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 1eb1eb359..73ae0115a 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -298,9 +298,9 @@ environment add_coercion(environment const & env, name const & f, name const & C expr fn = mk_constant(f, const_levels(C_fn)); optional cls = type_to_coercion_class(binding_body(t)); if (!cls) - throw exception(sstream() << "invalid coercion, '" << f << "' does not have the expected type to be used as a coercion"); + throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'"); else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C) - throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' on itself"); + throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); return add_coercion(env, C, fn, d.get_type(), d.get_params(), num, *cls, ios); } t = binding_body(t); @@ -317,7 +317,7 @@ environment add_coercion(environment const & env, name const & f, io_state const t = binding_body(t); expr C = get_app_fn(binding_domain(t)); if (!is_constant(C)) - throw exception(sstream() << "invalid coercion, '" << f << "' does not have the expected type to be used as a coercion"); + throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion"); return add_coercion(env, f, const_name(C), ios); } diff --git a/tests/lua/coe4.lua b/tests/lua/coe4.lua new file mode 100644 index 000000000..c2085815d --- /dev/null +++ b/tests/lua/coe4.lua @@ -0,0 +1,23 @@ +local env = environment() +local l = param_univ("l") +local Ul = mk_sort(l) +local lst_l = Const("lst", {l}) +local A = Local("A", Ul) +env = add_decl(env, mk_var_decl("lst", {l}, mk_arrow(Ul, Ul))) +env = add_decl(env, mk_var_decl("lst2lst", {l}, Pi(A, mk_arrow(lst_l(A), lst_l(A))))) +env = add_decl(env, mk_var_decl("head", {l}, Pi(A, mk_arrow(lst_l(A), A)))) +env = add_decl(env, mk_var_decl("id", {l}, Pi(A, mk_arrow(A, A)))) +function add_bad_coercion(env, c) + ok, msg = pcall(function() add_coercion(env, c) end) + assert(not ok) + print("Expected error: " .. tostring(msg:what())) +end +function add_bad_coercion2(env, c, cls) + ok, msg = pcall(function() add_coercion(env, c, cls) end) + assert(not ok) + print("Expected error: " .. tostring(msg:what())) +end +add_bad_coercion(env, "lst2lst") +add_bad_coercion(env, "head") +add_bad_coercion(env, "id") +add_bad_coercion2(env, "head", "lst")