fix: another specialize.cpp bug

This is just a workaround. This code has to be ported to Lean.

The issue has been reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20unknown.20constant/near/283750650

src/library/compiler/specialize.cpp

@@ -919,7 +919,17 @@ class specialize_fn {
         buffer<expr> new_let_decls;
         name y("_y");
         for (unsigned i = 0; i < fvars.size(); i++) {
-            expr type     = tc.infer(fvar_vals[i]);
+            expr type;
+            try {
+                type = tc.infer(fvar_vals[i]);
+            } catch (exception &) {
+                /* We may fail to infer the type of fvar_vals, since it may be recursive
+                   This is a workaround. When we re-implement the compiler in Lean,
+                   we should write code to infer type that tolerates undefined constants,
+                   *AnyType*, etc.
+                   We just do not specialize when we cannot infer the type. */
+                return optional<comp_decl>();
+            }
             if (is_irrelevant_type(m_st, m_lctx, type)) {
                 /* In LCNF, the type `ty` at `let x : ty := v in t` must not be irrelevant. */
                 code = replace_fvar(code, fvars[i], fvar_vals[i]);

tests/lean/run/specialize3.lean

@@ -0,0 +1,20 @@
+class Class where
+instance empty: Class := {}
+
+mutual
+inductive T (δ: Class) where
+| mk (ss: List (S δ))
+
+inductive S (δ: Class) where
+| mk (ts: List (T δ))
+end
+
+mutual
+partial def str_T: T δ → String
+| .mk ss => "\n".intercalate (ss.map str_S)
+
+partial def str_S: S δ → String
+| .mk ts => "\n".intercalate (ts.map str_T)
+end
+
+def error := str_T (T.mk (δ := empty) [])