如何将TypeApplications用于类型类方法？GHCi推断类型为何不可用？

让我们逐个解决这两个GHC类型系统相关的问题：

问题1：GHCi能推断plus zero zero的类型，但手动标注却报错的原因 #

这个报错的核心是**非 injective 类型家族（non-injective type family）**导致的类型歧义。

当你在GHCi中用:t plus zero zero时，GHCi会给出一个宽松的多态类型F f => f (Plus f a b)——它只是指出存在某些a和b满足这个类型，但不需要明确a和b的具体值。

但当你手动给代码加上这个类型标注时，GHC需要完全确定所有类型变量。问题在于Plus是一个类型家族，且你没有将其声明为injective的（即不同的a、b组合可能生成相同的Plus f a b结果）。GHC无法从Plus f a b反向推导出a和b的具体类型，因此判定a和b是歧义变量，从而抛出错误。

解决方法 #

你可以通过显式指定类型变量来消除歧义，结合ScopedTypeVariables和TypeApplications即可实现：

plusZero :: forall f a b. F f => f (Plus f a b)
plusZero = plus @f @a @b zero zero

这样GHC就能明确a和b是你绑定的类型变量，无需再尝试反向推导。

如果你不需要关心a和b的具体类型，也可以用通配符让GHC接受歧义（不过显式标注始终是更推荐的做法）：

plusZero :: F f => f (Plus f _ _)
plusZero = plus zero zero

问题2：直接用TypeApplications调用plus/zero，无需辅助函数 #

报错的根源是你漏掉了kind参数的指定。你的类型类F是多态kind的（f :: k -> Type），所以plus和zero的类型参数列表里，第一个参数其实是kindk，之后才是f、a、b这些类型参数。

当你直接写plus @f @a @b时，GHC会把@f当成第一个类型参数，但f的kind是k -> Type，并非一个具体的类型（GHC期望第一个参数是对应kindk的类型），因此会抛出“Expecting one more argument to ‘f’”的错误。

解决方法 #

你需要严格按照类型参数的顺序，先指定kind参数，再指定其他类型参数：

1. 针对具体的kind（比如Type）调用：

-- 调用Empty实例，指定a为Int、b为String
plusZero2 = plus @Type @Empty @Int @String zero zero

2. 保持多态性，用ScopedTypeVariables绑定所有参数（包括kindk）：

plusZero2 :: forall k (f :: k -> Type) a b. F f => f (Plus f a b)
plusZero2 = plus @k @f @a @b zero zero

对于zero的调用逻辑完全一致，比如获取Empty Int类型的zero：

emptyZero = zero @Type @Empty @Int

内容的提问来源于stack exchange，提问作者statusfailed