induction complains about wrong binders in motive

Stream: lean4

[Edward van de Meent]

i was trying my hand at writing tests for a fix for lean4#4246 i'm working on when i came across the following:

class Foo (α : Type) where
  x : Nat

instance : Foo Nat where
  x := 0

structure Bar (α : Type) [Foo α] : Type where
  hy : Foo.x α = 2

@[elab_as_elim]
def Bar.induction (P : ∀ (α : Type) [Foo α] (b: Bar α), Prop)
  (α : Type) [ohno : Foo α] (x : Bar α) (nat : ∀ (x : Bar Nat), P Nat x) : P α x := sorry

example (α : Type) {noninst : Foo α} [inst : Foo α] (x:@Bar α noninst): Inhabited (@Bar α inst) := by
  induction α, x using Bar.induction with -- error here
  | nat x => sorry

/-
error: type mismatch when assigning motive
  fun α {noninst} x => Inhabited (Bar α)
has type
  (α : Type) → {noninst : Foo α} → Bar α → Type : Type 1
but is expected to have type
  (α : Type) → [inst : Foo α] → Bar α → Prop : Type 1
-/

I've looked into it, and it looks like induction uses the binderinfo of the arguments as they occur in the context to construct the motive, which causes this type error...

[Edward van de Meent]

this seems like a decently simple fix at Lean.Elab.Tactic.ElimApp.setMotiveArg nvm i misread the error