refactor: use isRecursiveDefinition when validating macro_inline (#12106)

This PR uses `isRecursiveDefinition` when validating `macro_inline`,
instead of rummaging in the internals of the definition.

src/Lean/Compiler/InlineAttrs.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Attributes
+import Lean.Meta.RecExt
 
 public section
 
@@ -33,14 +34,8 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
   unless info.all.length = 1 do
     -- We do not allow `[macro_inline]` attributes at mutual recursive definitions
     return false
-  let env ← getEnv
-  let isRec (declName' : Name) : Bool :=
-    isBRecOnRecursor env declName' ||
-    declName' == ``WellFounded.fix ||
-    declName' == ``WellFounded.Nat.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
+  if (← Meta.isRecursiveDefinition declName) then
+    -- It is recursive
     return false
   return true
 

src/Lean/Elab/PreDefinition/Mutual.lean

@@ -29,6 +29,10 @@ def addPreDefsFromUnary (docCtx : LocalContext × LocalInstances) (preDefs : Arr
   let preDefNonRec := unaryPreDefNonRec.filterAttrs fun attr => attr.name != `implemented_by
   let declNames := preDefs.toList.map (·.declName)
 
+  preDefs.forM fun preDef =>
+    unless preDef.kind.isTheorem do
+      markAsRecursive preDef.declName
+
   -- Do not complain if the user sets @[semireducible], which usually is a noop,
   -- we recognize that below and then do not set @[irreducible]
   withOptions (allowUnsafeReducibility.set · true) do
@@ -53,8 +57,6 @@ def cleanPreDef (preDef : PreDefinition) (cacheProofs := true) : MetaM PreDefini
 Assign final attributes to the definitions. Assumes the EqnInfos to be already present.
 -/
 def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
-  for preDef in preDefs do
-    markAsRecursive preDef.declName
   for preDef in preDefs.reverse do
     -- must happen before `generateEagerEqns`
     -- must happen in reverse order so that constants realized as part of the first decl

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -140,6 +140,8 @@ def structuralRecursion
   preDefsNonRec.forM fun preDefNonRec => do
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     prependError m!"structural recursion failed, produced type incorrect term" do
+      unless preDefNonRec.kind.isTheorem do
+        markAsRecursive preDefNonRec.declName
       -- We create the `_unsafe_rec` before we abstract nested proofs.
       -- Reason: the nested proofs may be referring to the _unsafe_rec.
       addNonRec docCtx preDefNonRec (applyAttrAfterCompilation := false) (all := names.toList)
@@ -157,7 +159,6 @@ def structuralRecursion
         -/
         registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos fixedParamPerms
     addSmartUnfoldingDef docCtx preDef recArgPos
-    markAsRecursive preDef.declName
   for preDef in preDefs do
     -- must happen in separate loop so realizations can see eqnInfos of all other preDefs
     enableRealizationsForConst preDef.declName

src/Lean/Meta/Eqns.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Meta.Match.MatcherInfo
 public import Lean.DefEqAttrib
+public import Lean.Meta.RecExt
 public import Lean.Meta.LetToHave
 import Lean.Meta.AppBuilder
 
@@ -40,26 +41,6 @@ This is implemented by
 -/
 def eqnAffectingOptions : Array (Lean.Option Bool) := #[backward.eqns.nonrecursive, backward.eqns.deepRecursiveSplit]
 
-/--
-Environment extension for storing which declarations are recursive.
-This information is populated by the `PreDefinition` module, but the simplifier
-uses when unfolding declarations.
--/
-builtin_initialize recExt : TagDeclarationExtension ←
-  mkTagDeclarationExtension `recExt (asyncMode := .async .asyncEnv)
-
-/--
-Marks the given declaration as recursive.
--/
-def markAsRecursive (declName : Name) : CoreM Unit :=
-  modifyEnv (recExt.tag · declName)
-
-/--
-Returns `true` if `declName` was defined using well-founded recursion, or structural recursion.
--/
-def isRecursiveDefinition (declName : Name) : CoreM Bool :=
-  return recExt.isTagged (← getEnv) declName
-
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"

src/Lean/Meta/RecExt.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Lean.Attributes
+
+public section
+
+namespace Lean.Meta
+
+/--
+Environment extension for storing which declarations are recursive.
+This information is populated by the `PreDefinition` module, but the simplifier
+uses when unfolding declarations.
+-/
+builtin_initialize recExt : TagDeclarationExtension ←
+  mkTagDeclarationExtension `recExt (asyncMode := .async .asyncEnv)
+
+/--
+Marks the given declaration as recursive.
+-/
+def markAsRecursive (declName : Name) : CoreM Unit :=
+  modifyEnv (recExt.tag · declName)
+
+/--
+Returns `true` if `declName` was defined using well-founded recursion, or structural recursion.
+-/
+def isRecursiveDefinition (declName : Name) : CoreM Bool :=
+  return recExt.isTagged (← getEnv) declName

tests/lean/1363.lean

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

tests/lean/1363.lean.expected.out

@@ -1,5 +0,0 @@
-1363.lean:4:2-4:14: error: Cannot add `[macro_inline]` attribute to `f`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
-1363.lean:9:2-9:14: error: Cannot add `[macro_inline]` attribute to `g`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
-1363.lean:15:2-15:14: error: Cannot add `[macro_inline]` attribute to `h._unary`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
-1363.lean:15:2-15:14: error: Cannot add `[macro_inline]` attribute to `h`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
-1363.lean:21:2-21:14: error: Cannot add `[macro_inline]` attribute to `skipMany`: This attribute does not support this kind of declaration; only non-recursive definitions are supported

tests/lean/run/1363.lean

@@ -0,0 +1,51 @@
+import Std.Internal.Parsec
+open Std Internal Parsec String
+
+/--
+error: Cannot add `[macro_inline]` attribute to `f`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+-/
+#guard_msgs in
+@[macro_inline] -- Error
+def f : Nat → Nat
+  | 0 => 0
+  | n + 1 => f n
+
+/--
+error: Cannot add `[macro_inline]` attribute to `g`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+-/
+#guard_msgs in
+@[macro_inline] -- Error
+def g : Nat → Nat
+  | 0 => 0
+  | n + 1 => g n
+termination_by x => x
+
+/--
+error: Cannot add `[macro_inline]` attribute to `h`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+-/
+#guard_msgs in
+@[macro_inline] -- Error
+def h : Nat → Nat → Nat
+  | 0, _ => 0
+  | n + 1, m => h n m
+termination_by x y => x
+
+/--
+error: Cannot add `[macro_inline]` attribute to `i`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+-/
+#guard_msgs in
+@[macro_inline] -- Error
+def i : Nat → Nat
+  | 0 => 0
+  | n + 1 => i n
+partial_fixpoint
+
+/--
+error: Cannot add `[macro_inline]` attribute to `skipMany`: This attribute does not support this kind of declaration; only non-recursive definitions are supported
+-/
+#guard_msgs in
+@[macro_inline] -- Error
+partial def skipMany (p : Parser α) (it : Sigma String.Pos) : Parser PUnit := do
+  match p it with
+  | .success it _ => skipMany p it
+  | .error _ _  => pure ()