为什么这个嵌套的类型类派生工作?

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))。(1.)。

---

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

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

如果知道Eq (f b)适用于任何b，则可以求解1。和通过用F f实例化b。

Answer 2

经过一段时间的尝试，我想我确定了这个问题。很抱歉频繁编辑问题!我过度简化了代码，没有仔细测试。

data T a = C | D a派生了一个Eq实例，该实例需要Eq a。没有这个，forall b. Eq (T b)前提就不能满足。对于forall b. (Eq b) => Eq (T b)，我们可以使用Eq b来获得a上所需的相等谓词。