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为任何数据类型提供Effect的实例，这些数据类型是GenericK的实例(来自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，只需将类型族应用程序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 tracker和此Reddit thread中找到更多信息。

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

Answer 2

好了，我找到了解决方案--我必须将RepK打包成一个新类型：

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是一个类型族所以..。有什么不对劲？我很想知道更多关于这个修复为什么有效的信息。