Prerequisites

• 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