fix: missing check at infer_proj

We should not allow `h.1` if `h` is a proposition and the result is
not. The recursor for `h`'s type can only eliminate into `Prop`.

src/kernel/type_checker.cpp

@@ -262,7 +262,10 @@ expr type_checker::infer_proj(expr const & e, bool infer_only) {
     }
     r = whnf(r);
     if (!is_pi(r)) throw invalid_proj_exception(env(), m_lctx, e);
-    return binding_domain(r);
+    r = binding_domain(r);
+    if (is_prop(type) && !is_prop(r))
+        throw invalid_proj_exception(env(), m_lctx, e);
+    return r;
 }
 
 /** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not.

tests/lean/unsound.lean

@@ -0,0 +1,3 @@
+def foo (h : ∃ x: Nat, True) := h.1
+theorem contradiction : False :=
+  (by decide : 0 ≠ 1) (show foo ⟨0, trivial⟩ = foo ⟨1, trivial⟩ from rfl)

tests/lean/unsound.lean.expected.out

@@ -0,0 +1,4 @@
+unsound.lean:1:4-1:7: error: (kernel) invalid projection
+  h.1
+unsound.lean:3:28-3:31: error: unknown identifier 'foo'
+unsound.lean:3:47-3:50: error: unknown identifier 'foo'