diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index c4caf86b2..5cf604320 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -84,7 +84,7 @@ environment check_cmd(parser & p) {
     e = p.lambda_abstract(section_ps, e);
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     level_param_names new_ls;
-    std::tie(e, new_ls) = p.elaborate(e, false);
+    std::tie(e, new_ls) = p.elaborate_relaxed(e);
     auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
     expr type = tc->check(e, append(ls, new_ls));
     p.regular_stream() << e << " : " << type << endl;
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 1602c1b56..f41589a2d 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -137,7 +137,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
     }
     level_param_names new_ls;
-    std::tie(type, new_ls) = p.elaborate(type);
+    std::tie(type, new_ls) = p.elaborate_type(type);
     update_section_local_levels(p, new_ls);
     return declare_var(p, p.env(), n, append(ls, new_ls), type, is_axiom, bi, pos);
 }
@@ -280,10 +280,10 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     level_param_names new_ls;
     if (is_theorem) {
         // TODO(Leo): delay theorems
-        std::tie(type, value, new_ls) = p.elaborate(n, type, value);
+        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
         env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value)));
     } else {
-        std::tie(type, value, new_ls) = p.elaborate(n, type, value);
+        std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
         env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
     }
     if (modifiers.m_is_class)
@@ -319,7 +319,7 @@ static environment variables_cmd(parser & p) {
     p.parse_close_binder_info(bi);
     level_param_names ls = to_level_param_names(collect_univ_params(type));
     level_param_names new_ls;
-    std::tie(type, new_ls) = p.elaborate(type);
+    std::tie(type, new_ls) = p.elaborate_type(type);
     update_section_local_levels(p, new_ls);
     ls = append(ls, new_ls);
     environment env = p.env();
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 57b8730fd..7fa3abba1 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -981,8 +981,10 @@ public:
         return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
     }
 
-    std::tuple<expr, level_param_names> operator()(expr const & e) {
+    std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type) {
         expr r  = visit(e);
+        if (_ensure_type)
+            r = ensure_type(r);
         auto p  = solve().pull();
         lean_assert(p);
         substitution s = p->first;
@@ -999,7 +1001,7 @@ public:
     }
 
     std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n) {
-        expr r_t      = visit(t);
+        expr r_t      = ensure_type(visit(t));
         expr r_v      = visit(v);
         expr r_v_type = infer_type(r_v);
         environment env = m_env;
@@ -1026,8 +1028,8 @@ public:
 static name g_tmp_prefix = name::mk_internal_unique_name();
 
 std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
-                                              expr const & e, pos_info_provider * pp, bool check_unassigned) {
-    return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e);
+                                              expr const & e, pos_info_provider * pp, bool check_unassigned, bool ensure_type) {
+    return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
 }
 
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 0e050d4f6..8d88c0bde 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios, expr const & e,
-                                              pos_info_provider * pp = nullptr, bool check_unassigned = true);
+                                              pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false);
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
                                                     name const & n, expr const & t, expr const & v, pos_info_provider * pp = nullptr);
 }
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index c1f406889..20a84decc 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -197,7 +197,7 @@ struct inductive_cmd_fn {
             d_type = update_result_sort(d_type, m_u);
             m_infer_result_universe = true;
         }
-        return m_p.elaborate(m_env, d_type);
+        return m_p.elaborate_at(m_env, d_type);
     }
 
     /** \brief Create a local constant based on the given binding */
@@ -435,7 +435,7 @@ struct inductive_cmd_fn {
                 name ir_name; expr ir_type;
                 std::tie(ir_name, ir_type) = ir;
                 level_param_names new_ls;
-                std::tie(ir_type, new_ls) = m_p.elaborate(m_env, ir_type);
+                std::tie(ir_type, new_ls) = m_p.elaborate_at(m_env, ir_type);
                 for (auto l : new_ls) m_levels.push_back(l);
                 accumulate_levels(ir_type, r_lvls);
                 new_irs.push_back(intro_rule(ir_name, ir_type));
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 75ed91056..e9e1dc485 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -467,17 +467,22 @@ expr parser::mk_Type() {
     return mk_sort(mk_level_placeholder());
 }
 
-std::tuple<expr, level_param_names> parser::elaborate(expr const & e, bool check_unassigned) {
+std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
-    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, check_unassigned);
+    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, false);
 }
 
-std::tuple<expr, level_param_names> parser::elaborate(environment const & env, expr const & e) {
+std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e) {
+    parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
+    return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, true, true);
+}
+
+std::tuple<expr, level_param_names> parser::elaborate_at(environment const & env, expr const & e) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
     return ::lean::elaborate(env, m_local_level_decls, m_ios, e, &pp);
 }
 
-std::tuple<expr, expr, level_param_names> parser::elaborate(name const & n, expr const & t, expr const & v) {
+std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v) {
     parser_pos_provider pp(m_pos_table, get_stream_name(), m_last_cmd_pos);
     return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, &pp);
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 6799d7b20..89a5bfae6 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -249,9 +249,14 @@ public:
     */
     struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
 
-    std::tuple<expr, level_param_names> elaborate(expr const & e, bool check_unassigned = true);
-    std::tuple<expr, level_param_names> elaborate(environment const & env, expr const & e);
-    std::tuple<expr, expr, level_param_names> elaborate(name const & n, expr const & t, expr const & v);
+    /** \brief Elaborate \c e, and tolerate metavariables in the result. */
+    std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e);
+    /** \brief Elaborate \c e, and ensure it is a type. */
+    std::tuple<expr, level_param_names> elaborate_type(expr const & e);
+    /** \brief Elaborate \c e in the given environment. */
+    std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
+    /** \brief Elaborate the definition n : t := v */
+    std::tuple<expr, expr, level_param_names> elaborate_definition(name const & n, expr const & t, expr const & v);
 
     /** parse all commands in the input stream */
     bool operator()() { return parse_commands(); }
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index 3263cb041..d317d1e96 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -24,6 +24,8 @@ inductive group : Type :=
 definition carrier (g : group) : Type
 := group_rec (λ c s, c) g
 
+coercion carrier
+
 definition group_to_struct [instance] (g : group) : group_struct (carrier g)
 := group_rec (λ (A : Type) (s : group_struct A), s) g
 
@@ -37,12 +39,17 @@ infixl `*`:75 := mul
 section
   variable  G1 : group
   variable  G2 : group
-  variables a b c : (carrier G2)
-  variables d e : (carrier G1)
+  variables a b c : G2
+  variables d e   : G1
   check a * b * b
   check d * e
 end
 
+variable G : group.{1}
+variables a b : G
+definition val : G := a*b
+check val
+
 variable pos_real : Type.{1}
 variable rmul  : pos_real → pos_real → pos_real
 variable rone  : pos_real