From d79a62652318873e951973cfa274c0b8ea075c27 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Dec 2013 13:07:33 -0800
Subject: [PATCH] fix(kernel/type_checker): Pi with metavariables case

The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/type_checker.cpp  | 4 ++--
 src/library/type_inferer.cpp | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 43e3750a6..e357b8254 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -173,9 +173,9 @@ class type_checker::imp {
         case expr_kind::Pi: {
             expr t1  = check_type(infer_type_core(abst_domain(e), ctx), abst_domain(e), ctx);
             expr t2;
+            context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
             {
                 cache::mk_scope sc(m_cache);
-                context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
                 t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx);
             }
             if (is_type(t1) && is_type(t2)) {
@@ -184,7 +184,7 @@ class type_checker::imp {
                 lean_assert(m_uc);
                 justification jst = mk_max_type_justification(ctx, e);
                 r = m_menv->mk_metavar(ctx);
-                m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, jst));
+                m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst));
             }
             break;
         }
diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index 8e9171662..7e674d421 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -181,9 +181,9 @@ class type_inferer::imp {
         case expr_kind::Pi: {
             expr t1  = check_type(infer_type(abst_domain(e), ctx), abst_domain(e), ctx);
             expr t2;
+            context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
             {
                 cache::mk_scope sc(m_cache);
-                context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
                 t2 = check_type(infer_type(abst_body(e), new_ctx), abst_body(e), new_ctx);
             }
             if (is_type(t1) && is_type(t2)) {
@@ -192,7 +192,7 @@ class type_inferer::imp {
                 lean_assert(m_uc);
                 justification jst = mk_max_type_justification(ctx, e);
                 r = m_menv->mk_metavar(ctx);
-                m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, jst));
+                m_uc->push_back(mk_max_constraint(new_ctx, lift_free_vars(t1, 0, 1), t2, r, jst));
             }
             break;
         }