From bccaaa7af0d3c7623ee4e3e103fd901884bcb10f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jan 2020 15:43:21 -0800
Subject: [PATCH] fix: bug at `lit_type` binding

cc @kha
---
 src/kernel/expr.cpp           | 2 +-
 src/kernel/expr.h             | 2 +-
 src/kernel/type_checker.cpp   | 2 +-
 src/library/type_context.cpp  | 2 +-
 tests/lean/run/frontend1.lean | 1 +
 5 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 184efddb1a..44b4fa1a20 100644
--- a/src/kernel/expr.cpp
+++ b/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()); }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 40610917ee..f301e551fa 100644
--- a/src/kernel/expr.h
+++ b/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)); }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index f29aef3b73..649c8747ef 100644
--- a/src/kernel/type_checker.cpp
+++ b/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;
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 14658a69a8..3f91467b90 100644
--- a/src/library/type_context.cpp
+++ b/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);
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index bb7f8269d1..5b36d03638 100644
--- a/tests/lean/run/frontend1.lean
+++ b/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"