outParam が予想外の挙動をする例

universe u v w

namespace Ex

/-- `outParam` なしで定義したダメな例 -/
class BadHMul (α : Type u) (β : Type v) (γ : Type w) where
  hMul : α → β → γ

instance : BadHMul Nat Nat Nat where
  hMul := Nat.mul

-- 返り値の型がわからないのでエラーになる
#check_failure BadHMul.hMul 1 2

-- 返り値の型を指定すればエラーにならない
#check (BadHMul.hMul 1 2 : Nat)

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hMul : α → β → γ

instance : HMul Nat Nat (List Nat) where
  hMul x y := []

#check (HMul.hMul 1 4 : List Nat)

instance : HMul Nat Nat Nat where
  hMul := Nat.mul

-- 返り値の型を自動で推論してくれて，エラーにならない
#eval HMul.hMul 4 3 -- 12

-- なぜか List Nat に変換する方だと解釈してくれない
-- outParam を付けたことで， Nat → Nat → Nat が優先される？？？
-- 怪奇現象
#check_failure (HMul.hMul 1 4 : List Nat) -- 4

instance : HMul Nat String Unit where
  hMul x y := ()

instance : HMul Nat String (List Nat) where
  hMul x y := []

-- これはいける
-- そして Unit が優先される(インスタンスの宣言順序は無関係)
#eval HMul.hMul 3 "hello"

instance : HMul Nat Nat Unit where
  hMul x y := ()

-- これは掛け算が勝つ
#guard HMul.hMul 2 3 = 6

end Ex

Start by running the supplied Lean example and reproducing each reported success or failure, especially the outParam cases. Trace how instance and result-type inference selects HMul instances, then document an explanation of the observed behavior and clarify what correction or example change is needed.