diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 5c2a750a8..7d438e757 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -305,16 +305,6 @@ level mk_result_level(environment const & env, buffer<level> const & r_lvls) {
     }
 }
 
-bool occurs(level const & u, level const & l) {
-    bool found = false;
-    for_each(l, [&](level const & l) {
-            if (found) return false;
-            if (l == u) { found = true; return false; }
-            return true;
-        });
-    return found;
-}
-
 /** \brief Functional object for converting the universe metavariables in an expression in new universe parameters.
     The substitution is updated with the mapping metavar -> new param.
     The set of parameter names m_params and the buffer m_new_params are also updated.
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 1d93162a0..87b689157 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -78,8 +78,6 @@ expr Fun_as_is(buffer<expr> const & locals, expr const & e, parser & p);
 expr Pi_as_is(buffer<expr> const & locals, expr const & e, parser & p);
 /** \brief Create the resultant universe level using the levels computed during introduction rule elaboration */
 level mk_result_level(environment const & env, buffer<level> const & r_lvls);
-/** \brief Return true if \c u occurs in \c l */
-bool occurs(level const & u, level const & l);
 
 /** \brief Convert the universe metavariables in \c e in new universe parameters.
     The substitution \c s is updated with the mapping metavar -> new param.
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 0ede5ed5d..f8fae30bd 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -418,6 +418,16 @@ level replace_level_fn::apply(level const & l) {
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
+bool occurs(level const & u, level const & l) {
+    bool found = false;
+    for_each(l, [&](level const & l) {
+            if (found) return false;
+            if (l == u) { found = true; return false; }
+            return true;
+        });
+    return found;
+}
+
 optional<name> get_undef_param(level const & l, level_param_names const & ps) {
     optional<name> r;
     for_each(l, [&](level const & l) {
diff --git a/src/kernel/level.h b/src/kernel/level.h
index 251a02c59..0a6e64c6c 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -200,6 +200,9 @@ public:
 };
 template<typename F> level replace(level const & l, F const & f) { return replace_level_fn(f)(l); }
 
+/** \brief Return true if \c u occurs in \c l */
+bool occurs(level const & u, level const & l);
+
 typedef list<name> level_param_names;
 
 /** \brief If \c l contains a global that is not in \c env, then return it. Otherwise, return none. */
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 79d44a284..8e36e339c 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -74,6 +74,7 @@ void substitution::assign(name const & m, expr const & t, justification const &
 }
 
 void substitution::assign(name const & m, level const & l, justification const & j) {
+    lean_assert(!::lean::occurs(mk_meta_univ(m), l), m, l);
     m_level_subst.insert(m, l);
     if (!j.is_none())
         m_level_jsts.insert(m, j);
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 0c8c5f52b..bbc94d5db 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -2504,6 +2504,8 @@ struct unifier_fn {
         }
         if (!is_meta(m))
             return Continue;
+        if (occurs(m, lhs))
+            return Continue;
         if (assign(m, lhs, jst)) {
             return Solved;
         } else {