fix(library/unifier): missing occurs check

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.

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.

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) {

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. */

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);

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 {