fix(library/tactic): type check generalization result, fixes #273

src/kernel/type_checker.cpp

@@ -362,6 +362,11 @@ pair<expr, constraint_seq> type_checker::check(expr const & e, level_param_names
     return infer_type_core(e, false);
 }
 
+pair<expr, constraint_seq> type_checker::check_ignore_levels(expr const & e) {
+    flet<level_param_names const *> updt(m_params, nullptr);
+    return infer_type_core(e, false);
+}
+
 pair<expr, constraint_seq> type_checker::ensure_sort(expr const & e, expr const & s) {
     return ensure_sort_core(e, s);
 }

src/kernel/type_checker.h

@@ -145,6 +145,8 @@ public:
        The result is meaningful only if the generated constraints can be solved.
     */
     pair<expr, constraint_seq> check(expr const & t, level_param_names const & ps = level_param_names());
+    /** \brief Like \c check, but ignores undefined universe level parameters */
+    pair<expr, constraint_seq> check_ignore_levels(expr const & e);
 
     /** \brief Return true iff t is definitionally equal to s. */
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);

src/library/tactic/generalize_tactic.cpp

@@ -34,6 +34,12 @@ 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);
                 expr new_v = g.abstract(mk_app(new_m, *new_e));
+                try {
+                    tc->check_ignore_levels(g.abstract(new_t));
+                } catch (exception &) {
+                    return none_proof_state();
+                }
+
                 subst.assign(g.get_name(), new_v);
                 goal new_g(new_m, new_t);
                 return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen));

tests/lean/gen_bug.lean

@@ -0,0 +1,24 @@
+import logic
+
+set_option pp.notation false
+set_option pp.implicit true
+
+theorem tst (A B : Type) (a : A) (b : B) : a == b → b == a :=
+begin
+  intro H,
+  generalize B, -- Should produce an error
+  intro B',
+  apply (heq.symm H),
+end
+
+theorem tst (A B : Type) (a : A) (b : B) : a == b → b == a :=
+begin
+  generalize a,
+  generalize b,
+  generalize B,
+  intro B',
+  intro b,
+  intro a,
+  intro H,
+  apply (heq.symm H),
+end

tests/lean/gen_bug.lean.expected.out

@@ -0,0 +1,10 @@
+gen_bug.lean:9:2: error: tactic failed
+A : Type,
+B : Type,
+a : A,
+b : B,
+H : @heq A a B b
+⊢ @heq B b A a
+gen_bug.lean:12:0: error: failed to add declaration 'tst' to environment, value has metavariables
+  λ (A B : Type) (a : A) (b : B),
+    ?M_1