GHCi类型推断失效与类型类方法的TypeApplications使用问题

先贴出你的代码方便参考：

{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main where
import GHC.Types (Type)
class F (f :: k -> Type) where
  type Plus f (a :: k) (b :: k) :: k
  zero :: f a
  plus :: f a -> f b -> f (Plus f a b)
data Empty (a :: Type) = Empty
instance F Empty where
  type Plus Empty a b = (a, b)
  zero = Empty
  plus _ _ = Empty

咱们得先搞清楚GHCi的:t命令和代码显式标注的本质区别：

• GHCi的:t只是输出它推断出的最一般类型，这个过程不需要解决类型歧义——它只是告诉你「这段表达式的类型可以是这个样子」，但不要求这段代码能实际编译通过。
• 而当你在代码里给表达式显式标注这个最一般类型时，GHC需要确保这个类型是可判定的，也就是它能明确找出所有类型变量的具体取值，不能有模糊地带。

这里的核心矛盾是Plus是一个非injective类型族——简单说就是不同的输入可能得到完全相同的输出。比如假设我们再定义一个实例：

data Foo (a :: Type) = Foo
instance F Foo where
  type Plus Foo a b = (a, b)  -- 和Empty的Plus输出完全一致
  zero = Foo
  plus _ _ = Foo

这时候f (Plus f a b)既可能是Empty (Int, String)，也可能是Foo (Int, String)，GHC没办法从(Int, String)反向推导出到底用的是Empty还是Foo，更别说a和b的具体类型了。

当你标注F f => f (Plus f a b)时，类型变量f、a、b都是歧义的——GHC没有足够信息确定它们的具体取值，自然会报错。而GHCi的:t只是把这个模糊的类型展示出来，不需要解决歧义，所以不会报错。

解决方案：要么标注具体的类型（比如Empty (Int, String)），要么用TypeApplications指定类型变量，消除歧义。

其实完全不用额外定义plus'和zero'，直接给原方法用TypeApplications就行，关键是要搞清楚类型变量的顺序，以及确保所有隐式变量都被正确绑定。

先看两个方法展开隐式类型变量后的完整签名：

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

TypeApplications的参数顺序是从左到右匹配类型变量，所以：

1. 对于zero，直接指定f和a就能得到明确类型的实例：

   zeroInt :: Empty Int
   zeroInt = zero @Empty @Int
   

2. 对于plus，需要先指定f，再依次指定第一个参数的a、第二个参数的b，同时给zero也指定匹配的类型参数：

   plusExample :: Empty (Int, String)
   plusExample = plus @Empty @Int @String (zero @Empty @Int) (zero @Empty @String)
   

你之前尝试plus @f @a @b zero zero报错，是因为zero本身的类型也是模糊的（F f => f a），GHC没办法把zero的类型变量和plus的类型变量自动绑定起来。只要给zero也指定对应的类型参数，或者利用上下文推断（比如给整个表达式指定返回类型），就能解决这个问题。

另外，如果上下文已经能确定类型，还可以省略部分TypeApplications：

-- 因为返回类型指定了Empty (Bool, Char)，GHC能自动推断出f=Empty，a=Bool，b=Char
plusExample2 :: Empty (Bool, Char)
plusExample2 = plus zero zero

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