From 697a536d9eb44caa07031e47c553f48ae09e117c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Apr 2015 19:24:52 -0700
Subject: [PATCH] fix(library/tactic/inversion_tactic): type incorrect term
 being built by 'cases' tactic

fixes #545
---
 src/library/tactic/inversion_tactic.cpp     | 37 ++++++++++++++-------
 tests/lean/cases_failure.hlean              | 13 ++++++++
 tests/lean/cases_failure.hlean.expected.out | 34 +++++++++++++++++++
 3 files changed, 72 insertions(+), 12 deletions(-)
 create mode 100644 tests/lean/cases_failure.hlean
 create mode 100644 tests/lean/cases_failure.hlean.expected.out

diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index a8c909cd8..a2cd0629d 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -700,6 +700,19 @@ class inversion_tac {
         }
     }
 
+    [[ noreturn ]] void throw_unify_eqs_failure(goal const & g) {
+        if (m_throw_tactic_exception) {
+            throw tactic_exception([=](formatter const & fmt) {
+                    format r("invalid 'cases' tactic, unification failed");
+                    r += compose(line(), format("auxiliary goal at time of failure"));
+                    r += nest(get_pp_indent(fmt.get_options()), compose(line(), g.pp(fmt)));
+                    return r;
+                });
+        } else {
+            throw inversion_exception();
+        }
+    }
+
     // Remark: it also updates m_renames and m_imps
     optional<goal> unify_eqs(goal g, unsigned neqs) {
         if (neqs == 0)
@@ -803,10 +816,19 @@ class inversion_tac {
                 level eq_rec_lvl1   = sort_level(m_tc.ensure_type(deps_g_type).first);
                 level eq_rec_lvl2   = sort_level(m_tc.ensure_type(A).first);
                 expr tformer;
-                if (m_proof_irrel)
+                if (m_proof_irrel) {
                     tformer = Fun(rhs, deps_g_type);
-                else
+                } else {
+                    if (depends_on(lhs, rhs)) {
+                        // tformer must be of the form
+                        //   fun x, fun (Heq : lhs = x, ...)
+                        // If the lhs contains occurrences of rhs, then
+                        // we would produce the following ill-typed tformer
+                        //   fun x, fun (Heq : lhs[x] = x, ...)
+                        throw_unify_eqs_failure(g);
+                    }
                     tformer = Fun(rhs, Fun(Heq, deps_g_type));
+                }
                 expr eq_rec         = mk_constant(get_eq_rec_name(), {eq_rec_lvl1, eq_rec_lvl2});
                 eq_rec              = mk_app(eq_rec, A, lhs, tformer);
                 buffer<expr> new_hyps;
@@ -877,16 +899,7 @@ class inversion_tac {
                 return unify_eqs(new_g, neqs);
             }
         }
-        if (m_throw_tactic_exception) {
-            throw tactic_exception([=](formatter const & fmt) {
-                    format r("invalid 'cases' tactic, unification failed");
-                    r += compose(line(), format("auxiliary goal at time of failure"));
-                    r += nest(get_pp_indent(fmt.get_options()), compose(line(), g.pp(fmt)));
-                    return r;
-                });
-        } else {
-            throw inversion_exception();
-        }
+        throw_unify_eqs_failure(g);
     }
 
     auto unify_eqs(list<goal> const & gs, list<list<expr>> args, list<implementation_list> imps) ->
diff --git a/tests/lean/cases_failure.hlean b/tests/lean/cases_failure.hlean
new file mode 100644
index 000000000..348b7a95e
--- /dev/null
+++ b/tests/lean/cases_failure.hlean
@@ -0,0 +1,13 @@
+-- .hlean file
+open eq
+
+inductive square {A : Type} {a₀₀ : A}
+  : Π{a₀₁ a₁₀ a₁₁ : A}, a₀₀ = a₀₁ → a₁₀ = a₁₁ → a₀₀ = a₁₀ → a₀₁ = a₁₁ → Type :=
+ids : square idp idp idp idp
+
+definition foo {A : Type} {x y z : A} {t : x = y} {b : z = y} {l : x = z} {r : y = y}
+  (s : square t b l r)  : unit :=
+begin
+  cases s,
+  exact unit.star
+end
diff --git a/tests/lean/cases_failure.hlean.expected.out b/tests/lean/cases_failure.hlean.expected.out
new file mode 100644
index 000000000..ced0aa679
--- /dev/null
+++ b/tests/lean/cases_failure.hlean.expected.out
@@ -0,0 +1,34 @@
+cases_failure.hlean:11:2: error:invalid 'cases' tactic, unification failed
+auxiliary goal at time of failure
+  A : Type,
+  x y z : A,
+  b r t l : z = z,
+  s : square t b l r,
+  e_3 : z = z
+  ⊢ Π (e_4 : eq.rec t (refl z) = idp) (e_5 : eq.rec (eq.rec b (refl z)) e_3 = idp) (e_6 : eq.rec l (refl z) = idp)
+    (e_7 : eq.rec (eq.rec r (refl z)) e_3 = idp),
+      eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec (eq.rec s (refl z)) (refl z)) e_3) e_4) e_5) e_6)
+        e_7 = square.ids →
+      unit
+proof state:
+A : Type,
+x y z : A,
+t : x = y,
+b : z = y,
+l : x = z,
+r : y = y,
+s : square t b l r
+⊢ unit
+cases_failure.hlean:13:0: error: don't know how to synthesize placeholder
+A : Type,
+x y z : A,
+t : x = y,
+b : z = y,
+l : x = z,
+r : y = y,
+s : square t b l r
+⊢ unit
+cases_failure.hlean:13:0: error: failed to add declaration 'foo' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (x y z : A) (t : …) (b : …) (l : …) (r : …) (s : …),
+    ?M_1