From 4c28cb933b91e623988f4cb51d853e49a085ff2c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Aug 2013 16:44:22 -0700
Subject: [PATCH] Fix bug in is_convertible

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/type_check.cpp | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index 7ca56f261..decd9e510 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -17,11 +17,21 @@ namespace lean {
 bool is_convertible_core(expr const & expected, expr const & given, environment const & env) {
     if (expected == given)
         return true;
-    if (is_type(expected) && is_type(given)) {
-        if (env.is_ge(ty_level(expected), ty_level(given)))
-            return true;
+    expr const * e = &expected;
+    expr const * g = &given;
+    while (true) {
+        if (is_type(*e) && is_type(*g)) {
+            if (env.is_ge(ty_level(*e), ty_level(*g)))
+                return true;
+        }
+        if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) {
+            e = &abst_body(*e);
+            g = &abst_body(*g);
+        }
+        else {
+            return false;
+        }
     }
-    return false;
 }
 
 bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) {