diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index dcc10f407..2e0d0c7bb 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 000000000..383608452
--- /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