Induction generalizes given instance arguments

Stream: lean4

[pandaman]

I'm defining a custom induction principle that takes a class instance as a parameter. When I used the induction principle with the induction tactic, it seems to generalize the instance parameter even when the instance is given (explicitly or via the instance search). Is the behavior expected? I'd like it to use the given instance.

MWE:

open String (Pos)

class PositionRecorder (s : String) (α : Type) where

instance instPos {s : String} : PositionRecorder s (Pos s) where

theorem inductionOn {s : String} (α : Type) (inst : PositionRecorder s α)
  (motive : Pos s → Prop)
  (not_found : motive s.endPos)
  (pos : Pos s) :
  motive pos := sorry

theorem test {s : String} {pos : Pos s}:
  True := by
  induction pos using inductionOn (Pos s) inferInstance with
  | not_found => sorry
  -- BUG: induction tactic introduces `x_1` for `PositionRecorder s (Pos s)` even though it's provided explicitly.
  -- Without this branch, the tactic fails with "Alternative `x_1` has not been provided"
  | x_1 => sorry

theorem inductionOnInst {s : String} (α : Type) [inst : PositionRecorder s α]
  (motive : Pos s → Prop)
  (not_found : motive s.endPos)
  (pos : Pos s) :
  motive pos := sorry

theorem test' {s : String} {pos : Pos s}:
  True := by
  induction pos using inductionOnInst (Pos s) with
  | not_found => sorry
  -- BUG: induction tactic introduces `x_1` for `PositionRecorder s (Pos s)` even though it's provided via the instance search.
  -- Without this branch, the tactic fails with "Alternative `x_1` has not been provided"
  | x_1 => sorry

[Aaron Liu]

the x_1 branch seems to be going into the implicit argument of inferInstance

[pandaman]

Interesting. Passing instPos explicitly to inductionOn seems to work. Do you have any ideas for the inductionOnInst version? It's closer to the one I want to use.