diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp
index 8b282b6147..638594b3b2 100644
--- a/src/kernel/error_msgs.cpp
+++ b/src/kernel/error_msgs.cpp
@@ -41,4 +41,18 @@ format pp_def_type_mismatch(formatter const & fmt, environment const & env, opti
     r += pp_indent_expr(fmt, env, opts, given_type);
     return r;
 }
+
+format pp_decl_has_metavars(formatter const & fmt, environment const & env, options const & opts, name const & n,
+                            expr const & e, bool is_type) {
+    format r("failed to add declaration '");
+    r += format(n);
+    r += format("' to environment, ");
+    if (is_type)
+        r += format("type");
+    else
+        r += format("value");
+    r += format(" has metavariables");
+    r += pp_indent_expr(fmt, env, opts, e);
+    return r;
+}
 }
diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h
index a2ec5eaa77..f0672e41bf 100644
--- a/src/kernel/error_msgs.h
+++ b/src/kernel/error_msgs.h
@@ -15,4 +15,6 @@ format pp_app_type_mismatch(formatter const & fmt, environment const & env, opti
                             expr const & expected_type, expr const & given_type);
 format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n,
                             expr const & expected_type, expr const & given_type);
+format pp_decl_has_metavars(formatter const & fmt, environment const & env, options const & opts, name const & n,
+                            expr const & e, bool is_type);
 }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 4da46a85a2..57177d0e2b 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -433,9 +433,12 @@ type_checker::type_checker(environment const & env):
 
 type_checker::~type_checker() {}
 
-static void check_no_metavar(environment const & env, expr const & e) {
+static void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
     if (has_metavar(e))
-        throw_kernel_exception(env, "failed to add declaration to environment, it contains metavariables", e);
+        throw_kernel_exception(env, e,
+                               [=](formatter const & fmt, options const & o) {
+                                   return pp_decl_has_metavars(fmt, env, o, n, e, is_type);
+                               });
 }
 
 static void check_no_local(environment const & env, expr const & e) {
@@ -443,8 +446,8 @@ static void check_no_local(environment const & env, expr const & e) {
         throw_kernel_exception(env, "failed to add declaration to environment, it contains local constants", e);
 }
 
-static void check_no_mlocal(environment const & env, expr const & e) {
-    check_no_metavar(env, e);
+static void check_no_mlocal(environment const & env, name const & n, expr const & e, bool is_type) {
+    check_no_metavar(env, n, e, is_type);
     check_no_local(env, e);
 }
 
@@ -466,9 +469,9 @@ static void check_duplicated_params(environment const & env, declaration const &
 }
 
 certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
-    check_no_mlocal(env, d.get_type());
     if (d.is_definition())
-        check_no_mlocal(env, d.get_value());
+        check_no_mlocal(env, d.get_name(), d.get_value(), false);
+    check_no_mlocal(env, d.get_name(), d.get_type(), true);
     check_name(env, d.get_name());
     check_duplicated_params(env, d);
     type_checker checker1(env, g, mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque));