fix(library/unifier): too much reduction

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/type_checker.h

@@ -95,7 +95,6 @@ class type_checker {
 
     friend class converter; // allow converter to access the following methods
     name mk_fresh_name() { return m_gen.next(); }
-    optional<expr> expand_macro(expr const & m);
     pair<expr, expr> open_binding_body(expr const & e);
     pair<expr, constraint_seq> ensure_sort_core(expr e, expr const & s);
     pair<expr, constraint_seq> ensure_pi_core(expr e, expr const & s);
@@ -199,6 +198,8 @@ public:
             cs = r.second + cs;
         return r.first;
     }
+
+    optional<expr> expand_macro(expr const & m);
 };
 
 typedef std::shared_ptr<type_checker> type_checker_ref;

src/library/unifier.cpp

@@ -1697,6 +1697,19 @@ struct unifier_fn {
         return std::all_of(margs.begin(), margs.end(), [&](expr const & e) { return is_local(e); });
     }
 
+    optional<expr> expand_rhs(expr const & rhs, bool relax) {
+        buffer<expr> args;
+        expr const & f = get_app_rev_args(rhs, args);
+        lean_assert(!is_local(f) && !is_constant(f) && !is_var(f) && !is_metavar(f));
+        if (is_lambda(f)) {
+            return some_expr(apply_beta(f, args.size(), args.data()));
+        } else if (is_macro(f)) {
+            return m_tc[relax]->expand_macro(rhs);
+        } else {
+            return none_expr();
+        }
+    }
+
     /** \brief Process a flex rigid constraint */
     bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) {
         lean_assert(is_meta(lhs));
@@ -1704,12 +1717,12 @@ struct unifier_fn {
         if (is_app(rhs)) {
             expr const & f = get_app_fn(rhs);
             if (!is_local(f) && !is_constant(f)) {
-                constraint_seq cs;
-                expr new_rhs = whnf(rhs, relax, cs);
-                lean_assert(new_rhs != rhs);
-                if (!process_constraints(cs, j))
+                if (auto new_rhs = expand_rhs(rhs, relax)) {
+                    lean_assert(*new_rhs != rhs);
+                    return is_def_eq(lhs, *new_rhs, j, relax);
+                } else {
                     return false;
-                return is_def_eq(lhs, new_rhs, j, relax);
+                }
             }
         }
 

tests/lean/run/sum_bug.lean

@@ -0,0 +1,70 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura, Jeremy Avigad
+
+import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
+
+using inhabited decidable
+
+namespace sum
+
+-- TODO: take this outside the namespace when the inductive package handles it better
+inductive sum (A B : Type) : Type :=
+| inl : A → sum A B
+| inr : B → sum A B
+
+infixr `+`:25 := sum
+
+abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B)
+  (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
+sum_rec H1 H2 s
+
+
+theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
+let f := λs, rec_on s (λa, a1 = a) (λb, false) in
+have H1 : f (inl B a1), from rfl,
+have H2 : f (inl B a2), from subst H H1,
+H2
+
+abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B)
+  (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
+sum_rec H1 H2 s
+
+theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
+let f := λs, rec_on s (λa', a = a') (λb, false) in
+have H1 : f (inl B a), from rfl,
+have H2 : f (inr A b), from subst H H1,
+H2
+
+theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
+let f := λs, rec_on s (λa, false) (λb, b1 = b) in
+have H1 : f (inr A b1), from rfl,
+have H2 : f (inr A b2), from subst H H1,
+H2
+
+theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) :=
+inhabited_mk (inl B (default A))
+
+theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A + B) :=
+inhabited_mk (inr A (default B))
+
+theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B)
+  (H1 : ∀a1 a2, decidable (inl B a1 = inl B a2))
+  (H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
+rec_on s1
+  (take a1, show decidable (inl B a1 = s2), from
+    rec_on s2
+      (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
+      (take b2,
+        have H3 : (inl B a1 = inr A b2) ↔ false,
+          from iff_intro inl_neq_inr (assume H4, false_elim _ H4),
+        show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3)))
+  (take b1, show decidable (inr A b1 = s2), from
+    rec_on s2
+      (take a2,
+        have H3 : (inr A b1 = inl B a2) ↔ false,
+          from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim _ H4),
+        show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
+      (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
+
+end sum