种类签名和类型族

是的,有一个微妙的区别。

type family F a :: *->* 比如说, F Int 类构造函数类型 [] , Maybe

type family F a :: * -> *

-- these three examples can be removed / changed, if wished
type instance F Int = []
type instance F Char = Maybe
type instance F Bool = (,) String

foo :: (F Int a :~: F Int b) -> (a :~: b)
foo Refl = Refl

为了进行上述类型检查,编译器利用了以下事实: F Int a ~ F Int b 暗示 a ~ b

type family F a b :: * F整数

type family F a b :: *
type instance F Int a = ()