fix(library/tactic): we must unfold untrusted macros when type checking intermediate results

Example: before this commit, the file librata/data/list/perm.lean would
not type check if the option -t 0 (trust level zero) was provided.
Reason: the intermediate term contained a macro, and macros are not
allowed at trust level zero.

src/library/tactic/contradiction_tactic.cpp

@@ -51,7 +51,7 @@ tactic contradiction_tactic() {
                                 expr V = mk_app(mk_app(mk_constant(no_confusion, cons(t_lvl, const_levels(I_fn))), args),
                                                 t, lhs, rhs, h);
                                 if (auto r = lift_down_if_hott(*tc, V)) {
-                                    tc->check_ignore_undefined_universes(*r);
+                                    check_term(*tc, *r);
                                     assign(subst, g, *r);
                                     return some_proof_state(proof_state(s, tail(gs), subst, ngen));
                                 }

src/library/tactic/generalize_tactic.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/kernel_exception.h"
 #include "library/reducible.h"
+#include "library/util.h"
 #include "library/tactic/elaborate.h"
 #include "library/tactic/expr_to_tactic.h"
 
@@ -44,7 +45,7 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
                 expr new_t = mk_pi(n, e_t, abstract(t, *new_e));
                 expr new_m = g.mk_meta(ngen.next(), new_t);
                 try {
-                    tc->check_ignore_undefined_universes(g.abstract(new_t));
+                    check_term(*tc, g.abstract(new_t));
                 } catch (kernel_exception const & ex) {
                     std::shared_ptr<kernel_exception> ex_ptr(static_cast<kernel_exception*>(ex.clone()));
                     throw_tactic_exception_if_enabled(s, [=](formatter const & fmt) {

src/library/tactic/rewrite_tactic.cpp

@@ -29,6 +29,7 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/locals.h"
 #include "library/constants.h"
+#include "library/unfold_macros.h"
 #include "library/generic_exception.h"
 #include "library/tactic/clear_tactic.h"
 #include "library/tactic/trace_tactic.h"
@@ -1188,7 +1189,7 @@ class rewrite_fn {
     }
 
     void check_term(expr const & H) {
-        type_checker(m_env).check_ignore_undefined_universes(H);
+        lean::check_term(m_env, H);
     }
 
     bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) {

src/library/util.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/util.h"
 #include "library/constants.h"
+#include "library/unfold_macros.h"
 
 namespace lean {
 bool is_standard(environment const & env) {
@@ -645,4 +646,14 @@ constraint instantiate_metavars(constraint const & c, substitution & s) {
     }}
     lean_unreachable(); // LCOV_EXCL_LINE
 }
+
+void check_term(type_checker & tc, expr const & e) {
+    expr tmp = unfold_untrusted_macros(tc.env(), e);
+    tc.check_ignore_undefined_universes(tmp);
+}
+
+void check_term(environment const & env, expr const & e) {
+    expr tmp = unfold_untrusted_macros(env, e);
+    type_checker(env).check_ignore_undefined_universes(tmp);
+}
 }

src/library/util.h

@@ -191,6 +191,16 @@ bool has_expr_metavar_relaxed(expr const & e);
     elaborator with the tactic framework. */
 constraint instantiate_metavars(constraint const & c, substitution & s);
 
+
+/** \brief Check whether the given term is type correct or not, undefined universe levels are ignored,
+    and untrusted macros are unfolded before performing the test.
+
+    These procedures are useful for checking whether intermediate results produced by
+    tactics and automation are type correct.
+*/
+void check_term(type_checker & tc, expr const & e);
+void check_term(environment const & env, expr const & e);
+
 void initialize_library_util();
 void finalize_library_util();
 }