导出具有量化约束的 Ord (forall a. Ord a => Ord (f a))

Question

有了量化约束，我可以得出 Eq (A f) 就好了？但是，当我尝试导出 Ord (A f) 时，它失败了。当约束 class 具有超级 class 时，我不明白如何使用量化约束。我如何导出 Ord (A f) 和其他具有超 classes 的 classes？

> newtype A f = A (f Int)
> deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
> deriving instance (forall a. Ord a => Ord (f a)) => Ord (A f)
<interactive>:3:1: error:
    • Could not deduce (Ord a)
        arising from the superclasses of an instance declaration
      from the context: forall a. Ord a => Ord (f a)
        bound by the instance declaration at <interactive>:3:1-61
      or from: Eq a bound by a quantified context at <interactive>:1:1
      Possible fix: add (Ord a) to the context of a quantified context
    • In the instance declaration for 'Ord (A f)'

PS。我也检查了 ghc proposals 0109-quantified-constraints。使用 ghc 8.6.5

Answer 1

问题是 Eq 是 Ord 的超类，约束 (forall a. Ord a => Ord (f a)) 不包含声明 [=] 所需的超类约束 Eq (A f) 16=]实例.

我们有(forall a. Ord a => Ord (f a))
我们需要Eq (A f)，即(forall a. Eq a => Eq (f a))，这不是我们所拥有的。

解决方案：将 (forall a. Eq a => Eq (f a)) 添加到 Ord 实例。

（我其实不明白GHC给出的错误信息和问题有什么关系。）

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

newtype A f = A (f Int)
deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
deriving instance (forall a. Eq a => Eq (f a), forall a. Ord a => Ord (f a)) => Ord (A f)

或者更整齐一点：

{-# LANGUAGE ConstraintKinds, RankNTypes, KindSignatures, QuantifiedConstraints, StandaloneDeriving, UndecidableInstances, FlexibleContexts #-}

import Data.Kind (Constraint)

type Eq1 f = (forall a. Eq a => Eq (f a) :: Constraint)
type Ord1 f = (forall a. Ord a => Ord (f a) :: Constraint)  -- I also wanted to put Eq1 in here but was getting some impredicativity errors...

-----

newtype A f = A (f Int)
deriving instance Eq1 f => Eq (A f)
deriving instance (Eq1 f, Ord1 f) => Ord (A f)

导出具有量化约束的 Ord (forall a. Ord a => Ord (f a))

Derive Ord with Quantified Constraints (forall a. Ord a => Ord (f a))

haskell

derived-class

typeclass

quantified-constraints