时间戳

首页 > 解决方案 > 尽管在量化约束中被提及，但 GHC 无法推断存在实例

haskell - 尽管在量化约束中被提及，但 GHC 无法推断存在实例

问题描述

我有以下程序：

{-# 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提供实例（来自Hackage 上的库）。这是完全可行的，并且是大部分工作。最后一步就是简单地说。但是，GHC 似乎拒绝接受这一点，即使我在实例声明中添加了必要的约束：EffectGenericKkind-genericsweaveFromToinstance Effect (HigherOrder e) where weave f = weaveFromTo fEffect (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安装，上面的代码应该可以工作。

标签： haskell

解决方案

您不需要使用 a 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 ein 时kind-generics，总是在任何量化之外给它一个明确的名字。否则，您最终会遇到奇怪的错误，例如您遇到的错误。

推荐阅读