特化未使用的类型变量时不可触及的类型

Question

我正在为我的 haskell 程序创建一个 eDSL，它允许定义一组指令来存储数据。这些指令可能会相互依赖结果，甚至被序列化为文件以进一步恢复。这是我想出的东西（相当冗长，但这是我可以提取的最少代码量来重现我的问题）：

{-# LANGUAGE TypeFamilies, RankNTypes, ExistentialQuantification, FlexibleContexts #-}
module Untouchable where

import Control.Applicative
import Control.Monad.Writer
import System.Random

class ResultClass e where
  type ResultMonad :: * -> *
  statementAResult :: ResultMonad (e Int)
  literalResult    :: a -> ResultMonad (e a)

data Statement result = StatementA | StatementB (result Int)
data StatementWithResult result t = StatementWithResult (Statement result, result t)
data AnyStatementWithResult result = forall t. AnyStatementWithResult (StatementWithResult result     t)
type Program result a = (ResultClass result, ResultMonad ~ m) => WriterT [AnyStatementWithResult     result] m a

doA :: Program result (result Int)
doA = do
  r <- lift statementAResult
  tell [AnyStatementWithResult $ StatementWithResult (StatementA, r)]
  return r

doB :: result Int -> Program result ()
doB arg = do
  r <- lift $ literalResult ()
  tell [AnyStatementWithResult $ StatementWithResult (StatementB arg, r)]

prog :: Program result ()
prog = do
  x <- doA
  doB x

data PrettyPrintResult x = PrettyPrintResult Int
  deriving Show

instance ResultClass PrettyPrintResult where
  type ResultMonad = IO
  statementAResult = PrettyPrintResult <$> randomIO
  literalResult _ = PrettyPrintResult <$> randomIO

printProg :: Program PrettyPrintResult a -> IO ()
printProg p = do
  stmts <- execWriterT p
  forM_ stmts $ \(AnyStatementWithResult (StatementWithResult (stmt, r))) -> do
    putStrLn $ "Statement: " ++ case stmt of
      StatementA -> "A"
      StatementB arg -> "B with arg " ++ show arg
    putStrLn $ "Result: " ++ show r

test :: IO ()
test = printProg prog

问题本身在于printProg期望漂亮地打印 eDSL 块的函数。我希望它能够独立于返回类型而适用于所有程序。但 GHC 抱怨：

untouchable.hs: line 52, column 18:
  Couldn't match type `a0' with `()'
    `a0' is untouchable
      inside the constraints (ResultClass PrettyPrintResult,
                              ResultMonad ~ m)
      bound by a type expected by the context:
                 (ResultClass PrettyPrintResult, ResultMonad ~ m) =>
                 WriterT [AnyStatementWithResult PrettyPrintResult] m a0
      at untouchable.hs:52:8-21
  Expected type: WriterT
                   [AnyStatementWithResult PrettyPrintResult] m a0
    Actual type: WriterT
                   [AnyStatementWithResult PrettyPrintResult] m ()
  In the first argument of `printProg', namely `prog'
  In the expression: printProg prog

如果我printProg用Program PrettyPrintResult () -> IO ()一切替换签名，甚至可以按预期工作。

那么问题来了，为什么 GHC 匹配失败的类型变量，实际上是被代码忽略了？我怎么能重写printProg（或者可能是代码的其他部分）它会接受所有程序而不管它们的结果类型如何？

Answer 1

这与 的类型同义词中的约束有关Program。更换的类型签名printProg与真正的类型：

printProg :: WriterT [AnyStatementWithResult PrettyPrintResult] IO a -> IO () 

它会编译。m ~ ResultMonad必须确定约束（给定的maResultMonad是给定的result吗？），但m是存在的，并且不存在其他信息来帮助确定这一点。为什么错误谈到a不可触碰，我不知道。如果您想要好的类型错误，请不要在类型同义词中放置约束！以下更改也可以解决您的问题：

type Program result a = 
  (ResultClass result) => WriterT [AnyStatementWithResult result] ResultMonad a

最后，这些问题是更大问题的征兆。请注意以下事项：

*Untouchable> :t lift statementAResult
lift statementAResult
  :: (ResultClass e, MonadTrans t) => t IO (e Int)

该ResultMonad立刻变得IO！这当然是错误的。发生这种情况的原因是lift有一个Monad约束，并且没有办法得到Monad ResultMonad- 因为ResultMonad取决于 type result，但在任何地方ResultMonad都没有result。本质上，您的result和ResultMonad类型已变得完全无关。

简单的解决方法是使用函数依赖而不是类型族：

class Monad m => ResultClass e m | e -> m where
  statementAResult :: m (e Int)
  literalResult    :: a -> m (e a)

您不需要Monad m约束，但大概您的结果 monad 必须始终是 monad。然后，Program简单地编写您的类型，没有任何限制：

type Program result m a = WriterT [AnyStatementWithResult result] m a

并将所有约束放在它们出现的函数类型中：

doA :: ResultClass result m => Program result m (result Int)

doB :: ResultClass result m => result Int -> Program result m ()

prog :: ResultClass result m => Program result m ()

-- etc ...

不是现在使用lift不再“忘记”你的结果 monad 类型：

*Untouchable> :t lift statementAResult
lift statementAResult
  :: (ResultClass e m, MonadTrans t) => t m (e Int)