型クラスのダイアモンド継承があるときに、型クラス解決がうまくいかない

Left と Right のインスタンスがあれば Both のインスタンスも当然あってほしいが、それが上手くいかない

これは Base を両方が継承していることによる問題。回避方法はベストプラクティスとしてあったはずだが…

set_option autoImplicit false
set_option relaxedAutoImplicit false

class Base (α : Type) where
  base : α

class Left (α : Type) extends Base α where
  left : α

class Right (α : Type) extends Base α where
  right : α

class Both (α : Type) extends Left α, Right α

inductive Direction where
  | south
  | north
  | west
  | east

instance : Base Direction where
  base := Direction.south

instance : Left Direction where
  left := Direction.west

instance : Right Direction where
  right := Direction.east

/--
error: failed to synthesize
  Both Direction
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#check (inferInstance : Both Direction)

Start with the minimal Lean example in the issue and reproduce the failed inferInstance synthesis. Investigate the type-class diamond inheritance behavior and the referenced best-practice workaround. Done means the expected Both Direction resolution works, or the repository documents a verified workaround if the behavior is intentional.