Structural recursion produces application type mismatch

[fpfu]

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 TyBox
| mk (ty: Type) : TyBox

inductive Foo: Type → Type
def Foo.ty_box (_: Foo α): TyBox := .mk α

mutual
  inductive Bar : Type → Type 1
  | mk (foo: Foo α) (box: BarBox foo.ty_box) : Bar α

  inductive BarBox : TyBox → Type 1
  | mk (bar: Bar α): BarBox (.mk α)
end

def toFoo : Bar α → Foo α
| ⟨_, .mk f ⟩ => toFoo f

Expected behavior: example works

Actual behavior: get an error message:

fail to show termination for
  toFoo
with errors
argument #2 was not used for structural recursion
  application type mismatch
    @Bar.brecOn (fun {α} x => Foo α) α
  argument
    α
  has type
    Type : Type 1
  but is expected to have type
    (a : TyBox) → BarBox a → Type : Type 1

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-03-01

[Kha]

Works in 4.16.0