关联类型族报错‘T是类型函数，可能非单射’问题咨询

嘿，这个报错我太熟悉了！核心问题出在关联类型族不自带单射性保证——简单说就是，不同的a类型可能对应完全一样的T a类型。编译器看到pred :: T a -> Bool这个签名时，根本没办法从T a反推出唯一的a，自然就会喊“类型变量歧义”啦。

举个直观的例子，要是咱们给C写两个实例：

instance C Int where
  type T Int = String
  pred = null -- 检查字符串是否为空

instance C Bool where
  type T Bool = String
  pred = (== "True") -- 检查字符串是不是"True"

这时候你写pred ""，编译器懵了：到底该用Int的实例还是Bool的？俩实例的T a都是String，它完全没法判断。

方案1：启用AllowAmbiguousTypes延迟检查 #

错误提示里其实已经给了一个方向——启用AllowAmbiguousTypes扩展，把歧义检查推迟到你实际调用方法的时候，之后再通过类型注解或者类型应用明确指定要用到的a类型。

先修改代码开头：

{-# LANGUAGE TypeFamilies, AllowAmbiguousTypes #-}
module Study where
class C a where
  type T a :: *
  pred :: T a -> Bool

调用的时候有两种方式：

-- 方式一：给参数加类型注解
checkEmpty :: Bool
checkEmpty = pred ("" :: T Int)

-- 方式二：用TypeApplications（得额外开这个扩展）
{-# LANGUAGE TypeApplications #-}
checkIsTrue :: Bool
checkIsTrue = pred @Bool "True"

方案2：给关联类型族加上单射性约束 #

如果你能保证每个T a都对应唯一的a（不会出现上面例子里两个不同a对应同一个T a的情况），那可以用TypeFamilyDependencies扩展来声明这个单射关系：

{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
module Study where
class C a where
  type T a = r | r -> a -- 这里的`r -> a`表示：知道r就能唯一确定a
  pred :: T a -> Bool

这样编译器就明白，只要看到T a的类型，就能反推出对应的a，自然不会再报歧义错误了。不过要注意，之后所有的C实例都必须遵守这个单射规则，不然编译会失败哦。

再唠两句为啥会报错 #

Haskell的类型检查器默认要求所有类型变量都能被唯一确定。关联类型族本身没承诺“一个T a只对应一个a”，所以当方法签名里只出现T a、没直接出现a的时候，编译器找不到确定a的依据，就会抛出这个错误啦。

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