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

@@ -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);
+            }
         }
     }
 

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