feat: reject [macroInline] declarations in recursive declarations

closes #1363

src/Lean/Compiler/InlineAttrs.lean

@@ -12,15 +12,36 @@ inductive InlineAttributeKind where
   | inline | noinline | macroInline | inlineIfReduce
   deriving Inhabited, BEq
 
+/--
+  This is an approximate test for testing whether `declName` can be annotated with the `[macroInline]` attribute or not.
+-/
+private def isValidMacroInline (declName : Name) : CoreM Bool := do
+  let .defnInfo info ← getConstInfo declName
+    | return false
+  unless info.all.length = 1 do
+    -- We do not allow `[macroInline]` attributes at mutual recursive definitions
+    return false
+  let env ← getEnv
+  let isRec (declName' : Name) : Bool :=
+    isBRecOnRecursor env declName' ||
+    declName' == ``WellFounded.fix ||
+    declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module
+  if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then
+    -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie
+    return false
+  return true
+
 builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ←
   registerEnumAttributes `inlineAttrs
     [(`inline, "mark definition to always be inlined", InlineAttributeKind.inline),
      (`inlineIfReduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", InlineAttributeKind.inlineIfReduce),
      (`noinline, "mark definition to never be inlined", InlineAttributeKind.noinline),
      (`macroInline, "mark definition to always be inlined before ANF conversion", InlineAttributeKind.macroInline)]
-    (fun declName _ => do
-      let env ← getEnv
-      ofExcept <| checkIsDefinition env declName)
+    fun declName kind => do
+      ofExcept <| checkIsDefinition (← getEnv) declName
+      if kind matches .macroInline then
+        unless (← isValidMacroInline declName) do
+          throwError "invalid use of `[macro_inline]` attribute at `{declName}`, it is not supported in this kind of declaration, declaration must be a non-recursive definition"
 
 private partial def hasInlineAttrAux (env : Environment) (kind : InlineAttributeKind) (n : Name) : Bool :=
   /- We never inline auxiliary declarations created by eager lambda lifting -/

src/library/compiler/util.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
+#include "kernel/find_fn.h"
 #include "kernel/inductive.h"
 #include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
@@ -129,6 +130,16 @@ struct unfold_macro_defs_fn : public replace_visitor {
     unfold_macro_defs_fn(environment const & env):m_env(env) {}
 
 
+    bool should_macro_inline(name const & n) {
+        if (!has_macro_inline_attribute(m_env, n)) return false;
+        auto info = m_env.get(n);
+        if (!info.has_value())
+            return false;
+        bool is_rec = static_cast<bool>(find(info.get_value(), [&](expr const & e, unsigned) { return is_const(e, n); }));
+        // We do not macro_inline recursive definitions. TODO: check that when setting the attribute.
+        return !is_rec;
+    }
+
     virtual expr visit_app(expr const & e) override {
         buffer<expr> args;
         expr const & fn = get_app_args(e, args);
@@ -141,7 +152,7 @@ struct unfold_macro_defs_fn : public replace_visitor {
         }
         if (is_constant(fn)) {
             name const & n = const_name(fn);
-            if (has_macro_inline_attribute(m_env, n)) {
+            if (should_macro_inline(n)) {
                 expr new_fn = instantiate_value_lparams(m_env.get(n), const_levels(fn));
                 std::reverse(args.begin(), args.end());
                 return visit(apply_beta(new_fn, args.size(), args.data()));
@@ -156,7 +167,7 @@ struct unfold_macro_defs_fn : public replace_visitor {
 
     virtual expr visit_constant(expr const & e) override {
         name const & n = const_name(e);
-        if (has_macro_inline_attribute(m_env, n)) {
+        if (should_macro_inline(n)) {
             return visit(instantiate_value_lparams(m_env.get(n), const_levels(e)));
         } else {
             return e;

tests/lean/1363.lean

@@ -0,0 +1,25 @@
+import Lean.Data.Parsec
+open Lean Parsec
+
+@[macroInline] -- Error
+def f : Nat → Nat
+  | 0 => 0
+  | n + 1 => f n
+
+@[macroInline] -- Error
+def g : Nat → Nat
+  | 0 => 0
+  | n + 1 => g n
+termination_by g x => x
+
+@[macroInline] -- Error
+def h : Nat → Nat → Nat
+  | 0, _ => 0
+  | n + 1, m => h n m
+termination_by h x y => x
+
+@[macroInline] -- Error
+partial def skipMany (p : Parsec α) (it : String.Iterator) : Parsec PUnit := do
+  match p it with
+  | .success it _ => skipMany p it
+  | .error _ _  => pure ()

tests/lean/1363.lean.expected.out

@@ -0,0 +1,5 @@
+1363.lean:4:2-4:13: error: invalid use of `[macro_inline]` attribute at `f`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
+1363.lean:9:2-9:13: error: invalid use of `[macro_inline]` attribute at `g`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
+1363.lean:15:2-15:13: error: invalid use of `[macro_inline]` attribute at `h._unary`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
+1363.lean:15:2-15:13: error: invalid use of `[macro_inline]` attribute at `h`, it is not supported in this kind of declaration, declaration must be a non-recursive definition
+1363.lean:21:2-21:13: error: invalid use of `[macro_inline]` attribute at `skipMany`, it is not supported in this kind of declaration, declaration must be a non-recursive definition