From 16553e77fa6992086db55c80b9b8260e93db6358 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 May 2014 14:17:34 -0700 Subject: [PATCH] fix(kernel/type_checker): avoid assertion violation due to API misuse Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index ce9c66389..d0a7089af 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -276,6 +276,9 @@ struct type_checker::imp { \pre closed(e) */ expr infer_type_core(expr const & e, bool infer_only) { + if (is_var(e)) + throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e); + lean_assert(closed(e)); check_system("type checker"); @@ -291,7 +294,7 @@ struct type_checker::imp { r = mlocal_type(e); break; case expr_kind::Var: - throw_kernel_exception(m_env, "type checker does not support free variables, replace them with local constants before invoking it", e); + lean_unreachable(); // LCOV_EXCL_LINE case expr_kind::Sort: if (!infer_only) check_level(sort_level(e), e);