fix: mutual structural recursion: check that datatype parameters agree

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

@@ -109,7 +109,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (recArgPoss : Ar
     let maxNumFixed ← getMutualFixedPrefix preDefs
 
     -- We do two passes to get the RecArgInfo values.
-    -- From the first pass, we only keep the  mininum of the `numFixed` reported.
+    -- From the first pass, we only keep the mininum of the `numFixed` reported.
     let numFixed ← lambdaBoundedTelescope preDefs[0]!.value maxNumFixed fun xs _ => do
       assert! xs.size = maxNumFixed
       let values ← preDefs.mapM (instantiateLambda ·.value xs)
@@ -120,6 +120,18 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (recArgPoss : Ar
         lambdaTelescope value fun ys _value => do
           getRecArgInfo preDef.declName maxNumFixed (xs ++ ys) recArgPos
 
+      -- Check that the inductive parameters agree. This also ensures that they only depend on the
+      -- trimmed prefix (minimum of all `.numFixed`).
+      for recArgInfo in recArgInfos[1:] do
+        let ok ← Array.allM
+          (fun (e₁, e₂) => isDefEqGuarded e₁ e₂)
+          (Array.zip recArgInfo.indParams recArgInfos[0]!.indParams)
+        unless recArgInfos[0]!.indParams.size = recArgInfo.indParams.size && ok do
+          throwError m!"The inductive type of the recursive parameter of {recArgInfos[0]!.fnName} " ++
+            m!"and {recArgInfo.fnName} have different parameters:" ++
+            indentD m!"{recArgInfos[0]!.indParams}" ++
+            indentD m!"{recArgInfo.indParams}"
+
       return (recArgInfos.map (·.numFixed)).foldl Nat.min maxNumFixed
 
     if numFixed < maxNumFixed then

tests/lean/run/structuralMutual.lean

@@ -489,6 +489,60 @@ termination_by structural t => t
 
 end FixedIndex
 
+namespace IndexIsParameter
+
+-- Not actual mutual, but since I was at it
+
+inductive T (n : Nat) : Nat → Type where
+  | z : T n n
+  | n : T n n → T n n
+
+/--
+error: its type is an inductive datatype
+  T n n
+and the datatype parameter
+  n
+depends on the function parameter
+  n
+which does not come before the varying parameters and before the indices of the recursion parameter.
+-/
+#guard_msgs in
+def T.a (n : Nat) : T n n → Nat
+  | .z => 0
+  | .n t => t.a + 1
+termination_by structural t => t
+
+
+end IndexIsParameter
+
+
+namespace DifferentParameters
+
+-- An attempt to make it fall over mutual recursion over the same type
+-- but with different parameters.
+
+inductive T (n : Nat) : Type where
+  | z : T n
+  | n : T n → T n
+
+/--
+error: The inductive type of the recursive parameter of DifferentParameters.T.a and DifferentParameters.T.b have different parameters:
+  [23]
+  [42]
+-/
+#guard_msgs in
+mutual
+def T.a : T 23 → Nat
+  | .z => 0
+  | .n t => t.a + 1 + T.b .z
+termination_by structural t => t
+def T.b : T 42 → Nat
+  | .z => 0
+  | .n t => t.b + 1 + T.a .z
+termination_by structural t => t
+end
+
+end DifferentParameters
 
 namespace FunIndTests