Dear Haskellers,Yesterday I stumbled upon a problem type checking a program involving multi-parameter type classes. GHC rejected the program; still, I was not immediately convinced it contained a type error. Having given it some more thoughts, I start to suspect that the type checker is in err and that the program is well-typed after all. But, well, I might be overlooking something obvious...
I have reduced my code to a small but hopelessly contrived example program exposing the problem. Please hang on.
Because we employ multi-parameter type classes, we need the Glasgow extensions:
{-# OPTIONS -fglasgow-exts #-}
Let's start easy and define the identity monad:
newtype Identity a = Identity {runIdentity :: a}
instance Monad Identity where
return = Identity
Identity a >>= f = f a
Then, let's introduce the foundations for the (contrived) example:
class (Monad m) => IsItem m i where
processItem :: i -> m ()
class (Monad m) => IsProcessor p m | m -> p where
process :: (IsItem m i) => i -> m ()
-- ...some more methods, possibly involving p...
So, an item is something that can be processed within the context of a
certain monad, and a processor is something that can process an item of
an appropriate type. Note the functional dependency from m to p: a
processor type m uniquely determines the type of the processing context
p.
Before we move on, consider this canonical item type, which is just a one-field record representing an implementation of the IsItem class:
newtype Item m = Item {processItemImpl :: m ()}
The corresponding instance declaration is obvious:
instance (Monad m) => IsItem m (Item m) where
processItem = processItemImpl
Furthermore values of every type that is an instance of IsItem can be
converted to corresponding Item values:
toItem :: (IsItem m i) => i -> Item m toItem = Item . processItemPlease stick with me, for we are now going to implement a monad transformer for processors (which, for this example, is really just the identity monad transformer):
newtype ProcessorT p m a = ProcessorT {runProcessorT :: m a}
instance (Monad m) => Monad (ProcessorT p m) where
return = ProcessorT . return
ProcessorT m >>= f = ProcessorT (m >>= runProcessorT . f)
instance (Monad m) => IsProcessor p (ProcessorT p m) where
process = processItem
Then, finally, we use this transformer to derive a processor monad:
newtype Processor p a = Processor {unwrap :: ProcessorT p Identity a}
runProcessor :: Processor p a -> a
runProcessor = runIdentity . runProcessorT . unwrap
So, we just make sure that Processor is a monad:
instance Monad (Processor p) where
return = Processor . return
Processor m >>= f = Processor (m >>= unwrap . f)
Now all what is left to do is declare Processor an instance of
IsProcessor. To this end, we need to be able to cast items for
Processor p to items for ProcessorT p Identity (for all p). The
following function takes care of that:
castItem :: (IsItem (Processor p) i) => i -> Item (ProcessorT p Identity)
castItem = Item . unwrap . processItemNote that up 'til now everything is fine: GHC is happy, I am happy. But then, when all the hard work is done, and we just only have to connect things properly, it just breaks:
instance IsProcessor p (Processor p) where
process = Processor . process . castItem
After adding this last instance declaration, GHC happily reports:
Processor.hs:56:24:
Could not deduce (IsItem (ProcessorT p Identity)
(Item (ProcessorT p1 Identity)))
from the context (IsProcessor p (Processor p),
Monad (Processor p),
IsItem (Processor p) i)
arising from use of `process' at Processor.hs:56:24-30
Probable fix:
add (IsItem (ProcessorT p Identity) (Item (ProcessorT p1
Identity)))
to the class or instance method `process'
or add an instance declaration for
(IsItem (ProcessorT p Identity)
(Item (ProcessorT p1 Identity)))
In the first argument of `(.)', namely `process'
In the second argument of `(.)', namely `process . castItem'
In the definition of `process': process = Processor . (process .
castItem)
Processor.hs:56:34:
Could not deduce (IsItem (Processor p1) i)
from the context (IsProcessor p (Processor p),
Monad (Processor p),
IsItem (Processor p) i)
arising from use of `castItem' at Processor.hs:56:34-41
Probable fix:
add (IsItem (Processor p1) i) to the class or instance method
`process'
or add an instance declaration for (IsItem (Processor p1) i)
In the second argument of `(.)', namely `castItem'
In the second argument of `(.)', namely `process . castItem'
In the definition of `process': process = Processor . (process .
castItem)
It seems to me that the type checker fails to unify p and p1 where it really should. But once again: I may be wrong here. So, could you either explain to me what I'm missing here and why this program is indeed ill-typed, or confirm that it's really just GHC that should be accepting this program.
I have attached a file Processor.hs containing the example program.
Processor.hs
Description: Binary data
Please note that I've only tested this with GHC 6.4. I did not try it (yet) with the version in HEAD. Neither did I investigate how Hugs acts on this code.
I'm aware that there are some workarounds to get past this problem. The most obvious approach to circumventing this issue is to alter the signature of process so that it takes an explicit Item value and put the need for casting (using toItem) to the caller side. But that's just not the point, of course.
I'm sorry for this far too long post, but this issue is quite essential for the code I'm currently working. Reactions, therefore, are much appreciated.
TIA, Stefan http://www.cs.uu.nl/~stefan/
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
