fix: bug at lit_type binding

cc @kha

src/kernel/expr.cpp

@@ -77,7 +77,7 @@ extern "C" uint8 lean_expr_binder_info(object * e);
 binder_info binding_info(expr const & e) { return static_cast<binder_info>(lean_expr_binder_info(e.to_obj_arg())); }
 
 extern "C" object * lean_lit_type(obj_arg e);
-expr lit_type(expr const & e) { return expr(lean_lit_type(e.to_obj_arg())); }
+expr lit_type(literal const & lit) { return expr(lean_lit_type(lit.to_obj_arg())); }
 
 extern "C" usize lean_expr_hash(obj_arg e);
 unsigned hash(expr const & e) { return lean_expr_hash(e.to_obj_arg()); }

src/kernel/expr.h

@@ -226,7 +226,7 @@ expr mk_Type();
 inline literal const & lit_value(expr const & e)             { lean_assert(is_lit(e)); return static_cast<literal const &>(cnstr_get_ref(e, 0)); }
 inline bool is_nat_lit(expr const & e)                       { return is_lit(e) && lit_value(e).kind() == literal_kind::Nat; }
 inline bool is_string_lit(expr const & e)                    { return is_lit(e) && lit_value(e).kind() == literal_kind::String; }
-expr lit_type(expr const & e);
+expr lit_type(literal const & e);
 inline kvmap const &   mdata_data(expr const & e)            { lean_assert(is_mdata(e)); return static_cast<kvmap const &>(cnstr_get_ref(e, 0)); }
 inline expr const &    mdata_expr(expr const & e)            { lean_assert(is_mdata(e)); return static_cast<expr const &>(cnstr_get_ref(e, 1)); }
 inline name const &    proj_sname(expr const & e)            { lean_assert(is_proj(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }

src/kernel/type_checker.cpp

@@ -271,7 +271,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
 
     expr r;
     switch (e.kind()) {
-    case expr_kind::Lit:      r = lit_type(e);    break;
+    case expr_kind::Lit:      r = lit_type(lit_value(e)); break;
     case expr_kind::MData:    r = infer_type_core(mdata_expr(e), infer_only); break;
     case expr_kind::Proj:     r = infer_proj(e, infer_only); break;
     case expr_kind::FVar:     r = infer_fvar(e);  break;

src/library/type_context.cpp

@@ -994,7 +994,7 @@ expr type_context_old::infer_core(expr const & e) {
         r = local_type(e);
         break;
     case expr_kind::Lit:
-        r = lit_type(e);
+        r = lit_type(lit_value(e));
         break;
     case expr_kind::MVar:
         r = infer_metavar(e);

tests/lean/run/frontend1.lean

@@ -202,3 +202,4 @@ f a
 #eval run "def x := Nat.zero #check x"
 #eval run "open Lean.Parser def x := parser! symbol \"foo\" Nat.zero #check x"
 #eval run "open Lean.Parser def x := tparser! symbol \"foo\" Nat.zero #check x"
+#eval run "def x : Nat := 1 #check x"