#synth

型クラス C と型 T があるとき、#synth C T は T が C のインスタンスになっているかチェックします。もしインスタンスでなかった場合にはエラーになります。

型クラスとは

型クラスとは、複数の型に対して共通の機能や実装を提供するものです。具体例を見てみましょう。たとえば逆数は、複数の型に対して定義されています。

-- `⁻¹` で逆数を表すことができる
#check (1 : ℚ)⁻¹

-- 実数として見ても同じ
#check (1 : ℝ)⁻¹

逆数をとる関数 fun x => x⁻¹ の定義域はどうなっているのでしょうか？定義域を一般の型 α に拡張してみて、どうなるか見てみましょう。

variable (α : Type)

/--
error: failed to synthesize
  Inv α
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in #check (_ : α)⁻¹

一般の型に対して逆数は定義できないので、エラーになってしまいました。エラーメッセージで α は Inv のインスタンスではないと言われています。この Inv が型クラスです。Inv のインスタンスであるような型 T に対しては、逆数関数 (·)⁻¹ : T → T が定義できるというわけです。

インスタンスとは

例えば実数 ℝ に対して逆数は定義できるだろうと予想されますが、実際 ℝ は Inv のインスタンスであることが確認できます。

/-- info: Real.instInv -/
#guard_msgs in #synth Inv Real

自然数 ℕ に対しては逆数が定義されていないと予想されますが、実際 Inv のインスタンスになっていません。

-- エラーになってしまう
/--
error: failed to synthesize
  Inv ℕ
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in #synth Inv Nat

-- Inv のインスタンスになっていない
#check_failure (inferInstance : Inv Nat)

自分で無理やり ℕ を Inv のインスタンスにしてみると、通るようになります。ここでは逆数関数を常に 1 になる定数関数としてみましょう。

instance : Inv Nat := ⟨fun _ => 1⟩

#synth Inv Nat

example : (1 : ℕ)⁻¹ = 1 := by rfl