fix(library/tactic/rewrite_tactic): fixes #1277

src/library/CMakeLists.txt

@@ -17,4 +17,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
   locals.cpp normalize.cpp discr_tree.cpp
   mt_task_queue.cpp st_task_queue.cpp task_helper.cpp
-  messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp)
+  messages.cpp message_buffer.cpp versioned_msg_buf.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
+  documentation.cpp check.cpp)

src/library/check.cpp

@@ -0,0 +1,145 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/expr_sets.h"
+#include "kernel/instantiate.h"
+#include "library/trace.h"
+#include "library/type_context.h"
+
+namespace lean {
+struct check_fn {
+    type_context &   m_ctx;
+    expr_struct_set  m_visited;
+
+    void visit_constant(expr const & e) {
+        declaration d = m_ctx.env().get(const_name(e));
+        if (d.get_num_univ_params() != length(const_levels(e))) {
+            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
+                       tout() << "incorrect of universe levels at " << e << "\n";);
+            throw exception("check failed, incorrect number of universe levels "
+                            "(use 'set_option trace.check true' for additional details)");
+        }
+    }
+
+    void visit_macro(expr const & e) {
+        for (unsigned i = 0; i < macro_num_args(e); i++)
+            visit(macro_arg(e, i));
+    }
+
+    void ensure_type(expr const & e) {
+        if (!is_sort(m_ctx.relaxed_whnf(m_ctx.infer(e)))) {
+            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
+                       tout() << "type expected at " << e << "\n";);
+            throw exception("check failed, type expected "
+                            "(use 'set_option trace.check true' for additional details)");
+        }
+    }
+
+    void visit_binding(expr const & e, bool is_pi) {
+        type_context::tmp_locals locals(m_ctx);
+        expr it = e;
+        while (it.kind() == e.kind()) {
+            expr d = instantiate_rev(binding_domain(it), locals.size(), locals.data());
+            visit(d);
+            locals.push_local(binding_name(it), d, binding_info(it));
+            ensure_type(d);
+            it = binding_body(it);
+        }
+        expr b = instantiate_rev(it, locals.size(), locals.data());
+        visit(b);
+        if (is_pi)
+            ensure_type(b);
+    }
+
+    void visit_lambda(expr const & e) {
+        visit_binding(e, false);
+    }
+
+    void visit_pi(expr const & e) {
+        visit_binding(e, true);
+    }
+
+    void visit_let(expr const & e) {
+        visit(let_value(e));
+        visit(let_type(e));
+        expr v_type = m_ctx.infer(let_value(e));
+        if (!m_ctx.relaxed_is_def_eq(let_type(e), v_type)) {
+            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
+                       tout() << "type mismatch at let binder\n  " << e << "\n";);
+            throw exception("check failed, type mismatch at let binder "
+                            "(use 'set_option trace.check true' for additional details)");
+        }
+        /* Improve performance if bottleneck */
+        type_context::tmp_locals locals(m_ctx);
+        expr local = locals.push_local_from_let(e);
+        visit(instantiate(let_body(e), local));
+    }
+
+    void visit_app(expr const & e) {
+        visit(app_fn(e));
+        visit(app_arg(e));
+        expr f_type = m_ctx.relaxed_whnf(m_ctx.infer(app_fn(e)));
+        if (!is_pi(f_type)) {
+            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
+                       tout() << "function expected at\n  " << e << "\ntype\n  " << f_type << "\n";);
+            throw exception("check failed, function expected (use 'set_option trace.check true' for additional details)");
+        }
+        expr a_type = m_ctx.infer(app_arg(e));
+        expr d_type = binding_domain(f_type);
+        if (!m_ctx.relaxed_is_def_eq(a_type, d_type)) {
+            lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
+                       tout() << "application type mismatch at\n  " << e << "\nargument type\n  "
+                       << a_type << "\nexpected type\n  " << d_type;);
+            throw exception("check failed, application type mismatch "
+                            "(use 'set_option trace.check true' for additional details)");
+        }
+    }
+
+    void visit(expr const & e) {
+        if (m_visited.find(e) != m_visited.end())
+            return;
+        m_visited.insert(e);
+        switch (e.kind()) {
+        case expr_kind::Local:
+        case expr_kind::Meta:
+        case expr_kind::Sort:
+            break; /* do nothing */
+        case expr_kind::Constant:
+            return visit_constant(e);
+        case expr_kind::Var:
+            lean_unreachable();  // LCOV_EXCL_LINE
+        case expr_kind::Macro:
+            return visit_macro(e);
+        case expr_kind::Lambda:
+            return visit_lambda(e);
+        case expr_kind::Pi:
+            return visit_pi(e);
+        case expr_kind::App:
+            return visit_app(e);
+        case expr_kind::Let:
+            return visit_let(e);
+        }
+    }
+
+public:
+    check_fn(type_context & ctx):m_ctx(ctx) {}
+    void operator()(expr const & e) { return visit(e); }
+};
+
+void check(type_context & ctx, expr const & e) {
+    metavar_context mctx = ctx.mctx();
+    check_fn checker(ctx);
+    checker(e);
+    ctx.set_mctx(mctx);
+}
+
+void initialize_check() {
+    register_trace_class("check");
+}
+
+void finalize_check() {
+}
+}

src/library/check.h

@@ -0,0 +1,20 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/type_context.h"
+
+namespace lean {
+/* Type check 'e' using the given type context.
+   It throws an exception in case of failure.
+
+   This procedure is use to check the proof-term produced by tactics such as
+   rewrite.
+*/
+void check(type_context & ctx, expr const & e);
+void initialize_check();
+void finalize_check();
+}

src/library/init_module.cpp

@@ -50,6 +50,7 @@ Author: Leonardo de Moura
 #include "library/comp_val.h"
 #include "library/documentation.h"
 #include "library/defeq_canonizer.h"
+#include "library/check.h"
 
 namespace lean {
 void initialize_library_core_module() {
@@ -110,9 +111,11 @@ void initialize_library_module() {
     initialize_comp_val();
     initialize_documentation();
     initialize_defeq_canonizer();
+    initialize_check();
 }
 
 void finalize_library_module() {
+    finalize_check();
     finalize_defeq_canonizer();
     finalize_documentation();
     finalize_comp_val();

src/library/tactic/rewrite_tactic.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/app_builder.h"
 #include "library/constants.h"
 #include "library/trace.h"
+#include "library/check.h"
 #include "library/pp_options.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_option.h"
@@ -105,6 +106,11 @@ vm_obj rewrite(transparency_mode const & m, bool approx, bool use_instances, occ
     /* Motive and resulting type */
     expr new_e  = ctx.instantiate_mvars(instantiate(e_abst, target ? rhs : lhs));
     expr motive = mk_lambda("a", A, e_abst);
+    try {
+        check(ctx, motive);
+    } catch (exception & ex) {
+        throw nested_exception("rewrite tactic failed, motive is not type correct", ex);
+    }
     if (target) {
         expr prf        = mk_eq_rec(ctx, motive, *target, H);
         name Hname      = is_local(*target) ? local_pp_name(*target) : name("H");
@@ -130,14 +136,18 @@ vm_obj rewrite(transparency_mode const & m, bool approx, bool use_instances, occ
 }
 
 vm_obj tactic_rewrite(vm_obj const & m, vm_obj const & approx, vm_obj const & use_instances, vm_obj const & occs, vm_obj const & symm, vm_obj const & H, vm_obj const & s) {
+    LEAN_TACTIC_TRY;
     return rewrite(to_transparency_mode(m), to_bool(approx), to_bool(use_instances),
                    to_occurrences(occs), to_bool(symm), to_expr(H), none_expr(), to_tactic_state(s));
+    LEAN_TACTIC_CATCH(to_tactic_state(s));
 }
 
 vm_obj tactic_rewrite_at(vm_obj const & m, vm_obj const & approx, vm_obj const & use_instances,
                          vm_obj const & occs, vm_obj const & symm, vm_obj const & H1, vm_obj const & H2, vm_obj const & s) {
+    LEAN_TACTIC_TRY;
     return rewrite(to_transparency_mode(m), to_bool(approx), to_bool(use_instances), to_occurrences(occs),
                    to_bool(symm), to_expr(H1), some_expr(to_expr(H2)), to_tactic_state(s));
+    LEAN_TACTIC_CATCH(to_tactic_state(s));
 }
 
 void initialize_rewrite_tactic() {

tests/lean/1277.lean

@@ -0,0 +1,11 @@
+variables {α₁ : Type} {α₂ : α₁ → Type} {β₁ : Type} {β₂ : β₁ → Type}
+
+def map (f₁ : α₁ → β₁) (f₂ : Π⦃a⦄, α₂ a → β₂ (f₁ a)) : (Σa, α₂ a) → (Σb, β₂ b)
+| ⟨a₁, a₂⟩ := ⟨f₁ a₁, f₂ a₂⟩
+
+set_option trace.check true
+
+example (f₁ : α₁ → α₁) (f₂ : Π⦃a⦄, α₂ a → α₂ (f₁ a)) (eq₁ : f₁ = id) : map f₁ f₂ = id :=
+begin
+  rw [eq₁],
+end

tests/lean/1277.lean.expected.out

@@ -0,0 +1,23 @@
+[check] application type mismatch at
+  map a f₂
+argument type
+  Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a)
+expected type
+  Π ⦃a_1 : α₁⦄, (λ (a : α₁), α₂ a) a_1 → α₂ (a a_1)/home/leo/projects/lean/tests/lean/1277.lean:10:2: error: rewrite tactic failed, motive is not type correct
+nested exception message:
+check failed, application type mismatch (use 'set_option trace.check true' for additional details)
+state:
+α₁ : Type,
+α₂ : α₁ → Type,
+f₁ : α₁ → α₁,
+f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
+eq₁ : f₁ = id
+⊢ map f₁ f₂ = id
+1277.lean:11:0: error: failed
+state:
+α₁ : Type,
+α₂ : α₁ → Type,
+f₁ : α₁ → α₁,
+f₂ : Π ⦃a : α₁⦄, α₂ a → α₂ (f₁ a),
+eq₁ : f₁ = id
+⊢ map f₁ f₂ = id