From db38bc404388b6b7ea2fe4589f417265a988eb95 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Feb 2022 07:15:34 -0800 Subject: [PATCH] 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 | 5 ++++- tests/lean/unsound.lean | 3 +++ tests/lean/unsound.lean.expected.out | 4 ++++ 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 tests/lean/unsound.lean create mode 100644 tests/lean/unsound.lean.expected.out diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 59df747054..b097689ea4 100644 --- a/src/kernel/type_checker.cpp +++ b/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. diff --git a/tests/lean/unsound.lean b/tests/lean/unsound.lean new file mode 100644 index 0000000000..9bc1833063 --- /dev/null +++ b/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) diff --git a/tests/lean/unsound.lean.expected.out b/tests/lean/unsound.lean.expected.out new file mode 100644 index 0000000000..5aa44c511b --- /dev/null +++ b/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'