无法将“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）每个字段，但我希望同时强制转换整个数据类型(这是必需的，以便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
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

- Shersh

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在第三个参数上是名义化的，导致Reader在其第二个参数上也是名义化的，从而使您的强制转换失败。您不能使用Flow类型的角色注释来破坏这一点，因为那将应对ReaderT之前的角色注释。

现在，您可能会想知道为什么ReaderT具有名义化的第三个参数。要理解这一点，请考虑其定义：

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不支持像上面那样的角色多态性，因此我们只能使用最严格的角色：名义。

- chi

---

哦，这实际上相当有趣。请注意，如果您导入ReaderT（newtype构造函数是重要部分），则确实会获得coerce ::（Coercible i i'，Coercible o o'）=> Reader i o-> Reader i' o'。但是，即使导入了它，OP的代码也无法正常工作。似乎强制转换求解器忽略newtype上的角色的能力不扩展到data。我不确定这是否是有意还是疏忽或其他什么原因。 - HTNW

@HTNW 这很奇怪。我没有预料到coerce会这样转换类型。看起来 GHC 在 OP 的情况下展开了第一个data定义，但没有展开第二个。 - chi

我认为这个提案实际上可以让OP的代码工作，因为它允许GHC查看data和newtype（只要所有相关构造函数都可见）。不过我不确定。 - HTNW

Answer 2

问题由@chi解释，如果您避免使用ReaderT并使用一个纯文本的 (->) r monad，则不再存在这个问题。

{-# LANGUAGE FlexibleContexts #-}
module Foo where
import Data.Coerce (Coercible, coerce)

newtype RT r o = RT { runR :: r -> o }
data Flow i o = Flow (i -> RT Int o) (o -> i)

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

- Thomas M. DuBuisson