fix: reject projection (_ : ∃ x, p).2

The inferred type of this projection does not even type check, in general.

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;
 }

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

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