`trans` does not work on implicit arguments

[staroperator]

import Batteries.Tactic.Trans

inductive A (α : Type) where
| mk : α → A α

inductive r {α} : A α → A α → Prop where
| trans {a b c} : r a b → r b c → r a c

attribute [trans] r.trans

set_option trace.Tactic.trans true

example {α} {a b c : A α} : r a c := by
  trans b

gives

α : Type
a b c : A α
⊢ r a c

[Tactic.trans] goal decomposed 
[Tactic.trans] rel: 
      @r 
[Tactic.trans] x: 
      a 
[Tactic.trans] z: 
      c 
[Tactic.trans] trying homogeneous case 
[Tactic.trans] trying lemma Trans.simple 

It looks like rel here should be @r α instead of @r. If the index is explicit, trans succeed:

inductive r' (α) : A α → A α → Prop where
| trans {a b c} : r' α a b → r' α b c → r' α a c

attribute [trans] r'.trans

example {α} {a b c : A α} : r' α a c := by
  trans b -- succeed

[fgdorais]

Quick update: #1223 fixes this issue but it introduces a regression somewhere else. If anyone knows how to help, please do!