fix: structural recursion: do not check for brecOn too early (#4831)

Due to nested recursion, we do two passes of `getRecArgInfo`: One on
each argument in isolation, to see which inductive types are around
(e.g. `Tree` and `List`), and
then we later refine/replace this result with the data for the nested
type former (the implicit `ListTree`).

If we have nested recursion through a non-recursive data type like
`Array` or `Prod` then arguemnts of these types should survive the first
phase, so that we can still use them when looking for, say, `Array
Tree`.

This was helpfully reported by @arthur-adjedj.

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

@@ -68,9 +68,7 @@ def getRecArgInfo (fnName : Name) (numFixed : Nat) (xs : Array Expr) (i : Nat) :
       throwError "it is a let-binding"
     let xType ← whnfD localDecl.type
     matchConstInduct xType.getAppFn (fun _ => throwError "its type is not an inductive") fun indInfo us => do
-    if !(← hasConst (mkBRecOnName indInfo.name)) then
-      throwError "its type {indInfo.name} does not have a recursor"
-    else if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
+    if indInfo.isReflexive && !(← hasConst (mkBInductionOnName indInfo.name)) && !(← isInductivePredicate indInfo.name) then
       throwError "its type {indInfo.name} is a reflexive inductive, but {mkBInductionOnName indInfo.name} does not exist and it is not an inductive predicate"
     else
       let indArgs    : Array Expr := xType.getAppArgs
@@ -263,6 +261,11 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
     if let some combs := allCombinations recArgInfoss' then
       for comb in combs do
         try
+          -- Check that the group actually has a brecOn (we used to check this in getRecArgInfo,
+          -- but in the first phase we do not want to rule-out non-recursive types like `Array`, which
+          -- are ok in a nested group. This logic can maybe simplified)
+          unless (← hasConst (group.brecOnName false 0)) do
+            throwError "the type {group} does not have a `.brecOn` recursor"
           -- TODO: Here we used to save and restore the state. But should the `try`-`catch`
           -- not suffice?
           let r ← k comb

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

@@ -36,6 +36,16 @@ def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
 def IndGroupInfo.numMotives (group : IndGroupInfo) : Nat :=
   group.all.size + group.numNested
 
+/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
+including universe parameters and fixed prefix.  -/
+partial def IndGroupInfo.brecOnName (info : IndGroupInfo) (ind : Bool) (idx : Nat) : Name :=
+  if let .some n := info.all[idx]? then
+      if ind then mkBInductionOnName n
+      else        mkBRecOnName n
+    else
+      let j := idx - info.all.size + 1
+      info.brecOnName ind 0 |>.appendIndexAfter j
+
 /--
 An instance of an mutually inductive group of inductives, identified by the `all` array
 and the level and expressions parameters.
@@ -65,15 +75,9 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do
 /-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
 including universe parameters and fixed prefix.  -/
 def IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr :=
-  let e := if let .some n := group.all[idx]? then
-      if ind then .const (mkBInductionOnName n) group.levels
-      else        .const (mkBRecOnName n)      (lvl :: group.levels)
-    else
-      let n := group.all[0]!
-      let j := idx - group.all.size + 1
-      if ind then .const (mkBInductionOnName n |>.appendIndexAfter j) group.levels
-      else        .const (mkBRecOnName n |>.appendIndexAfter j)       (lvl :: group.levels)
-  mkAppN e group.params
+  let n := group.brecOnName ind idx
+  let us := if ind then group.levels else lvl :: group.levels
+  mkAppN (.const n us) group.params
 
 /--
 Figures out the nested type formers of an inductive group, with parameters instantiated

tests/lean/guessLexFailures.lean.expected.out

@@ -72,11 +72,10 @@ Not considering parameter fixed of Mutual.f:
   it is unchanged in the recursive calls
 Not considering parameter fixed of Mutual.g:
   it is unchanged in the recursive calls
-Not considering parameter H of Mutual.g:
-  its type True does not have a recursor
 Not considering parameter fixed of Mutual.h:
   it is unchanged in the recursive calls
 Too many possible combinations of parameters of type Nat (or please indicate the recursive argument explicitly using `termination_by structural`).
+Skipping arguments of type True, as Mutual.f has no compatible argument.
 
 
 Could not find a decreasing measure.

tests/lean/run/structuralMutual.lean

@@ -575,6 +575,53 @@ end
 
 end ManyCombinations
 
+namespace WithTuple
+
+inductive Tree (α : Type) where
+  | node : α → (Tree α × Tree α) → Tree α
+
+mutual
+
+def Tree.map (f : α → β) (x : Tree α): Tree β :=
+  match x with
+    | node x arrs => node (f x) $ Tree.map_tup f arrs
+termination_by structural x
+
+def Tree.map_tup (f : α → β) (x : Tree α × Tree α): (Tree β × Tree β) :=
+  match x with
+    | (t₁,t₂) => (Tree.map f t₁, Tree.map f t₂)
+termination_by structural x
+
+end
+
+end WithTuple
+
+namespace WithArray
+
+inductive Tree (α : Type) where
+  | node : α → Array (Tree α) → Tree α
+
+mutual
+
+def Tree.map (f : α → β) (x : Tree α): Tree β :=
+  match x with
+    | node x arr₁ => node (f x) $ Tree.map_arr f arr₁
+termination_by structural x
+
+def Tree.map_arr (f : α → β) (x : Array (Tree α)): Array (Tree β) :=
+  match x with
+    | .mk arr₁ => .mk (Tree.map_list f arr₁)
+termination_by structural x
+
+def Tree.map_list (f : α → β) (x : List (Tree α)): List (Tree β) :=
+  match x with
+    | [] => []
+    | h₁::t₁ => (Tree.map f h₁)::Tree.map_list f t₁
+termination_by structural x
+end
+
+end WithArray
+
 namespace FunIndTests
 
 -- FunInd does not handle mutual structural recursion yet, so make sure we error
@@ -632,6 +679,28 @@ info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1
   (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a
 -/
 #guard_msgs in
-#check EvenOdd.isEven.induct -- TODO: This error message can be improved
+#check EvenOdd.isEven.induct
+
+/--
+info: WithTuple.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithTuple.Tree α → Prop)
+  (motive_2 : WithTuple.Tree α × WithTuple.Tree α → Prop)
+  (case1 :
+    ∀ (x : α) (arrs : WithTuple.Tree α × WithTuple.Tree α), motive_2 arrs → motive_1 (WithTuple.Tree.node x arrs))
+  (case2 : ∀ (t₁ t₂ : WithTuple.Tree α), motive_1 t₁ → motive_1 t₂ → motive_2 (t₁, t₂)) (x : WithTuple.Tree α) :
+  motive_1 x
+-/
+#guard_msgs in
+#check WithTuple.Tree.map.induct
+
+/--
+info: WithArray.Tree.map.induct {α β : Type} (f : α → β) (motive_1 : WithArray.Tree α → Prop)
+  (motive_2 : Array (WithArray.Tree α) → Prop) (motive_3 : List (WithArray.Tree α) → Prop)
+  (case1 : ∀ (x : α) (arr₁ : Array (WithArray.Tree α)), motive_2 arr₁ → motive_1 (WithArray.Tree.node x arr₁))
+  (case2 : ∀ (arr₁ : List (WithArray.Tree α)), motive_3 arr₁ → motive_2 { data := arr₁ }) (case3 : motive_3 [])
+  (case4 : ∀ (h₁ : WithArray.Tree α) (t₁ : List (WithArray.Tree α)), motive_1 h₁ → motive_3 t₁ → motive_3 (h₁ :: t₁))
+  (x : WithArray.Tree α) : motive_1 x
+-/
+#guard_msgs in
+#check WithArray.Tree.map.induct
 
 end FunIndTests

tests/lean/run/terminationByStructurally.lean

@@ -83,5 +83,32 @@ def foo4 (n : Nat) : Nat → Nat := match n with
   | n+1 => foo4 n
 termination_by structural id n + 1
 
+/--
+error: failed to infer structural recursion:
+Cannot use parameter #2:
+  the type Nat × Nat does not have a `.brecOn` recursor
+-/
+#guard_msgs in
+def foo5 : Nat → (Nat × Nat) → Nat
+ | 0, _ => 0
+ | n+1, t => foo5 n t
+termination_by structural n t => t
+
+/--
+error: failed to infer structural recursion:
+Cannot use parameters #2 of Errors.foo6 and #2 of Errors.bar6:
+  the type Nat × Nat does not have a `.brecOn` recursor
+-/
+#guard_msgs in
+mutual
+def foo6 : Nat → (Nat × Nat) → Nat
+ | 0, _ => 0
+ | n+1, t => bar6 n t
+termination_by structural n t => t
+def bar6 : Nat → (Nat × Nat) → Nat
+ | 0, _ => 0
+ | n+1, t => foo6 n t
+termination_by structural n t => t
+end
 
 end Errors