fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/data/quotient/basic.lean

@@ -281,7 +281,7 @@ idempotent_image_fix (representative_map_idempotent H1 H2) b
 
 theorem representative_map_to_quotient {A : Type} {R : A → A → Prop} {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') :
-  is_quotient _ (fun_image f) elt_of :=
+  is_quotient R (fun_image f) elt_of :=
 let abs := fun_image f in
 intro
   (take u : image f,

src/frontends/lean/decl_cmds.cpp

@@ -312,6 +312,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         if (is_theorem) {
             auto type_pos = p.pos_of(type);
             std::tie(type, new_ls) = p.elaborate_type(type);
+            check_no_metavar(env, real_n, type, true);
             ls = append(ls, new_ls);
             expr type_as_is = p.save_pos(mk_as_is(type), type_pos);
             if (!p.collecting_info() && p.num_threads() > 1) {

src/kernel/type_checker.cpp

@@ -421,7 +421,7 @@ type_checker::type_checker(environment const & env):
 
 type_checker::~type_checker() {}
 
-static void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
+void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
     if (has_metavar(e))
         throw_kernel_exception(env, e, [=](formatter const & fmt) { return pp_decl_has_metavars(fmt, n, e, is_type); });
 }

src/kernel/type_checker.h

@@ -204,6 +204,8 @@ public:
 
 typedef std::shared_ptr<type_checker> type_checker_ref;
 
+void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type);
+
 /**
    \brief Type check the given declaration, and return a certified declaration if it is type correct.
    Throw an exception if the declaration is type incorrect.