From 836357c65c16efb316e07a89b2039ea04e0dc3de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 17 Dec 2013 12:35:25 -0800
Subject: [PATCH] fix(kernel/normalizer): bug in Let normalization

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/normalizer.cpp       |  2 +-
 src/tests/kernel/normalizer.cpp | 13 +++++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 46ed6fb7b..bc0242b88 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -267,7 +267,7 @@ class normalizer::imp {
             svalue v = normalize(let_value(a), s, k);
             {
                 freset<cache> reset(m_cache);
-                r = normalize(let_body(a), extend(s, v), k+1);
+                r = normalize(let_body(a), extend(s, v), k);
             }
             break;
         }}
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index 620911d0b..a619a3f30 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -291,6 +291,18 @@ static void tst8() {
     lean_assert_eq(N1, N2);
 }
 
+static void tst9() {
+    environment env;
+    expr f = Const("f");
+    env->add_var("f", Type() >> (Type() >> Type()));
+    expr x = Const("x");
+    expr v = Const("v");
+    expr F = Fun({x, Type()}, Let({v, Bool}, f(x, v)));
+    expr N = normalizer(env)(F);
+    std::cout << F << " ==> " << N << "\n";
+    lean_assert_eq(N, Fun({x, Type()}, f(x, Bool)));
+}
+
 int main() {
     save_stack_info();
     tst_church_numbers();
@@ -302,5 +314,6 @@ int main() {
     tst6();
     tst7();
     tst8();
+    tst9();
     return has_violations() ? 1 : 0;
 }