Structural recursion: wrong motive generated

[arthur-adjedj]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Structural recursion may fail due to a badly formed motive in a brecOn call

Context

I encountered this issue when trying to formalise a theory of signatures for inductive types.

Steps to Reproduce

MWE:

inductive Tyₛ (l : List Unit): Type
| U : Tyₛ l
open Tyₛ

inductive Varₚ (d : Unit): List Unit → Type
| vz : Varₚ d [d']
| vs : Varₚ d l → Varₚ d (Bₛ :: l)

inductive Tmₛ {l : List Unit}: Tyₛ l → Unit → Type 1
| arr   : (T : Type) → Tmₛ A d → Tmₛ A d
| param : Varₚ d l → Tmₛ A d → Tmₛ (@U l) d

def TmₛA {l : List Unit} {d : Unit} {Aₛ : Tyₛ l} (t : Tmₛ Aₛ d): Type := 
match t with
  | .arr dom cd => 
    let cd := TmₛA cd
    dom → cd
  | _ => sorry
termination_by structural t

Expected behavior: The function gets accepted.

Actual behavior: The following error pops up:

failed to infer structural recursion:
Cannot use parameter t:
  application type mismatch
    @Tmₛ.brecOn l fun {d} {Aₛ} t => Type
  argument
    fun {d} {Aₛ} t => Type
  has type
    {d : Unit} → {Aₛ : Tyₛ l} → Tmₛ Aₛ d → Type 1 : Type 2
  but is expected to have type
    (a : Tyₛ l) → (a_1 : Unit) → Tmₛ a a_1 → Type 1 : Type 2

Versions

Lean 4.15.0-nightly-2024-11-08 Target: x86_64-unknown-linux-gnu

Additional Information

The issue seems to be that the motive generated for the recursive call puts arguments in the wrong order. Changing the order of arguments in the signature of Tmₛ fixes things:

def TmₛA {l : List Unit} {Aₛ : Tyₛ l} {d : Unit} (t : Tmₛ Aₛ d): Type := 
match t with
  | .arr dom cd => 
    let cd := TmₛA cd
    dom → cd
  | _ => sorry
termination_by structural t 
-- works

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Ok, in general there is code there for this kind of reshuffling of arguments, but it seems to be not tested enough. Maybe the tests only had one level of indices or so. I can have a look next week.

[nomeata]

Mostly a straight-forward fix, it seems: #6116