GHC尽管在量化的约束中被提及，但仍无法推断出实例

Question

我有以下程序：

{-# language MultiParamTypeClasses #-}
{-# language PolyKinds #-}
{-# language QuantifiedConstraints #-}
{-# language RankNTypes #-}
{-# language ScopedTypeVariables #-}
{-# language TypeApplications #-}
{-# language UndecidableInstances #-}
module Control.IO.GWeave where
import Generics.Kind

newtype HigherOrder e m a =
  HigherOrder ( e m a )

weaveFromTo
  :: forall m n e a code.
     ( GenericK e ( LoT2 n a )
     , GenericK e ( LoT2 m a )
     , GWeave ( RepK e ) m n ( LoT2 m a ) ( LoT2 n a )
     )
  => ( forall x. m x -> n x ) -> HigherOrder e m a -> HigherOrder e n a
weaveFromTo eta ( HigherOrder a ) =
    HigherOrder ( toK ( gweave @_ @m @n @( LoT2 m a ) @( LoT2 n a ) eta ( fromK a ) ) )
class GWeave f ( m :: * -> * ) ( n :: * -> * ) as bs where
  gweave :: ( forall x. m x -> n x ) -> f as -> f bs
class Effect e where
  weave :: ( forall x. m x -> n x ) -> e m a -> e n a
instance
  ( forall n a. GenericK e ( LoT2 n a )
  , forall m n a. GWeave ( RepK e ) m n ( LoT2 m a ) ( LoT2 n a )
  ) => Effect ( HigherOrder e ) where
  weave eta =
    weaveFromTo eta

在此，我有class Effect e where weave = ...。我想使用DerivingVia为GenericK实例提供Effect的实例(来自Hackage上的kind-generics库(。这是完全可行的，weaveFromTo是工作的大部分。最后一步是简单地说instance Effect (HigherOrder e) where weave f = weaveFromTo f。但是，GHC似乎拒绝接受这一点，即使我在Effect (HigherOrder e)的实例声明中添加了必要的约束：

• Could not deduce (GWeave (RepK e) m n (LoT2 m a) (LoT2 n a))
  from the context: (forall (n :: * -> *) (a :: k).
                     GenericK e (LoT2 n a),
                     forall (m :: * -> *) (n :: * -> *) (a :: k).
                     GWeave (RepK e) m n (LoT2 m a) (LoT2 n a))
    bound by an instance declaration:
               forall k (e :: (* -> *) -> k -> *).
               (forall (n :: * -> *) (a :: k). GenericK e (LoT2 n a),
                forall (m :: * -> *) (n :: * -> *) (a :: k).
                GWeave (RepK e) m n (LoT2 m a) (LoT2 n a)) =>
               Effect (HigherOrder e)

我无法弄清楚为什么GHC不开心。谁能看到问题？如果您安装了kind-generics，则上述代码应工作。

Answer 1

您不需要使用newtype，只需将类型的family应用程序RepK e移动到量化之外(更改在标记为(!)的行中(：

instance
  ( forall n a. GenericK e ( LoT2 n a )
  , r ~ ( RepK e )  -- (!)
  , forall m n a. GWeave r m n ( LoT2 m a ) ( LoT2 n a )
  ) => Effect ( HigherOrder e ) where
  weave eta =
    weaveFromTo eta

这是因为，根据设计，Haskell中的实例不能使用类型的家庭。也就是说，您无法编写看起来像：

的实例

instance Eq (RepK e) where ...

量化的约束继承了限制，因为它们引入了"本地实例"。您可以在GHC跟踪器和此reddit线程中找到更多信息。

作为额外的建议，每次您在kind-generics中使用RepK e时，请始终在任何量化之外给它一个明确的名称。否则，您最终会遇到奇怪的错误。

Answer 2

好吧，我找到了解决方案 - 我必须将 RepK打包到newtype中：

weaveFromTo
  :: forall m n e a code.
     ( GenericK e ( n :&&: a :&&: LoT0 )
     , GenericK e ( m :&&: a :&&: LoT0 )
     , GWeave ( WrappedRepK e ) m n ( LoT2 m a ) ( LoT2 n a )
     )
  => ( forall x. m x -> n x ) -> HigherOrder e m a -> HigherOrder e n a
weaveFromTo eta ( HigherOrder a ) =
    HigherOrder ( toK ( unWrapRepK ( gweave @_ @m @n @( LoT2 m a ) @( LoT2 n a ) eta ( WrapRepK @e ( fromK a ) ) ) ) )
class GWeave f ( m :: * -> * ) ( n :: * -> * ) as bs where
  gweave :: ( forall x. m x -> n x ) -> f as -> f bs
instance GWeave ( RepK e ) m n ( LoT2 m a ) ( LoT2 n a ) => GWeave ( WrappedRepK e ) m n ( LoT2 m a ) ( LoT2 n a ) where
  gweave eta ( WrapRepK a ) =
    WrapRepK ( gweave eta a )

instance
  ( forall n a. GenericK e ( LoT2 n a )
  , forall m n a. GWeave ( WrappedRepK e ) m n ( m :&&: a :&&: LoT0 ) ( n :&&: a :&&: LoT0 )
  ) => Effect ( HigherOrder e ) where
  weave eta =
    weaveFromTo eta
newtype WrappedRepK r a =
  WrapRepK { unWrapRepK :: RepK r a }

我认为这是因为RepK是一个类型的家庭，所以...有些事情变得棘手吗？我想了解更多有关此修复程序为什么有效的信息。