CoeDep

CoeDep は型強制を行うための型クラスですが、Coe と異なり「項に依存する型強制」(dependent coercion)を行うことができます。

たとえば空でないリストからなる型 NonEmptyList を定義したとします。空リストを変換する方法がないため、List α → NonEmptyList α という変換を定義する自然な方法はありません。しかし CoeDep を使えば空でないリストに限って NonEmptyList に変換するという型強制を定義することができます。

/-- 空でないリスト -/
structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

-- 型強制がないのでエラー
#check_failure ([1, 2] : NonEmptyList Nat)

variable {α : Type}

/-- 型強制。`x :: xs` という形をしている `List` の要素だけを `NonEmptyList` の項に変換する -/
instance {x : α} {xs : List α} : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := {head := x, tail := xs}

-- 型強制が定義された
#check ([1, 2] : NonEmptyList Nat)