为什么使用QuantifiedConstraints指定类型类的子类也需要该子类的实例？

Question

我正在玩一种多类型的无标签编码 Free

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
module Free where
import GHC.Types

type (a :: k) ~> (b :: k) = Morphism k a b

newtype Natural (f :: j -> k) (g :: j -> k) = 
  Natural { getNatural :: forall (x :: j). f x ~> g x }

type family Morphism k :: k -> k -> Type where
  Morphism Type = (->)
  Morphism (j -> k) = Natural

class DataKind k where
  data Free :: (k -> Constraint) -> k -> k
  interpret :: forall (cls :: k -> Constraint) (u :: k) (v :: k). 
               cls v => (u ~> v) -> (Free cls u ~> v)
  call :: forall (cls :: k -> Constraint) (u :: k). 
          u ~> Free cls u

instance DataKind Type where
  newtype Free cls u = Free0
    { runFree0 :: forall v. cls v => (u ~> v) -> v }
  interpret f = \(Free0 g) -> g f
  call = \u -> Free0 $ \f -> f u

我可以写Semigroup为实例Free Semigroup，并Free Monoid没有问题：

instance Semigroup (Free Semigroup u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

instance Semigroup (Free Monoid u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

这些实例相同，并且适用于的任何其他子类Semigroup。

我想使用它，QuantifiedConstraints所以我可以为以下所有子类编写一个实例Semigroup：

instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

但是编译器（GHC-8.6.3）抱怨它无法推断cls (Free cls u)：

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmsconcat’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmsconcat @(Free cls u)
      In an equation for ‘GHC.Base.sconcat’:
          GHC.Base.sconcat = GHC.Base.$dmsconcat @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        sconcat :: GHC.Base.NonEmpty (Free cls u) -> Free cls u
          (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmstimes’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
      or from: Integral b
        bound by the type signature for:
                   GHC.Base.stimes :: forall b.
                                      Integral b =>
                                      b -> Free cls u -> Free cls u
        at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmstimes @(Free cls u)
      In an equation for ‘GHC.Base.stimes’:
          GHC.Base.stimes = GHC.Base.$dmstimes @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        stimes :: b -> Free cls u -> Free cls u (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

当我将其添加为实例的上下文时，它可以正常编译：

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmsconcat’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmsconcat @(Free cls u)
      In an equation for ‘GHC.Base.sconcat’:
          GHC.Base.sconcat = GHC.Base.$dmsconcat @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        sconcat :: GHC.Base.NonEmpty (Free cls u) -> Free cls u
          (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Free.hs:57:10: error:
    • Could not deduce: cls (Free cls u)
        arising from a use of ‘GHC.Base.$dmstimes’
      from the context: forall v. cls v => Semigroup v
        bound by the instance declaration at Free.hs:57:10-67
      or from: Integral b
        bound by the type signature for:
                   GHC.Base.stimes :: forall b.
                                      Integral b =>
                                      b -> Free cls u -> Free cls u
        at Free.hs:57:10-67
    • In the expression: GHC.Base.$dmstimes @(Free cls u)
      In an equation for ‘GHC.Base.stimes’:
          GHC.Base.stimes = GHC.Base.$dmstimes @(Free cls u)
      In the instance declaration for ‘Semigroup (Free cls u)’
    • Relevant bindings include
        stimes :: b -> Free cls u -> Free cls u (bound at Free.hs:57:10)
   |
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

增加的背景是有点冗长，但由于整点Free是，cls (Free cls u)始终是真实的，没有繁重。

我不明白的是，为什么 GHC需要能够为要编译的实例cls (Free cls u)的子类得出结论。我试图取代的定义与并得到了同样的错误，所以我觉得这个问题是不是在执行本身，而是在实例的声明; 可能是由于某些方面我不了解。SemigroupSemigroup(<>)undefinedQuantifiedConstraints

Answer 1

错误信息说明这些错误来自默认的定义sconcat和stimes。量化上下文的行为类似于instances：在您的内部instance Semigroup (Free cls v)，就好像存在一个instance cls v => Semigroup v范围。instance通过匹配选择。sconcat和stimes想要Semigroup (Free cls v)，因此他们与需求相匹配instance forall z. cls z => Semigroup z，成功z ~ Free cls v并得到进一步的需求cls (Free cls v)。即使我们也有递归操作instance _etc => Semigroup (Free cls v)，也会发生这种情况。记住，我们假设类型类实例是连贯的。使用量化上下文还是使用当前定义的实例应该没有什么区别，因此GHC只会选择感觉上要使用的任何实例。

但是，这不是一个好情况。量化上下文与我们的实例重叠（实际上，它与每个 Semigroup实例重叠），这令人震惊。如果尝试类似的操作(<>) = const (Free0 _etc) ([1, 2] <> [3, 4])，则会得到类似的错误，因为量化的上下文instance Semigroup [a]会使库中的实数蒙上阴影。我认为，包括问题14877中的一些想法可以使此问题不太舒服：

class (a => b) => Implies a b
instance (a => b) => Implies a b
instance (forall v. cls v `Implies` Semigroup v) => Semigroup (Free cls u) where
  Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f

使用Implies此处意味着量化的上下文不再匹配所需的需求，Semigroup (Free cls v)而是通过递归释放了需求。但是，约束背后的要求没有改变。从本质上讲，我们保留量化约束的需求片段，对于用户来说，Semigroup v应该由来隐含cls v，同时在排放片段上拍打安全性以进行实施，因此不会破坏我们的约束分辨率。该Implies限制还是可以的，并已被用来证明Semigroup v的限制(<>)，但它被认为是作为最后的手段明确之后Semigroup情况已耗尽。