给定其值类型的强制转换，对新类型化的reader monad进行强制转换。

Question

拥有相应数据类型族X的类型类C需要函数coerceX。如果我按照下面的方式实现类型类，那么我该如何编写coerceX 函数？

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}

import Data.Type.Coercion
import Control.Monad.Reader

data (T r t)

class C t where
  data X t :: * -> *
  coerceX :: Coercion a b -> Coercion (X t a) (X t b)

instance (C t) => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX = ...

- æons

Answer 1

你可以使用构造函数Coercion进行模式匹配，并对新值使用相同的构造函数Coercion。模式匹配将在范围内引入约束条件Coercible a b，使用Coercion作为结果将使用该约束条件来证明所需的Coercible (X (T r) a) (X (T r) b)。

实际上，这种方法可以编译通过。魔法发生在最后一行，编译器会自动推断进入作用域的约束条件及结果所需的约束条件是否满足要求。然后编译器会验证假定的约束条件确实意味着给定数据类型data X (T r) a的所需条件。

{-# LANGUAGE TypeFamilies #-}

import Data.Type.Coercion
import Control.Monad.Trans.Reader

class C t where
  data X t :: * -> *
  coerceX :: Coercion a b -> Coercion (X t a) (X t b)

data T r = Unused

instance C (T r) where
  newtype X (T r) a = X (Reader r a)
  coerceX Coercion = Coercion

---

自上面的回答写出来以后，问题已经发生了变化。 对于更新后的问题，我认为我们需要要求一个量化的约束条件来进行类型检查。

instance
    (forall a b . Coercible a b
               => Coercible (X (T r t) a) (X (T r t) b))
    => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX :: Coercion a b -> Coercion (X (T r t) a) (X (T r t) b)
  coerceX Coercion = Coercion

我不确定这个以后会怎么使用。

- chi

---

谢谢你的回答，chi。我的问题实际上更加复杂，你能否再看一下编辑后的问题？ - æons

我忘记在我的实现中添加（C t）约束，所以我又进行了编辑。必须以某种方式使用来自（C t）的coerceX，但是对类型应用版本进行模式匹配似乎行不通。 - æons

Answer 2

看起来你可以通过必要的强制转换来引导 GHC，就像这样：

{-# LANGUAGE InstanceSigs #-}
instance (C t) => C (T r t) where
  newtype X (T r t) a = X (Reader r (X t a))
  coerceX :: forall a b. Coercion a b -> Coercion (X (T r t) a) (X (T r t) b)
  coerceX Coercion
    = gcoerceWith (coerceX Coercion :: Coercion (X t a) (X t b)) $
        (Coercion :: Coercion (X (T r t) a) (Reader r (X t a))) `trans`
        (Coercion :: Coercible a' b' => Coercion (Reader r a') (Reader r b')) `trans`
        (Coercion :: Coercion (Reader r (X t b)) (X (T r t) b))

一旦模式匹配：

coerceX Coercion = ...

将Coercible a b引入范围，我认为你需要显式调用coerceX来获取C t实例的Coercion (X t a) (X t b)。我不知道GHC如何自动推导这一点。

现在，在理想的情况下，只需编写以下内容即可：

coerceX Coercion = gcoerceWith (coerceX Coercion :: Coercion (X t a) (X t b)) Coercion

当作用域中存在 Coercible (X t a) (X t b) 时， GHC 可以推断出 Reader r (X t a) 和 Reader r (X t b) 的代表性相等，进而推断出 X (T r t) a 和 X (T r t) b 的代表性相等，但它不能完全做到这一点。

- K. A. Buhr