From 3746005f5fc35d030d26ced2f7bcaabc295224c2 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 1 Mar 2022 16:34:44 +0100
Subject: [PATCH] =?UTF-8?q?fix:=20reject=20projection=20`(=5F=20:=20?=
 =?UTF-8?q?=E2=88=83=20x,=20p).2`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The inferred type of this projection does not even type check, in general.
---
 src/kernel/type_checker.cpp          | 10 +++++++---
 tests/lean/magical.lean              |  4 ++++
 tests/lean/magical.lean.expected.out |  4 +++-
 3 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b097689ea4..60ca5f9ea1 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -252,18 +252,22 @@ expr type_checker::infer_proj(expr const & e, bool infer_only) {
         if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
         r = instantiate(binding_body(r), args[i]);
     }
+    bool is_prop_type = is_prop(type);
     for (unsigned i = 0; i < idx; i++) {
         r = whnf(r);
         if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
-        if (has_loose_bvars(binding_body(r)))
+        if (has_loose_bvars(binding_body(r))) {
+            if (is_prop_type && !is_prop(binding_domain(r)))
+                throw invalid_proj_exception(env(), m_lctx, e);
             r = instantiate(binding_body(r), mk_proj(I_name, i, proj_expr(e)));
-        else
+        } else {
             r = binding_body(r);
+        }
     }
     r = whnf(r);
     if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
     r = binding_domain(r);
-    if (is_prop(type) && !is_prop(r))
+    if (is_prop_type && !is_prop(r))
         throw invalid_proj_exception(env(), m_lctx, e);
     return r;
 }
diff --git a/tests/lean/magical.lean b/tests/lean/magical.lean
index f217e1b9a0..81f707fec1 100644
--- a/tests/lean/magical.lean
+++ b/tests/lean/magical.lean
@@ -1 +1,5 @@
+-- Projection to the witness should be rejected.
 def witness : Nat := (⟨1, Nat.le_refl _⟩ : ∃ x, x ≥ 1).1
+
+-- Projection to the property as well (it could contain the witness projection).
+theorem witness_eq (h : ∃ x : Nat, True) : h.2 = h.2 := rfl
diff --git a/tests/lean/magical.lean.expected.out b/tests/lean/magical.lean.expected.out
index 56f322d532..3957ad5b53 100644
--- a/tests/lean/magical.lean.expected.out
+++ b/tests/lean/magical.lean.expected.out
@@ -1,6 +1,8 @@
-magical.lean:1:21-1:56: error: invalid projection, the expression
+magical.lean:2:21-2:56: error: invalid projection, the expression
   Exists.intro 1 (Nat.le_refl 1)
 is a proposition and has type
   ∃ x, x ≥ 1
 but the projected value is not, it has type
   Nat
+magical.lean:5:8-5:18: error: (kernel) invalid projection
+  h.2