From 0c15724e8e13b618ee41508693553532bfb2eac9 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 3 Aug 2017 17:36:36 +0100
Subject: [PATCH] fix(library/tactic/simplify): handle universe polymorphic
 simplification rules

The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not.  Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
---
 src/library/tactic/simplify.cpp    |  6 +++++-
 tests/lean/run/simp_univ_poly.lean | 23 +++++++++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/simp_univ_poly.lean

diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 9c856ea9f1..1d74421f38 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -322,7 +322,11 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const &
 
             expr pf_body = finalize(m_ctx, const_name(h_rel), r_congr_hyp).get_proof();
             expr pf      = local_factory.mk_lambda(pf_body);
-            tmp_ctx.assign(m, pf);
+            if (!tmp_ctx.is_def_eq(m, pf)) {
+                lean_simp_trace(tmp_ctx, name({"simplify", "congruence"}),
+                    tout() << "failed to unify proof " << pf << " of " << tmp_ctx.infer(pf););
+                return simp_result(e);
+            }
         }
     }
 
diff --git a/tests/lean/run/simp_univ_poly.lean b/tests/lean/run/simp_univ_poly.lean
new file mode 100644
index 0000000000..52e0cea0ac
--- /dev/null
+++ b/tests/lean/run/simp_univ_poly.lean
@@ -0,0 +1,23 @@
+universes u v
+
+def equinumerous (α : Type u) (β : Type v) :=
+∃ f : α → β, function.bijective f
+
+local infix ` ≈ ` := equinumerous
+
+@[refl] lemma refl {α} : α ≈ α := sorry
+@[trans] lemma trans {α β γ} :
+    α ≈ β → β ≈ γ → α ≈ γ := sorry
+
+@[congr] lemma equinumerous.congr_eqn {α α' β β'} :
+    α ≈ α' → β ≈ β' → (α ≈ β) = (α' ≈ β') := sorry
+
+@[congr] lemma congr_sum {α α' β β'} :
+    α ≈ α' → β ≈ β' → (α ⊕ β) ≈ (α' ⊕ β') := sorry
+
+@[simp] lemma eqn_ulift {α} : ulift α ≈ α := sorry
+
+@[simp] lemma sum_empty {α} : (α ⊕ empty) ≈ α := sorry
+
+-- rewriting `ulift empty` ==> `empty` changes the universe level
+example {α : Type u} : (α ⊕ ulift empty) ≈ α := by simp
\ No newline at end of file