structural recursion: inductive parameters after varying function parameters?

[nomeata]

The following function is structurally recursive over a data type with an index, and the index depends on function parameters that come after the “fixed prefix”.

This makes lean stumble. This wasn’t easily visible before, because it would then try well-founded recursion, but with termination_by structural we can force the error to show up:

set_option linter.constructorNameAsVariable false

inductive  A (n : Nat) : Type
  | a : A n
  | b : A n → A n

/--
error: structural recursion failed, produced type incorrect term
  application type mismatch
    size.match_1 n (fun x => A.below (motive := fun x => Nat → Nat → Nat) x → Nat) x✝
  argument has type
    A n✝
  but function has type
    (x : A n) →
      (Unit → (fun x => A.below (motive := fun x => Nat → Nat → Nat) x → Nat) A.a) →
        ((a' : A n) → (fun x => A.below (motive := fun x => Nat → Nat → Nat) x → Nat) a'.b) →
          (fun x => A.below (motive := fun x => Nat → Nat → Nat) x → Nat) x
-/
#guard_msgs in
def A.size (acc n : Nat) : A n → Nat
  | .a => acc
  | .b a' => 1 + A.size (acc + 1) n a'
termination_by structural a => a

My first guess was that this is a bug in hasBadParamDeps?, confusing the value of the inductive parameter with its type (not unlikely, as the nearby hasBadIndexDep? certainly has to consider the index’s type’s dependencies), and within #4575 I tried this fix:

diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 9770fc54f1..0e1c87fce9 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -29,9 +29,8 @@ private def hasBadIndexDep? (ys : Array Expr) (indices : Array Expr) : MetaM (Op
 -- Inductive datatype parameters cannot depend on ys
 private def hasBadParamDep? (ys : Array Expr) (indParams : Array Expr) : MetaM (Option (Expr × Expr)) := do
   for p in indParams do
-    let pType ← inferType p
     for y in ys do
-      if ← dependsOn pType y.fvarId! then
+      if ← dependsOn p y.fvarId! then
         return some (p, y)
   return none

This passed our test suite and mathlib, but caused a regression to @tobiasgrosser, as reported in another comment, where the old behavior seems to have worked.

There is a fix/workaround: Reorder the function parameters appropriately so that the inductive’s parameters depend only on a fixed prefix of the function’s parameters. But I am unsure:

• Is the old check wrong, or is the old check correct but there is a bug later in the processing?
• Is my fix correct (and Tobias was just lucky before that it worked for him, but really should reorder the function parameters) or too restrictive?

[nomeata]

I pushed my proposed fix to #4672, which should soon get a mathlib branch, in case someone wants to play around with this.

[nomeata]

Maybe the most liberal approach would be to allow any argument order that we can possibly make sense of:

• Find the recursive parameter and its indices
• Try to reorder (while keeping dependencies in mind) to bring all unchanging parameters to the front, then the indices and recursive parameter, then all other argument

I don’t quite know if this is flexibility is really needed and worth the implementation and documentation complexity, or if we want our users to order the parameters more logically.

[tobiasgrosser]

We are potentially pushing limits in lean unnecessarily. Better documentation or just an error message that we can search for to get to documentation might be all that is needed.

[alexkeizer]

I don't think that flexibility is really needed: if someone really want to have their variables in a particular order they can always define a simple wrapper around the recursive definition with the correct order.
Like Tobias says, though, throwing a meaningful error when the order is wrong, would be nice

[nomeata]

Thanks for your feedback!

The error message in #4672 is

/--
error: argument #3 cannot be used for structural recursion
  its type is an inductive datatype
    A n
  and parameter
    n
  depends on
    n
-/

and maybe it’s actually useable once it also says what makes it bad to depend on n, namely that the parameter of the inductive must only mention function parameters that come before the first function parameter that changes in recursive calls and before the first parameter that’s an index of the parameter that the function is recursing on.

Suggestions for elegant concise precise formulations are welcome!