diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index 2f3717fe2b..45f1810d3e 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -355,7 +355,8 @@ struct eta_expand_rec_apps_fn : public replace_visitor_with_tc {
 };
 
 static expr compile_equations_main(environment & env, elaborator & elab,
-                                   metavar_context & mctx, local_context const & lctx, expr const & _eqns, bool report_cexs) {
+                                   metavar_context & mctx, local_context const & lctx, expr const & _eqns,
+                                   bool report_cexs) {
     // all following code assumes that all recursive occurrences are applications
     type_context_old ctx(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
     expr eqns = eta_expand_rec_apps_fn(ctx)(_eqns);
@@ -402,7 +403,8 @@ expr compile_equations(environment & env, elaborator & elab, metavar_context & m
         aux_header.m_aux_lemmas = false;
         aux_header.m_fn_actual_names = map(header.m_fn_actual_names, mk_unsafe_rec_name);
         expr aux_eqns = remove_wf_annotation_from_equations(update_equations(eqns, aux_header));
-        compile_equations_main(env, elab, mctx, lctx, aux_eqns, false);
+        aux_eqns      = eta_expand_rec_apps_fn(ctx)(aux_eqns);
+        unbounded_rec(env, elab, mctx, lctx, aux_eqns, some_expr(result));
         return result;
     } else {
         return compile_equations_main(env, elab, mctx, lctx, eqns, true);
diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp
index 24cedf28c8..ec7bddaf7c 100644
--- a/src/library/equations_compiler/unbounded_rec.cpp
+++ b/src/library/equations_compiler/unbounded_rec.cpp
@@ -82,7 +82,8 @@ static expr fix_rec_apps(expr const & e, name_map<name> const & aux_rec_name2act
 
 eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
                                   metavar_context & mctx, local_context const & lctx,
-                                  expr const & e) {
+                                  expr const & e, optional<expr> const & safe_result) {
+    lean_assert(!safe_result || is_equations_result(*safe_result));
     /* Split recursive equations by using new auxiliary `.rec` locals */
     buffer<expr> aux_rec_fns;
     buffer<expr> es;
@@ -118,6 +119,11 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
             for (list<expr> const & ts : R.m_counter_examples) {
                 counter_examples.push_back(mk_app(ues.get_fn(0), ts));
             }
+            if (safe_result) {
+                lean_assert(is_equations_result(*safe_result));
+                lean_assert(get_equations_result_size(*safe_result) == es.size());
+                helper.collect(get_equations_result(*safe_result, fidx));
+            }
         }
         helper.finalize_collection();
 
diff --git a/src/library/equations_compiler/unbounded_rec.h b/src/library/equations_compiler/unbounded_rec.h
index 88004fa9a1..587daa2bb1 100644
--- a/src/library/equations_compiler/unbounded_rec.h
+++ b/src/library/equations_compiler/unbounded_rec.h
@@ -9,11 +9,17 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/util.h"
 namespace lean {
 class elaborator;
-/** \brief Eliminate "recursive calls" using rec_fn_macro.
+/** \brief Eliminate "recursive calls" using unbounded recursion.
 
     This compilation step can only be used to compile unsafe definitions.
-    If we use it on regular definitions, the kernel will reject it. */
+    If we use it on regular definitions, the kernel will reject it.
+
+    Remark: If `eqns` has already been compiled in safe mode,
+    then `safe_result` contains the result of the compilation.
+    We need this information to make sure the type of the auxiliary `_unsafe_rec` definitions
+    match the type of the regular ones.
+*/
 eqn_compiler_result unbounded_rec(environment & env, elaborator & elab,
                                   metavar_context & mctx, local_context const & lctx,
-                                  expr const & eqns);
+                                  expr const & eqns, optional<expr> const & safe_result = optional<expr>());
 }