使用复杂类型参数强制记录时出现问题

Question

我有这样的记录：

import Data.Functor.Identity
import Control.Monad.Trans.Identity
import Data.Coerce

data Env m = Env {
        logger :: String -> m ()
    }

env :: Env IO
env = undefined

和这个强制函数

decorate 
    :: Coercible (r_ m) (r_ (IdentityT m))   
    => r_ m -> r_ (IdentityT m)        
decorate = coerce

适用于没有问题的记录值：

decoratedEnv :: Env (IdentityT IO)
decoratedEnv = decorate env

但是，如果我定义唯一稍微复杂的记录

data Env' h m = Env' {
        logger' :: h (String -> m ())
    }

env' :: Env' Identity IO
env' = undefined

IdentityT并尝试像我之前那样插入包装纸

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = decorate env'

我收到错误：

* Couldn't match type `IO' with `IdentityT IO'
    arising from a use of `decorate'

Identity在我看来，所采用的额外参数Env'不应停止coerce工作。为什么coerce在这种情况下会失败？有办法打工coerce吗？

Answer 1

强制Coercible A B并不意味着强制Coercion (h A) (h B)所有人h。

考虑这个 GADT：

data T a where
  K1 :: Int  -> T A
  K2 :: Bool -> T B

强迫T A就T B等于强迫Int，Bool而这显然不应该发生。

仅当我们知道 的参数h具有正确的角色（例如representationalor phantom，但不是nominal）时，我们才能执行该强制转换。

现在，在您的具体情况下h已知（Identity），并且肯定具有正确的角色，因此它应该起作用。我猜GHC强制系统并没有那么强大，无法处理如此“行为良好”的人h，同时拒绝行为不端的人，所以它保守地拒绝一切。

添加一个类型孔似乎证实了这一点。我试过

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = _ decorate' @(Env' Identity)

并得到错误

* Couldn't match representation of type: r_0 m0
                           with that of: r_0 (IdentityT m0)
    arising from a use of decorate'
  NB: We cannot know what roles the parameters to `r_0' have;
    we must assume that the role is nominal
* In the first argument of `_', namely decorate'
  In the expression: _ decorate' @(Env' Identity)
  In an equation for decoratedEnv':
      decoratedEnv' = _ decorate' @(Env' Identity)

“NB：”部分就在现场。

我也尝试着去坚持，去强行扮演这个角色

type role Env' representational representational
data Env' h m = Env' {
        logger' :: h (String -> m ())
    }

无济于事：

* Role mismatch on variable m:
    Annotation says representational but role nominal is required
* while checking a role annotation for Env'

我能找到的最好的解决方法是解开/重新包装，并利用QuantifiedConstraints本质上要求h具有非nominal角色：

decorate' 
    :: (forall a b. Coercible a b => Coercible (h a) (h' b))
    => Coercible m m'
    => Env' h m -> Env' h' m'
decorate' (Env' x) = Env' (coerce x)

decoratedEnv' :: Env' Identity (IdentityT IO)
decoratedEnv' = decorate' env'

这不是一个理想的解决方案，因为它违背了Coercible. 在这种情况下，重新包装只有 O(1) 成本，但如果我们有一个要转换的列表Env' Identity IO，我们将支付 O(N) 成本。