From eb3a236119590f5676a3626f0bc3320f8ae5cd9f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 May 2015 16:17:38 -0700
Subject: [PATCH] fix(library/unifier): typo

fixes #588
---
 src/library/unifier.cpp |  2 +-
 tests/lean/run/588.lean | 20 ++++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/588.lean

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index dcc10f4070..2e0d0c7bb6 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1359,7 +1359,7 @@ struct unifier_fn {
         expr rhs_fn     = get_app_rev_args(rhs, rhs_args);
         declaration d   = *m_env.find(const_name(lhs_fn));
         levels lhs_lvls = const_levels(lhs_fn);
-        levels rhs_lvls = const_levels(lhs_fn);
+        levels rhs_lvls = const_levels(rhs_fn);
         if (length(lhs_lvls) != length(rhs_lvls) ||
             d.get_num_univ_params() != length(lhs_lvls)) {
             // the constraint is not well-formed, this can happen when users are abusing the API
diff --git a/tests/lean/run/588.lean b/tests/lean/run/588.lean
new file mode 100644
index 0000000000..383608452d
--- /dev/null
+++ b/tests/lean/run/588.lean
@@ -0,0 +1,20 @@
+import standard
+open function
+
+variables {a b r : Type}
+
+definition f a := Πr, (a -> r) -> r
+
+definition g (fn : a -> b) (sa : f a) : f b := sorry
+
+-- ok
+check λx, g id x = x
+
+check λ(x : f a), g id x = x
+
+universe variables l₁ l₂ l₃
+
+check λ (x : f.{_ l₂} a), g.{_ _ l₂ l₂} id x = x
+
+example (x : f a) : g id x = x :=
+sorry