fix: kernel must ensure that safe functions cannot use partial ones.

Fix issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Meaning.20of.20.60DefinitionSafety.2Epartial.60

src/kernel/environment.cpp

@@ -118,11 +118,15 @@ static void check_constant_val(environment const & env, constant_val const & v,
     checker.ensure_sort(sort, v.get_type());
 }
 
-static void check_constant_val(environment const & env, constant_val const & v, bool safe_only) {
-    type_checker checker(env, safe_only);
+static void check_constant_val(environment const & env, constant_val const & v, definition_safety ds) {
+    type_checker checker(env, ds);
     check_constant_val(env, v, checker);
 }
 
+static void check_constant_val(environment const & env, constant_val const & v, bool safe_only) {
+  check_constant_val(env, v, safe_only ? definition_safety::safe : definition_safety::unsafe);
+}
+
 void environment::add_core(constant_info const & info) {
     m_obj = lean_environment_add(m_obj, info.to_obj_arg());
 }
@@ -144,14 +148,12 @@ environment environment::add_definition(declaration const & d, bool check) const
         /* Meta definition can be recursive.
            So, we check the header, add, and then type check the body. */
         if (check) {
-            bool safe_only = false;
-            type_checker checker(*this, safe_only);
+            type_checker checker(*this, definition_safety::unsafe);
             check_constant_val(*this, v.to_constant_val(), checker);
         }
         environment new_env = add(constant_info(d));
         if (check) {
-            bool safe_only = false;
-            type_checker checker(new_env, safe_only);
+            type_checker checker(new_env, definition_safety::unsafe);
             check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());
             expr val_type = checker.check(v.get_value(), v.get_lparams());
             if (!checker.is_def_eq(val_type, v.get_type()))
@@ -204,10 +206,9 @@ environment environment::add_mutual(declaration const & d, bool check) const {
     definition_safety safety = head(vs).get_safety();
     if (safety == definition_safety::safe)
         throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as unsafe/partial");
-    bool safe_only = safety == definition_safety::partial;
     /* Check declarations header */
     if (check) {
-        type_checker checker(*this, safe_only);
+        type_checker checker(*this, safety);
         for (definition_val const & v : vs) {
             if (v.get_safety() != safety)
                 throw kernel_exception(*this, "invalid mutual definition, declarations must have the same safety annotation");
@@ -221,7 +222,7 @@ environment environment::add_mutual(declaration const & d, bool check) const {
     }
     /* Check actual definitions */
     if (check) {
-        type_checker checker(new_env, safe_only);
+        type_checker checker(new_env, safety);
         for (definition_val const & v : vs) {
             check_no_metavar_no_fvar(new_env, v.get_name(), v.get_value());
             expr val_type = checker.check(v.get_value(), v.get_lparams());

src/kernel/inductive.cpp

@@ -167,7 +167,7 @@ public:
         to_buffer(decl.get_types(), m_ind_types);
     }
 
-    type_checker tc() { return type_checker(m_env, m_lctx, !m_is_unsafe); }
+    type_checker tc() { return type_checker(m_env, m_lctx, m_is_unsafe ? definition_safety::unsafe : definition_safety::safe); }
 
     /** Return type of the parameter at position `i` */
     expr get_param_type(unsigned i) const {

src/kernel/type_checker.cpp

@@ -90,12 +90,17 @@ expr type_checker::infer_constant(expr const & e, bool infer_only) {
                                << const_name(e) << "', #"
                                << length(ps)  << " expected, #" << length(ls) << " provided");
     if (!infer_only) {
-        if (m_safe_only && info.is_unsafe()) {
+        if (info.is_unsafe() && m_definition_safety != definition_safety::unsafe) {
             throw kernel_exception(env(), sstream() << "invalid declaration, it uses unsafe declaration '"
                                    << const_name(e) << "'");
         }
-        for (level const & l : ls)
+        if (info.is_definition() && info.to_definition_val().get_safety() == definition_safety::partial && m_definition_safety == definition_safety::safe) {
+            throw kernel_exception(env(), sstream() << "invalid declaration, safe declaration must not contain partial declaration '"
+                                   << const_name(e) << "'");
+        }
+        for (level const & l : ls) {
             check_level(l);
+        }
     }
     return instantiate_type_lparams(info, ls);
 }
@@ -1092,19 +1097,19 @@ expr type_checker::eta_expand(expr const & e) {
     return m_lctx.mk_lambda(fvars, r);
 }
 
-type_checker::type_checker(environment const & env, local_ctx const & lctx, bool safe_only):
+type_checker::type_checker(environment const & env, local_ctx const & lctx, definition_safety ds):
     m_st_owner(true), m_st(new state(env)),
-    m_lctx(lctx), m_safe_only(safe_only), m_lparams(nullptr) {
+    m_lctx(lctx), m_definition_safety(ds), m_lparams(nullptr) {
 }
 
-type_checker::type_checker(state & st, local_ctx const & lctx, bool safe_only):
+type_checker::type_checker(state & st, local_ctx const & lctx, definition_safety ds):
     m_st_owner(false), m_st(&st), m_lctx(lctx),
-    m_safe_only(safe_only), m_lparams(nullptr) {
+    m_definition_safety(ds), m_lparams(nullptr) {
 }
 
 type_checker::type_checker(type_checker && src):
     m_st_owner(src.m_st_owner), m_st(src.m_st), m_lctx(std::move(src.m_lctx)),
-    m_safe_only(src.m_safe_only), m_lparams(src.m_lparams) {
+    m_definition_safety(src.m_definition_safety), m_lparams(src.m_lparams) {
     src.m_st_owner = false;
 }
 

src/kernel/type_checker.h

@@ -43,7 +43,7 @@ private:
     bool                      m_st_owner;
     state *                   m_st;
     local_ctx                 m_lctx;
-    bool                      m_safe_only;
+    definition_safety         m_definition_safety;
     /* When `m_lparams != nullptr, the `check` method makes sure all level parameters
        are in `m_lparams`. */
     names const *             m_lparams;
@@ -100,10 +100,10 @@ private:
     template<typename F> optional<expr> reduce_bin_nat_pred(F const & f, expr const & e);
     optional<expr> reduce_nat(expr const & e);
 public:
-    type_checker(state & st, local_ctx const & lctx, bool safe_only = true);
-    type_checker(state & st, bool safe_only = true):type_checker(st, local_ctx(), safe_only) {}
-    type_checker(environment const & env, local_ctx const & lctx, bool safe_only = true);
-    type_checker(environment const & env, bool safe_only = true):type_checker(env, local_ctx(), safe_only) {}
+    type_checker(state & st, local_ctx const & lctx, definition_safety ds = definition_safety::safe);
+    type_checker(state & st, definition_safety ds = definition_safety::safe):type_checker(st, local_ctx(), ds) {}
+    type_checker(environment const & env, local_ctx const & lctx, definition_safety ds = definition_safety::safe);
+    type_checker(environment const & env, definition_safety ds = definition_safety::safe):type_checker(env, local_ctx(), ds) {}
     type_checker(type_checker &&);
     type_checker(type_checker const &) = delete;
     ~type_checker();

tests/lean/partialIssue.lean

@@ -0,0 +1,12 @@
+import Lean.CoreM
+
+#eval Lean.addDecl <| .mutualDefnDecl [{
+  name := `False_intro
+  levelParams := []
+  type := .const ``False []
+  value := .const `False_intro []
+  hints := .opaque
+  safety := .partial
+}]
+
+theorem False.intro : False := False_intro

tests/lean/partialIssue.lean.expected.out

@@ -0,0 +1,2 @@
+
+partialIssue.lean:12:8-12:19: error: (kernel) invalid declaration, safe declaration must not contain partial declaration 'False_intro'