Неприкасаемые типы при использовании переменной неиспользуемого типа

Question

Я создаю eDSL для моей программы haskell, которая позволит определить набор инструкций для хранения данных. Эти инструкции могут зависеть от результатов друг друга и даже сериализоваться в файл для дальнейшего восстановления. Вот то, что я придумал (а многословен, но это наименьшее количество кода я мог бы извлечь воспроизвести мою проблему):

{-# 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 (задано m a ResultMonad для данного 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 зависит от типа 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 ограничения, но предположительно, ваш результат монада всегда должна быть монадой.Затем написать 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 type:

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