Почему использование 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
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Когда я добавляю это как контекст для экземпляра, он прекрасно компилируется:

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

Добавленный контекст немного многословен, но суть Free в том, что cls (Free cls u) всегда верно, а не обременительно.

Что я не понимаю, так это , почему GHC должен иметь возможность заключить cls (Free cls u) для подкласса Semigroup для экземпляра Semigroup для компиляции. Я попытался заменить определение (<>) на undefined и получил ту же ошибку, поэтому я думаю, что проблема не в самой реализации, а в объявлении экземпляра; вероятно, из-за какого-то аспекта QuantifiedConstraints я не понимаю.

Answer 1

В сообщениях об ошибках указано, что эти ошибки получены из значений по умолчанию sconcat и stimes.Количественные контексты действуют как instance s: внутри вашего 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 экземпляров.