diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index e5df2d1f5..05e1ecc77 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -233,7 +233,7 @@ static void tst5() {
 #endif
 }
 
-void tst6() {
+static void tst6() {
     environment env;
     expr x = Const("x");
     expr t = Fun({x, Type()}, mk_app(x, x));
@@ -253,5 +253,6 @@ int main() {
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }
diff --git a/tests/lean/tst8.lean b/tests/lean/tst8.lean
index 6aef8a164..7c1baff1e 100644
--- a/tests/lean/tst8.lean
+++ b/tests/lean/tst8.lean
@@ -8,3 +8,6 @@ Definition f (A: Type) (a : A) : A :=
    let b := g A a,
        c := g A b
    in c
+
+Show f _ 10.
+Show f _ (- 10).
diff --git a/tests/lean/tst8.lean.expected.out b/tests/lean/tst8.lean.expected.out
index 81384291f..09a98f224 100644
--- a/tests/lean/tst8.lean.expected.out
+++ b/tests/lean/tst8.lean.expected.out
@@ -3,3 +3,5 @@
 Π (A : Type) (a : A), A
   Assumed: g
   Defined: f
+f Nat 10
+f Int (- 10)