尽管在量化约束中提到了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（来自kind-genericsHackage上的库）。这是完全可行的，并且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跟踪器和此Reddit线程中找到更多信息。

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