haskell - 为什么这种嵌套类型类派生有效？

Question

是的，这是一个不寻常的“为什么这样做”的问题。我有这段代码:

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

data F a = A (F a) | B (a (F a)) -- a :: * -> *
deriving instance (forall b. Eq b => Eq (a b)) => Eq (F a)

-- the following errors, asking me to add (Eq b) into the context
deriving instance (forall b. Eq (a b)) => Eq (F a)

如果定义第二个版本会出错

data T a = C | D a deriving Eq
x = B C == B C

从逻辑上讲，将(Eq b)添加到约束中应该类似于(forall b.Eq b && Eq (a b)) => Eq (F a)，因为我们需要把它放在forall的范围内。可以想象 (Eq b) 是隐式假设的，就像大多数派生实例所做的那样。但如果是这样，为什么第二个版本不起作用？

Answer 1

第一个推导等于以下实例

instance (forall b. Eq b => Eq (f b)) => Eq (F f) where
  (==) :: F f -> F f -> Bool
  A a1 == A b1 = (==) @(F f)     a1 b1
  B a1 == B b1 = (==) @(f (F f)) a1 b1
  _    == _    = False

假设等式在 f (forall b.Eq b => Eq (f b)) 下是封闭的，(==) 需要以下约束@(F f) 和 (==) @(f (F f))

1. Eq (F f)
2. Eq (f (F f))

第一个是我们正在编写/推导的相等实例:Eq (F f) 它在当前上下文中成立(Eq 在 下关闭f).因此该约束得到满足。

第二个要求我们提升类型的相等性:Eq (f (F f)) 遵循上下文:Eq 在 f 下被关闭.

如果我们用 F f 实例化 b，我们会看到我们提升的类型支持相等性 Eq (F f) => Eq (f (F f)) 如果我们定义的类型支持 equlity.. 它支持 (1.)。

---

第二个实例在 GHC Head 上编译。

deriving instance (forall b. Eq (f b)) => Eq (F f)

如果您知道 Eq (f b) 对任何 b 都成立，您就可以求解 1. 和 2。 通过使用 F f 实例化 b。