haskell - 新类型阅读器单子(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 = ...

Answer 1

看起来你可以通过必要的强制手段来牵制 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带入范围，我认为您需要为C t实例显式调用coerceX以获得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 的表示相等，但它不能完全实现了这一飞跃。