[Haskell-cafe] Problem type checking class-method implementation

[Stefan Holdermans]

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

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

Note 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Processor.hs
Type: application/octet-stream
Size: 1495 bytes
Desc: not available
Url : http://www.haskell.org//pipermail/haskell-cafe/attachments/20050803/649f941e/Processor.obj
-------------- next part --------------


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/