`structural recursion cannot be used` when index depends on non index

[fpfu]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Steps to Reproduce

inductive Foo {f: Nat}: {d: Nat} → (h: d ≤ f) → Type where
| foo : Foo (Nat.zero_le _) → (Bool → Foo h) → Foo h

def Foo.bar (h: d ≤ f): Foo h → Foo h
| foo _ f => (f true).bar h

-- workaround is to use induction and provide code manually

unsafe -- or partial
def Foo.bar_impl (h: d ≤ f): Foo h → Foo h
| foo _ f => (f true).bar_impl h

@[implemented_by bar_impl]
def Foo.bar' (h: d ≤ f) (x: Foo h): Foo h := by 
  induction x
  case foo ih => exact ih true

Expected behavior: Foo.bar works. I guess it's a low priority unimplemented feature, hopes the workaround will be useful for everyone who will encounter the same error.

Actual behavior: get error message:

fail to show termination for

with errors
argument #4 was not used because its type is an inductive family

and index

depends on the non index

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

Reproduces how often: 100%

Versions

nightly-2023-02-03

[fpfu]

Have found another failing example, when structural recursion doesn't work without explicit mention of implicit argument:

inductive Foo {f: Nat}: (h₁: d₁ ≤ f) → (h₂: d₂ ≤ f) → Type where
|  foo {h₁: d₁ ≤ f} : (Bool → Foo h₁ h₂) → Foo h₁ h₂

-- can't justify structural recursion without `h` explicitly mentioned
def Foo.fails             : (h₂: d₂ ≤ f) → Foo h h₁ → Foo h h₂ | _, foo f => foo (λ b => (f b).fails ‹_›)
def Foo.works {h: d₁ ≤ f} : (h₂: d₂ ≤ f) → Foo h h₁ → Foo h h₂ | _, foo f => foo (λ b => (f b).works ‹_›)

message:

fail to show termination for
  Foo.fails
with errors
argument #7 was not used for structural recursion
  application type mismatch
    @Nat.le.brecOn d₂ fun {f} x => {a : Nat} → {h : a ≤ f} → {a_1 : Nat} → {h₁ : a_1 ≤ f} → Foo h h₁ → Foo h x
  argument
    fun {f} x => {a : Nat} → {h : a ≤ f} → {a_1 : Nat} → {h₁ : a_1 ≤ f} → Foo h h₁ → Foo h x
  has type
    {f : Nat} → d₂ ≤ f → Type : Type 1
  but is expected to have type
    (a : Nat) → Nat.le d₂ a → Prop : Type

argument #8 was not used because its type is an inductive family
  Foo h h₁
and index
  h₁
depends on the non index
  a✝

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation