为什么这个Haskell代码使用fundeps进行类型检查,但是对类型系列产生了不可触摸的错误？

Question

给定一些类型定义:

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

我阅读了OutsideIn(X)论文的第5.2节,它描述了可触摸和不可触摸的类型变量,我有点理解这里发生了什么.如果我添加一个额外的参数f是推动的选择f内之外forall,那么程序typechecks:

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以类型族不实例化的方式实例化？

Answer 1

我不知道我是否应该将此作为答案发布，因为它仍然非常手动，但我确实认为这就是本质上正在发生的事情：

要评估一个(C k (B X)) => X k值，您必须为 选择一个具体类型k，并指向instance C k (B X)满足约束的 。为此，您必须明确指出 typeclass'a参数的形式B f为 ，编译器可以从中提取类型f（并发X现在本例中是这样）——重要的是，它可以在实际查看实例之前执行此操作执行此操作，这将是变得不可触碰的时刻f。

要评估 a (F k ~ B X) => X k，则有点不同。这里你不需要指向一个具体的实例，你只需要保证如果编译器查找 的类型族F k，那么这个类型将与 相同B X。但在实际查找实例之前，编译器无法在这里推断其F k具有以下形式B f，因此也不会使用它来f与外部量化参数统一，因为不可触及。

因此，GHC的行为至少并非完全无理。我仍然不确定它是否应该这样做。