From 682df7699db05a508d3e44904362204146c65aca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Aug 2013 01:23:12 -0700
Subject: [PATCH] Fix is_convertible propositions => type

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/normalize.cpp        | 4 ++++
 src/tests/kernel/type_check.cpp | 9 +++++++++
 2 files changed, 13 insertions(+)

diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index d9a40726f..74da6036a 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -244,6 +244,10 @@ class normalizer::imp {
                     if (m_env.is_ge(ty_level(*e), ty_level(*g)))
                         return true;
                 }
+
+                if (is_type(*e) && *g == mk_bool_type())
+                    return true;
+
                 if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
                     e = &abst_body(*e);
                     g = &abst_body(*g);
diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp
index 87fac7b7f..0e78a0ccf 100644
--- a/src/tests/kernel/type_check.cpp
+++ b/src/tests/kernel/type_check.cpp
@@ -239,6 +239,14 @@ static void tst12() {
 #endif
 }
 
+static void tst13() {
+    environment env = mk_toplevel();
+    env.add_var("f", Type() >> Type());
+    expr f = Const("f");
+    std::cout << infer_type(f(Bool), env) << "\n";
+    std::cout << infer_type(f(Eq(True,False)), env) << "\n";
+}
+
 int main() {
     tst1();
     tst2();
@@ -252,5 +260,6 @@ int main() {
     tst10();
     tst11();
     tst12();
+    tst13();
     return has_violations() ? 1 : 0;
 }