给定一些类型定义：
data A
data B (f :: * -> *)
data X (k :: *)
...和这个类型类：
class C k a | k -> a
...这些（为了最小的例子的目的而高度设计）函数定义类型检查：
f :: forall f. (forall k. (C k (B f)) => f k) -> A
f _ = undefined
g :: (forall k. (C k (B X)) => X k) -> A
g = f
但是，如果我们使用类型族而不是具有函数依赖性的类：
type family F (k :: *)
...然后等效的函数定义无法进行类型检查：
f :: forall f. (forall k. (F k ~ B f) => f k) -> A
f _ = undefined
g :: (forall k. (F k ~ B X) => X k) -> A
g = f
• Couldn't match type ‘f0’ with ‘X’
‘f0’ is untouchable
inside the constraints: F k ~ B f0
bound by a type expected by the context:
F k ~ B f0 => f0 k
Expected type: f0 k
Actual type: X k
• In the expression: f
In an equation for ‘g’: g = f
我阅读了the OutsideIn(X) paper的5.2节，它描述了可触摸和不可触摸的类型变量，我有点理解这里发生了什么。如果我向f添加一个额外的参数，推动f在内部forall之外的选择，那么程序类型检查：
f :: forall f a. f a -> (forall k. (F k ~ B f) => f k) -> A
f _ _ = undefined
g :: forall a. X a -> (forall k. (F k ~ B X) => X k) -> A
g = f
但是，在这个特定的例子中让我特别困惑的是为什么函数依赖具有不同的行为。我听过人们在不同时间声称像这样的功能依赖等同于类型族和等式，但这表明实际上并非如此。
在这种情况下，函数依赖提供了哪些信息，允许f以类型族不实例化的方式实例化？
我不知道我是否应该将此作为答案发布，因为它仍然非常浪漫，但我确实认为这是本质上正在发生的事情：
要评估(C k (B X)) => X k值，您必须为k选择具体类型，并指向满足约束的instance C k (B X)。要做到这一点，你必须说出类型类'a参数的形式为B f，编译器可以从中提取f类型（并且在这种情况下发现它是X） - 重要的是，它可以在实际查看之前执行此操作实例，这将是f变得不可触碰的点。
为了评估(F k ~ B X) => X k，它有点不同。在这里你不需要指向一个具体的实例，你只需要保证如果编译器查找F k的类型家族，那么这个类型将与B X相同。但在实际查找实例之前，编译器无法在此推断F k具有B f形式，因此也不会使用此来将f与外部量化参数统一起来，因为不可触及。
因此，GHC的行为至少不是完全不合理的。我仍然不确定它是否应该这样做。
好的，我有机会玩这个。有几个分心：
在Type Family版本中，只有f的定义给出了错误'f0' is untouchable。 （你可以使用AllowAmbiguousTypes来抑制它;这只是推迟了对g出现的错误。）让我们在这里忽略g。
然后没有AllowAmbiguousTypes，f的错误消息提供了更多信息：
• Couldn't match type ‘f0’ with ‘f’
‘f0’ is untouchable
inside the constraints: F k ~ B f0
bound by the type signature for:
f :: F k ~ B f0 => f0 k
‘f’ is a rigid type variable bound by
the type signature for:
f :: forall (f :: * -> *). (forall k. F k ~ B f => f k) -> A
Expected type: f0 k
Actual type: f k
啊哈！一个rigid type variable问题。我猜因为f是由k的等式约束修正的，因为它也是刚性的...
转向没有FunDep的g版本，在什么类型我们可以称为f？尝试
f (undefined undefined :: X a) -- OK
f (undefined "string" :: X String) -- rejected
f Nothing -- OK
f (Just 'c') -- rejected
拒绝消息（对于X String示例）是
• Couldn't match type ‘k’ with ‘String’
‘k’ is a rigid type variable bound by
a type expected by the context:
forall k. C k (B X) => X k
Expected type: X k
Actual type: X String
• In the first argument of ‘f’, namely
‘(undefined "string" :: X String)’
注意消息是关于k，而不是f，它是从FunDep确定的 - 或者如果我们能找到合适的k。
说明
功能f的签名称k是存在量化/更高排名。然后我们不能允许任何关于k的类型信息逃逸到周围的上下文中。我们不能为k提供任何（非底部）值，因为它的类型会侵入forall。
这是一个更简单的例子：
f2 :: forall f. (forall k. f k) -> A
f2 _ = undefined
f2 Nothing -- OK
f2 (Just 'c') -- rejected rigid type var
所以原来的FunDep版本编译是一个分心：它不能有人居住。 （根据我之前的怀疑，这是FunDeps的常见症状。）