Untouchable types when specializing an unused type variable

Question

I'm creating an eDSL for my haskell program that would allow defining a set of instructions to store data. These instructions may depend on each other results, and even serialized to file to be further restored. Here is something I came up with (rather verbose, but it's the least code amount I could extract to reproduce my problem):

{-# 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

The problem itself lies in the printProg function that is expected to pretty-print an eDSL chunk. I wanted it to be able to work for all programs independent of their return type. But GHC complains:

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

If I replace the signature of printProg with Program PrettyPrintResult () -> IO () everything builds and even works as expected.

So the question is why GHC fails to match a type variable, which is actually ignored by code? How could I rewrite printProg (or maybe other parts of code) that it would accept all the programs regardless of their result type?

Answer 1

This has to do with the constraint in the type synonym for Program. Replace the type signature of printProg with the real type:

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

and it will compile. The constraint m ~ ResultMonad must be decided (is the given m a ResultMonad for the given result?), but the m is existential and no other information exists to help decide this. Why the error talks about a being untouchable, I have no idea. If you want good type errors, don't put constraints in type synonyms! The following change also fixes your problem:

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

And finally, these problems are symptoms of a bigger problem. Note the following:

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

The ResultMonad immediately becomes IO! This is certainly wrong. The reason this happens is lift has a Monad constraint, and there is no way to get Monad ResultMonad - since ResultMonad depends on the type result, but ResultMonad does not have result in it anywhere. Essentially, your result and ResultMonad types have become completely unrelated.

The easy fix is to use a functional dependency instead of a type family:

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

You don't need the Monad m constraint but presumably your result monad must always be a monad. Then, write your Program type simply without any constraints:

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

and put all constraints in the type of functions where they appear:

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 ...

Not that now using lift no longer "forgets" your result monad type:

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