haskell - 不能使用 'coerce' 作为字段的 'Reader' 数据类型

Question

我有以下 Haskell 代码，可以完美编译:

import Control.Monad.Reader (Reader (..))
import Data.Coerce (Coercible, coerce)

data Flow i o = Flow (i -> o) (o -> i)

coerceFlow
    :: (Coercible i i', Coercible o o')
    => Flow i o
    -> Flow i' o'
coerceFlow = coerce

但是，如果我更改 Flow 的定义键入以下内容:

data Flow i o = Flow (i -> Reader Int o) (o -> i)

我开始看到一个奇怪的错误:

Coerce.hs:10:14: error:
    • Couldn't match type ‘o’ with ‘o'’ arising from a use of ‘coerce’
      ‘o’ is a rigid type variable bound by
        the type signature for:
          coerceFlow :: forall i i' o o'.
                        (Coercible i i', Coercible o o') =>
                        Flow i o -> Flow i' o'
        at Coerce.hs:(6,1)-(9,17)
      ‘o'’ is a rigid type variable bound by
        the type signature for:
          coerceFlow :: forall i i' o o'.
                        (Coercible i i', Coercible o o') =>
                        Flow i o -> Flow i' o'
        at Coerce.hs:(6,1)-(9,17)
    • In the expression: coerce
      In an equation for ‘coerceFlow’: coerceFlow = coerce
    • Relevant bindings include
        coerceFlow :: Flow i o -> Flow i' o' (bound at Coerce.hs:10:1)
   |
10 | coerceFlow = coerce
   |              ^^^^^^

据我了解，我的数据类型不再是 Coercible自动地。有没有办法告诉 GHC 我可以强制 Flow 类型的值自动地？我可以 coerce每个字段手动，但我想 coerce一次完整的数据类型( DerivingVia 需要这样做)。

我尝试使用 RoleAnnotations像这样的扩展:

type role Flow representational representational

但我看到一个错误:

Coerce.hs:6:1: error:
    • Role mismatch on variable o:
        Annotation says representational but role nominal is required
    • while checking a role annotation for ‘Flow’
  |
6 | type role Flow representational representational
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Answer 1

让我们调查一下:

> :info Reader
type Reader r = ReaderT r Data.Functor.Identity.Identity :: * -> *
        -- Defined in `Control.Monad.Trans.Reader'

所以， Reader定义为 ReaderT .

> :info ReaderT
type role ReaderT representational representational nominal
newtype ReaderT r (m :: k -> *) (a :: k)
  = ReaderT {runReaderT :: r -> m a}
        -- Defined in `Control.Monad.Trans.Reader'

...和 ReaderT是 nominal在它的第三个参数上，导致 Reader成为 nominal在第二个论点中，并使您的强制失败。您无法使用 Flow 的角色注释来颠覆这一点。类型，因为这将处理 ReaderT 的先前角色注释.

现在，您可能想知道为什么 ReaderT有一个 nominal第三个论点。要理解这一点，请考虑其定义:

newtype ReaderT r m a = ReaderT (r -> m a)

a应该是什么角色| ， 以上？这得看情况。如果 m :: * -> *是 representational在它的论点上，然后 ReaderT在 a 上是这样的. nominal 也是如此。和 phantom .在这里表达角色的“最佳”方式是使用角色多态性，例如

type role forall r .
     ReaderT representational (representational :: (* with role r) -> *) r

其中第三个参数的作用取决于第二个更高种类的参数。

唉，GHC 不支持像上面那样的角色多态性，所以我们只能使用最严格的角色: nominal .